# Does Damas-Milner still have principal types if existential type schemata are added?

In the Damas-Milner type system, type schemata can be formed in two ways:

• $T$
• $\forall X. S$

Where $T$ ranges over monotypes and $S$ ranges over type schemata. The type-checking algorithm for this system is well known, and explanations of it can be found in several places.

What happens if I add a third type schema former?

• $\exists X. S$

In other words, type schemata must still be in prenex normal form, but both universal and existential quantifiers may be used. As in Damas-Milner, only let-bound variables may be ascribed type schemata.

My questions are:

1. Does this system still have principal types?
2. How much does the type-checking algorithm change?