fix: save/restore state at elabTypeWithAutoBoundImplicit

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

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