ML is remarkable in providing statically typed polymorphism without the programmer ever having to write any type annotations. The cost of this parsimony is that the programmer is limited to a form of polymorphism in which quantifiers can occur only at the outermost level of a type and type variables can be instantiated only with monomorphic types.

The general problem of type inference for unrestricted System F-style polymorphism is undecidable in general. Nevertheless, the literature abounds with a range of proposals to bridge the gap between ML and System F by augmenting ML with type annotations or other features.

We present a new proposal, with different goals to much of the existing literature. Our aim is to design a minimal extension to ML to support first-class polymorphism. We err on the side of explicitness over parsimony, extending ML with two new features. First, λ- and let-bindings may be annotated with arbitrary System F types. Second, variable occurrences may be frozen, explicitly disabling instantiation. The resulting language is not always as concise as more sophisticated systems, but in practice it does not appear to require a great deal more ink. FreezeML is a conservative extension of ML, equipped with type-preserving translations back and forth between System F. It admits a type inference algorithm, a mild extension of algorithm W, that is sound and complete and which yields principal types.