2 files changed, 21 insertions, 29 deletions
diff --git a/src/Data/Array/Nested/Ranked/Base.hs b/src/Data/Array/Nested/Ranked/Base.hs
index ce7025d..b7aa00f 100644
--- a/src/Data/Array/Nested/Ranked/Base.hs
+++ b/src/Data/Array/Nested/Ranked/Base.hs
@@ -137,7 +137,7 @@ instance Elt a => Elt (Ranked n a) where
 
   type ShapeTree (Ranked n a) = (IShR n, ShapeTree a)
 
-  mshapeTree (Ranked arr) = first shCvtXR' (mshapeTree arr)
+  mshapeTree (Ranked arr) = first shrFromShX2 (mshapeTree arr)
 
   mshapeTreeEq _ (sh1, t1) (sh2, t2) = sh1 == sh2 && mshapeTreeEq (Proxy @a) t1 t2
 
@@ -248,7 +248,7 @@ ratan2Array = liftRanked2 matan2Array
 
 
 rshape :: Elt a => Ranked n a -> IShR n
-rshape (Ranked arr) = shCvtXR' (mshape arr)
+rshape (Ranked arr) = shrFromShX2 (mshape arr)
 
 rrank :: Elt a => Ranked n a -> SNat n
 rrank = shrRank . rshape
diff --git a/src/Data/Array/Nested/Ranked/Shape.hs b/src/Data/Array/Nested/Ranked/Shape.hs
index c18f9ee..8f54673 100644
--- a/src/Data/Array/Nested/Ranked/Shape.hs
+++ b/src/Data/Array/Nested/Ranked/Shape.hs
@@ -213,15 +213,15 @@ ixrZero :: SNat n -> IIxR n
 ixrZero SZ = ZIR
 ixrZero (SS n) = 0 :.: ixrZero n
 
-ixCvtXR :: IIxX sh -> IIxR (Rank sh)
-ixCvtXR ZIX = ZIR
-ixCvtXR (n :.% idx) = n :.: ixCvtXR idx
+ixrFromIxX :: IIxX sh -> IIxR (Rank sh)
+ixrFromIxX ZIX = ZIR
+ixrFromIxX (n :.% idx) = n :.: ixrFromIxX idx
 
-ixCvtRX :: IIxR n -> IIxX (Replicate n Nothing)
-ixCvtRX ZIR = ZIX
-ixCvtRX (n :.: (idx :: IxR m Int)) =
+ixxFromIxR :: IIxR n -> IIxX (Replicate n Nothing)
+ixxFromIxR ZIR = ZIX
+ixxFromIxR (n :.: (idx :: IxR m Int)) =
   castWith (subst2 @IxX @Int (lemReplicateSucc @(Nothing @Nat) @m))
-    (n :.% ixCvtRX idx)
+    (n :.% ixxFromIxR idx)
 
 ixrHead :: IxR (n + 1) i -> i
 ixrHead (IxR list) = listrHead list
@@ -278,29 +278,21 @@ instance Show i => Show (ShR n i) where
 
 instance NFData i => NFData (ShR sh i)
 
-shCvtXR' :: forall n. IShX (Replicate n Nothing) -> IShR n
-shCvtXR' ZSX =
-  castWith (subst2 (unsafeCoerceRefl :: 0 :~: n))
-    ZSR
-shCvtXR' (n :$% (idx :: IShX sh))
-  | Refl <- lemReplicateSucc @(Nothing @Nat) @(n - 1) =
-  castWith (subst2 (lem1 @sh Refl))
-    (fromSMayNat' n :$: shCvtXR' (castWith (subst2 (lem2 Refl)) idx))
-  where
-    lem1 :: forall sh' n' k.
-            k : sh' :~: Replicate n' Nothing
-         -> Rank sh' + 1 :~: n'
-    lem1 Refl = unsafeCoerceRefl
+shrFromShX :: forall sh. IShX sh -> IShR (Rank sh)
+shrFromShX ZSX = ZSR
+shrFromShX (n :$% idx) = fromSMayNat' n :$: shrFromShX idx
 
-    lem2 :: k : sh :~: Replicate n Nothing
-         -> sh :~: Replicate (Rank sh) Nothing
-    lem2 Refl = unsafeCoerceRefl
+-- | Convenience wrapper around 'shrFromShX' that applies 'lemRankReplicate'.
+shrFromShX2 :: forall n. IShX (Replicate n Nothing) -> IShR n
+shrFromShX2 sh
+  | Refl <- lemRankReplicate (Proxy @n)
+  = shrFromShX sh
 
-shCvtRX :: IShR n -> IShX (Replicate n Nothing)
-shCvtRX ZSR = ZSX
-shCvtRX (n :$: (idx :: ShR m Int)) =
+shxFromShR :: IShR n -> IShX (Replicate n Nothing)
+shxFromShR ZSR = ZSX
+shxFromShR (n :$: (idx :: ShR m Int)) =
   castWith (subst2 @ShX @Int (lemReplicateSucc @(Nothing @Nat) @m))
-    (SUnknown n :$% shCvtRX idx)
+    (SUnknown n :$% shxFromShR idx)
 
 -- | This checks only whether the ranks are equal, not whether the actual
 -- values are.