Type family consistency checks: order of performing checks matters greatly for performance

Consider a module M which imports modules A, B and C, all defining (open) type family instances.

We can waste a lot of work in type family consistency checking depending on the order in which the modules are processed.

Suppose for example that C imports A and B. When we compiled C, we will have checked A and B for consistency against eachother. This means that, when processing the imports of M to check type family instance consistency:

• if C is processed first, then A and B will not need to be checked for consistency against eachother again,
• if we process A and B before C,then the consistency checks between A and B will be performed again. This is wasted work, as we already performed them for C.

This can make a significant difference. Keeping the nomenclature of the above example for illustration, we have observed situations in practice in which the compilation time of M goes from 1 second (the "processing A and B first" case) down to 80 milliseconds (the "processing C first" case).

At the moment, the order in which the consistency checks for imported modules are performed is non-deterministic (it doesn't even follow the order in which the modules are imported).

---

Clearly we should engineer that C is checked before B and A, but by what scheme?

A simple one is to observe that if a module M is in the transitive closure of X then the size of the consistent family set of M is less than or equal to size of the consistent family set of X.

Therefore, by sorting the imports by the size of the consistent family set and processing the largest first, we make sure to process modules in topological order.

In practice we have observed that this strategy has reduced the amount of consistency checks performed.

added needs triage label

mentioned in commit cbe04637

mentioned in merge request !13685 (closed)

changed the description

changed title from Type family consistency checks, order of performing checks matters greatly to Type family consistency checks: order of performing checks matters greatly

added Pnormal Tbug compiler perf typechecker labels and removed needs triage label

changed title from Type family consistency checks: order of performing checks matters greatly to Type family consistency checks: order of performing checks matters greatly for performance

changed the description

mentioned in commit 2257ffaf

mentioned in issue #25558

Related: !13685 (closed).

mentioned in commit 7698a505

mentioned in commit 13fe48d4

mentioned in commit 2feb717e

mentioned in commit 2d8c8094

mentioned in commit 8c363c54