fully informed type-checking algorithms can. Type-checking here means that an algorithm does not have to find a proof, but only to validate a given one. Efficiency is slightly reduced because the binding of type variables in the context has to be maintained to allow computation of and enable an occurs check to prevent the building of recursive types during . An example of such a case is , for which no type can be derived using HM. Practically, types are only small terms and do not build up expanding structures. Thus, in complexity analysis, one can treat comparing them as a constant, retaining O(1) costs. Proving the algorithm In the previous section, while sketching the algorithm its proof was hinted at with metalogical argumentation. While this leads to an efficient algorithm J, it is not clear whether the algorithm properly reflects the deduction systems D or S which serve as a semantic base line. The most critical point in the above argumentation is the refinement of monotype variables bound by the context. For instance, the algorithm boldly changes the context while inferring e.g. , because the monotype variable added to the context for the parameter later needs to be refined to when handling application. The problem is that the deduction rules do not allow such a refinement. Arguing that the refined type could have been added earlier instead of the monotype variable is an expedient at best. The key to reaching a formally satisfying argument is to properly include the context within the refinement. Formally, typing is compatible with substitution of free type variables. To refine the free variables thus means to refine the whole typing. Algorithm W From there, a proof of algorithm J leads to algorithm W, which only makes the side effects imposed by the procedure explicit by expressing its serial composition by means of the substitutions . The presentation of algorithm W in the sidebar still makes use of side effects in the operations set in italic, but these are now limited to generating fresh symbols. The form of judgement is , denoting a function with a context and expression as parameter producing a monotype together with a substitution. is a side-effect free version of producing a substitution which is the most general unifier. While algorithm W is normally considered to be the HM algorithm and is often directly presented after the rule system in literature,