fix test moddoc

src/Init/Classical.lean

@@ -142,6 +142,7 @@ is classically true but not constructively. -/
 
 /-- Transfer decidability of `¬ p` to decidability of `p`. -/
 -- This can not be an instance as it would be tried everywhere.
+@[instance_reducible]
 def decidable_of_decidable_not (p : Prop) [h : Decidable (¬ p)] : Decidable p :=
   match h with
   | isFalse h => isTrue (Classical.not_not.mp h)

src/Init/Control/MonadAttach.lean

@@ -70,7 +70,7 @@ information to the return value, except a trivial proof of {name}`True`.
 This instance is used whenever no more useful {name}`MonadAttach` instance can be implemented.
 It always has a {name}`WeaklyLawfulMonadAttach`, but usually no {name}`LawfulMonadAttach` instance.
 -/
-@[expose]
+@[expose, instance_reducible]
 public protected def MonadAttach.trivial {m : Type u → Type v} [Monad m] : MonadAttach m where
   CanReturn _ _ := True
   attach x := (⟨·, .intro⟩) <$> x

src/Init/Data/Bool.lean

@@ -636,7 +636,7 @@ def boolPredToPred : Coe (α → Bool) (α  → Prop) where
 This should not be turned on globally as an instance because it degrades performance in Mathlib,
 but may be used locally.
 -/
-@[expose] def boolRelToRel : Coe (α → α → Bool) (α → α → Prop) where
+@[expose, instance_reducible] def boolRelToRel : Coe (α → α → Bool) (α → α → Prop) where
   coe r := fun a b => Eq (r a b) true
 
 /-! ### subtypes -/

src/Init/Data/Char/Lemmas.lean

@@ -48,6 +48,7 @@ instance ltTrans : Trans (· < · : Char → Char → Prop) (· < ·) (· < ·)
   trans := Char.lt_trans
 
 -- This instance is useful while setting up instances for `String`.
+@[instance_reducible]
 def notLTTrans : Trans (¬ · < · : Char → Char → Prop) (¬ · < ·) (¬ · < ·) where
   trans h₁ h₂ := by simpa using Char.le_trans (by simpa using h₂) (by simpa using h₁)
 

src/Init/Data/Fin/Lemmas.lean

@@ -118,7 +118,7 @@ For example, for `x : Fin k` and `n : Nat`,
 it causes `x < n` to be elaborated as `x < ↑n` rather than `↑x < n`,
 silently introducing wraparound arithmetic.
 -/
-@[expose]
+@[expose, instance_reducible]
 def instNatCast (n : Nat) [NeZero n] : NatCast (Fin n) where
   natCast a := Fin.ofNat n a
 
@@ -140,7 +140,7 @@ This is not a global instance, but may be activated locally via `open Fin.IntCas
 
 See the doc-string for `Fin.NatCast.instNatCast` for more details.
 -/
-@[expose]
+@[expose, instance_reducible]
 def instIntCast (n : Nat) [NeZero n] : IntCast (Fin n) where
   intCast := Fin.intCast
 

src/Init/Data/Ord/Basic.lean

@@ -609,21 +609,22 @@ protected theorem compare_nil_right_eq_eq {α} [Ord α] {xs : List α} :
 end List
 
 /-- The lexicographic order on pairs. -/
-@[expose] def lexOrd [Ord α] [Ord β] : Ord (α × β) where
+@[expose, instance_reducible]
+def lexOrd [Ord α] [Ord β] : Ord (α × β) where
   compare := compareLex (compareOn (·.1)) (compareOn (·.2))
 
 /--
 Constructs an `BEq` instance from an `Ord` instance that asserts that the result of `compare` is
 `Ordering.eq`.
 -/
-@[expose] def beqOfOrd [Ord α] : BEq α where
+@[expose, instance_reducible] def beqOfOrd [Ord α] : BEq α where
   beq a b := (compare a b).isEq
 
 /--
 Constructs an `LT` instance from an `Ord` instance that asserts that the result of `compare` is
 `Ordering.lt`.
 -/
-@[expose] def ltOfOrd [Ord α] : LT α where
+@[expose, instance_reducible] def ltOfOrd [Ord α] : LT α where
   lt a b := compare a b = Ordering.lt
 
 @[inline]

src/Init/Data/Order/Factories.lean

@@ -23,7 +23,7 @@ preferring `a` over `b` when in doubt.
 
 Has a `LawfulOrderLeftLeaningMin α` instance.
 -/
-@[inline]
+@[inline, instance_reducible]
 public def _root_.Min.leftLeaningOfLE (α : Type u) [LE α] [DecidableLE α] : Min α where
   min a b := if a ≤ b then a else b
 
@@ -33,7 +33,7 @@ preferring `a` over `b` when in doubt.
 
 Has a `LawfulOrderLeftLeaningMax α` instance.
 -/
-@[inline]
+@[inline, instance_reducible]
 public def _root_.Max.leftLeaningOfLE (α : Type u) [LE α] [DecidableLE α] : Max α where
   max a b := if b ≤ a then a else b
 

src/Init/Data/Order/FactoriesExtra.lean

@@ -18,7 +18,7 @@ Creates an `LE α` instance from an `Ord α` instance.
 `OrientedOrd α` must be satisfied so that the resulting `LE α` instance faithfully represents
 the `Ord α` instance.
 -/
-@[inline, expose]
+@[inline, expose, instance_reducible]
 public def _root_.LE.ofOrd (α : Type u) [Ord α] : LE α where
   le a b := (compare a b).isLE
 
@@ -38,7 +38,7 @@ Creates an `LT α` instance from an `Ord α` instance.
 `OrientedOrd α` must be satisfied so that the resulting `LT α` instance faithfully represents
 the `Ord α` instance.
 -/
-@[inline, expose]
+@[inline, expose, instance_reducible]
 public def _root_.LT.ofOrd (α : Type u) [Ord α] :
     LT α where
   lt a b := compare a b = .lt
@@ -82,7 +82,7 @@ public def _root_.DecidableLT.ofOrd (α : Type u) [LE α] [LT α] [Ord α] [Lawf
 
 /--
 Creates a `BEq α` instance from an `Ord α` instance. -/
-@[inline, expose]
+@[inline, expose, instance_reducible]
 public def _root_.BEq.ofOrd (α : Type u) [Ord α] :
     BEq α where
   beq a b := compare a b = .eq

src/Init/Data/SInt/Basic.lean

@@ -409,7 +409,7 @@ Examples:
  * `(if (5 : Int8) < 5 then "yes" else "no") = "no"`
  * `show ¬((7 : Int8) < 7) by decide`
 -/
-@[extern "lean_int8_dec_lt"]
+@[extern "lean_int8_dec_lt", instance_reducible]
 def Int8.decLt (a b : Int8) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
 
@@ -425,7 +425,7 @@ Examples:
  * `(if (15 : Int8) ≤ 5 then "yes" else "no") = "no"`
  * `show (7 : Int8) ≤ 7 by decide`
 -/
-@[extern "lean_int8_dec_le"]
+@[extern "lean_int8_dec_le", instance_reducible]
 def Int8.decLe (a b : Int8) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
 
@@ -778,7 +778,7 @@ Examples:
  * `(if (5 : Int16) < 5 then "yes" else "no") = "no"`
  * `show ¬((7 : Int16) < 7) by decide`
 -/
-@[extern "lean_int16_dec_lt"]
+@[extern "lean_int16_dec_lt", instance_reducible]
 def Int16.decLt (a b : Int16) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
 
@@ -794,7 +794,7 @@ Examples:
  * `(if (15 : Int16) ≤ 5 then "yes" else "no") = "no"`
  * `show (7 : Int16) ≤ 7 by decide`
 -/
-@[extern "lean_int16_dec_le"]
+@[extern "lean_int16_dec_le", instance_reducible]
 def Int16.decLe (a b : Int16) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
 
@@ -1163,7 +1163,7 @@ Examples:
  * `(if (5 : Int32) < 5 then "yes" else "no") = "no"`
  * `show ¬((7 : Int32) < 7) by decide`
 -/
-@[extern "lean_int32_dec_lt"]
+@[extern "lean_int32_dec_lt", instance_reducible]
 def Int32.decLt (a b : Int32) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
 
@@ -1179,7 +1179,7 @@ Examples:
  * `(if (15 : Int32) ≤ 5 then "yes" else "no") = "no"`
  * `show (7 : Int32) ≤ 7 by decide`
 -/
-@[extern "lean_int32_dec_le"]
+@[extern "lean_int32_dec_le", instance_reducible]
 def Int32.decLe (a b : Int32) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
 
@@ -1568,7 +1568,7 @@ Examples:
  * `(if (5 : Int64) < 5 then "yes" else "no") = "no"`
  * `show ¬((7 : Int64) < 7) by decide`
 -/
-@[extern "lean_int64_dec_lt"]
+@[extern "lean_int64_dec_lt", instance_reducible]
 def Int64.decLt (a b : Int64) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
 /--
@@ -1583,7 +1583,7 @@ Examples:
  * `(if (15 : Int64) ≤ 5 then "yes" else "no") = "no"`
  * `show (7 : Int64) ≤ 7 by decide`
 -/
-@[extern "lean_int64_dec_le"]
+@[extern "lean_int64_dec_le", instance_reducible]
 def Int64.decLe (a b : Int64) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
 
@@ -1958,7 +1958,7 @@ Examples:
  * `(if (5 : ISize) < 5 then "yes" else "no") = "no"`
  * `show ¬((7 : ISize) < 7) by decide`
 -/
-@[extern "lean_isize_dec_lt"]
+@[extern "lean_isize_dec_lt", instance_reducible]
 def ISize.decLt (a b : ISize) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
 
@@ -1974,7 +1974,7 @@ Examples:
  * `(if (15 : ISize) ≤ 5 then "yes" else "no") = "no"`
  * `show (7 : ISize) ≤ 7 by decide`
 -/
-@[extern "lean_isize_dec_le"]
+@[extern "lean_isize_dec_le", instance_reducible]
 def ISize.decLe (a b : ISize) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
 

src/Init/Data/Slice/Array/Iterator.lean

@@ -61,7 +61,7 @@ instance SubarrayIterator.instFinite : Finite (SubarrayIterator α) Id :=
 
 instance [Monad m] : IteratorLoop (SubarrayIterator α) Id m := .defaultImplementation
 
-@[inline, expose]
+@[inline, expose, instance_reducible]
 def Subarray.instToIterator :=
   ToIterator.of (γ := Slice (Internal.SubarrayData α)) (β := α) (SubarrayIterator α) (⟨⟨·⟩⟩)
 attribute [instance] Subarray.instToIterator

src/Init/Data/Slice/List/Iterator.lean

@@ -24,7 +24,7 @@ open Std Slice PRange Iterators
 
 variable {α : Type u}
 
-@[inline, expose]
+@[inline, expose, instance_reducible]
 def ListSlice.instToIterator :=
   ToIterator.of (γ := Slice (Internal.ListSliceData α)) _ (fun s => match s.internalRepresentation.stop with
       | some n => s.internalRepresentation.list.iter.take n

src/Init/Data/UInt/Basic.lean

@@ -373,7 +373,7 @@ Examples:
  * `(if (5 : UInt16) < 5 then "yes" else "no") = "no"`
  * `show ¬((7 : UInt16) < 7) by decide`
 -/
-@[extern "lean_uint16_dec_lt"]
+@[extern "lean_uint16_dec_lt", instance_reducible]
 def UInt16.decLt (a b : UInt16) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))
 
@@ -390,7 +390,7 @@ Examples:
  * `(if (5 : UInt16) ≤ 15 then "yes" else "no") = "yes"`
  * `show (7 : UInt16) ≤ 7 by decide`
 -/
-@[extern "lean_uint16_dec_le"]
+@[extern "lean_uint16_dec_le", instance_reducible]
 def UInt16.decLe (a b : UInt16) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))
 
@@ -737,7 +737,7 @@ Examples:
  * `(if (5 : UInt64) < 5 then "yes" else "no") = "no"`
  * `show ¬((7 : UInt64) < 7) by decide`
 -/
-@[extern "lean_uint64_dec_lt"]
+@[extern "lean_uint64_dec_lt", instance_reducible]
 def UInt64.decLt (a b : UInt64) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))
 
@@ -753,7 +753,7 @@ Examples:
  * `(if (5 : UInt64) ≤ 15 then "yes" else "no") = "yes"`
  * `show (7 : UInt64) ≤ 7 by decide`
 -/
-@[extern "lean_uint64_dec_le"]
+@[extern "lean_uint64_dec_le", instance_reducible]
 def UInt64.decLe (a b : UInt64) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))
 

src/Init/Data/UInt/BasicAux.lean

@@ -397,7 +397,7 @@ Examples:
  * `(if (5 : USize) < 5 then "yes" else "no") = "no"`
  * `show ¬((7 : USize) < 7) by decide`
 -/
-@[extern "lean_usize_dec_lt"]
+@[extern "lean_usize_dec_lt", instance_reducible]
 def USize.decLt (a b : USize) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))
 
@@ -413,7 +413,7 @@ Examples:
  * `(if (5 : USize) ≤ 15 then "yes" else "no") = "yes"`
  * `show (7 : USize) ≤ 7 by decide`
 -/
-@[extern "lean_usize_dec_le"]
+@[extern "lean_usize_dec_le", instance_reducible]
 def USize.decLe (a b : USize) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))
 

src/Init/Data/Vector/Algebra.lean

@@ -74,6 +74,7 @@ def mul [Mul α] (xs ys : Vector α n) : Vector α n :=
 Pointwise multiplication of vectors.
 This is not a global instance as in some applications different multiplications may be relevant.
 -/
+@[instance_reducible]
 def instMul [Mul α] : Mul (Vector α n) := ⟨mul⟩
 
 section mul

src/Init/Grind/Module/Basic.lean

@@ -60,6 +60,7 @@ class NatModule (M : Type u) extends AddCommMonoid M where
   /-- Scalar multiplication by a successor. -/
   add_one_nsmul : ∀ n : Nat, ∀ a : M, (n + 1) • a = n • a + a
 
+attribute [instance_reducible] NatModule.nsmul
 attribute [instance 100] NatModule.toAddCommMonoid NatModule.nsmul
 
 /--
@@ -82,6 +83,7 @@ class IntModule (M : Type u) extends AddCommGroup M where
   /-- Scalar multiplication by natural numbers is consistent with scalar multiplication by integers. -/
   zsmul_natCast_eq_nsmul : ∀ n : Nat, ∀ a : M, (n : Int) • a = n • a
 
+attribute [instance_reducible] IntModule.zsmul
 attribute [instance 100] IntModule.toAddCommGroup IntModule.zsmul
 
 namespace IntModule

src/Init/Grind/Module/Envelope.lean

@@ -203,6 +203,7 @@ theorem zsmul_natCast_eq_nsmul (n : Nat) (a : Q α) : zsmul (n : Int) a = nsmul
   induction a using Q.ind with | _ a
   rcases a with ⟨a₁, a₂⟩; simp; omega
 
+@[instance_reducible]
 def ofNatModule : IntModule (Q α) := {
   nsmul := ⟨nsmul⟩,
   zsmul := ⟨zsmul⟩,

src/Init/Grind/Ring/Basic.lean

@@ -88,6 +88,8 @@ class Semiring (α : Type u) extends Add α, Mul α where
   -/
   nsmul_eq_natCast_mul : ∀ n : Nat, ∀ a : α, n • a = Nat.cast n * a := by intros; rfl
 
+attribute [instance_reducible] Semiring.npow Semiring.ofNat Semiring.natCast
+
 /--
 A ring, i.e. a type equipped with addition, negation, multiplication, and a map from the integers,
 satisfying appropriate compatibilities.
@@ -112,6 +114,8 @@ class Ring (α : Type u) extends Semiring α, Neg α, Sub α where
   /-- The canonical map from the integers is consistent with negation. -/
   intCast_neg : ∀ i : Int, Int.cast (R := α) (-i) = -Int.cast i := by intros; rfl
 
+attribute [instance_reducible] Ring.intCast Ring.zsmul
+
 /--
 A commutative semiring, i.e. a semiring with commutative multiplication.
 

src/Init/Grind/Ring/Envelope.lean

@@ -244,6 +244,7 @@ theorem neg_zsmul (i : Int) (a : Q α) : zsmul (-i) a = neg (zsmul i a) := by
     · have : i = 0 := by omega
       simp [this]
 
+@[instance_reducible]
 def ofSemiring : Ring (Q α) := {
   nsmul := ⟨nsmul⟩
   zsmul := ⟨zsmul⟩
@@ -504,6 +505,7 @@ theorem mul_comm (a b : OfSemiring.Q α) : OfSemiring.mul a b = OfSemiring.mul b
   obtain ⟨⟨b₁, b₂⟩⟩ := b
   apply Quot.sound; refine ⟨0, ?_⟩; simp; ac_rfl
 
+@[instance_reducible]
 def ofCommSemiring : CommRing (OfSemiring.Q α) :=
   { OfSemiring.ofSemiring with
     mul_comm := mul_comm }

src/Init/Grind/Ring/Field.lean

@@ -33,6 +33,7 @@ class Field (α : Type u) extends CommRing α, Inv α, Div α where
   /-- Raising to a negative power is the inverse of raising to the positive power. -/
   zpow_neg : ∀ (a : α) (n : Int), a ^ (-n) = (a ^ n)⁻¹
 
+attribute [instance_reducible] Field.zpow
 attribute [instance 100] Field.toInv Field.toDiv Field.zpow
 
 namespace Field

src/Init/GrindInstances/Ring/SInt.lean

@@ -15,11 +15,11 @@ public section
 
 namespace Lean.Grind
 
-@[expose]
+@[expose, instance_reducible]
 def Int8.natCast : NatCast Int8 where
   natCast x := Int8.ofNat x
 
-@[expose]
+@[expose, instance_reducible]
 def Int8.intCast : IntCast Int8 where
   intCast x := Int8.ofInt x
 
@@ -70,11 +70,11 @@ example : ToInt.Sub Int8 (.sint 8) := inferInstance
 
 instance : ToInt.Pow Int8 (.sint 8) := ToInt.pow_of_semiring (by simp)
 
-@[expose]
+@[expose, instance_reducible]
 def Int16.natCast : NatCast Int16 where
   natCast x := Int16.ofNat x
 
-@[expose]
+@[expose, instance_reducible]
 def Int16.intCast : IntCast Int16 where
   intCast x := Int16.ofInt x
 
@@ -125,11 +125,11 @@ example : ToInt.Sub Int16 (.sint 16) := inferInstance
 
 instance : ToInt.Pow Int16 (.sint 16) := ToInt.pow_of_semiring (by simp)
 
-@[expose]
+@[expose, instance_reducible]
 def Int32.natCast : NatCast Int32 where
   natCast x := Int32.ofNat x
 
-@[expose]
+@[expose, instance_reducible]
 def Int32.intCast : IntCast Int32 where
   intCast x := Int32.ofInt x
 
@@ -180,11 +180,11 @@ example : ToInt.Sub Int32 (.sint 32) := inferInstance
 
 instance : ToInt.Pow Int32 (.sint 32) := ToInt.pow_of_semiring (by simp)
 
-@[expose]
+@[expose, instance_reducible]
 def Int64.natCast : NatCast Int64 where
   natCast x := Int64.ofNat x
 
-@[expose]
+@[expose, instance_reducible]
 def Int64.intCast : IntCast Int64 where
   intCast x := Int64.ofInt x
 
@@ -235,11 +235,11 @@ example : ToInt.Sub Int64 (.sint 64) := inferInstance
 
 instance : ToInt.Pow Int64 (.sint 64) := ToInt.pow_of_semiring (by simp)
 
-@[expose]
+@[expose, instance_reducible]
 def ISize.natCast : NatCast ISize where
   natCast x := ISize.ofNat x
 
-@[expose]
+@[expose, instance_reducible]
 def ISize.intCast : IntCast ISize where
   intCast x := ISize.ofInt x
 

src/Init/GrindInstances/Ring/UInt.lean

@@ -17,11 +17,11 @@ namespace UInt8
 /-- Variant of `UInt8.ofNat_mod_size` replacing `2 ^ 8` with `256`.-/
 theorem ofNat_mod_size' : ofNat (x % 256) = ofNat x := ofNat_mod_size
 
-@[expose]
+@[expose, instance_reducible]
 def natCast : NatCast UInt8 where
   natCast x := UInt8.ofNat x
 
-@[expose]
+@[expose, instance_reducible]
 def intCast : IntCast UInt8 where
   intCast x := UInt8.ofInt x
 
@@ -47,11 +47,11 @@ namespace UInt16
 /-- Variant of `UInt16.ofNat_mod_size` replacing `2 ^ 16` with `65536`.-/
 theorem ofNat_mod_size' : ofNat (x % 65536) = ofNat x := ofNat_mod_size
 
-@[expose]
+@[expose, instance_reducible]
 def natCast : NatCast UInt16 where
   natCast x := UInt16.ofNat x
 
-@[expose]
+@[expose, instance_reducible]
 def intCast : IntCast UInt16 where
   intCast x := UInt16.ofInt x
 
@@ -77,11 +77,11 @@ namespace UInt32
 /-- Variant of `UInt32.ofNat_mod_size` replacing `2 ^ 32` with `4294967296`.-/
 theorem ofNat_mod_size' : ofNat (x % 4294967296) = ofNat x := ofNat_mod_size
 
-@[expose]
+@[expose, instance_reducible]
 def natCast : NatCast UInt32 where
   natCast x := UInt32.ofNat x
 
-@[expose]
+@[expose, instance_reducible]
 def intCast : IntCast UInt32 where
   intCast x := UInt32.ofInt x
 
@@ -107,11 +107,11 @@ namespace UInt64
 /-- Variant of `UInt64.ofNat_mod_size` replacing `2 ^ 64` with `18446744073709551616`.-/
 theorem ofNat_mod_size' : ofNat (x % 18446744073709551616) = ofNat x := ofNat_mod_size
 
-@[expose]
+@[expose, instance_reducible]
 def natCast : NatCast UInt64 where
   natCast x := UInt64.ofNat x
 
-@[expose]
+@[expose, instance_reducible]
 def intCast : IntCast UInt64 where
   intCast x := UInt64.ofInt x
 
@@ -134,11 +134,11 @@ end UInt64
 
 namespace USize
 
-@[expose]
+@[expose, instance_reducible]
 def natCast : NatCast USize where
   natCast x := USize.ofNat x
 
-@[expose]
+@[expose, instance_reducible]
 def intCast : IntCast USize where
   intCast x := USize.ofInt x
 

src/Init/Prelude.lean

@@ -2478,7 +2478,7 @@ Examples:
  * `(if (5 : UInt8) < 5 then "yes" else "no") = "no"`
  * `show ¬((7 : UInt8) < 7) by decide`
 -/
-@[extern "lean_uint8_dec_lt"]
+@[extern "lean_uint8_dec_lt", instance_reducible]
 def UInt8.decLt (a b : UInt8) : Decidable (LT.lt a b) :=
   inferInstanceAs (Decidable (LT.lt a.toBitVec b.toBitVec))
 
@@ -2494,7 +2494,7 @@ Examples:
  * `(if (5 : UInt8) ≤ 15 then "yes" else "no") = "yes"`
  * `show (7 : UInt8) ≤ 7 by decide`
 -/
-@[extern "lean_uint8_dec_le"]
+@[extern "lean_uint8_dec_le", instance_reducible]
 def UInt8.decLe (a b : UInt8) : Decidable (LE.le a b) :=
   inferInstanceAs (Decidable (LE.le a.toBitVec b.toBitVec))
 
@@ -2638,7 +2638,7 @@ Examples:
  * `(if (5 : UInt32) < 5 then "yes" else "no") = "no"`
  * `show ¬((7 : UInt32) < 7) by decide`
 -/
-@[extern "lean_uint32_dec_lt"]
+@[extern "lean_uint32_dec_lt", instance_reducible]
 def UInt32.decLt (a b : UInt32) : Decidable (LT.lt a b) :=
   inferInstanceAs (Decidable (LT.lt a.toBitVec b.toBitVec))
 
@@ -2654,7 +2654,7 @@ Examples:
  * `(if (5 : UInt32) ≤ 15 then "yes" else "no") = "yes"`
  * `show (7 : UInt32) ≤ 7 by decide`
 -/
-@[extern "lean_uint32_dec_le"]
+@[extern "lean_uint32_dec_le", instance_reducible]
 def UInt32.decLe (a b : UInt32) : Decidable (LE.le a b) :=
   inferInstanceAs (Decidable (LE.le a.toBitVec b.toBitVec))
 

src/Lean/Elab/DefView.lean

@@ -162,15 +162,9 @@ def mkDefViewOfTheorem (modifiers : Modifiers) (stx : Syntax) : DefView :=
 
 def mkDefViewOfInstance (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefView := do
   -- leading_parser Term.attrKind >> "instance " >> optNamedPrio >> optional declId >> declSig >> declVal
-  /-
-  **Note**: add `instance_reducible` attribute if declaration is not already marked with `@[reducible]`
-  -/
-  let modifiers       := if modifiers.anyAttr fun attr => attr.name == `reducible then
-    modifiers
-  else
-    modifiers.addAttr { name := `instance_reducible }
   let attrKind        ← liftMacroM <| toAttributeKind stx[0]
   let prio            ← liftMacroM <| expandOptNamedPrio stx[2]
+  -- NOTE: `[instance_reducible]` is added conditionally in `elabMutualDef`
   let attrStx         ← `(attr| instance $(quote prio):num)
   let modifiers       := modifiers.addAttr { kind := attrKind, name := `instance, stx := attrStx }
   let (binders, type) := expandDeclSig stx[4]

src/Lean/Elab/MutualDef.lean

@@ -1221,6 +1221,14 @@ where
     withSaveInfoContext do  -- save adjusted env in info tree
     let headers ← elabHeaders views expandedDeclIds bodyPromises tacPromises
     let headers ← levelMVarToParamHeaders views headers
+
+    -- Now that we have elaborated types, default data instances to `[instance_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 .instanceReducible
+
     if let (#[view], #[declId]) := (views, expandedDeclIds) then
       if Elab.async.get (← getOptions) && view.kind.isTheorem &&
           !deprecated.oldSectionVars.get (← getOptions) &&

src/Lean/Meta/GetUnfoldableConst.lean

@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Lean.Meta.GlobalInstances -- **TODO**: Delete after update stage0
+public import Lean.Meta.Basic
 import Lean.ReducibilityAttrs
 public section
 namespace Lean.Meta
@@ -19,8 +19,7 @@ private def canUnfoldDefault (cfg : Config) (info : ConstantInfo) : CoreM Bool :
     let status ← getReducibilityStatus info.name
     if status == .reducible then
       return true
-    -- **TODO**: Delete `isGlobalInstance` after update stage0
-    else if m == .instances && (isGlobalInstance (← getEnv) info.name || status == .instanceReducible) then
+    else if m == .instances && status == .instanceReducible then
       return true
     else
       return false

src/Lean/Meta/GlobalInstances.lean

@@ -1,28 +0,0 @@
-/-
-Copyright (c) 2021 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-module
-
-prelude
-public import Lean.Meta.Basic
-
-public section
-
-namespace Lean.Meta
-
-builtin_initialize globalInstanceExtension : SimpleScopedEnvExtension Name (PersistentHashMap Name Unit)  ←
-  registerSimpleScopedEnvExtension {
-    initial  := {}
-    addEntry := fun s n => s.insert n ()
-  }
-
-def addGlobalInstance (declName : Name) (attrKind : AttributeKind) : MetaM Unit := do
-  globalInstanceExtension.add declName attrKind
-
-@[export lean_is_instance]
-def isGlobalInstance (env : Environment) (declName : Name) : Bool :=
-  globalInstanceExtension.getState env |>.contains declName
-
-end Lean.Meta

src/Lean/Meta/Instances.lean

@@ -10,6 +10,7 @@ public import Lean.Meta.DiscrTree.Main
 public import Lean.Meta.CollectMVars
 import Lean.ReducibilityAttrs
 import Lean.Meta.WHNF
+import Lean.AddDecl
 public section
 namespace Lean.Meta
 
@@ -235,10 +236,9 @@ def addInstance (declName : Name) (attrKind : AttributeKind) (prio : Nat) : Meta
   unless status matches .reducible | .instanceReducible do
     let info ← getConstInfo declName
     if info.isDefinition then
-      -- **TODO**: uncomment after update stage0
-      -- logWarning m!"instance `{declName}` must be marked with @[reducible] or @[instance_reducible]"
-      pure ()
-  addGlobalInstance declName attrKind
+      logWarning m!"instance `{declName}` must be marked with `@[reducible]` or `@[instance_reducible]`"
+    else if wasOriginallyDefn (← getEnv) declName then
+      logWarning m!"instance `{declName}` must be marked with `@[expose]`"
   let projInfo? ← getProjectionFnInfo? declName
   let synthOrder ← computeSynthOrder c projInfo?
   instanceExtension.add { keys, val := c, priority := prio, globalName? := declName, attrKind, synthOrder } attrKind
@@ -368,15 +368,4 @@ def getDefaultInstancesPriorities [Monad m] [MonadEnv m] : m PrioritySet :=
 def getDefaultInstances [Monad m] [MonadEnv m] (className : Name) : m (List (Name × Nat)) :=
   return defaultInstanceExtension.getState (← getEnv) |>.defaultInstances.find? className |>.getD []
 
-end Meta
-
--- **TODO**: Move to `ReducibilityAttrs.lean` after update stage0
-def isInstanceReducibleCore (env : Environment) (declName : Name) : Bool :=
-  getReducibilityStatusCore env declName matches .instanceReducible
-    || Meta.isInstanceCore env declName -- **TODO**: Delete after update stage0
-
-/-- Return `true` if the given declaration has been marked as `[instance_reducible]`. -/
-def isInstanceReducible [Monad m] [MonadEnv m] (declName : Name) : m Bool :=
-  return isInstanceReducibleCore (← getEnv) declName
-
-end Lean
+end Lean.Meta

src/Lean/Meta/WHNF.lean

@@ -490,7 +490,8 @@ def canUnfoldAtMatcher (cfg : Config) (info : ConstantInfo) : CoreM Bool := do
   | .all     => return true
   | .default => return !(← isIrreducible info.name)
   | _ =>
-    if (← isReducible info.name) || isGlobalInstance (← getEnv) info.name then
+    let status ← getReducibilityStatus info.name
+    if status matches .reducible | .instanceReducible then
       return true
     else if hasMatchPatternAttribute (← getEnv) info.name then
       return true

src/Lean/ReducibilityAttrs.lean

@@ -4,12 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.ScopedEnvExtension
-
+import Lean.OriginalConstKind
 public section
-
 namespace Lean
 
 /--
@@ -126,8 +124,8 @@ private def validate (declName : Name) (status : ReducibilityStatus) (attrKind :
         unless statusOld matches .semireducible do
           throwError "failed to set `[reducible]`, `{.ofConstName declName}` is not currently `[semireducible]`, but `{statusOld.toAttrString}`{suffix}"
       | .irreducible =>
-        unless statusOld matches .semireducible do
-          throwError "failed to set `[irreducible]`, `{.ofConstName declName}` is not currently `[semireducible]`, but `{statusOld.toAttrString}`{suffix}"
+        unless statusOld matches .semireducible | .instanceReducible do
+          throwError "failed to set `[irreducible]`, `{.ofConstName declName}` is not currently `[semireducible]` nor `[instance_reducible]`, but `{statusOld.toAttrString}`{suffix}"
       | .instanceReducible =>
         unless statusOld matches .semireducible do
           throwError "failed to set `[instance_reducible]`, `{.ofConstName declName}` is not currently `[semireducible]`, but `{statusOld.toAttrString}`{suffix}"
@@ -138,8 +136,8 @@ private def validate (declName : Name) (status : ReducibilityStatus) (attrKind :
       | .reducible =>
         throwError "failed to set `[local reducible]` for `{.ofConstName declName}`, recall that `[reducible]` affects the term indexing datastructures used by `simp` and type class resolution{suffix}"
       | .irreducible =>
-        unless statusOld matches .semireducible do
-          throwError "failed to set `[local irreducible]`, `{.ofConstName declName}` is currently `{statusOld.toAttrString}`, `[semireducible]` expected{suffix}"
+        unless statusOld matches .semireducible | .instanceReducible do
+          throwError "failed to set `[local irreducible]`, `{.ofConstName declName}` is currently `{statusOld.toAttrString}`, `[semireducible]` nor `[instance_reducible]` expected{suffix}"
       | .instanceReducible =>
         unless statusOld matches .semireducible do
           throwError "failed to set `[local instance_reducible]`, `{.ofConstName declName}` is currently `{statusOld.toAttrString}`, `[semireducible]` expected{suffix}"
@@ -147,17 +145,7 @@ private def validate (declName : Name) (status : ReducibilityStatus) (attrKind :
         unless statusOld matches .irreducible do
           throwError "failed to set `[local semireducible]`, `{.ofConstName declName}` is currently `{statusOld.toAttrString}`, `[irreducible]` expected{suffix}"
 
-/-
-**Note**: Some instances are not definitions, but theorems. Thus, they don't need the `[instance_reducible]` attribute,
-but the current frontend adds the attribute `[instance_reducible]` when pre-processing the command `instance` before
-we know whether its type is a proposition or not. Thus, we just skip these annotations for now.
--/
-private def ignoreAttr (status : ReducibilityStatus) (declName : Name) : CoreM Bool := do
-  let .instanceReducible := status | return false
-  return !(← getConstInfo declName).isDefinition
-
 private def addAttr (status : ReducibilityStatus) (declName : Name) (stx : Syntax) (attrKind : AttributeKind) : AttrM Unit := do
-  if (← ignoreAttr status declName) then return ()
   Attribute.Builtin.ensureNoArgs stx
   validate declName status attrKind
   let ns ← getCurrNamespace
@@ -194,7 +182,7 @@ builtin_initialize
   registerBuiltinAttribute {
     ref             := by exact decl_name%
     name            := `instance_reducible
-    descr           := "semireducible declaration"
+    descr           := "instance reducible declaration"
     add             := addAttr .instanceReducible
     applicationTime := .afterTypeChecking
  }
@@ -219,9 +207,15 @@ def isReducible [Monad m] [MonadEnv m] (declName : Name) : m Bool := do
 def isIrreducible [Monad m] [MonadEnv m] (declName : Name) : m Bool := do
   return (← getReducibilityStatus declName) matches .irreducible
 
+def isInstanceReducibleCore (env : Environment) (declName : Name) : Bool :=
+  getReducibilityStatusCore env declName matches .instanceReducible
+
+/-- Return `true` if the given declaration has been marked as `[instance_reducible]`. -/
+def isInstanceReducible [Monad m] [MonadEnv m] (declName : Name) : m Bool :=
+  return isInstanceReducibleCore (← getEnv) declName
+
 /-- Set the given declaration as `[irreducible]` -/
 def setIrreducibleAttribute [MonadEnv m] (declName : Name) : m Unit :=
   setReducibilityStatus declName ReducibilityStatus.irreducible
 
-
 end Lean

src/Std/Data/DHashMap/Lemmas.lean

@@ -4535,6 +4535,7 @@ end Const
 end Equiv
 
 /-- Internal implementation detail of the hash map. -/
+@[instance_reducible]
 def isSetoid (α β) [BEq α] [Hashable α] : Setoid (DHashMap α β) where
   r := Equiv
   iseqv := {

src/Std/Data/DTreeMap/Internal/Zipper.lean

@@ -365,7 +365,7 @@ public def Zipper.iter (t : Zipper α β) : Iter (α := Zipper α β) ((a : α)
 public def Zipper.iterOfTree (t : Impl α β) : Iter (α := Zipper α β) ((a : α) × β a) :=
   Zipper.iter <| Zipper.done.prependMap t
 
-@[inline, expose]
+@[inline, expose, instance_reducible]
 public def Zipper.instToIterator :=
   ToIterator.of (γ := Zipper α β) _ (fun z => z.iter)
 attribute [instance] Zipper.instToIterator
@@ -678,7 +678,7 @@ public abbrev RicSlice α β [Ord α] := Slice (RicSliceData α β)
 public instance {α : Type u} {β : α → Type v} [Ord α] : Ric.Sliceable (Impl α β) α (RicSlice α β) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose]
+@[inline, expose, instance_reducible]
 public def RicSlice.instToIterator {β : α → Type v} [Ord α] :=
   ToIterator.of (γ := Slice (Internal.RicSliceData α β)) (β := ((a : α) × β a)) _
     (fun s => ⟨RxcIterator.mk (Zipper.prependMap s.1.treeMap Zipper.done) s.1.range.upper⟩)
@@ -708,7 +708,7 @@ public abbrev RicSlice α [Ord α] := Slice (RicSliceData α)
 public instance {α : Type u} [Ord α] : Ric.Sliceable (Impl α (fun _ => Unit)) α (Unit.RicSlice α) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose]
+@[inline, expose, instance_reducible]
 public def RicSlice.instToIterator [Ord α] :=
   ToIterator.of (γ := Slice (RicSliceData α)) (β := α) _ fun s =>
     (⟨RxcIterator.mk (Zipper.prependMap s.1.treeMap Zipper.done) s.1.range.upper⟩ : Iter _ ).map fun e => (e.1)
@@ -742,7 +742,7 @@ public abbrev RicSlice α β [Ord α] := Slice (RicSliceData α β)
 public instance {α : Type u} {β : Type v} [Ord α] : Ric.Sliceable (Impl α (fun _ => β)) α (RicSlice α β) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose]
+@[inline, expose, instance_reducible]
 public def RicSlice.instToIterator {β : Type v} [Ord α] :=
   ToIterator.of (γ := Slice (RicSliceData α β)) _ fun s =>
     (⟨RxcIterator.mk (Zipper.prependMap s.1.treeMap Zipper.done) s.1.range.upper⟩ : Iter ((_ : α) × β)).map fun e => (e.1, e.2)
@@ -776,7 +776,7 @@ public abbrev RioSlice α β [Ord α] := Slice (RioSliceData α β)
 public instance {α : Type u} {β : α → Type v} [Ord α] : Rio.Sliceable (Impl α β) α (RioSlice α β) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose]
+@[inline, expose, instance_reducible]
 public def RioSlice.instToIterator {β : α → Type v} [Ord α] :=
   ToIterator.of (γ := Slice (RioSliceData α β)) (β := (a : α) × β a) _ fun s =>
     ⟨RxoIterator.mk (Zipper.prependMap s.1.treeMap Zipper.done) s.1.range.upper⟩
@@ -806,7 +806,7 @@ public abbrev RioSlice α [Ord α] := Slice (RioSliceData α)
 public instance {α : Type u} [Ord α] : Rio.Sliceable (Impl α (fun _ => Unit)) α (Unit.RioSlice α) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose]
+@[inline, expose, instance_reducible]
 public def RioSlice.instToIterator [Ord α] :=
   ToIterator.of (γ := Slice (RioSliceData α)) _ fun s =>
     (⟨RxoIterator.mk (Zipper.prependMap s.1.treeMap Zipper.done) s.1.range.upper⟩ : Iter _ ).map fun e => (e.1)
@@ -840,7 +840,7 @@ public abbrev RioSlice α β [Ord α] := Slice (RioSliceData α β)
 public instance {α : Type u} {β : Type v} [Ord α] : Rio.Sliceable (Impl α (fun _ => β)) α (RioSlice α β) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose]
+@[inline, expose, instance_reducible]
 public def RioSlice.instToIterator {β : Type v} [Ord α] :=
   ToIterator.of (γ := Slice (RioSliceData α β)) _ fun s =>
     (⟨RxoIterator.mk (Zipper.prependMap s.1.treeMap Zipper.done) s.1.range.upper⟩ : Iter ((_ : α) × β)).map fun e => (e.1, e.2)
@@ -907,7 +907,7 @@ public abbrev RccSlice α β [Ord α] := Slice (RccSliceData α β)
 public instance {α : Type u} {β : α → Type v} [Ord α] : Rcc.Sliceable (Impl α β) α (RccSlice α β) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose]
+@[inline, expose, instance_reducible]
 public def RccSlice.instToIterator {β : α → Type v} [Ord α] :=
   ToIterator.of (γ := Slice (RccSliceData α β)) (β := (a : α) × β a) _ fun s =>
     (rccIterator s.1.treeMap s.1.range.lower s.1.range.upper)
@@ -934,7 +934,7 @@ public abbrev RccSlice α [Ord α] := Slice (RccSliceData α)
 public instance {α : Type u} [Ord α] : Rcc.Sliceable (Impl α (fun _ => Unit)) α (Unit.RccSlice α) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose]
+@[inline, expose, instance_reducible]
 public def RccSlice.instToIterator [Ord α] :=
   ToIterator.of (γ := Slice (RccSliceData α)) _ fun s =>
     (⟨RxcIterator.mk (Zipper.prependMapGE s.1.treeMap s.1.range.lower .done) s.1.range.upper⟩ : Iter _ ).map fun e => (e.1)
@@ -970,7 +970,7 @@ public abbrev RccSlice α β [Ord α] := Slice (RccSliceData α β)
 public instance {α : Type u} {β : Type v} [Ord α] : Rcc.Sliceable (Impl α (fun _ => β)) α (RccSlice α β) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose]
+@[inline, expose, instance_reducible]
 public def RccSlice.instToIterator {β : Type v} [Ord α] :=
   ToIterator.of (γ := Slice (RccSliceData α β)) _ fun s =>
     (⟨RxcIterator.mk (Zipper.prependMapGE s.1.treeMap s.1.range.lower .done) s.1.range.upper⟩ : Iter ((_ : α) × β)).map fun e => (e.1, e.2)
@@ -1041,7 +1041,7 @@ public abbrev RcoSlice α β [Ord α] := Slice (RcoSliceData α β)
 public instance {α : Type u} {β : α → Type v} [Ord α] : Rco.Sliceable (Impl α β) α (RcoSlice α β) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose]
+@[inline, expose, instance_reducible]
 public def RcoSlice.instToIterator {β : α → Type v} [Ord α] :=
   ToIterator.of (γ := Slice (RcoSliceData α β)) (β := (a : α) × β a) _ fun s =>
     rcoIterator s.1.treeMap s.1.range.lower s.1.range.upper
@@ -1068,7 +1068,7 @@ public abbrev RcoSlice α [Ord α] := Slice (RcoSliceData α)
 public instance {α : Type u} [Ord α] : Rco.Sliceable (Impl α (fun _ => Unit)) α (Unit.RcoSlice α) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose]
+@[inline, expose, instance_reducible]
 public def RcoSlice.instToIterator [Ord α] :=
   ToIterator.of (γ := Slice (RcoSliceData α)) _ fun s =>
     (⟨RxoIterator.mk (Zipper.prependMapGE s.1.treeMap s.1.range.lower .done) s.1.range.upper⟩ : Iter _ ).map fun e => (e.1)
@@ -1104,7 +1104,7 @@ public abbrev RcoSlice α β [Ord α] := Slice (RcoSliceData α β)
 public instance {α : Type u} {β : Type v} [Ord α] : Rco.Sliceable (Impl α (fun _ => β)) α (RcoSlice α β) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose]
+@[inline, expose, instance_reducible]
 public def RcoSlice.instToIterator {β : Type v} [Ord α] :=
   ToIterator.of (γ := Slice (RcoSliceData α β)) _ fun s =>
     (⟨RxoIterator.mk (Zipper.prependMapGE s.1.treeMap s.1.range.lower .done) s.1.range.upper⟩ : Iter ((_ : α) × β)).map fun e => (e.1, e.2)
@@ -1174,7 +1174,7 @@ public abbrev RooSlice α β [Ord α] := Slice (RooSliceData α β)
 public instance {α : Type u} {β : α → Type v} [Ord α] : Roo.Sliceable (Impl α β) α (RooSlice α β) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose]
+@[inline, expose, instance_reducible]
 public def RooSlice.instToIterator {β : α → Type v} [Ord α] :=
   ToIterator.of (γ := Slice (RooSliceData α β)) (β := (a : α) × β a) _ fun s =>
     rooIterator s.1.treeMap s.1.range.lower s.1.range.upper
@@ -1201,7 +1201,7 @@ public abbrev RooSlice α [Ord α] := Slice (RooSliceData α)
 public instance {α : Type u} [Ord α] : Roo.Sliceable (Impl α (fun _ => Unit)) α (Unit.RooSlice α) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose]
+@[inline, expose, instance_reducible]
 public def RooSlice.instToIterator [Ord α] :=
   ToIterator.of (γ := Slice (RooSliceData α)) _ fun s =>
     (⟨RxoIterator.mk (Zipper.prependMapGT s.1.treeMap s.1.range.lower .done) s.1.range.upper⟩ : Iter _ ).map fun e => (e.1)
@@ -1237,7 +1237,7 @@ public abbrev RooSlice α β [Ord α] := Slice (RooSliceData α β)
 public instance {α : Type u} {β : Type v} [Ord α] : Roo.Sliceable (Impl α (fun _ => β)) α (RooSlice α β) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose]
+@[inline, expose, instance_reducible]
 public def RooSlice.instToIterator {β : Type v} [Ord α] :=
   ToIterator.of (γ := Slice (RooSliceData α β)) _ fun s =>
     (⟨RxoIterator.mk (Zipper.prependMapGT s.1.treeMap s.1.range.lower .done) s.1.range.upper⟩ : Iter ((_ : α) × β)).map fun e => (e.1, e.2)
@@ -1308,7 +1308,7 @@ public abbrev RocSlice α β [Ord α] := Slice (RocSliceData α β)
 public instance {α : Type u} {β : α → Type v} [Ord α] : Roc.Sliceable (Impl α β) α (RocSlice α β) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose]
+@[inline, expose, instance_reducible]
 public def RocSlice.instToIterator {β : α → Type v} [Ord α] :=
   ToIterator.of (γ := Slice (RocSliceData α β)) (β := (a : α) × β a) _ fun s =>
     rocIterator s.1.treeMap s.1.range.lower s.1.range.upper
@@ -1335,7 +1335,7 @@ public abbrev RocSlice α [Ord α] := Slice (RocSliceData α)
 public instance {α : Type u} [Ord α] : Roc.Sliceable (Impl α (fun _ => Unit)) α (Unit.RocSlice α) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose]
+@[inline, expose, instance_reducible]
 public def RocSlice.instToIterator [Ord α] :=
   ToIterator.of (γ := Slice (RocSliceData α)) _ fun s =>
     (⟨RxcIterator.mk (Zipper.prependMapGT s.1.treeMap s.1.range.lower .done) s.1.range.upper⟩ : Iter _ ).map fun e => (e.1)
@@ -1371,7 +1371,7 @@ public abbrev RocSlice α β [Ord α] := Slice (RocSliceData α β)
 public instance {α : Type u} {β : Type v} [Ord α] : Roc.Sliceable (Impl α (fun _ => β)) α (RocSlice α β) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose]
+@[inline, expose, instance_reducible]
 public def RocSlice.instToIterator {β : Type v} [Ord α] :=
   ToIterator.of (γ := Slice (RocSliceData α β)) _ fun s =>
     (⟨RxcIterator.mk (Zipper.prependMapGT s.1.treeMap s.1.range.lower .done) s.1.range.upper⟩ : Iter ((_ : α) × β)).map fun e => (e.1, e.2)
@@ -1427,7 +1427,7 @@ public abbrev RciSlice α β [Ord α] := Slice (RciSliceData α β)
 public instance {α : Type u} {β : α → Type v} [Ord α] : Rci.Sliceable (Impl α β) α (RciSlice α β) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose]
+@[inline, expose, instance_reducible]
 public def RciSlice.instToIterator {β : α → Type v} [Ord α] :=
   ToIterator.of (γ := Slice (RciSliceData α β)) (β := (a : α) × β a) _ fun s =>
     rciIterator s.1.treeMap s.1.range.lower
@@ -1454,7 +1454,7 @@ public abbrev RciSlice α [Ord α] := Slice (RciSliceData α)
 public instance {α : Type u} [Ord α] : Rci.Sliceable (Impl α (fun _ => Unit)) α (Unit.RciSlice α) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose]
+@[inline, expose, instance_reducible]
 public def RciSlice.instToIterator [Ord α] :=
   ToIterator.of (γ := Slice (RciSliceData α)) _ fun s =>
     (⟨Zipper.prependMapGE s.1.treeMap s.1.range.lower Zipper.done⟩ : Iter _ ).map fun e => (e.1)
@@ -1493,7 +1493,7 @@ public abbrev RciSlice α β [Ord α] := Slice (RciSliceData α β)
 public instance {α : Type u} {β : Type v} [Ord α] : Rci.Sliceable (Impl α (fun _ => β)) α (RciSlice α β) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose]
+@[inline, expose, instance_reducible]
 public def RciSlice.instToIterator {β : Type v} [Ord α] :=
   ToIterator.of (γ := Slice (RciSliceData α β)) _ fun s =>
     (⟨(Zipper.prependMapGE s.1.treeMap s.1.range.lower Zipper.done)⟩ : Iter ((_ : α) × β)).map fun e => (e.1, e.2)
@@ -1550,7 +1550,7 @@ public abbrev RoiSlice α β [Ord α] := Slice (RoiSliceData α β)
 public instance {α : Type u} {β : α → Type v} [Ord α] : Roi.Sliceable (Impl α β) α (RoiSlice α β) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose]
+@[inline, expose, instance_reducible]
 public def RoiSlice.instToIterator {β : α → Type v} [Ord α] :=
   ToIterator.of (γ := Slice (RoiSliceData α β)) (β := (a : α) × β a) _ fun s =>
     roiIterator s.1.treeMap s.1.range.lower
@@ -1577,7 +1577,7 @@ public abbrev RoiSlice α [Ord α] := Slice (RoiSliceData α)
 public instance {α : Type u} [Ord α] : Roi.Sliceable (Impl α (fun _ => Unit)) α (Unit.RoiSlice α) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose]
+@[inline, expose, instance_reducible]
 public def RoiSlice.instToIterator [Ord α] :=
   ToIterator.of (γ := Slice (RoiSliceData α)) _ fun s =>
     (⟨Zipper.prependMapGT s.1.treeMap s.1.range.lower Zipper.done⟩ : Iter _ ).map fun e => (e.1)
@@ -1616,7 +1616,7 @@ public abbrev RoiSlice α β [Ord α] := Slice (RoiSliceData α β)
 public instance {α : Type u} {β : Type v} [Ord α] : Roi.Sliceable (Impl α (fun _ => β)) α (RoiSlice α β) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose]
+@[inline, expose, instance_reducible]
 public def RoiSlice.instToIterator {β : Type v} [Ord α] :=
   ToIterator.of (γ := Slice (RoiSliceData α β)) _ fun s =>
     (⟨(Zipper.prependMapGT s.1.treeMap s.1.range.lower .done)⟩ : Iter ((_ : α) × β)).map fun e => (e.1, e.2)
@@ -1667,7 +1667,7 @@ public abbrev RiiSlice α β := Slice (RiiSliceData α β)
 public instance {α : Type u} {β : α → Type v} : Rii.Sliceable (Impl α β) α (RiiSlice α β) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose]
+@[inline, expose, instance_reducible]
 public def RiiSlice.instToIterator {β : α → Type v} :=
   ToIterator.of (γ := Slice (RiiSliceData α β)) (β := (a : α) × β a) _ fun s =>
     riiIterator s.1.treeMap
@@ -1692,7 +1692,7 @@ public abbrev RiiSlice α  := Slice (RiiSliceData α)
 public instance {α : Type u} : Rii.Sliceable (Impl α (fun _ => Unit)) α (Unit.RiiSlice α) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose]
+@[inline, expose, instance_reducible]
 public def RiiSlice.instToIterator {α : Type u} :=
   ToIterator.of (γ := Slice (RiiSliceData α)) _ fun s =>
     (⟨Zipper.prependMap s.internalRepresentation.treeMap .done⟩ : Iter _ ).map fun e => (e.1)
@@ -1724,7 +1724,7 @@ public abbrev RiiSlice α β  := Slice (RiiSliceData α β)
 public instance {α : Type u} {β : Type v} : Rii.Sliceable (Impl α (fun _ => β)) α (Const.RiiSlice α β) where
   mkSlice carrier range := ⟨carrier, range⟩
 
-@[inline, expose]
+@[inline, expose, instance_reducible]
 public def RiiSlice.instToIterator {α : Type u} {β : Type v} :=
   ToIterator.of (γ := Slice (RiiSliceData α β)) _ fun s =>
     (⟨Zipper.prependMap s.internalRepresentation.treeMap .done⟩ : Iter ((_ : α) × β)).map fun e => (e.1, e.2)

src/Std/Data/DTreeMap/Lemmas.lean

@@ -5871,6 +5871,7 @@ end Equiv
 section Equiv
 
 /-- Implementation detail of the tree map -/
+@[instance_reducible]
 def isSetoid (α : Type u) (β : α → Type v) (cmp : α → α → Ordering := by exact compare) :
     Setoid (Std.DTreeMap α β cmp) where
   r := Equiv

src/lake/Lake/Build/Data.lean

@@ -50,7 +50,7 @@ public class OptDataKind (α : Type u) where
 
 namespace OptDataKind
 
-@[instance low]
+@[instance_reducible, instance low]
 public def anonymous : OptDataKind α where
   name := .anonymous
   wf h := by simp [Name.isAnonymous_iff_eq_anonymous] at h

src/library/CMakeLists.txt

@@ -9,7 +9,6 @@ add_library(
   dynlib.cpp
   replace_visitor.cpp
   num.cpp
-  class.cpp
   util.cpp
   print.cpp
   annotation.cpp

src/library/class.cpp

@@ -1,50 +0,0 @@
-/*
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include <string>
-#include "util/io.h"
-#include "library/class.h"
-
-namespace lean {
-extern "C" uint8 lean_is_class(object* env, object* n);
-extern "C" uint8 lean_is_instance(object* env, object* n);
-extern "C" uint8 lean_is_out_param(object* e);
-extern "C" uint8 lean_has_out_params(object* env, object* n);
-
-bool is_class_out_param(expr const & e) { return lean_is_out_param(e.to_obj_arg()); }
-bool has_class_out_params(elab_environment const & env, name const & c) { return lean_has_out_params(env.to_obj_arg(), c.to_obj_arg()); }
-bool is_class(elab_environment const & env, name const & c) { return lean_is_class(env.to_obj_arg(), c.to_obj_arg()); }
-bool is_instance(elab_environment const & env, name const & i) { return lean_is_instance(env.to_obj_arg(), i.to_obj_arg()); }
-
-static name * g_anonymous_inst_name_prefix = nullptr;
-
-name const & get_anonymous_instance_prefix() {
-    return *g_anonymous_inst_name_prefix;
-}
-
-name mk_anonymous_inst_name(unsigned idx) {
-    return g_anonymous_inst_name_prefix->append_after(idx);
-}
-
-bool is_anonymous_inst_name(name const & n) {
-    // remove mangled macro scopes
-    auto n2 = n.get_root();
-    if (!n2.is_string()) return false;
-    return strncmp(n2.get_string().data(),
-                   g_anonymous_inst_name_prefix->get_string().data(),
-                   strlen(g_anonymous_inst_name_prefix->get_string().data())) == 0;
-}
-
-
-void initialize_class() {
-    g_anonymous_inst_name_prefix = new name("_inst");
-    mark_persistent(g_anonymous_inst_name_prefix->raw());
-}
-
-void finalize_class() {
-    delete g_anonymous_inst_name_prefix;
-}
-}

src/library/class.h

@@ -1,28 +0,0 @@
-/*
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include "library/util.h"
-#include "library/elab_environment.h"
-namespace lean {
-/** \brief Return true iff \c c was declared with \c add_class. */
-bool is_class(elab_environment const & env, name const & c);
-/** \brief Return true iff \c i was declared with \c add_instance. */
-bool is_instance(elab_environment const & env, name const & i);
-
-name const & get_anonymous_instance_prefix();
-name mk_anonymous_inst_name(unsigned idx);
-bool is_anonymous_inst_name(name const & n);
-
-/** \brief Return true iff e is of the form `outParam a` */
-bool is_class_out_param(expr const & e);
-
-/** \brief Return true iff c is a type class that contains an `outParam` */
-bool has_class_out_params(elab_environment const & env, name const & c);
-
-void initialize_class();
-void finalize_class();
-}

src/library/init_module.cpp

@@ -6,7 +6,6 @@ Author: Leonardo de Moura
 */
 #include "library/init_module.h"
 #include "library/constants.h"
-#include "library/class.h"
 #include "library/num.h"
 #include "library/annotation.h"
 #include "library/print.h"
@@ -34,7 +33,6 @@ void initialize_library_module() {
     initialize_print();
     initialize_num();
     initialize_annotation();
-    initialize_class();
     initialize_library_util();
     initialize_time_task();
     initialize_dynlib();
@@ -45,7 +43,6 @@ void finalize_library_module() {
     finalize_ir_interpreter();
     finalize_time_task();
     finalize_library_util();
-    finalize_class();
     finalize_annotation();
     finalize_num();
     finalize_print();

tests/lean/run/boxing_bug.lean

@@ -1,3 +1,4 @@
+@[instance_reducible]
 def myCast : NatCast UInt8 where
   natCast := UInt8.ofNat
 
@@ -29,4 +30,3 @@ set_option trace.compiler.ir.result true in
 attribute [local instance] myCast UInt8.intCast in
 instance : Semiring UInt8 where
   nsmul := ⟨(· * ·)⟩
-

tests/lean/run/instanceReducibility.lean

@@ -0,0 +1,34 @@
+module
+
+/-! Reducibility of instances should default to `[instance_reducible]` but be overridable. -/
+
+instance i1 : Inhabited Nat := inferInstance
+
+/--
+info: @[instance_reducible] private def i1 : Inhabited Nat :=
+inferInstance
+-/
+#guard_msgs in
+#print i1
+
+@[reducible] instance i2 : Inhabited Nat := inferInstance
+
+/--
+info: @[reducible] private def i2 : Inhabited Nat :=
+inferInstance
+-/
+#guard_msgs in
+#print i2
+
+/--
+warning: instance `_private.lean.run.instanceReducibility.0.i3` must be marked with `@[reducible]` or `@[instance_reducible]`
+-/
+#guard_msgs in
+@[irreducible] instance i3 : Inhabited Nat := inferInstance
+
+/--
+info: @[irreducible] private def i3 : Inhabited Nat :=
+inferInstance
+-/
+#guard_msgs in
+#print i3

tests/lean/run/instanceReducible.lean

@@ -0,0 +1,38 @@
+module
+
+/-! Applying `[instance]` after the fact should check for appropriate reducibility. -/
+
+public def unexposed : Inhabited Nat := inferInstance
+
+/-- warning: instance `unexposed` must be marked with `@[expose]` -/
+#guard_msgs in
+attribute [instance] unexposed
+
+/-- warning: instance `unexposed` must be marked with `@[reducible]` or `@[instance_reducible]` -/
+#guard_msgs in
+attribute [local instance] unexposed
+
+@[expose]
+public def exposed : Inhabited Nat := inferInstance
+
+/-- warning: instance `exposed` must be marked with `@[reducible]` or `@[instance_reducible]` -/
+#guard_msgs in
+attribute [instance] exposed
+
+/-- warning: instance `exposed` must be marked with `@[reducible]` or `@[instance_reducible]` -/
+#guard_msgs in
+attribute [local instance] exposed
+
+@[expose, instance_reducible]
+public def exposedAndReducible : Inhabited Nat := inferInstance
+
+#guard_msgs in
+attribute [instance] exposedAndReducible
+
+#guard_msgs in
+attribute [local instance] exposedAndReducible
+
+instance bla : Add Int := ⟨Int.add⟩
+
+#guard_msgs in
+attribute [irreducible] bla

tests/lean/run/reducibilityAttrValidation.lean

@@ -25,7 +25,7 @@ attribute [semireducible] f
 attribute [irreducible] f
 
 /--
-error: failed to set `[irreducible]`, `f` is not currently `[semireducible]`, but `[irreducible]`
+error: failed to set `[irreducible]`, `f` is not currently `[semireducible]` nor `[instance_reducible]`, but `[irreducible]`
 
 Note: Use `set_option allowUnsafeReducibility true` to override reducibility status validation
 -/
@@ -45,7 +45,7 @@ attribute [local semireducible] f
 attribute [local irreducible] f
 
 /--
-error: failed to set `[local irreducible]`, `f` is currently `[irreducible]`, `[semireducible]` expected
+error: failed to set `[local irreducible]`, `f` is currently `[irreducible]`, `[semireducible]` nor `[instance_reducible]` expected
 
 Note: Use `set_option allowUnsafeReducibility true` to override reducibility status validation
 -/