Despite the great success of inferring and programming with
universal types, their dual—existential types—are much harder
to work with. Existential types are useful in building abstract types,
working with indexed types, and providing first-class
support for refinement types. This paper, set in the context of Haskell,
presents a bidirectional type-inference algorithm that infers where to introduce
and eliminate existentials without any annotations in terms, along with
an explicitly typed, type-safe core language usable as a compilation target.
This approach is backward compatible. The key ingredient is to use \emph{strong}
existentials, which support (lazily) projecting out the encapsulated data,
not weak existentials accessible only by pattern-matching.