A new design for the type constraint solver

[kyouko-taiga]

The current implementation of the type constraint solver is responsible for most of the time spent during type checking. As profiling suggests that excessive backtracking is making our solver prohibitively slow, I'd like to discuss an idea for an improved design that would reduce the depth of the search trees.

Current design

We use type inference to determine the type of each expression. In the type checker, the main entry point for this process is checkedType(of:withHint:), which performs two tasks. First, the method visits the expression to check to generate constraints between its subexpressions. These constraints form a constraint system that is essentially a set of equations between type expressions. Then, the method solves the generated constraint system, thereby inferring all type information related to the expression to check.

Solving a constraint involves various operations. To keep things simple here, let's focus only on three kind of constraints:

• Equality constraints (e.g., A == B). These are heart of type inference. They are solved by determining whether A is equal to B, using type unification to infer necessary substitutions.
• Conformance constraints (e.g., A : P). Solving these merely consists of querying the type checker to determine whether there exists a conformance of A to P. Conformance constraints require A to be closed, i.e. a type that contains no free type variables (e.g., Array<Int> but not Array<%0>).
• Disjunction constrains (e.g., A == B ∨ A == C). These represent choices. They are solved by distributing each alternative over the other constraints, then solve each resulting sub-system separately, and finally pick the best solution.

In theory, there's no specific order in which a constraint system should be processed, it's just a set. In practice, however, it is very likely that there exist some form of dependencies between constraints. For example, if we had to solve a conformance constraint %0 : Equatable, we'd first have to determine the type of the variable %0.

We can address this issue by carefully choosing the order in which we solve constraint. For example, if our constraint system contains %0 == Int and %0 : Equatable, the former will be processed before the latter. The current implementation uses a very naive heuristic to pick this order (see: ConstraintSystem.simpler(than:)):

1. Equality constraints are ordered before all other constraints
2. Disjunctive constraints are ordered after all other constraints

This ordering has the added advantage to minimize the amount of work by minimizing the size of the sub-systems being solved separately. However, ordering constraints that way is clearly not good enough. For example, if we'd be unable to solve a system containing only %0 : Equatable and (%0 == A ∨ %0 == B) because the disjunction would be ordered after the conformance constraint.

To solve this issue, the solver maintains two sets of constraints internally, called the fresh and stale sets, respectively. The fresh set contains the constraints left to solve while the stale set contains the constraints that were examined but could not be solved without first gathering more information (in the form of type substitutions). Every time solving a fresh constraint improves the knowledge of the solver, the stale constraints that may depend on the new information are moved back to the fresh set to be processed again. Once there are no more fresh constraints to process, either the solver could solve all constraints or there remains state constraints, meaning that the constraint system was underspecified.

Unfortunately, this approach leads to combinatorial explosion in constraint systems containing many disjunctions. This explosion is not always justified because it is possible that two disjunctions be actually unrelated.

Proposed improvement

The main idea is to better understand the relationship between the elements of a constraint system. Rather than trying to come up with a simple ordering, we could generate a dependency graph by looking at the type variables mentioned by each constraint. Since only few constraints can be used to infer new substitutions (in our example, only equality constraints), then we can say that any other constraint mentioning a type variable must transitively depend on a constraint capable of inferring the value of that variable.

If the dependency graph contains separate subgraphs, then these subgraphs would be subsystems that could be solved separately, thereby drastically reducing combinatorial explosion. For example, if we had to solve (A == B ∨ A == C ∨ A == D)and(W == X ∨ W == Y ∨ W == Z)`, we'd had to solve only 6 equality constraints instead of 9.

The other advantage of this approach is that I think we could get rid of the fresh/stale sets. Any constraint system containing an unsolvable constraint with no dependencies could be directly identified as being underspecified, without having to solve anything.

[dabrahams]

What causes disjunction constraints? Overload resolution?

If the dependency graph contains separate subgraphs…

I don't understand what you mean by this. The definition of subgraph suggests that every nontrivial graph contains subgraphs, that a subgraph is never “separate” from the whole graph, and that every nontrivial graph contains subgraphs that are separate (disjoint) from one another.

[kyouko-taiga]

What causes disjunction constraints? Overload resolution?

Overloads, subtyping, and literal types.

I've been looking for a better way to solve subtyping constraints for years but haven't found one yet. If we could rely less heavily on disjunction we would already dramatically speed up constraint solving. My problem is that I don't know how to compute the meet or join of two types where one is a type variable (e.g., %0 <: any P).

Literal types are causing combinatorial explosion but solutions to this problem in Swift have already been partially documented.

I don't understand what you mean by this.

The right term is "component". My claim is that any component of a constraint set can be solved in isolation because it cannot contain information that would be help solve another component. So we have a way to divide and conquer.

Further, I think that we can identify new components as we solve constraints. If we start from a component with constraints C1, C2, and C3 such that C2 and C3 depend on C1 but are otherwise unrelated, then after we solved C1 we can solve C2 and C3 separately. That would attenuate combinatorial explosion if C2 and C3 are large disjunctions.

[kyouko-taiga]

I've run some experiment with this approach and could not see significant improvement. It seems like the performance bottleneck is more about name resolution than it is about solving disjunctions.

The code that I wrote to implement the constraint component extraction is here: https://gist.github.com/kyouko-taiga/09498a39acb00746d8721a4f9731df8b