feat: add type-correctness note to rewrite tactic error messages

src/Lean/Meta/Check.lean

@@ -328,11 +328,11 @@ where
 /--
 Throw an exception if `e` is not type correct.
 -/
-def check (e : Expr) : MetaM Unit :=
+def check (e : Expr) (transparency : TransparencyMode := .all) : MetaM Unit :=
   withTraceNode `Meta.check (fun _ =>
       return m!"{e}") do
     try
-      withTransparency TransparencyMode.all $ checkAux e
+      withTransparency transparency $ checkAux e
     catch ex =>
       trace[Meta.check] ex.toMessageData
       throw ex

src/Lean/Meta/Tactic/Rewrite.lean

@@ -11,6 +11,7 @@ public import Lean.Meta.MatchUtil
 public import Lean.Meta.KAbstract
 public import Lean.Meta.Tactic.Apply
 public import Lean.Meta.BinderNameHint
+import Lean.Meta.Check
 
 public section
 
@@ -21,12 +22,32 @@ structure RewriteResult where
   eqProof  : Expr
   mvarIds  : List MVarId -- new goals
 
+/--
+Run `x` and, on any error, lazily check whether `e` is type-correct at `instances` transparency.
+If not, append a note to the error message.
+-/
+def withRewriteTypeCheck (e : Expr) (x : MetaM α) : MetaM α := do
+  let typeCheckNote := MessageData.ofLazyM (es := #[e]) do
+    try
+      check e .instances
+      return .nil
+    catch _ =>
+      return MessageData.note m!"The target expression is not type-correct \
+        under the `instances` transparency level, which may have triggered the failure. \
+        This is usually caused by unfolding of semireducible definitions in prior tactic steps."
+  try
+    x
+  catch
+    | .error ref msg => throw (.error ref (msg ++ typeCheckNote))
+    | ex => throw ex
+
 /--
 Rewrite `e` using `heq` in the context of `mvarId`.
 Returns the result of the rewrite, the metavariable `mvarId` is not assigned.
 -/
 def _root_.Lean.MVarId.rewrite (mvarId : MVarId) (e : Expr) (heq : Expr)
     (symm : Bool := false) (config := { : Rewrite.Config }) : MetaM RewriteResult :=
+  withRewriteTypeCheck e do
   mvarId.withContext do
     mvarId.checkNotAssigned `rewrite
     let heqIn := heq

tests/elab/rewrite_type_check_note.lean

@@ -0,0 +1,71 @@
+module
+
+/-!
+After `unfold`, the goal may become not type-correct at `instances` transparency
+because hypotheses still refer to the pre-unfolded definition. When `rw` fails
+to find a pattern match in such a goal, the error message should include a note
+about the type-correctness issue.
+-/
+
+structure S where
+  decls : Array Nat
+
+structure E where
+  s : S
+
+structure Inp (s : S) where
+  x : Nat
+
+class C (β : S → Type) (f : (s : S) → β s → E) where
+  decl_eq : ∀ (s : S) (input : β s)
+    (idx : Nat) (h1 : idx < s.decls.size) (h2 : idx < (f s input).s.decls.size),
+    (f s input).s.decls[idx]'h2 = s.decls[idx]'h1
+
+def myF (s : S) (_ : Inp s) : E := ⟨s⟩
+
+set_option warn.sorry false in
+instance : C Inp myF where
+  decl_eq := by intros; sorry
+
+def composed (s : S) (a b : Nat) : E :=
+  let res := myF s ⟨a⟩
+  myF res.s ⟨b⟩
+
+-- Without `unfold`, the note should NOT fire (goal is type-correct at `instances`)
+/--
+error: Tactic `rewrite` failed: Did not find an occurrence of the pattern
+  (myF ?s ?input).s.decls[?idx]
+in the target expression
+  (composed s a b).s.decls[idx] = s.decls[idx]
+
+s : S
+a b idx : Nat
+h1 : idx < s.decls.size
+h2 : idx < (composed s a b).s.decls.size
+⊢ (composed s a b).s.decls[idx] = s.decls[idx]
+-/
+#guard_msgs in
+example (s : S) (a b idx : Nat) (h1 : idx < s.decls.size)
+    (h2 : idx < (composed s a b).s.decls.size) :
+    (composed s a b).s.decls[idx]'h2 = s.decls[idx]'h1 := by
+  rw [C.decl_eq (f := myF)]
+
+-- With `unfold`, the note SHOULD fire (`h2`'s type no longer matches after unfolding)
+/--
+Note: The target expression is not type-correct under the `instances` transparency level, which may have triggered the failure. This is usually caused by unfolding of semireducible definitions in prior tactic steps.
+-/
+#guard_msgs (substring := true) in
+example (s : S) (a b idx : Nat) (h1 : idx < s.decls.size)
+    (h2 : idx < (composed s a b).s.decls.size) :
+    (composed s a b).s.decls[idx]'h2 = s.decls[idx]'h1 := by
+  unfold composed
+  rw [C.decl_eq (f := myF)]
+
+-- However, the defeq abuse may already be part of the initial goal, in which case the note is not as helpful.
+/--
+Note: The target expression is not type-correct under the `instances` transparency level, which may have triggered the failure. This is usually caused by unfolding of semireducible definitions in prior tactic steps.
+-/
+#guard_msgs (substring := true) in
+example (s : S) (a b idx : Nat) (h1 : idx < s.decls.size) :
+    (composed s a b).s.decls[idx] = s.decls[idx] := by
+  rw [C.decl_eq (f := myF)]