From 24d93b59d75c1ea11f4443965d681236c459b439 Mon Sep 17 00:00:00 2001 From: Mikolaj Konarski Date: Fri, 26 Sep 2025 21:09:23 +0200 Subject: Done --- src/Data/Array/Nested/Convert.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/Data/Array/Nested/Convert.hs') diff --git a/src/Data/Array/Nested/Convert.hs b/src/Data/Array/Nested/Convert.hs index 2438f68..07777d5 100644 --- a/src/Data/Array/Nested/Convert.hs +++ b/src/Data/Array/Nested/Convert.hs @@ -136,7 +136,7 @@ shsFromSSX = shsFromShX Prelude.. shxFromSSX ixxFromIxR :: IxR n i -> IxX (Replicate n Nothing) i ixxFromIxR ZIR = ZIX ixxFromIxR (n :.: (idx :: IxR m i)) = - castWith (subst2 @IxX @i (lemReplicateSucc @(Nothing @Nat) @m)) + castWith (subst2 @IxX @i (lemReplicateSucc @(Nothing @Nat) (Proxy @m))) (n :.% ixxFromIxR idx) ixxFromIxS :: IxS sh i -> IxX (MapJust sh) i @@ -146,7 +146,7 @@ ixxFromIxS (n :.$ sh) = n :.% ixxFromIxS sh shxFromShR :: ShR n i -> ShX (Replicate n Nothing) i shxFromShR ZSR = ZSX shxFromShR (n :$: (idx :: ShR m i)) = - castWith (subst2 @ShX @i (lemReplicateSucc @(Nothing @Nat) @m)) + castWith (subst2 @ShX @i (lemReplicateSucc @(Nothing @Nat) (Proxy @m))) (SUnknown n :$% shxFromShR idx) shxFromShS :: ShS sh -> IShX (MapJust sh) -- cgit v1.2.3-70-g09d2