fix: teach Exception.isRuntime to detect nested errors (#11490)

This PR prevents `try` swallowing heartbeat errors from nested `simp`
calls, and more generally ensures the `isRuntime` flag is propagated by
`throwNestedTacticEx`. This prevents the behavior of proofs (especially
those using `aesop`) being affected by the current recursion depth or
heartbeat limit.

This breaks a single caller in Mathlib where `simp` uses a lemma of the
form `x = f (g x)` and stack overflows, which can be fixed by
generalizing over `g x`.

Closes #7811.

---------

Co-authored-by: Sebastian Ullrich <[email protected]>

Author: eric-wieser

src/Lean/CoreM.lean

@@ -647,7 +647,10 @@ export Core (CoreM mkFreshUserName checkSystem withCurrHeartbeats)
   This function is a bit hackish. The heartbeat exception should probably be an internal exception.
   We used a similar hack at `Exception.isMaxRecDepth` -/
 def Exception.isMaxHeartbeat (ex : Exception) : Bool :=
-  ex matches Exception.error _ (.tagged `runtime.maxHeartbeats _)
+  if let Exception.error _ msg := ex then
+    msg.stripNestedTags.kind == `runtime.maxHeartbeats
+  else
+    false
 
 /-- Creates the expression `d → b` -/
 def mkArrow (d b : Expr) : CoreM Expr :=

src/Lean/Exception.lean

@@ -232,7 +232,10 @@ but it is also produced by `MacroM` which implemented in the prelude, and intern
 been defined yet.
 -/
 def Exception.isMaxRecDepth (ex : Exception) : Bool :=
-  ex matches error _ (.tagged `runtime.maxRecDepth _)
+  if let Exception.error _ msg := ex then
+    msg.stripNestedTags.kind == `runtime.maxRecDepth
+  else
+    false
 
 /--
 Increment the current recursion depth and then execute `x`.

src/Lean/Log.lean

@@ -86,8 +86,7 @@ If `msg` is tagged as a named error, appends the error description widget displa
 corresponding error name and explanation link. Otherwise, returns `msg` unaltered.
 -/
 private def MessageData.appendDescriptionWidgetIfNamed (msg : MessageData) : MessageData :=
-  let kind := stripNestedTags msg.kind
-  match errorNameOfKind? kind with
+  match msg.stripNestedTags.errorName? with
   | some errorName =>
     let url := manualRoot ++ s!"find/?domain={errorExplanationManualDomain}&name={errorName}"
     let inst := {
@@ -102,13 +101,6 @@ private def MessageData.appendDescriptionWidgetIfNamed (msg : MessageData) : Mes
     -- console output
     msg.composePreservingKind <| .ofWidget inst .nil
   | none => msg
-where
-  /-- Remove any `` `nested `` name components prepended by `throwNestedTacticEx`. -/
-  stripNestedTags : Name → Name
-  | .str p "nested" => stripNestedTags p
-  | .str p s => .str (stripNestedTags p) s
-  | .num p n => .num (stripNestedTags p) n
-  | .anonymous => .anonymous
 
 /--
 Log the message `msgData` at the position provided by `ref` with the given `severity`.

src/Lean/Message.lean

@@ -457,6 +457,23 @@ and `throwNamedError`.
 def MessageData.tagWithErrorName (msg : MessageData) (name : Name) : MessageData :=
   .tagged (kindOfErrorName name) msg
 
+/-- Strip the `` `nested`` prefix components added to tags by `throwNestedTacticEx`. -/
+def MessageData.stripNestedTags : MessageData → MessageData
+  | .withContext ctx msg => .withContext ctx msg.stripNestedTags
+  | .withNamingContext ctx msg => .withNamingContext ctx msg.stripNestedTags
+  | .tagged n msg => .tagged (stripNestedNamePrefix n) msg
+  | msg => msg
+where
+  stripNestedNamePrefix : Name → Name
+  | .anonymous => .anonymous
+  | .str p s =>
+    let p' := stripNestedNamePrefix p
+    if p'.isAnonymous && s == "nested" then
+      .anonymous
+    else
+      .str p' s
+  | .num p n => .num (stripNestedNamePrefix p) n
+
 /--
 If the provided name is labeled as a diagnostic name, removes the label and returns the
 corresponding diagnostic name.

tests/lean/run/7811.lean

@@ -0,0 +1,38 @@
+import Lean
+
+
+-- This should not be swallowed by the `try`
+/--
+warning: Possibly looping simp theorem: `← Nat.add_zero 1`
+
+Hint: You can disable a simp theorem from the default simp set by passing `- theoremName` to `simp`.
+---
+error: Tactic `simp` failed with a nested error:
+maximum recursion depth has been reached
+use `set_option maxRecDepth <num>` to increase limit
+use `set_option diagnostics true` to get diagnostic information
+-/
+#guard_msgs in
+set_option maxRecDepth 200 in-- low to make this fast
+example : 1 = sorry := by
+  try simp [← Nat.add_zero 1]
+
+open Lean
+
+/--
+error: Tactic `foo` failed with a nested error:
+maximum recursion depth has been reached
+use `set_option maxRecDepth <num>` to increase limit
+use `set_option diagnostics true` to get diagnostic information
+-/
+#guard_msgs in
+run_meta show MetaM Unit from do
+  try
+    -- Throw a recursion depth error wrapped in a nested error
+    tryCatchRuntimeEx
+      (throwMaxRecDepthAt .missing)
+      (fun e =>
+        Meta.throwNestedTacticEx `foo e)
+  catch e =>
+    -- We didn't use `tryCatchRuntimeEx` here so we shouldn't catch it.
+    throwError m!"Should not be caught"