diff options
| -rw-r--r-- | src/Data/Array/Nested/Internal.hs | 22 |
1 files changed, 13 insertions, 9 deletions
diff --git a/src/Data/Array/Nested/Internal.hs b/src/Data/Array/Nested/Internal.hs index 594abd4..efb9dc6 100644 --- a/src/Data/Array/Nested/Internal.hs +++ b/src/Data/Array/Nested/Internal.hs @@ -695,7 +695,7 @@ instance (Elt a, KnownINat n) => Elt (Ranked n a) where -- | The shape of a shape-typed array given as a list of 'SNat' values. data SShape sh where ShNil :: SShape '[] - ShCons :: SNat n -> SShape sh -> SShape (n : sh) + ShCons :: KnownShape sh => SNat n -> SShape sh -> SShape (n : sh) deriving instance Show (SShape sh) infixr 5 `ShCons` @@ -1079,7 +1079,8 @@ type role ListS nominal representational type ListS :: [Nat] -> Type -> Type data ListS sh i where ZS :: ListS '[] i - (::$) :: forall n sh {i}. i -> ListS sh i -> ListS (n : sh) i + (::$) :: forall n sh {i}. (KnownNat n, KnownShape sh) + => i -> ListS sh i -> ListS (n : sh) i deriving instance Show i => Show (ListS sh i) deriving instance Eq i => Eq (ListS sh i) deriving instance Ord i => Ord (ListS sh i) @@ -1115,7 +1116,7 @@ pattern ZIS = IxS ZS pattern (:.$) :: forall {sh1} {i}. - forall n sh. (n : sh ~ sh1) + forall n sh. (KnownNat n, KnownShape sh, n : sh ~ sh1) => i -> IxS sh i -> IxS sh1 i pattern i :.$ shl <- (unconsIxS -> Just (UnconsIxSRes shl i)) where i :.$ (IxS shl) = IxS (i ::$ shl) @@ -1123,7 +1124,8 @@ pattern i :.$ shl <- (unconsIxS -> Just (UnconsIxSRes shl i)) infixr 3 :.$ data UnconsIxSRes i sh1 = - forall n sh. (n : sh ~ sh1) => UnconsIxSRes (IxS sh i) i + forall n sh. (KnownNat n, KnownShape sh, n : sh ~ sh1) + => UnconsIxSRes (IxS sh i) i unconsIxS :: IxS sh1 i -> Maybe (UnconsIxSRes i sh1) unconsIxS (IxS shl) = case shl of i ::$ shl' -> Just (UnconsIxSRes (IxS shl') i) @@ -1146,7 +1148,7 @@ pattern ZSS = StaticShapeS ZS pattern (:$$) :: forall {sh1} {i}. - forall n sh. (n : sh ~ sh1) + forall n sh. (KnownNat n, KnownShape sh, n : sh ~ sh1) => i -> StaticShapeS sh i -> StaticShapeS sh1 i pattern i :$$ shl <- (unconsStaticShapeS -> Just (UnconsStaticShapeSRes shl i)) where i :$$ (StaticShapeS shl) = StaticShapeS (i ::$ shl) @@ -1154,7 +1156,8 @@ pattern i :$$ shl <- (unconsStaticShapeS -> Just (UnconsStaticShapeSRes shl i)) infixr 3 :$$ data UnconsStaticShapeSRes i sh1 = - forall n sh. (n : sh ~ sh1) => UnconsStaticShapeSRes (StaticShapeS sh i) i + forall n sh. (KnownNat n, KnownShape sh, n : sh ~ sh1) + => UnconsStaticShapeSRes (StaticShapeS sh i) i unconsStaticShapeS :: StaticShapeS sh1 i -> Maybe (UnconsStaticShapeSRes i sh1) unconsStaticShapeS (StaticShapeS shl) = case shl of i ::$ shl' -> Just (UnconsStaticShapeSRes (StaticShapeS shl') i) @@ -1162,15 +1165,16 @@ unconsStaticShapeS (StaticShapeS shl) = case shl of zeroIxS :: SShape sh -> IIxS sh zeroIxS ShNil = ZIS -zeroIxS (ShCons _ sh) = 0 :.$ zeroIxS sh +zeroIxS (ShCons GHC_SNat sh) = 0 :.$ zeroIxS sh cvtSShapeIxS :: SShape sh -> IIxS sh cvtSShapeIxS ShNil = ZIS -cvtSShapeIxS (ShCons n sh) = fromIntegral (fromSNat n) :.$ cvtSShapeIxS sh +cvtSShapeIxS (ShCons n@GHC_SNat sh) = + fromIntegral (fromSNat n) :.$ cvtSShapeIxS sh ixCvtXS :: SShape sh -> IIxX (MapJust sh) -> IIxS sh ixCvtXS ShNil ZIX = ZIS -ixCvtXS (ShCons _ sh) (n :.@ idx) = n :.$ ixCvtXS sh idx +ixCvtXS (ShCons GHC_SNat sh) (n :.@ idx) = n :.$ ixCvtXS sh idx ixCvtSX :: IIxS sh -> IIxX (MapJust sh) ixCvtSX ZIS = ZIX |