Lesson 7.5 — Swift's constraint solver: overloads, literals, and exponential expressions

Techniques: Swift's type checker — per-expression constraint generation with type variables, conformance, conversion and disjunction constraints (one per overloaded name), solved by a backtracking search that splits the constraint graph into independent components, ranks every solution with a score (non-default literal types, conversions, …) and picks the best; its exponential worst cases and the mitigations (component splitting, disjunction favoring, time and scope limits) (the design document [SWIFT-TypeCheckerDoc]; sources at swift-6.3.3-RELEASE [SWIFT-CSStep, SWIFT-CSOptimizer, SWIFT-CSSolver]) · Pebble implements: none — Pebble deliberately has no overloading, so its constraint problems (Lesson 7.6) have no disjunctions; its literal defaulting is Swift's "default literal types" · Drills: — (see §9; the model tools/course/lib/overload.py computes every table) · Prerequisites: Lessons 7.1–7.4; Lesson 6.3 (overload resolution by ranking) · Time: 3 hours

Swift combines three things that each complicate inference: overloading (the standard library defines dozens of +), literals that can have many types (1 can be Int, Double, CGFloat, UInt8, …), and bidirectional flow of type information inside an expression. It answers all three with one mechanism: turn the expression into a constraint system in which each overloaded name is a disjunction of alternatives, and search. Most expressions resolve in microseconds. Some — a few operators, a few literals, one mistake — take seconds, or end with "the compiler is unable to type-check this expression in reasonable time". This lesson explains both.

1. Problem and motivation

Swift's constraint solver

The problem. C++ resolves overloads bottom-up: each argument's type is known before its call is resolved (Lesson 6.3). Swift wants information to flow down as well — let x: Double = 1 + 2 should make the literals Double and pick the Double overload of + — and it wants generic functions, closures with inferred parameter types, and implicit conversions (optional promotion, CGFloat/Double since Swift 5.5). A bottom-up checker cannot do this, and HM cannot either: overloading means a name has several unrelated types, and choosing among them is a search problem. Swift's design [SWIFT-TypeCheckerDoc, "Approach"] limits inference to one expression or statement at a time "for purely practical reasons", generates a constraint system for it in the style of HM(X) (Lesson 7.4) extended with disjunctions, and solves it by backtracking with ranking. The price is a worst case that is exponential in the size of an expression — and, as Proposition 7.5.6 shows, not because the implementation is naive: overload resolution with generics is NP-hard.

2. Definitions and algorithms

Swift's constraint solver

Definition 7.5.1 (Swift-style constraint system)

Over type variables \(T_1, T_2, \dots\) (one per subexpression) the constraints are: - Bind/Equal \(T_i = \tau\) and \(T_i = T_j\) (unification, Lesson 7.1); - Conversion \(T_i <: T_j\) (argument conversion, optional promotion; this lesson's model uses equality only); - ConformsTo \(T_i : P\) — for a literal, \(P\) is a literal protocol with a default type (ExpressibleByIntegerLiteral, default Int; ExpressibleByFloatLiteral, default Double); - Disjunction \(D = c_1 \vee \dots \vee c_k\), each alternative \(c_i\) a conjunction of the above: one alternative per overload of a name (for a + b: \((T_a = \mathsf{Int} \wedge T_b = \mathsf{Int} \wedge T_r = \mathsf{Int}) \vee (T_a = \mathsf{Double} \wedge \dots) \vee \dots\)). A solution assigns every type variable and chooses one alternative per disjunction so that all constraints hold.

Definition 7.5.2 (Score, best solution, ambiguity)

The score of a solution is a vector of counters compared lexicographically (Swift's ScoreKind: fixes, value-to-optional conversions, …, and SK_NonDefaultLiteral, the number of literals whose type is not their protocol's default). A solution is best if no other solution has a smaller score; if two different solutions share the best score, the expression is ambiguous (an error). The lesson's model uses only the non-default-literal counter.

Definition 7.5.3 (Constraint graph and components)

The constraint graph has one node per type variable and an edge between variables that occur in a common constraint (including a common disjunction). Its connected components are independent subproblems: a solution of the whole system is a product of solutions of the components.

Algorithm 7.5.4 (Swift-style solving: split, simplify, choose, score)

• Input: a constraint system \(S\) (Definition 7.5.1) for one expression, with the contextual type (if any) as an equation.
• Output: the best solution (Definition 7.5.2), or "no solution", or "ambiguous", or "too complex" when a limit is exceeded.
• Precondition: simplification (unification and conformance checking) is sound and complete for the non-disjunctive constraints.
• Postcondition: if no limit is hit, the result is the minimum-score solution over all choices of alternatives (Theorem 7.5.5).
• Invariant: every state on the search stack satisfies all constraints simplified so far; a failed alternative leaves no trace (bindings are undone on backtracking); the search explores alternatives of each disjunction in a fixed order.

function SolveSystem(S):
    if not Simplify(S): return "no solution"            # unify equations, check conformances
    comps ← connected components of the constraint graph of S      # Definition 7.5.3
    result ← empty solution
    for each component C:                               # independent: solve separately
        sols ← Search(C)
        if sols = []: return "no solution"
        result ← result combined with Best(sols)        # "ambiguous" if Best is not unique
    return result

function Search(C):                                     # backtracking over disjunctions
    if C has no unsolved disjunction:
        bind every unbound literal variable to its protocol's default     # defaulting
        return [(Score(C), assignment)]
    D ← ChooseDisjunction(C)                            # favoring heuristics decide order
    sols ← []
    for each alternative c of D, in ChooseOrder(D):
        if steps or time exceed the limits: raise "too complex"
        C' ← C with c added
        if Simplify(C'):                                # propagate; fail early
            sols ← sols ++ Search(C')                   # (the real solver prunes by score)
    return sols

function Simplify(C):  apply equalities (union-find); fail if a literal variable is bound
                       to a type outside its protocol, or two different types are equated
function Score(C):     the number of literal variables bound to a non-default type

3. Worked example

Swift's constraint solver

The model tools/course/lib/overload.py (arith, solve) with the overload sets +: (Int,Int)->Int, (Double,Double)->Double, (String,String)->String and *: (Int,Int)->Int, (Double,Double)->Double. Expression let r: Double = 1 + 2 * d with d: Double. Type variables: \(T_1\) (literal 1), \(T_2\) (literal 2), \(T_d = \mathsf{Double}\), \(T_{*}\) for 2 * d, \(T_{+}\) for the whole expression, with the contextual equation \(T_{+} = \mathsf{Double}\). Disjunction order: * first, then + (the order of creation).

state	disjunction	alternative	propagation	verdict
1	*	(Int,Int)->Int	\(T_d = \mathsf{Int}\) contradicts \(T_d = \mathsf{Double}\)	fail
2	*	(Double,Double)->Double	\(T_2 = \mathsf{Double}\) (allowed: Double is an integer-literal type), \(T_{*} = \mathsf{Double}\)	ok
3	+	(Int,Int)->Int	\(T_{*} = \mathsf{Int}\) contradicts state 2	fail
4	+	(Double,Double)->Double	\(T_1 = \mathsf{Double}\), \(T_{+} = \mathsf{Double}\) = context	ok: solution
5	+	(String,String)->String	\(T_1 = \mathsf{String}\): not an integer-literal type	fail

Five states, one solution, score 2 (both integer literals are Double, not their default Int). Without the contextual type the search is the same (5 states) and still finds only this solution, because d forces Double. For 1 + 2 alone the model explores 3 states and finds two solutions — (Int,Int)->Int with score 0 and (Double,Double)->Double with score 2 — and the ranking picks Int: that is why let x = 1 + 2 is an Int in Swift, and why Pebble's defaulting to int (Lesson 7.6) is the same rule without the search.

4. Invariants and correctness

Swift's constraint solver

Theorem 7.5.5 (The search is complete and the ranking is exact)

If no limit is exceeded, Algorithm 7.5.4 returns a solution iff one exists, and the returned solution has the minimum score over all solutions; it reports "ambiguous" iff at least two solutions share that minimum.

Proof

Components (Definition 7.5.3): two components share no type variable and no constraint, so a pair of solutions of the components is a solution of the whole and conversely; minimizing a score that is a sum over literals (hence over components) componentwise minimizes the total. Search: by induction on the number of unsolved disjunctions of a component. With none, Simplify has already decided every equation and conformance, so the current assignment (after defaulting, which is admissible because the default belongs to its protocol) is the unique completion, and it is returned. Otherwise every solution chooses exactly one alternative of \(D\); the loop tries each, and Simplify removes an alternative only if it is inconsistent with constraints every solution must satisfy (soundness of simplification); by the induction hypothesis the recursive call returns all solutions extending it. The union over the alternatives is therefore the set of all solutions, and Best selects the minimum and detects ties.

Proposition 7.5.6 (Overload resolution with generics is NP-hard)

Deciding whether an expression built from overloaded functions and one call of a generic function has a solution is NP-hard; hence (unless P = NP) every complete solver for Swift-style constraint systems has super-polynomial worst cases.

Proof

Reduction from 3-SAT. Given a formula over \(x_1, \dots, x_n\) with clauses \(c_1, \dots, c_m\), declare two types T, F and a type OK, and: - for each variable, a function pick_i with two overloads, () -> T and () -> F; - for each clause \(c_j = (\ell_1 \vee \ell_2 \vee \ell_3)\) over variables \(x_a, x_b, x_c\), a function clause_j with one overload (V_a, V_b, V_c) -> OK for each of the 7 assignments \((V_a, V_b, V_c) \in \{T, F\}^3\) that make the clause true; - one generic function sat<A_1, …, A_n>(_: A_1, …, _: A_n, _: (A_{a_1}, A_{b_1}, A_{c_1}) -> OK, …, _: (A_{a_m}, A_{b_m}, A_{c_m}) -> OK).

The expression sat(pick_1(), …, pick_n(), clause_1, …, clause_m) has size \(O(n + m)\). A solution chooses an overload of each pick_i, which fixes the generic parameter \(A_i\) to T or F — one truth value per variable, shared by every clause through the type variables \(A_i\) — and an overload of each clause_j whose parameter types equal \((A_{a_j}, A_{b_j}, A_{c_j})\), which exists iff that assignment satisfies \(c_j\). So the expression type-checks iff the formula is satisfiable. The course's model builds exactly this system (overload.sat_problem), and test_ch07.py checks on 300 random formulas that the solver finds a solution iff a brute-force check finds a satisfying assignment.

5. Complexity

Technique	Time (worst)	Time (typical)	Space	Variables
Swift-style search (Algorithm 7.5.4)	\(O(\prod_{i} k_i)\) states per component, times propagation; NP-hard in general (Proposition 7.5.6)	microseconds: propagation leaves one viable alternative per disjunction	the trail of bindings, \(O(\text{constraints})\)	\(k_i\) alternatives of disjunction \(i\), per component

Justification. The search tree has one level per disjunction and at most \(k_i\) children at level \(i\), so at most \(\prod_i k_i\) leaves; each state costs one Simplify. Splitting into components turns the product over all disjunctions into a sum of products over components, which is why independent subexpressions do not multiply.

Pathological family, derived. Encode the formula \(\varphi_n = (y \vee y \vee y) \wedge (\neg y \vee \neg y \vee \neg y)\) with \(y = x_n\) and \(x_1, \dots, x_{n-1}\) unused, and search the disjunctions in the order pick_1, …, pick_n, clause_1, clause_2 (the order of Proposition 7.5.6's expression). The first \(n - 1\) levels have 2 alternatives each and no constraint prunes them: \(2 + 4 + \dots + 2^{n-1} = 2^n - 2\) states. Level \(n\) tries both values of \(y\) under each of the \(2^{n-1}\) prefixes: \(2^n\) states. Under \(y = T\), clause_1 tries its 7 alternatives (one consistent) and clause_2 then tries 7 and all fail: 14 states; under \(y = F\), all 7 alternatives of clause_1 fail: 7 states. Total \(2^n - 2 + 2^n + 21 \cdot 2^{n-1} = 12.5 \cdot 2^n - 2\), and there is no solution. The model reproduces this count exactly (48 states for \(n = 2\), 3198 for \(n = 8\); test_ch07.py). A heuristic that picks the most constrained disjunction first (clause_1) would fail after 21 states — which is what favoring is for — but for every heuristic there are formulas on which it is exponential (unless P = NP).

Real-world scale. Swift's own test suite keeps a directory of expressions known to hit the limits: 47 test files in validation-test/Sema/type_checker_perf/slow/ at swift-6.3.3-RELEASE, 32 of which expect the "reasonable time" diagnostic, next to 159 test files of formerly slow expressions in …/fast/ that the solver now handles (counted in a sparse checkout of the tag; §7). One of them, issue-52861.swift, "type checks in ~800ms with the default limits" according to its own comment.

6. Variants and refinements

Swift's constraint solver

• Component splitting (SplitterStep [SWIFT-CSStep]): solve independent parts of the constraint graph separately (Definition 7.5.3). Trade-off: turns products into sums; useless when one variable connects everything (a long chain of operators).
• Disjunction favoring / pruning (determineBestChoicesInContext in CSOptimizer.cpp [SWIFT-CSOptimizer]): before searching, rank the overloads of each disjunction by how well they match the already-known argument types and literal defaults, try the favored ones first, and skip the others when a favored one succeeds. Trade-off: orders of magnitude faster on common code; must not change which solution wins, which constrains the heuristics.
• Limits (-solver-expression-time-threshold, -solver-scope-threshold [SWIFT-FrontendOptions]; isTooComplex in CSSolver.cpp [SWIFT-CSSolver]): abort with "unable to type-check this expression in reasonable time". Trade-off: bounded compile time at the price of rejecting valid code, and of a diagnostic that names no culprit.
• Scoped inference: Swift limits a constraint system to one expression; SE-0326 [SE0326] extended it to multi-statement closures by solving the closure body after the enclosing expression (conjunctions solved in isolation). Trade-off: more inference, bounded growth of each system.
• No overloading (Rust, Go, Pebble): traits or interfaces instead of ad-hoc overloads, so inference has no disjunctions. Trade-off: no + on unrelated types without a trait; linear-time inference.

7. In real compilers

Swift's constraint solver

The Swift compiler is the reference: constraint generation in lib/Sema/CSGen.cpp, the solver steps (SplitterStep, ComponentStep, DisjunctionStep) in lib/Sema/CSStep.cpp [SWIFT-CSStep], the favoring pass in lib/Sema/CSOptimizer.cpp [SWIFT-CSOptimizer], the scores (ScoreKind, including SK_NonDefaultLiteral) in include/swift/Sema/ConstraintSystem.h, and the limits and the entry point ConstraintSystem::solve in lib/Sema/CSSolver.cpp [SWIFT-CSSolver]. C# performs a comparable (but bottom-up) resolution for lambdas passed to overloaded methods; Ada resolves overloads over whole expressions with two passes. No swiftc is available in the course container (the Swift toolchain host is not reachable), so the box below shows Swift's behavior through its own sources and test suite at the pinned tag.

Expressions Swift 6.3.3 cannot type-check in reasonable time (quoted from its test suite)

Reproduce (Swift 6.3.3 sources, swift-6.3.3-RELEASE; curl):

B=https://raw.githubusercontent.com/swiftlang/swift/swift-6.3.3-RELEASE
curl -sSL $B/include/swift/AST/DiagnosticsSema.def | grep -A2 'ERROR(expression_too_complex'
curl -sSL $B/validation-test/Sema/type_checker_perf/slow/issue-53523.swift
curl -sSL $B/validation-test/Sema/type_checker_perf/slow/issue-52861.swift

Output (complete; quoted source files, not a compiler run):

ERROR(expression_too_complex,none,
      "the compiler is unable to type-check this expression in reasonable time; "
      "try breaking up the expression into distinct sub-expressions", ())
// RUN: %target-typecheck-verify-swift -solver-scope-threshold=1000

// https://github.com/swiftlang/swift/issues/53523

// This is invalid: we're mixing Double and Int.

public func slow(d: Double, n: Int) {
  return d * 1.0 + 1.0 / n + d / d
  // expected-error@-1 {{reasonable time}}
}
// RUN: %target-typecheck-verify-swift -solver-scope-threshold=1000
// REQUIRES: objc_interop

// https://github.com/swiftlang/swift/issues/52861

// This type checks in ~800ms with the default limits, but we make it fail sooner.

import simd

func test(_ p0: float2, _ p1: float2, _ p2: float2, _ p3: float2) {
    let i = 3*(-p0 + 3*p1) - (3*p2 + p3) // expected-error{{reasonable time}}
    let j = 6*(p0 - 2*p1 + p2) // expected-error{{reasonable time}}
    let k = 3*(p1 - p0)
    print(i, j, k)
}
test(float2(0.1, 1.2), float2(2.3, 3.4), float2(4.5, 5.6), float2(6.7, 7.8))

What to notice: issue-53523 is an invalid expression of five operators: proving that no combination of the overloads of *, + and / (and the literal types of 1.0) works requires exhausting the search — the no-solution case of §5, where favoring cannot help because nothing succeeds. issue-52861 is valid: float2 (SIMD2<Float>) has scalar–vector overloads of * and - in addition to the scalar ones, so each literal and operator has several viable alternatives that propagation does not prune — about 0.8 s at the default limits, per the file's own comment. The RUN lines set a lower -solver-scope-threshold so the test fails fast; the diagnostic text is the one in DiagnosticsSema.def.

8. Comparison

Technique	Power / precision	Speed (asymptotic · practical)	Output / error quality	Implementation effort	Typical use
Swift's constraint solver	Overloads, literals of many types, generics, conversions and bidirectional flow within an expression; exact best solution by score (Theorem 7.5.5)	Exponential worst case, NP-hard (Proposition 7.5.6) · microseconds typically; seconds, or the "reasonable time" error, on the §7 tests	Excellent when one solution exists; ambiguity and "too complex" errors name no culprit	Very high: generation, graph splitting, disjunction heuristics, scoring, diagnostics by "fixes"	Swift; the model in tools/course/lib/overload.py

Choose a search-based solver only if the language needs ad-hoc overloading and bidirectional inference in the same expression; bound the search, split components, and invest in favoring heuristics from day one. Pebble, Rust and Go avoid the whole problem by having no overloading; C++ avoids it by resolving bottom-up.

9. Assessment

Technique	Quiz ids	Drill	Flashcard tag	Exercises
Swift's constraint solver	swift-states, swift-family-states	— (a drill over random overloaded expressions would mostly produce trivially propagated problems; the quiz items swift-states and swift-family-states are computed with overload.solve)	swift-solver	—

References

See the chapter references.