From ca1315e3baf2d60fc78a03bb347b14d8848da2e2 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 18 Sep 2025 14:33:57 +0200
Subject: [PATCH] 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                 |  4 +++-
 tests/lean/run/kernelBacktrack.lean | 21 +++++++++++++++++++++
 2 files changed, 24 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/kernelBacktrack.lean

diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean
index f5d603fcde..d8394f4731 100644
--- a/src/Lean/CoreM.lean
+++ b/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
diff --git a/tests/lean/run/kernelBacktrack.lean b/tests/lean/run/kernelBacktrack.lean
new file mode 100644
index 0000000000..a30745ca26
--- /dev/null
+++ b/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