diff options
| author | Mikolaj Konarski <mikolaj.konarski@funktory.com> | 2025-09-24 20:56:20 +0200 |
|---|---|---|
| committer | Mikolaj Konarski <mikolaj.konarski@funktory.com> | 2025-10-02 12:54:23 +0200 |
| commit | 22a3d9c5cbafb7a633f2f802af884d042718e78d (patch) | |
| tree | e0fb4cacfc39f182e2f1e0313bddc8836dbae651 /src/Data/Array/Nested/Convert.hs | |
| parent | 2fae6bf7f6704e3dd9a3f73acbdc84331adb1bf0 (diff) | |
Port to ghc-typelits-natnormalise-0.8.1 that is much overhauledport-to-natnormalise-0.8.1
and probably more sound than earlier versions.
Diffstat (limited to 'src/Data/Array/Nested/Convert.hs')
| -rw-r--r-- | src/Data/Array/Nested/Convert.hs | 4 |
1 files changed, 2 insertions, 2 deletions
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) |