diff options
Diffstat (limited to 'src/Data')
| -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) |