From a872f0e171825654c9559fd963f447b326d88400 Mon Sep 17 00:00:00 2001
From: Tom Smeding <tom@tomsmeding.com>
Date: Wed, 24 Jul 2024 12:10:05 +0200
Subject: Make ShS an instance of TestEquality

---
 src/Data/Array/Nested/Internal/Shape.hs | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'src/Data/Array/Nested/Internal')

diff --git a/src/Data/Array/Nested/Internal/Shape.hs b/src/Data/Array/Nested/Internal/Shape.hs
index 0d75b04..99cca06 100644
--- a/src/Data/Array/Nested/Internal/Shape.hs
+++ b/src/Data/Array/Nested/Internal/Shape.hs
@@ -314,6 +314,14 @@ listsUncons :: ListS sh1 f -> Maybe (UnconsListSRes f sh1)
 listsUncons (x ::$ sh') = Just (UnconsListSRes sh' x)
 listsUncons ZS = Nothing
 
+listsEq :: TestEquality f => ListS sh f -> ListS sh' f -> Maybe (sh :~: sh')
+listsEq ZS ZS = Just Refl
+listsEq (n ::$ sh) (m ::$ sh')
+  | Just Refl <- testEquality n m
+  , Just Refl <- listsEq sh sh'
+  = Just Refl
+listsEq _ _ = Nothing
+
 listsFmap :: (forall n. f n -> g n) -> ListS sh f -> ListS sh g
 listsFmap _ ZS = ZS
 listsFmap f (x ::$ xs) = f x ::$ listsFmap f xs
@@ -473,6 +481,9 @@ infixr 3 :$$
 instance Show (ShS sh) where
   showsPrec _ (ShS l) = listsShow (shows . fromSNat) l
 
+instance TestEquality ShS where
+  testEquality (ShS l1) (ShS l2) = listsEq l1 l2
+
 shsLength :: ShS sh -> Int
 shsLength (ShS l) = getSum (listsFold (\_ -> Sum 1) l)
 
-- 
cgit v1.2.3-70-g09d2