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?