fix: improve error message when decide +kernel fails (#10780)

This PR improves the error message when `decide +kernel` fails in the kernel, but not the elaborator. Fixes #10766.
2025-10-15 09:11:27 +02:00 · 2025-10-15 09:11:27 +02:00 · 54a3fbf88f
commit 54a3fbf88f
parent 746206c5e6
2 changed files with 101 additions and 57 deletions
--- a/src/Lean/Elab/Tactic/ElabTerm.lean
+++ b/src/Lean/Elab/Tactic/ElabTerm.lean
@ -482,7 +482,10 @@ where
      -- efficient term. The kernel handles the unification `e =?= true` specially.
      return pf
    else
-      diagnose expectedType s r
+      -- Diagnose the failure, lazily so that there is no performance impact if `decide` isn't being used interactively.
+      throwError MessageData.ofLazyM (es := #[expectedType]) do
+        diagnose expectedType s r
+
  doKernel (expectedType : Expr) : TacticM Expr := do
    let pf ← mkDecideProof expectedType
    -- Get instance from `pf`
@ -498,64 +501,66 @@ where
      let lemmaName ← withOptions (Elab.async.set · false) do
        mkAuxLemma lemmaLevels expectedType pf
      return mkConst lemmaName (lemmaLevels.map .param)
-    catch _ =>
-      diagnose expectedType s none
-  diagnose {α : Type} (expectedType s : Expr) (r? : Option Expr) : TacticM α :=
-    -- Diagnose the failure, lazily so that there is no performance impact if `decide` isn't being used interactively.
-    throwError MessageData.ofLazyM (es := #[expectedType]) do
-      let r ← r?.getDM (withAtLeastTransparency .default <| whnf s)
-      if r.isAppOf ``isTrue then
-        return m!"\
-          Tactic `{tacticName}` failed. Internal error: The elaborator is able to reduce the \
-          `{.ofConstName ``Decidable}` instance, but the kernel is not able to"
-      else if r.isAppOf ``isFalse then
-        return m!"\
-          Tactic `{tacticName}` proved that the proposition\
-          {indentExpr expectedType}\n\
-          is false"
-      -- Re-reduce the instance and collect diagnostics, to get all unfolded Decidable instances
-      let (reason, unfoldedInsts) ← withoutModifyingState <| withOptions (fun opt => diagnostics.set opt true) do
-        modifyDiag (fun _ => {})
-        let reason ← withAtLeastTransparency .default <| blameDecideReductionFailure s
-        let unfolded := (← get).diag.unfoldCounter.foldl (init := #[]) fun cs n _ => cs.push n
-        let unfoldedInsts ← unfolded |>.qsort Name.lt |>.filterMapM fun n => do
-          let e ← mkConstWithLevelParams n
-          if (← Meta.isClass? (← inferType e)) == ``Decidable then
-            return m!"`{.ofConst e}`"
-          else
-            return none
-        return (reason, unfoldedInsts)
-      let stuckMsg :=
-        if unfoldedInsts.isEmpty then
-          m!"Reduction got stuck at the `{.ofConstName ``Decidable}` instance{indentExpr reason}"
-        else
-          let instances := if unfoldedInsts.size == 1 then "instance" else "instances"
-          m!"After unfolding the {instances} {.andList unfoldedInsts.toList}, \
-          reduction got stuck at the `{.ofConstName ``Decidable}` instance{indentExpr reason}"
-      let hint :=
-        if reason.isAppOf ``Eq.rec then
-          .hint' m!"Reduction got stuck on `▸` ({.ofConstName ``Eq.rec}), \
-            which suggests that one of the `{.ofConstName ``Decidable}` instances is defined using tactics such as `rw` or `simp`. \
-            To avoid tactics, make use of functions such as \
-            `{.ofConstName ``inferInstanceAs}` or `{.ofConstName ``decidable_of_decidable_of_iff}` \
-            to alter a proposition."
-        else if reason.isAppOf ``Classical.choice then
-          .hint' m!"Reduction got stuck on `{.ofConstName ``Classical.choice}`, \
-            which indicates that a `{.ofConstName ``Decidable}` instance \
-            is defined using classical reasoning, proving an instance exists rather than giving a concrete construction. \
-            The `{tacticName}` tactic works by evaluating a decision procedure via reduction, \
-            and it cannot make progress with such instances. \
-            This can occur due to the `open scoped Classical` command, which enables the instance \
-            `{.ofConstName ``Classical.propDecidable}`."
-        else
-          MessageData.nil
+    catch ex =>
+      -- Diagnose the failure, lazily so that there is no performance impact if `decide` isn't being used interactively.
+      throwError MessageData.ofLazyM (es := #[expectedType]) do
+        let r ← withAtLeastTransparency .default <| whnf s
+        if r.isAppOf ``isTrue then
+          return m!"\
+            Tactic `{tacticName}` failed. The elaborator is able to reduce the \
+            `{.ofConstName ``Decidable}` instance, but the kernel fails with:\n\
+            {indentD ex.toMessageData}"
+        diagnose expectedType s r
+
+  diagnose (expectedType s : Expr) (r : Expr) : MetaM MessageData := do
+    if r.isAppOf ``isFalse then
      return m!"\
-        Tactic `{tacticName}` failed for proposition\
+        Tactic `{tacticName}` proved that the proposition\
        {indentExpr expectedType}\n\
-        because its `{.ofConstName ``Decidable}` instance\
-        {indentExpr s}\n\
-        did not reduce to `{.ofConstName ``isTrue}` or `{.ofConstName ``isFalse}`.\n\n\
-        {stuckMsg}{hint}"
+        is false"
+    -- Re-reduce the instance and collect diagnostics, to get all unfolded Decidable instances
+    let (reason, unfoldedInsts) ← withoutModifyingState <| withOptions (fun opt => diagnostics.set opt true) do
+      modifyDiag (fun _ => {})
+      let reason ← withAtLeastTransparency .default <| blameDecideReductionFailure s
+      let unfolded := (← get).diag.unfoldCounter.foldl (init := #[]) fun cs n _ => cs.push n
+      let unfoldedInsts ← unfolded |>.qsort Name.lt |>.filterMapM fun n => do
+        let e ← mkConstWithLevelParams n
+        if (← Meta.isClass? (← inferType e)) == ``Decidable then
+          return m!"`{.ofConst e}`"
+        else
+          return none
+      return (reason, unfoldedInsts)
+    let stuckMsg :=
+      if unfoldedInsts.isEmpty then
+        m!"Reduction got stuck at the `{.ofConstName ``Decidable}` instance{indentExpr reason}"
+      else
+        let instances := if unfoldedInsts.size == 1 then "instance" else "instances"
+        m!"After unfolding the {instances} {.andList unfoldedInsts.toList}, \
+        reduction got stuck at the `{.ofConstName ``Decidable}` instance{indentExpr reason}"
+    let hint :=
+      if reason.isAppOf ``Eq.rec then
+        .hint' m!"Reduction got stuck on `▸` ({.ofConstName ``Eq.rec}), \
+          which suggests that one of the `{.ofConstName ``Decidable}` instances is defined using tactics such as `rw` or `simp`. \
+          To avoid tactics, make use of functions such as \
+          `{.ofConstName ``inferInstanceAs}` or `{.ofConstName ``decidable_of_decidable_of_iff}` \
+          to alter a proposition."
+      else if reason.isAppOf ``Classical.choice then
+        .hint' m!"Reduction got stuck on `{.ofConstName ``Classical.choice}`, \
+          which indicates that a `{.ofConstName ``Decidable}` instance \
+          is defined using classical reasoning, proving an instance exists rather than giving a concrete construction. \
+          The `{tacticName}` tactic works by evaluating a decision procedure via reduction, \
+          and it cannot make progress with such instances. \
+          This can occur due to the `open scoped Classical` command, which enables the instance \
+          `{.ofConstName ``Classical.propDecidable}`."
+      else
+        MessageData.nil
+    return m!"\
+      Tactic `{tacticName}` failed for proposition\
+      {indentExpr expectedType}\n\
+      because its `{.ofConstName ``Decidable}` instance\
+      {indentExpr s}\n\
+      did not reduce to `{.ofConstName ``isTrue}` or `{.ofConstName ``isFalse}`.\n\n\
+      {stuckMsg}{hint}"

 declare_config_elab elabDecideConfig Parser.Tactic.DecideConfig

--- a/tests/lean/run/issue10766.lean
+++ b/tests/lean/run/issue10766.lean
@ -0,0 +1,39 @@
+noncomputable def powMod (a b n : Nat) : Nat :=
+  aux (b + 1) (a.mod n) b 1
+where
+  aux : Nat → ((a b c : Nat) → Nat) :=
+    Nat.rec (fun _ _ _ => 0)
+      (fun _ r a b c =>
+        (b.beq 0).rec
+          (((b.mod 2).beq 0).rec
+            (r ((a.mul a).mod n) (b.div 2) ((a.mul c).mod n))
+            (r ((a.mul a).mod n) (b.div 2) c))
+          (c.mod n))
+
+def x : Nat := 127780414391497973212171930170926986757577048484820926201064729783485263494817422495127775983679039078116803697168137524940219819335799478153348592755198599590903607242050230924443865709697486743641039970666450337071378658828331722728467720393963808366917988956767802913905167890490075236068196363700359481304279948916896583006686025357237170212018946813663108217900835975808683160984117514866915965161953626338070145596982334808959718966160701183250747572515090867613655044807172211728519357721287835503689517292364425608325467094686443862517374850243698013720305871319056887431952190952721719757200172695537054790570648290887720009455171821568413052107356003828041937567129362866696549587422369864562815134637684140271767482353107080370450890024342225936273158281477009232714640818424893445193089479459814572594522258577931514012256573162006292678354475638319009668319255772179069845291474717503333030909793536116894869761453687330048252587304656806182949368202671739705463406846852567720022377005763291104588535681445561286808586673846016527511475331939430139687698419185010117348285933672139833826832898565919546377321517928825162277951756632134321102813522053716838646284289
+
+set_option maxRecDepth 20000
+
+/--
+error: Tactic `decide` failed. The elaborator is able to reduce the `Decidable` instance, but the kernel fails with:
+
+  (kernel) deep recursion detected
+-/
+#guard_msgs in
+example : powMod 2 (x - 1) x = 1 := by decide +kernel
+
+/-- error: (kernel) deep recursion detected -/
+#guard_msgs in
+example : powMod 2 (x - 1) x = 1 := by decide
+
+/-- error: (kernel) deep recursion detected -/
+#guard_msgs in
+example : powMod 2 (x - 1) x = 1 := by rfl
+
+set_option debug.skipKernelTC true
+
+#guard_msgs in
+example : powMod 2 (x - 1) x = 1 := by decide
+
+#guard_msgs in
+example : powMod 2 (x - 1) x = 1 := by rfl