Tour of the Type Inferer
The type inferer assigns types to all names and expression in a unit. It does this via TypeState::equations which maps NameIDs and expression IDs to TypeVars. While NameIDs and Expressions remain constant during typeinference, TypeVars change as information is gathered.
TypeVars are either Known or Unknown, known meaning that they have a known base type (int, T, []) etc., and type parameters for the base type which themselves are other TypeVars. Unknown means that the base type is not yet known, additionally, they can have trait bounds that must be satisfied when the type goes from Unknown to Known.
The core of the type inference system is TypeState::unify which takes two things which have a type (names, expressions, typevars etc.) and unifies them into the same type if possible (same base type or unknown, traits are satisfied, parameters unify etc.), or errors otherwise. For example, unify(Unknown, int<8>) makes the left hand side an int<8>, unify(unknown1, unknown2) doesn’t result in a known type, but forces unknown1 and unknown2 to be the same type when either is unified with the other. All of this is handled within unify. unify(int<8>, int<unknown>) results in int<8>
The implementation of this is replacement, when unify has checked that two types can unify, it replaces all occurrences of either type with the least generic of the two. This is done with the replacements field in the OwnedTypeState struct.
TypeVars are not actually stored as TypeVar, they are stored as TypeVarID and you can exchange a TypeVarID for a TypeVar that is current, i.e. it doesn’t have any replaced type vars inside.
Constraints and Requirements
Unfortunately, not everything is solved with unify, in particular we might have something like a.b where we don’t know the type of a yet, which means we can’t say anything about the type of the b field. Decisions like these are deferred until later with either Constraints or Requirements which allow adding relations between types like this. Eventually (usually after types have been unified), the requirements and constraints are checked, and if enough information about them is known they perform additional unification. For example, if we now know that a is a struct and the b field has type SomeType, we now unify the Unknown type we created for the field access with SomeType.
A natural question to ask is what is the difference between requirements and constraints and why we need both. Answering this question is left as an exercise to the reader. If you do end up doing that exercise and come up with a satisfying answer, do let us know :P