head-based instance resolution

Stream: general

[Yury G. Kudryashov]

Hi,
I think, it would be nice to have "canonical" class instances associated with some "heads". E.g.., if we're looking for [group (opposite α)], then we can go ahead and look for [group α].

[Yury G. Kudryashov]

Actually, I wonder how many cases can be covered by (1) "heads" based canonical instances; (2) substructures.
E.g., is_group_hom → is_monoid_hom is not covered right now but can be covered if we redefine is_group_hom to extend is_monoid_hom, and define (not an instance) is_group_hom.mk' : ∀ f, is_mul_hom f → is_group_hom f.

[Yury G. Kudryashov]

Another related idea: may be, it is easier to cache all substructures of defined instances than to go up the tree every time we need [has_mul α].

[Yury G. Kudryashov]

I guess, this is bad for some reason but I can't see what is the reason.