diff options
| author | Tom Smeding <tom@tomsmeding.com> | 2025-05-16 12:25:44 +0200 |
|---|---|---|
| committer | Tom Smeding <tom@tomsmeding.com> | 2025-05-16 12:25:44 +0200 |
| commit | f969fb5d6172761a2148221b68a0384b53368f8c (patch) | |
| tree | a8a587547787493e40ca510dd532f182a4bac861 /src/Data | |
| parent | 26b8f3c19cd919f5a45ef07e4ba76bae5cab35ce (diff) | |
Revert "Remove the KnownNat constraint from (:5509)"
This reverts commit 8890526cac9e6c4d5583d00fce55f32ba613cf31.
Removing a _provided_ KnownNat constraint if we cannot remove the actual
Nat information from the data type is rather pointless.
Diffstat (limited to 'src/Data')
| -rw-r--r-- | src/Data/Array/Nested/Shaped/Shape.hs | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/Data/Array/Nested/Shaped/Shape.hs b/src/Data/Array/Nested/Shaped/Shape.hs index 8553b56..5a1003f 100644 --- a/src/Data/Array/Nested/Shaped/Shape.hs +++ b/src/Data/Array/Nested/Shaped/Shape.hs @@ -229,11 +229,11 @@ ixsRank (IxS l) = listsRank l ixsZero :: ShS sh -> IIxS sh ixsZero ZSS = ZIS -ixsZero (SNat :$$ sh) = 0 :.$ ixsZero sh +ixsZero (_ :$$ sh) = 0 :.$ ixsZero sh ixsFromIxX :: ShS sh -> IIxX (MapJust sh) -> IIxS sh ixsFromIxX ZSS ZIX = ZIS -ixsFromIxX (SNat :$$ sh) (n :.% idx) = n :.$ ixsFromIxX sh idx +ixsFromIxX (_ :$$ sh) (n :.% idx) = n :.$ ixsFromIxX sh idx ixxFromIxS :: IIxS sh -> IIxX (MapJust sh) ixxFromIxS ZIS = ZIX @@ -280,10 +280,10 @@ 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 (listsUncons -> Just (UnconsListSRes (ShS -> shl) i)) - where i@SNat :$$ ShS shl = ShS (i ::$ shl) + where i :$$ ShS shl = ShS (i ::$ shl) infixr 3 :$$ @@ -400,7 +400,7 @@ instance KnownShS sh => IsList (ListS sh (Const i)) where where go :: ShS sh' -> [i] -> ListS sh' (Const i) go ZSS [] = ZS - go (SNat :$$ sh) (i : is) = Const i ::$ go sh is + go (_ :$$ sh) (i : is) = Const i ::$ go sh is go _ _ = error $ "IsList(ListS): Mismatched list length (type says " ++ show (shsLength (knownShS @sh)) ++ ", list has length " ++ show (length topl) ++ ")" @@ -419,7 +419,7 @@ instance KnownShS sh => IsList (ShS sh) where where go :: ShS sh' -> [Int] -> ListS sh' SNat go ZSS [] = ZS - go (sn@SNat :$$ sh) (i : is) + go (sn :$$ sh) (i : is) | i == fromSNat' sn = sn ::$ go sh is | otherwise = error $ "IsList(ShS): Value does not match typing (type says " ++ show (fromSNat' sn) ++ ", list contains " ++ show i ++ ")" |