feat: improve error recovery at Tactic.elabTerm

src/Lean/Elab/Match.lean

@@ -939,7 +939,7 @@ register_builtin_option match.ignoreUnusedAlts : Bool := {
 
 def reportMatcherResultErrors (altLHSS : List AltLHS) (result : MatcherResult) : TermElabM Unit := do
   unless result.counterExamples.isEmpty do
-    withHeadRefOnly <| throwError "missing cases:\n{Meta.Match.counterExamplesToMessageData result.counterExamples}"
+    withHeadRefOnly <| logError m!"missing cases:\n{Meta.Match.counterExamplesToMessageData result.counterExamples}"
   unless match.ignoreUnusedAlts.get (← getOptions) || result.unusedAltIdxs.isEmpty do
     let mut i := 0
     for alt in altLHSS do

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -15,8 +15,12 @@ open Meta
 
 /- `elabTerm` for Tactics and basic tactics that use it. -/
 
-def elabTerm (stx : Syntax) (expectedType? : Option Expr) (mayPostpone := false) : TacticM Expr :=
-  withRef stx <| Term.withoutErrToSorry do
+def elabTerm (stx : Syntax) (expectedType? : Option Expr) (mayPostpone := false) : TacticM Expr := do
+  /- We have disabled `Term.withoutErrToSorry` to improve error recovery.
+     When we were using it, any tactic using `elabTerm` would be interrupted at elaboration errors.
+     Tactics that do not want to proceed should check whether the result contains sythetic sorrys or
+     disable `errToSorry` before invoking `elabTerm` -/
+  withRef stx do -- <| Term.withoutErrToSorry do
     let e ← Term.elabTerm stx expectedType?
     Term.synthesizeSyntheticMVars mayPostpone
     instantiateMVars e

tests/lean/301.lean.expected.out

@@ -1,2 +1,12 @@
 301.lean:1:9-1:17: error: missing cases:
 (Nat.succ _)
+301.lean:1:21-1:24: error: type mismatch
+  
+    (
+      fun (x : Nat) =>
+        match x with 
+        | 0 => 0)
+has type
+  Nat → Nat : Type
+but is expected to have type
+  Nat : Type

tests/lean/exactErrorPos.lean

@@ -17,3 +17,7 @@ theorem ex4 (f : Nat → Nat) (x : Nat) (h1 : (x : Nat) → x > 0 → f x = x) (
 theorem ex5 (f g : Nat → Nat) (x : Nat) (h1 : (x : Nat) → x > 0 → f x = x) (h2 : x > 0) (h3 : g x = x) : f x = x := by
   first | apply h3 | apply h1
   assumption
+
+theorem ex6 (f : Nat → Nat) (x : Nat) (h1 : (x : Nat) → x > 0 → f x = x) (h2 : x > 0) : f x = x := by
+  first | refine h1 _ _ | refine h1 _ _
+  assumption

tests/lean/exactErrorPos.lean.expected.out

@@ -24,3 +24,16 @@ x : Nat
 h1 : ∀ (x : Nat), x > 0 → f x = x
 h2 : x > 0
 ⊢ f x = x
+exactErrorPos.lean:22:38-22:39: error: don't know how to synthesize placeholder
+context:
+f : Nat → Nat
+x : Nat
+h1 : ∀ (x : Nat), x > 0 → f x = x
+h2 : x > 0
+⊢ x > 0
+exactErrorPos.lean:21:99-23:12: error: unsolved goals
+f : Nat → Nat
+x : Nat
+h1 : ∀ (x : Nat), x > 0 → f x = x
+h2 : x > 0
+⊢ f x = x

tests/lean/hygienicIntro.lean.expected.out

@@ -1,2 +1,3 @@
 hygienicIntro.lean:14:6-14:9: error: unknown identifier 'a_1'
 hygienicIntro.lean:24:20-24:21: error: unknown identifier 'h'
+hygienicIntro.lean:25:8-25:9: error: unknown identifier 'h'

tests/lean/interactive/match.lean

@@ -0,0 +1,18 @@
+structure S where
+  fn1 : Nat
+  value : Bool
+  name : String
+
+def f (s : S) : Nat := by
+  refine s.
+         --^ textDocument/completion
+
+def g (s : S) : Nat := by
+  match s.
+        --^ textDocument/completion
+
+theorem ex (x : Nat) : 0 + x = x := by
+  match x with
+--^ $/lean/plainGoal
+  | 0 => done
+       --^ $/lean/plainGoal

tests/lean/interactive/match.lean.expected.out

@@ -0,0 +1,22 @@
+{"textDocument": {"uri": "file://match.lean"},
+ "position": {"line": 6, "character": 11}}
+{"items":
+ [{"label": "fn1", "detail": "S → Nat"},
+  {"label": "name", "detail": "S → String"},
+  {"label": "value", "detail": "S → Bool"}],
+ "isIncomplete": true}
+{"textDocument": {"uri": "file://match.lean"},
+ "position": {"line": 10, "character": 10}}
+{"items":
+ [{"label": "fn1", "detail": "S → Nat"},
+  {"label": "name", "detail": "S → String"},
+  {"label": "value", "detail": "S → Bool"}],
+ "isIncomplete": true}
+{"textDocument": {"uri": "file://match.lean"},
+ "position": {"line": 14, "character": 2}}
+{"rendered": "```lean\nx : Nat\n⊢ 0 + x = x\n```",
+ "goals": ["x : Nat\n⊢ 0 + x = x"]}
+{"textDocument": {"uri": "file://match.lean"},
+ "position": {"line": 16, "character": 9}}
+{"rendered": "```lean\nx : Nat\n⊢ 0 + 0 = 0\n```",
+ "goals": ["x : Nat\n⊢ 0 + 0 = 0"]}

tests/lean/matchUnknownFVarBug.lean.expected.out

@@ -1,3 +1,9 @@
 matchUnknownFVarBug.lean:2:2-2:7: error: missing cases:
 (some (Nat.succ _)), Eq.refl, (some _), Eq.refl
 none, Eq.refl, none, Eq.refl
+matchUnknownFVarBug.lean:3:18-3:19: error: unsolved goals
+n? : Option Nat
+h : n? = some 0
+x✝ : Option Nat
+h' : some 0 = x✝
+⊢ False