[RFC] automatic instance priorities

Background

Type-class inference is a large part of the Mathlib's compilation time (roughly 50%). I think it can be greatly improved using better instance priorities. A preliminary test changing only 2 instances in Mathlib resulted in a 29% decrease in peak memory usage.

In mathlib3 we used the following heuristics:

• instances that apply in all type-class searches (e.g. instance [CommGroup α] : Group α or [Algebra R A] : Module R A) should have a lower-than-default priority. This is usually the case if all types in the conclusion are (distinct) variables, and this is sometimes called forgetful inheritance. The reason is that we first want to try instances that are specific to this class (we want to find add_group ℤ before trying all add_comm_group instances). We typically used priority 100 for this, but based on human judgement we sometimes used a priority that is a bit higher or lower
• (Almost) all other instances are type-directed. These instances only work for specific types, and therefore will fail very quickly if they don't apply. They are also almost always the correct instance if they do apply. An example is [Group G] [Group H] : Group (G × H). These instances have (approximately) the default priority of 1000.

Current Mathlib4 status

Currently, all instances generated by class ... extends ... have priority 1000 (the default, which until recently we couldn't change). Other than that we mostly follow mathlib3's priorities.

Mathlib4 heavily uses diamonds when extending classes (i.e. extending 2 or more classes that share a field). Here is an example of a diamond:

class A (α : Type _) : Type _ where
  a : Nat

class AB (α : Type _) extends A α where
  b : Nat

class AC (α : Type _) extends A α where
  c : Nat

class ABCD (α : Type _) extends AB α, AC α where
  d : Nat

instance foo [ABCD α] : A α := by infer_instance
set_option pp.explicit true
#print foo -- (@AC.toA α (@ABCD.toAC α inst))

My understanding is that whenever we have a diamond and we write a projection we strongly prefer to use the first parent for each structure (we want to use ABCD.toAB). These functions are just projections, so let's call these parents "projection parents". The function ABCD.toAC involves unpacking and re-packing the structure, and is therefore worse to use. Let's call these "auxiliary parents". Note however that the above instance search produces the suboptimal projection ABCD.toAC.

Note that this is not solved by changing the priorities of ABCD.toAB or ABCD.toAC: we need to change the instance priorities of AB.toA or AC.toA. So this is not a local problem: we need some global coherence of instance priorities. I think we want to have the following coherence rule for instance priorities:

Whenever a class (ABCD) extends 2+ classes (AB and AC) that share a common ancestor (A), then the priority of AB.toA should be higher than that of AC.toA.

Ideally, we also have the following two refinements:

• If ABCD extends more than 2 classes this condition should hold for every pair of (AB,AC) where AB is a projection parent and AC is a auxiliary parent.
• We should also have a condition if A is not a direct parent of AB or AC, but any ancestor. The rule should be that the path with highest priority from A to ABCD goes via AB.

Possible solutions

Here are some possible solutions, going from least changes in Lean core to most changes in Lean core

1. We don't change Lean core, but in Mathlib (or Std) we add linters + manually-configured priorities to ensure the coherence rule above. This will result in manually specifying the priority of every class projection in Mathlib.
2. We make simple and easily-explainable adjustments to the structure instance priorities in core. For example, we could make the default priority of projection parents 200 and that of auxiliary parents 100. This is in line with Mathlib's convention to use priority 100 for forgetful inheritance. We make the projection parents a higher (but lower-than-default) priority so that we tend to use them more often. This is simple and will use slightly better instances during type class resolution, but it doesn't satisfy the coherence rule. Mathlib will still use linters and modify a few priorities for class projections so that the coherence rule is satisfied.
3. When adding a structure we run a test to check that the coherence rule is satisfied. If not, we print a warning/error stating how the user should change the priorities manually.
4. We could try to satisfy the coherence rule automatically, but since this requires changing existing instance priorities, I think that is a bad idea: it is probably quite untransparent and unintuitive. Another issue is that the user might write clases with conflicting coherence rules (e.g. class ACB (α : Type _) extends AC α, AB α conflicts with ABCD above), and in this case the only proper solution is to reorder the arguments of the extends command.

Related Zulip discussion

The issue names no specific files or tests; start by tracing Lean core's structure elaboration and instance-priority handling, then review the Mathlib/Std linter and manually configured priority options described here. Done would require an agreed coherence strategy and an implementation or validation path, not just a choice among the proposed solutions.