From dae01324398c4ebf86b4d1ed15b3a470d92a8d28 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 3 Feb 2021 15:03:34 -0800
Subject: [PATCH] fix: save/restore state at `elabTypeWithAutoBoundImplicit`

---
 src/Lean/Elab/Term.lean          | 3 +++
 tests/lean/302.lean.expected.out | 8 --------
 2 files changed, 3 insertions(+), 8 deletions(-)

diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index e6855118b7..b0d2ce08a3 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -1113,11 +1113,14 @@ def elabType (stx : Syntax) : TermElabM Expr := do
 partial def elabTypeWithAutoBoundImplicit {α} (stx : Syntax) (k : Expr → TermElabM α) : TermElabM α  := do
   if (← read).autoBoundImplicit then
     let rec loop : TermElabM α := do
+      let s ← saveAllState
       try
         k (← elabType stx)
       catch
         | ex => match isAutoBoundImplicitLocalException? ex with
           | some n =>
+            -- Restore state, declare `n`, and try again
+            s.restore
             withLocalDecl n BinderInfo.implicit (← mkFreshTypeMVar) fun x =>
               withReader (fun ctx => { ctx with autoBoundImplicits := ctx.autoBoundImplicits.push x } )
                 loop
diff --git a/tests/lean/302.lean.expected.out b/tests/lean/302.lean.expected.out
index b078015fbc..043c66ee68 100644
--- a/tests/lean/302.lean.expected.out
+++ b/tests/lean/302.lean.expected.out
@@ -2,11 +2,3 @@
   m
 term has type
   ?m
-302.lean:1:8-1:11: error: function expected at
-  m
-term has type
-  ?m
-302.lean:1:8-1:11: error: function expected at
-  m
-term has type
-  ?m