From 561d42c85438e6a2742fe159e04db86a92636665 Mon Sep 17 00:00:00 2001
From: Julia Markus Himmel <2065352+TwoFX@users.noreply.github.com>
Date: Mon, 25 May 2026 10:15:46 +0000
Subject: [PATCH 01/16] experiment: always check types for instance
 metavariables at instances transparency

---
 src/Lean/Meta/ExprDefEq.lean | 15 ++++++++++++++-
 1 file changed, 14 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index 6a8b7ce3e962..b37aa59346de 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -674,7 +674,20 @@ private def checkTypesAndAssign (mvar : Expr) (v : Expr) : MetaM Bool :=
       let mvarType ← inferType mvar
       let vType ← inferType v
       if (← respectTransparencyAtTypes) then
-        withImplicitConfig do
+        -- For instance metavariables — those created for an instance-implicit (`[..]`) parameter,
+        -- identified by `.synthetic` kind together with a class type — cap the transparency at
+        -- exactly `.instances` so an ambient `.default`/`.all` does not let semireducible
+        -- definitions be unfolded while checking the type of an instance assignment. This
+        -- intentionally does not apply to ordinary implicit (`{..}`) metavariables that happen
+        -- to have a class type, which are created with `.natural` kind.
+        let isInstance ←
+          if (← mvar.mvarId!.getKind) matches .synthetic then
+            pure (← isClass? mvarType).isSome
+          else
+            pure false
+        let capInstance (x : MetaM Bool) : MetaM Bool :=
+          if isInstance then withTransparency .instances x else x
+        capInstance <| withImplicitConfig do
           if (← Meta.isExprDefEqAux mvarType vType) then
             mvar.mvarId!.assign v
             return true

From 020bb06e0444910b7249a1fcaef70e32f93ce8eb Mon Sep 17 00:00:00 2001
From: Julia Markus Himmel <2065352+TwoFX@users.noreply.github.com>
Date: Tue, 26 May 2026 10:28:31 +0000
Subject: [PATCH 02/16] fixes

---
 src/Init/Prelude.lean                              | 14 ++++++++++++++
 .../LRAT/Internal/Formula/RatAddSound.lean         |  4 +++-
 src/Std/Time/Format/Basic.lean                     |  4 ++--
 3 files changed, 19 insertions(+), 3 deletions(-)

diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 497df8c35249..7a793406e367 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -1023,11 +1023,25 @@ theorem of_decide_eq_true [inst : Decidable p] : Eq (decide p) true → p := fun
   | isTrue  h₁ => h₁
   | isFalse h₁ => absurd h (Bool.ne_true_of_eq_false (decide_eq_false h₁))
 
+/--
+Variant of `of_decide_eq_true` that takes `Decidable` as an implicit argument, intended for
+forward reasoning.
+-/
+theorem of_decide_eq_true_forward {inst : Decidable p} : Eq (decide p) true → p :=
+  of_decide_eq_true
+
 theorem of_decide_eq_false [inst : Decidable p] : Eq (decide p) false → Not p := fun h =>
   match (generalizing := false) inst with
   | isTrue  h₁ => absurd h (Bool.ne_false_of_eq_true (decide_eq_true h₁))
   | isFalse h₁ => h₁
 
+/--
+Variant of `of_decide_eq_false` that takes `Decidable` as an implicit argument, intended for
+forward reasoning.
+-/
+theorem of_decide_eq_false_forward {inst : Decidable p} : Eq (decide p) false → Not p :=
+  of_decide_eq_false
+
 theorem of_decide_eq_self_eq_true [inst : DecidableEq α] (a : α) : Eq (decide (Eq a a)) true :=
   match (generalizing := false) inst a a with
   | isTrue  _  => rfl
diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean
index 38b719eb9cd2..85a826d5cbc1 100644
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean
@@ -412,11 +412,13 @@ theorem existsRatHint_of_ratHintsExhaustive {n : Nat} (f : DefaultFormula n)
     List.mem_filterMap, id_eq, exists_eq_right] at c'_in_f
   rw [List.mem_iff_getElem] at c'_in_f
   rcases c'_in_f with ⟨i, hi, c'_in_f⟩
+  -- The following `simp only` leaves behind a term containing a `decide` where the embedded
+  -- `Decidable` instances does not typecheck at `instances` transparency.
   simp only [ratHintsExhaustive, getRatClauseIndices] at ratHintsExhaustive_eq_true
   have i_in_bounds : i < Array.size (Array.range (Array.size f.clauses)) := by grind
   have i_lt_f_clauses_size : i < f.clauses.size := by grind
   have h : i ∈ (ratHints.map (fun x => x.1)).toList := by
-    rw [← of_decide_eq_true ratHintsExhaustive_eq_true]
+    simp only [← of_decide_eq_true_forward ratHintsExhaustive_eq_true]
     have i_eq_range_i : i = (Array.range f.clauses.size)[i]'i_in_bounds := by grind
     rw [i_eq_range_i]
     rw [Array.mem_toList_iff]
diff --git a/src/Std/Time/Format/Basic.lean b/src/Std/Time/Format/Basic.lean
index 10bdf6dfd934..312a918fdd2e 100644
--- a/src/Std/Time/Format/Basic.lean
+++ b/src/Std/Time/Format/Basic.lean
@@ -740,13 +740,13 @@ private def parseWith (config : FormatConfig) : (mod : Modifier) → Parser (Typ
   | .y format =>
     match format with
     | .any => Int.ofNat <$> parseAtLeastNum 1
-    | .twoDigit => (2000 + ·) <$> Int.ofNat <$> parseNum 2
+    | .twoDigit => (fun x => (2000 + x : Int)) <$> Int.ofNat <$> parseNum 2
     | .fourDigit => Int.ofNat <$> parseNum 4
     | .extended n => Int.ofNat <$> parseNum n
   | .u format =>
     match format with
     | .any => parseSigned <| parseAtLeastNum 1
-    | .twoDigit => (2000 + ·) <$> Int.ofNat <$> parseNum 2
+    | .twoDigit => (fun x => (2000 + x : Int)) <$> Int.ofNat <$> parseNum 2
     | .fourDigit => parseSigned <| parseNum 4
     | .extended n => parseSigned <| parseNum n
   | .Y format =>

From e1bde313638d3696a559f6ab111b3aca22ea64a8 Mon Sep 17 00:00:00 2001
From: Julia Markus Himmel <2065352+TwoFX@users.noreply.github.com>
Date: Tue, 26 May 2026 12:54:47 +0000
Subject: [PATCH 03/16] Introduct option

---
 src/Lean/Meta/ExprDefEq.lean | 16 +++++++++++++++-
 1 file changed, 15 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index b37aa59346de..f92b14615d8d 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -60,6 +60,19 @@ register_builtin_option backward.isDefEq.respectTransparency.types : Bool := {
   when checking whether the type of a metavariable matches the type of the term being assigned to it."
 }
 
+/--
+Controls whether, when checking the type of an assignment to an instance-implicit (`[..]`)
+metavariable, the transparency is capped at `.instances` so an ambient `.default`/`.all`
+does not let semireducible definitions be unfolded.
+
+This option only has an effect when `backward.isDefEq.respectTransparency.types` is `true`.
+-/
+register_builtin_option backward.isDefEq.respectTransparency.instances : Bool := {
+  defValue := true
+  descr    := "if true (the default), cap transparency at `.instances` when checking the type \
+  of an assignment to an instance-implicit metavariable"
+}
+
 /--
 Controls whether non-instance implicit arguments get their transparency bumped to
 `TransparencyMode.implicit` during `isDefEq`.
@@ -681,7 +694,8 @@ private def checkTypesAndAssign (mvar : Expr) (v : Expr) : MetaM Bool :=
         -- intentionally does not apply to ordinary implicit (`{..}`) metavariables that happen
         -- to have a class type, which are created with `.natural` kind.
         let isInstance ←
-          if (← mvar.mvarId!.getKind) matches .synthetic then
+          if backward.isDefEq.respectTransparency.instances.get (← getOptions) &&
+              (← mvar.mvarId!.getKind) matches .synthetic then
             pure (← isClass? mvarType).isSome
           else
             pure false

From 11206ad146504fd90b658d885204a8abeb3f1596 Mon Sep 17 00:00:00 2001
From: Julia Markus Himmel <2065352+TwoFX@users.noreply.github.com>
Date: Wed, 27 May 2026 08:41:02 +0000
Subject: [PATCH 04/16] experiment: do not bump transparency when assigning
 `outParam`s

---
 src/Lean/Meta/SynthInstance.lean | 30 +++++++++++++++++++++++++++++-
 tests/elab/irredoutparam.lean    | 15 +++++++++++++++
 2 files changed, 44 insertions(+), 1 deletion(-)
 create mode 100644 tests/elab/irredoutparam.lean

diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean
index 6a03f9943177..abffcbf2dc7e 100644
--- a/src/Lean/Meta/SynthInstance.lean
+++ b/src/Lean/Meta/SynthInstance.lean
@@ -32,6 +32,28 @@ register_builtin_option backward.synthInstance.canonInstances : Bool := {
   descr := "use optimization that relies on 'morally canonical' instances during type class resolution"
 }
 
+/--
+Controls the transparency used by the post-synthesis check that unifies the original goal type
+with the synthesized result's type when the class has `outParam`s.
+
+When `true` (the default), the check uses `.instances` transparency, matching the transparency
+used by the rest of typeclass resolution. This means a non-reducible `def Bar := Nat` is *not*
+unfolded, so e.g. `#synth Foo Nat Bar` cannot be satisfied by `instance : Foo Nat Nat`.
+
+When `false`, the check bumps transparency to `.default`, which unfolds semireducible
+definitions. This was the historical behavior, retained because patterns like Mathlib's
+`def OrderDual (α : Type) : Type := α` rely on `OrderDual α` and `α` being defEq at `.default`
+during the outParam check.
+
+See `assignOutParams` for the implementation.
+-/
+register_builtin_option backward.isDefEq.respectTransparency.outParams : Bool := {
+  defValue := true
+  descr    := "if true (the default), do not bump transparency to `.default` \
+  when checking that a synthesized instance's type matches the original goal type \
+  for classes with `outParam`s"
+}
+
 namespace SynthInstance
 
 def getMaxHeartbeats (opts : Options) : Nat :=
@@ -842,8 +864,14 @@ private def assignOutParams (type : Expr) (result : Expr) : MetaM Bool := do
   ```
   Mathlib developers are currently trying to refactor the `OrderDual` declaration,
   but it will take time. We will try to remove the `withDefault` again after the refactoring.
+
+  The `backward.isDefEq.respectTransparency.outParams` option (defaulting to `true`) keeps the
+  check at `.instances` transparency. Setting it to `false` restores the historical `withDefault`
+  behavior.
   -/
-  let defEq ← withDefault <| withAssignableSyntheticOpaque <| isDefEq type resultType
+  let bumpTransparency := !backward.isDefEq.respectTransparency.outParams.get (← getOptions)
+  let defEq ← (if bumpTransparency then withDefault else id) <|
+    withAssignableSyntheticOpaque <| isDefEq type resultType
   unless defEq do
     trace[Meta.synthInstance] "{crossEmoji} result type{indentExpr resultType}\nis not definitionally equal to{indentExpr type}"
   return defEq
diff --git a/tests/elab/irredoutparam.lean b/tests/elab/irredoutparam.lean
new file mode 100644
index 000000000000..a82e11569a6e
--- /dev/null
+++ b/tests/elab/irredoutparam.lean
@@ -0,0 +1,15 @@
+class Foo (α : Type) (β : outParam Type) where
+
+def Bar :=
+  Nat
+
+instance : Foo Nat Nat where
+
+/--
+error: failed to synthesize
+  Foo Nat Bar
+
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+-/
+#guard_msgs in
+#synth Foo Nat Bar -- instFooNat

From 4200b4baf1127e0947c39d7c05a4e9a01ea6039b Mon Sep 17 00:00:00 2001
From: Julia Markus Himmel <2065352+TwoFX@users.noreply.github.com>
Date: Wed, 27 May 2026 12:03:12 +0000
Subject: [PATCH 05/16] experiment: fix `inferInstanceAs` elaborator

---
 src/Lean/Elab/BuiltinTerm.lean   | 38 ++++++++++++++++++++++++++++++-
 tests/elab/inferInstanceAs2.lean | 39 ++++++++++++++++++++++++++++++++
 2 files changed, 76 insertions(+), 1 deletion(-)
 create mode 100644 tests/elab/inferInstanceAs2.lean

diff --git a/src/Lean/Elab/BuiltinTerm.lean b/src/Lean/Elab/BuiltinTerm.lean
index 32906b9bc869..3a16c592efdc 100644
--- a/src/Lean/Elab/BuiltinTerm.lean
+++ b/src/Lean/Elab/BuiltinTerm.lean
@@ -349,6 +349,42 @@ private def resynthInstImplicitArgs (type : Expr) : TermElabM Expr := do
   let args := mvars ++ args.drop mvars.size
   instantiateMVars (mkAppN fn args)
 
+/--
+Best-effort unification of the user-supplied `type` against the `expectedType` to resolve
+user-placed `_` placeholders. We decompose both sides as applications of a common head and
+unify arguments position-by-position, skipping instance-implicit positions.
+
+Instance-implicit arguments of `type` are fresh synthetic class metavariables introduced by
+`elabType` that will be discarded by `resynthInstImplicitArgs`. Routing them through `isDefEq`
+serves no purpose and can spuriously fail: assigning a synthetic class metavariable triggers
+a transparency cap at `.instances` in the type-equality check (see
+`backward.isDefEq.respectTransparency.instances`), which prevents non-`[reducible]` definitions
+from unfolding — so, e.g., `Neg (Nat ⧸ n) =?= Neg (Zmod n)` fails even though `Zmod` reduces
+to `Nat ⧸ n` at `.default` transparency. The outer `isDefEq` then fails and rolls back the
+useful assignments made to user `_` placeholders.
+
+When the two sides do not share a common-shape head, we fall back to a plain `isDefEq`.
+Per-argument `isDefEq` calls are best-effort: a failure at one position does not roll back
+successes at others.
+-/
+private def unifyTypeForInferInstanceAs (type expectedType : Expr) : TermElabM Unit := do
+  let typeFn := type.getAppFn
+  let expectedFn := expectedType.getAppFn
+  let typeArgs := type.getAppArgs
+  let expectedArgs := expectedType.getAppArgs
+  unless typeFn.isConst && expectedFn.isConst
+      && typeFn.constName! == expectedFn.constName!
+      && typeArgs.size == expectedArgs.size do
+    discard <| isDefEq type expectedType
+    return
+  unless (← isDefEq typeFn expectedFn) do
+    return
+  let (_, bis, _) ← forallMetaTelescope (← inferType typeFn)
+  for i in [:typeArgs.size] do
+    if i < bis.size && bis[i]!.isInstImplicit then
+      continue
+    discard <| isDefEq typeArgs[i]! expectedArgs[i]!
+
 @[builtin_term_elab Lean.Parser.Term.inferInstanceAs] def elabInferInstanceAs : TermElab := fun stx expectedType? => do
   -- The type argument is the last child (works for both `inferInstanceAs T` and `inferInstanceAs <| T`)
   let typeStx := stx[stx.getNumArgs - 1]!
@@ -363,7 +399,7 @@ private def resynthInstImplicitArgs (type : Expr) : TermElabM Expr := do
   let type ← withSynthesize do
     let type ← elabType typeStx
     -- Unify with expected type to resolve metavariables (e.g., `_` placeholders)
-    discard <| isDefEq type expectedType
+    unifyTypeForInferInstanceAs type expectedType
     return type
   -- Re-infer instance-implicit args, so that synthesis is not influenced by the expected type's
   -- instance choices.
diff --git a/tests/elab/inferInstanceAs2.lean b/tests/elab/inferInstanceAs2.lean
new file mode 100644
index 000000000000..2b417f1bdb0d
--- /dev/null
+++ b/tests/elab/inferInstanceAs2.lean
@@ -0,0 +1,39 @@
+/-!
+Tests for `inferInstanceAs` against expected types whose explicit arguments wrap a
+non-reducible defined type (`Zmod n` here, which unfolds to `Nat ⧸ n`). User-placed
+`_` placeholders in the `inferInstanceAs` type argument must be resolved by matching
+against the expected type without getting blocked by the `.instances` transparency
+cap on synthetic instance metavariables.
+-/
+
+class HasQuotient (A : outParam <| Type u) (B : Type v) where
+  Quotient (A) : B → Type max u v
+
+notation:35 G " ⧸ " H:34 => HasQuotient.Quotient G H
+
+class Foo (α : Type) [Neg α] where
+
+instance {n : Nat} : Foo (Fin n) where
+
+instance : HasQuotient Nat Nat where
+  Quotient n := Fin n
+
+instance {n : Nat} : Neg (Nat ⧸ n) :=
+  inferInstanceAs <| Neg (Fin n)
+
+instance {n : Nat} : Foo (Nat ⧸ n) :=
+  inferInstanceAs <| Foo (Fin n)
+
+def Zmod (n : Nat) :=
+  Nat ⧸ n
+deriving Neg
+
+instance {n : Nat} : Foo (Zmod n) :=
+  inferInstanceAs <| Foo (_ ⧸ _)
+
+instance {n : Nat} : Foo (Zmod n) :=
+  inferInstanceAs <| Foo (Nat ⧸ n)
+
+set_option backward.isDefEq.respectTransparency.instances false in
+instance {n : Nat} : Foo (Zmod n) :=
+  inferInstanceAs <| Foo (_ ⧸ _)

From 8e04897322c04a3cec3bec3d81595f858c7cc4ae Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Tue, 11 Aug 2026 07:33:45 +0000
Subject: [PATCH 06/16] fixes for stage2

---
 src/Lean/Environment.lean                | 2 ++
 src/Std/Time/Format/Basic.lean           | 1 +
 src/Std/Time/Zoned/Database/PosixTz.lean | 1 +
 3 files changed, 4 insertions(+)

diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index 7acba898530b..446900430e48 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -2301,6 +2301,8 @@ where
       p := body
     p.isProp
 
+set_option allowUnsafeReducibility true in
+attribute [local instance_reducible] Id in
 /--
 Constructs environment from `importModulesCore` results.
 
diff --git a/src/Std/Time/Format/Basic.lean b/src/Std/Time/Format/Basic.lean
index 312a918fdd2e..3988d5bccdc0 100644
--- a/src/Std/Time/Format/Basic.lean
+++ b/src/Std/Time/Format/Basic.lean
@@ -731,6 +731,7 @@ private def parseOffset (withMinutes : Reason) (withSeconds : Reason) (withColon
 
   return Offset.ofSeconds ⟨hours.val * sign⟩
 
+set_option backward.isDefEq.respectTransparency false in
 private def parseWith (config : FormatConfig) : (mod : Modifier) → Parser (TypeFormat mod)
   | .G format =>
     match format with
diff --git a/src/Std/Time/Zoned/Database/PosixTz.lean b/src/Std/Time/Zoned/Database/PosixTz.lean
index 1fe9328ca6cd..b568a35bec46 100644
--- a/src/Std/Time/Zoned/Database/PosixTz.lean
+++ b/src/Std/Time/Zoned/Database/PosixTz.lean
@@ -36,6 +36,7 @@ private def posixParseSign : Parser Int :=
   <|> attempt (pchar '+' *> pure 1)
   <|> pure 1
 
+set_option backward.isDefEq.respectTransparency false in
 -- <time> ::= <hour> [":" <minute> [":" <second>]]
 -- `maxHour` caps the hour field; POSIX requires 0–24, extended mode allows 0–167.
 private def posixParseHMS (maxHour : Nat := 24) : Parser Second.Offset := do

From a2d3c7bb84e0773e32a4501e63ea564bb80bb9e4 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Thu, 13 Aug 2026 13:15:53 +0000
Subject: [PATCH 07/16] mark-or-synth strategy

---
 src/Init/WF.lean                              |  2 +-
 src/Lean/Meta/ExprDefEq.lean                  | 24 ++++++++++++++++---
 src/Lean/Server/CodeActions/Provider.lean     |  2 +-
 .../LRAT/Internal/Formula/RatAddSound.lean    |  2 +-
 4 files changed, 24 insertions(+), 6 deletions(-)

diff --git a/src/Init/WF.lean b/src/Init/WF.lean
index 1d0216ed49d1..87ae4267a137 100644
--- a/src/Init/WF.lean
+++ b/src/Init/WF.lean
@@ -523,7 +523,7 @@ The `wfParam` gadget is used internally during the construction of recursive fun
 wellfounded recursion, to keep track of the parameter for which the automatic introduction
 of `List.attach` (or similar) is plausible.
 -/
-@[implicit_reducible] def wfParam {α : Sort u} (a : α) : α := a
+@[instance_reducible] def wfParam {α : Sort u} (a : α) : α := a
 
 /--
 Reverse direction of `dite_eq_ite`. Used by the well-founded definition preprocessor to extend the
diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index f92b14615d8d..6cdc9bd0d12d 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -699,9 +699,13 @@ private def checkTypesAndAssign (mvar : Expr) (v : Expr) : MetaM Bool :=
             pure (← isClass? mvarType).isSome
           else
             pure false
-        let capInstance (x : MetaM Bool) : MetaM Bool :=
-          if isInstance then withTransparency .instances x else x
-        capInstance <| withImplicitConfig do
+        if isInstance then
+          -- TODO: spine analysis
+          if (← checkTypesForInstanceTypedMVarAssignment mvarType vType v) then
+            mvar.mvarId!.assign v
+            return true
+          synthInstanceTypedMVarAndUnify mvar v
+        else withImplicitConfig do
           if (← Meta.isExprDefEqAux mvarType vType) then
             mvar.mvarId!.assign v
             return true
@@ -710,6 +714,20 @@ private def checkTypesAndAssign (mvar : Expr) (v : Expr) : MetaM Bool :=
               if (← Meta.isExprDefEqAux mvarType vType) then
                 trace[diagnostics] "failure when assigning metavariable with type{indentExpr mvarType}\nwhich is not definitionally equal to{indentExpr vType}\nwhen using `.implicit` transparency, but it is with `.default`.\nWorkaround: `set_option backward.isDefEq.respectTransparency.types false`"
             return false
+        -- let withCorrectTransparency (x : MetaM Bool) : MetaM Bool :=
+        --   if isInstance then withExactInstancesConfig x else withImplicitConfig x
+        -- -- withCorrectTransparency do
+        -- if (← withCorrectTransparency <| Meta.isExprDefEqAux mvarType vType) then
+        --   mvar.mvarId!.assign v
+        --   return true
+        -- else
+        --   if isInstance then
+        --     synthInstanceTypedMVarAndUnify mvar v
+        --   else
+        --     if (← isDiagnosticsEnabled) then withInferTypeConfig do
+        --       if (← Meta.isExprDefEqAux mvarType vType) then
+        --         trace[diagnostics] "failure when assigning metavariable with type{indentExpr mvarType}\nwhich is not definitionally equal to{indentExpr vType}\nwhen using `.implicit` transparency, but it is with `.default`.\nWorkaround: `set_option backward.isDefEq.respectTransparency.types false`"
+        --     return false
       else
         withInferTypeConfig do
           if (← Meta.isExprDefEqAux mvarType vType) then
diff --git a/src/Lean/Server/CodeActions/Provider.lean b/src/Lean/Server/CodeActions/Provider.lean
index 91f4f795bbbc..8b7dd7e38e39 100644
--- a/src/Lean/Server/CodeActions/Provider.lean
+++ b/src/Lean/Server/CodeActions/Provider.lean
@@ -120,7 +120,7 @@ where
             if let some pos' := stx[2*i].getPos? then
               if range.stop < pos' then
                 return i
-          (stx.getNumArgs + 1) / 2
+          pure <| (stx.getNumArgs + 1) / 2
         .tacticSeq (bracket || preferred pos) i ((stx, 0) :: stack)
       let mut childRes := none
       for i in (*...stx.getNumArgs).iter.stepSize 2 do
diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean
index 85a826d5cbc1..303b3684b4bc 100644
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean
@@ -418,7 +418,7 @@ theorem existsRatHint_of_ratHintsExhaustive {n : Nat} (f : DefaultFormula n)
   have i_in_bounds : i < Array.size (Array.range (Array.size f.clauses)) := by grind
   have i_lt_f_clauses_size : i < f.clauses.size := by grind
   have h : i ∈ (ratHints.map (fun x => x.1)).toList := by
-    simp only [← of_decide_eq_true_forward ratHintsExhaustive_eq_true]
+    simp only [← of_decide_eq_true ratHintsExhaustive_eq_true]
     have i_eq_range_i : i = (Array.range f.clauses.size)[i]'i_in_bounds := by grind
     rw [i_eq_range_i]
     rw [Array.mem_toList_iff]

From 0ef0c6997e6ce4b6c3978c3824f563d871cbd0f3 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Fri, 14 Aug 2026 13:22:32 +0000
Subject: [PATCH 08/16] synthetic auxMVars

---
 src/Lean/Meta/ExprDefEq.lean | 69 +++++++++++++++++++++++-------------
 src/Lean/MetavarContext.lean |  2 ++
 2 files changed, 47 insertions(+), 24 deletions(-)

diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index 6cdc9bd0d12d..e7e9ab9c0381 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -566,11 +566,30 @@ abbrev respectTransparencyAtTypes : CoreM Bool := do
   let opts ← getOptions
   return backward.isDefEq.respectTransparency.types.get opts && backward.isDefEq.respectTransparency.get opts
 
+/--
+Returns `true` if `mvarId` is an instance metavariable — created for an instance-implicit (`[..]`)
+parameter, identified by `.synthetic` kind together with a class type.
+
+Assignments to these are checked at exactly `.instances` transparency, so an ambient
+`.default`/`.all` does not let semireducible definitions be unfolded while checking the type of an
+instance assignment. This intentionally does not apply to ordinary implicit (`{..}`) metavariables
+that happen to have a class type, which are created with `.natural` kind.
+-/
+private def isInstanceMVar (mvarId : MVarId) : MetaM Bool := do
+  unless (← respectTransparencyAtTypes) &&
+      backward.isDefEq.respectTransparency.instances.get (← getOptions) do
+    return false
+  unless (← mvarId.getKind) matches .synthetic do return false
+  return (← isClass? (← mvarId.getDecl).type).isSome
+
 /--
 Returns `true` if all metavariables whose types influence the type of `e`, a value assigned to an
-instance-typed metavariable unter `backward.isDefEq.respectTransparency.instanceSearchTypes`, are admissible. Admissible are:
+instance-typed metavariable unter `backward.isDefEq.respectTransparency.instanceSearchTypes`, are admissible.
+Admissible are:
 
-* instance-typed metavariables: their own assignments are subject to the same restriction;
+* metavariables whose own assignments are subject to the same restriction: instance-typed ones
+  (spawned by instance search, see `backward.isDefEq.instanceTypes`) and instance metavariables
+  (see `isInstanceMVar`);
 * metavariables `isDefEq` cannot assign (from an outer `MetavarContext` depth, or synthetic
   opaque): the current instance search cannot commit them to a wrong-typed value, and their
   eventual assignment is governed by whoever created them.
@@ -600,8 +619,12 @@ where
     | .mvar mvarId =>
       if let some d ← getDelayedMVarAssignment? mvarId then
         go (mkMVar d.mvarIdPending)
+      else if (← mvarId.isReadOnlyOrSyntheticOpaque) then
+        return true
+      else if (← mvarId.isInstanceTyped) then
+        return backward.isDefEq.instanceTypes.get (← getOptions)
       else
-        mvarId.isInstanceTyped <||> mvarId.isReadOnlyOrSyntheticOpaque
+        isInstanceMVar mvarId
     | .app f _ => go f
     | .lam _ _ b _ => go b
     | .letE _ _ v b _ => go v <&&> go b
@@ -687,23 +710,11 @@ private def checkTypesAndAssign (mvar : Expr) (v : Expr) : MetaM Bool :=
       let mvarType ← inferType mvar
       let vType ← inferType v
       if (← respectTransparencyAtTypes) then
-        -- For instance metavariables — those created for an instance-implicit (`[..]`) parameter,
-        -- identified by `.synthetic` kind together with a class type — cap the transparency at
-        -- exactly `.instances` so an ambient `.default`/`.all` does not let semireducible
-        -- definitions be unfolded while checking the type of an instance assignment. This
-        -- intentionally does not apply to ordinary implicit (`{..}`) metavariables that happen
-        -- to have a class type, which are created with `.natural` kind.
-        let isInstance ←
-          if backward.isDefEq.respectTransparency.instances.get (← getOptions) &&
-              (← mvar.mvarId!.getKind) matches .synthetic then
-            pure (← isClass? mvarType).isSome
-          else
-            pure false
-        if isInstance then
-          -- TODO: spine analysis
-          if (← checkTypesForInstanceTypedMVarAssignment mvarType vType v) then
-            mvar.mvarId!.assign v
-            return true
+        if (← isInstanceMVar mvar.mvarId!) then
+          if (← spineMVarsAdmissible v) then
+            if (← checkTypesForInstanceTypedMVarAssignment mvarType vType v) then
+              mvar.mvarId!.assign v
+              return true
           synthInstanceTypedMVarAndUnify mvar v
         else withImplicitConfig do
           if (← Meta.isExprDefEqAux mvarType vType) then
@@ -1017,8 +1028,9 @@ where
      how many metavariable arguments are representing dependencies.
 -/
 
-def mkAuxMVar (lctx : LocalContext) (localInsts : LocalInstances) (type : Expr) (numScopeArgs : Nat := 0) : MetaM Expr := do
-  mkFreshExprMVarAt lctx localInsts type MetavarKind.natural Name.anonymous numScopeArgs
+def mkAuxMVar (lctx : LocalContext) (localInsts : LocalInstances) (type : Expr) (numScopeArgs : Nat := 0)
+    (kind : MetavarKind := .natural) : MetaM Expr := do
+  mkFreshExprMVarAt lctx localInsts type kind Name.anonymous numScopeArgs
 
 namespace CheckAssignment
 
@@ -1153,7 +1165,10 @@ mutual
     /- Compute new set of local instances. -/
     let localInsts := mvarDecl.localInstances.filter fun localInst => !toErase.contains localInst.fvar.fvarId!
     let mvarType ← check mvarDecl.type
-    let newMVar ← mkAuxMVar lctx localInsts mvarType mvarDecl.numScopeArgs
+    -- `newMVar` stands for `mvarId`, so restrictions on its assignments must carry over
+    let newMVar ← mkAuxMVar lctx localInsts mvarType mvarDecl.numScopeArgs (kind := mvarDecl.kind)
+    if (← mvarId.isInstanceTyped) then
+      newMVar.mvarId!.markInstanceTyped
     mvarId.assign newMVar
     return newMVar
 
@@ -1195,6 +1210,9 @@ mutual
                Note that `mvarType` may be different from `eType`. -/
             let ctx ← read
             let newMVar ← mkAuxMVar ctx.mvarDecl.lctx ctx.mvarDecl.localInstances mvarType
+              (kind := (← f.mvarId!.getDecl).kind)
+            if (← f.mvarId!.isInstanceTyped) then
+              newMVar.mvarId!.markInstanceTyped
             if (← assignToConstFun f args.size newMVar) then
               pure newMVar
             else
@@ -2019,7 +2037,10 @@ private def isDefEqMVarSelf (mvar : Expr) (args₁ args₂ : Array Expr) : MetaM
     let mvarDecl ← mvarId.getDecl
     if mvarDecl.numScopeArgs == args₁.size || cfg.constApprox then
       let type ← inferType (mkAppN mvar args₁)
-      let auxMVar ← mkAuxMVar mvarDecl.lctx mvarDecl.localInstances type
+      -- `auxMVar` stands for `mvarId`, so restrictions on its assignments must carry over
+      let auxMVar ← mkAuxMVar mvarDecl.lctx mvarDecl.localInstances type (kind := mvarDecl.kind)
+      if (← mvarId.isInstanceTyped) then
+        auxMVar.mvarId!.markInstanceTyped
       assignConst mvar args₁.size auxMVar
     else
       pure false
diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean
index 4a11d8b1b83d..e47937fb35d0 100644
--- a/src/Lean/MetavarContext.lean
+++ b/src/Lean/MetavarContext.lean
@@ -1235,6 +1235,8 @@ mutual
           mctx := s.mctx.addExprMVarDecl newMVarId Name.anonymous newMVarLCtx newLocalInsts newMVarType newMVarKind numScopeArgs,
           ngen := s.ngen.next
         }
+      if (← mvarId.isInstanceTyped) then
+        newMVarId.markInstanceTyped
       if !mvarDecl.kind.isSyntheticOpaque then
         mvarId.assign result
       else

From bbc4f826579bc9099e554eef54dfa7e017ec8607 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Fri, 14 Aug 2026 17:32:32 +0200
Subject: [PATCH 09/16] clean up Lean.Environment

---
 src/Lean/Environment.lean | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index 446900430e48..03f938f66bf1 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -2301,8 +2301,6 @@ where
       p := body
     p.isProp
 
-set_option allowUnsafeReducibility true in
-attribute [local instance_reducible] Id in
 /--
 Constructs environment from `importModulesCore` results.
 
@@ -2329,7 +2327,8 @@ def finalizeImport (s : ImportState) (imports : Array Import) (opts : Options) (
   let numPublicConsts := modules.foldl (init := 0) fun numPublicConsts mod => Id.run do
     if !mod.isExported then numPublicConsts else
       let some data := mod.publicModule? | numPublicConsts
-      numPublicConsts + data.constants.size
+      -- binop issue: can't synthesize `HAdd Nat Nat (Id Nat)`; solved using `pure`
+      pure <| numPublicConsts + data.constants.size
   let mut const2ModIdx : Std.HashMap Name ModuleIdx := Std.HashMap.emptyWithCapacity (capacity := numPrivateConsts + numExtraConsts)
   let mut privateConstantMap : Std.HashMap Name ConstantInfo := Std.HashMap.emptyWithCapacity (capacity := numPrivateConsts)
   let mut publicConstantMap : Std.HashMap Name ConstantInfo := Std.HashMap.emptyWithCapacity (capacity := numPublicConsts)

From cc7922e35163493e7501c357a8f4e0203a60ed0a Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Tue, 18 Aug 2026 11:21:24 +0200
Subject: [PATCH 10/16] respectTransparency.outParams disabled by default;
 respectTransparency.instances enabled even if respectTransparency.types is
 disabled

---
 src/Lean/Meta/ExprDefEq.lean     | 41 ++++++++++++++++----------------
 src/Lean/Meta/SynthInstance.lean |  2 +-
 2 files changed, 21 insertions(+), 22 deletions(-)

diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index e7e9ab9c0381..cc616ee5b4d3 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -576,20 +576,19 @@ instance assignment. This intentionally does not apply to ordinary implicit (`{.
 that happen to have a class type, which are created with `.natural` kind.
 -/
 private def isInstanceMVar (mvarId : MVarId) : MetaM Bool := do
-  unless (← respectTransparencyAtTypes) &&
-      backward.isDefEq.respectTransparency.instances.get (← getOptions) do
+  unless backward.isDefEq.respectTransparency.instances.get (← getOptions) do
     return false
   unless (← mvarId.getKind) matches .synthetic do return false
   return (← isClass? (← mvarId.getDecl).type).isSome
 
 /--
 Returns `true` if all metavariables whose types influence the type of `e`, a value assigned to an
-instance-typed metavariable unter `backward.isDefEq.respectTransparency.instanceSearchTypes`, are admissible.
-Admissible are:
+instance-typed metavariable unter `backward.isDefEq.respectTransparency.instanceSearchTypes`, are
+admissible. Admissible are:
 
 * metavariables whose own assignments are subject to the same restriction: instance-typed ones
-  (spawned by instance search, see `backward.isDefEq.instanceTypes`) and instance metavariables
-  (see `isInstanceMVar`);
+  (spawned by instance search, see `backward.isDefEq.respectTransparency.instanceSearchTypes`) and
+  instance metavariables (see `isInstanceMVar`);
 * metavariables `isDefEq` cannot assign (from an outer `MetavarContext` depth, or synthetic
   opaque): the current instance search cannot commit them to a wrong-typed value, and their
   eventual assignment is governed by whoever created them.
@@ -622,7 +621,7 @@ where
       else if (← mvarId.isReadOnlyOrSyntheticOpaque) then
         return true
       else if (← mvarId.isInstanceTyped) then
-        return backward.isDefEq.instanceTypes.get (← getOptions)
+        return backward.isDefEq.respectTransparency.instanceSearchTypes.get (← getOptions)
       else
         isInstanceMVar mvarId
     | .app f _ => go f
@@ -709,22 +708,22 @@ private def checkTypesAndAssign (mvar : Expr) (v : Expr) : MetaM Bool :=
       -- must check whether types are definitionally equal or not, before assigning and returning true
       let mvarType ← inferType mvar
       let vType ← inferType v
-      if (← respectTransparencyAtTypes) then
-        if (← isInstanceMVar mvar.mvarId!) then
-          if (← spineMVarsAdmissible v) then
-            if (← checkTypesForInstanceTypedMVarAssignment mvarType vType v) then
-              mvar.mvarId!.assign v
-              return true
-          synthInstanceTypedMVarAndUnify mvar v
-        else withImplicitConfig do
-          if (← Meta.isExprDefEqAux mvarType vType) then
+      if (← isInstanceMVar mvar.mvarId!) then
+        if (← spineMVarsAdmissible v) then
+          if (← checkTypesForInstanceTypedMVarAssignment mvarType vType v) then
             mvar.mvarId!.assign v
             return true
-          else
-            if (← isDiagnosticsEnabled) then withInferTypeConfig do
-              if (← Meta.isExprDefEqAux mvarType vType) then
-                trace[diagnostics] "failure when assigning metavariable with type{indentExpr mvarType}\nwhich is not definitionally equal to{indentExpr vType}\nwhen using `.implicit` transparency, but it is with `.default`.\nWorkaround: `set_option backward.isDefEq.respectTransparency.types false`"
-            return false
+        synthInstanceTypedMVarAndUnify mvar v
+      else if (← respectTransparencyAtTypes) then
+        withImplicitConfig do
+        if (← Meta.isExprDefEqAux mvarType vType) then
+          mvar.mvarId!.assign v
+          return true
+        else
+          if (← isDiagnosticsEnabled) then withInferTypeConfig do
+            if (← Meta.isExprDefEqAux mvarType vType) then
+              trace[diagnostics] "failure when assigning metavariable with type{indentExpr mvarType}\nwhich is not definitionally equal to{indentExpr vType}\nwhen using `.implicit` transparency, but it is with `.default`.\nWorkaround: `set_option backward.isDefEq.respectTransparency.types false`"
+          return false
         -- let withCorrectTransparency (x : MetaM Bool) : MetaM Bool :=
         --   if isInstance then withExactInstancesConfig x else withImplicitConfig x
         -- -- withCorrectTransparency do
diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean
index abffcbf2dc7e..1e0983ac4f9a 100644
--- a/src/Lean/Meta/SynthInstance.lean
+++ b/src/Lean/Meta/SynthInstance.lean
@@ -48,7 +48,7 @@ during the outParam check.
 See `assignOutParams` for the implementation.
 -/
 register_builtin_option backward.isDefEq.respectTransparency.outParams : Bool := {
-  defValue := true
+  defValue := false
   descr    := "if true (the default), do not bump transparency to `.default` \
   when checking that a synthesized instance's type matches the original goal type \
   for classes with `outParam`s"

From 7dd284a06a5bced4df5d897219faab7b6fba6794 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Thu, 20 Aug 2026 12:58:13 +0000
Subject: [PATCH 11/16] instance linter

---
 src/Lean/Linter/TacticTypeCheck.lean       | 74 +++++++++++++---------
 src/Lean/Meta/Check.lean                   | 57 +++++++++++++++++
 tests/elab/linterTacticCheckInstances.lean | 59 +++++++++++++++++
 3 files changed, 161 insertions(+), 29 deletions(-)

diff --git a/src/Lean/Linter/TacticTypeCheck.lean b/src/Lean/Linter/TacticTypeCheck.lean
index c1e0228870ad..de6e094b52d3 100644
--- a/src/Lean/Linter/TacticTypeCheck.lean
+++ b/src/Lean/Linter/TacticTypeCheck.lean
@@ -17,16 +17,24 @@ open Lean Elab Command
 open Lean.Linter (logLint)
 
 /--
-Warn when the goal target is not type-correct at `.implicit` 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.
+Warn when the goal target is not type-correct at `.implicit` transparency, or when it contains an
+instance argument that only has the expected type above `.instances` transparency.
+
+The former happens when e.g. `unfold` leaves hypotheses whose types still refer to the pre-unfolded
+definition, preventing `rw`/`simp` from matching patterns. The latter happens when e.g. an `rfl`
+lemma rewrites a value without updating the instances mentioning it, preventing `rw`/`simp` from
+unifying the instance argument.
 -/
 register_builtin_option linter.tacticCheckInstances : Bool := {
   defValue := false
-  descr := "enable the linter that type-checks every tactic goal at `.implicit` transparency"
+  descr := "enable the linter that type-checks every tactic goal at `.implicit` transparency and \
+    checks its instance arguments at `.instances` transparency"
 }
 
-/-- A linter that runs `Meta.check _ .implicit` on every tactic goal. -/
+/--
+A linter that runs `Meta.check _ .implicit` and `Meta.findInstanceArgMismatch?` on every tactic
+goal.
+-/
 def tacticCheckInstances : Linter where
   run _cmdStx := do
     -- Do *not* check `linter.all` here, this linter is purely for debugging
@@ -56,7 +64,8 @@ def tacticCheckInstances : Linter where
         -- `.implicit` check fails, the defs unfolded at `.default` but not at
         -- `.implicit` are the candidates for `@[implicit_reducible]` and get
         -- reported to the user. The pattern mirrors `mkUnfoldAxiomsNote` in
-        -- `Lean.Meta.Check`.
+        -- `Lean.Meta.Check`. If it succeeds, we look for instance arguments
+        -- that stop matching one transparency level down.
         -- `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).
@@ -74,30 +83,37 @@ def tacticCheckInstances : Linter where
             let counterDefault := (← get).diag.unfoldCounter
             -- Reset and try at `.implicit`.
             modify ({ · with diag := origDiag })
-            try
-              Meta.check target .implicit
+            let implicitError? : Option Exception ←
+              try Meta.check target .implicit; pure none catch e => pure (some e)
+            let some e := implicitError? | do
+              -- Type-correct at `.implicit`, but `simp`/`rw` unify instance-implicit arguments at
+              -- `.instances`, where an argument left behind by an earlier rewrite may no longer
+              -- match.
+              let some msg ← Meta.findInstanceArgMismatch? target | return none
+              return some m!"{kind} tactic goal contains an instance argument whose type does \
+                not match at `.instances` transparency; `simp` and `rw` unify instance-implicit \
+                arguments at that transparency, so lemmas mentioning this instance will fail to \
+                apply:{indentD msg}"
+            let counterInst := (← get).diag.unfoldCounter
+            let diff := Meta.subCounters counterDefault 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
-            catch e =>
-              let counterInst := (← get).diag.unfoldCounter
-              let diff := Meta.subCounters counterDefault 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 \
-                `.implicit` transparency; {remedy} some of the following as \
-                `@[implicit_reducible]`:\
-                {indentD (.joinSep candidates Format.line)}\n\
-                Full error:\
-                {indentD e.toMessageData}"
+            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 \
+              `.implicit` transparency; {remedy} some of the following as \
+              `@[implicit_reducible]`:\
+              {indentD (.joinSep candidates Format.line)}\n\
+              Full error:\
+              {indentD e.toMessageData}"
           -- Always restore the original diagnostics snapshot.
           modify ({ · with diag := origDiag })
           return result
diff --git a/src/Lean/Meta/Check.lean b/src/Lean/Meta/Check.lean
index 3796de18422b..b8d1356f493f 100644
--- a/src/Lean/Meta/Check.lean
+++ b/src/Lean/Meta/Check.lean
@@ -337,6 +337,63 @@ def check (e : Expr) (transparency : TransparencyMode := .all) : MetaM Unit :=
       trace[Meta.check] ex.toMessageData
       throw ex
 
+/--
+Describes the first application in `e` whose instance-implicit argument has the expected type at
+`.implicit` transparency but not at `.instances`, if there is one.
+
+`check e .implicit` accepts such an application, but `simp` and `rw` unify instance-implicit
+arguments at `.instances`, so a lemma mentioning the instance still fails to apply. This state
+typically arises when an `rfl` lemma rewrites a value without updating the instances mentioning it.
+-/
+partial def findInstanceArgMismatch? (e : Expr) : MetaM (Option MessageData) :=
+  withDefault <| visit e |>.run
+where
+  visit (e : Expr) : MonadCacheT ExprStructEq (Option MessageData) MetaM (Option MessageData) :=
+    checkCache { val := e : ExprStructEq } fun _ => do
+      match e with
+      | .forallE ..      => visitForall e
+      | .lam ..          => visitLambdaLet e
+      | .letE ..         => visitLambdaLet e
+      | .app f a         =>
+        if let some msg ← visit f then return some msg
+        if let some msg ← visit a then return some msg
+        visitApp f a
+      | .mdata _ e       => visit e
+      | .proj _ _ e      => visit e
+      | _                => return none
+
+  visitApp (f a : Expr) : MetaM (Option MessageData) := do
+    let (expectedType, binfo) ← try getFunctionDomain f catch _ => return none
+    unless binfo.isInstImplicit do return none
+    let aType ← try inferType a catch _ => return none
+    let defEqAt (transparency : TransparencyMode) : MetaM Bool :=
+      withoutModifyingState <| withTransparency transparency <| isDefEqGuarded expectedType aType
+    if (← defEqAt .instances) then return none
+    -- A mismatch that persists at `.implicit` is an outright type error, which `check e .implicit`
+    -- reports with more context.
+    unless (← defEqAt .implicit) do return none
+    let app := (mkApp f a).setAppPPExplicit
+    addMessageContext m!"The instance argument{indentExpr a}\n\
+      {← mkHasTypeButIsExpectedMsg aType expectedType
+        (trailing? := m!"in the application{indentExpr app}") (trailingExprs := #[app])}"
+
+  visitLambdaLet (e : Expr) : MonadCacheT ExprStructEq (Option MessageData) MetaM (Option MessageData) :=
+    lambdaLetTelescope e fun xs b => do
+      for x in xs do
+        match ← getFVarLocalDecl x with
+        | .cdecl (type := t) .. =>
+          if let some msg ← visit t then return some msg
+        | .ldecl (type := t) (value := v) .. =>
+          if let some msg ← visit t then return some msg
+          if let some msg ← visit v then return some msg
+      visit b
+
+  visitForall (e : Expr) : MonadCacheT ExprStructEq (Option MessageData) MetaM (Option MessageData) :=
+    forallTelescope e fun xs b => do
+      for x in xs do
+        if let some msg ← visit (← getFVarLocalDecl x).type then return some msg
+      visit b
+
 /--
 Runs `x` and, on any error, lazily checks whether `e` is type-correct at `instances` transparency.
 If not, appends an explanatory note to the error message.
diff --git a/tests/elab/linterTacticCheckInstances.lean b/tests/elab/linterTacticCheckInstances.lean
index 7ce96726dc46..85c5df095b0a 100644
--- a/tests/elab/linterTacticCheckInstances.lean
+++ b/tests/elab/linterTacticCheckInstances.lean
@@ -74,3 +74,62 @@ Note: This linter can be disabled with `set_option linter.tacticCheckInstances f
 example (s : S) (a b idx : Nat) (h1 : idx < s.decls.size) :
     (composed s a b).s.decls[idx] = s.decls[idx] := by
   rfl
+
+/-!
+The goal below is type-correct at `.implicit` transparency (`natZero` is `@[implicit_reducible]`,
+so `X natZero` and `X 0` are defeq there), but `simp`/`rw` unify instance-implicit arguments at
+`.instances`, where they are not. The linter reports the stale instance argument that
+`simp only [natZero_def]` left behind.
+-/
+
+class X (n : Nat)
+
+@[implicit_reducible]
+def natZero := 0
+
+instance instXNatZero : X natZero where
+
+theorem natZero_def : natZero = 0 := rfl
+
+def g (n : Nat) [X n] : Nat := n + 1
+
+theorem g_eq {n} [X n] : g n = n + 1 := by
+  simp [g]
+
+/--
+@ +1:27...+2:31
+error: unsolved goals
+⊢ g 0 = 1
+---
+@ +2:2...31
+warning: produced tactic goal contains an instance argument whose type does not match at `.instances` transparency; `simp` and `rw` unify instance-implicit arguments at that transparency, so lemmas mentioning this instance will fail to apply:
+  The instance argument
+    instXNatZero
+  has type
+    X natZero
+  but is expected to have type
+    X 0
+  in the application
+    @g 0 instXNatZero
+
+Note: This linter can be disabled with `set_option linter.tacticCheckInstances false`
+-/
+#guard_msgs (positions := true) in
+example : g natZero = 1 := by
+  simp only [natZero_def, g_eq]
+
+/-!
+The mismatch has to survive down to `.instances` transparency: with an `@[instance_reducible]`
+value the instance argument still matches there, so `g_eq` applies and the linter stays quiet.
+-/
+
+@[instance_reducible]
+def natZeroI := 0
+
+instance instXNatZeroI : X natZeroI where
+
+theorem natZeroI_def : natZeroI = 0 := rfl
+
+#guard_msgs in
+example : g natZeroI = 1 := by
+  simp only [natZeroI_def, g_eq]

From 275bacf9ec1ae45f1948e00b1395fef3a8d6c918 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Thu, 20 Aug 2026 13:50:52 +0000
Subject: [PATCH 12/16] simp-splitting warnings

---
 src/Lean/Linter/TacticTypeCheck.lean       | 31 ++++---
 src/Lean/Meta/Check.lean                   | 22 +++++
 src/Lean/Meta/Tactic/Simp/Main.lean        | 34 +++++++-
 src/Lean/Meta/Tactic/Simp/Types.lean       | 14 +++-
 tests/elab/linterTacticCheckInstances.lean | 94 +++++++++++++++++++---
 5 files changed, 167 insertions(+), 28 deletions(-)

diff --git a/src/Lean/Linter/TacticTypeCheck.lean b/src/Lean/Linter/TacticTypeCheck.lean
index de6e094b52d3..7fe9d1ba588c 100644
--- a/src/Lean/Linter/TacticTypeCheck.lean
+++ b/src/Lean/Linter/TacticTypeCheck.lean
@@ -17,19 +17,14 @@ open Lean Elab Command
 open Lean.Linter (logLint)
 
 /--
-Warn when the goal target is not type-correct at `.implicit` transparency, or when it contains an
-instance argument that only has the expected type above `.instances` transparency.
-
-The former happens when e.g. `unfold` leaves hypotheses whose types still refer to the pre-unfolded
-definition, preventing `rw`/`simp` from matching patterns. The latter happens when e.g. an `rfl`
-lemma rewrites a value without updating the instances mentioning it, preventing `rw`/`simp` from
-unifying the instance argument.
+Whether a `linter.tacticCheckInstances` warning has already been logged for this command, e.g. by
+`simp` checking its own intermediate results while the command was elaborated.
 -/
-register_builtin_option linter.tacticCheckInstances : Bool := {
-  defValue := false
-  descr := "enable the linter that type-checks every tactic goal at `.implicit` transparency and \
-    checks its instance arguments at `.instances` transparency"
-}
+private def alreadyReported : CommandElabM Bool := do
+  -- `Command.State.messages` is reset per command, but by the time linters run its messages have
+  -- been marked reported, which `MessageLog.toList` does not return.
+  return (← get).messages.reportedPlusUnreported.any
+    (·.data.hasTag (· == linter.tacticCheckInstances.name))
 
 /--
 A linter that runs `Meta.check _ .implicit` and `Meta.findInstanceArgMismatch?` on every tactic
@@ -43,8 +38,10 @@ def tacticCheckInstances : Linter where
     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
-    let warned : IO.Ref Bool ← IO.mkRef false
+    -- steps. `simp` runs the same instance-argument check on its intermediate
+    -- results during elaboration, so start out suppressed if it already
+    -- reported one.
+    let warned : IO.Ref Bool ← IO.mkRef (← alreadyReported)
     for tree in infoTrees do
       -- `postNode` so children are visited before parents: leaf tactic infos
       -- (the actual user-written `unfold`, `rw`, ...) fire before the
@@ -90,9 +87,9 @@ def tacticCheckInstances : Linter where
               -- `.instances`, where an argument left behind by an earlier rewrite may no longer
               -- match.
               let some msg ← Meta.findInstanceArgMismatch? target | return none
-              return some m!"{kind} tactic goal contains an instance argument whose type does \
-                not match at `.instances` transparency; `simp` and `rw` unify instance-implicit \
-                arguments at that transparency, so lemmas mentioning this instance will fail to \
+              return some m!"The {kind} tactic goal has an instance argument whose type does not \
+                match at `.instances` transparency. `simp` and `rw` unify instance-implicit \
+                arguments at that transparency. Lemmas that mention this instance do not \
                 apply:{indentD msg}"
             let counterInst := (← get).diag.unfoldCounter
             let diff := Meta.subCounters counterDefault counterInst
diff --git a/src/Lean/Meta/Check.lean b/src/Lean/Meta/Check.lean
index b8d1356f493f..639dfa3d1c23 100644
--- a/src/Lean/Meta/Check.lean
+++ b/src/Lean/Meta/Check.lean
@@ -17,6 +17,28 @@ This is not the Kernel type checker, but an auxiliary method for checking
 whether terms produced by tactics and `isDefEq` are type correct.
 -/
 
+namespace Lean.Linter
+
+/--
+Warn when the goal target is not type-correct at `.implicit` transparency, or when it contains an
+instance argument that only has the expected type above `.instances` transparency.
+
+The former happens when e.g. `unfold` leaves hypotheses whose types still refer to the pre-unfolded
+definition, preventing `rw`/`simp` from matching patterns. The latter happens when e.g. an `rfl`
+lemma rewrites a value without updating the instances mentioning it, preventing `rw`/`simp` from
+unifying the instance argument.
+
+The option lives here rather than next to the linter in `Lean.Linter.TacticTypeCheck` because
+`simp` reads it too, to run `findInstanceArgMismatch?` on its intermediate results.
+-/
+register_builtin_option linter.tacticCheckInstances : Bool := {
+  defValue := false
+  descr := "enable the linter that type-checks every tactic goal at `.implicit` transparency and \
+    checks its instance arguments at `.instances` transparency"
+}
+
+end Lean.Linter
+
 namespace Lean.Meta
 
 private def ensureType (e : Expr) : MetaM Unit := do
diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean
index b648566cb9eb..c28b986fc2a5 100644
--- a/src/Lean/Meta/Tactic/Simp/Main.lean
+++ b/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.Linter.Init
 import Lean.Meta.HaveTelescope
 import Lean.PrettyPrinter
 import Lean.ExtraModUses
@@ -647,12 +648,43 @@ def congr (e : Expr) : SimpM Result := do
   else
     congrDefault e
 
+/--
+Report the first instance argument in `eNew` whose type stopped matching at `.instances`
+transparency, blaming the theorem that was applied most recently.
+
+`simp` reaches such a term when it rewrites a value an instance argument's type depends on without
+being able to rewrite the instance along with it, which leaves every later lemma about that
+instance inapplicable. The state is often transient — a later rewrite in the same `simp` call may
+remove it again — so the tactic goals the `tacticCheckInstances` linter inspects need not show any
+trace of it.
+-/
+private def reportInstanceArgMismatch (eNew : Expr) : SimpM Unit := do
+  let some msg ← (try findInstanceArgMismatch? eNew catch _ => pure none) | return
+  -- At most one report per command, and stop checking once we have one: the check is a full
+  -- traversal of every intermediate result.
+  modify fun s => { s with checkInstanceArgs := false }
+  let alreadyReported := (← Core.getMessageLog).reportedPlusUnreported.any
+    (·.data.hasTag (· == Linter.linter.tacticCheckInstances.name))
+  if alreadyReported then return
+  let rewrote ← match (← get).lastThm? with
+    | some thm => do pure m!"`simp` rewrote a term with {← ppOrigin thm}."
+    | none     => pure m!"`simp` rewrote a term."
+  Linter.logLint Linter.linter.tacticCheckInstances (← getRef)
+    m!"{rewrote} The new term has an instance argument whose type does not match at \
+      `.instances` transparency:{indentD msg}\n\
+      For the rest of this `simp` call, lemmas that mention this instance do not apply."
+
 def simpApp (e : Expr) : SimpM Result := do
   if isOfNatNatLit e || isOfScientificLit e || isCharLit e then
     -- Recall that we fold "orphan" kernel Nat literals `n` into `OfNat.ofNat n`
     return { expr := e }
   else
-    congr e
+    let r ← congr e
+    -- Check here rather than once per simplified subterm: congruence is what leaves an instance
+    -- argument behind, and a `post` rewrite may well repair the result before it is cached.
+    if (← get).checkInstanceArgs && r.expr != e then
+      reportInstanceArgMismatch r.expr
+    return r
 
 def simpStep (e : Expr) : SimpM Result := do
   match e with
diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean
index 478b7f82f24f..7bb3f60cd4e5 100644
--- a/src/Lean/Meta/Tactic/Simp/Types.lean
+++ b/src/Lean/Meta/Tactic/Simp/Types.lean
@@ -252,6 +252,14 @@ structure State where
   usedTheorems : UsedSimps := {}
   numSteps     : Nat := 0
   diag         : Diagnostics := {}
+  /--
+  Whether to check intermediate results for instance arguments that stopped matching at
+  `.instances` transparency. Set from `linter.tacticCheckInstances` by `SimpM.run`, and cleared
+  again once a mismatch has been reported: the linter reports at most one per command.
+  -/
+  checkInstanceArgs : Bool := false
+  /-- Theorem applied by the most recent rewrite; only tracked while `checkInstanceArgs` is set. -/
+  lastThm?     : Option Origin := none
 
 structure Stats where
   usedTheorems : UsedSimps := {}
@@ -308,7 +316,8 @@ opaque dsimp (e : Expr) : SimpM Expr
 
 @[inline] def modifyDiag (f : Diagnostics → Diagnostics) : SimpM Unit := do
   if (← isDiagnosticsEnabled) then
-    modify fun { cache, congrCache, dsimpCache, usedTheorems, numSteps, diag } => { cache, congrCache, dsimpCache, usedTheorems, numSteps, diag := f diag }
+    modify fun { cache, congrCache, dsimpCache, usedTheorems, numSteps, diag, checkInstanceArgs, lastThm? } =>
+      { cache, congrCache, dsimpCache, usedTheorems, numSteps, diag := f diag, checkInstanceArgs, lastThm? }
 
 /--
 Result type for a simplification procedure. We have `pre` and `post` simplification procedures.
@@ -524,6 +533,8 @@ def recordTriedSimpTheorem (thmId : Origin) : SimpM Unit := do
     { s with triedThmCounter := s.triedThmCounter.insert thmId cNew }
 
 def recordSimpTheorem (thmId : Origin) : SimpM Unit := do
+  if (← get).checkInstanceArgs then
+    modify fun s => { s with lastThm? := some thmId }
   modifyDiag fun s =>
     let cNew := if let some c := s.usedThmCounter.find? thmId then c + 1 else 1
     { s with usedThmCounter := s.usedThmCounter.insert thmId cNew }
@@ -990,6 +1001,7 @@ private def updateUsedSimpsWithZetaDelta (ctx : Context) (stats : Stats) : MetaM
 
 def SimpM.run (ctx : Context) (s : State := {}) (methods : Methods := {}) (k : SimpM α) : MetaM (α × State) := do
   let ctx ← ctx.setLctxInitIndices
+  let s := { s with checkInstanceArgs := Linter.linter.tacticCheckInstances.get (← getOptions) }
   withSimpContext ctx do
     let (r, s) ← k methods.toMethodsRef ctx |>.run s
     trace[Meta.Tactic.simp.numSteps] "{s.numSteps}"
diff --git a/tests/elab/linterTacticCheckInstances.lean b/tests/elab/linterTacticCheckInstances.lean
index 85c5df095b0a..1e21f78e0bd9 100644
--- a/tests/elab/linterTacticCheckInstances.lean
+++ b/tests/elab/linterTacticCheckInstances.lean
@@ -78,8 +78,8 @@ example (s : S) (a b idx : Nat) (h1 : idx < s.decls.size) :
 /-!
 The goal below is type-correct at `.implicit` transparency (`natZero` is `@[implicit_reducible]`,
 so `X natZero` and `X 0` are defeq there), but `simp`/`rw` unify instance-implicit arguments at
-`.instances`, where they are not. The linter reports the stale instance argument that
-`simp only [natZero_def]` left behind.
+`.instances`, where they are not. `simp` checks its own intermediate results, so it reports the
+stale instance argument that rewriting with `natZero_def` left behind, naming the lemma.
 -/
 
 class X (n : Nat)
@@ -91,18 +91,14 @@ instance instXNatZero : X natZero where
 
 theorem natZero_def : natZero = 0 := rfl
 
-def g (n : Nat) [X n] : Nat := n + 1
+def g (m : Nat) [X m] : Nat := m + 1
 
-theorem g_eq {n} [X n] : g n = n + 1 := by
+theorem g_eq {m} [X m] : g m = m + 1 := by
   simp [g]
 
 /--
-@ +1:27...+2:31
-error: unsolved goals
-⊢ g 0 = 1
----
 @ +2:2...31
-warning: produced tactic goal contains an instance argument whose type does not match at `.instances` transparency; `simp` and `rw` unify instance-implicit arguments at that transparency, so lemmas mentioning this instance will fail to apply:
+warning: `simp` rewrote a term with natZero_def. The new term has an instance argument whose type does not match at `.instances` transparency:
   The instance argument
     instXNatZero
   has type
@@ -111,8 +107,13 @@ warning: produced tactic goal contains an instance argument whose type does not
     X 0
   in the application
     @g 0 instXNatZero
+For the rest of this `simp` call, lemmas that mention this instance do not apply.
 
 Note: This linter can be disabled with `set_option linter.tacticCheckInstances false`
+---
+@ +1:27...+2:31
+error: unsolved goals
+⊢ g 0 = 1
 -/
 #guard_msgs (positions := true) in
 example : g natZero = 1 := by
@@ -133,3 +134,78 @@ theorem natZeroI_def : natZeroI = 0 := rfl
 #guard_msgs in
 example : g natZeroI = 1 := by
   simp only [natZeroI_def, g_eq]
+
+/-!
+Because `simp` checks its own intermediate results, a mismatch is reported even when a later
+rewrite in the same `simp` call repairs it and no tactic goal ever exhibits it. `g_stale` is stated
+about the stale application, so `simp only [natZero_def, g_stale]` closes the goal.
+-/
+
+theorem g_stale : @g 0 instXNatZero = 1 := rfl
+
+/--
+@ +2:2...34
+warning: `simp` rewrote a term with natZero_def. The new term has an instance argument whose type does not match at `.instances` transparency:
+  The instance argument
+    instXNatZero
+  has type
+    X natZero
+  but is expected to have type
+    X 0
+  in the application
+    @g 0 instXNatZero
+For the rest of this `simp` call, lemmas that mention this instance do not apply.
+
+Note: This linter can be disabled with `set_option linter.tacticCheckInstances false`
+-/
+#guard_msgs (positions := true) in
+example : g natZero = 1 := by
+  simp only [natZero_def, g_stale]
+
+/-!
+At most one mismatch is reported per command: splitting the simp set leaves the stale goal visible
+to the post-hoc check too, but `simp` has already reported it.
+-/
+
+/--
+@ +2:2...25
+warning: `simp` rewrote a term with natZero_def. The new term has an instance argument whose type does not match at `.instances` transparency:
+  The instance argument
+    instXNatZero
+  has type
+    X natZero
+  but is expected to have type
+    X 0
+  in the application
+    @g 0 instXNatZero
+For the rest of this `simp` call, lemmas that mention this instance do not apply.
+
+Note: This linter can be disabled with `set_option linter.tacticCheckInstances false`
+-/
+#guard_msgs (positions := true) in
+example : g natZero = 1 := by
+  simp only [natZero_def]
+  simp only [g_stale]
+
+/-!
+Goals that no `simp` call produced are still checked after the command, by the linter itself. The
+statement below carries the stale instance argument from the start.
+-/
+
+/--
+@ +2:2...5
+warning: The initial tactic goal has an instance argument whose type does not match at `.instances` transparency. `simp` and `rw` unify instance-implicit arguments at that transparency. Lemmas that mention this instance do not apply:
+  The instance argument
+    instXNatZero
+  has type
+    X natZero
+  but is expected to have type
+    X 0
+  in the application
+    @g 0 instXNatZero
+
+Note: This linter can be disabled with `set_option linter.tacticCheckInstances false`
+-/
+#guard_msgs (positions := true) in
+example : @g 0 instXNatZero = 1 := by
+  rfl

From 309e9b8f28dfcf8e5007b121e1d20a3f4536ca7e Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Fri, 21 Aug 2026 09:59:01 +0000
Subject: [PATCH 13/16] feat: check instance arguments after definitional
 rewrites

This PR makes `simp` and `dsimp` check, after they rewrite an argument of an application, the instance arguments whose types depend on that argument. When such an instance no longer has the expected type at `.instances` transparency, a replacement instance is synthesized and adopted if it is defeq to the old one at `.implicit` transparency; otherwise the rewrite of the argument is refused and a warning is logged. Previously the rewrite was applied unconditionally, leaving behind an instance argument that later lemmas mentioning that instance no longer match.

The check is controlled by `dsimp.resynthInstances` (default `true`), its warning by `dsimp.resynthInstances.warning` (default `true`). Adoptions and refusals are traced under `Meta.Tactic.simp.resynthInstances`.

Both entry points run the same fix-up: `simpApp` covers every argument-wise rebuild in `simp` (`simpAppUsingCongr`, `congrArgs`, and the `.fixed` branch of `tryAutoCongrTheorem?`), and standalone `dsimp` uses a new `postApp` hook of `transformWithCache`. The arguments an instance depends on carry forward dependencies, so `simp` can only ever have changed them definitionally; reverting or replacing them therefore keeps an already-built `Result.proof?` valid.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01FXiCjRqcz5MmCqu6YxoBFR
---
 src/Lean/Meta/Tactic/Simp.lean             |   1 +
 src/Lean/Meta/Tactic/Simp/Main.lean        |   4 +
 src/Lean/Meta/Tactic/Simp/Types.lean       | 165 ++++++++++++++++++++-
 src/Lean/Meta/Transform.lean               |   7 +-
 tests/elab/dsimpResynthInstances.lean      | 115 ++++++++++++++
 tests/elab/linterTacticCheckInstances.lean |   3 +
 6 files changed, 289 insertions(+), 6 deletions(-)
 create mode 100644 tests/elab/dsimpResynthInstances.lean

diff --git a/src/Lean/Meta/Tactic/Simp.lean b/src/Lean/Meta/Tactic/Simp.lean
index 7faa9f28c5a0..84e0f8194202 100644
--- a/src/Lean/Meta/Tactic/Simp.lean
+++ b/src/Lean/Meta/Tactic/Simp.lean
@@ -30,6 +30,7 @@ builtin_initialize registerTraceClass `Meta.Tactic.simp.rewrite (inherited := tr
 builtin_initialize registerTraceClass `Meta.Tactic.simp.backwardDefEq (inherited := true)
 builtin_initialize registerTraceClass `Meta.Tactic.simp.unify (inherited := true)
 builtin_initialize registerTraceClass `Meta.Tactic.simp.ground (inherited := true)
+builtin_initialize registerTraceClass `Meta.Tactic.simp.resynthInstances (inherited := true)
 builtin_initialize registerTraceClass `Meta.Tactic.simp.loopProtection (inherited := true)
 builtin_initialize registerTraceClass `Meta.Tactic.simp.numSteps
 builtin_initialize registerTraceClass `Meta.Tactic.simp.heads
diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean
index c28b986fc2a5..4c64ef1046f8 100644
--- a/src/Lean/Meta/Tactic/Simp/Main.lean
+++ b/src/Lean/Meta/Tactic/Simp/Main.lean
@@ -528,6 +528,7 @@ private partial def dsimpImpl (e : Expr) : SimpM Expr := do
       (skipInstances := !cfg.instances)
       (pre := pre)
       (post := post)
+      (postApp := fixResynthInstancesD)
 
 def visitFn (e : Expr) : SimpM Result := do
   let f := e.getAppFn
@@ -680,6 +681,9 @@ def simpApp (e : Expr) : SimpM Result := do
     return { expr := e }
   else
     let r ← congr e
+    -- All argument-wise rebuilds (`simpAppUsingCongr`, `congrArgs`, `tryAutoCongrTheorem?`)
+    -- flow through here, so one fix-up covers them.
+    let r ← fixResynthInstances e r
     -- Check here rather than once per simplified subterm: congruence is what leaves an instance
     -- argument behind, and a `post` rewrite may well repair the result before it is cached.
     if (← get).checkInstanceArgs && r.expr != e then
diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean
index 7bb3f60cd4e5..a601fb3d3afb 100644
--- a/src/Lean/Meta/Tactic/Simp/Types.lean
+++ b/src/Lean/Meta/Tactic/Simp/Types.lean
@@ -21,6 +21,22 @@ register_builtin_option backward.dsimp.instances : Bool := {
     descr    := "Let `dsimp` and `simp` simplify instance terms"
   }
 
+/--
+After a definitional rewrite of an argument, check the instance arguments whose types depend on
+it at `.instances` transparency; adopt a resynthesized instance when one exists and is defeq at
+`.implicit`, and refuse the rewrite otherwise. See `Simp.resynthInstanceArgs`.
+-/
+register_builtin_option dsimp.resynthInstances : Bool := {
+    defValue := true
+    descr    := "check instance arguments after definitional rewrites of the arguments they \
+      depend on; adopt a resynthesized instance when possible, refuse the rewrite otherwise"
+  }
+
+register_builtin_option dsimp.resynthInstances.warning : Bool := {
+    defValue := true
+    descr    := "warn when `dsimp.resynthInstances` refuses a rewrite"
+  }
+
 /-- The result of simplifying some expression `e`. -/
 structure Result where
   /-- The simplified version of `e` -/
@@ -76,6 +92,8 @@ structure Context where
   maxDischargeDepth : UInt32 := UInt32.ofNatClamp config.maxDischargeDepth
   simpTheorems      : SimpTheoremsArray := {}
   congrTheorems     : SimpCongrTheorems := {}
+  /-- See `dsimp.resynthInstances`. Set by `mkContext`. -/
+  resynthInstances  : Bool := false
   /--
   Stores the "parent" term for the term being simplified.
   If a simplification procedure result depends on this value,
@@ -180,6 +198,7 @@ def mkContext (config : Config := {}) (simpTheorems : SimpTheoremsArray := {}) (
     config, userConfig, simpTheorems, congrTheorems
     metaConfig := (← mkMetaConfig config)
     indexConfig := (← mkIndexConfig config)
+    resynthInstances := dsimp.resynthInstances.get (← getOptions)
   }
 
 def Context.setConfig (context : Context) (config : Config) : MetaM Context := do
@@ -258,8 +277,13 @@ structure State where
   again once a mismatch has been reported: the linter reports at most one per command.
   -/
   checkInstanceArgs : Bool := false
-  /-- Theorem applied by the most recent rewrite; only tracked while `checkInstanceArgs` is set. -/
+  /--
+  Theorem applied by the most recent rewrite; only tracked while `checkInstanceArgs` or
+  `Context.resynthInstances` is set.
+  -/
   lastThm?     : Option Origin := none
+  /-- Whether `resynthInstanceArgs` already warned about a refused rewrite in this run. -/
+  resynthWarned : Bool := false
 
 structure Stats where
   usedTheorems : UsedSimps := {}
@@ -316,8 +340,10 @@ opaque dsimp (e : Expr) : SimpM Expr
 
 @[inline] def modifyDiag (f : Diagnostics → Diagnostics) : SimpM Unit := do
   if (← isDiagnosticsEnabled) then
-    modify fun { cache, congrCache, dsimpCache, usedTheorems, numSteps, diag, checkInstanceArgs, lastThm? } =>
-      { cache, congrCache, dsimpCache, usedTheorems, numSteps, diag := f diag, checkInstanceArgs, lastThm? }
+    modify fun { cache, congrCache, dsimpCache, usedTheorems, numSteps, diag, checkInstanceArgs,
+                 lastThm?, resynthWarned } =>
+      { cache, congrCache, dsimpCache, usedTheorems, numSteps, diag := f diag, checkInstanceArgs,
+        lastThm?, resynthWarned }
 
 /--
 Result type for a simplification procedure. We have `pre` and `post` simplification procedures.
@@ -533,7 +559,7 @@ def recordTriedSimpTheorem (thmId : Origin) : SimpM Unit := do
     { s with triedThmCounter := s.triedThmCounter.insert thmId cNew }
 
 def recordSimpTheorem (thmId : Origin) : SimpM Unit := do
-  if (← get).checkInstanceArgs then
+  if (← get).checkInstanceArgs || (← readThe Simp.Context).resynthInstances then
     modify fun s => { s with lastThm? := some thmId }
   modifyDiag fun s =>
     let cNew := if let some c := s.usedThmCounter.find? thmId then c + 1 else 1
@@ -653,6 +679,137 @@ where
     else
       e
 
+/-- The binder domain of the `j`-th argument of `fType`, instantiated with `args[0..j-1]`. -/
+private def instantiatedBinderDomain? (fType : Expr) (args : Array Expr) (j : Nat) :
+    SimpM (Option Expr) := do
+  let mut t := fType
+  for i in [0:j] do
+    t ← whnfD t
+    let .forallE _ _ b _ := t | return none
+    t := b.instantiate1 args[i]!
+  t ← whnfD t
+  let .forallE _ d _ _ := t | return none
+  return some d
+
+/--
+Check the instance arguments of `f` after its arguments changed from `origArgs` to `args0`.
+An instance argument whose type depends on a changed argument is checked against its new binder
+domain at `.instances` transparency. On a mismatch, synthesize an instance of the new domain and
+adopt it if it is defeq to the old instance at `.implicit` transparency; otherwise revert the
+changed arguments the instance depends on, i.e. refuse those rewrites.
+
+The arguments an instance depends on are only ever changed definitionally (they have forward
+dependencies, so `simp` cannot rewrite them with a proof), which makes both adoption and
+reversion transparent to an already-built `Result.proof?`. `e` is the original application, used
+for messages. See `dsimp.resynthInstances`.
+-/
+def resynthInstanceArgs (e f : Expr) (origArgs args0 : Array Expr) : SimpM (Array Expr) := do
+  let infos := (← getFunInfoNArgs f args0.size).paramInfo
+  let n := min (min infos.size args0.size) origArgs.size
+  let mut relevant := false
+  for j in [0:n] do
+    if infos[j]!.isInstance && infos[j]!.backDeps.any (fun i => i < n && args0[i]! != origArgs[i]!) then
+      relevant := true
+      break
+  unless relevant do return args0
+  let fType ← inferType f
+  let mut args := args0
+  let mut rounds := 0
+  repeat
+    rounds := rounds + 1
+    if rounds > n + 1 then break
+    let mut dirty := false
+    for j in [0:n] do
+      let info := infos[j]!
+      unless info.isInstance do continue
+      unless info.backDeps.any (fun i => i < n && args[i]! != origArgs[i]!) do continue
+      let some expected ← instantiatedBinderDomain? fType args j | continue
+      let instOld := args[j]!
+      let actual ← inferType instOld
+      if ← withNewMCtxDepth <| withReducibleAndInstances <| isDefEqGuarded actual expected then
+        continue
+      let adopt? : Option Expr ← withNewMCtxDepth do
+        let inst'? ← try
+            match ← trySynthInstance expected with
+            | .some v => pure (some v)
+            | _ => pure none
+          catch _ => pure none
+        match inst'? with
+        | some inst' =>
+          if ← withTransparency .implicit <| isDefEqGuarded instOld inst' then
+            pure (some inst')
+          else
+            pure none
+        | none => pure none
+      match adopt? with
+      | some inst' =>
+        if inst' != instOld then
+          trace[Meta.Tactic.simp.resynthInstances] "adopted resynthesized instance \
+            in{indentExpr e}\nold instance{indentExpr instOld}\nnew instance{indentExpr inst'}"
+          args := args.set! j inst'
+          dirty := true
+      | none =>
+        -- Refuse: revert the changed arguments this instance depends on, and reset instance
+        -- arguments that depend on the reverted positions.
+        let mut reverted : Array Nat := #[]
+        for i in info.backDeps do
+          if i < n && args[i]! != origArgs[i]! then
+            -- Guard: reverting is only sound for definitional changes.
+            if ← withNewMCtxDepth <| withDefault <| isDefEqGuarded args[i]! origArgs[i]! then
+              args := args.set! i origArgs[i]!
+              reverted := reverted.push i
+        unless reverted.isEmpty do
+          for k in [0:n] do
+            if infos[k]!.isInstance && infos[k]!.backDeps.any reverted.contains
+                && args[k]! != origArgs[k]! then
+              if ← withNewMCtxDepth <| withDefault <| isDefEqGuarded args[k]! origArgs[k]! then
+                args := args.set! k origArgs[k]!
+          dirty := true
+          trace[Meta.Tactic.simp.resynthInstances] "refused rewrite in{indentExpr e}\n\
+            instance argument{indentExpr instOld}\nhas type{indentExpr actual}\n\
+            but is expected to have type{indentExpr expected}"
+          unless (← get).resynthWarned do
+            modify fun s => { s with resynthWarned := true }
+            if dsimp.resynthInstances.warning.get (← getOptions) then
+              let cause ← match (← get).lastThm? with
+                | some thm => do pure m!"A rewrite with {← ppOrigin thm}"
+                | none     => pure m!"A rewrite"
+              logWarning <| m!"{cause} changed an argument of{indentExpr e}\n\
+                The instance argument{indentExpr instOld}\nthen does not have the expected \
+                type at `.instances` transparency, and no usable replacement instance was \
+                found. The rewrite was not applied here." ++
+                .note m!"Disable this warning with `set_option \
+                  dsimp.resynthInstances.warning false`, or the whole check with `set_option \
+                  dsimp.resynthInstances false`."
+    unless dirty do break
+  return args
+
+/--
+Apply `resynthInstanceArgs` to the result of simplifying the application `e`. The reverted or
+adopted arguments are defeq to the ones they replace, so `r.proof?` remains valid.
+-/
+def fixResynthInstances (e : Expr) (r : Result) : SimpM Result := do
+  unless (← readThe Simp.Context).resynthInstances do return r
+  let eNew := r.expr
+  unless e.isApp && eNew.isApp && eNew.getAppNumArgs == e.getAppNumArgs do return r
+  let origArgs := e.getAppArgs
+  let newArgs := eNew.getAppArgs
+  if origArgs == newArgs then return r
+  let fixed ← resynthInstanceArgs e eNew.getAppFn origArgs newArgs
+  if fixed == newArgs then return r
+  return { r with expr := mkAppN eNew.getAppFn fixed }
+
+/-- `fixResynthInstances` for `dsimp`'s application rebuild. -/
+def fixResynthInstancesD (orig new : Expr) : SimpM Expr := do
+  unless (← readThe Simp.Context).resynthInstances do return new
+  unless orig.isApp && new.isApp && new.getAppNumArgs == orig.getAppNumArgs do return new
+  let origArgs := orig.getAppArgs
+  let newArgs := new.getAppArgs
+  if origArgs == newArgs then return new
+  let fixed ← resynthInstanceArgs orig new.getAppFn origArgs newArgs
+  if fixed == newArgs then return new
+  return mkAppN new.getAppFn fixed
+
 /--
 Given a simplified function result `r` and arguments `args`, simplify arguments using `simp` and `dsimp`.
 The resulting proof is built using `congr` and `congrFun` theorems.
diff --git a/src/Lean/Meta/Transform.lean b/src/Lean/Meta/Transform.lean
index e526c71d7539..28e17f9c8244 100644
--- a/src/Lean/Meta/Transform.lean
+++ b/src/Lean/Meta/Transform.lean
@@ -87,6 +87,8 @@ Parameters:
   over variables that are actually used in the body.
 - `skipConstInApp`: when true, constant heads in applications are not visited separately.
 - `skipInstances`: when true, instance arguments (determined via `getFunInfo`) are not visited.
+- `postApp`: called on each rebuilt application with the original and the rebuilt application;
+  its result is passed to `post`. Used by `dsimp` to fix up instance arguments.
 
 The `skipInstances` flag is used by `dsimp` to avoid rewriting instances.
 
@@ -103,6 +105,7 @@ partial def transformWithCache {m} [Monad m] [MonadLiftT MetaM m] [MonadControlT
     (usedLetOnly := false)
     (skipConstInApp := false)
     (skipInstances := false)
+    (postApp : Expr → Expr → m Expr := fun _ e => pure e)
     : m (Expr × Std.HashMap ExprStructEq Expr) :=
   let _ : STWorld IO.RealWorld m := ⟨⟩
   let _ : MonadLiftT (ST IO.RealWorld) m := { monadLift := fun x => liftM (m := MetaM) (liftM (m := ST IO.RealWorld) x) }
@@ -147,9 +150,9 @@ partial def transformWithCache {m} [Monad m] [MonadLiftT MetaM m] [MonadControlT
               args := args.set i (← visit arg)
             else
               args := args.set i (← visit arg)
-          visitPost (mkAppN f args.toArray)
+          visitPost (← postApp e (mkAppN f args.toArray))
         else
-          visitPost (mkAppN f (← args.mapM visit))
+          visitPost (← postApp e (mkAppN f (← args.mapM visit)))
       match (← pre e) with
       | .done e  => pure e
       | .visit e => visit e
diff --git a/tests/elab/dsimpResynthInstances.lean b/tests/elab/dsimpResynthInstances.lean
new file mode 100644
index 000000000000..83f5c22b7c20
--- /dev/null
+++ b/tests/elab/dsimpResynthInstances.lean
@@ -0,0 +1,115 @@
+module
+
+/-!
+Tests for `dsimp.resynthInstances`: after a definitional rewrite of an argument, `simp` and
+`dsimp` check the instance arguments whose types depend on it at `.instances` transparency.
+A resynthesized instance is adopted when it is defeq to the old one at `.implicit`
+transparency; otherwise the rewrite of the argument is refused.
+-/
+
+class X (n : Nat)
+
+@[implicit_reducible]
+def natZero := 0
+
+instance instXNatZero : X natZero where
+
+theorem natZero_def : natZero = 0 := rfl
+
+def g (m : Nat) [X m] : Nat := m + 1
+
+theorem g_eq {m} [X m] : g m = m + 1 := by
+  simp [g]
+
+/-!
+Refusal: there is no `X 0` instance, so the rewrite `natZero ↦ 0` inside `g` is refused with a
+warning. `g_eq` then still applies, and the goal closes.
+-/
+
+/--
+warning: A rewrite with natZero_def changed an argument of
+  g natZero
+The instance argument
+  instXNatZero
+then does not have the expected type at `.instances` transparency, and no usable replacement instance was found. The rewrite was not applied here.
+
+Note: Disable this warning with `set_option dsimp.resynthInstances.warning false`, or the whole check with `set_option dsimp.resynthInstances false`.
+-/
+#guard_msgs in
+example : g natZero = 1 := by
+  simp only [natZero_def, g_eq]
+
+/-!
+Adoption: `Y` has instances for both `natZeroY` and `0`, and they are defeq at `.implicit`
+transparency. The rewrite goes through with the resynthesized instance, silently (the trace
+shows the adoption).
+-/
+
+class Y (n : Nat)
+
+@[implicit_reducible]
+def natZeroY := 0
+
+instance instYNatZeroY : Y natZeroY where
+instance instY0 : Y 0 where
+
+theorem natZeroY_def : natZeroY = 0 := rfl
+
+def gY (m : Nat) [Y m] : Nat := m + 1
+
+theorem gY_eq {m} [Y m] : gY m = m + 1 := by
+  simp [gY]
+
+/--
+trace: [Meta.Tactic.simp.resynthInstances] adopted resynthesized instance in
+      gY natZeroY
+    old instance
+      instYNatZeroY
+    new instance
+      instY0
+-/
+#guard_msgs in
+set_option trace.Meta.Tactic.simp.resynthInstances true in
+example : gY natZeroY = 1 := by
+  simp only [natZeroY_def, gY_eq]
+
+/-!
+Standalone `dsimp` refuses the rewrite inside `g` but performs it elsewhere.
+-/
+
+/--
+warning: A rewrite with natZero_def changed an argument of
+  g natZero
+The instance argument
+  instXNatZero
+then does not have the expected type at `.instances` transparency, and no usable replacement instance was found. The rewrite was not applied here.
+
+Note: Disable this warning with `set_option dsimp.resynthInstances.warning false`, or the whole check with `set_option dsimp.resynthInstances false`.
+-/
+#guard_msgs in
+example : g natZero = natZero + 1 := by
+  dsimp only [natZero_def]
+  exact g_eq
+
+/-!
+`dsimp.resynthInstances.warning := false` silences the warning; the refusal still happens.
+-/
+
+#guard_msgs in
+set_option dsimp.resynthInstances.warning false in
+example : g natZero = 1 := by
+  simp only [natZero_def, g_eq]
+
+/-!
+`dsimp.resynthInstances := false` restores the old behavior: the stale term `@g 0 instXNatZero`
+is produced, `g_eq` no longer applies, and the goal remains open.
+-/
+
+/--
+error: unsolved goals
+⊢ g 0 = 1
+-/
+#guard_msgs in
+set_option dsimp.resynthInstances false in
+example : g natZero = 1 := by
+  simp only [natZero_def, g_eq]
diff --git a/tests/elab/linterTacticCheckInstances.lean b/tests/elab/linterTacticCheckInstances.lean
index 1e21f78e0bd9..e5360cab6c36 100644
--- a/tests/elab/linterTacticCheckInstances.lean
+++ b/tests/elab/linterTacticCheckInstances.lean
@@ -25,6 +25,9 @@ example (s : S) (a b idx : Nat) (h1 : idx < s.decls.size)
   sorry
 
 set_option linter.tacticCheckInstances true
+-- The cases below exercise the linter on stale instance arguments; disable the resynth guard so
+-- the stale terms are actually produced.
+set_option dsimp.resynthInstances false
 
 /--
 @ +4:2...17

From 4b6ada0b251197be72d7ff8571ca462bee05b463 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Fri, 21 Aug 2026 14:19:33 +0000
Subject: [PATCH 14/16] feat: add `@[lax_instance_defeq]` to exempt classes
 from the strict instance check

This PR adds the `@[lax_instance_defeq]` attribute, which exempts a class from the strict instance-argument discipline of `backward.isDefEq.respectTransparency.instances`: values assigned to instance metavariables of an exempt class are not required to match the metavariable's type at `.instances` transparency, and the instance-argument checks of `simp`/`dsimp` (`dsimp.resynthInstances`) and `linter.tacticCheckInstances` skip the class as well. Propositional classes are exempt by default, since proof irrelevance makes a stale instance argument harmless there.

The attribute is backed by a scoped environment extension, so it supports `local`/`scoped` use and can be applied retroactively to classes from other modules. The exemption is consulted in `isInstanceMVar` (which also feeds `spineMVarsAdmissible`), in `Simp.resynthInstanceArgs`, and in `Meta.findInstanceArgMismatch?`. The `backward.isDefEq.respectTransparency.instanceSearchTypes` path is deliberately not affected.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01FXiCjRqcz5MmCqu6YxoBFR
---
 src/Lean/Class.lean                   | 43 ++++++++++++++
 src/Lean/Meta/Check.lean              |  2 +
 src/Lean/Meta/ExprDefEq.lean          |  6 +-
 src/Lean/Meta/Tactic/Simp/Types.lean  |  5 +-
 tests/elab/dsimpResynthInstances.lean | 85 +++++++++++++++++++++++++++
 5 files changed, 138 insertions(+), 3 deletions(-)

diff --git a/src/Lean/Class.lean b/src/Lean/Class.lean
index 79b457a08230..cec936893e2b 100644
--- a/src/Lean/Class.lean
+++ b/src/Lean/Class.lean
@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Attributes
+public import Lean.ScopedEnvExtension
 import Lean.Util.CollectLevelParams
 public section
 namespace Lean
@@ -174,6 +175,48 @@ def addClass (env : Environment) (clsName : Name) : Except MessageData Environme
   let outLevelParams := computeOutLevelParams decl.type outParams decl.levelParams
   return classExtension.addEntry env { name := clsName, outParams, outLevelParams }
 
+/--
+Classes marked `@[lax_instance_defeq]` are exempt from the strict instance-argument discipline of
+`backward.isDefEq.respectTransparency.instances`: a value assigned to an instance metavariable of
+such a class is not required to have a type that matches the metavariable's type at `.instances`
+transparency. The instance-argument check of `simp`/`dsimp` (`dsimp.resynthInstances`) and the
+`linter.tacticCheckInstances` linter skip these classes as well.
+-/
+builtin_initialize laxInstanceDefeqExt : SimpleScopedEnvExtension Name NameSet ←
+  registerSimpleScopedEnvExtension {
+    initial  := {}
+    addEntry := fun s n => s.insert n
+  }
+
+builtin_initialize
+  registerBuiltinAttribute {
+    name  := `lax_instance_defeq
+    descr := "exempt instances of a class from the strict defeq check at `.instances` \
+      transparency (see `backward.isDefEq.respectTransparency.instances`)"
+    add   := fun declName stx kind => do
+      Attribute.Builtin.ensureNoArgs stx
+      unless isClass (← getEnv) declName do
+        throwError "invalid `lax_instance_defeq`, `{.ofConstName declName}` is not a class"
+      laxInstanceDefeqExt.add declName kind
+  }
+
+/-- Whether a class type's result sort is `Prop`. -/
+private def isPropValued : Expr → Bool
+  | .forallE _ _ b _ => isPropValued b
+  | .sort u          => u == .zero
+  | _                => false
+
+/--
+Return `true` if instances of class `className` are exempt from the strict defeq check at
+`.instances` transparency: the class is marked `@[lax_instance_defeq]`, or it is propositional
+(proof irrelevance makes a stale instance argument harmless there). See `laxInstanceDefeqExt`.
+-/
+def isLaxInstanceDefeqClass (env : Environment) (className : Name) : Bool :=
+  (laxInstanceDefeqExt.getState env).contains className ||
+    match env.find? className with
+    | some info => isPropValued info.type
+    | none => false
+
 /--
 Registers an inductive type or structure as a type class. Using `class` or `class inductive` is
 generally preferred over using `@[class] structure` or `@[class] inductive` directly.
diff --git a/src/Lean/Meta/Check.lean b/src/Lean/Meta/Check.lean
index 639dfa3d1c23..ec27311284c1 100644
--- a/src/Lean/Meta/Check.lean
+++ b/src/Lean/Meta/Check.lean
@@ -387,6 +387,8 @@ where
   visitApp (f a : Expr) : MetaM (Option MessageData) := do
     let (expectedType, binfo) ← try getFunctionDomain f catch _ => return none
     unless binfo.isInstImplicit do return none
+    if let some className ← isClass? expectedType then
+      if isLaxInstanceDefeqClass (← getEnv) className then return none
     let aType ← try inferType a catch _ => return none
     let defEqAt (transparency : TransparencyMode) : MetaM Bool :=
       withoutModifyingState <| withTransparency transparency <| isDefEqGuarded expectedType aType
diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index cc616ee5b4d3..bbd50292d94d 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -573,13 +573,15 @@ parameter, identified by `.synthetic` kind together with a class type.
 Assignments to these are checked at exactly `.instances` transparency, so an ambient
 `.default`/`.all` does not let semireducible definitions be unfolded while checking the type of an
 instance assignment. This intentionally does not apply to ordinary implicit (`{..}`) metavariables
-that happen to have a class type, which are created with `.natural` kind.
+that happen to have a class type, which are created with `.natural` kind, nor to classes exempted
+by `isLaxInstanceDefeqClass` (marked `@[lax_instance_defeq]`, or propositional).
 -/
 private def isInstanceMVar (mvarId : MVarId) : MetaM Bool := do
   unless backward.isDefEq.respectTransparency.instances.get (← getOptions) do
     return false
   unless (← mvarId.getKind) matches .synthetic do return false
-  return (← isClass? (← mvarId.getDecl).type).isSome
+  let some className ← isClass? (← mvarId.getDecl).type | return false
+  return !isLaxInstanceDefeqClass (← getEnv) className
 
 /--
 Returns `true` if all metavariables whose types influence the type of `e`, a value assigned to an
diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean
index a601fb3d3afb..c0eac17d3b84 100644
--- a/src/Lean/Meta/Tactic/Simp/Types.lean
+++ b/src/Lean/Meta/Tactic/Simp/Types.lean
@@ -694,7 +694,8 @@ private def instantiatedBinderDomain? (fType : Expr) (args : Array Expr) (j : Na
 /--
 Check the instance arguments of `f` after its arguments changed from `origArgs` to `args0`.
 An instance argument whose type depends on a changed argument is checked against its new binder
-domain at `.instances` transparency. On a mismatch, synthesize an instance of the new domain and
+domain at `.instances` transparency; classes exempted by `isLaxInstanceDefeqClass` (marked
+`@[lax_instance_defeq]`, or propositional) are skipped. On a mismatch, synthesize an instance of the new domain and
 adopt it if it is defeq to the old instance at `.implicit` transparency; otherwise revert the
 changed arguments the instance depends on, i.e. refuse those rewrites.
 
@@ -724,6 +725,8 @@ def resynthInstanceArgs (e f : Expr) (origArgs args0 : Array Expr) : SimpM (Arra
       unless info.isInstance do continue
       unless info.backDeps.any (fun i => i < n && args[i]! != origArgs[i]!) do continue
       let some expected ← instantiatedBinderDomain? fType args j | continue
+      if let some className ← isClass? expected then
+        if isLaxInstanceDefeqClass (← getEnv) className then continue
       let instOld := args[j]!
       let actual ← inferType instOld
       if ← withNewMCtxDepth <| withReducibleAndInstances <| isDefEqGuarded actual expected then
diff --git a/tests/elab/dsimpResynthInstances.lean b/tests/elab/dsimpResynthInstances.lean
index 83f5c22b7c20..d720c0531507 100644
--- a/tests/elab/dsimpResynthInstances.lean
+++ b/tests/elab/dsimpResynthInstances.lean
@@ -100,6 +100,91 @@ set_option dsimp.resynthInstances.warning false in
 example : g natZero = 1 := by
   simp only [natZero_def, g_eq]
 
+/-!
+A class marked `@[lax_instance_defeq]` is exempt: the rewrite goes through unchecked as in the
+old behavior, producing the stale term `@gZ 0 instZNatZeroZ`. Since the class is also exempt
+from the strict assignment check in `isDefEq`, `gZ_eq` still applies (the instance assignment
+is checked at `.implicit`, where `natZeroZ` unfolds), and the goal closes silently.
+-/
+
+@[lax_instance_defeq]
+class Z (n : Nat)
+
+@[implicit_reducible]
+def natZeroZ := 0
+
+instance instZNatZeroZ : Z natZeroZ where
+
+theorem natZeroZ_def : natZeroZ = 0 := rfl
+
+def gZ (m : Nat) [Z m] : Nat := m + 1
+
+theorem gZ_eq {m} [Z m] : gZ m = m + 1 := by
+  simp [gZ]
+
+#guard_msgs in
+example : gZ natZeroZ = 1 := by
+  simp only [natZeroZ_def, gZ_eq]
+
+/-!
+The attribute can be applied retroactively and locally; outside the section, `X` is strict
+again.
+-/
+
+section
+attribute [local lax_instance_defeq] X
+
+#guard_msgs in
+example : g natZero = 1 := by
+  simp only [natZero_def, g_eq]
+
+end
+
+/--
+warning: A rewrite with natZero_def changed an argument of
+  g natZero
+The instance argument
+  instXNatZero
+then does not have the expected type at `.instances` transparency, and no usable replacement instance was found. The rewrite was not applied here.
+
+Note: Disable this warning with `set_option dsimp.resynthInstances.warning false`, or the whole check with `set_option dsimp.resynthInstances false`.
+-/
+#guard_msgs in
+example : g natZero = 1 := by
+  simp only [natZero_def, g_eq]
+
+/-!
+Only classes can be marked.
+-/
+
+/--
+error: invalid `lax_instance_defeq`, `Nat.add` is not a class
+-/
+#guard_msgs in
+attribute [lax_instance_defeq] Nat.add
+
+/-!
+Propositional classes are exempt by default, without the attribute; same behavior as above.
+-/
+
+class P (n : Nat) : Prop
+
+@[implicit_reducible]
+def natZeroP := 0
+
+instance instPNatZeroP : P natZeroP where
+
+theorem natZeroP_def : natZeroP = 0 := rfl
+
+def gP (m : Nat) [P m] : Nat := m + 1
+
+theorem gP_eq {m} [P m] : gP m = m + 1 := by
+  simp [gP]
+
+#guard_msgs in
+example : gP natZeroP = 1 := by
+  simp only [natZeroP_def, gP_eq]
+
 /-!
 `dsimp.resynthInstances := false` restores the old behavior: the stale term `@g 0 instXNatZero`
 is produced, `g_eq` no longer applies, and the goal remains open.

From 07ce7d7090dcced7c02f49dd512121f7d51b740d Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Fri, 21 Aug 2026 14:27:38 +0000
Subject: [PATCH 15/16] chore: disable `dsimp.resynthInstances` by default on
 this branch

The option's default is a property of the toolchain and governs every package built with it, including dependencies such as Batteries that do not receive Mathlib's `leanOptions`. This branch (worktree `julia-instance-mvars`) keeps the backward-compatible behavior by default; the sibling branch `instance-strict-dsimp` enables the check by default. The feature test sets the option explicitly so it passes under either default.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01FXiCjRqcz5MmCqu6YxoBFR
---
 src/Lean/Meta/Tactic/Simp/Types.lean  | 2 +-
 tests/elab/dsimpResynthInstances.lean | 5 +++++
 2 files changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean
index c0eac17d3b84..e05e8f46e89a 100644
--- a/src/Lean/Meta/Tactic/Simp/Types.lean
+++ b/src/Lean/Meta/Tactic/Simp/Types.lean
@@ -27,7 +27,7 @@ it at `.instances` transparency; adopt a resynthesized instance when one exists
 `.implicit`, and refuse the rewrite otherwise. See `Simp.resynthInstanceArgs`.
 -/
 register_builtin_option dsimp.resynthInstances : Bool := {
-    defValue := true
+    defValue := false
     descr    := "check instance arguments after definitional rewrites of the arguments they \
       depend on; adopt a resynthesized instance when possible, refuse the rewrite otherwise"
   }
diff --git a/tests/elab/dsimpResynthInstances.lean b/tests/elab/dsimpResynthInstances.lean
index d720c0531507..0454ffaa1271 100644
--- a/tests/elab/dsimpResynthInstances.lean
+++ b/tests/elab/dsimpResynthInstances.lean
@@ -5,8 +5,13 @@ Tests for `dsimp.resynthInstances`: after a definitional rewrite of an argument,
 `dsimp` check the instance arguments whose types depend on it at `.instances` transparency.
 A resynthesized instance is adopted when it is defeq to the old one at `.implicit`
 transparency; otherwise the rewrite of the argument is refused.
+
+The check is enabled explicitly so that the tests are independent of the option's default,
+which differs between toolchain branches.
 -/
 
+set_option dsimp.resynthInstances true
+
 class X (n : Nat)
 
 @[implicit_reducible]

From 983d39e41bd4e0511bb71667454bc28868a59710 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Fri, 28 Aug 2026 22:13:17 +0200
Subject: [PATCH 16/16] poke