From c1dd11717ecff65bae94cf0d4fb2dfcff5eeae3f Mon Sep 17 00:00:00 2001 From: Tom Smeding Date: Wed, 17 Apr 2024 10:23:27 +0200 Subject: Remove redundant constraint from rgenerate --- src/Data/Array/Nested/Internal.hs | 9 +++++++-- 1 file 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)) -- cgit v1.2.3-70-g09d2