From 1b8403a66572c3ed85580ec6745130ad1627042e Mon Sep 17 00:00:00 2001
From: Tom Smeding <tom@tomsmeding.com>
Date: Wed, 11 Dec 2024 21:27:23 +0100
Subject: rcastToMixed

---
 src/Data/Array/Nested.hs                 | 2 +-
 src/Data/Array/Nested/Internal/Ranked.hs | 7 +++++++
 2 files changed, 8 insertions(+), 1 deletion(-)

(limited to 'src/Data/Array')

diff --git a/src/Data/Array/Nested.hs b/src/Data/Array/Nested.hs
index cf60fa1..6bef5f7 100644
--- a/src/Data/Array/Nested.hs
+++ b/src/Data/Array/Nested.hs
@@ -19,7 +19,7 @@ module Data.Array.Nested (
   rlift, rlift2,
   -- ** Conversions
   rtoXArrayPrim, rfromXArrayPrim,
-  rcastToShaped, rtoMixed,
+  rcastToShaped, rtoMixed, rcastToMixed,
   rfromOrthotope, rtoOrthotope,
 
   -- * Shaped arrays
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