From 27f5fd474a85bd0c404215a1ce38ed378594e54b Mon Sep 17 00:00:00 2001
From: Mikolaj Konarski <mikolaj.konarski@funktory.com>
Date: Thu, 9 Apr 2026 17:48:51 +0200
Subject: Get rid of ListH

---
 src/Data/Array/Nested/Ranked/Shape.hs | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

(limited to 'src/Data/Array/Nested/Ranked/Shape.hs')

diff --git a/src/Data/Array/Nested/Ranked/Shape.hs b/src/Data/Array/Nested/Ranked/Shape.hs
index 690b7da..a352eb3 100644
--- a/src/Data/Array/Nested/Ranked/Shape.hs
+++ b/src/Data/Array/Nested/Ranked/Shape.hs
@@ -366,10 +366,10 @@ shrSize (ShR sh) = shxSize sh
 -- We don't report the size of the list in case of errors in order not to retain the list.
 {-# INLINEABLE shrFromList #-}
 shrFromList :: SNat n -> [Int] -> IShR n
-shrFromList snat topl = ShR $ ShX $ go snat topl
+shrFromList snat topl = ShR $ go snat topl
   where
-    go :: SNat n -> [Int] -> ListH (Replicate n Nothing) Int
-    go SZ [] = ZH
+    go :: SNat n -> [Int] -> ShX (Replicate n Nothing) Int
+    go SZ [] = ZSX
     go SZ _ = error $ "shrFromList: List too long (type says " ++ show (fromSNat' snat) ++ ")"
     go (SS sn :: SNat n1) (i : is) | Refl <- lemReplicateSucc2 (Proxy @n1) Refl = ConsUnknown i (go sn is)
     go _ _ = error $ "shrFromList: List too short (type says " ++ show (fromSNat' snat) ++ ")"
@@ -377,9 +377,9 @@ shrFromList snat topl = ShR $ ShX $ go snat topl
 -- This is equivalent to but faster than @coerce shxToList@.
 {-# INLINEABLE shrToList #-}
 shrToList :: IShR n -> [Int]
-shrToList (ShR (ShX l)) = build (\(cons :: i -> is -> is) (nil :: is) ->
-  let go :: ListH sh Int -> is
-      go ZH = nil
+shrToList (ShR l) = build (\(cons :: i -> is -> is) (nil :: is) ->
+  let go :: ShX sh Int -> is
+      go ZSX = nil
       go (ConsUnknown i rest) = i `cons` go rest
       go ConsKnown{} = error "shrToList: impossible case"
   in go l)
@@ -411,7 +411,7 @@ shrInit
   = -- TODO: change this and all other unsafeCoerceRefl to lemmas:
     gcastWith (unsafeCoerceRefl
                :: Init (Replicate (n + 1) (Nothing @Nat)) :~: Replicate n Nothing) $
-    coerce (shxInit @_ @_ @i)
+    coerce (shxInit @i)
 
 shrLast :: forall n i. ShR (n + 1) i -> i
 shrLast (ShR sh)
@@ -431,7 +431,7 @@ shrAppend =
   -- lemReplicatePlusApp requires an SNat
   gcastWith (unsafeCoerceRefl
              :: Replicate n (Nothing @Nat) ++ Replicate m Nothing :~: Replicate (n + m) Nothing) $
-  coerce (shxAppend @_ @_ @i)
+  coerce (shxAppend @_ @i)
 
 {-# INLINE shrZipWith #-}
 shrZipWith :: (i -> j -> k) -> ShR n i -> ShR n j -> ShR n k
@@ -447,7 +447,7 @@ shrSplitAt (SS m) (n :$: sh) = (\(pre, post) -> (n :$: pre, post)) (shrSplitAt m
 shrSplitAt SS{} ZSR = error "m' + 1 <= 0"
 
 shrIndex :: forall k sh i. SNat k -> ShR sh i -> i
-shrIndex k (ShR sh) = case shxIndex @_ @_ @i k sh of
+shrIndex k (ShR sh) = case shxIndex @i k sh of
   SUnknown i -> i
   SKnown{} -> error "shrIndex: impossible SKnown"
 
-- 
cgit v1.3