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