From 0d06aadc72635011ef4c2ac4d7f45ece42817470 Mon Sep 17 00:00:00 2001
From: Tom Smeding <tom@tomsmeding.com>
Date: Fri, 29 Nov 2024 15:59:32 +0100
Subject: scastToMixed, weakly-typed version of stoMixed

---
 src/Data/Array/Nested.hs                 |  2 +-
 src/Data/Array/Nested/Internal/Shaped.hs | 10 ++++++++++
 2 files changed, 11 insertions(+), 1 deletion(-)

(limited to 'src/Data')

diff --git a/src/Data/Array/Nested.hs b/src/Data/Array/Nested.hs
index 499fdda..767f606 100644
--- a/src/Data/Array/Nested.hs
+++ b/src/Data/Array/Nested.hs
@@ -41,7 +41,7 @@ module Data.Array.Nested (
   slift, slift2,
   -- ** Conversions
   stoXArrayPrim, sfromXArrayPrim,
-  stoRanked, stoMixed,
+  stoRanked, stoMixed, scastToMixed,
   sfromOrthotope, stoOrthotope,
 
   -- * Mixed arrays
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
-- 
cgit v1.2.3-70-g09d2