diff options
| author | Tom Smeding <tom@tomsmeding.com> | 2024-05-18 19:14:03 +0200 |
|---|---|---|
| committer | Tom Smeding <tom@tomsmeding.com> | 2024-05-18 19:14:03 +0200 |
| commit | 958f0ded6eca13ae0e1a7011bfd14ba9d8300541 (patch) | |
| tree | f6756b01fab96c6bc5aac25f3f936e5cfc3a17a6 | |
| parent | 6b5139c0a8d0c4e76c349f2847cc5629137f4536 (diff) | |
Put KnownNat inside ListS; REVERT ME LATER
| -rw-r--r-- | src/Data/Array/Nested/Internal.hs | 10 |
1 files changed, 5 insertions, 5 deletions
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) |