From 0d6f77762d1697ea41b190e550f94e459079e3d1 Mon Sep 17 00:00:00 2001
From: Mikolaj Konarski <mikolaj.konarski@funktory.com>
Date: Sat, 17 May 2025 00:04:53 +0200
Subject: Eliminate the dependency cycle of Lemmas modules

---
 src/Data/Array/Mixed/Lemmas.hs        |  9 ---------
 src/Data/Array/Nested/Ranked/Shape.hs |  2 +-
 src/Data/Array/Nested/Shaped/Shape.hs |  5 ++---
 src/Data/Array/Nested/Types.hs        | 11 +++++++++++
 4 files changed, 14 insertions(+), 13 deletions(-)

(limited to 'src')

diff --git a/src/Data/Array/Mixed/Lemmas.hs b/src/Data/Array/Mixed/Lemmas.hs
index ded6af5..e6d970c 100644
--- a/src/Data/Array/Mixed/Lemmas.hs
+++ b/src/Data/Array/Mixed/Lemmas.hs
@@ -17,15 +17,6 @@ import Data.Array.Nested.Permutation
 import Data.Array.Nested.Types
 
 
--- * 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
-
-
 -- * Lemmas
 
 -- ** Nat
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
-- 
cgit v1.2.3-70-g09d2