Qualified types for MLF

ML-F is a type system that extends a functional language with impredicative higher-rank polymorphism. Type inference remains possible and only in some clearly defined situations, a local type annotation is required. Qualified types are a general concept that can accomodate a wide range of type systems extension, for example, type classes in Haskell. We show how the theory of qualified types can be used seamlessly with the higher-ranked impredicative polymorphism of ML-F. A core contribution of the paper is that we show a solution to the non-trivial problem of evidence translation in the presence of impredicative data types. (Note: one can experiment with MLF types with the experimental Morrow interpreter. However, this does not yet implement the qualified type extension discussed in the paper).