feat: clarify warning for semireducible definitions of class type

src/Lean/Elab/MutualDef.lean

@@ -1251,8 +1251,11 @@ where
             (← isClass? header.type).isSome /-TODO-/ &&
             !header.type.getForallBody.getAppFn.constName? matches ``Decidable | ``DecidableEq | ``Setoid then
           let status ← getReducibilityStatus header.declName
-          unless status matches .reducible | .instanceReducible | .implicitReducible | .irreducible do
-            logWarning m!"Definition `{header.declName}` of class type must be marked with `@[reducible]`, `@[instance_reducible]`, `@[implicit_reducible]` or `@[irreducible]`"
+          if status == .semireducible then do
+            logWarning m!"Definition `{header.declName}` of class type is semireducible. \
+Most type class instances should be instance-reducible, so consider marking this
+definition with `@[instance_reducible]`. If it is intentionally semireducible, \
+this warning can be disabled with `set_option warn.classDefReducibility false`."
     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/Lean/Meta/Instances.lean

@@ -274,6 +274,12 @@ def checkNonClassInstance (c : Expr) : MetaM Unit := do
       throwError m!"The declaration `{c}` should not be an instance as its return type `{target}` \
       is not a type class."
 
+-- This option is registered in Lean.Elab.MutualDef.
+private def warnClassDefReducibility : Lean.Option Bool := {
+  defValue := true,
+  name := `warn.classDefReducibility
+}
+
 def addInstance (declName : Name) (attrKind : AttributeKind) (prio : Nat) : MetaM Unit := do
   let c ← mkConstWithLevelParams declName
   let cinfo ← getConstInfo declName
@@ -283,10 +289,14 @@ def addInstance (declName : Name) (attrKind : AttributeKind) (prio : Nat) : Meta
     checkImpossibleInstance cinfo
   let keys ← mkInstanceKey c
   let status ← getReducibilityStatus declName
-  unless status matches .reducible | .instanceReducible | .implicitReducible do
+  if status == .semireducible then do
     let info ← getConstInfo declName
     if info.isDefinition then
-      logWarning m!"instance `{declName}` must be marked with `@[reducible]`, `@[instance_reducible]` or `@[implicit_reducible]`"
+      if warnClassDefReducibility.get (← getOptions) then
+        logWarning m!"Definition `{declName}` of class type is semireducible. \
+Most type class instances should be instance-reducible, so consider marking this
+definition with `@[instance_reducible]`. If it is intentionally semireducible, \
+this warning can be disabled with `set_option warn.classDefReducibility false`."
     else if wasOriginallyDefn (← getEnv) declName then
       logWarning m!"instance `{declName}` must be marked with `@[expose]`"
   let projInfo? ← getProjectionFnInfo? declName

src/Lean/ReducibilityAttrs.lean

@@ -156,7 +156,10 @@ private def validate (declName : Name) (status : ReducibilityStatus) (attrKind :
         unless statusOld matches .semireducible do
           throwError "failed to set `[instance_reducible]`, `{.ofConstName declName}` is not currently `[semireducible]`, but `{statusOld.toAttrString}`{suffix}"
       | .semireducible =>
-        throwError "failed to set `[semireducible]` for `{.ofConstName declName}`, declarations are `[semireducible]` by default{suffix}"
+        if statusOld matches .semireducible then do
+          throwError "failed to set `[semireducible]` for `{.ofConstName declName}` because it already is `[semireducible]`{suffix}"
+        else
+          throwError "failed to set `[semireducible]` for `{.ofConstName declName}`{suffix}"
     | .local =>
       match status with
       | .reducible =>

tests/elab/2115.lean

@@ -12,6 +12,7 @@ class D (α : Type) extends B α, C α
 attribute [instance 10] C.toA
 
 set_option pp.all true
+set_option warn.classDefReducibility false
 
 def foo [D α] : A α := inferInstance -- should use `B.toA` since it has higher priority
 #print foo

tests/elab/2115.lean.out.expected

@@ -1,12 +1,8 @@
-2115.lean:16:0-16:36: warning: Definition `foo` of class type must be marked with `@[reducible]`, `@[instance_reducible]`, `@[implicit_reducible]` or `@[irreducible]`
 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]`, `@[instance_reducible]`, `@[implicit_reducible]` or `@[irreducible]`
 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]`, `@[instance_reducible]`, `@[implicit_reducible]` or `@[irreducible]`
 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]`, `@[instance_reducible]`, `@[implicit_reducible]` or `@[irreducible]`
 def boo2 : {α : Type} → [D α] → A α :=
 fun {α : Type} [inst : D α] => @inferInstance.{1} (A α) (@C.toA α (@D.toC α inst))

tests/elab/366.lean

@@ -1,3 +1,4 @@
+set_option warn.classDefReducibility false in
 def foo : Inhabited Nat :=
   set_option trace.Meta.synthInstance true in by { exact inferInstance }
 

tests/elab/366.lean.out.expected

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

tests/elab/4203.lean

@@ -11,13 +11,12 @@ variable {dIn dOut dOut₂ : Type} [Fintype dIn] [Fintype dOut] [Fintype dOut₂
 def IsGood [DecidableEq dOut] [DecidableEq dOut₂] (Λ : Mappish dIn dOut) (Λ₂ : Mappish dIn dOut₂) : Prop :=
   ∃ (D : Mappish dOut (dOut₂)), D.k = Λ.k + Λ₂.k
 
+set_option warn.classDefReducibility false in
 /--
 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]`, `@[instance_reducible]`, `@[implicit_reducible]` or `@[irreducible]`
 -/
 #guard_msgs in
 def MappishOrder [DecidableEq dIn] : Preorder

tests/elab/classDefReducibilityAfterAttr.lean

@@ -12,7 +12,8 @@ class Foo where
 
 /-! Warning should fire when no reducibility attribute is present. -/
 /--
-warning: Definition `baz` of class type must be marked with `@[reducible]`, `@[instance_reducible]`, `@[implicit_reducible]` or `@[irreducible]`
+warning: Definition `baz` of class type is semireducible. Most type class instances should be instance-reducible, so consider marking this
+definition with `@[instance_reducible]`. If it is intentionally semireducible, this warning can be disabled with `set_option warn.classDefReducibility false`.
 -/
 #guard_msgs in
 def baz : Foo := ⟨42⟩

tests/elab/instanceReducibility.lean

@@ -20,9 +20,6 @@ inferInstance
 #guard_msgs in
 #print i2
 
-/--
-warning: instance `_private.elab.instanceReducibility.0.i3` must be marked with `@[reducible]`, `@[instance_reducible]` or `@[implicit_reducible]`
--/
 #guard_msgs in
 @[irreducible] instance i3 : Inhabited Nat := inferInstance
 
@@ -32,3 +29,17 @@ inferInstance
 -/
 #guard_msgs in
 #print i3
+
+#guard_msgs in
+set_option warn.classDefReducibility false in
+@[irreducible] instance i4 : Inhabited Nat := inferInstance
+
+set_option allowUnsafeReducibility true in
+/--
+warning: Definition `_private.elab.instanceReducibility.0.i5` of class type is semireducible. Most type class instances should be instance-reducible, so consider marking this
+definition with `@[instance_reducible]`. If it is intentionally semireducible, this warning can be disabled with `set_option warn.classDefReducibility false`.
+-/
+#guard_msgs in
+@[semireducible] instance i5 : Inhabited Nat := inferInstance
+
+-- Why does `i5` not get any warning?

tests/elab/instanceReducible.lean

@@ -3,7 +3,8 @@ module
 /-! Applying `[instance]` after the fact should check for appropriate reducibility. -/
 
 /--
-warning: Definition `unexposed` of class type must be marked with `@[reducible]`, `@[instance_reducible]`, `@[implicit_reducible]` or `@[irreducible]`
+warning: Definition `unexposed` of class type is semireducible. Most type class instances should be instance-reducible, so consider marking this
+definition with `@[instance_reducible]`. If it is intentionally semireducible, this warning can be disabled with `set_option warn.classDefReducibility false`.
 -/
 #guard_msgs in
 public def unexposed : Inhabited Nat := inferInstance
@@ -13,26 +14,30 @@ public def unexposed : Inhabited Nat := inferInstance
 attribute [instance] unexposed
 
 /--
-warning: instance `unexposed` must be marked with `@[reducible]`, `@[instance_reducible]` or `@[implicit_reducible]`
+warning: Definition `unexposed` of class type is semireducible. Most type class instances should be instance-reducible, so consider marking this
+definition with `@[instance_reducible]`. If it is intentionally semireducible, this warning can be disabled with `set_option warn.classDefReducibility false`.
 -/
 #guard_msgs in
 attribute [local instance] unexposed
 
 /--
-warning: Definition `exposed` of class type must be marked with `@[reducible]`, `@[instance_reducible]`, `@[implicit_reducible]` or `@[irreducible]`
+warning: Definition `exposed` of class type is semireducible. Most type class instances should be instance-reducible, so consider marking this
+definition with `@[instance_reducible]`. If it is intentionally semireducible, this warning can be disabled with `set_option warn.classDefReducibility false`.
 -/
 #guard_msgs in
 @[expose]
 public def exposed : Inhabited Nat := inferInstance
 
 /--
-warning: instance `exposed` must be marked with `@[reducible]`, `@[instance_reducible]` or `@[implicit_reducible]`
+warning: Definition `exposed` of class type is semireducible. Most type class instances should be instance-reducible, so consider marking this
+definition with `@[instance_reducible]`. If it is intentionally semireducible, this warning can be disabled with `set_option warn.classDefReducibility false`.
 -/
 #guard_msgs in
 attribute [instance] exposed
 
 /--
-warning: instance `exposed` must be marked with `@[reducible]`, `@[instance_reducible]` or `@[implicit_reducible]`
+warning: Definition `exposed` of class type is semireducible. Most type class instances should be instance-reducible, so consider marking this
+definition with `@[instance_reducible]`. If it is intentionally semireducible, this warning can be disabled with `set_option warn.classDefReducibility false`.
 -/
 #guard_msgs in
 attribute [local instance] exposed

tests/elab/linearCategory_perf_issue.lean

@@ -275,6 +275,7 @@ class Preadditive where
   add_comp : ∀ (P Q R : C) (f f' : P ⟶ Q) (g : Q ⟶ R), (f + f') ≫ g = f ≫ g + f' ≫ g
   comp_add : ∀ (P Q R : C) (f : P ⟶ Q) (g g' : Q ⟶ R), f ≫ (g + g') = f ≫ g + f ≫ g'
 
+set_option warn.classDefReducibility false in
 attribute [instance] Preadditive.homGroup
 
 end CategoryTheory
@@ -382,6 +383,7 @@ class Linear (R : Type w) [Semiring R] (C : Type u₁) [Category.{v₁} C] [Prea
   smul_comp : ∀ (X Y Z : C) (r : R) (f : X ⟶ Y) (g : Y ⟶ Z), (r • f) ≫ g = r • f ≫ g
   comp_smul : ∀ (X Y Z : C) (f : X ⟶ Y) (r : R) (g : Y ⟶ Z), f ≫ (r • g) = r • f ≫ g
 
+set_option warn.classDefReducibility false in
 attribute [instance] Linear.homModule
 
 end CategoryTheory

tests/elab/methodSpecs.lean

@@ -109,11 +109,9 @@ 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
----
-warning: Definition `instIndClass` of class type must be marked with `@[reducible]`, `@[instance_reducible]`, `@[implicit_reducible]` or `@[irreducible]`
--/
+
+set_option warn.classDefReducibility false in
+/-- error: `indClass` is not a structure -/
 #guard_msgs in @[method_specs] def instIndClass : indClass := .mk
 
 -- This used to fail until we eta-reduced the field values

tests/elab/reducibilityAttrValidation.lean

@@ -1,7 +1,7 @@
 def f (x : Nat) := x + 1
 
 /--
-error: failed to set `[semireducible]` for `f`, declarations are `[semireducible]` by default
+error: failed to set `[semireducible]` for `f` because it already is `[semireducible]`
 
 Note: Use `set_option allowUnsafeReducibility true` to override reducibility status validation
 -/

tests/elab/splitImplicitReducible.lean

@@ -71,7 +71,8 @@ run_meta do
 /-! ## A class-typed `def` is rejected if it lacks any reducibility attribute. -/
 
 /--
-warning: Definition `noAttr` of class type must be marked with `@[reducible]`, `@[instance_reducible]`, `@[implicit_reducible]` or `@[irreducible]`
+warning: Definition `noAttr` of class type is semireducible. Most type class instances should be instance-reducible, so consider marking this
+definition with `@[instance_reducible]`. If it is intentionally semireducible, this warning can be disabled with `set_option warn.classDefReducibility false`.
 -/
 #guard_msgs in
 def noAttr : Foo := ⟨42⟩

tests/elab/stuckMVarBug.lean

@@ -3,11 +3,13 @@ class HasMulComm (α : Type u) [Mul α] : Prop where
 
 class A (α : Type u) where
     [Mul : Mul α]
+set_option warn.classDefReducibility false in
 attribute [instance] A.mk A.Mul
 
 class B (α : Type u) where
     [Mul : Mul α]
     [HasMulComm : HasMulComm α]
+set_option warn.classDefReducibility false in
 attribute [instance] B.mk B.Mul B.HasMulComm
 
 example [A α] [HasMulComm α] : B α := inferInstance

tests/elab/synthOrderRegression.lean

@@ -4,6 +4,7 @@
 class Foo (α : Type) [Add α] where
    bla : [Mul α] → BEq α
 
+set_option warn.classDefReducibility false in
 attribute [instance] Foo.bla
 
 inductive Boo where

tests/elab_fail/2273.lean

@@ -21,10 +21,10 @@ For this test we just hard code the `allowSynthFailures` option into `apply'`.
 elab "apply'" e:term : tactic => do
   evalApplyLikeTactic (·.apply · { allowSynthFailures := true }) e
 
+@[instance_reducible]
 def instP (n : Nat) : P n := {}
 
 example : True := by
   apply' foo
   apply instP
   exact 37
-

tests/elab_fail/2273.lean.out.expected

@@ -2,4 +2,3 @@
   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]`, `@[instance_reducible]`, `@[implicit_reducible]` or `@[irreducible]`

tests/elab_fail/phashmap_inst_coherence.lean

@@ -5,6 +5,7 @@ def m : PersistentHashMap Nat Nat :=
 let m : PersistentHashMap Nat Nat := {};
 m.insert 1 1
 
+@[instance_reducible]
 def natDiffHash : Hashable Nat :=
 ⟨fun n => UInt64.ofNat $ n+10⟩
 

tests/elab_fail/phashmap_inst_coherence.lean.out.expected

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

tests/elab_fail/scopedInstanceOutsideNamespace.lean

@@ -5,6 +5,7 @@ scoped instance : ToString Bool where -- Error
 
 scoped infix:65 "+" => Nat.add -- Error
 
+set_option warn.classDefReducibility false in
 @[scoped instance] -- Error
 def myInst : ToString Bool where
   toString b := if b then "t" else "f"

tests/elab_fail/scopedInstanceOutsideNamespace.lean.out.expected

@@ -3,5 +3,4 @@ scopedInstanceOutsideNamespace.lean:1:0-2:38: error: Scoped attributes must be u
 scopedInstanceOutsideNamespace.lean:6:0-6:30: error: Scoped attributes must be used inside namespaces
 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]`, `@[instance_reducible]`, `@[implicit_reducible]` or `@[irreducible]`
+scopedInstanceOutsideNamespace.lean:9:2-9:17: error: Scoped attributes must be used inside namespaces

tests/elab_fail/tcloop.lean

@@ -10,5 +10,6 @@ instance [s : B (Array α)] : A α  where
 instance [s : A (Array α)] : B α where
   a := ()
 
+set_option warn.classDefReducibility false in
 def f : B Nat :=
   inferInstance

tests/elab_fail/tcloop.lean.out.expected

@@ -1,4 +1,4 @@
-tcloop.lean:14:2-14:15: error: failed to synthesize
+tcloop.lean:15:2-15:15: error: failed to synthesize
   B Nat
 (deterministic) timeout at `typeclass`, maximum number of heartbeats (20000) has been reached
 
@@ -7,4 +7,3 @@ 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]`, `@[instance_reducible]`, `@[implicit_reducible]` or `@[irreducible]`

tests/pkg/module/Module/Imported.lean

@@ -70,10 +70,9 @@ 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]`, `@[instance_reducible]`, `@[implicit_reducible]` or `@[irreducible]`
 -/
 #guard_msgs in
+set_option warn.classDefReducibility false in
 def fX : X := inferInstance
 
 /-- error: `dsimp` made no progress -/