aboutsummaryrefslogtreecommitdiff
path: root/src/Data
diff options
context:
space:
mode:
authorTom Smeding <tom@tomsmeding.com>2024-04-17 10:23:27 +0200
committerTom Smeding <tom@tomsmeding.com>2024-04-17 10:23:27 +0200
commitc1dd11717ecff65bae94cf0d4fb2dfcff5eeae3f (patch)
tree2043ce5f94080b32b517a9cac1431b1a1986141f /src/Data
parentd5c6f0ec8d9bffed3d1d60af9ca323178e6a9d8e (diff)
Remove redundant constraint from rgenerate
Diffstat (limited to 'src/Data')
-rw-r--r--src/Data/Array/Nested/Internal.hs9
1 files changed, 7 insertions, 2 deletions
diff --git a/src/Data/Array/Nested/Internal.hs b/src/Data/Array/Nested/Internal.hs
index d6808a0..8edf5be 100644
--- a/src/Data/Array/Nested/Internal.hs
+++ b/src/Data/Array/Nested/Internal.hs
@@ -780,6 +780,10 @@ ixCvtRX :: IxR n -> IxX (Replicate n Nothing)
ixCvtRX IZR = IZX
ixCvtRX (n ::: idx) = n ::? ixCvtRX idx
+knownIxR :: IxR n -> Dict KnownINat n
+knownIxR IZR = Dict
+knownIxR (_ ::: idx) | Dict <- knownIxR idx = Dict
+
shapeSizeR :: IxR n -> Int
shapeSizeR IZR = 1
shapeSizeR (n ::: sh) = n * shapeSizeR sh
@@ -802,9 +806,10 @@ rindexPartial (Ranked arr) idx =
-- | **WARNING**: All values returned from the function must have equal shape.
-- See the documentation of 'mgenerate' for more details.
-rgenerate :: forall n a. (KnownINat n, Elt a) => IxR n -> (IxR n -> a) -> Ranked n a
+rgenerate :: forall n a. Elt a => IxR n -> (IxR n -> a) -> Ranked n a
rgenerate sh f
- | Dict <- lemKnownReplicate (Proxy @n)
+ | Dict <- knownIxR sh
+ , Dict <- lemKnownReplicate (Proxy @n)
, Refl <- lemRankReplicate (Proxy @n)
= Ranked (mgenerate (ixCvtRX sh) (f . ixCvtXR))