Slow type-class search

Stream: general

[Gabriel Ebner]

This takes more than three seconds on my machine:

import all
set_option profiler true
example {α : Type*} {β : Type*} : has_add (α → β) :=
by apply_instance

Any idea what's going on here? (Also filed as issue #3080)

[Sebastien Gouezel]

Is this really surprising? When it succeeds because there is a ring or whatever around, it can be pretty quick, but when it fails it has to try every possible instance, even those that have low priority. And there are many many many ways in mathlib to have a has_add instance.

[Gabriel Ebner]

Good point. Then we'll have to fix this in core. lean#332 reduces the example to 83ms.

[Sebastien Gouezel]

Gabriel, you're still going to shave off 30 minutes on compilation time :)

[Johan Commelin]

This is really crazy... I'm amazed by all these fixes that keep improving the system.