From 436992de3845d65a944d0de9890447cb42fdb7f5 Mon Sep 17 00:00:00 2001
From: Joel Berkeley <16429957+joelberkeley@users.noreply.github.com>
Date: Sat, 12 Apr 2025 00:53:07 +0100
Subject: [PATCH 1/6] Make the property argument to `replace` explicit

---
 CHANGELOG_NEXT.md                                |  2 ++
 docs/source/proofs/patterns.rst                  | 10 +++++-----
 docs/source/proofs/propositional.rst             | 14 +++++++-------
 docs/source/tutorial/theorems.rst                |  2 +-
 libs/base/Data/Fin.idr                           |  2 +-
 libs/base/Data/Nat/Order/Properties.idr          |  6 +++---
 libs/base/Syntax/PreorderReasoning/Generic.idr   |  2 +-
 libs/contrib/Data/Nat/Factor.idr                 | 10 +++++-----
 libs/contrib/Data/Telescope/Segment.idr          |  6 +++---
 libs/contrib/Data/Vect/Properties/Fin.idr        |  2 +-
 libs/contrib/Decidable/Decidable/Extra.idr       |  6 +++---
 libs/papers/Data/Linear/Inverse.idr              |  4 ++--
 libs/papers/Language/IntrinsicTyping/Krivine.idr |  2 +-
 libs/papers/Search/Tychonoff/PartI.idr           |  6 +++---
 libs/prelude/Builtin.idr                         |  4 ++--
 samples/Proofs.idr                               |  2 +-
 tests/idris2/data/record021/Issue3501.idr        |  2 +-
 tests/idris2/error/perror021/Implicit.idr        |  2 +-
 18 files changed, 43 insertions(+), 41 deletions(-)

diff --git a/CHANGELOG_NEXT.md b/CHANGELOG_NEXT.md
index d3dd26951a1..9163e3f42a1 100644
--- a/CHANGELOG_NEXT.md
+++ b/CHANGELOG_NEXT.md
@@ -206,6 +206,8 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
 
 #### Prelude
 
+* The property argument to `replace` is now explicit.
+
 * Added pipeline operators `(|>)` and `(<|)`.
 
 #### Base
diff --git a/docs/source/proofs/patterns.rst b/docs/source/proofs/patterns.rst
index ed621e00b38..55faed35a5b 100644
--- a/docs/source/proofs/patterns.rst
+++ b/docs/source/proofs/patterns.rst
@@ -180,16 +180,16 @@ prelude:
 .. code-block:: idris
 
     Main> :t replace
-    Builtin.replace : (0 rule : x = y) -> p x -> p y
+    Builtin.replace : (0 p : _) -> (0 rule : x = y) -> p x -> p y
 
 Given a proof that ``x = y``, and a property ``p`` which holds for
 ``x``, we can get a proof of the same property for ``y``, because we
 know ``x`` and ``y`` must be the same. Note the multiplicity on ``rule``
 means that it's guaranteed to be erased at run time.
-In practice, this function can be
-a little tricky to use because in general the implicit argument ``p``
-can be hard to infer by unification, so Idris provides a high level
-syntax which calculates the property and applies ``replace``:
+In practice, this function can be a little tricky to use because in
+general the argument ``p`` can be hard to infer by unification, so
+Idris provides a high level syntax which calculates the property
+and applies ``replace``:
 
 .. code-block:: idris
 
diff --git a/docs/source/proofs/propositional.rst b/docs/source/proofs/propositional.rst
index 09294317819..4fc0352b3d0 100644
--- a/docs/source/proofs/propositional.rst
+++ b/docs/source/proofs/propositional.rst
@@ -56,8 +56,8 @@ To use this in our proofs there is the following function in the prelude:
 .. code-block:: idris
 
    ||| Perform substitution in a term according to some equality.
-   replace : forall x, y, prop . (0 rule : x = y) -> prop x -> prop y
-   replace Refl prf = prf
+   replace : forall x, y . (0 prop : _) -> (0 rule : x = y) -> prop x -> prop y
+   replace _ Refl prf = prf
 
 If we supply an equality (x=y) and a proof of a property of x (``prop x``) then we get
 a proof of a property of y (``prop y``).
@@ -70,15 +70,15 @@ the equality ``x=y`` then we get a proof that ``y=2``.
    p1 n = (n=2)
 
    testReplace: (x=y) -> (p1 x) -> (p1 y)
-   testReplace a b = replace a b
+   testReplace a b = replace p1 a b
 
 Rewrite
 =======
 
-In practice, ``replace`` can be
-a little tricky to use because in general the implicit argument ``prop``
-can be hard to infer for the machine, so Idris provides a high level
-syntax which calculates the property and applies ``replace``.
+In practice, ``replace`` can be a little tricky to use because in
+general the argument ``prop`` can be hard to infer for the machine,
+so Idris provides a high level syntax which calculates the property
+and applies ``replace``.
 
 Example: again we supply ``p1 x`` which is a proof that ``x=2`` and the equality
 ``y=x`` then we get a proof that ``y=2``.
diff --git a/docs/source/tutorial/theorems.rst b/docs/source/tutorial/theorems.rst
index ebf0599d819..7c759045ee7 100644
--- a/docs/source/tutorial/theorems.rst
+++ b/docs/source/tutorial/theorems.rst
@@ -60,7 +60,7 @@ never equal to a successor:
 .. code-block:: idris
 
     disjoint : (n : Nat) -> Z = S n -> Void
-    disjoint n prf = replace {p = disjointTy} prf ()
+    disjoint n prf = replace disjointTy prf ()
       where
         disjointTy : Nat -> Type
         disjointTy Z = ()
diff --git a/libs/base/Data/Fin.idr b/libs/base/Data/Fin.idr
index 0eff1af21d5..dd98b878855 100644
--- a/libs/base/Data/Fin.idr
+++ b/libs/base/Data/Fin.idr
@@ -28,7 +28,7 @@ coerce {n = Z} eq FZ impossible
 coerce {n = S _} eq (FS k) = FS (coerce (injective eq) k)
 coerce {n = Z} eq (FS k) impossible
 
-%transform "coerce-identity" coerce eq k = replace {p = Fin} eq k
+%transform "coerce-identity" coerce eq k = replace Fin eq k
 
 export
 Uninhabited (Fin Z) where
diff --git a/libs/base/Data/Nat/Order/Properties.idr b/libs/base/Data/Nat/Order/Properties.idr
index 2fe81fb5262..18b842181a8 100644
--- a/libs/base/Data/Nat/Order/Properties.idr
+++ b/libs/base/Data/Nat/Order/Properties.idr
@@ -26,7 +26,7 @@ ltReflection a = lteReflection (S a)
 -- For example:
 export
 lteIsLTE : (a, b : Nat) -> a `lte` b = True -> a `LTE` b
-lteIsLTE  a b prf = invert (replace {p = Reflects (a `LTE` b)} prf (lteReflection a b))
+lteIsLTE  a b prf = invert (replace (Reflects (a `LTE` b)) prf (lteReflection a b))
 
 export
 ltIsLT : (a, b : Nat) -> a `lt` b = True -> a `LT` b
@@ -34,7 +34,7 @@ ltIsLT  a = lteIsLTE (S a)
 
 export
 notlteIsNotLTE : (a, b : Nat) -> a `lte` b = False -> Not (a `LTE` b)
-notlteIsNotLTE a b prf = invert (replace {p = Reflects (a `LTE` b)} prf (lteReflection a b))
+notlteIsNotLTE a b prf = invert (replace (Reflects (a `LTE` b)) prf (lteReflection a b))
 
 export
 notltIsNotLT : (a, b : Nat) -> a `lt` b = False -> Not (a `LT` b)
@@ -45,7 +45,7 @@ export
 notlteIsLT : (a, b : Nat) -> a `lte` b = False -> b `LT` a
 notlteIsLT a b prf = notLTImpliesGTE $
                        \prf' =>
-                         (invert $ replace {p = Reflects (S a `LTE` S b)} prf
+                         (invert $ replace (Reflects (S a `LTE` S b)) prf
                                  $ lteReflection (S a) (S b)) prf'
 
 export
diff --git a/libs/base/Syntax/PreorderReasoning/Generic.idr b/libs/base/Syntax/PreorderReasoning/Generic.idr
index 2f77322698a..6082a76d3b3 100644
--- a/libs/base/Syntax/PreorderReasoning/Generic.idr
+++ b/libs/base/Syntax/PreorderReasoning/Generic.idr
@@ -74,7 +74,7 @@ public export
 (~~) : {0 x : dom} -> {0 y : dom}
          -> FastDerivation leq x y -> {0 z : dom} -> (0 step : Step Equal y z)
          -> FastDerivation leq x z
-(~~) der (z ... yEqZ) = replace {p = FastDerivation leq _} yEqZ der
+(~~) der (z ... yEqZ) = replace (FastDerivation leq _) yEqZ der
 
 -- Smart constructors
 public export
diff --git a/libs/contrib/Data/Nat/Factor.idr b/libs/contrib/Data/Nat/Factor.idr
index faf817387a4..7d512f73b42 100644
--- a/libs/contrib/Data/Nat/Factor.idr
+++ b/libs/contrib/Data/Nat/Factor.idr
@@ -199,7 +199,7 @@ export
 factorLteNumber : Factor p n -> {auto positN : LTE 1 n} -> LTE p n
 factorLteNumber (CofactorExists Z prf) =
         let nIsZero = trans prf $ multCommutative p 0
-            oneLteZero = replace {p = LTE 1} nIsZero positN
+            oneLteZero = replace (LTE 1) nIsZero positN
         in
         absurd $ succNotLTEzero oneLteZero
 factorLteNumber (CofactorExists (S k) prf) =
@@ -258,7 +258,7 @@ minusFactor (CofactorExists qab prfAB) (CofactorExists qa prfA) =
             rewrite multDistributesOverMinusRight p qab qa in
             rewrite sym prfA in
             rewrite sym prfAB in
-            replace {p = \x => b = minus (a + b) x} (plusZeroRightNeutral a) $
+            replace (\x => b = minus (a + b) x) (plusZeroRightNeutral a) $
             rewrite plusMinusLeftCancel a b 0 in
             rewrite minusZeroRight b in
             Refl
@@ -459,15 +459,15 @@ export
 divByGcdGcdOne : {a, b, c : Nat} -> GCD a (a * b) (a * c) -> GCD 1 b c
 divByGcdGcdOne {a = Z} (MkGCD _ _) impossible
 divByGcdGcdOne {a = S a} {b = Z} {c = Z} (MkGCD {notBothZero} _ _) =
-        case replace {p = \x => NotBothZero x x} (multZeroRightZero (S a)) notBothZero of
+        case replace (\x => NotBothZero x x) (multZeroRightZero (S a)) notBothZero of
             LeftIsNotZero impossible
             RightIsNotZero impossible
 divByGcdGcdOne {a = S a} {b = Z} {c = S c} gcdPrf@(MkGCD {notBothZero} _ _) =
-        case replace {p = \x => NotBothZero x (S a * S c)} (multZeroRightZero (S a)) notBothZero of
+        case replace (\x => NotBothZero x (S a * S c)) (multZeroRightZero (S a)) notBothZero of
             LeftIsNotZero impossible
             RightIsNotZero => symmetric $ divByGcdHelper a c Z $ symmetric gcdPrf
 divByGcdGcdOne {a = S a} {b = S b} {c = Z} gcdPrf@(MkGCD {notBothZero} _ _) =
-        case replace {p = \x => NotBothZero (S a * S b) x} (multZeroRightZero (S a)) notBothZero of
+        case replace (\x => NotBothZero (S a * S b) x) (multZeroRightZero (S a)) notBothZero of
             RightIsNotZero impossible
             LeftIsNotZero => divByGcdHelper a b Z gcdPrf
 divByGcdGcdOne {a = S a} {b = S b} {c = S c} gcdPrf =
diff --git a/libs/contrib/Data/Telescope/Segment.idr b/libs/contrib/Data/Telescope/Segment.idr
index 1d97e6a95fb..e109b5c1446 100644
--- a/libs/contrib/Data/Telescope/Segment.idr
+++ b/libs/contrib/Data/Telescope/Segment.idr
@@ -219,7 +219,7 @@ breakOnto : {0 k,k' : Nat} -> (gamma : Telescope k) -> (pos : Position gamma)
          -> {auto 0 ford1 : k' === (finToNat $ finComplement pos) }
          -> {default
                -- disgusting, sorry
-               (replace {p = \u => k = finToNat pos + u}
+               (replace (\u => k = finToNat pos + u)
                         (sym ford1)
                         (sym $ finComplementSpec pos))
              0 ford2 : (k === ((finToNat pos) + k')) }
@@ -252,12 +252,12 @@ breakStartEmpty {k} {k' = S k'} {ford1} {ford2} (gamma -. ty) =
                     v : break {k} {k'} gamma (start gamma) {ford = u}
                         ~=~ Telescope.Nil
                     v = breakStartEmpty {k} {k'} gamma {ford2 = u}
-                in replace {p = \z =>
+                in replace (\z =>
                              Equal {a = Telescope k} {b = Telescope 0}
                                    (break {k'} {k} gamma (start gamma)
                                           {ford = z})
                                           []
-                        }
+                        )
                         (uip u _)
                         (keep v)
 
diff --git a/libs/contrib/Data/Vect/Properties/Fin.idr b/libs/contrib/Data/Vect/Properties/Fin.idr
index 0cdcde58358..c548f75afd8 100644
--- a/libs/contrib/Data/Vect/Properties/Fin.idr
+++ b/libs/contrib/Data/Vect/Properties/Fin.idr
@@ -25,7 +25,7 @@ finNonZero (FS i) = ItIsSucc
 ||| Inhabitants of `Fin n` witness runtime-irrelevant vectors of length `n` aren't empty
 export
 finNonEmpty : (0 xs : Vect n a) -> NonZero n -> NonEmpty xs
-finNonEmpty xs ItIsSucc = replace {p = NonEmpty} (etaCons xs) IsNonEmpty
+finNonEmpty xs ItIsSucc = replace NonEmpty (etaCons xs) IsNonEmpty
 
 ||| Cast an index into a runtime-irrelevant `Vect` into the position
 ||| of the corresponding element
diff --git a/libs/contrib/Decidable/Decidable/Extra.idr b/libs/contrib/Decidable/Decidable/Extra.idr
index 6b1c2ce3162..c0b4d6f7b7e 100644
--- a/libs/contrib/Decidable/Decidable/Extra.idr
+++ b/libs/contrib/Decidable/Decidable/Extra.idr
@@ -64,9 +64,9 @@ decideTransform :
   -> IsDecidable n ts (chain {ts} t r)
 decideTransform tDec posDec =
   curryAll $ \xs =>
-    replace {p = id} (chainUncurry (chain t r) Dec xs) $
-      replace {p = Dec} (chainUncurry r t xs) $
-        tDec $ replace {p = id} (sym $ chainUncurry r Dec xs) $
+    replace id (chainUncurry (chain t r) Dec xs) $
+      replace Dec (chainUncurry r t xs) $
+        tDec $ replace id (sym $ chainUncurry r Dec xs) $
           uncurryAll posDec xs
 
 
diff --git a/libs/papers/Data/Linear/Inverse.idr b/libs/papers/Data/Linear/Inverse.idr
index 3b60a6415b6..22b019914fb 100644
--- a/libs/papers/Data/Linear/Inverse.idr
+++ b/libs/papers/Data/Linear/Inverse.idr
@@ -138,7 +138,7 @@ powMinusAux : (m, n : Nat) -> CmpNat m n ->
   Pow a (cast m) -@ Pow a (- cast n) -@ Pow a (cast m - cast n)
 powMinusAux m (m + S n) (CmpLT n) pos neg
   = let (neg1 # neg2) = powNegativeL m (S n) neg in
-    powAnnihilate m pos neg1 `seq` replace {p = Pow a} eq neg2
+    powAnnihilate m pos neg1 `seq` replace (Pow a) eq neg2
 
   where
 
@@ -159,7 +159,7 @@ powMinusAux m m CmpEQ pos neg
     powAnnihilate (cast m) pos neg
 powMinusAux (_ + S m) n (CmpGT m) pos neg
   = let (pos1 # pos2) = powPositiveL n (S m) pos in
-    powAnnihilate n pos1 neg `seq` replace {p = Pow a} eq pos2
+    powAnnihilate n pos1 neg `seq` replace (Pow a) eq pos2
 
   where
 
diff --git a/libs/papers/Language/IntrinsicTyping/Krivine.idr b/libs/papers/Language/IntrinsicTyping/Krivine.idr
index 5b92c9dbd92..505ddb4a0b0 100644
--- a/libs/papers/Language/IntrinsicTyping/Krivine.idr
+++ b/libs/papers/Language/IntrinsicTyping/Krivine.idr
@@ -269,7 +269,7 @@ expand {a = Arr a b} {c = ClApp f t} (tr, hored)
   = MkPair (step tr)
   $ \ arg, red =>
     let 0 eq = headReduceClApp (ClApp f t) (\case Lam impossible) arg in
-    let red = replace {p = Reducible b} (sym eq) (hored arg red) in
+    let red = replace (Reducible b) (sym eq) (hored arg red) in
     expand {c = ClApp (ClApp f t) arg} red
 
 public export
diff --git a/libs/papers/Search/Tychonoff/PartI.idr b/libs/papers/Search/Tychonoff/PartI.idr
index 50c7f50236f..6a93453adab 100644
--- a/libs/papers/Search/Tychonoff/PartI.idr
+++ b/libs/papers/Search/Tychonoff/PartI.idr
@@ -52,7 +52,7 @@ record (<->) (a, b : Type) where
 map : (a <-> b) -> IsSearchable a -> IsSearchable b
 map (MkIso f g _ inv) search p pdec =
   let (xa ** prfa) = search (p . f) (\ x => pdec (f x)) in
-  (f xa ** \ xb, pxb => prfa (g xb) $ replace {p} (sym $ inv xb) pxb)
+  (f xa ** \ xb, pxb => prfa (g xb) $ replace p (sym $ inv xb) pxb)
 
 interface Searchable (0 a : Type) where
   constructor MkSearchable
@@ -485,7 +485,7 @@ discreteIsUContinuous pdec = MkUC 1 isUContinuous where
 
   isUContinuous : IsUModFor PartI.dc p 1
   isUContinuous v w hyp pv with (decEq v w)
-    _ | Yes eq = replace {p} eq pv
+    _ | Yes eq = replace p eq pv
     _ | No neq = absurd (hyp 0 Oh)
 
 [PROMOTE] Discrete x => CSearchable x PartI.dc => Searchable x where
@@ -571,7 +571,7 @@ parameters
                  v0s : Nat -> x; v0s = tail vv0s
              in sH .snd v0
               $ (sT v0) .snd v0s
-              $ replace {p} (eta vv0s) pvv0s
+              $ replace p (eta vv0s) pvv0s
 
 cantorIsCSearchable : Extensionality => IsCSearchable (Nat -> Bool) PartI.dsc
 cantorIsCSearchable = csearch @{BYUCONTINUITY}
diff --git a/libs/prelude/Builtin.idr b/libs/prelude/Builtin.idr
index 85e778142f0..5e00cd8ebca 100644
--- a/libs/prelude/Builtin.idr
+++ b/libs/prelude/Builtin.idr
@@ -161,8 +161,8 @@ rewrite__impl p Refl prf = prf
 ||| Perform substitution in a term according to some equality.
 %inline
 public export
-replace : forall x, y, p . (0 rule : x = y) -> (1 _ : p x) -> p y
-replace Refl prf = prf
+replace : forall x, y . (0 p : _) -> (0 rule : x = y) -> (1 _ : p x) -> p y
+replace _ Refl prf = prf
 
 ||| Symmetry of propositional equality.
 %inline
diff --git a/samples/Proofs.idr b/samples/Proofs.idr
index c5fa68de2bb..6e144dbcd6a 100644
--- a/samples/Proofs.idr
+++ b/samples/Proofs.idr
@@ -8,7 +8,7 @@ twoPlusTwo = Refl
 -- twoPlusTwoBad = Refl
 
 disjoint : (n : Nat) -> Z = S n -> Void
-disjoint n prf = replace {p = disjointTy} prf ()
+disjoint n prf = replace disjointTy prf ()
   where
     disjointTy : Nat -> Type
     disjointTy Z = ()
diff --git a/tests/idris2/data/record021/Issue3501.idr b/tests/idris2/data/record021/Issue3501.idr
index a75048422f7..53782afff01 100644
--- a/tests/idris2/data/record021/Issue3501.idr
+++ b/tests/idris2/data/record021/Issue3501.idr
@@ -2,6 +2,6 @@ import Data.Vect
 record Foo (th : Vect n a) where
   nIsZero     : n === 0
   vectIsEmpty : (th ===)
-                 $ replace {p = \ n => Vect n a} (sym nIsZero)
+                 $ replace (\ n => Vect n a) (sym nIsZero)
                  $ Nil
 
diff --git a/tests/idris2/error/perror021/Implicit.idr b/tests/idris2/error/perror021/Implicit.idr
index 2fae069a62a..70c97bfc5b0 100644
--- a/tests/idris2/error/perror021/Implicit.idr
+++ b/tests/idris2/error/perror021/Implicit.idr
@@ -3,4 +3,4 @@ import Data.Vect
 myReverse : Vect n el -> Vect n el
 myReverse [] = []
 myReverse {n = S k} (x :: xs) =
-    replace {p=\n => Vect n el} (plusCommutative k 1) (myReverse xs ++ [x])
+    replace (\n => Vect n el) (plusCommutative k 1) (myReverse xs ++ [x])

From f49abe9f7914563484c289cdeed1ad6c7893f042 Mon Sep 17 00:00:00 2001
From: Joel Berkeley <16429957+joelberkeley@users.noreply.github.com>
Date: Sat, 12 Apr 2025 01:26:05 +0100
Subject: [PATCH 2/6] wording

---
 CHANGELOG_NEXT.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/CHANGELOG_NEXT.md b/CHANGELOG_NEXT.md
index 9163e3f42a1..074799cdb5d 100644
--- a/CHANGELOG_NEXT.md
+++ b/CHANGELOG_NEXT.md
@@ -206,7 +206,7 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
 
 #### Prelude
 
-* The property argument to `replace` is now explicit.
+* Made the property argument to `replace` explicit.
 
 * Added pipeline operators `(|>)` and `(<|)`.
 

From 4bf7e06527f8304e030952b667e7622978e1a043 Mon Sep 17 00:00:00 2001
From: Joel Berkeley <16429957+joelberkeley@users.noreply.github.com>
Date: Sat, 12 Apr 2025 16:39:55 +0100
Subject: [PATCH 3/6] delete test

---
 src/Core/TT/Var.idr                       |  2 +-
 tests/idris2/error/perror021/Implicit.idr |  6 ------
 tests/idris2/error/perror021/expected     | 11 -----------
 tests/idris2/error/perror021/run          |  3 ---
 4 files changed, 1 insertion(+), 21 deletions(-)
 delete mode 100644 tests/idris2/error/perror021/Implicit.idr
 delete mode 100644 tests/idris2/error/perror021/expected
 delete mode 100644 tests/idris2/error/perror021/run

diff --git a/src/Core/TT/Var.idr b/src/Core/TT/Var.idr
index 163c8857504..9d2aa41b034 100644
--- a/src/Core/TT/Var.idr
+++ b/src/Core/TT/Var.idr
@@ -283,7 +283,7 @@ insertNVarChiply : SizeOf local ->
 insertNVarChiply p v
   = rewrite chipsAsListAppend local (n :: outer) in
     insertNVar (p <>> zero)
-  $ replace {p = NVar nm} (chipsAsListAppend local outer) v
+  $ replace (NVar nm) (chipsAsListAppend local outer) v
 
 export
 insertNVarNames : GenWeakenable (NVar name)
diff --git a/tests/idris2/error/perror021/Implicit.idr b/tests/idris2/error/perror021/Implicit.idr
deleted file mode 100644
index 70c97bfc5b0..00000000000
--- a/tests/idris2/error/perror021/Implicit.idr
+++ /dev/null
@@ -1,6 +0,0 @@
-import Data.Vect
-
-myReverse : Vect n el -> Vect n el
-myReverse [] = []
-myReverse {n = S k} (x :: xs) =
-    replace (\n => Vect n el) (plusCommutative k 1) (myReverse xs ++ [x])
diff --git a/tests/idris2/error/perror021/expected b/tests/idris2/error/perror021/expected
deleted file mode 100644
index f1e69f95068..00000000000
--- a/tests/idris2/error/perror021/expected
+++ /dev/null
@@ -1,11 +0,0 @@
-1/1: Building Implicit (Implicit.idr)
-Error: Expected '}'.
-
-Implicit:6:15--6:17
- 2 | 
- 3 | myReverse : Vect n el -> Vect n el
- 4 | myReverse [] = []
- 5 | myReverse {n = S k} (x :: xs) =
- 6 |     replace {p=\n => Vect n el} (plusCommutative k 1) (myReverse xs ++ [x])
-                   ^^
-
diff --git a/tests/idris2/error/perror021/run b/tests/idris2/error/perror021/run
deleted file mode 100644
index c88212c0ede..00000000000
--- a/tests/idris2/error/perror021/run
+++ /dev/null
@@ -1,3 +0,0 @@
-. ../../../testutils.sh
-
-check Implicit.idr

From 92f498c0fcbd3a7bace239b1e4ee3042e24d533f Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Tue, 12 Aug 2025 15:08:04 +0100
Subject: [PATCH 4/6] Revert "delete test"

This reverts commit 4bf7e06527f8304e030952b667e7622978e1a043.
---
 src/Core/TT/Var.idr                       |  2 +-
 tests/idris2/error/perror021/Implicit.idr |  6 ++++++
 tests/idris2/error/perror021/expected     | 11 +++++++++++
 tests/idris2/error/perror021/run          |  3 +++
 4 files changed, 21 insertions(+), 1 deletion(-)
 create mode 100644 tests/idris2/error/perror021/Implicit.idr
 create mode 100644 tests/idris2/error/perror021/expected
 create mode 100644 tests/idris2/error/perror021/run

diff --git a/src/Core/TT/Var.idr b/src/Core/TT/Var.idr
index 9d2aa41b034..163c8857504 100644
--- a/src/Core/TT/Var.idr
+++ b/src/Core/TT/Var.idr
@@ -283,7 +283,7 @@ insertNVarChiply : SizeOf local ->
 insertNVarChiply p v
   = rewrite chipsAsListAppend local (n :: outer) in
     insertNVar (p <>> zero)
-  $ replace (NVar nm) (chipsAsListAppend local outer) v
+  $ replace {p = NVar nm} (chipsAsListAppend local outer) v
 
 export
 insertNVarNames : GenWeakenable (NVar name)
diff --git a/tests/idris2/error/perror021/Implicit.idr b/tests/idris2/error/perror021/Implicit.idr
new file mode 100644
index 00000000000..70c97bfc5b0
--- /dev/null
+++ b/tests/idris2/error/perror021/Implicit.idr
@@ -0,0 +1,6 @@
+import Data.Vect
+
+myReverse : Vect n el -> Vect n el
+myReverse [] = []
+myReverse {n = S k} (x :: xs) =
+    replace (\n => Vect n el) (plusCommutative k 1) (myReverse xs ++ [x])
diff --git a/tests/idris2/error/perror021/expected b/tests/idris2/error/perror021/expected
new file mode 100644
index 00000000000..f1e69f95068
--- /dev/null
+++ b/tests/idris2/error/perror021/expected
@@ -0,0 +1,11 @@
+1/1: Building Implicit (Implicit.idr)
+Error: Expected '}'.
+
+Implicit:6:15--6:17
+ 2 | 
+ 3 | myReverse : Vect n el -> Vect n el
+ 4 | myReverse [] = []
+ 5 | myReverse {n = S k} (x :: xs) =
+ 6 |     replace {p=\n => Vect n el} (plusCommutative k 1) (myReverse xs ++ [x])
+                   ^^
+
diff --git a/tests/idris2/error/perror021/run b/tests/idris2/error/perror021/run
new file mode 100644
index 00000000000..c88212c0ede
--- /dev/null
+++ b/tests/idris2/error/perror021/run
@@ -0,0 +1,3 @@
+. ../../../testutils.sh
+
+check Implicit.idr

From a3f5714e6b919fa4342eb19c3703576f11734317 Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Tue, 12 Aug 2025 15:13:23 +0100
Subject: [PATCH 5/6] [ fix ] update parse error test

---
 tests/idris2/error/perror021/Implicit.idr |  5 ++++-
 tests/idris2/error/perror021/expected     | 14 +++++++-------
 2 files changed, 11 insertions(+), 8 deletions(-)

diff --git a/tests/idris2/error/perror021/Implicit.idr b/tests/idris2/error/perror021/Implicit.idr
index 70c97bfc5b0..a1563518876 100644
--- a/tests/idris2/error/perror021/Implicit.idr
+++ b/tests/idris2/error/perror021/Implicit.idr
@@ -1,6 +1,9 @@
 import Data.Vect
 
+myReplace : x === y -> p x -> p y
+myReplace Refl px = px
+
 myReverse : Vect n el -> Vect n el
 myReverse [] = []
 myReverse {n = S k} (x :: xs) =
-    replace (\n => Vect n el) (plusCommutative k 1) (myReverse xs ++ [x])
+    myReplace {p=\n => Vect n el} (plusCommutative k 1) (myReverse xs ++ [x])
diff --git a/tests/idris2/error/perror021/expected b/tests/idris2/error/perror021/expected
index f1e69f95068..0552046da95 100644
--- a/tests/idris2/error/perror021/expected
+++ b/tests/idris2/error/perror021/expected
@@ -1,11 +1,11 @@
 1/1: Building Implicit (Implicit.idr)
 Error: Expected '}'.
 
-Implicit:6:15--6:17
- 2 | 
- 3 | myReverse : Vect n el -> Vect n el
- 4 | myReverse [] = []
- 5 | myReverse {n = S k} (x :: xs) =
- 6 |     replace {p=\n => Vect n el} (plusCommutative k 1) (myReverse xs ++ [x])
-                   ^^
+Implicit:9:17--9:19
+ 5 | 
+ 6 | myReverse : Vect n el -> Vect n el
+ 7 | myReverse [] = []
+ 8 | myReverse {n = S k} (x :: xs) =
+ 9 |     myReplace {p=\n => Vect n el} (plusCommutative k 1) (myReverse xs ++ [x])
+                     ^^
 

From 5fb3db3b4044d1e5a2b151701e7788ae56cbf0fe Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Tue, 12 Aug 2025 15:14:34 +0100
Subject: [PATCH 6/6] [ doc ] wording

---
 docs/source/proofs/patterns.rst | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/docs/source/proofs/patterns.rst b/docs/source/proofs/patterns.rst
index 55faed35a5b..5d8d50e1e49 100644
--- a/docs/source/proofs/patterns.rst
+++ b/docs/source/proofs/patterns.rst
@@ -180,15 +180,15 @@ prelude:
 .. code-block:: idris
 
     Main> :t replace
-    Builtin.replace : (0 p : _) -> (0 rule : x = y) -> p x -> p y
+    Builtin.replace : (0 p : a -> Type) -> (0 rule : x = y) -> p x -> p y
 
 Given a proof that ``x = y``, and a property ``p`` which holds for
 ``x``, we can get a proof of the same property for ``y``, because we
 know ``x`` and ``y`` must be the same. Note the multiplicity on ``rule``
 means that it's guaranteed to be erased at run time.
 In practice, this function can be a little tricky to use because in
-general the argument ``p`` can be hard to infer by unification, so
-Idris provides a high level syntax which calculates the property
+general the argument ``p`` can be big and thus cumbersome to write by
+hand. Idris provides a high level syntax which calculates the property
 and applies ``replace``:
 
 .. code-block:: idris