From d1f0db7072897fdfa416c0c222571cc85ec2483e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 12 Jul 2022 16:36:01 -0700
Subject: [PATCH] fix: `resumePostponed` backtracking
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Note that test for issue #1200 broke.
The bug fixed by this commit was allowing the example to be elaborated
correctly :(
Initially, the type of the discriminant is not available, and
`.none (α:=α)` can only be elaborated when the expected type is of the
form `C ...`. Lean then tries to elaborate the alternatives, learn
that the discriminant should be `Option ?m`, and fails because the
patterns still have metavariables after elaboration. Before the bug
fix, `resumePostpone` was **not** restoring the metavariable context,
and the assingnment would stay there. With this information, Lean
can now elaborate `.none (α:=α)`.
Although the bug had a positive impact in this case, it produced
incorrect behavior in other examples.
The fixed example looks reasonable. Thus, we will not reopen
issue #1200
---
 src/Lean/Elab/SyntheticMVars.lean | 6 +++---
 tests/lean/run/1200.lean          | 2 +-
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean
index 2aed1dfb6a..5ef71672f2 100644
--- a/src/Lean/Elab/SyntheticMVars.lean
+++ b/src/Lean/Elab/SyntheticMVars.lean
@@ -23,7 +23,7 @@ private def resumeElabTerm (stx : Syntax) (expectedType? : Option Expr) (errToSo
   It is used to implement `synthesizeSyntheticMVars`. -/
 private def resumePostponed (savedContext : SavedContext) (stx : Syntax) (mvarId : MVarId) (postponeOnError : Bool) : TermElabM Bool :=
   withRef stx <| withMVarContext mvarId do
-    let s ← get
+    let s ← saveState
     try
       withSavedContext savedContext do
         let mvarDecl     ← getMVarDecl mvarId
@@ -42,13 +42,13 @@ private def resumePostponed (savedContext : SavedContext) (stx : Syntax) (mvarId
     catch
      | ex@(.internal id _) =>
        if id == postponeExceptionId then
-         set s
+         s.restore (restoreInfo := true)
          return false
        else
          throw ex
      | ex@(.error ..) =>
        if postponeOnError then
-         set s
+         s.restore (restoreInfo := true)
          return false
        else
          logException ex
diff --git a/tests/lean/run/1200.lean b/tests/lean/run/1200.lean
index ab113ce2bd..e04343c048 100644
--- a/tests/lean/run/1200.lean
+++ b/tests/lean/run/1200.lean
@@ -1,5 +1,5 @@
 example
-(h: match .none (α:=α) with
+(h: match none (α:=α) with
 | some _ => True
 | _      => True):
   True := by