3 files changed, 14 insertions, 4 deletions
diff --git a/src/Data/Array/Nested/Ranked/Shape.hs b/src/Data/Array/Nested/Ranked/Shape.hs
index 580bc59..c0c4f17 100644
--- a/src/Data/Array/Nested/Ranked/Shape.hs
+++ b/src/Data/Array/Nested/Ranked/Shape.hs
@@ -28,7 +28,6 @@
 module Data.Array.Nested.Ranked.Shape where
 
 import Control.DeepSeq (NFData(..))
-import Data.Array.Nested.Types
 import Data.Coerce (coerce)
 import Data.Foldable qualified as Foldable
 import Data.Kind (Type)
@@ -42,6 +41,7 @@ import GHC.TypeNats qualified as TN
 
 import Data.Array.Mixed.Lemmas
 import Data.Array.Nested.Mixed.Shape
+import Data.Array.Nested.Types
 
 
 type role ListR nominal representational
diff --git a/src/Data/Array/Nested/Shaped/Shape.hs b/src/Data/Array/Nested/Shaped/Shape.hs
index 3b33b05..0b7d1c9 100644
--- a/src/Data/Array/Nested/Shaped/Shape.hs
+++ b/src/Data/Array/Nested/Shaped/Shape.hs
@@ -28,7 +28,6 @@
 module Data.Array.Nested.Shaped.Shape where
 
 import Control.DeepSeq (NFData(..))
-import Data.Array.Nested.Types
 import Data.Array.Shape qualified as O
 import Data.Coerce (coerce)
 import Data.Foldable qualified as Foldable
@@ -44,9 +43,9 @@ import GHC.IsList (IsList)
 import GHC.IsList qualified as IsList
 import GHC.TypeLits
 
-import Data.Array.Mixed.Lemmas
-import Data.Array.Nested.Permutation
 import Data.Array.Nested.Mixed.Shape
+import Data.Array.Nested.Permutation
+import Data.Array.Nested.Types
 
 
 type role ListS nominal representational
diff --git a/src/Data/Array/Nested/Types.hs b/src/Data/Array/Nested/Types.hs
index 90a499b..4172fa0 100644
--- a/src/Data/Array/Nested/Types.hs
+++ b/src/Data/Array/Nested/Types.hs
@@ -13,6 +13,9 @@
 {-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
 {-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
 module Data.Array.Nested.Types (
+  -- * Reasoning helpers
+  subst1, subst2,
+
   -- * Reified evidence of a type class
   Dict(..),
 
@@ -43,6 +46,14 @@ import GHC.TypeNats qualified as TN
 import Unsafe.Coerce qualified
 
 
+-- Reasoning helpers
+
+subst1 :: forall f a b. a :~: b -> f a :~: f b
+subst1 Refl = Refl
+
+subst2 :: forall f c a b. a :~: b -> f a c :~: f b c
+subst2 Refl = Refl
+
 -- | Evidence for the constraint @c a@.
 data Dict c a where
   Dict :: c a => Dict c a