Constraint Generation¶

The process of constraint generation produces a constraint system that relates the types of the various subexpressions within an expression. Programmatically, constraint generation walks an expression from the leaves up to the root, assigning a type (which often involves type variables) to each subexpression as it goes.

Constraint generation is driven by the syntax of the expression, and each different kind of expression—function application, member access, etc.—generates a specific set of constraints. Here, we enumerate the primary expression kinds in the language and describe the type assigned to the expression and the constraints generated from such as expression. We use T(a) to refer to the type assigned to the subexpression a. The constraints and types generated from the primary expression kinds are:

Declaration reference

An expression that refers to a declaration x is assigned the type of a reference to x. For example, if x is declared as var x: Int, the expression x is assigned the type @lvalue Int. No constraints are generated.

When a name refers to a set of overloaded declarations, the selection of the appropriate declaration is handled by the solver. This particular issue is discussed in the Overloading section. Additionally, when the name refers to a generic function or a generic type, the declaration reference may introduce new type variables; see the Polymorphic Types section for more information.

Member reference

A member reference expression a.b is assigned the type T0 for a fresh type variable T0. In addition, the expression generates the value member constraint T(a).b == T0. Member references may end up resolving to a member of a nominal type or an element of a tuple; in the latter case, the name (b) may either be an identifier or a positional argument (e.g., 1).

Note that resolution of the member constraint can refer to a set of overloaded declarations; this is described further in the Overloading section.

Unresolved member reference

An unresolved member reference .name refers to a member of a enum type. The enum type is assumed to have a fresh variable type T0 (since that type can only be known from context), and a value member constraint T0.name == T1, for fresh type variable T1, captures the fact that it has a member named name with some as-yet-unknown type T1. The type of the unresolved member reference is T1, the type of the member. When the unresolved member reference is actually a call .name(x), the function application is folded into the constraints generated by the unresolved member reference.

Note that the constraint system above actually has insufficient information to determine the type T0 without additional contextual information. The Overloading section describes how the overload-selection mechanism is used to resolve this problem.

Function application

A function application a(b) generates two constraints. First, the applicable function constraint T0 -> T1 ==Fn T(a) (for fresh type variables T0 and T1) captures the rvalue-to-lvalue conversion applied on the function (a) and decomposes the function type into its argument and result types. Second, the conversion constraint T(b) <c T0 captures the requirement that the actual argument type (b) be convertible to the argument type of the function. Finally, the expression is given the type T1, i.e., the result type of the function.

Construction

A type construction``A(b)``, where A refers to a type, generates a construction constraint T(b) <C A, which requires that A have a constructor that accepts b. The type of the expression is A.

Note that construction and function application use the same syntax. Here, the constraint generator performs a shallow analysis of the type of the “function” argument (A or a, in the exposition above); if it obviously has metatype type, the expression is considered a coercion/construction rather than a function application. This particular area of the language needs more work.

Subscripting

A subscript operation a[b] is similar to function application. A value member constraint T(a).subscript == T0 -> T1 treats the subscript as a function from the key type to the value type, represented by fresh type variables T0 and T1, respectively. The constraint T(b) <c T0 requires the key argument to be convertible to the key type, and the type of the subscript operation is T1.

Literals

A literal expression, such as 17, 1.5, or "Hello, world!, is assigned a fresh type variable T0. Additionally, a literal constraint is placed on that type variable depending on the kind of literal, e.g., “T0 is an integer literal.”

Closures

A closure is assigned a function type based on the parameters and return type. When a parameter has no specified type or is positional ($1, $2, etc.), it is assigned a fresh type variable to capture the type. Similarly, if the return type is omitted, it is assigned a fresh type variable.

When the body of the closure is a single expression, that expression participates in the type checking of its enclosing expression directly. Otherwise, the body of the closure is separately type-checked once the type checking of its context has computed a complete function type.

Array allocation

An array allocation new A[s] is assigned the type A[]. The type checker (separately) checks that T(s) is an array bound type.

Address of

An address-of expression &a always returns an @inout type. Therefore, it is assigned the type @inout T0 for a fresh type variable T0. The subtyping constraint @inout T0 < @lvalue T(a) captures the requirement that input expression be an lvalue of some type.

Ternary operator

A ternary operator``x ? y : z`` generates a number of constraints. The type T(x) must conform to the LogicValue protocol to determine which branch is taken. Then, a new type variable T0 is introduced to capture the result type, and the constraints T(y) <c T0 and T(z) <c T0 capture the need for both branches of the ternary operator to convert to a common type.

There are a number of other expression kinds within the language; see the constraint generator for their mapping to constraints.

func negate(x: Int) -> Int { return -x }
func negate(x: Double) -> Double { return -x }

enum Optional<T> {
  case None
  case Some(T)
}

func min<T : Comparable>(x: T, y: T) -> T {
  if y < x { return y }
  return x
}

class Dictionary<Key : Hashable, Value> {
  // ...
}

Simplification¶

The constraint generation process introduces a number of constraints that can be immediately solved, either directly (because the solution is obvious and trivial) or by breaking the constraint down into a number of smaller constraints. This process, referred to as simplification, canonicalizes a constraint system for later stages of constraint solving. It is also re-invoked each time the constraint solver makes a guess (at resolving an overload or binding a type variable, for example), because each such guess often leads to other simplifications. When all type variables and overloads have been resolved, simplification terminates the constraint solving process either by detecting a trivial constraint that is not satisfied (hence, this is not a proper solution) or by reducing the set of constraints down to only simple constraints that are trivially satisfied.

The simplification process breaks down constraints into simpler constraints, and each different kind of constraint is handled by different rules based on the Swift type system. The constraints fall intofive categories: relational constraints, member constraints, type properties, conjunctions, and disjunctions. Only the first three kinds of constraints have interesting simplification rules, and are discussed in the following sections.

A -> B <c C -> D

Strategies¶

The basic approach to constraint solving is to simplify the constraints until they can no longer be simplified, then produce (and check) educated guesses about which declaration from an overload set should be selected or what concrete type should be bound to a given type variable. Each guess is tested as an assumption, possibly with other guesses, until the solver either arrives at a solution or concludes that the guess was incorrect.

Within the implementation, each guess is modeled as an assumption within a new solver scope. The solver scope inherits all of the constraints, overload selections, and type variable bindings of its parent solver scope, then adds one more guess. As such, the solution space explored by the solver can be viewed as a tree, where the top-most node is the constraint system generated directly from the expression. The leaves of the tree are either solutions to the type-checking problem (where all constraints have been simplified away) or represent sets of assumptions that do not lead to a solution.

The following sections describe the techniques used by the solver to produce derived constraint systems that explore the solution space.

Comparing Solutions¶

The solver explores a potentially large solution space, and it is possible that it will find multiple solutions to the constraint system as given. Such cases are not necessarily ambiguities, because the solver can then compare the solutions to to determine whether one of the solutions is better than all of the others. To do so, it computes a “score” for each solution based on a number of factors:

• How many user-defined conversions were applied.
• How many non-trivial function conversions were applied.
• How many literals were given “non-default” types.

Solutions with smaller scores are considered better solutions. When two solutions have the same score, the type variables and overload choices of the two systems are compared to produce a relative score:

• If the two solutions have selected different type variable bindings for a type variable where a “more specific” type variable is a better match, and one of the type variable bindings is a subtype of the other, the solution with the subtype earns +1.
• If an overload set has different selected overloads in the two soluions, the overloads are compared. If the type of the overload picked in one solution is a subtype of the type of the overload picked in the other solution, then first solution earns +1.

The solution with the greater relative score is considered to be better than the other solution.

Locators¶

During constraint generation and solving, numerous constraints are created, broken apart, and solved. During constraint application as well as during diagnostics emission, it is important to track the relationship between the constraints and the actual expressions from which they originally came. For example, consider the following type checking problem:

struct X {
  // user-defined conversions
  func [conversion] __conversion () -> String { /* ... */ }
  func [conversion] __conversion () -> Int { /* ... */ }
}

func f(i : Int, s : String) { }

var x : X
f(10.5, x)

This constraint system generates the constraints “T(f) ==Fn T0 -> T1” (for fresh variables T0 and T1), “(T2, X) <c T0” (for fresh variable T2) and “T2 conforms to ``FloatLiteralConvertible”. As part of the solution, after T0 is replaced with (i : Int, s : String), the second of these constraints is broken down into “T2 <c ``Int” and “X <c String”. These two constraints are interesting for different reasons: the first will fail, because Int does not conform to FloatLiteralConvertible. The second will succeed by selecting one of the (overloaded) conversion functions.

In both of these cases, we need to map the actual constraint of interest back to the expressions they refer to. In the first case, we want to report not only that the failure occurred because Int is not FloatLiteralConvertible, but we also want to point out where the Int type actually came from, i.e., in the parameter. In the second case, we want to determine which of the overloaded conversion functions was selected to perform the conversion, so that conversion function can be called by constraint application if all else succeeds.

Locators address both issues by tracking the location and derivation of constraints. Each locator is anchored at a specific expression, i.e., the function application f(10.5, x), and contains a path of zero or more derivation steps from that anchor. For example, the “T(f) ==Fn T0 -> T1” constraint has a locator that is anchored at the function application and a path with the “apply function” derivation step, meaning that this is the function being applied. Similarly, the “(T2, X) <c T0 constraint has a locator anchored at the function application and a path with the “apply argument” derivation step, meaning that this is the argument to the function.

When constraints are simplified, the resulting constraints have locators with longer paths. For example, when a conversion constraint between two tuples is simplified conversion constraints between the corresponding tuple elements, the resulting locators refer to specific elements. For example, the T2 <c Int constraint will be anchored at the function application (still), and have two derivation steps in its path: the “apply function” derivation step from its parent constraint followed by the “tuple element 0” constraint that refers to this specific tuple element. Similarly, the X <c String constraint will have the same locator, but with “tuple element 1” rather than “tuple element 0”. The ConstraintLocator type in the constraint solver has a number of different derivation step kinds (called “path elements” in the source) that describe the various ways in which larger constraints can be broken down into smaller ones.

function application -> apply argument -> tuple element #1 -> conversion member

function application -> apply argument -> tuple element #0

func f(i : Int, s : String) { }
func g() -> (f : Float, x : X) { }

f(g())

function application -> apply argument -> tuple element #0

function application of g -> tuple element #0

Constraint Graph¶

The constraint graph describes the relationships among type variables in the constraint system. Each vertex in the constraint graph corresponds to a single type variable. The edges of the graph correspond to constraints in the constraint system, relating sets of type variables together. Technically, this makes the constraint graph a multigraph, although the internal representation is more akin to a graph with multiple kinds of edges: each vertex (node) tracks the set of constraints that mention the given type variable as well as the set of type variables that are adjacent to this type variable. A vertex also includes information about the equivalence class corresponding to a given type variable (when type variables have been merged) or the binding of a type variable to a specific type.

The constraint graph is critical to a number of solver optimizations. For example, it is used to compute the connected components within the constraint graph, so that each connected component can be solved independently. The partial results from all of the connected components are then combined into a complete solution. Additionally, the constraint graph is used to direct simplification, described below.

Simplification Worklist¶

When the solver has attempted a type variable binding, that binding often leads to additional simplifications in the constraint system. The solver will query the constraint graph to determine which constraints mention the type variable and will place those constraints onto the simplification worklist. If those constraints can be simplified further, it may lead to additional type variable bindings, which in turn adds more constraints to the worklist. Once the worklist is exhausted, simplification has completed. The use of the worklist eliminates the need to reprocess constraints that could not have changed because the type variables they mention have not changed.

Solver Scopes¶

The solver proceeds through the solution space in a depth-first manner. Whenever the solver is about to make a guess—such as a speculative type variable binding or the selection of a term from a disjunction—it introduces a new solver scope to capture the results of that assumption. Subsequent solver scopes are nested as the solver builds up a set of assumptions, eventually leading to either a solution or an error. When a solution is found, the stack of solver scopes contains all of the assumptions needed to produce that solution, and is saved in a separate solution data structure.

The solver scopes themselves are designed to be fairly cheap to create and destroy. To support this, all of the major data structures used by the constraint solver have reversible operations, allowing the solver to easily backtrack. For example, the addition of a constraint to the constraint graph can be reversed by removing that same constraint. The constraint graph tracks all such additions in a stack: pushing a new solver scope stores a marker to the current top of the stack, and popping that solver scope reverses all of the operations on that stack until it hits the marker.

Online Scoring¶

As the solver evaluates potential solutions, it keeps track of the score of the current solution and of the best complete solution found thus far. If the score of the current solution is ever greater than that of the best complete solution, it abandons the current solution and backtracks to continue its search.

The solver makes some attempt at evaluating cheaper solutions before more expensive solutions. For example, it will prefer to try normal conversions before user-defined conversions, prefer the “default” literal types over other literal types, and prefer cheaper conversions to more expensive conversions. However, some of the rules are fairly ad hoc, and could benefit from more study.

Arena Memory Management¶

Each constraint system introduces its own memory allocation arena, making allocations cheap and deallocation essentially free. The allocation arena extends all the way into the AST context, so that types composed of type variables (e.g., T0 -> T1) will be allocated within the constraint system’s arena rather than the permanent arena. Most data structures involved in constraint solving use this same arena.