Slow type-class search for has_add (α → β)

[gebner]

Linting takes half an hour at the moment. A large part of this runtime is spent in type-class search in the simp_nf linter. (For example, simplifying the left-hand side of pfun.coe_val takes 3.6 seconds.)

One particularly slow type-class problem that pops up is has_add (α → β):

import all
set_option profiler true
example {α : Type*} {β : Type*} : has_add (α → β) :=
by apply_instance -- 3.3s on my machine

[gebner]

Fixed by leanprover-community/lean#332