Improving the performance of typeclass inference

Nobody has claimed this yet.

Currently, the performance of typeclass inference in mathlib is still unsatisfactory. This is often because the DFS process enters a node that cannot reach the goal and does a lot of useless searching.

One solution is to adjust the instance priority so that frequent targets are reached more quickly. This can significantly improve performance overall. See previous attempts in #7873 #13852 #13690.

Another solution is to use more mixins to avoid oversized hierarchies, but be careful that this may cause additional searching with the current synthesis algorithm. See https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Ways.20to.20speed.20up.20Mathlib/near/468146934.

The following are relevant PRs or experiments.

Adjusting typeclass search paths:

(needs to be split) #7873
#14712
#18464
~~#18468~~ migrated to mixins
#18470
#18472
#18474

Adding shortcuts:

#13852

Slow multi-parameter class instances:

#13690
#16607
#16646
#16486
#17410
#17411
#17529
#17530
#17675

Decouple hierarchies / Migrate to mixin typeclasses:

~~6326~~ ~~13519~~ #17444
#20676
#23621
#23961

Start by reviewing the prior attempts and experiments linked in the issue, especially the listed pull requests and the Zulip discussion. Identify a bounded typeclass-inference optimization before making changes; done should be demonstrated by improved performance without introducing the cautions described in the issue.

Written by the indexing model from the issue text.

Description

Contributor guide

First steps

Research direction

Assessment