feat: move instance-class check to declaration site (#12325)

This PR adds a warning to any `def` of class type that does not also
declare an appropriate reducibility.

The warning check runs after elaboration (checking the actual
reducibility status via `getReducibilityStatus`) rather than
syntactically checking modifiers before elaboration. This is necessary
to accommodate patterns like `@[to_additive (attr :=
implicit_reducible)]` in Mathlib, where the reducibility attribute is
applied during `.afterCompilation` by another attribute, and would be
missed by a purely syntactic check.

---------

Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

.github/workflows/build-template.yml

@@ -137,7 +137,7 @@ jobs:
           [ -d build ] || mkdir build
           cd build
           # arguments passed to `cmake`
-          OPTIONS=(-DLEAN_EXTRA_MAKE_OPTS=-DwarningAsError=true)
+          OPTIONS=()
           if [[ -n '${{ matrix.release }}' ]]; then
             # this also enables githash embedding into stage 1 library, which prohibits reusing
             # `.olean`s across commits, so we don't do it in the fast non-release CI

src/Init/Data/Char/Lemmas.lean

@@ -62,7 +62,7 @@ instance ltTrichotomous : Std.Trichotomous (· < · : Char → Char → Prop) wh
   trichotomous _ _ h₁ h₂ := Char.le_antisymm (by simpa using h₂) (by simpa using h₁)
 
 @[deprecated ltTrichotomous (since := "2025-10-27")]
-def notLTAntisymm : Std.Antisymm (¬ · < · : Char → Char → Prop) where
+theorem notLTAntisymm : Std.Antisymm (¬ · < · : Char → Char → Prop) where
   antisymm := Char.ltTrichotomous.trichotomous
 
 instance ltAsymm : Std.Asymm (· < · : Char → Char → Prop) where
@@ -73,7 +73,7 @@ instance leTotal : Std.Total (· ≤ · : Char → Char → Prop) where
 
 -- This instance is useful while setting up instances for `String`.
 @[deprecated ltAsymm (since := "2025-08-01")]
-def notLTTotal : Std.Total (¬ · < · : Char → Char → Prop) where
+theorem notLTTotal : Std.Total (¬ · < · : Char → Char → Prop) where
   total := fun x y => by simpa using Char.le_total y x
 
 @[simp] theorem ofNat_toNat (c : Char) : Char.ofNat c.toNat = c := by

src/Init/Data/Iterators/Combinators/Monadic/FlatMap.lean

@@ -362,8 +362,7 @@ def Flatten.instProductivenessRelation [Monad m] [Iterator α m (IterM (α := α
     case innerDone =>
       apply Flatten.productiveRel_of_right₂
 
-@[no_expose]
-public def Flatten.instProductive [Monad m] [Iterator α m (IterM (α := α₂) m β)] [Iterator α₂ m β]
+public theorem Flatten.instProductive [Monad m] [Iterator α m (IterM (α := α₂) m β)] [Iterator α₂ m β]
     [Finite α m] [Productive α₂ m] : Productive (Flatten α α₂ β m) m :=
   .of_productivenessRelation instProductivenessRelation
 

src/Init/Data/Iterators/Consumers/Loop.lean

@@ -35,7 +35,7 @@ A `ForIn'` instance for iterators. Its generic membership relation is not easy t
 so this is not marked as `instance`. This way, more convenient instances can be built on top of it
 or future library improvements will make it more comfortable.
 -/
-@[always_inline, inline]
+@[always_inline, inline, expose, implicit_reducible]
 def Iter.instForIn' {α : Type w} {β : Type w} {n : Type x → Type x'} [Monad n]
     [Iterator α Id β] [IteratorLoop α Id n] :
     ForIn' n (Iter (α := α) β) β ⟨fun it out => it.IsPlausibleIndirectOutput out⟩ where
@@ -53,7 +53,7 @@ instance (α : Type w) (β : Type w) (n : Type x → Type x') [Monad n]
 /--
 An implementation of `for h : ... in ... do ...` notation for partial iterators.
 -/
-@[always_inline, inline]
+@[always_inline, inline, expose, implicit_reducible]
 def Iter.Partial.instForIn' {α : Type w} {β : Type w} {n : Type x → Type x'} [Monad n]
     [Iterator α Id β] [IteratorLoop α Id n] :
     ForIn' n (Iter.Partial (α := α) β) β ⟨fun it out => it.it.IsPlausibleIndirectOutput out⟩ where
@@ -71,7 +71,7 @@ instance (α : Type w) (β : Type w) (n : Type x → Type x') [Monad n]
 A `ForIn'` instance for iterators that is guaranteed to terminate after finitely many steps.
 It is not marked as an instance because the membership predicate is difficult to work with.
 -/
-@[always_inline, inline]
+@[always_inline, inline, expose, implicit_reducible]
 def Iter.Total.instForIn' {α : Type w} {β : Type w} {n : Type x → Type x'} [Monad n]
     [Iterator α Id β] [IteratorLoop α Id n] [Finite α Id] :
     ForIn' n (Iter.Total (α := α) β) β ⟨fun it out => it.it.IsPlausibleIndirectOutput out⟩ where

src/Init/Data/Iterators/Consumers/Monadic/Loop.lean

@@ -159,7 +159,7 @@ This is the default implementation of the `IteratorLoop` class.
 It simply iterates through the iterator using `IterM.step`. For certain iterators, more efficient
 implementations are possible and should be used instead.
 -/
-@[always_inline, inline, expose]
+@[always_inline, inline, expose, implicit_reducible]
 def IteratorLoop.defaultImplementation {α : Type w} {m : Type w → Type w'} {n : Type x → Type x'}
     [Monad n] [Iterator α m β] :
     IteratorLoop α m n where
@@ -211,7 +211,7 @@ theorem IteratorLoop.wellFounded_of_productive {α β : Type w} {m : Type w →
 /--
 This `ForIn'`-style loop construct traverses a finite iterator using an `IteratorLoop` instance.
 -/
-@[always_inline, inline]
+@[always_inline, inline, expose, implicit_reducible]
 def IteratorLoop.finiteForIn' {m : Type w → Type w'} {n : Type x → Type x'}
     {α : Type w} {β : Type w} [Iterator α m β] [IteratorLoop α m n] [Monad n]
     (lift : ∀ γ δ, (γ → n δ) → m γ → n δ) :
@@ -224,7 +224,7 @@ A `ForIn'` instance for iterators. Its generic membership relation is not easy t
 so this is not marked as `instance`. This way, more convenient instances can be built on top of it
 or future library improvements will make it more comfortable.
 -/
-@[always_inline, inline]
+@[always_inline, inline, expose, implicit_reducible]
 def IterM.instForIn' {m : Type w → Type w'} {n : Type w → Type w''}
     {α : Type w} {β : Type w} [Iterator α m β] [IteratorLoop α m n] [Monad n]
     [MonadLiftT m n] :
@@ -239,7 +239,7 @@ instance IterM.instForInOfIteratorLoop {m : Type w → Type w'} {n : Type w →
   instForInOfForIn'
 
 /-- Internal implementation detail of the iterator library. -/
-@[always_inline, inline]
+@[always_inline, inline, expose, implicit_reducible]
 def IterM.Partial.instForIn' {m : Type w → Type w'} {n : Type w → Type w''}
     {α : Type w} {β : Type w} [Iterator α m β] [IteratorLoop α m n] [MonadLiftT m n] [Monad n] :
     ForIn' n (IterM.Partial (α := α) m β) β ⟨fun it out => it.it.IsPlausibleIndirectOutput out⟩ where
@@ -247,7 +247,7 @@ def IterM.Partial.instForIn' {m : Type w → Type w'} {n : Type w → Type w''}
     haveI := @IterM.instForIn'; forIn' it.it init f
 
 /-- Internal implementation detail of the iterator library. -/
-@[always_inline, inline]
+@[always_inline, inline, expose, implicit_reducible]
 def IterM.Total.instForIn' {m : Type w → Type w'} {n : Type w → Type w''}
     {α : Type w} {β : Type w} [Iterator α m β] [IteratorLoop α m n] [MonadLiftT m n] [Monad n]
     [Finite α m] :

src/Init/Data/Iterators/Internal/LawfulMonadLiftFunction.lean

@@ -70,7 +70,7 @@ theorem LawfulMonadLiftFunction.lift_seqRight [LawfulMonad m] [LawfulMonad n]
 abbrev idToMonad [Monad m] ⦃α : Type u⦄ (x : Id α) : m α :=
     pure x.run
 
-def LawfulMonadLiftFunction.idToMonad [Monad m] [LawfulMonad m] :
+theorem LawfulMonadLiftFunction.idToMonad [LawfulMonad m] :
     LawfulMonadLiftFunction (m := Id) (n := m) idToMonad where
   lift_pure := by simp [Internal.idToMonad]
   lift_bind := by simp [Internal.idToMonad]
@@ -95,7 +95,7 @@ instance [LawfulMonadLiftBindFunction (n := n) (fun _ _ f x => lift x >>= f)] [L
     simpa using LawfulMonadLiftBindFunction.liftBind_bind (n := n)
       (liftBind := fun _ _ f x => lift x >>= f) (β := β) (γ := γ) (δ := γ) pure x g
 
-def LawfulMonadLiftBindFunction.id [Monad m] [LawfulMonad m] :
+theorem LawfulMonadLiftBindFunction.id [LawfulMonad m] :
     LawfulMonadLiftBindFunction (m := Id) (n := m) (fun _ _ f x => f x.run) where
   liftBind_pure := by simp
   liftBind_bind := by simp

src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean

@@ -32,7 +32,7 @@ theorem Iter.forIn'_eq {α β : Type w} [Iterator α Id β] [Finite α Id]
       IterM.DefaultConsumers.forIn' (n := m) (fun _ _ f x => f x.run) γ (fun _ _ _ => True)
         it.toIterM init _ (fun _ => id)
           (fun out h acc => return ⟨← f out (Iter.isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM.mpr h) acc, trivial⟩) := by
-  simp +instances only [instForIn', ForIn'.forIn', IteratorLoop.finiteForIn']
+  simp +instances only [ForIn'.forIn']
   have : ∀ a b c, f a b c = (Subtype.val <$> (⟨·, trivial⟩) <$> f a b c) := by simp
   simp +singlePass only [this]
   rw [hl.lawful (fun _ _ f x => f x.run) (wf := IteratorLoop.wellFounded_of_finite)]
@@ -81,7 +81,7 @@ theorem Iter.forIn'_eq_forIn'_toIterM {α β : Type w} [Iterator α Id β]
       letI : ForIn' m (IterM (α := α) Id β) β _ := IterM.instForIn'
       ForIn'.forIn' it.toIterM init
         (fun out h acc => f out (isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM.mpr h) acc) := by
-  simp +instances [ForIn'.forIn', Iter.instForIn', IterM.instForIn', monadLift]
+  simp +instances [ForIn'.forIn', monadLift]
 
 theorem Iter.forIn_eq_forIn_toIterM {α β : Type w} [Iterator α Id β]
     [Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m]

src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean

@@ -109,7 +109,7 @@ theorem IterM.forIn'_eq {α β : Type w} {m : Type w → Type w'} [Iterator α m
     letI : ForIn' n (IterM (α := α) m β) β _ := IterM.instForIn'
     ForIn'.forIn' (α := β) (m := n) it init f = IterM.DefaultConsumers.forIn' (n := n)
         (fun _ _ f x => monadLift x >>= f) γ (fun _ _ _ => True) it init _ (fun _ => id) (return ⟨← f · · ·, trivial⟩) := by
-  simp +instances only [instForIn', ForIn'.forIn', IteratorLoop.finiteForIn']
+  simp +instances only [ForIn'.forIn']
   have : f = (Subtype.val <$> (⟨·, trivial⟩) <$> f · · ·) := by simp
   rw [this, hl.lawful (fun _ _ f x => monadLift x >>= f) (wf := IteratorLoop.wellFounded_of_finite)]
   simp +instances [IteratorLoop.defaultImplementation]

src/Init/Data/Iterators/ToIterator.lean

@@ -32,14 +32,14 @@ def ToIterator.iter [ToIterator γ Id α β] (x : γ) : Iter (α := α) β :=
   ToIterator.iterM x |>.toIter
 
 /-- Creates a monadic `ToIterator` instance. -/
-@[always_inline, inline, expose, instance_reducible]
+@[always_inline, inline, expose, implicit_reducible]
 def ToIterator.ofM (α : Type w)
     (iterM : γ → IterM (α := α) m β) :
     ToIterator γ m α β where
   iterMInternal x := iterM x
 
 /-- Creates a pure `ToIterator` instance. -/
-@[always_inline, inline, expose, instance_reducible]
+@[always_inline, inline, expose, implicit_reducible]
 def ToIterator.of (α : Type w)
     (iter : γ → Iter (α := α) β) :
     ToIterator γ Id α β where

src/Init/Data/Order/Factories.lean

@@ -147,7 +147,7 @@ public theorem LawfulOrderMin.of_min_le {α : Type u} [Min α] [LE α]
 This lemma characterizes in terms of `LE α` when a `Max α` instance "behaves like a supremum
 operator".
 -/
-public def LawfulOrderSup.of_le {α : Type u} [Max α] [LE α]
+public theorem LawfulOrderSup.of_le {α : Type u} [Max α] [LE α]
     (max_le_iff : ∀ a b c : α, max a b ≤ c ↔ a ≤ c ∧ b ≤ c) : LawfulOrderSup α where
   max_le_iff := max_le_iff
 
@@ -159,7 +159,7 @@ instances.
 
 The produced instance entails `LawfulOrderSup α` and `MaxEqOr α`.
 -/
-public def LawfulOrderMax.of_max_le_iff {α : Type u} [Max α] [LE α]
+public theorem LawfulOrderMax.of_max_le_iff {α : Type u} [Max α] [LE α]
     (max_le_iff : ∀ a b c : α, max a b ≤ c ↔ a ≤ c ∧ b ≤ c := by exact LawfulOrderInf.le_min_iff)
     (max_eq_or : ∀ a b : α, max a b = a ∨ max a b = b := by exact MaxEqOr.max_eq_or) :
     LawfulOrderMax α where
@@ -196,7 +196,7 @@ Creates a *total* `LE α` instance from an `LT α` instance.
 
 This only makes sense for asymmetric `LT α` instances (see `Std.Asymm`).
 -/
-@[inline]
+@[inline, implicit_reducible, expose]
 public def _root_.LE.ofLT (α : Type u) [LT α] : LE α where
   le a b := ¬ b < a
 
@@ -276,7 +276,7 @@ public theorem LawfulOrderMin.of_lt {α : Type u} [Min α] [LT α]
 This lemma characterizes in terms of `LT α` when a `Max α` instance
 "behaves like an supremum operator" with respect to `LE.ofLT α`.
 -/
-public def LawfulOrderSup.of_lt {α : Type u} [Max α] [LT α]
+public theorem LawfulOrderSup.of_lt {α : Type u} [Max α] [LT α]
     (lt_max_iff : ∀ a b c : α, c < max a b ↔ c < a ∨ c < b) :
     haveI := LE.ofLT α
     LawfulOrderSup α :=
@@ -293,7 +293,7 @@ Derives a `LawfulOrderMax α` instance for `LE.ofLT` from two properties involvi
 
 The produced instance entails `LawfulOrderSup α` and `MaxEqOr α`.
 -/
-public def LawfulOrderMax.of_lt {α : Type u} [Max α] [LT α]
+public theorem LawfulOrderMax.of_lt {α : Type u} [Max α] [LT α]
     (lt_max_iff : ∀ a b c : α, c < max a b ↔ c < a ∨ c < b)
     (max_eq_or : ∀ a b : α, max a b = a ∨ max a b = b) :
     haveI := LE.ofLT α

src/Init/Data/Order/FactoriesExtra.lean

@@ -26,7 +26,7 @@ public def _root_.LE.ofOrd (α : Type u) [Ord α] : LE α where
 /--
 Creates an `DecidableLE α` instance using a well-behaved `Ord α` instance.
 -/
-@[inline, expose]
+@[inline, expose, implicit_reducible]
 public def _root_.DecidableLE.ofOrd (α : Type u) [LE α] [Ord α] [LawfulOrderOrd α] :
     DecidableLE α :=
   fun a b => match h : (compare a b).isLE with
@@ -93,7 +93,7 @@ grind_pattern compare_ne_eq => compare a b, Ordering.eq where
 /--
 Creates a `DecidableLT α` instance using a well-behaved `Ord α` instance.
 -/
-@[inline, expose]
+@[inline, expose, implicit_reducible]
 public def _root_.DecidableLT.ofOrd (α : Type u) [LE α] [LT α] [Ord α] [LawfulOrderOrd α]
     [LawfulOrderLT α] :
     DecidableLT α :=

src/Init/Data/Order/Opposite.lean

@@ -52,7 +52,8 @@ def max' [LE α] [DecidableLE α] (a b : α) : α :=
 Without the `open scoped` command, Lean would not find the required {lit}`DecidableLE α`
 instance for the opposite order.
 -/
-@[implicit_reducible] def LE.opposite (le : LE α) : LE α where
+@[implicit_reducible]
+def LE.opposite (le : LE α) : LE α where
   le a b := b ≤ a
 
 theorem LE.opposite_def {le : LE α} :
@@ -89,6 +90,7 @@ example [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsLinearOrder α] {x y : α}
 Without the `open scoped` command, Lean would not find the {lit}`LawfulOrderLT α`
 and {lit}`IsLinearOrder α` instances for the opposite order that are required by {name}`not_le`.
 -/
+@[implicit_reducible]
 def LT.opposite (lt : LT α) : LT α where
   lt a b := b < a
 
@@ -125,6 +127,7 @@ example [LE α] [DecidableLE α] [Min α] [Std.LawfulOrderLeftLeaningMin α] {a
 Without the `open scoped` command, Lean would not find the {lit}`LawfulOrderLeftLeaningMax α`
 instance for the opposite order that is required by {name}`max_eq_if`.
 -/
+@[implicit_reducible]
 def Min.oppositeMax (min : Min α) : Max α where
   max a b := Min.min a b
 
@@ -161,6 +164,7 @@ example [LE α] [DecidableLE α] [Max α] [Std.LawfulOrderLeftLeaningMax α] {a
 Without the `open scoped` command, Lean would not find the {lit}`LawfulOrderLeftLeaningMin α`
 instance for the opposite order that is required by {name}`min_eq_if`.
 -/
+@[implicit_reducible]
 def Max.oppositeMin (max : Max α) : Min α where
   min a b := Max.max a b
 

src/Init/Data/Order/PackageFactories.lean

@@ -47,7 +47,7 @@ public instance instLawfulOrderBEqOfDecidableLE {α : Type u} [LE α] [Decidable
   beq_iff_le_and_ge := by simp [BEq.beq]
 
 /-- If `LT` can be characterized in terms of a decidable `LE`, then `LT` is decidable either. -/
-@[expose, instance_reducible]
+@[inline, expose, implicit_reducible]
 public def decidableLTOfLE {α : Type u} [LE α] {_ : LT α} [DecidableLE α] [LawfulOrderLT α] :
     DecidableLT α :=
   fun a b =>
@@ -171,7 +171,7 @@ automatically. If it fails, it is necessary to provide some of the fields manual
 * Other proof obligations, namely `le_refl` and `le_trans`, can be omitted if `Refl` and `Trans`
   instances can be synthesized.
 -/
-@[expose, implicit_reducible]
+@[inline, expose, implicit_reducible]
 public def PreorderPackage.ofLE (α : Type u)
     (args : Packages.PreorderOfLEArgs α := by exact {}) : PreorderPackage α where
   toLE := args.le
@@ -256,7 +256,7 @@ automatically. If it fails, it is necessary to provide some of the fields manual
 * Other proof obligations, namely `le_refl`, `le_trans` and `le_antisymm`, can be omitted if `Refl`,
   `Trans` and `Antisymm` instances can be synthesized.
 -/
-@[expose, implicit_reducible]
+@[inline, expose, implicit_reducible]
 public def PartialOrderPackage.ofLE (α : Type u)
     (args : Packages.PartialOrderOfLEArgs α := by exact {}) : PartialOrderPackage α where
   toPreorderPackage := .ofLE α args.toPreorderOfLEArgs
@@ -385,7 +385,7 @@ automatically. If it fails, it is necessary to provide some of the fields manual
 * Other proof obligations, namely `le_total` and `le_trans`, can be omitted if `Total` and `Trans`
   instances can be synthesized.
 -/
-@[expose, implicit_reducible]
+@[inline, expose, implicit_reducible]
 public def LinearPreorderPackage.ofLE (α : Type u)
     (args : Packages.LinearPreorderOfLEArgs α := by exact {}) : LinearPreorderPackage α where
   toPreorderPackage := .ofLE α args.toPreorderOfLEArgs
@@ -487,7 +487,7 @@ automatically. If it fails, it is necessary to provide some of the fields manual
 * Other proof obligations, namely `le_total`, `le_trans` and `le_antisymm`, can be omitted if
   `Total`, `Trans` and `Antisymm` instances can be synthesized.
 -/
-@[expose, implicit_reducible]
+@[inline, expose, implicit_reducible]
 public def LinearOrderPackage.ofLE (α : Type u)
     (args : Packages.LinearOrderOfLEArgs α := by exact {}) : LinearOrderPackage α where
   toLinearPreorderPackage := .ofLE α args.toLinearPreorderOfLEArgs
@@ -647,7 +647,7 @@ automatically. If it fails, it is necessary to provide some of the fields manual
 * Other proof obligations, for example `transOrd`, can be omitted if a matching instance can be
   synthesized.
 -/
-@[expose, instance_reducible]
+@[inline, expose, implicit_reducible]
 public def LinearPreorderPackage.ofOrd (α : Type u)
     (args : Packages.LinearPreorderOfOrdArgs α := by exact {}) : LinearPreorderPackage α :=
   letI := args.ord
@@ -793,7 +793,7 @@ automatically. If it fails, it is necessary to provide some of the fields manual
 * Other proof obligations, such as `transOrd`, can be omitted if matching instances can be
   synthesized.
 -/
-@[expose, instance_reducible]
+@[inline, expose, implicit_reducible]
 public def LinearOrderPackage.ofOrd (α : Type u)
     (args : Packages.LinearOrderOfOrdArgs α := by exact {}) : LinearOrderPackage α :=
   -- set_option backward.isDefEq.respectTransparency false in

src/Init/Data/Range/Polymorphic/RangeIterator.lean

@@ -597,8 +597,7 @@ instance Iterator.instLawfulIteratorLoop [UpwardEnumerable α] [LE α] [Decidabl
     LawfulIteratorLoop (Rxc.Iterator α) Id n where
   lawful := by
     intro lift instLawfulMonadLiftFunction γ it init Pl wf f
-    simp +instances only [IteratorLoop.defaultImplementation, IteratorLoop.forIn,
-      IterM.DefaultConsumers.forIn'_eq_wf Pl wf]
+    simp +instances only [IteratorLoop.forIn, IterM.DefaultConsumers.forIn'_eq_wf Pl wf]
     rw [IterM.DefaultConsumers.forIn'.wf]
     split; rotate_left
     · simp only [IterM.step_eq,
@@ -1173,8 +1172,7 @@ instance Iterator.instLawfulIteratorLoop [UpwardEnumerable α] [LT α] [Decidabl
     LawfulIteratorLoop (Rxo.Iterator α) Id n where
   lawful := by
     intro lift instLawfulMonadLiftFunction γ it init Pl wf f
-    simp +instances only [IteratorLoop.defaultImplementation, IteratorLoop.forIn,
-      IterM.DefaultConsumers.forIn'_eq_wf Pl wf]
+    simp +instances only [IteratorLoop.forIn, IterM.DefaultConsumers.forIn'_eq_wf Pl wf]
     rw [IterM.DefaultConsumers.forIn'.wf]
     split; rotate_left
     · simp [IterM.step_eq, Monadic.step, Internal.LawfulMonadLiftBindFunction.liftBind_pure (liftBind := lift)]
@@ -1639,8 +1637,7 @@ instance Iterator.instLawfulIteratorLoop [UpwardEnumerable α]
     LawfulIteratorLoop (Rxi.Iterator α) Id n where
   lawful := by
     intro lift instLawfulMonadLiftFunction γ it init Pl wf f
-    simp +instances only [IteratorLoop.defaultImplementation, IteratorLoop.forIn,
-      IterM.DefaultConsumers.forIn'_eq_wf Pl wf]
+    simp +instances only [IteratorLoop.forIn, IterM.DefaultConsumers.forIn'_eq_wf Pl wf]
     rw [IterM.DefaultConsumers.forIn'.wf]
     split; rotate_left
     · simp [Monadic.step_eq_step, Monadic.step, Internal.LawfulMonadLiftBindFunction.liftBind_pure]

src/Init/Data/Range/Polymorphic/UpwardEnumerable.lean

@@ -438,6 +438,7 @@ protected theorem UpwardEnumerable.le_iff {α : Type u} [LE α] [UpwardEnumerabl
     [LawfulUpwardEnumerableLE α] {a b : α} : a ≤ b ↔ UpwardEnumerable.LE a b :=
   LawfulUpwardEnumerableLE.le_iff a b
 
+@[expose, implicit_reducible]
 def UpwardEnumerable.instLETransOfLawfulUpwardEnumerableLE {α : Type u} [LE α]
     [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] :
     Trans (α := α) (· ≤ ·) (· ≤ ·) (· ≤ ·) where
@@ -502,12 +503,13 @@ protected theorem UpwardEnumerable.lt_succ_iff {α : Type u} [UpwardEnumerable
       ← succMany?_eq_some_iff_succMany] at hn
     exact ⟨n, hn⟩
 
+@[expose, implicit_reducible]
 def UpwardEnumerable.instLTTransOfLawfulUpwardEnumerableLT {α : Type u} [LT α]
     [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] :
     Trans (α := α) (· < ·) (· < ·) (· < ·) where
   trans := by simpa [UpwardEnumerable.lt_iff] using @UpwardEnumerable.lt_trans
 
-def UpwardEnumerable.instLawfulOrderLTOfLawfulUpwardEnumerableLT {α : Type u} [LT α] [LE α]
+theorem UpwardEnumerable.instLawfulOrderLTOfLawfulUpwardEnumerableLT {α : Type u} [LT α] [LE α]
     [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
     [LawfulUpwardEnumerableLE α] :
     LawfulOrderLT α where

src/Lean/Elab/Deriving/TypeName.lean

@@ -19,11 +19,12 @@ private def deriveTypeNameInstance (declNames : Array Name) : CommandElabM Bool
     let cinfo ← getConstInfo declName
     unless cinfo.levelParams.isEmpty do
       throwError m!"{.ofConstName declName} has universe level parameters"
-    elabCommand <| ← withFreshMacroScope `(
-      unsafe def instImpl : TypeName @$(mkCIdent declName) := .mk _ $(quote declName)
-      @[implemented_by instImpl] opaque inst : TypeName @$(mkCIdent declName)
-      instance : TypeName @$(mkCIdent declName) := inst
-    )
+    withScope (fun scope => { scope with opts := scope.opts.setBool `warn.classDefReducibility false }) do
+      elabCommand <| ← withFreshMacroScope `(
+        unsafe def instImpl : TypeName @$(mkCIdent declName) := .mk _ $(quote declName)
+        @[implemented_by instImpl] opaque inst : TypeName @$(mkCIdent declName)
+        instance : TypeName @$(mkCIdent declName) := inst
+      )
   return true
 
 initialize

src/Lean/Elab/MutualDef.lean

@@ -1184,6 +1184,11 @@ private def checkAllDeclNamesDistinct (preDefs : Array PreDefinition) : TermElab
 structure AsyncBodyInfo where
 deriving TypeName
 
+register_builtin_option warn.classDefReducibility : Bool := {
+  defValue := true
+  descr    := "warn when a `def` of class type is not marked `@[reducible]` or `@[implicit_reducible]`"
+}
+
 register_builtin_option warn.exposeOnPrivate : Bool := {
   defValue := true
   descr    := "warn about uses of `@[expose]` on private declarations"
@@ -1225,9 +1230,11 @@ where
     -- Now that we have elaborated types, default data instances to `[implicit_reducible]`. This
     -- should happen before attribute application as `[instance]` will check for it.
     for header in headers do
-      if header.kind == .instance && !header.modifiers.anyAttr (·.name matches `reducible | `irreducible) then
-        if !(← isProp header.type) then
-          setReducibilityStatus header.declName .implicitReducible
+      -- TODO: remove `instance_reducible once the alias is deprecated
+      if !header.modifiers.anyAttr (·.name matches `reducible | `implicit_reducible | `instance_reducible | `irreducible) then
+        if header.kind == .instance then
+          if !(← isProp header.type) then
+            setReducibilityStatus header.declName .implicitReducible
 
     if let (#[view], #[declId]) := (views, expandedDeclIds) then
       if Elab.async.get (← getOptions) && view.kind.isTheorem &&
@@ -1237,6 +1244,18 @@ where
         elabAsync headers[0]! view declId
       else elabSync headers
     else elabSync headers
+
+    -- Warn about class-typed `def`s that aren't marked with a reducibility attribute.
+    -- This check runs after elaboration so that attributes applied by other attributes
+    -- (e.g. `to_additive (attr := implicit_reducible)`) are accounted for.
+    for header in headers do
+      if header.kind == .def then
+        if warn.classDefReducibility.get (← getOptions) &&
+            (← isClass? header.type).isSome /-TODO-/ &&
+            !header.type.getForallBody.getAppFn.constName? matches ``Decidable | ``DecidableEq | ``Setoid then
+          let status ← getReducibilityStatus header.declName
+          unless status matches .reducible | .implicitReducible | .irreducible do
+            logWarning m!"Definition `{header.declName}` of class type must be marked with `@[reducible]` or `@[implicit_reducible]`"
     for view in views, declId in expandedDeclIds do
       -- NOTE: this should be the full `ref`, and thus needs to be done after any snapshotting
       -- that depends only on a part of the ref

src/Std/Data/Iterators/Lemmas/Equivalence/HetT.lean

@@ -28,6 +28,7 @@ class ComputableSmall (α : Type v) where
 class Small (α : Type v) : Prop where
   h : Nonempty (ComputableSmall.{u} α)
 
+@[implicit_reducible]
 noncomputable def ComputableSmall.choose (α : Type v) [small : Small.{u} α] : ComputableSmall.{u} α :=
   haveI : Nonempty (ComputableSmall.{u} α) := Small.h
   Classical.ofNonempty (α := ComputableSmall.{u} α)
@@ -93,7 +94,7 @@ instance {α : Type v} {x : α} : Small.{u} (Subtype (· = x)) where
     inflate_deflate := by rintro ⟨_, rfl⟩; rfl
   }⟩
 
-def Small.of_surjective (α : Type v) {β : Type w} (f : α → β) [Small.{u} α]
+theorem Small.of_surjective (α : Type v) {β : Type w} (f : α → β) [Small.{u} α]
     (h : ∀ b, ∃ a, f a = b) : Small.{u} β where
   h := ⟨{
     Target := Quot (fun a a' : USquash α => f a.inflate = f a'.inflate)

stage0/src/stdlib_flags.h

@@ -1,5 +1,7 @@
 #include "util/options.h"
 
+// Dear CI, please build stage 2 first
+
 namespace lean {
 options get_default_options() {
     options opts;

tests/lean/2115.lean.expected.out

@@ -1,8 +1,12 @@
+2115.lean:16:0-16:36: warning: Definition `foo` of class type must be marked with `@[reducible]` or `@[implicit_reducible]`
 def foo : {α : Type} → [D α] → A α :=
 fun {α : Type} [inst : D α] => @inferInstance.{1} (A α) (@B.toA α (@D.toB α inst))
+2115.lean:21:0-21:36: warning: Definition `bla` of class type must be marked with `@[reducible]` or `@[implicit_reducible]`
 def bla : {α : Type} → [D α] → A α :=
 fun {α : Type} [inst : D α] => @inferInstance.{1} (A α) (@C.toA α (@D.toC α inst))
+2115.lean:26:0-26:36: warning: Definition `boo` of class type must be marked with `@[reducible]` or `@[implicit_reducible]`
 def boo : {α : Type} → [D α] → A α :=
 fun {α : Type} [inst : D α] => @inferInstance.{1} (A α) (@B.toA α (@D.toB α inst))
+2115.lean:31:0-31:37: warning: Definition `boo2` of class type must be marked with `@[reducible]` or `@[implicit_reducible]`
 def boo2 : {α : Type} → [D α] → A α :=
 fun {α : Type} [inst : D α] => @inferInstance.{1} (A α) (@C.toA α (@D.toC α inst))

tests/lean/2273.lean.expected.out

@@ -2,3 +2,4 @@
   P 37
 
 Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
+2273.lean:24:0-24:31: warning: Definition `instP` of class type must be marked with `@[reducible]` or `@[implicit_reducible]`

tests/lean/366.lean.expected.out

@@ -1,3 +1,4 @@
+366.lean:1:0-2:72: warning: Definition `foo` of class type must be marked with `@[reducible]` or `@[implicit_reducible]`
 [Meta.synthInstance] ✅️ Inhabited Nat
   [Meta.synthInstance] new goal Inhabited Nat
     [Meta.synthInstance.instances] #[@instInhabitedOfMonad, instInhabitedNat]

tests/lean/phashmap_inst_coherence.lean.expected.out

@@ -1,3 +1,4 @@
+phashmap_inst_coherence.lean:8:0-9:30: warning: Definition `natDiffHash` of class type must be marked with `@[reducible]` or `@[implicit_reducible]`
 phashmap_inst_coherence.lean:12:53-12:54: error: Application type mismatch: The argument
   m
 has type

tests/lean/run/1158.lean

@@ -1,3 +1,5 @@
+set_option warn.classDefReducibility false
+
 class magma (α) where op : α → α → α
 
 infix:70 " ⋆ " => magma.op (self := inferInstance)

tests/lean/run/1692.lean

@@ -1,5 +1,7 @@
 import Lean.Hygiene
 
+set_option warn.classDefReducibility false
+
 def otherInhabited : Inhabited Nat := ⟨42⟩
 
 def f := Id.run do

tests/lean/run/2461.lean

@@ -1,3 +1,5 @@
+set_option warn.classDefReducibility false
+
 section algebra_hierarchy_classes_to_comm_ring
 
 class Semiring (α : Type) extends Add α, Mul α, Zero α, One α

tests/lean/run/3965_2.lean

@@ -1,3 +1,5 @@
+set_option warn.classDefReducibility false
+
 section Mathlib.Init.Order.Defs
 
 universe u

tests/lean/run/3965_3.lean

@@ -1,3 +1,5 @@
+set_option warn.classDefReducibility false
+
 section Mathlib.Init.Order.Defs
 
 universe u

tests/lean/run/4171.lean

@@ -1,3 +1,5 @@
+set_option warn.classDefReducibility false
+
 /-!
 This is a minimization of a problem in Mathlib where a simp lemma `foo` would not fire,
 but variants:

tests/lean/run/4203.lean

@@ -16,6 +16,8 @@ error: failed to synthesize instance of type class
   Fintype v
 
 Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
+---
+warning: Definition `MappishOrder` of class type must be marked with `@[reducible]` or `@[implicit_reducible]`
 -/
 #guard_msgs in
 def MappishOrder [DecidableEq dIn] : Preorder

tests/lean/run/5176.lean

@@ -1,3 +1,5 @@
+set_option warn.classDefReducibility false
+
 class Foo where
 
 class Bar extends Foo where

tests/lean/run/6123_cat_adjunction.lean

@@ -1,3 +1,5 @@
+set_option warn.classDefReducibility false
+
 section Mathlib.CategoryTheory.ConcreteCategory.Bundled
 
 universe u v

tests/lean/run/616.lean

@@ -1,3 +1,5 @@
+set_option warn.classDefReducibility false
+
 def bug : Monad (λ α : Type _ => α → Prop) where
   pure x := (.=x)
   bind s f y := ∃ x, s x ∧ f x y

tests/lean/run/664.lean

@@ -1,3 +1,5 @@
+set_option warn.classDefReducibility false
+
 class A (α : Type _) where  a : α → Unit
 
 instance : A Empty where a x := nomatch x

tests/lean/run/796.lean

@@ -1,3 +1,5 @@
+set_option warn.classDefReducibility false
+
 namespace Ex1
 structure A
 class B (a : outParam A) (α : Sort u)

tests/lean/run/9624.lean

@@ -1,3 +1,5 @@
+set_option warn.classDefReducibility false
+
 set_option warn.sorry false
 
 inductive T : Type u where

tests/lean/run/KyleAlg.lean

@@ -1,5 +1,7 @@
 import Lean
 
+set_option warn.classDefReducibility false
+
 /- from core:
 class OfNat (α : Type u) (n : Nat) where
   ofNat : α

tests/lean/run/aStructPerfIssue.lean

@@ -1,3 +1,5 @@
+set_option warn.classDefReducibility false
+
 noncomputable section
 namespace MWE
 

tests/lean/run/binop_binrel_perf_issue.lean

@@ -1,3 +1,5 @@
+set_option warn.classDefReducibility false
+
 /-!
 This is a minimization of an `isDefEq` timeout from Mathlib.Algebra.Module.Submodule.Localization,
 where it is reasonably fast with `set_option backward.isDefEq.lazyWhnfCore false`,

tests/lean/run/classDefReducibilityAfterAttr.lean

@@ -0,0 +1,31 @@
+/-!
+# Class-typed `def` reducibility warning checks actual status
+
+The `classDefReducibility` warning should check the actual reducibility status
+after all attributes have been applied, not just syntactic modifiers.
+This ensures attributes that set reducibility during `.afterCompilation`
+(like Mathlib's `to_additive (attr := implicit_reducible)`) are respected.
+-/
+
+class Foo where
+  x : Nat
+
+/-! Warning should fire when no reducibility attribute is present. -/
+/-- warning: Definition `baz` of class type must be marked with `@[reducible]` or `@[implicit_reducible]` -/
+#guard_msgs in
+def baz : Foo := ⟨42⟩
+
+/-! No warning with direct `implicit_reducible`. -/
+#guard_msgs in
+@[implicit_reducible]
+def qux : Foo := ⟨42⟩
+
+/-! No warning with `reducible`. -/
+#guard_msgs in
+@[reducible]
+def quux : Foo := ⟨42⟩
+
+/-! No warning with `irreducible`. -/
+#guard_msgs in
+@[irreducible]
+def corge : Foo := ⟨42⟩

tests/lean/run/congrSimpMathlibIssue.lean

@@ -1,5 +1,7 @@
 import Lean.Elab.Term
 
+set_option warn.classDefReducibility false
+
 /-!
 # Turán's theorem
 -/

tests/lean/run/derivingBEq.lean

@@ -1,5 +1,7 @@
 module
 
+set_option warn.classDefReducibility false
+
 set_option deriving.beq.linear_construction_threshold 1000
 
 public section

tests/lean/run/derivingBEqLinear.lean

@@ -1,5 +1,7 @@
 module
 
+set_option warn.classDefReducibility false
+
 set_option deriving.beq.linear_construction_threshold 0
 
 public section

tests/lean/run/derivingInhabited.lean

@@ -1,5 +1,7 @@
 module
 
+set_option warn.classDefReducibility false
+
 inductive Foo (α : Type u) (β : Type v) where
   | mk₁ : α → Foo α β
   | mk₂ : List β → Foo α β

tests/lean/run/derivingNonempty.lean

@@ -1,5 +1,7 @@
 module
 
+set_option warn.classDefReducibility false
+
 inductive Foo (α : Type u) (β : Type v) where
   | mk₁ : α → Foo α β
   | mk₂ : List β → Foo α β

tests/lean/run/grind_cat2.lean

@@ -1,4 +1,6 @@
 module
+
+set_option warn.classDefReducibility false
 @[expose] public section
 -- import Lean.Meta.Tactic.Grind
 universe v v₁ v₂ v₃ u u₁ u₂ u₃

tests/lean/run/grind_section_var.lean

@@ -1,5 +1,7 @@
 import Std.Do
 
+set_option warn.classDefReducibility false
+
 /-
 Section variables should not be included.
 -/

tests/lean/run/inductionTacticBug.lean

@@ -1,3 +1,5 @@
+set_option warn.classDefReducibility false
+
 def ex {α} : Subsingleton (Squash α) := Subsingleton.intro $ by
   intro a b
   induction a using Squash.ind

tests/lean/run/instanceReducible.lean

@@ -2,6 +2,8 @@ module
 
 /-! Applying `[instance]` after the fact should check for appropriate reducibility. -/
 
+/-- warning: Definition `unexposed` of class type must be marked with `@[reducible]` or `@[implicit_reducible]` -/
+#guard_msgs in
 public def unexposed : Inhabited Nat := inferInstance
 
 /-- warning: instance `unexposed` must be marked with `@[expose]` -/
@@ -12,6 +14,8 @@ attribute [instance] unexposed
 #guard_msgs in
 attribute [local instance] unexposed
 
+/-- warning: Definition `exposed` of class type must be marked with `@[reducible]` or `@[implicit_reducible]` -/
+#guard_msgs in
 @[expose]
 public def exposed : Inhabited Nat := inferInstance
 

tests/lean/run/instanceUsingFalse.lean

@@ -1,3 +1,5 @@
+set_option warn.classDefReducibility false
+
 class WrappedNat (α : Type) where
   n : Nat
 

tests/lean/run/methodSpecs.lean

@@ -109,7 +109,11 @@ error: expected `aS` to be a type class instance, but its type `S` does not look
 #guard_msgs in @[method_specs] def aS : S := ⟨1⟩
 
 @[class] inductive indClass where | mk
-/-- error: `indClass` is not a structure -/
+/--
+error: `indClass` is not a structure
+---
+warning: Definition `instIndClass` of class type must be marked with `@[reducible]` or `@[implicit_reducible]`
+-/
 #guard_msgs in @[method_specs] def instIndClass : indClass := .mk
 
 -- This used to fail until we eta-reduced the field values

tests/lean/run/modAsClasses.lean

@@ -1,3 +1,5 @@
+set_option warn.classDefReducibility false
+
 class MyMod :=
 (a : Nat)
 

tests/lean/run/newfrontend1.lean

@@ -1,3 +1,5 @@
+set_option warn.classDefReducibility false
+
 def x := 1
 
 #check x

tests/lean/run/order.lean

@@ -1,6 +1,7 @@
-
 import Init.Data.Order.PackageFactories
 
+set_option warn.classDefReducibility false
+
 variable {α : Type u}
 
 opaque X : Type := Unit
@@ -60,7 +61,7 @@ end X
 
 section
 
-def packageWithoutSynthesizableInstances : Std.LinearOrderPackage X := .ofLE X {
+@[implicit_reducible] def packageWithoutSynthesizableInstances : Std.LinearOrderPackage X := .ofLE X {
   le := X.instLE
   decidableLE := X.instDecidableLE }
 
@@ -70,7 +71,7 @@ section
 
 attribute [local instance] X.LinearOrderPackage.packageOfLE
 
-def packageWithoutSynthesizableInstances' : Std.LinearOrderPackage X := .ofLE X {
+@[implicit_reducible] def packageWithoutSynthesizableInstances' : Std.LinearOrderPackage X := .ofLE X {
   le := X.instLE
   decidableLE := X.instDecidableLE
 }
@@ -90,11 +91,11 @@ this✝ : LT α := inferInstance
 ⊢ ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
 -/
 #guard_msgs in
-def packageOfLEOfLT1 [LE α] [DecidableLE α] [LT α] : Std.PreorderPackage α := .ofLE α {
+@[implicit_reducible] def packageOfLEOfLT1 [LE α] [DecidableLE α] [LT α] : Std.PreorderPackage α := .ofLE α {
   le_refl := sorry
   le_trans := sorry }
 
-def packageOfLEOfLT2 [LE α] [DecidableLE α] [LT α] (h : ∀ a b : α, a < b ↔ a ≤ b ∧ ¬ b ≤ a) :
+@[implicit_reducible] def packageOfLEOfLT2 [LE α] [DecidableLE α] [LT α] (h : ∀ a b : α, a < b ↔ a ≤ b ∧ ¬ b ≤ a) :
     Std.PreorderPackage α := .ofLE α {
   lt_iff := h
   le_refl := sorry
@@ -113,7 +114,7 @@ opaque _root_.X.instTransOrd : haveI := X.instOrd; Std.TransOrd X := sorry
 #guard_msgs(error, drop warning) in
 opaque _root_.X.instLawfulEqOrd : haveI := X.instOrd; Std.LawfulEqOrd X := sorry
 
-def packageWithoutSynthesizableInstances : Std.LinearOrderPackage X := .ofOrd X {
+@[implicit_reducible] def packageWithoutSynthesizableInstances : Std.LinearOrderPackage X := .ofOrd X {
   ord := X.instOrd
   transOrd := X.instTransOrd
   eq_of_compare := by
@@ -128,7 +129,7 @@ section WithSynthesizableInstances
 
 attribute [scoped instance] X.instOrd X.instTransOrd X.instLawfulEqOrd
 
-def packageWithSynthesizableInstances : Std.LinearOrderPackage X := .ofOrd X
+@[implicit_reducible] def packageWithSynthesizableInstances : Std.LinearOrderPackage X := .ofOrd X
 
 end WithSynthesizableInstances
 

tests/lean/run/propagateExpectedType.lean

@@ -1,3 +1,5 @@
+set_option warn.classDefReducibility false
+
 variable {α : Type _} (r : α → α → Prop) (π : α → α)
 
 inductive rel : α → α → Prop

tests/lean/run/simproc_timeout.lean

@@ -1,3 +1,5 @@
+set_option warn.classDefReducibility false
+
 -- Minimisation of a timeout triggered by leanprover/lean4#3124
 -- in Mathlib.Computability.PartrecCode
 

tests/lean/run/structInst2.lean

@@ -1,5 +1,7 @@
 import Init.Control.Option
 
+set_option warn.classDefReducibility false
+
 
 universe u v
 

tests/lean/run/structWithAlgTCSynth.lean

@@ -1,3 +1,5 @@
+set_option warn.classDefReducibility false
+
 /-!
 # Testing for timeouts in typeclass synthesis
 

tests/lean/run/synthInstsIssue.lean

@@ -1,3 +1,5 @@
+set_option warn.classDefReducibility false
+
 /-!
 This is a minimization of an issue widely seen in Mathlib after
 https://github.com/leanprover/lean4/pull/2793.

tests/lean/run/typeclass_diamond.lean

@@ -1,3 +1,5 @@
+set_option warn.classDefReducibility false
+
 class Top₁   (n : Nat) : Type := (u : Unit := ())
 class Bot₁   (n : Nat) : Type := (u : Unit := ())
 class Left₁  (n : Nat) : Type := (u : Unit := ())

tests/lean/scopedInstanceOutsideNamespace.lean.expected.out

@@ -4,3 +4,4 @@ scopedInstanceOutsideNamespace.lean:6:0-6:30: error: Scoped attributes must be u
 scopedInstanceOutsideNamespace.lean:6:0-6:30: error: invalid syntax node kind `«term_+__1»`
 scopedInstanceOutsideNamespace.lean:6:0-6:30: error: Scoped attributes must be used inside namespaces
 scopedInstanceOutsideNamespace.lean:8:2-8:17: error: Scoped attributes must be used inside namespaces
+scopedInstanceOutsideNamespace.lean:8:0-10:38: warning: Definition `myInst` of class type must be marked with `@[reducible]` or `@[implicit_reducible]`

tests/lean/tcloop.lean.expected.out

@@ -7,3 +7,4 @@ Note: Use `set_option synthInstance.maxHeartbeats <num>` to set the limit.
 Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
 
 Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+tcloop.lean:13:0-14:15: warning: Definition `f` of class type must be marked with `@[reducible]` or `@[implicit_reducible]`

tests/pkg/module/Module/Imported.lean

@@ -70,6 +70,8 @@ error: failed to synthesize instance of type class
   X
 
 Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
+---
+warning: Definition `_private.Module.Imported.0.fX` of class type must be marked with `@[reducible]` or `@[implicit_reducible]`
 -/
 #guard_msgs in
 def fX : X := inferInstance