linter for instance names

Stream: general

[Kenny Lau]

In ring_theory.subring:

namespace ring
instance : is_subring (closure s) :=

In group_theory.group_action:

namespace mul_action
instance (H : set α) [is_subgroup H] : mul_action α (quotient H) :=

As a result of these instances without explicit names, the first one is called ring.is_subring and the second one mul_action.mul_action. Could we detect such instances of undesirable names automatically?

[Reid Barton]

Maybe the best place to detect them is at their source: when Lean chooses them.