Swift's approach to type inference proceeds in two phases. In the first phrase, we walk the expression, and generate type variables for each sub-expression, relating those type variables with constraints. In the second phase, we try to find an assignment of concrete types to type variables that simultaneously satisfies all constraints. When an expression involves references to overloaded names, the type checker collects the types of all overloads in each set, and forms a disjunction. A disjunction is just a list of possible choices for the type that this expression will receive.

After we generate constraints, we start trying to solve each constraint in turn. Eventually, we will run out of constraints to solve that are not disjunctions. We select one of the remaining disjunctions and remove it from the list. As part of selecting the disjunction, we also "favor" some of the overload choices. We try the favored choices first, and only attempt remaining choices if none of the favored choices succeeded. When we select an overload choice, some more constraints get generated and simplified; if one of those constraints fails, our current combination of choices is not viable, and we backtrack. Otherwise, we're once again presented with the problem of selecting the next disjunction, and this continues until we've chosen an overload choice from each disjunction.

This idea of "favoring" choices that are close matches based on type was new in Swift 6.3. It works really well if every favored choice actually succeeds; we skip a lot of work in that case, and sometimes avoid backtracking altogether. But the problem was that as soon as you're off the happy path and you're looking at an impossible combination of overloads, it would sometimes attempt a large explosion of choices.

I added a new analysis to distinguish overload choices which *might* match from those that *definitely cannot* match. Disabling impossible choices improves performance in the worst case when a large number of combinations must be attempted. In some cases, it avoids an expensive search entirely. If we get to a point where a disjunction has zero or one choices remaining, we can immediately attempt it next, skipping the disjunction selection heuristic entirely.

This is basically just the equivalent of unit propagation in a SAT solver.

Attempting disjunctions in the correct order can make a huge difference in performance, and for disjunction selection to work, type information must "flow through" the constraint system from function arguments to results, and through closures, and so on.

A complication is that Swift has implicit conversions. If you have something like f(g()), then not only can both f() and g() be overloaded, but the result of g() might not exactly match f(); there might be an implicit conversion involved.

Some of the implicit conversions are straightforward (subclass to base class, concrete type to existential, etc) others are more esoteric (collection conversions, etc). But, there's a fixed set, and no possibility of user-defined conversions, so it's something we can analyze.

If both sides of a conversion constraint are concrete types, it becomes a yes/no a question. For example, Int can be converted to Any:

Int conv Any

Every type is also a subtype of itself wrapped in an optional:

Int conv Optional<Int>

Arrays are covariant:

Array<Int> conv Array<Any>

... and so on.

However, String cannot convert to Int, so this constraint fails:

String conv Int

Now, when one side of a conversion is a type variable, it's trickier. Suppose you have:

String conv $T0

At this point, all we can say that $T0 is a supertype of String, but we don't know what $T0 is. If $T0 is then the argument to an overloaded call, this lack of type information can cause problems.

So the constraint solver has an extra step between solving constraints and selecting a disjunction; it tries to attempt a _type variable binding_. It looks at the set of unsolved conversion constraints and tries to "guess" one of them, and binds that type variable.

The problem here is to basically compute the domain for each type variable--the set of possible concrete types it might have.

Often, constraint systems have quite simple domains, finite sets for example (and in SAT it's just {0, 1}). In Swift's case, the set of "all possible types" is infinite, because of generics, and quite complicated, so we cannot represent a domain exactly, but we can apply some rough heuristics.

If we can prove that a type variable's domain consists of exactly one type, we can bind it to that type variable, and if we can prove the domain is empty, we can bind it to anything; no matter what, some constraint will fail.

In binding inference, we had an existing optimization that would consider types that have no proper subtypes. For example, if you have

$T0 conv Int

Then in fact we know that Int (like almost all structs, and all user-defined structs) has no proper subtypes, that is, types that convert to it. So we can always bind $T0 to Int in this case.

I generalized this idea further. Suppose you instead have:

Int conv $T0

You can't apply the same optimization here, and just say that $T0 is Int. In Swift, _every_ type has supertypes; those are an optional wrapping the type, the existential types to which this type conforms, and the special standard library AnyHashable type, which is a supertype of every concrete type that conforms to Hashable.

But suppose you also have a conformance constraint, and you know that $T0 must conform to some protocol, say BinaryInteger:

Int conv $T0
$T0 conforms BinaryInteger

Well, existential types cannot conform to protocols in Swift, so we can rule out the possibility that $T0 is existential. It might still be Optional<Int> or AnyHashable, perhaps, but those don't conform to BinaryInteger either.

So now, we can "prove" that $T0's domain contains exactly one type, and so we can bind $T0 to Int.

What if you end up in a situation where you're looking at this?

Int conv $T0
$T0 conforms Sequence

Well, Int doesn't conform to Sequence, and neither does Optional<Int> or AnyHashable, so we've made a conflicting set of overload choices; we just haven't realized it yet, because the domain of $T0 is the empty set.

Now we _do_ realize it, and bind Int to $T0 anyway; this fails the conformance constraint, and in some cases, it fails it much sooner than it would have otherwise, reducing wasted time spent in dead ends.

There are more tricks possible by considering multiple adjacent constraints.

An existing optimization would compute the join of two types (the least common supertype) in a situation like this:

Foo conv $T0
Bar conv $T0

The implementation of joins() was old and incomplete though and it missed many common situations. I rewrote it to model Swift's subtyping rules faithfully. I got it to compute meets. Unlike joins, where all types are subtypes of the universal Any type, the meet can be empty. For example, suppose that Foo and Bar are classes:

$T0 conv Foo
$T0 conv Bar

By the previous rules, we cannot bind $T0 to Foo or Bar, because Foo and Bar might have proper subtypes (one might be a subclass of the other).

But if neither is a subclass of the other, then $T0's domain is empty, and we can bind $T0 to Foo or Bar at this point, and backtrack.

There are a few more combinations, for example if you have this:

Int conv $T0
$T0 conv Optional<String>

There is no type for $T0 that is a supertype of Int but also a subtype of Optional<String>.