[Merged by Bors] - perf(library/type_context): cache type-class searches w/o mvars

[gebner]

This PR adds caching of intermediate results during type-class synthesis, under the condition that the subgoals have no temporary metavariables. For example, a subgoal has_add α is cached, but has_coe_t α ?m is not.

It is theoretically possible that some type-class searches fail now, because we no longer try all possible instances (and if this actually matters for another instance to apply). But it's a bug anyhow if you have two instances that are not definitionally equal.

[gebner]

As expected, all errors were theoretical. mathlib builds fine.

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build linux Debug
• Build macos Debug
• Build linux Release
• Build macos Release
• Build windows Release
• Build emscripten

[fpvandoorn]

This is really nice! I feel that the exponential search time on type-class inference was one of the big bottlenecks for development in mathlib.

I wouldn't be surprised if this sped up a lot of other things as well, like simp (and maybe even library_search?).

[gebner]

It will definitely speed up simp (in some cases). My initial motivation came from this test case from the simp_nf linter:

import all
-- before: 16s
-- after: 0.3s
example {α : Type*} {β : Type*} (f : α → β) (a : α) :
  (f : pfun α β) a = roption.some (f a) :=
by simp