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')
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