From 61f393ff8f4179e1184e715679dcbadf871cde06 Mon Sep 17 00:00:00 2001
From: Mikolaj Konarski <mikolaj.konarski@funktory.com>
Date: Wed, 24 Sep 2025 20:56:20 +0200
Subject: WIP

---
 src/Data/Array/Nested/Lemmas.hs      | 4 ++--
 src/Data/Array/Nested/Mixed/Shape.hs | 4 ++--
 src/Data/Array/Nested/Permutation.hs | 1 -
 src/Data/Array/Nested/Types.hs       | 5 +++--
 4 files changed, 7 insertions(+), 7 deletions(-)

(limited to 'src/Data/Array')

diff --git a/src/Data/Array/Nested/Lemmas.hs b/src/Data/Array/Nested/Lemmas.hs
index 8cac298..e8c3b9e 100644
--- a/src/Data/Array/Nested/Lemmas.hs
+++ b/src/Data/Array/Nested/Lemmas.hs
@@ -48,9 +48,9 @@ lemReplicatePlusApp sn _ _ = go sn
     go :: SNat n' -> Replicate (n' + m) a :~: Replicate n' a ++ Replicate m a
     go SZ = Refl
     go (SS (n :: SNat n'm1))
-      | Refl <- lemReplicateSucc @a @n'm1
+      | Refl <- lemReplicateSucc @a n
       , Refl <- go n
-      = sym (lemReplicateSucc @a @(n'm1 + m))
+      = sym (lemReplicateSucc @a (SNat @(n'm1 + m)))
 
 lemDropLenApp :: Rank l1 <= Rank l2
               => Proxy l1 -> Proxy l2 -> Proxy rest
diff --git a/src/Data/Array/Nested/Mixed/Shape.hs b/src/Data/Array/Nested/Mixed/Shape.hs
index de2796b..ffa3613 100644
--- a/src/Data/Array/Nested/Mixed/Shape.hs
+++ b/src/Data/Array/Nested/Mixed/Shape.hs
@@ -563,7 +563,7 @@ ssxLast = coerce (listxLast @(SMayNat () SNat))
 ssxReplicate :: SNat n -> StaticShX (Replicate n Nothing)
 ssxReplicate SZ = ZKX
 ssxReplicate (SS (n :: SNat n'))
-  | Refl <- lemReplicateSucc @(Nothing @Nat) @n'
+  | Refl <- lemReplicateSucc @(Nothing @Nat) n
   = SUnknown () :!% ssxReplicate n
 
 ssxIotaFrom :: StaticShX sh -> Int -> [Int]
@@ -576,7 +576,7 @@ ssxFromShX (n :$% sh) = fromSMayNat (\_ -> SUnknown ()) SKnown n :!% ssxFromShX
 
 ssxFromSNat :: SNat n -> StaticShX (Replicate n Nothing)
 ssxFromSNat SZ = ZKX
-ssxFromSNat (SS (n :: SNat nm1)) | Refl <- lemReplicateSucc @(Nothing @Nat) @nm1 = SUnknown () :!% ssxFromSNat n
+ssxFromSNat (SS (n :: SNat nm1)) | Refl <- lemReplicateSucc @(Nothing @Nat) n = SUnknown () :!% ssxFromSNat n
 
 
 -- | Evidence for the static part of a shape. This pops up only when you are
diff --git a/src/Data/Array/Nested/Permutation.hs b/src/Data/Array/Nested/Permutation.hs
index 03d1640..1eb7be1 100644
--- a/src/Data/Array/Nested/Permutation.hs
+++ b/src/Data/Array/Nested/Permutation.hs
@@ -276,7 +276,6 @@ lemRankDropLen :: forall is sh. (Rank is <= Rank sh)
 lemRankDropLen ZKX PNil = Refl
 lemRankDropLen (_ :!% sh) (_ `PCons` is) | Refl <- lemRankDropLen sh is = Refl
 lemRankDropLen (_ :!% _) PNil = Refl
-lemRankDropLen ZKX (_ `PCons` _) = error "1 <= 0"
 
 lemIndexSucc :: Proxy i -> Proxy a -> Proxy l
              -> Index (i + 1) (a : l) :~: Index i l
diff --git a/src/Data/Array/Nested/Types.hs b/src/Data/Array/Nested/Types.hs
index 4444acd..ba22e97 100644
--- a/src/Data/Array/Nested/Types.hs
+++ b/src/Data/Array/Nested/Types.hs
@@ -109,8 +109,9 @@ type family Replicate n a where
   Replicate 0 a = '[]
   Replicate n a = a : Replicate (n - 1) a
 
-lemReplicateSucc :: (a : Replicate n a) :~: Replicate (n + 1) a
-lemReplicateSucc = unsafeCoerceRefl
+lemReplicateSucc :: forall a n.
+                    SNat n -> (a : Replicate n a) :~: Replicate (n + 1) a
+lemReplicateSucc _ = unsafeCoerceRefl
 
 type family MapJust l = r | r -> l where
   MapJust '[] = '[]
-- 
cgit v1.2.3-70-g09d2