From 292bab5a11dc05e019068a579a42eac251bf587f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 13 Apr 2021 08:12:39 -0700
Subject: [PATCH] fix: loop due to error recovery

---
 src/Lean/Elab/Match.lean                      | 19 +++++++++++++++++--
 src/Lean/Elab/StructInst.lean                 | 11 +++++++----
 tests/lean/loopErrorRecovery.lean             |  1 +
 .../lean/loopErrorRecovery.lean.expected.out  |  1 +
 4 files changed, 26 insertions(+), 6 deletions(-)
 create mode 100644 tests/lean/loopErrorRecovery.lean
 create mode 100644 tests/lean/loopErrorRecovery.lean.expected.out

diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean
index cc6dada59a..39affaa00a 100644
--- a/src/Lean/Elab/Match.lean
+++ b/src/Lean/Elab/Match.lean
@@ -66,12 +66,27 @@ def isAuxDiscrName (n : Name) : Bool :=
 
 /- We treat `@x` as atomic to avoid unnecessary extra local declarations from being
    inserted into the local context. Recall that `expandMatchAltsIntoMatch` uses `@` modifier.
-   Thus this is kind of discriminant is quite common. -/
+   Thus this is kind of discriminant is quite common.
+
+   Remark: if the discriminat is `Systax.missing`, we abort the elaboration of the `match`-expression.
+   This can happen due to error recovery. Example
+   ```
+   example : (p ∨ p) → p := fun h => match
+   ```
+   If we don't abort, the elaborator loops because we will keep trying to expand
+   ```
+   match
+   ```
+   into
+   ```
+   let d := <Syntax.missing>; match
+   ```
+   Recall that `Syntax.setArg stx i arg` is a no-op when `i` is out-of-bounds. -/
 def isAtomicDiscr? (discr : Syntax) : TermElabM (Option Expr) := do
   match discr with
   | `($x:ident)  => isLocalIdent? x
   | `(@$x:ident) => isLocalIdent? x
-  | _ => return none
+  | _ => if discr.isMissing then throwAbortTerm else return none
 
 -- See expandNonAtomicDiscrs?
 private def elabAtomicDiscr (discr : Syntax) : TermElabM Expr := do
diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean
index 8d0c6c16ed..77c3c11068 100644
--- a/src/Lean/Elab/StructInst.lean
+++ b/src/Lean/Elab/StructInst.lean
@@ -47,10 +47,13 @@ private def expandNonAtomicExplicitSource (stx : Syntax) : TermElabM (Option Syn
       match (← isLocalIdent? source) with
       | some _ => pure none
       | none   =>
-        let src ← `(src)
-        let sourceOpt := sourceOpt.setArg 0 src
-        let stxNew    := stx.setArg 1 sourceOpt
-        `(let src := $source; $stxNew)
+        if source.isMissing then
+          throwAbortTerm
+        else
+          let src ← `(src)
+          let sourceOpt := sourceOpt.setArg 0 src
+          let stxNew    := stx.setArg 1 sourceOpt
+          `(let src := $source; $stxNew)
 
 inductive Source where
   | none     -- structure instance source has not been provieded
diff --git a/tests/lean/loopErrorRecovery.lean b/tests/lean/loopErrorRecovery.lean
new file mode 100644
index 0000000000..577ee72a2e
--- /dev/null
+++ b/tests/lean/loopErrorRecovery.lean
@@ -0,0 +1 @@
+example : (p ∨ p) → p := fun h => match
diff --git a/tests/lean/loopErrorRecovery.lean.expected.out b/tests/lean/loopErrorRecovery.lean.expected.out
new file mode 100644
index 0000000000..123f7858d7
--- /dev/null
+++ b/tests/lean/loopErrorRecovery.lean.expected.out
@@ -0,0 +1 @@
+loopErrorRecovery.lean:2:0: error: unexpected end of input