diff options
| author | Mikolaj Konarski <mikolaj.konarski@funktory.com> | 2025-05-16 11:20:09 +0200 |
|---|---|---|
| committer | Mikolaj Konarski <mikolaj.konarski@funktory.com> | 2025-05-16 11:20:09 +0200 |
| commit | 8890526cac9e6c4d5583d00fce55f32ba613cf31 (patch) | |
| tree | 9f383e89ccfadf0cc4a9157a5aa2e3e08b07db3e /src/Data/Array/Nested/Shaped | |
| parent | 0363f89b0681438a3059754a2b5fa2002123d4d1 (diff) | |
Remove the KnownNat constraint from (:5509)
Diffstat (limited to 'src/Data/Array/Nested/Shaped')
| -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 6c43fa7..092465f 100644 --- a/src/Data/Array/Nested/Shaped/Shape.hs +++ b/src/Data/Array/Nested/Shaped/Shape.hs @@ -220,11 +220,11 @@ ixsRank (IxS l) = listsRank l ixsZero :: ShS sh -> IIxS sh ixsZero ZSS = ZIS -ixsZero (_ :$$ sh) = 0 :.$ ixsZero sh +ixsZero (SNat :$$ sh) = 0 :.$ ixsZero sh ixCvtXS :: ShS sh -> IIxX (MapJust sh) -> IIxS sh ixCvtXS ZSS ZIX = ZIS -ixCvtXS (_ :$$ sh) (n :.% idx) = n :.$ ixCvtXS sh idx +ixCvtXS (SNat :$$ sh) (n :.% idx) = n :.$ ixCvtXS sh idx ixCvtSX :: IIxS sh -> IIxX (MapJust sh) ixCvtSX ZIS = ZIX @@ -271,10 +271,10 @@ pattern ZSS = ShS ZS pattern (:$$) :: forall {sh1}. - forall n sh. (KnownNat n, n : sh ~ sh1) + forall n sh. n : sh ~ sh1 => SNat n -> ShS sh -> ShS sh1 pattern i :$$ shl <- ShS (listsUncons -> Just (UnconsListSRes (ShS -> shl) i)) - where i :$$ ShS shl = ShS (i ::$ shl) + where i@SNat :$$ ShS shl = ShS (i ::$ shl) infixr 3 :$$ @@ -387,7 +387,7 @@ instance KnownShS sh => IsList (ListS sh (Const i)) where where go :: ShS sh' -> [i] -> ListS sh' (Const i) go ZSS [] = ZS - go (_ :$$ sh) (i : is) = Const i ::$ go sh is + go (SNat :$$ 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) ++ ")" @@ -406,7 +406,7 @@ instance KnownShS sh => IsList (ShS sh) where where go :: ShS sh' -> [Int] -> ListS sh' SNat go ZSS [] = ZS - go (sn :$$ sh) (i : is) + go (sn@SNat :$$ 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 ++ ")" |