From 6f2206b61ea05d4b1cd1fb6d0971484bbc820b02 Mon Sep 17 00:00:00 2001
From: Mikolaj Konarski <mikolaj.konarski@funktory.com>
Date: Tue, 16 Dec 2025 10:28:42 +0100
Subject: Implement ranked shape conversions as newtype coerces

---
 src/Data/Array/Nested/Convert.hs | 16 +++++++++-------
 1 file changed, 9 insertions(+), 7 deletions(-)

(limited to 'src/Data/Array/Nested/Convert.hs')

diff --git a/src/Data/Array/Nested/Convert.hs b/src/Data/Array/Nested/Convert.hs
index d4d1cea..32248c4 100644
--- a/src/Data/Array/Nested/Convert.hs
+++ b/src/Data/Array/Nested/Convert.hs
@@ -15,7 +15,7 @@
 module Data.Array.Nested.Convert (
   -- * Shape\/index\/list casting functions
   -- ** To ranked
-  ixrFromIxS, ixrFromIxX, shrFromShS, shrFromShX, shrFromShX2,
+  ixrFromIxS, ixrFromIxX, shrFromShS, shrFromShXAnyShape, shrFromShX,
   listrCast, ixrCast, shrCast,
   -- ** To shaped
   ixsFromIxR, ixsFromIxR', ixsFromIxX, ixsFromIxX', withShsFromShR, shsFromShX, withShsFromShX, shsFromSSX,
@@ -70,8 +70,13 @@ shrFromShS :: ShS sh -> IShR (Rank sh)
 shrFromShS ZSS = ZSR
 shrFromShS (n :$$ sh) = fromSNat' n :$: shrFromShS sh
 
--- shrFromShX re-exported
--- shrFromShX2 re-exported
+shrFromShXAnyShape :: IShX sh -> IShR (Rank sh)
+shrFromShXAnyShape ZSX = ZSR
+shrFromShXAnyShape (n :$% idx) = fromSMayNat' n :$: shrFromShXAnyShape idx
+
+shrFromShX :: IShX (Replicate n Nothing) -> IShR n
+shrFromShX = coerce
+
 -- listrCast re-exported
 -- ixrCast re-exported
 -- shrCast re-exported
@@ -146,10 +151,7 @@ ixxFromIxS :: IxS sh i -> IxX (MapJust sh) i
 ixxFromIxS = unsafeCoerce
 
 shxFromShR :: ShR n i -> ShX (Replicate n Nothing) i
-shxFromShR ZSR = ZSX
-shxFromShR (n :$: (idx :: ShR m i)) =
-  castWith (subst2 @ShX @i (lemReplicateSucc @(Nothing @Nat) (Proxy @m)))
-    (SUnknown n :$% shxFromShR idx)
+shxFromShR = coerce
 
 shxFromShS :: ShS sh -> IShX (MapJust sh)
 shxFromShS = coerce
-- 
cgit v1.2.3-70-g09d2