Make the property argument to replace explicit

CHANGELOG_NEXT.md

@@ -206,6 +206,8 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
 
 #### Prelude
 
+* Made the property argument to `replace` explicit.
+
 * Added pipeline operators `(|>)` and `(<|)`.
 
 #### Base

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 : 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 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 big and thus cumbersome to write by
+hand. Idris provides a high level syntax which calculates the property
+and applies ``replace``:
 
 .. code-block:: idris
 

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``.

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 = ()

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

libs/base/Data/Nat/Order/Properties.idr

@@ -26,15 +26,15 @@ 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
 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

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

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 =

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)
 

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

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
 
 

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
 

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

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}

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

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 = ()

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
 

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 {p=\n => Vect n el} (plusCommutative k 1) (myReverse xs ++ [x])
+    myReplace {p=\n => Vect n el} (plusCommutative k 1) (myReverse xs ++ [x])

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])
+                     ^^