A linter for declarations with local instances that overlap

If the same data can be obtained from two different instances, we risk having non-defeq versions of that data. This situation is known as an "instance diamond". This linter warns against instance diamonds in local contexts.

This is a syntax linter. It is run on partially and fully elaborated declarations.

To find diamonds, we compute the parent classes of each local instance. For classes that aren't structures, this is just the class itself. If any of these parent classes is duplicated, we throw a warning.

This linter also warns on redundant proposition classes, i.e. those that can be synthesized from the other instances in the local context. (Note: we do not warn on proposition classes that merely overlap.) Even though redundant proposition classes cause no meaningful issue, they are still undesirable.

A common case where this linter may fire is if the same type class assumption is given in both a variable statement and a declaration. This kind of variable shadowing does not actually produce declarations with duplicate type class assumptions, but it is still not desirable.

TODO

Support declarations without bodies (structures/classes/inductives etc.)