to refine them with the help of the order while traversing the proof tree, additionally assuming, because the resulting algorithm is to become an inference method, that the type in any premise will be determined as the best possible. And in fact, one can, as looking at the rules of suggests: : The critical choice is . At this point, nothing is known about , so one can only assume the most general type, which is . The plan is to specialize the type if it should become necessary. Unfortunately, a polytype is not permitted in this place, so some has to do for the moment. To avoid unwanted captures, a type variable not yet in the proof is a safe choice. Additionally, one has to keep in mind that this monotype is not yet fixed, but might be further refined. : The choice is how to refine . Because any choice of a type here depends on the usage of the variable, which is not locally known, the safest bet is the most general one. Using the same method as above one can instantiate all quantified variables in with fresh monotype variables, again keeping them open to further refinement. : The rule does not leave any choice. Done. : Only the application rule might force a refinement to the variables "opened" so far, as required by both premises. The first premise forces the outcome of the inference to be of the form . If it is, then fine. One can later pick its for the result. If not, it might be an open variable. Then this can be refined to the required form with two new variables as before. Otherwise, the type checking fails because the first premise inferred a type which is not and cannot be made into a function type. The second premise requires that the inferred type is equal to of the first premise. Now there are two possibly different types, perhaps with open type variables, at hand to compare and to make equal if it is possible. If it is, a refinement is found, and if not, a type error is detected again. An effective method is known to "make two terms equal" by substitution, Robinson's Unification in combination with the so-called Union-Find algorithm. To briefly summarize the union-find algorithm, given the set of all types in a proof, it allows one to group them