From f2129e063bc5ee6241b2cf0891f8f39c8265ccb7 Mon Sep 17 00:00:00 2001
From: Mikolaj Konarski <mikolaj.konarski@funktory.com>
Date: Sat, 13 Dec 2025 14:18:46 +0100
Subject: Implement index conversions as unsafeCoerce

until maybe we make shaped and ranked newtypes over mixed?
---
 src/Data/Array/Nested/Convert.hs | 21 +++++++--------------
 1 file changed, 7 insertions(+), 14 deletions(-)

(limited to 'src/Data/Array/Nested')

diff --git a/src/Data/Array/Nested/Convert.hs b/src/Data/Array/Nested/Convert.hs
index 3d0da37..da1c384 100644
--- a/src/Data/Array/Nested/Convert.hs
+++ b/src/Data/Array/Nested/Convert.hs
@@ -41,6 +41,7 @@ import Control.Category
 import Data.Proxy
 import Data.Type.Equality
 import GHC.TypeLits
+import Unsafe.Coerce (unsafeCoerce)
 
 import Data.Array.Nested.Lemmas
 import Data.Array.Nested.Mixed
@@ -56,12 +57,10 @@ import Data.Array.Nested.Types
 -- * To ranked
 
 ixrFromIxS :: IxS sh i -> IxR (Rank sh) i
-ixrFromIxS ZIS = ZIR
-ixrFromIxS (i :.$ ix) = i :.: ixrFromIxS ix
+ixrFromIxS = unsafeCoerce
 
 ixrFromIxX :: IxX sh i -> IxR (Rank sh) i
-ixrFromIxX ZIX = ZIR
-ixrFromIxX (n :.% idx) = n :.: ixrFromIxX idx
+ixrFromIxX = unsafeCoerce
 
 shrFromShS :: ShS sh -> IShR (Rank sh)
 shrFromShS ZSS = ZSR
@@ -77,8 +76,7 @@ shrFromShS (n :$$ sh) = fromSNat' n :$: shrFromShS sh
 
 -- TODO: remove the ShS now that no KnownNats is inside IxS.
 ixsFromIxR :: ShS sh -> IxR (Rank sh) i -> IxS sh i
-ixsFromIxR ZSS ZIR = ZIS
-ixsFromIxR (_ :$$ sh) (n :.: idx) = n :.$ ixsFromIxR sh idx
+ixsFromIxR _ = unsafeCoerce
 
 -- TODO: if possible, remove the ShS now that no KnownNats is inside IxS.
 -- | Performs a runtime check that @n@ matches @Rank sh@. Equivalent to the
@@ -92,8 +90,7 @@ ixsFromIxR' _ _ = error "ixsFromIxR': index rank does not match shape rank"
 
 -- TODO: remove the ShS now that no KnownNats is inside IxS.
 ixsFromIxX :: ShS sh -> IxX (MapJust sh) i -> IxS sh i
-ixsFromIxX ZSS ZIX = ZIS
-ixsFromIxX (_ :$$ sh) (n :.% idx) = n :.$ ixsFromIxX sh idx
+ixsFromIxX _ = unsafeCoerce
 
 -- TODO: if possible, remove the ShS now that no KnownNats is inside IxS.
 -- | Performs a runtime check that @Rank sh'@ match @Rank sh@. Equivalent to
@@ -137,14 +134,10 @@ shsFromSSX = shsFromShX Prelude.. shxFromSSX
 -- * To mixed
 
 ixxFromIxR :: IxR n i -> IxX (Replicate n Nothing) i
-ixxFromIxR ZIR = ZIX
-ixxFromIxR (n :.: (idx :: IxR m i)) =
-  castWith (subst2 @IxX @i (lemReplicateSucc @(Nothing @Nat) (Proxy @m)))
-    (n :.% ixxFromIxR idx)
+ixxFromIxR = unsafeCoerce
 
 ixxFromIxS :: IxS sh i -> IxX (MapJust sh) i
-ixxFromIxS ZIS = ZIX
-ixxFromIxS (n :.$ sh) = n :.% ixxFromIxS sh
+ixxFromIxS = unsafeCoerce
 
 shxFromShR :: ShR n i -> ShX (Replicate n Nothing) i
 shxFromShR ZSR = ZSX
-- 
cgit v1.2.3-70-g09d2