occur. Such a chain could also exist between the conclusion of the proof and the rule for topmost expression. All proofs must have the so sketched shape. Because the only choice in a proof with respect of rule selection are the and chains, the form of the proof suggests the question whether it can be made more precise, where these chains might not be needed. This is in fact possible and leads to a variant of the rules system with no such rules. Syntax-directed rule system A contemporary treatment of HM uses a purely syntax-directed rule system due to Clement as an intermediate step. In this system, the specialization is located directly after the original rule and merged into it, while the generalization becomes part of the rule. There the generalization is also determined to always produce the most general type by introducing the function , which quantifies all monotype variables not bound in . Formally, to validate that this new rule system is equivalent to the original , one has to show that , which decomposes into two sub-proofs: (Consistency) (Completeness) While consistency can be seen by decomposing the rules and of into proofs in , it is likely visible that is incomplete, as one cannot show in , for instance, but only . An only slightly weaker version of completeness is provable though, namely implying, one can derive the principal type for an expression in allowing us to generalize the proof in the end. Comparing and , now only monotypes appear in the judgments of all rules. Additionally, the shape of any possible proof with the deduction system is now identical to the shape of the expression (both seen as trees). Thus the expression fully determines the shape of the proof. In the shape would likely be determined with respect to all rules except and , which allow building arbitrarily long branches (chains) between the other nodes. Degrees of freedom instantiating the rules Now that the shape of the proof is known, one is already close to formulating a type inference algorithm. Because any proof for a given expression must have the same shape, one can assume the monotypes in the proof's judgements to be undetermined and consider how to determine them. Here, the substitution (specialisation) order comes into play. Although at the first glance one cannot determine the types locally, the hope is that it is possible