duplicate instance linter

Stream: general

[Kenny Lau]

Do we need a duplicate instance linter or is the linter sufficiently slow already?

[Kenny Lau]

Because this happened in data.polynomial:

 instance algebra_of_algebra : algebra R (polynomial A) := add_monoid_algebra.algebra

[...]

 instance algebra' (R : Type u) [comm_semiring R] (A : Type v) [semiring A] [algebra R A] :
   algebra R (polynomial A) :=
 { smul := λ r p, algebra_map R A r • p,
   commutes' := λ c p, ext $ λ n,
     show (C (algebra_map R A c) * p).coeff n = (p * C (algebra_map R A c)).coeff n,
     by rw [coeff_C_mul, coeff_mul_C, algebra.commutes],
   smul_def' := λ c p, (C_mul' _ _).symm,
   .. C.comp (algebra_map R A) }

[Johan Commelin]

Good catch! I think we can run another linter. When you lint 1 file, it takes a noticeable amount of seconds, but it's not too bad. When you lint the entire project, in CI, this is something you can parallelize, so adding an extra linter doesn't hurt.