Improving the performance of typeclass inference

[FR-vdash-bot]

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) perf: reorder extends and change instance priority in algebra hierarchy #7873
• perf: change instance priority and order about OfNat #14712
• perf: lower the priority of toMul and toAdd instances #18464
• perf: lower the priority of Ordered*.to* instances #18468
• perf: lower the priority of Normed*.to* instances #18470
• perf: lower the priority of Comm*.to* instances #18472
• perf: lower the priority of *WithOne.to* instances #18474

Adding shortcuts:

• perf: skip some typeclasses in TC search #13852

Slow mixins instances:

• perf: change instance priority of SMul #13690
• perf: change instance priority of SMul #16607
• [Merged by Bors] - perf: synth order of SMul hierarchy #16646
• perf: investigate mixin TC slowness #16486
• perf: use implicit parameters in SMul hierarchy #17410
• perf: use implicit parameters in SMul hierarchy #17411
• perf: use implicit parameters in SetLike hierarchy instances #17529
• perf: use implicit parameters in some SMul instances #17530
• perf: do not search algebraic hierarchy when searching FunLike hierarchy #17675

Migrate to mixin typeclasses:

• refactor: make CanonicallyOrdered... mixin #17444 (was 6326 13519)