feat: have "motive is not type correct" come with an explanation (#6168)

This PR extends the "motive is not type correct" error message for the
rewrite tactic to explain what it means. It also pretty prints the
type-incorrect motive and reports the type error.

Suggested [on
Zulip](https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/tactic.20'rewrite'.20failed.2C.20motive.20is.20not.20type.20correct/near/483545154).

src/Lean/Meta/Tactic/Rewrite.lean

@@ -45,12 +45,26 @@ def _root_.Lean.MVarId.rewrite (mvarId : MVarId) (e : Expr) (heq : Expr)
           let eNew ← instantiateMVars eNew
           let eType ← inferType e
           let motive := Lean.mkLambda `_a BinderInfo.default α eAbst
-          unless (← isTypeCorrect motive) do
-            throwTacticEx `rewrite mvarId "motive is not type correct"
+          try
+            check motive
+          catch ex =>
+            throwTacticEx `rewrite mvarId m!"\
+              motive is not type correct:{indentD motive}\nError: {ex.toMessageData}\
+              \n\n\
+              Explanation: The rewrite tactic rewrites an expression 'e' using an equality 'a = b' by the following process. \
+              First, it looks for all 'a' in 'e'. Second, it tries to abstract these occurrences of 'a' to create a function 'm := fun _a => ...', called the *motive*, \
+              with the property that 'm a' is definitionally equal to 'e'. \
+              Third, we observe that '{.ofConstName ``congrArg}' implies that 'm a = m b', which can be used with lemmas such as '{.ofConstName ``Eq.mpr}' to change the goal. \
+              However, if 'e' depends on specific properties of 'a', then the motive 'm' might not typecheck.\
+              \n\n\
+              Possible solutions: use rewrite's 'occs' configuration option to limit which occurrences are rewritten, \
+              or use 'simp' or 'conv' mode, which have strategies for certain kinds of dependencies \
+              (these tactics can handle proofs and '{.ofConstName ``Decidable}' instances whose types depend on the rewritten term, \
+              and 'simp' can apply user-defined '@[congr]' theorems as well)."
           unless (← withLocalDeclD `_a α fun a => do isDefEq (← inferType (eAbst.instantiate1 a)) eType) do
             -- NB: using motive.arrow? would disallow motives where the dependency
             -- can be reduced away
-            throwTacticEx `rewrite mvarId "motive is dependent"
+            throwTacticEx `rewrite mvarId m!"motive is dependent{indentD motive}"
           let u1 ← getLevel α
           let u2 ← getLevel eType
           let eqPrf := mkApp6 (.const ``congrArg [u1, u2]) α eType lhs rhs motive heq

tests/lean/motiveNotTypeCorect.lean.expected.out

@@ -1,11 +1,25 @@
-motiveNotTypeCorect.lean:7:6-7:7: error: tactic 'rewrite' failed, motive is not type correct
+motiveNotTypeCorect.lean:7:6-7:7: error: tactic 'rewrite' failed, motive is not type correct:
+  fun _a => P _a d
+Error: application type mismatch
+  P _a d
+argument
+  d
+has type
+  D (f t) : Type
+but is expected to have type
+  D _a : Type
+
+Explanation: The rewrite tactic rewrites an expression 'e' using an equality 'a = b' by the following process. First, it looks for all 'a' in 'e'. Second, it tries to abstract these occurrences of 'a' to create a function 'm := fun _a => ...', called the *motive*, with the property that 'm a' is definitionally equal to 'e'. Third, we observe that 'congrArg' implies that 'm a = m b', which can be used with lemmas such as 'Eq.mpr' to change the goal. However, if 'e' depends on specific properties of 'a', then the motive 'm' might not typecheck.
+
+Possible solutions: use rewrite's 'occs' configuration option to limit which occurrences are rewritten, or use 'simp' or 'conv' mode, which have strategies for certain kinds of dependencies (these tactics can handle proofs and 'Decidable' instances whose types depend on the rewritten term, and 'simp' can apply user-defined '@[congr]' theorems as well).
 t : Nat
 f : Nat → Nat
 h : f t = t
 d : D (f t)
 P : (t : Nat) → D t → Prop
 ⊢ P (f t) d
 motiveNotTypeCorect.lean:18:8-18:9: error: tactic 'rewrite' failed, motive is dependent
+  fun _a => A _a
 h : true = false
 A : (b : Bool) → if b = true then Prop else Nat
 ⊢ A true