From fe034ff95a1f299ed140f37e416b5562cd423457 Mon Sep 17 00:00:00 2001
From: Mikolaj Konarski <mikolaj.konarski@funktory.com>
Date: Wed, 17 Dec 2025 19:06:38 +0100
Subject: Make List?, except ListH, less general

---
 src/Data/Array/Nested/Permutation.hs | 17 +++++++----------
 1 file changed, 7 insertions(+), 10 deletions(-)

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

diff --git a/src/Data/Array/Nested/Permutation.hs b/src/Data/Array/Nested/Permutation.hs
index c3d2075..ecdb06d 100644
--- a/src/Data/Array/Nested/Permutation.hs
+++ b/src/Data/Array/Nested/Permutation.hs
@@ -18,7 +18,6 @@
 module Data.Array.Nested.Permutation where
 
 import Data.Coerce (coerce)
-import Data.Functor.Const
 import Data.List (sort)
 import Data.Maybe (fromMaybe)
 import Data.Proxy
@@ -236,33 +235,31 @@ shxPermutePrefix :: Perm is -> IShX sh -> IShX (PermutePrefix is sh)
 shxPermutePrefix = coerce (listhPermutePrefix @Int)
 
 
-listxTakeLen :: forall f is sh. Perm is -> ListX sh f -> ListX (TakeLen is sh) f
+listxTakeLen :: forall i is sh. Perm is -> ListX sh i -> ListX (TakeLen is sh) i
 listxTakeLen PNil _ = ZX
 listxTakeLen (_ `PCons` is) (n ::% sh) = n ::% listxTakeLen is sh
 listxTakeLen (_ `PCons` _) ZX = error "Permutation longer than shape"
 
-listxDropLen :: forall f is sh. Perm is -> ListX sh f -> ListX (DropLen is sh) f
+listxDropLen :: forall i is sh. Perm is -> ListX sh i -> ListX (DropLen is sh) i
 listxDropLen PNil sh = sh
 listxDropLen (_ `PCons` is) (_ ::% sh) = listxDropLen is sh
 listxDropLen (_ `PCons` _) ZX = error "Permutation longer than shape"
 
-listxPermute :: forall f is sh. Perm is -> ListX sh f -> ListX (Permute is sh) f
+listxPermute :: forall i is sh. Perm is -> ListX sh i -> ListX (Permute is sh) i
 listxPermute PNil _ = ZX
 listxPermute (i `PCons` (is :: Perm is')) (sh :: ListX sh f) =
   listxIndex i sh ::% listxPermute is sh
 
-listxIndex :: forall f i sh. SNat i -> ListX sh f -> f (Index i sh)
+listxIndex :: forall j i sh. SNat i -> ListX sh j -> j
 listxIndex SZ (n ::% _) = n
-listxIndex (SS (i :: SNat i')) ((_ :: f n) ::% (sh :: ListX sh' f))
-  | Refl <- lemIndexSucc (Proxy @i') (Proxy @n) (Proxy @sh')
-  = listxIndex i sh
+listxIndex (SS i) (_ ::% sh) = listxIndex i sh
 listxIndex _ ZX = error "Index into empty shape"
 
-listxPermutePrefix :: forall f is sh. Perm is -> ListX sh f -> ListX (PermutePrefix is sh) f
+listxPermutePrefix :: forall i is sh. Perm is -> ListX sh i -> ListX (PermutePrefix is sh) i
 listxPermutePrefix perm sh = listxAppend (listxPermute perm (listxTakeLen perm sh)) (listxDropLen perm sh)
 
 ixxPermutePrefix :: forall i is sh. Perm is -> IxX sh i -> IxX (PermutePrefix is sh) i
-ixxPermutePrefix = coerce (listxPermutePrefix @(Const i))
+ixxPermutePrefix = coerce (listxPermutePrefix @i)
 
 -- * Operations on permutations
 
-- 
cgit v1.2.3-70-g09d2