[RFC] automatic instance priorities

[fpvandoorn]

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

[kim-em]

It seems 2. is the obvious option here, if it can be done in a low-impact way. It would be good to have a PR that we can run Mathlib against to measure the performance effect.

I think 3. is too bossy to users, and 4. is too unpredictable.

[fpvandoorn]

I think 2 is also the best option.

I started trying to manually change the priorities in mathlib as a preparation (i.e. with a script) - and to see how big the effects are on elaboration time. Changing instance priorities causes many things to break in the library, and I stopped, because of a lack of time.

What might be a good idea is to make a branch where we delete 75-95% of mathlib and test changes on the remainder. That way we can get reasonable estimates about performance, but not have to fix all files in mathlib that break because of the instance changes.

Once I have more time for Lean, I'm willing to do that, but of course anyone should feel free to do this earlier.

[leodemoura]

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.

What happens if user later adds?

class ABCE (α : Type _) extends AC α, AB α where
  e : Nat

[fpvandoorn]

Automatically satisfying the coherence rule (option 4) is probably not feasible, since you can indeed write structures that conflict with each other.

[leodemoura]

Automatically satisfying the coherence rule (option 4) is probably not feasible, since you can indeed write structures that conflict with each other.

This is my point. Solution 2 will generate counter intuitive behavior because we will have conflicts.

[urkud]

What is counterintuitive about "extends uses priority 100"? Probably, I got used to Mathlib convention too much and don't see why it's counterintuitive.