Practical type inference for first-class polymorphism

Type inference is a key component of modern statically typed programming languages. It allows programmers to omit many—and in some cases all—type annotations from programs. Type inference becomes particularly interesting theoretically and from an implementation standpoint in the presence of polymorphism. Hindley-Damas-Milner type inference, underlying modern functional programming languages with let-bound polymorphism, allows for full type reconstruction for programs with types that (i) only contain top-level quantifiers, and (ii) can only be instantiated with quantifier-free types. As soon as one attempts to overcome these barriers to allow higher-rank or impredicative polymorphism full type reconstruction becomes either undecidable or non-modular because many typeable programs no longer possess principal types. The only hope then for modular and decidable type inference for first-class polymorphism arises from exploiting type annotations to guide the type checker in a mixture of type reconstruction and type checking. The first contribution of this dissertation is a formal study of various theoretical properties of annotation-guided inference for predicative higher-rank types. The second contribution is the presentation of a type system and inference algorithm that lift both Damas-Milner restrictions, allowing impredicative higher-rank types. A central claim of this dissertation is that annotation-guided type inference for first-class polymorphism is compatible with intuitive specifications that do not have to be more complicated than the familiar Damas-Milner type system