Type Checking and Inference for Polymorphic and Existential Types

This paper proves undecidability of type checking and type inference problems in some variants of typed lambda calculi with polymorphic and existen-tial types. First, type inference in the domain-free polymorphic lambda calculus is proved to be unde-cidable, and then it is proved that type inference is undecidable in the negation, conjunction, and exis-tence fragment of the domain-free typed lambda cal-culus. Secondly, their variants with multiple quanti-fier rules are introduced, and their type checking and type inference are proved to be undecidable. Finally, it is proved that we can reduce undecidability of type checking and type inference problems in the Curry-style lambda calculus in negation, conjunction, and existential fragment to undecidability of those prob-lems in another variant of the domain-free polymor-phic lambda calculus