From 958f0ded6eca13ae0e1a7011bfd14ba9d8300541 Mon Sep 17 00:00:00 2001
From: Tom Smeding <tom@tomsmeding.com>
Date: Sat, 18 May 2024 19:14:03 +0200
Subject: Put KnownNat inside ListS; REVERT ME LATER

---
 src/Data/Array/Nested/Internal.hs | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'src/Data/Array/Nested/Internal.hs')

diff --git a/src/Data/Array/Nested/Internal.hs b/src/Data/Array/Nested/Internal.hs
index a3c2b6d..cf90240 100644
--- a/src/Data/Array/Nested/Internal.hs
+++ b/src/Data/Array/Nested/Internal.hs
@@ -255,14 +255,14 @@ type role ListS nominal representational
 type ListS :: [Nat] -> (Nat -> Type) -> Type
 data ListS sh f where
   ZS :: ListS '[] f
-  (::$) :: forall n sh {f}. f n -> ListS sh f -> ListS (n : sh) f
+  (::$) :: forall n sh {f}. KnownNat n => f n -> ListS sh f -> ListS (n : sh) f
 deriving instance (forall n. Show (f n)) => Show (ListS sh f)
 deriving instance (forall n. Eq (f n)) => Eq (ListS sh f)
 deriving instance (forall n. Ord (f n)) => Ord (ListS sh f)
 infixr 3 ::$
 
 data UnconsListSRes f sh1 =
-  forall n sh. (n : sh ~ sh1) => UnconsListSRes (ListS sh f) (f n)
+  forall n sh. (KnownNat n, n : sh ~ sh1) => UnconsListSRes (ListS sh f) (f n)
 unconsListS :: ListS sh1 f -> Maybe (UnconsListSRes f sh1)
 unconsListS (x ::$ sh') = Just (UnconsListSRes sh' x)
 unconsListS ZS = Nothing
@@ -292,7 +292,7 @@ pattern ZIS = IxS ZS
 
 pattern (:.$)
   :: forall {sh1} {i}.
-     forall n sh. (n : sh ~ sh1)
+     forall n sh. (KnownNat n, n : sh ~ sh1)
   => i -> IxS sh i -> IxS sh1 i
 pattern i :.$ shl <- IxS (unconsListS -> Just (UnconsListSRes (IxS -> shl) (getConst -> i)))
   where i :.$ IxS shl = IxS (Const i ::$ shl)
@@ -320,7 +320,7 @@ pattern ZSS = ShS ZS
 
 pattern (:$$)
   :: forall {sh1}.
-     forall n sh. (n : sh ~ sh1)
+     forall n sh. (KnownNat n, n : sh ~ sh1)
   => SNat n -> ShS sh -> ShS sh1
 pattern i :$$ shl <- ShS (unconsListS -> Just (UnconsListSRes (ShS -> shl) i))
   where i :$$ ShS shl = ShS (i ::$ shl)
@@ -1345,7 +1345,7 @@ type family Tail l where
 
 shCvtXS' :: forall sh. IShX (MapJust sh) -> ShS sh
 shCvtXS' ZSX = castWith (subst1 (unsafeCoerce Refl :: '[] :~: sh)) ZSS
-shCvtXS' (SKnown n :$% (idx :: IShX mjshT)) =
+shCvtXS' (SKnown n@SNat :$% (idx :: IShX mjshT)) =
   castWith (subst1 (lem Refl)) $
     n :$$ shCvtXS' @(Tail sh) (castWith (subst2 (unsafeCoerce Refl :: mjshT :~: MapJust (Tail sh)))
                                  idx)
-- 
cgit v1.2.3-70-g09d2