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).

Author: kmill

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,31 +370,95 @@ 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
     let d ← mkDecide expectedType
     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,17 +128,32 @@ 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
     .ofFormatWithInfosM (PrettyPrinter.ppExprWithInfos (delab := delab) e)
   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

@@ -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/2161.lean.expected.out

@@ -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