speed up typeclass inference involving isequiv_compose

[jdchristensen]

Since this was discussed in a merged pull request, #1204, I thought I should record a few things in an issue so they aren't lost. See #1204 for some more info.

Based on what I see with Typeclasses eauto := debug set, Coq spends time trying lots of other things before trying isequiv_compose when trying to show IsEquiv (g o f). If the priority of the instance is made too high, then I think Coq will also try isequiv_compose when trying to prove IsEquiv f because it will insert an identity function. (Recall that o is a notation and g o f is definitionally equal to f when g is fun x => x.) So it's not simply a matter of making the priority higher.

Ideas for what might work:

Hint Extern 0 (IsEquiv (_ o _)) => class_apply @isequiv_compose : typeclass_instances.
Hint Extern 0 (IsEquiv (fun x => ?f (?g x))) => class_apply @isequiv_compose : typeclass_instances.

But will Coq still try the identity map with these?

Another idea is for the user to be more explicit. For example, in some cases writing equiv_compose g f instead of g o f makes things fast because it forces Coq to use isequiv_compose right away. oE is a notation for equiv_compose', but we could introduce a notation for equiv_compose and use it in such situations.

Another idea would be to define:

Definition Eq {A B} (f : A -> B) `{IsEquiv A B f} : Equiv A B := Build_Equiv _ _ f _.

and then use Eq g oE Eq f instead of g o f. It does seem to work in a few tests that I did. If we only need this for composition, then an alternative to oE is probably cleaner. But if we want to upgrade maps to equivalences more generally, then Eq will work. There are lots of places in the library where Build_Equiv _ _ foo _ could be replaced by Eq foo.

I see now that #1165 has an idea similar to my Eq idea as part of a more general framework.

[Alizter]

I am not able to run anything at the moment, but what does Typeclass debug say when you try isequiv_compose with high priority?

Now that I think about it, I would have thought typeclasses would try to insert idmap for isequiv_compose but then realise it got the exact same goal and backtrack?