2 files changed, 16 insertions, 29 deletions
diff --git a/src/Data/Array/Nested/Ranked/Base.hs b/src/Data/Array/Nested/Ranked/Base.hs
index beb5b0e..babc809 100644
--- a/src/Data/Array/Nested/Ranked/Base.hs
+++ b/src/Data/Array/Nested/Ranked/Base.hs
@@ -5,6 +5,7 @@
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE ImportQualifiedPost #-}
 {-# LANGUAGE InstanceSigs #-}
+{-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE StandaloneDeriving #-}
@@ -25,6 +26,7 @@ import Data.Coerce (coerce)
 import Data.Kind (Type)
 import Data.List.NonEmpty (NonEmpty)
 import Data.Proxy
+import Data.Type.Equality
 import Foreign.Storable (Storable)
 import GHC.Float qualified (expm1, log1mexp, log1p, log1pexp)
 import GHC.Generics (Generic)
@@ -35,12 +37,12 @@ import Data.Foldable (toList)
 #endif
 
 import Data.Array.Nested.Lemmas
-import Data.Array.Nested.Types
-import Data.Array.XArray (XArray(..))
 import Data.Array.Nested.Mixed
 import Data.Array.Nested.Mixed.Shape
 import Data.Array.Nested.Ranked.Shape
+import Data.Array.Nested.Types
 import Data.Array.Strided.Arith
+import Data.Array.XArray (XArray(..))
 
 
 -- | A rank-typed array: the number of dimensions of the array (its /rank/) is
@@ -252,3 +254,15 @@ rshape (Ranked arr) = shrFromShX2 (mshape arr)
 
 rrank :: Elt a => Ranked n a -> SNat n
 rrank = shrRank . rshape
+
+-- Needed already here, but re-exported in Data.Array.Nested.Convert.
+shrFromShX :: forall sh. IShX sh -> IShR (Rank sh)
+shrFromShX ZSX = ZSR
+shrFromShX (n :$% idx) = fromSMayNat' n :$: shrFromShX idx
+
+-- Needed already here, but re-exported in Data.Array.Nested.Convert.
+-- | Convenience wrapper around 'shrFromShX' that applies 'lemRankReplicate'.
+shrFromShX2 :: forall n. IShX (Replicate n Nothing) -> IShR n
+shrFromShX2 sh
+  | Refl <- lemRankReplicate (Proxy @n)
+  = shrFromShX sh
diff --git a/src/Data/Array/Nested/Ranked/Shape.hs b/src/Data/Array/Nested/Ranked/Shape.hs
index 75a1e5b..326bf61 100644
--- a/src/Data/Array/Nested/Ranked/Shape.hs
+++ b/src/Data/Array/Nested/Ranked/Shape.hs
@@ -40,7 +40,6 @@ import GHC.TypeLits
 import GHC.TypeNats qualified as TN
 
 import Data.Array.Nested.Lemmas
-import Data.Array.Nested.Mixed.Shape
 import Data.Array.Nested.Types
 
 
@@ -213,16 +212,6 @@ ixrZero :: SNat n -> IIxR n
 ixrZero SZ = ZIR
 ixrZero (SS n) = 0 :.: ixrZero n
 
-ixrFromIxX :: IxX sh i -> IxR (Rank sh) i
-ixrFromIxX ZIX = ZIR
-ixrFromIxX (n :.% idx) = n :.: ixrFromIxX idx
-
-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) @m))
-    (n :.% ixxFromIxR idx)
-
 ixrHead :: IxR (n + 1) i -> i
 ixrHead (IxR list) = listrHead list
 
@@ -278,22 +267,6 @@ instance Show i => Show (ShR n i) where
 
 instance NFData i => NFData (ShR sh i)
 
-shrFromShX :: forall sh. IShX sh -> IShR (Rank sh)
-shrFromShX ZSX = ZSR
-shrFromShX (n :$% idx) = fromSMayNat' n :$: shrFromShX idx
-
--- | Convenience wrapper around 'shrFromShX' that applies 'lemRankReplicate'.
-shrFromShX2 :: forall n. IShX (Replicate n Nothing) -> IShR n
-shrFromShX2 sh
-  | Refl <- lemRankReplicate (Proxy @n)
-  = shrFromShX sh
-
-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) @m))
-    (SUnknown n :$% shxFromShR idx)
-
 -- | This checks only whether the ranks are equal, not whether the actual
 -- values are.
 shrEqRank :: ShR n i -> ShR n' i -> Maybe (n :~: n')