fix: backtracking kernel errors under Elab.async (#10438)

This PR fixes an issue where notations and other overloadings would
signal kernel errors even though there exists a successful
interpretation.

src/Lean/CoreM.lean

@@ -408,7 +408,9 @@ itself after calling `act` as well as by reuse-handling code such as the one sup
 
 /-- Restore backtrackable parts of the state. -/
 def SavedState.restore (b : SavedState) : CoreM Unit :=
-  modify fun s => { s with env := b.env, messages := b.messages, infoState := b.infoState }
+  modify fun s => { s with
+      env := b.env, messages := b.messages, infoState := b.infoState
+      snapshotTasks := b.snapshotTasks }
 
 private def mkFreshNameImp (n : Name) : CoreM Name := do
   withFreshMacroScope do

tests/lean/run/kernelBacktrack.lean

@@ -0,0 +1,21 @@
+/-! Kernel errors (via `Lean.Core.State.snapshotTasks`) should be backtracked. -/
+
+structure Wrapper (α) where val : α
+
+instance {α : Type} [NatCast α] : NatCast (Wrapper α) := sorry
+
+def foo {α : Type} (μ : Wrapper α) (f : α → Nat) : Nat := sorry
+
+macro:max P:term noWs "[" term "]" : term => `(foo $P fun x => 0)
+
+/-! This used to give a kernel error even though there is a succeeding interpretation. -/
+
+/-- warning: declaration uses 'sorry' -/
+#guard_msgs in
+theorem kernel_error
+    (L : List Nat) (hL : L.length = 2 ∧ ∀ i : Fin L.length, L[i] = 0) (i : Nat) :
+    L[i % 2] = 0 := sorry
+
+/-- info: 'kernel_error' depends on axioms: [propext, sorryAx, Quot.sound] -/
+#guard_msgs in
+#print axioms kernel_error