From 24d93b59d75c1ea11f4443965d681236c459b439 Mon Sep 17 00:00:00 2001
From: Mikolaj Konarski <mikolaj.konarski@funktory.com>
Date: Fri, 26 Sep 2025 21:09:23 +0200
Subject: Done

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

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

diff --git a/src/Data/Array/Nested/Ranked.hs b/src/Data/Array/Nested/Ranked.hs
index 9778c54..8b95d0f 100644
--- a/src/Data/Array/Nested/Ranked.hs
+++ b/src/Data/Array/Nested/Ranked.hs
@@ -85,7 +85,7 @@ rsumOuter1P :: forall n a.
                (Storable a, NumElt a)
             => Ranked (n + 1) (Primitive a) -> Ranked n (Primitive a)
 rsumOuter1P (Ranked arr)
-  | Refl <- lemReplicateSucc @(Nothing @Nat) @n
+  | Refl <- lemReplicateSucc @(Nothing @Nat) (Proxy @n)
   = Ranked (msumOuter1P arr)
 
 rsumOuter1 :: forall n a. (NumElt a, PrimElt a)
@@ -108,7 +108,7 @@ rtranspose perm arr
 
 rconcat :: forall n a. Elt a => NonEmpty (Ranked (n + 1) a) -> Ranked (n + 1) a
 rconcat
-  | Refl <- lemReplicateSucc @(Nothing @Nat) @n
+  | Refl <- lemReplicateSucc @(Nothing @Nat) (Proxy @n)
   = coerce mconcat
 
 rappend :: forall n a. Elt a
@@ -116,7 +116,7 @@ rappend :: forall n a. Elt a
 rappend arr1 arr2
   | sn@SNat <- rrank arr1
   , Dict <- lemKnownReplicate sn
-  , Refl <- lemReplicateSucc @(Nothing @Nat) @n
+  , Refl <- lemReplicateSucc @(Nothing @Nat) (SNat @n)
   = coerce (mappend @Nothing @Nothing @(Replicate n Nothing))
       arr1 arr2
 
@@ -142,7 +142,7 @@ rfromList1 l = Ranked (mfromList1 l)
 
 rfromListOuter :: forall n a. Elt a => NonEmpty (Ranked n a) -> Ranked (n + 1) a
 rfromListOuter l
-  | Refl <- lemReplicateSucc @(Nothing @Nat) @n
+  | Refl <- lemReplicateSucc @(Nothing @Nat) (Proxy @n)
   = Ranked (mfromListOuter (coerce l :: NonEmpty (Mixed (Replicate n Nothing) a)))
 
 rfromListLinear :: forall n a. Elt a => IShR n -> NonEmpty a -> Ranked n a
@@ -161,7 +161,7 @@ rtoList = map runScalar . rtoListOuter
 
 rtoListOuter :: forall n a. Elt a => Ranked (n + 1) a -> [Ranked n a]
 rtoListOuter (Ranked arr)
-  | Refl <- lemReplicateSucc @(Nothing @Nat) @n
+  | Refl <- lemReplicateSucc @(Nothing @Nat) (Proxy @n)
   = coerce (mtoListOuter @a @Nothing @(Replicate n Nothing) arr)
 
 rtoListLinear :: Elt a => Ranked n a -> [a]
@@ -173,9 +173,9 @@ rfromOrthotope sn arr
   = let xarr = XArray arr
     in Ranked (fromPrimitive (M_Primitive (X.shape (ssxFromSNat sn) xarr) xarr))
 
-rtoOrthotope :: PrimElt a => Ranked n a -> S.Array n a
+rtoOrthotope :: forall a n. PrimElt a => Ranked n a -> S.Array n a
 rtoOrthotope (rtoPrimitive -> Ranked (M_Primitive sh (XArray arr)))
-  | Refl <- lemRankReplicate (shrRank $ shrFromShX2 sh)
+  | Refl <- lemRankReplicate (shrRank $ shrFromShX2 @n sh)
   = arr
 
 runScalar :: Elt a => Ranked 0 a -> a
@@ -255,7 +255,7 @@ rreplicateScal sh x = rfromPrimitive (rreplicateScalP sh x)
 
 rslice :: forall n a. Elt a => Int -> Int -> Ranked (n + 1) a -> Ranked (n + 1) a
 rslice i n arr
-  | Refl <- lemReplicateSucc @(Nothing @Nat) @n
+  | Refl <- lemReplicateSucc @(Nothing @Nat) (Proxy @n)
   = rlift (rrank arr)
           (\_ -> X.sliceU i n)
           arr
@@ -264,7 +264,7 @@ rrev1 :: forall n a. Elt a => Ranked (n + 1) a -> Ranked (n + 1) a
 rrev1 arr =
   rlift (rrank arr)
         (\(_ :: StaticShX sh') ->
-          case lemReplicateSucc @(Nothing @Nat) @n of
+          case lemReplicateSucc @(Nothing @Nat) (Proxy @n) of
             Refl -> X.rev1 @Nothing @(Replicate n Nothing ++ sh'))
         arr
 
-- 
cgit v1.2.3-70-g09d2