ML^F: raising ML to the power of system F

We propose a type system ML F that generalizes ML with first-class polymorphism as in System F. Expressions may contain second-order type annotations. Every typable expression admits a principal type, which however depends on type annotations. Principal types capture all other types that can be obtained by implicit type instantiation and they can be inferred.All expressions of ML are well-typed without any annotations. All expressions of System F can be mechanically encoded into ML F by dropping all type abstractions and type applications, and injecting types of lambda-abstractions into ML F types. Moreover, only parameters of lambda-abstractions that are used polymorphically need to remain annotated.