fix: teach Exception.isRuntime to detect nested errors

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.