Extending the Type Checker of SML by Polymorphic Recursion: A Correctness Proof

We describe an extension of the type inference of Standard ML that covers polymorphic recursion. For any term t of SML, a type scheme ø and a system L of inequations between (simple) types is computed, such that the types of t are the instances of ø by substitutions S that satisfy L. The inequation constraints L are computed bottom-up in a modification of Milner's algorithm W . The correctness proof is complicated by the fact that unknowns for polytypes are needed -- in contrast to type inference for SML