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.