From 1b8403a66572c3ed85580ec6745130ad1627042e Mon Sep 17 00:00:00 2001 From: Tom Smeding Date: Wed, 11 Dec 2024 21:27:23 +0100 Subject: rcastToMixed --- src/Data/Array/Nested/Internal/Ranked.hs | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'src/Data/Array/Nested') 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 -- cgit v1.2.3-70-g09d2