feat: overlapping instances linter (leanprover-community#38126)

This PR implements the overlapping instances linter, with better performance than the previous attempt.

The overlapping instances linter warns on data-carrying overlaps between instances in the local context of a declaration, as well as on redundant instances of `Prop` classes (i.e. those which can be synthesized from another instance in the context).

An annoyance is the need for `withSetBoolOptionIn`. This is a private declaration in the `unusedInstancesInType` linter, with a link to leanprover/lean4#13133, which has been merged. When that commit lands in mathlib, we should move to `withSetOptionIn`.

See leanprover-community#35095 and leanprover-community#33677 for previous iterations of this linter.

See leanprover-community#14731 for an old attempt at a weaker form of this linter.

Co-authored-by: @thorimur
Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com>

Author: 2 people

Mathlib.lean

@@ -7239,6 +7239,7 @@ public import Mathlib.Tactic.Linter.Lint
 public import Mathlib.Tactic.Linter.MinImports
 public import Mathlib.Tactic.Linter.Multigoal
 public import Mathlib.Tactic.Linter.OldObtain
+public import Mathlib.Tactic.Linter.OverlappingInstances
 public import Mathlib.Tactic.Linter.PPRoundtrip
 public import Mathlib.Tactic.Linter.PrivateModule
 public import Mathlib.Tactic.Linter.Style

Mathlib/Algebra/Category/Ring/FilteredColimits.lean

@@ -376,6 +376,7 @@ protected lemma nontrivial {F : J ⥤ CommRingCat.{v}} [IsFilteredOrEmpty J]
     (Types.FilteredColimit.isColimit_eq_iff' (isColimitOfPreserves (forget _) hc) _ _).mp h
   exact zero_ne_one (((F.map f).hom.map_zero.symm.trans e).trans (F.map f).hom.map_one)
 
+set_option linter.overlappingInstances false in
 omit [IsFiltered J] in
 instance {F : J ⥤ CommRingCat.{v}} [IsFilteredOrEmpty J]
     [HasColimit F] [∀ i, Nontrivial (F.obj i)] : Nontrivial ↑(Limits.colimit F) :=

Mathlib/Algebra/Colimit/DirectLimit.lean

@@ -833,8 +833,8 @@ end NonUnitalStarRing
 namespace Algebra
 
 variable [CommSemiring R]
-variable [∀ i, Semiring (G i)] [∀ i j h, RingHomClass (T h) (G i) (G j)]
-variable [∀ i, Algebra R (G i)] [∀ i j h, AlgHomClass (T h) R (G i) (G j)]
+variable [∀ i, Semiring (G i)] [∀ i, Algebra R (G i)]
+variable [∀ i j h, AlgHomClass (T h) R (G i) (G j)]
 variable [Nonempty ι]
 
 variable (G f) in

Mathlib/Algebra/Homology/HomotopyFiber.lean

@@ -42,7 +42,7 @@ class HasHomotopyFiber (φ : F ⟶ G) : Prop where
 instance [HasBinaryBiproducts C] : HasHomotopyFiber φ where
   hasBinaryBiproduct _ _ _ := inferInstance
 
-variable [HasHomotopyFiber φ] [DecidableRel c.Rel]
+variable [HasHomotopyFiber φ]
 
 instance : HasHomotopyCofiber ((opFunctor C c).map φ.op) where
   hasBinaryBiproduct i j hij := by

Mathlib/Algebra/Module/DedekindDomain.lean

@@ -22,14 +22,12 @@ public section
 
 universe u v
 
-variable {R : Type u} [CommRing R] [IsDomain R] {M : Type v} [AddCommGroup M] [Module R M]
+variable {R : Type u} [CommRing R] [IsDedekindDomain R] {M : Type v} [AddCommGroup M] [Module R M]
 
 open scoped DirectSum
 
 namespace Submodule
 
-variable [IsDedekindDomain R]
-
 open UniqueFactorizationMonoid
 
 /-- Over a Dedekind domain, an `I`-torsion module is the internal direct sum of its `p i ^ e i`-

Mathlib/Algebra/Module/Equiv/Defs.lean

@@ -296,6 +296,7 @@ variable [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] [RingHomCompTriple σ₄
 variable [RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [RingHomCompTriple σ₄₃ σ₃₂ σ₄₂]
 variable (e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂) (e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃)
 
+set_option linter.overlappingInstances false in
 /-- Linear equivalences are transitive. -/
 -- Note: the `RingHomCompTriple σ₃₂ σ₂₁ σ₃₁` is unused, but is convenient to carry around
 -- implicitly for lemmas like `LinearEquiv.self_trans_symm`.

Mathlib/Algebra/Module/GradedModule.lean

@@ -191,20 +191,21 @@ end SetLike
 namespace GradedModule
 
 variable [AddCommMonoid M] [Module A M] [SetLike σ M] [AddSubmonoidClass σ' A]
-  [AddSubmonoidClass σ M] [SetLike.GradedMonoid 𝓐] [SetLike.GradedSMul 𝓐 𝓜]
+  [AddSubmonoidClass σ M] [SetLike.GradedSMul 𝓐 𝓜]
+  [DecidableEq ιA] [DecidableEq ιM] [GradedRing 𝓐]
 
 /-- The smul multiplication of `A` on `⨁ i, 𝓜 i` from `(⨁ i, 𝓐 i) →+ (⨁ i, 𝓜 i) →+ ⨁ i, 𝓜 i`
 turns `⨁ i, 𝓜 i` into an `A`-module
 -/
 @[implicit_reducible]
-def isModule [DecidableEq ιA] [DecidableEq ιM] [GradedRing 𝓐] : Module A (⨁ i, 𝓜 i) :=
+def isModule : Module A (⨁ i, 𝓜 i) :=
   { Module.compHom _ (DirectSum.decomposeRingEquiv 𝓐 : A ≃+* ⨁ i, 𝓐 i).toRingHom with
     smul := fun a b => DirectSum.decompose 𝓐 a • b }
 
 /-- `⨁ i, 𝓜 i` and `M` are isomorphic as `A`-modules.
 "The internal version" and "the external version" are isomorphism as `A`-modules.
 -/
-def linearEquiv [DecidableEq ιA] [DecidableEq ιM] [GradedRing 𝓐] [DirectSum.Decomposition 𝓜] :
+def linearEquiv [DirectSum.Decomposition 𝓜] :
     @LinearEquiv A A _ _ (RingHom.id A) (RingHom.id A) _ _ M (⨁ i, 𝓜 i) _
     _ _ (by letI := isModule 𝓐 𝓜; infer_instance) := by
   letI h := isModule 𝓐 𝓜

Mathlib/Algebra/Order/Antidiag/Prod.lean

@@ -77,6 +77,7 @@ instance [AddMonoid A] : Subsingleton (HasAntidiagonal A) where
 
 -- The goal of this lemma is to allow to rewrite antidiagonal
 -- when the decidability instances obfuscate Lean
+set_option linter.overlappingInstances false in
 lemma hasAntidiagonal_congr (A : Type*) [AddMonoid A]
     [H1 : HasAntidiagonal A] [H2 : HasAntidiagonal A] :
     H1.antidiagonal = H2.antidiagonal := by congr!; subsingleton

Mathlib/Algebra/Order/Invertible.lean

@@ -41,6 +41,5 @@ theorem invOf_le_one [Invertible a] (h : 1 ≤ a) : ⅟a ≤ 1 :=
 theorem invOf_lt_one [Invertible a] (h : 1 < a) : ⅟a < 1 :=
   mul_invOf_self a ▸ lt_mul_of_one_lt_left (invOf_pos.2 <| one_pos.trans h) h
 
-theorem pos_invOf_of_invertible_cast [Nontrivial R] (n : ℕ)
-    [Invertible (n : R)] : 0 < ⅟(n : R) :=
+theorem pos_invOf_of_invertible_cast (n : ℕ) [Invertible (n : R)] : 0 < ⅟(n : R) :=
   invOf_pos.2 <| Nat.cast_pos.2 <| pos_of_invertible_cast (R := R) n

Mathlib/Algebra/Polynomial/Div.lean

@@ -789,7 +789,7 @@ lemma _root_.Irreducible.isRoot_eq_bot_of_natDegree_ne_one
     (hi : Irreducible p) (hdeg : p.natDegree ≠ 1) : p.IsRoot = ⊥ :=
   le_bot_iff.mp fun _ ↦ hi.not_isRoot_of_natDegree_ne_one hdeg
 
-lemma _root_.Irreducible.subsingleton_isRoot [IsLeftCancelMulZero R]
+lemma _root_.Irreducible.subsingleton_isRoot
     (hi : Irreducible p) : { x | p.IsRoot x }.Subsingleton :=
   fun _ hx ↦ (subsingleton_isRoot_of_natDegree_eq_one <| natDegree_eq_of_degree_eq_some <|
     degree_eq_one_of_irreducible_of_root hi hx) hx