fix: remove withoutRecover from apply elaboration (#5862)

The assumptions behind disabling error recovery for the `apply` tactic
no longer seem to hold, since tactic combinators like `first` themselves
disable error recovery when it makes sense.

This addresses part of #3831

Breaking change: `elabTermForApply` no longer uses `withoutRecover`.
Tactics using `elabTermForApply` should evaluate whether it makes sense
to wrap it with `withoutRecover`, which is generally speaking when it's
used to elaborate identifiers.

src/Lean/Elab/Tactic/Conv/Unfold.lean

@@ -13,7 +13,7 @@ open Meta
 @[builtin_tactic Lean.Parser.Tactic.Conv.unfold] def evalUnfold : Tactic := fun stx => withMainContext do
   for declNameId in stx[1].getArgs do
     withRef declNameId do
-      let e ← elabTermForApply declNameId (mayPostpone := false)
+      let e ← withoutRecover <| elabTermForApply declNameId (mayPostpone := false)
       match e with
       | .const declName _ =>
         applySimpResult (← unfold (← getLhs) declName)

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -257,45 +257,11 @@ def elabTermForApply (stx : Syntax) (mayPostpone := true) : TacticM Expr := do
     match (← Term.resolveId? stx (withInfo := true)) with
     | some e => return e
     | _      => pure ()
-  /-
-    By disabling the "error recovery" (and consequently "error to sorry") feature,
-    we make sure an `apply e` fails without logging an error message.
-    The motivation is that `apply` is frequently used when writing tactic such as
-    ```
-    cases h <;> intro h' <;> first | apply t[h'] | ....
-    ```
-    Here the type of `h'` may be different in each case, and the term `t[h']` containing `h'` may even fail to
-    be elaborated in some cases. When this happens we want the tactic to fail without reporting any error to the user,
-    and the next tactic is tried.
+  elabTerm stx none mayPostpone
 
-    A drawback of disabling "error to sorry" is that there is no error recovery after the error is thrown, and features such
-    as auto-completion are affected.
-
-    By disabling "error to sorry", we also limit ourselves to at most one error at `t[h']`.
-
-    By disabling "error to sorry", we also miss the opportunity to catch mistakes in tactic code such as
-      `first | apply nonsensical-term | assumption`
-
-    This should not be a big problem for the `apply` tactic since we usually provide small terms there.
-
-    Note that we do not disable "error to sorry" at `exact` and `refine` since they are often used to elaborate big terms,
-    and we do want error recovery there, and we want to see the error messages.
-
-    We should probably provide options for allowing users to control this behavior.
-
-    see issue #1037
-
-    More complex solution:
-      - We do not disable "error to sorry"
-      - We elaborate term and check whether errors were produced
-      - If there are other tactic branches and there are errors, we remove the errors from the log, and throw a new error to force the tactic to backtrack.
-  -/
-  withoutRecover <| elabTerm stx none mayPostpone
-
-def getFVarId (id : Syntax) : TacticM FVarId := withRef id do
+def getFVarId (id : Syntax) : TacticM FVarId := withRef id <| withMainContext do
   -- use apply-like elaboration to suppress insertion of implicit arguments
-  let e ← withMainContext do
-    elabTermForApply id (mayPostpone := false)
+  let e ← withoutRecover <| elabTermForApply id (mayPostpone := false)
   match e with
   | Expr.fvar fvarId => return fvarId
   | _                => throwError "unexpected term '{e}'; expected single reference to variable"

src/Lean/Elab/Tactic/Unfold.lean

@@ -30,7 +30,7 @@ def zetaDeltaTarget (declFVarId : FVarId) : TacticM Unit := do
     go declNameId loc
 where
   go (declNameId : Syntax) (loc : Location) : TacticM Unit := withMainContext <| withRef declNameId do
-    let e ← elabTermForApply declNameId (mayPostpone := false)
+    let e ← withoutRecover <| elabTermForApply declNameId (mayPostpone := false)
     match e with
     | .const declName _ =>
       withLocation loc (unfoldLocalDecl declName) (unfoldTarget declName) (throwTacticEx `unfold · m!"did not unfold '{declName}'")

tests/lean/1719.lean.expected.out

@@ -1,6 +1,2 @@
 1719.lean:2:8-2:12: error: invalid dotted identifier notation, expected type is not of the form (... → C ...) where C is a constant
   ?m
-1719.lean:1:27-2:12: error: unsolved goals
-P Q : Prop
-h : P
-⊢ P ∨ Q

tests/lean/run/1037.lean

@@ -11,3 +11,10 @@ example (p q r s: Prop) (h1: p -> s) (h2: q -> s) (h3: r -> s)
   (try (apply h.elim <;> intro h)) <;>
   revert h <;> assumption;
 }
+
+/-!
+Verify that `withoutRecover` is not necessary for `apply`.
+This is because `first` enables it itself.
+-/
+example (p : Prop) (h : p) : p := by
+  first | apply bogusTerm | assumption