feat: detailed feedback on decide tactic failure (#4674)

When the `decide` tactic fails, it can try to give hints about the
failure:
- It tells you which `Decidable` instances it unfolded, by making use of
the diagnostics feature.
- If it encounters `Eq.rec`, it gives you a hint that one of these
instances was likely defined using tactics.
- If it encounters `Classical.choice`, it hints that you might have
classical instances in scope.
- During this, it tries to process `Decidable.rec`s and matchers to pin
blame on a particular instance that failed to reduce.

This idea comes from discussion with Heather Macbeth [on
Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Decidable.20with.20structures/near/449409870).

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -359,8 +359,8 @@ def elabAsFVar (stx : Syntax) (userName? : Option Name := none) : TacticM FVarId
   | _ => throwUnsupportedSyntax
 
 /--
-   Make sure `expectedType` does not contain free and metavariables.
-   It applies zeta and zetaDelta-reduction to eliminate let-free-vars.
+Make sure `expectedType` does not contain free and metavariables.
+It applies zeta and zetaDelta-reduction to eliminate let-free-vars.
 -/
 private def preprocessPropToDecide (expectedType : Expr) : TermElabM Expr := do
   let mut expectedType ← instantiateMVars expectedType
@@ -370,6 +370,28 @@ private def preprocessPropToDecide (expectedType : Expr) : TermElabM Expr := do
     throwError "expected type must not contain free or meta variables{indentExpr expectedType}"
   return expectedType
 
+/--
+Given the decidable instance `inst`, reduces it and returns a decidable instance expression
+in whnf that can be regarded as the reason for the failure of `inst` to fully reduce.
+-/
+private partial def blameDecideReductionFailure (inst : Expr) : MetaM Expr := do
+  let inst ← whnf inst
+  -- If it's the Decidable recursor, then blame the major premise.
+  if inst.isAppOfArity ``Decidable.rec 5 then
+    return ← blameDecideReductionFailure inst.appArg!
+  -- If it is a matcher, look for a discriminant that's a Decidable instance to blame.
+  if let .const c _ := inst.getAppFn then
+    if let some info ← getMatcherInfo? c then
+      if inst.getAppNumArgs == info.arity then
+        let args := inst.getAppArgs
+        for i in [0:info.numDiscrs] do
+          let inst' := args[info.numParams + 1 + i]!
+          if (← Meta.isClass? (← inferType inst')) == ``Decidable then
+            let inst'' ← whnf inst'
+            if !(inst''.isAppOf ``isTrue || inst''.isAppOf ``isFalse) then
+              return ← blameDecideReductionFailure inst''
+  return inst
+
 @[builtin_tactic Lean.Parser.Tactic.decide] def evalDecide : Tactic := fun _ =>
   closeMainGoalUsing fun expectedType => do
     let expectedType ← preprocessPropToDecide expectedType
@@ -377,24 +399,66 @@ private def preprocessPropToDecide (expectedType : Expr) : TermElabM Expr := do
     let d ← instantiateMVars d
     -- Get instance from `d`
     let s := d.appArg!
-    -- Reduce the instance rather than `d` itself, since that gives a nicer error message on failure.
+    -- Reduce the instance rather than `d` itself for diagnostics purposes.
     let r ← withAtLeastTransparency .default <| whnf s
-    if r.isAppOf ``isFalse then
-      throwError "\
-        tactic 'decide' proved that the proposition\
-        {indentExpr expectedType}\n\
-        is false"
-    unless r.isAppOf ``isTrue do
-      throwError "\
-        tactic 'decide' failed for proposition\
-        {indentExpr expectedType}\n\
-        since its 'Decidable' instance reduced to\
-        {indentExpr r}\n\
-        rather than to the 'isTrue' constructor."
-    -- While we have a proof from reduction, we do not embed it in the proof term,
-    -- but rather we let the kernel recompute it during type checking from a more efficient term.
-    let rflPrf ← mkEqRefl (toExpr true)
-    return mkApp3 (Lean.mkConst ``of_decide_eq_true) expectedType s rflPrf
+    if r.isAppOf ``isTrue then
+      -- Success!
+      -- While we have a proof from reduction, we do not embed it in the proof term,
+      -- and instead we let the kernel recompute it during type checking from the following more efficient term.
+      let rflPrf ← mkEqRefl (toExpr true)
+      return mkApp3 (Lean.mkConst ``of_decide_eq_true) expectedType s rflPrf
+    else
+      -- Diagnose the failure, lazily so that there is no performance impact if `decide` isn't being used interactively.
+      throwError MessageData.ofLazyM (es := #[expectedType]) do
+        if r.isAppOf ``isFalse then
+          return m!"\
+          tactic 'decide' 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!"'{MessageData.ofConst e}'"
+            else
+              return none
+          return (reason, unfoldedInsts)
+        let stuckMsg :=
+          if unfoldedInsts.isEmpty then
+            m!"Reduction got stuck at the '{MessageData.ofConstName ``Decidable}' instance{indentExpr reason}"
+          else
+            let instances := if unfoldedInsts.size == 1 then "instance" else "instances"
+            m!"After unfolding the {instances} {MessageData.andList unfoldedInsts.toList}, \
+            reduction got stuck at the '{MessageData.ofConstName ``Decidable}' instance{indentExpr reason}"
+        let hint :=
+          if reason.isAppOf ``Eq.rec then
+            m!"\n\n\
+            Hint: Reduction got stuck on '▸' ({MessageData.ofConstName ``Eq.rec}), \
+            which suggests that one of the '{MessageData.ofConstName ``Decidable}' instances is defined using tactics such as 'rw' or 'simp'. \
+            To avoid tactics, make use of functions such as \
+            '{MessageData.ofConstName ``inferInstanceAs}' or '{MessageData.ofConstName ``decidable_of_decidable_of_iff}' \
+            to alter a proposition."
+          else if reason.isAppOf ``Classical.choice then
+            m!"\n\n\
+            Hint: Reduction got stuck on '{MessageData.ofConstName ``Classical.choice}', \
+            which indicates that a '{MessageData.ofConstName ``Decidable}' instance \
+            is defined using classical reasoning, proving an instance exists rather than giving a concrete construction. \
+            The 'decide' tactic works by evaluating a decision procedure via reduction, and it cannot make progress with such instances. \
+            This can occur due to the 'opened scoped Classical' command, which enables the instance \
+            '{MessageData.ofConstName ``Classical.propDecidable}'."
+          else
+            MessageData.nil
+        return m!"\
+          tactic 'decide' failed for proposition\
+          {indentExpr expectedType}\n\
+          since its '{MessageData.ofConstName ``Decidable}' instance\
+          {indentExpr s}\n\
+          did not reduce to '{MessageData.ofConstName ``isTrue}' or '{MessageData.ofConstName ``isFalse}'.\n\n\
+          {stuckMsg}{hint}"
 
 private def mkNativeAuxDecl (baseName : Name) (type value : Expr) : TermElabM Name := do
   let auxName ← Term.mkAuxName baseName

src/Lean/PrettyPrinter.lean

@@ -128,10 +128,12 @@ def ofLazyM (f : MetaM MessageData) (es : Array Expr := #[]) : MessageData :=
         instantiateMVarsCore mvarctxt a |>.1.hasSyntheticSorry
     ))
 
-/-- Pretty print a const expression using `delabConst` and generate terminfo.
+/--
+Pretty print a const expression using `delabConst` and generate terminfo.
 This function avoids inserting `@` if the constant is for a function whose first
 argument is implicit, which is what the default `toMessageData` for `Expr` does.
-Panics if `e` is not a constant. -/
+Panics if `e` is not a constant.
+-/
 def ofConst (e : Expr) : MessageData :=
   if e.isConst then
     let delab : Delab := withOptionAtCurrPos `pp.tagAppFns true delabConst
@@ -139,6 +141,19 @@ def ofConst (e : Expr) : MessageData :=
   else
     panic! "not a constant"
 
+/--
+Pretty print a constant given its name, similar to `Lean.MessageData.ofConst`.
+Uses the constant's universe level parameters when pretty printing.
+If there is no such constant in the environment, the name is simply formatted.
+-/
+def ofConstName (constName : Name) : MessageData :=
+  .ofFormatWithInfosM do
+    if let some info := (← getEnv).find? constName then
+      let delab : Delab := withOptionAtCurrPos `pp.tagAppFns true delabConst
+      PrettyPrinter.ppExprWithInfos (delab := delab) (.const constName <| info.levelParams.map mkLevelParam)
+    else
+      return format constName
+
 /-- Generates `MessageData` for a declaration `c` as `c.{<levels>} <params> : <type>`, with terminfo. -/
 def signature (c : Name) : MessageData :=
   .ofFormatWithInfosM (PrettyPrinter.ppSignature c)

tests/lean/2161.lean

@@ -1,22 +0,0 @@
-structure Foo where num : Nat deriving DecidableEq
-
-namespace Foo
-
-instance : OfNat Foo n := ⟨⟨n⟩⟩
-
-/-! # Example 1 -/
-
-@[irreducible] def mul (a b : Foo) : Foo :=
-  let d := Nat.gcd a.num 1
-  ⟨(a.num.div d) * (b.num.div d)⟩
-
--- should fail fast; exact heartbeat count at time of writing is 31
-set_option maxHeartbeats 310
-example : ((Foo.mul 4 1).mul 1).mul 1 = 4 := by decide
-
-/-! # Example 2 -/
-
-@[irreducible] def add (a b : Foo) : Foo := ⟨a.num * b.num⟩
-
--- should not succeed (and fail fast); exact heartbeat count at time of writing is 21
-example : ((Foo.add 4 1).add 1).add 1 = 4 := by decide

tests/lean/2161.lean.expected.out

@@ -1,12 +0,0 @@
-2161.lean:15:48-15:54: error: tactic 'decide' failed for proposition
-  ((mul 4 1).mul 1).mul 1 = 4
-since its 'Decidable' instance reduced to
-  Decidable.rec (fun h => (fun h => isFalse ⋯) h) (fun h => (fun h => h ▸ isTrue ⋯) h)
-    (instDecidableEqNat (((mul 4 1).mul 1).mul 1).num 4)
-rather than to the 'isTrue' constructor.
-2161.lean:22:48-22:54: error: tactic 'decide' failed for proposition
-  ((add 4 1).add 1).add 1 = 4
-since its 'Decidable' instance reduced to
-  Decidable.rec (fun h => (fun h => isFalse ⋯) h) (fun h => (fun h => h ▸ isTrue ⋯) h)
-    (instDecidableEqNat (((add 4 1).add 1).add 1).num 4)
-rather than to the 'isTrue' constructor.

tests/lean/decideTactic.lean

@@ -1,21 +0,0 @@
-/-!
-# Tests of the `decide` tactic
--/
-
-/-!
-Success
--/
-example : 2 + 2 ≠ 5 := by decide
-
-/-!
-False proposition
--/
-example : 1 ≠ 1 := by decide
-
-/-!
-Irreducible decidable instance
--/
-opaque unknownProp : Prop
-
-open scoped Classical in
-example : unknownProp := by decide

tests/lean/decideTactic.lean.expected.out

@@ -1,8 +0,0 @@
-decideTactic.lean:13:22-13:28: error: tactic 'decide' proved that the proposition
-  1 ≠ 1
-is false
-decideTactic.lean:21:28-21:34: error: tactic 'decide' failed for proposition
-  unknownProp
-since its 'Decidable' instance reduced to
-  Classical.choice ⋯
-rather than to the 'isTrue' constructor.

tests/lean/run/2161.lean

@@ -0,0 +1,50 @@
+structure Foo where num : Nat deriving DecidableEq
+
+namespace Foo
+
+instance : OfNat Foo n := ⟨⟨n⟩⟩
+
+/-! # Example 1 -/
+
+@[irreducible] def mul (a b : Foo) : Foo :=
+  let d := Nat.gcd a.num 1
+  ⟨(a.num.div d) * (b.num.div d)⟩
+
+-- should fail fast; exact heartbeat count at time of writing is 31
+set_option maxHeartbeats 310
+/--
+error: tactic 'decide' failed for proposition
+  ((mul 4 1).mul 1).mul 1 = 4
+since its 'Decidable' instance
+  instDecidableEqFoo (((mul 4 1).mul 1).mul 1) 4
+did not reduce to 'isTrue' or 'isFalse'.
+
+After unfolding the instances 'decEqFoo✝', 'instDecidableEqFoo', 'instDecidableEqNat' and
+'Nat.decEq', reduction got stuck at the 'Decidable' instance
+  match h : (((mul 4 1).mul 1).mul 1).num.beq 4 with
+  | true => isTrue ⋯
+  | false => isFalse ⋯
+-/
+#guard_msgs in
+example : ((Foo.mul 4 1).mul 1).mul 1 = 4 := by decide
+
+/-! # Example 2 -/
+
+@[irreducible] def add (a b : Foo) : Foo := ⟨a.num * b.num⟩
+
+-- should not succeed (and fail fast); exact heartbeat count at time of writing is 21
+/--
+error: tactic 'decide' failed for proposition
+  ((add 4 1).add 1).add 1 = 4
+since its 'Decidable' instance
+  instDecidableEqFoo (((add 4 1).add 1).add 1) 4
+did not reduce to 'isTrue' or 'isFalse'.
+
+After unfolding the instances 'decEqFoo✝', 'instDecidableEqFoo', 'instDecidableEqNat' and
+'Nat.decEq', reduction got stuck at the 'Decidable' instance
+  match h : (((add 4 1).add 1).add 1).num.beq 4 with
+  | true => isTrue ⋯
+  | false => isFalse ⋯
+-/
+#guard_msgs in
+example : ((Foo.add 4 1).add 1).add 1 = 4 := by decide

tests/lean/run/4644.lean

@@ -17,13 +17,16 @@ example: check_sorted #[0, 3, 3, 5, 8, 10, 10, 10] := by
 /--
 error: tactic 'decide' failed for proposition
   check_sorted #[0, 3, 3, 5, 8, 10, 10, 10] = true
-since its 'Decidable' instance reduced to
+since its 'Decidable' instance
+  instDecidableEqBool (check_sorted #[0, 3, 3, 5, 8, 10, 10, 10]) true
+did not reduce to 'isTrue' or 'isFalse'.
+
+After unfolding the instances 'instDecidableEqBool' and 'Bool.decEq', reduction got stuck at the 'Decidable' instance
   match check_sorted #[0, 3, 3, 5, 8, 10, 10, 10], true with
   | false, false => isTrue ⋯
   | false, true => isFalse ⋯
   | true, false => isFalse ⋯
   | true, true => isTrue ⋯
-rather than to the 'isTrue' constructor.
 -/
 #guard_msgs in
 example: check_sorted #[0, 3, 3, 5, 8, 10, 10, 10] := by

tests/lean/run/decideTactic.lean

@@ -0,0 +1,104 @@
+/-!
+# Tests of the `decide` tactic
+-/
+
+/-!
+Success
+-/
+#guard_msgs in
+example : 2 + 2 ≠ 5 := by decide
+
+
+/-!
+False proposition
+-/
+
+/--
+error: tactic 'decide' proved that the proposition
+  1 ≠ 1
+is false
+-/
+#guard_msgs in
+example : 1 ≠ 1 := by decide
+
+
+/-!
+Irreducible decidable instance
+-/
+opaque unknownProp : Prop
+
+/--
+error: tactic 'decide' failed for proposition
+  unknownProp
+since its 'Decidable' instance
+  Classical.propDecidable unknownProp
+did not reduce to 'isTrue' or 'isFalse'.
+
+After unfolding the instance 'Classical.propDecidable', reduction got stuck at the 'Decidable' instance
+  Classical.choice ⋯
+
+Hint: Reduction got stuck on 'Classical.choice', which indicates that a 'Decidable' instance is
+defined using classical reasoning, proving an instance exists rather than giving a concrete
+construction. The 'decide' tactic works by evaluating a decision procedure via reduction, and it
+cannot make progress with such instances. This can occur due to the 'opened scoped Classical'
+command, which enables the instance 'Classical.propDecidable'.
+-/
+#guard_msgs in
+open scoped Classical in
+example : unknownProp := by decide
+
+
+/-!
+Reporting unfolded instances and give hint about Eq.rec.
+From discussion with Heather Macbeth on Zulip
+-/
+structure Nice (n : Nat) : Prop :=
+  (large : 100 ≤ n)
+
+theorem nice_iff (n : Nat) : Nice n ↔ 100 ≤ n := ⟨Nice.rec id, Nice.mk⟩
+
+def baz (n : Nat) : Decidable (Nice n) := by
+  rw [nice_iff]
+  infer_instance
+
+instance : Decidable (Nice n) := baz n
+
+/--
+error: tactic 'decide' failed for proposition
+  Nice 102
+since its 'Decidable' instance
+  instDecidableNice
+did not reduce to 'isTrue' or 'isFalse'.
+
+After unfolding the instances 'baz' and 'instDecidableNice', reduction got stuck at the 'Decidable' instance
+  ⋯ ▸ inferInstance
+
+Hint: Reduction got stuck on '▸' (Eq.rec), which suggests that one of the 'Decidable' instances is
+defined using tactics such as 'rw' or 'simp'. To avoid tactics, make use of functions such as
+'inferInstanceAs' or 'decidable_of_decidable_of_iff' to alter a proposition.
+-/
+#guard_msgs in
+example : Nice 102 := by decide
+
+
+/-!
+Following `Decidable.rec` to give better messages
+-/
+
+/--
+error: tactic 'decide' failed for proposition
+  ¬Nice 102
+since its 'Decidable' instance
+  instDecidableNot
+did not reduce to 'isTrue' or 'isFalse'.
+
+After unfolding the instances 'baz', 'instDecidableNice' and 'instDecidableNot', reduction got stuck
+at the 'Decidable' instance
+  ⋯ ▸ inferInstance
+
+Hint: Reduction got stuck on '▸' (Eq.rec), which suggests that one of the 'Decidable' instances is
+defined using tactics such as 'rw' or 'simp'. To avoid tactics, make use of functions such as
+'inferInstanceAs' or 'decidable_of_decidable_of_iff' to alter a proposition.
+-/
+#guard_msgs in
+example : ¬ Nice 102 := by decide