As in ordinary ML, MinCaml infers the types of variables and functions even though they are not written in the program. This functionality is called type inference. Type inference in general is very useful for programs with polymorphic and higher-order functions in particular (though MinCaml itself is monomorphic as specified by the syntax of types).
The core of type inference in MinCaml is function Typing.g. This function takes type environment env (mapping from the names of variables to their types) and expression e, and returns the inferred type of e. It also checks the types of sub-expressions. If an undefined type variable is found, it is substituted with an appropriate type. This checking and substitution are implemented by function Typing.unify.
For example, in the case of integer addition e1 + e2 (or Add(e1, e2) in terms of Syntax.t), we first infer the type of sub-expression e1 by g env e1, which is checked against int by unify. Ditto for e2. Then, we return int as the whole expression's type.
A little more complex case is function application e e1 ... en, where e is a function and e1 through en are its arguments. In this case, the function's type can be inferred by g env e and the arguments' types by g env e1 through g env en, but the result's type cannot. Thus, we create a fresh undefined type variable t, and call unify so that g env e equals the function type from g env e1, ..., g env en to t. Then, we return t as the whole expression's type.
When a new variable is introduced as in let and let rec, the type environment env is extended. Conversely, when variable x appears, its type is obtained by looking up env. However, when a variable is not found in the type environment, it is regarded as an external variable, assigned a fresh undefined type variable, and added to the special type environment extenv for external variables. This functionality is specific to MinCaml and not available in ordinary ML. Thanks to it, external variables can be used without being declared.
Function Typing.unify recursively inspects whether two given types are equal and, if one of the types is an unfefined type variable Type.var(ref None), substitutes it with the other type so that they become equal. However, before this substitution, it is checked whether the type variable appears inside the other type. This process is called occur check. It is necessary so that the resulting type has no cycle. For example, if we unified (with no occur check) type variable α with function type int->α, the result would be an infinite type like int->int->int->... because α = int->α! In order to prevent such cases, occur check is necessary even though it may appear mysterious at first.
After type inference is finished (either by type error or by normal termination), Typing.deref_typ replaces all type variables with their contents for the sake of simplicity. Type variables that are still undetermined are substituted at will with int. This feature is also specific to MinCaml.