From 475f5fecaa626ffda796b8dda5f226471d4ac0c1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 6 May 2021 20:36:42 -0700
Subject: [PATCH] feat: improve error recovery at `Tactic.elabTerm`

---
 src/Lean/Elab/Match.lean                      |  2 +-
 src/Lean/Elab/Tactic/ElabTerm.lean            |  8 +++++--
 tests/lean/301.lean.expected.out              | 10 +++++++++
 tests/lean/exactErrorPos.lean                 |  4 ++++
 tests/lean/exactErrorPos.lean.expected.out    | 13 +++++++++++
 tests/lean/hygienicIntro.lean.expected.out    |  1 +
 tests/lean/interactive/match.lean             | 18 +++++++++++++++
 .../lean/interactive/match.lean.expected.out  | 22 +++++++++++++++++++
 .../matchUnknownFVarBug.lean.expected.out     |  6 +++++
 9 files changed, 81 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/interactive/match.lean
 create mode 100644 tests/lean/interactive/match.lean.expected.out

diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean
index c14b7936f0..1f93e5a1c5 100644
--- a/src/Lean/Elab/Match.lean
+++ b/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
diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean
index 4739aa2d8c..7f6a3cb2b8 100644
--- a/src/Lean/Elab/Tactic/ElabTerm.lean
+++ b/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
diff --git a/tests/lean/301.lean.expected.out b/tests/lean/301.lean.expected.out
index fda53a71e7..7c936244a8 100644
--- a/tests/lean/301.lean.expected.out
+++ b/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
diff --git a/tests/lean/exactErrorPos.lean b/tests/lean/exactErrorPos.lean
index 0a6da62fb9..acbc74db05 100644
--- a/tests/lean/exactErrorPos.lean
+++ b/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
diff --git a/tests/lean/exactErrorPos.lean.expected.out b/tests/lean/exactErrorPos.lean.expected.out
index 29be7d9834..0f8b632f9e 100644
--- a/tests/lean/exactErrorPos.lean.expected.out
+++ b/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
diff --git a/tests/lean/hygienicIntro.lean.expected.out b/tests/lean/hygienicIntro.lean.expected.out
index 2fea245a39..be671c9fc0 100644
--- a/tests/lean/hygienicIntro.lean.expected.out
+++ b/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'
diff --git a/tests/lean/interactive/match.lean b/tests/lean/interactive/match.lean
new file mode 100644
index 0000000000..25ea123537
--- /dev/null
+++ b/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
diff --git a/tests/lean/interactive/match.lean.expected.out b/tests/lean/interactive/match.lean.expected.out
new file mode 100644
index 0000000000..7fe9ab1f4d
--- /dev/null
+++ b/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"]}
diff --git a/tests/lean/matchUnknownFVarBug.lean.expected.out b/tests/lean/matchUnknownFVarBug.lean.expected.out
index 9300b9f5fd..3c34e589a7 100644
--- a/tests/lean/matchUnknownFVarBug.lean.expected.out
+++ b/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