1 files changed, 19 insertions, 20 deletions

diff --git a/src/Data/Array/Nested/Convert.hs b/src/Data/Array/Nested/Convert.hs
index 8c88d23..d4d1cea 100644
--- a/src/Data/Array/Nested/Convert.hs
+++ b/src/Data/Array/Nested/Convert.hs
@@ -38,9 +38,11 @@ module Data.Array.Nested.Convert (
 ) where
 
 import Control.Category
+import Data.Coerce (coerce)
 import Data.Proxy
 import Data.Type.Equality
 import GHC.TypeLits
+import Unsafe.Coerce (unsafeCoerce)
 
 import Data.Array.Nested.Lemmas
 import Data.Array.Nested.Mixed
@@ -55,13 +57,14 @@ import Data.Array.Nested.Types
 
 -- * To ranked
 
+-- TODO: change all those unsafeCoerces into coerces by defining shaped
+-- and ranekd index types as newtypes of the mixed index type
+-- and similarly for the sized lists
 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
@@ -75,12 +78,11 @@ shrFromShS (n :$$ sh) = fromSNat' n :$: shrFromShS sh
 
 -- * To shaped
 
--- TODO: these take a ShS because there are KnownNats inside IxS.
-
+-- 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
 -- following, but more efficient:
 --
@@ -90,11 +92,11 @@ ixsFromIxR' ZSS ZIR = ZIS
 ixsFromIxR' (_ :$$ sh) (n :.: idx) = n :.$ ixsFromIxR' sh idx
 ixsFromIxR' _ _ = error "ixsFromIxR': index rank does not match shape rank"
 
--- TODO: this takes a ShS because there are KnownNats inside IxS.
+-- 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
 -- the following, but more efficient:
 --
@@ -113,7 +115,8 @@ withShsFromShR (n :$: sh) k =
       Just sn@SNat -> k (sn :$$ sh')
       Nothing -> error $ "withShsFromShR: negative dimension size (" ++ show n ++ ")"
 
--- shsFromShX re-exported
+shsFromShX :: IShX (MapJust sh) -> ShS sh
+shsFromShX = coerce
 
 -- | Produce an existential 'ShS' from an 'IShX'. If you already know that
 -- @sh'@ is @MapJust@ of something, use 'shsFromShX' instead.
@@ -128,6 +131,7 @@ withShsFromShX (SUnknown n :$% sh) k =
       Just sn@SNat -> k (sn :$$ sh')
       Nothing -> error $ "withShsFromShX: negative SUnknown dimension size (" ++ show n ++ ")"
 
+-- If it ever matters for performance, this is unsafeCoercible.
 shsFromSSX :: StaticShX (MapJust sh) -> ShS sh
 shsFromSSX = shsFromShX Prelude.. shxFromSSX
 
@@ -136,14 +140,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
@@ -152,8 +152,7 @@ shxFromShR (n :$: (idx :: ShR m i)) =
     (SUnknown n :$% shxFromShR idx)
 
 shxFromShS :: ShS sh -> IShX (MapJust sh)
-shxFromShS ZSS = ZSX
-shxFromShS (n :$$ sh) = SKnown n :$% shxFromShS sh
+shxFromShS = coerce
 
 -- ixxCast re-exported
 -- shxCast re-exported