Polymorphic variants are a useful feature of the OCaml language whose
current definition and implementation rely on kinding constraints to
simulate a subtyping relation via unification. This yields an awkward
formalization and results in a type system whose behaviour is in some
cases unintuitive and/or unduly restrictive.

In this work, we present an alternative formalization of polymorphic
variants, based on set-theoretic types and subtyping, that yields
a cleaner and more streamlined system. Our formalization is more
expressive than the current one (it types more programs while preserving
type safety), it can internalize some meta-theoretic properties, and it
removes some pathological cases of the current implementation resulting
in a more intuitive and, thus, predictable type system.
More generally, this work shows how to add full-fledged union types to
functional languages of the ML family that usually rely on the
Hindley-Milner type system. As an aside, our system also improves
the theory of semantic subtyping, notably by proving completeness for
the type reconstruction algorithm.