Standard ML is a useful programming language with a polymorphic type
system and a flexible module facility. One notable feature of the
core expression language of ML is that it is {\em implicitly typed}:
no explicit type information need be supplied by the programmer. In
contrast, the module language of ML is {\em explicitly typed}; in
particular, the types of parameters in parametric modules must be
supplied by the programmer. We study the type structure of Standard
ML by giving an explicitly-typed, polymorphic function calculus that
captures many of the essential aspects of both the core and module
language.
In this setting, implicitly-typed core language expressions
are regarded as a convenient short-hand for an explicitly-typed
counterpart in our function calculus. In contrast to the
Girard-Reynolds polymorphic calculus, our function calculus is
{\em predicative}: the type system may be built up by induction on
type levels. We show that, in a precise sense, the
language becomes inconsistent if restrictions imposed by type levels
are relaxed. More specifically, we prove that the important
programming features of ML cannot be added to any impredicative
language, such as the Girard-Reynolds calculus, without implicitly
assuming a type of all types.