diff options
| author | Tom Smeding <tom@tomsmeding.com> | 2024-12-11 21:27:23 +0100 |
|---|---|---|
| committer | Tom Smeding <tom@tomsmeding.com> | 2024-12-11 21:30:05 +0100 |
| commit | 1b8403a66572c3ed85580ec6745130ad1627042e (patch) | |
| tree | 31443a6dff3a495877a76e0ba738120b6b586a53 /src/Data/Array/Nested/Internal | |
| parent | a3299c09e0fd12cf73c4a0a9a2ae37b8f69f9b10 (diff) | |
rcastToMixed
Diffstat (limited to 'src/Data/Array/Nested/Internal')
| -rw-r--r-- | src/Data/Array/Nested/Internal/Ranked.hs | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/Data/Array/Nested/Internal/Ranked.hs b/src/Data/Array/Nested/Internal/Ranked.hs index ed89d82..5160078 100644 --- a/src/Data/Array/Nested/Internal/Ranked.hs +++ b/src/Data/Array/Nested/Internal/Ranked.hs @@ -534,3 +534,10 @@ mtoRanked arr rtoMixed :: forall n a. Ranked n a -> Mixed (Replicate n Nothing) a rtoMixed (Ranked arr) = arr + +-- | A more weakly-typed version of 'rtoMixed' that does a runtime shape +-- compatibility check. +rcastToMixed :: (Rank sh ~ n, Elt a) => StaticShX sh -> Ranked n a -> Mixed sh a +rcastToMixed sshx rarr@(Ranked arr) + | Refl <- lemRankReplicate (rrank rarr) + = mcast sshx arr |