From 54a3fbf88fd077c2aafcdc68e151c0973c9a3f19 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 15 Oct 2025 09:11:27 +0200 Subject: [PATCH] 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. --- src/Lean/Elab/Tactic/ElabTerm.lean | 119 +++++++++++++++-------------- tests/lean/run/issue10766.lean | 39 ++++++++++ 2 files changed, 101 insertions(+), 57 deletions(-) create mode 100644 tests/lean/run/issue10766.lean diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean index b1613725e6..1041fd7b03 100644 --- 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 diff --git a/tests/lean/run/issue10766.lean b/tests/lean/run/issue10766.lean new file mode 100644 index 0000000000..e274dba83c --- /dev/null +++ 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