Does Damas-Milner still have principal types if existential type schemata are added?
Yes, adding existentials doesn't add many complications for type inference, if quantifier alternation is controlled carefully. This is not surprising since universals and existentials are dual and the the function space operator gives a form of negation. Small type annotations that can help regaining type-inference are discussed in (4).

Adding existentials to pragmatically viable programming languages was first discussed in N. Perry's dissertation (1).  Perry's work was later formalised by Odersky and Läufer in (2). Läufer also described how to integrate existentials with Haskell type classes (3). 


1. N. Perry, The Implementation of Practical Functional Programming Languages.

2. K. Läufer, M. Odersky, Polymorphic type inference and abstract data types.

3. K. Läufer, Type classes with existential types.

4. M. Odersky, K. Läufer, Putting type annotations to work.