Make `contractive_proper` into a lemma, or control other instances that make it costly.
Successful typeclass searches for contractive_proper
take 0.1s — as shown by replacing contractive_proper _
with _
. So it should maybe be disabled like ne_proper
(see 6df6c641).
Logs like https://gist.github.com/Blaisorblade/541416169b97729e60bb80fb0f259b7d reveal that the problem is that proper_reflexive
is tried first, and then search diverges. Finding a way to blacklist certain instances for Reflexive (equiv ==> equiv)%signature
would be useful — maybe removing them and replacing them with Hint Extern
?