From 824078db9bc0b26bdde282f28ce7805c634101e2 Mon Sep 17 00:00:00 2001
From: Mikolaj Konarski <mikolaj.konarski@funktory.com>
Date: Mon, 15 Dec 2025 22:17:34 +0100
Subject: Simplify the signature of fooIndex

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

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

diff --git a/src/Data/Array/Nested/Shaped/Shape.hs b/src/Data/Array/Nested/Shaped/Shape.hs
index d815adf..030a065 100644
--- a/src/Data/Array/Nested/Shaped/Shape.hs
+++ b/src/Data/Array/Nested/Shaped/Shape.hs
@@ -196,16 +196,16 @@ listsDropLenPerm (_ `PCons` _) ZS = error "Permutation longer than shape"
 listsPermute :: forall f is sh. Perm is -> ListS sh f -> ListS (Permute is sh) f
 listsPermute PNil _ = ZS
 listsPermute (i `PCons` (is :: Perm is')) (sh :: ListS sh f) =
-  case listsIndex (Proxy @is') (Proxy @sh) i sh of
+  case listsIndex i sh of
     item -> item ::$ listsPermute is sh
 
 -- TODO: try to remove this SNat now that the KnownNat constraint in ListS is removed
-listsIndex :: forall f i is sh shT. Proxy is -> Proxy shT -> SNat i -> ListS sh f -> f (Index i sh)
-listsIndex _ _ SZ (n ::$ _) = n
-listsIndex p pT (SS (i :: SNat i')) ((_ :: f n) ::$ (sh :: ListS sh' f))
+listsIndex :: forall f i sh. SNat i -> ListS sh f -> f (Index i sh)
+listsIndex SZ (n ::$ _) = n
+listsIndex (SS (i :: SNat i')) ((_ :: f n) ::$ (sh :: ListS sh' f))
   | Refl <- lemIndexSucc (Proxy @i') (Proxy @n) (Proxy @sh')
-  = listsIndex p pT i sh
-listsIndex _ _ _ ZS = error "Index into empty shape"
+  = listsIndex i sh
+listsIndex _ ZS = error "Index into empty shape"
 
 listsPermutePrefix :: forall f is sh. Perm is -> ListS sh f -> ListS (PermutePrefix is sh) f
 listsPermutePrefix perm sh = listsAppend (listsPermute perm (listsTakeLenPerm perm sh)) (listsDropLenPerm perm sh)
@@ -460,12 +460,11 @@ shsPermute =
              :: Permute is (MapJust sh) :~: MapJust (Permute is sh)) $
   coerce shxPermute
 
-shsIndex :: forall is shT i sh.
-            Proxy is -> Proxy shT -> SNat i -> ShS sh -> SNat (Index i sh)
-shsIndex pis pshT i sh =
+shsIndex :: forall i sh. SNat i -> ShS sh -> SNat (Index i sh)
+shsIndex i sh =
   gcastWith (unsafeCoerceRefl
              :: Index i (MapJust sh) :~: Just (Index i sh)) $
-  case shxIndex pis pshT i (coerce sh) of
+  case shxIndex i (coerce sh) of
     SKnown SNat -> SNat
 
 shsPermutePrefix :: forall is sh. Perm is -> ShS sh -> ShS (PermutePrefix is sh)
-- 
cgit v1.2.3-70-g09d2