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

src/Lean/Linter.lean

@@ -18,3 +18,4 @@ public import Lean.Linter.List
 public import Lean.Linter.Sets
 public import Lean.Linter.UnusedSimpArgs
 public import Lean.Linter.Coe
+public import Lean.Linter.TacticTypeCheck

src/Lean/Linter/TacticTypeCheck.lean

@@ -0,0 +1,123 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Ullrich
+-/
+module
+
+prelude
+public import Lean.Elab.Command
+public import Lean.Linter.Util
+import Lean.Meta.Check
+import Lean.Meta.Diagnostics
+
+public section
+
+set_option linter.missingDocs true
+
+namespace Lean.Linter
+
+open Lean Elab Command
+open Lean.Linter (logLint)
+
+/--
+Warn when the goal target is not type-correct at `.instances` transparency.
+This can happen when e.g. `unfold` leaves hypotheses whose types still refer to
+the pre-unfolded definition, preventing `rw`/`simp` from matching patterns.
+-/
+register_builtin_option linter.tacticCheckInstances : Bool := {
+  defValue := false
+  descr := "enable the linter that type-checks every tactic goal at `.instances` transparency"
+}
+
+/-- A linter that runs `Meta.check _ .instances` on every tactic goal. -/
+def tacticCheckInstances : Linter where
+  run _cmdStx := do
+    unless getLinterValue linter.tacticCheckInstances (← getLinterOptions) do
+      return
+    let infoTrees := (← get).infoState.trees.toArray
+    -- Once any tactic step in this command has produced a warning, suppress
+    -- all further checks: a bad lctx typically persists across many tactic
+    -- steps, and mvarIds change between steps (tactics like `unfold`/`rw`
+    -- call `replaceTargetEq` which allocates a fresh mvar), so mvarId-keyed
+    -- dedup would not suffice.
+    let warned : IO.Ref Bool ← IO.mkRef false
+    for tree in infoTrees do
+      -- `postNode` so children are visited before parents: leaf tactic infos
+      -- (the actual user-written `unfold`, `rw`, ...) fire before the
+      -- enclosing tactic-sequence node, which has the syntax of the whole
+      -- `by` block and would otherwise be the warning location.
+      tree.visitM' (postNode := fun ci info _ => do
+        if (← warned.get) then return
+        let .ofTacticInfo ti := info | return
+        -- Check `goalsBefore` then `goalsAfter`.
+        -- - `goalsBefore` catches an initially-bad goal at the first tactic.
+        -- - `goalsAfter` catches the result of this tactic — so `unfold foo`
+        --   gets blamed, not the next tactic whose `goalsBefore` inherits it.
+        --
+        -- For each goal, we run `check` first at `.all` transparency, then
+        -- (after resetting the unfold counter) at `.instances`. If the
+        -- `.instances` check fails, the defs unfolded at `.all` but not at
+        -- `.instances` are the candidates for `@[implicit_reducible]` and get
+        -- reported to the user. The pattern mirrors `mkUnfoldAxiomsNote` in
+        -- `Lean.Meta.Check`.
+        -- `kind` selects the wording of the warning:
+        --   * "initial" — the failure is in `goalsBefore` of the first tactic
+        --     (i.e. the `by` block started with a bad goal).
+        --   * "produced" — the failure is in `goalsAfter` of this tactic
+        --     (i.e. this tactic left the goal in a bad state).
+        let checkGoal (kind : String) (g : MVarId) : MetaM (Option MessageData) := do
+          let some mdecl := (← getMCtx).findDecl? g | return none
+          let target ← instantiateMVars mdecl.type
+          let origDiag := (← get).diag
+          let result : Option MessageData ← Meta.withLCtx mdecl.lctx #[] <|
+              withOptions (diagnostics.set · true) do
+            -- Record what `.all` unfolds (must succeed — the goal is
+            -- well-typed at `.all` by assumption).
+            Meta.check target .all
+            let counterAll := (← get).diag.unfoldCounter
+            -- Reset and try at `.instances`.
+            modify ({ · with diag := origDiag })
+            try
+              Meta.check target .instances
+              return none
+            catch _ =>
+              let counterInst := (← get).diag.unfoldCounter
+              let diff := Meta.subCounters counterAll counterInst
+              let env ← getEnv
+              let candidates : List MessageData :=
+                diff.toList.filterMap fun (n, count) => do
+                  guard <| count > 0
+                  guard <| getReducibilityStatusCore env n matches .semireducible
+                  guard <| !Meta.isInstanceCore env n
+                  return m!"{.ofConstName n}"
+              if candidates.isEmpty then
+                return none
+              let remedy : MessageData := match kind with
+                | "initial" => "consider rephrasing the goal or marking"
+                | _         => "consider using propositional rewriting or marking"
+              return some m!"{kind} tactic goal is not type-correct at \
+                `.instances` transparency; {remedy} some of the following as \
+                `@[implicit_reducible]`:\
+                {indentD (.joinSep candidates Format.line)}"
+          -- Always restore the original diagnostics snapshot.
+          modify ({ · with diag := origDiag })
+          return result
+        let check (kind : String) (goals : List MVarId) : MetaM (Option MessageData) := do
+          for g in goals do
+            if let some msg ← checkGoal kind g then
+              return some msg
+          return none
+        let ctxBefore : ContextInfo := { ci with mctx := ti.mctxBefore }
+        let ctxAfter  : ContextInfo := { ci with mctx := ti.mctxAfter }
+        let failure : Option MessageData ← liftM do
+          let m₁ ← ctxBefore.runMetaM {} (check "initial" ti.goalsBefore)
+          if m₁.isSome then return m₁
+          ctxAfter.runMetaM {} (check "produced" ti.goalsAfter)
+        if let some msg := failure then
+          warned.set true
+          logLint linter.tacticCheckInstances ti.stx msg)
+
+builtin_initialize addLinter tacticCheckInstances
+
+end Lean.Linter

src/Lean/Meta/Check.lean

@@ -328,15 +328,39 @@ 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
 
+/--
+Run `x` and, on any error, lazily check whether `e` is type-correct at `instances` transparency.
+If not, append an explanatory note to the error message.
+
+This is useful for tactics like `rw` and `simp` whose failure modes can be caused by
+prior tactics (such as `unfold`) leaving the goal in a state that's type-correct only at
+`.all` transparency, preventing pattern matching at `.instances`.
+-/
+def withInstancesTypeCheckNote (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. \
+        Use `set_option linter.tacticCheckInstances true` to investigate the source of the issue."
+  try
+    x
+  catch
+    | .error ref msg => throw (.error ref (msg ++ typeCheckNote))
+    | ex => throw ex
+
 /--
 Return true if `e` is type correct.
 -/

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
 
@@ -27,6 +28,7 @@ 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 :=
+  withInstancesTypeCheckNote e do
   mvarId.withContext do
     mvarId.checkNotAssigned `rewrite
     let heqIn := heq

src/Lean/Meta/Tactic/Simp/Main.lean

@@ -11,6 +11,7 @@ public import Lean.Meta.Tactic.Simp.Diagnostics
 public import Lean.Meta.Match.Value
 public import Lean.Meta.MonadSimp
 public import Lean.Util.CollectLooseBVars
+import Lean.Meta.Check
 import Lean.Meta.HaveTelescope
 import Lean.PrettyPrinter
 import Lean.ExtraModUses
@@ -797,7 +798,8 @@ def simpTarget (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray
     (mayCloseGoal := true) (stats : Stats := {}) : MetaM (Option MVarId × Stats) :=
   mvarId.withContext do
     mvarId.checkNotAssigned `simp
-    simpTargetCore mvarId ctx simprocs discharge? mayCloseGoal stats
+    withInstancesTypeCheckNote (← mvarId.getType) do
+      simpTargetCore mvarId ctx simprocs discharge? mayCloseGoal stats
 
 /--
 Applies the result `r` for `type` (which is inhabited by `val`). Returns `none` if the goal was closed. Returns `some (val', type')`
@@ -876,6 +878,7 @@ def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray :=
     (stats : Stats := {}) : MetaM (Option (Array FVarId × MVarId) × Stats) := do
   mvarId.withContext do
     mvarId.checkNotAssigned `simp
+    withInstancesTypeCheckNote (← mvarId.getType) do
     let mut mvarIdNew := mvarId
     let mut toAssert := #[]
     let mut replaced := #[]
@@ -930,6 +933,7 @@ def dsimpGoal (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray :
     (stats : Stats := {}) : MetaM (Option MVarId × Stats) := do
    mvarId.withContext do
     mvarId.checkNotAssigned `simp
+    withInstancesTypeCheckNote (← mvarId.getType) do
     let mut mvarIdNew := mvarId
     let mut stats : Stats := stats
     for fvarId in fvarIdsToSimp do

src/Lean/Meta/Tactic/Simp/SimpAll.lean

@@ -150,11 +150,12 @@ end SimpAll
 
 def simpAll (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (stats : Stats := {}) : MetaM (Option MVarId × Stats) := do
   mvarId.withContext do
-    let (r, s) ← SimpAll.main.run { stats with mvarId, ctx, simprocs }
-    if let .some mvarIdNew := r then
-      if ctx.config.failIfUnchanged && mvarId == mvarIdNew then
-        throwError "simp_all made no progress"
-    return (r, { s with })
+    withInstancesTypeCheckNote (← mvarId.getType) do
+      let (r, s) ← SimpAll.main.run { stats with mvarId, ctx, simprocs }
+      if let .some mvarIdNew := r then
+        if ctx.config.failIfUnchanged && mvarId == mvarIdNew then
+          throwError "simp_all made no progress"
+      return (r, { s with })
 
 builtin_initialize
   registerTraceClass `Meta.Tactic.simp.all

tests/elab/linterTacticCheckInstances.lean

@@ -0,0 +1,62 @@
+module
+
+structure S where
+  decls : Array Nat
+
+structure E where
+  s : S
+
+structure Inp (s : S) where
+  x : Nat
+
+def myF (s : S) (_ : Inp s) : E := ⟨s⟩
+
+def composed (s : S) (a b : Nat) : E :=
+  let res := myF s ⟨a⟩
+  myF res.s ⟨b⟩
+
+-- Sanity check: with the linter off (default), no warning is emitted.
+#guard_msgs in
+set_option warn.sorry false 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
+  sorry
+
+set_option linter.tacticCheckInstances true
+
+-- `unfold composed` leaves the goal in a state that is type-correct only at
+-- `.all` transparency. The linter should warn at `unfold composed`
+-- not at the enclosing `by` or the later tactic that inherits the
+-- bad state.
+/--
+@ +4:2...17
+warning: produced tactic goal is not type-correct at `.instances` transparency; consider using propositional rewriting or marking some of the following as `@[implicit_reducible]`:
+  composed
+  myF
+
+Note: This linter can be disabled with `set_option linter.tacticCheckInstances false`
+-/
+#guard_msgs (positions := 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
+  rfl
+
+-- The initial goal may already be type-incorrect at `.instances` (here the
+-- elaborator shares a single proof argument between the two `decls[idx]`
+-- accesses). The linter should warn on the first tactic of the `by` block.
+/--
+@ +3:2...5
+warning: initial tactic goal is not type-correct at `.instances` transparency; consider rephrasing the goal or marking some of the following as `@[implicit_reducible]`:
+  composed
+  myF
+
+Note: This linter can be disabled with `set_option linter.tacticCheckInstances false`
+-/
+#guard_msgs (positions := 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
+  rfl

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