diff options
Diffstat (limited to 'src/Data/Array/Nested/Internal')
| -rw-r--r-- | src/Data/Array/Nested/Internal/Shaped.hs | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/Data/Array/Nested/Internal/Shaped.hs b/src/Data/Array/Nested/Internal/Shaped.hs index 5d3eba1..76e0e6d 100644 --- a/src/Data/Array/Nested/Internal/Shaped.hs +++ b/src/Data/Array/Nested/Internal/Shaped.hs @@ -483,3 +483,13 @@ mcastToShaped arr targetsh stoMixed :: forall sh a. Shaped sh a -> Mixed (MapJust sh) a stoMixed (Shaped arr) = arr + +-- | A more weakly-typed version of 'stoMixed' that does a runtime shape +-- compatibility check. +scastToMixed :: forall sh sh' a. (Elt a, Rank sh ~ Rank sh') + => IShX sh' -> Shaped sh a -> Mixed sh' a +scastToMixed shx (Shaped arr) + | Refl <- lemAppNil @sh' + , Refl <- lemAppNil @(MapJust sh) + , Refl <- lemRankMapJust (shCvtXS' @sh (mshape arr)) + = mcast (ssxFromShape (mshape arr)) shx (Proxy @'[]) arr |