From 0d017c7e42c9618a0b1877974ea200b7741cada3 Mon Sep 17 00:00:00 2001
From: Mikolaj Konarski <mikolaj.konarski@funktory.com>
Date: Mon, 15 Dec 2025 02:05:11 +0100
Subject: Inline SMayNat in ListH

---
 src/Data/Array/Nested/Permutation.hs | 36 ++++++++++++++++++------------------
 1 file changed, 18 insertions(+), 18 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 7f4c02e..93c46ed 100644
--- a/src/Data/Array/Nested/Permutation.hs
+++ b/src/Data/Array/Nested/Permutation.hs
@@ -172,60 +172,60 @@ type family DropLen ref l where
   DropLen '[] l = l
   DropLen (_ : ref) (_ : xs) = DropLen ref xs
 
-listhTakeLen :: forall f is sh. Perm is -> ListH sh f -> ListH (TakeLen is sh) f
+listhTakeLen :: forall i is sh. Perm is -> ListH sh i -> ListH (TakeLen is sh) i
 listhTakeLen PNil _ = ZH
 listhTakeLen (_ `PCons` is) (n ::# sh) = n ::# listhTakeLen is sh
 listhTakeLen (_ `PCons` _) ZH = error "Permutation longer than shape"
 
-listhDropLen :: forall f is sh. Perm is -> ListH sh f -> ListH (DropLen is sh) f
+listhDropLen :: forall i is sh. Perm is -> ListH sh i -> ListH (DropLen is sh) i
 listhDropLen PNil sh = sh
 listhDropLen (_ `PCons` is) (_ ::# sh) = listhDropLen is sh
 listhDropLen (_ `PCons` _) ZH = error "Permutation longer than shape"
 
-listhPermute :: forall f is sh. Perm is -> ListH sh f -> ListH (Permute is sh) f
+listhPermute :: forall i is sh. Perm is -> ListH sh i -> ListH (Permute is sh) i
 listhPermute PNil _ = ZH
-listhPermute (i `PCons` (is :: Perm is')) (sh :: ListH sh f) =
+listhPermute (i `PCons` (is :: Perm is')) (sh :: ListH sh i) =
   listhIndex i sh ::# listhPermute is sh
 
-listhIndex :: forall f i sh. SNat i -> ListH sh f -> f (Index i sh)
+listhIndex :: forall i k sh. SNat k -> ListH sh i -> SMayNat i (Index k sh)
 listhIndex SZ (n ::# _) = n
-listhIndex (SS (i :: SNat i')) ((_ :: f n) ::# (sh :: ListH sh' f))
-  | Refl <- lemIndexSucc (Proxy @i') (Proxy @n) (Proxy @sh')
+listhIndex (SS (i :: SNat k')) ((_ :: SMayNat i n) ::# (sh :: ListH sh' i))
+  | Refl <- lemIndexSucc (Proxy @k') (Proxy @n) (Proxy @sh')
   = listhIndex i sh
 listhIndex _ ZH = error "Index into empty shape"
 
-listhPermutePrefix :: forall f is sh. Perm is -> ListH sh f -> ListH (PermutePrefix is sh) f
+listhPermutePrefix :: forall i is sh. Perm is -> ListH sh i -> ListH (PermutePrefix is sh) i
 listhPermutePrefix perm sh = listhAppend (listhPermute perm (listhTakeLen perm sh)) (listhDropLen perm sh)
 
 ssxTakeLen :: forall is sh. Perm is -> StaticShX sh -> StaticShX (TakeLen is sh)
-ssxTakeLen = coerce (listhTakeLen @(SMayNat ()))
+ssxTakeLen = coerce (listhTakeLen @())
 
 ssxDropLen :: Perm is -> StaticShX sh -> StaticShX (DropLen is sh)
-ssxDropLen = coerce (listhDropLen @(SMayNat ()))
+ssxDropLen = coerce (listhDropLen @())
 
 ssxPermute :: Perm is -> StaticShX sh -> StaticShX (Permute is sh)
-ssxPermute = coerce (listhPermute @(SMayNat ()))
+ssxPermute = coerce (listhPermute @())
 
 ssxIndex :: SNat i -> StaticShX sh -> SMayNat () (Index i sh)
-ssxIndex i = coerce (listhIndex @(SMayNat ()) i)
+ssxIndex i = coerce (listhIndex @() i)
 
 ssxPermutePrefix :: Perm is -> StaticShX sh -> StaticShX (PermutePrefix is sh)
-ssxPermutePrefix = coerce (listhPermutePrefix @(SMayNat ()))
+ssxPermutePrefix = coerce (listhPermutePrefix @())
 
 shxTakeLen :: forall is sh. Perm is -> IShX sh -> IShX (TakeLen is sh)
-shxTakeLen = coerce (listhTakeLen @(SMayNat Int))
+shxTakeLen = coerce (listhTakeLen @Int)
 
 shxDropLen :: Perm is -> IShX sh -> IShX (DropLen is sh)
-shxDropLen = coerce (listhDropLen @(SMayNat Int))
+shxDropLen = coerce (listhDropLen @Int)
 
 shxPermute :: Perm is -> IShX sh -> IShX (Permute is sh)
-shxPermute = coerce (listhPermute @(SMayNat Int))
+shxPermute = coerce (listhPermute @Int)
 
 shxIndex :: SNat i -> IShX sh -> SMayNat Int (Index i sh)
-shxIndex i = coerce (listhIndex @(SMayNat Int) i)
+shxIndex i = coerce (listhIndex @Int i)
 
 shxPermutePrefix :: Perm is -> IShX sh -> IShX (PermutePrefix is sh)
-shxPermutePrefix = coerce (listhPermutePrefix @(SMayNat Int))
+shxPermutePrefix = coerce (listhPermutePrefix @Int)
 
 
 listxTakeLen :: forall f is sh. Perm is -> ListX sh f -> ListX (TakeLen is sh) f
-- 
cgit v1.2.3-70-g09d2