diff options
| author | Tom Smeding <tom@tomsmeding.com> | 2024-04-17 10:23:27 +0200 | 
|---|---|---|
| committer | Tom Smeding <tom@tomsmeding.com> | 2024-04-17 10:23:27 +0200 | 
| commit | c1dd11717ecff65bae94cf0d4fb2dfcff5eeae3f (patch) | |
| tree | 2043ce5f94080b32b517a9cac1431b1a1986141f /src/Data/Array | |
| parent | d5c6f0ec8d9bffed3d1d60af9ca323178e6a9d8e (diff) | |
Remove redundant constraint from rgenerate
Diffstat (limited to 'src/Data/Array')
| -rw-r--r-- | src/Data/Array/Nested/Internal.hs | 9 | 
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)) | 
