From 5c926beb1aeed724787812c35a70c5ae362bc1f7 Mon Sep 17 00:00:00 2001
From: Mikolaj Konarski <mikolaj.konarski@funktory.com>
Date: Fri, 16 May 2025 13:42:47 +0200
Subject: Generalize some shape conversion functions

---
 src/Data/Array/Nested/Ranked/Shape.hs | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 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 8f54673..aa89d88 100644
--- a/src/Data/Array/Nested/Ranked/Shape.hs
+++ b/src/Data/Array/Nested/Ranked/Shape.hs
@@ -213,14 +213,14 @@ ixrZero :: SNat n -> IIxR n
 ixrZero SZ = ZIR
 ixrZero (SS n) = 0 :.: ixrZero n
 
-ixrFromIxX :: IIxX sh -> IIxR (Rank sh)
+ixrFromIxX :: IxX sh i -> IxR (Rank sh) i
 ixrFromIxX ZIX = ZIR
 ixrFromIxX (n :.% idx) = n :.: ixrFromIxX idx
 
-ixxFromIxR :: IIxR n -> IIxX (Replicate n Nothing)
+ixxFromIxR :: IxR n i -> IxX (Replicate n Nothing) i
 ixxFromIxR ZIR = ZIX
-ixxFromIxR (n :.: (idx :: IxR m Int)) =
-  castWith (subst2 @IxX @Int (lemReplicateSucc @(Nothing @Nat) @m))
+ixxFromIxR (n :.: (idx :: IxR m i)) =
+  castWith (subst2 @IxX @i (lemReplicateSucc @(Nothing @Nat) @m))
     (n :.% ixxFromIxR idx)
 
 ixrHead :: IxR (n + 1) i -> i
@@ -288,10 +288,10 @@ shrFromShX2 sh
   | Refl <- lemRankReplicate (Proxy @n)
   = shrFromShX sh
 
-shxFromShR :: IShR n -> IShX (Replicate n Nothing)
+shxFromShR :: ShR n i -> ShX (Replicate n Nothing) i
 shxFromShR ZSR = ZSX
-shxFromShR (n :$: (idx :: ShR m Int)) =
-  castWith (subst2 @ShX @Int (lemReplicateSucc @(Nothing @Nat) @m))
+shxFromShR (n :$: (idx :: ShR m i)) =
+  castWith (subst2 @ShX @i (lemReplicateSucc @(Nothing @Nat) @m))
     (SUnknown n :$% shxFromShR idx)
 
 -- | This checks only whether the ranks are equal, not whether the actual
-- 
cgit v1.2.3-70-g09d2