Existential type systems between Church and Curry style (type-free style)

We study type checking, typability, and type inference problems for second-order existential systems in type-free style. The type-free style is an intermediate representation of terms between the Curry style and the Church style. Terms in the type-free style contain information on where the existential quantifier elimination and introduction take place, but omit the information on which types are involved. We show that all the problems are undecidable employing reduction of second-order unification for considerably restricted special instances in flat form. These results hold even in a fragment of the existential system where →,∃→,∃ are only used and in case of predicative fragments of the existential systems.