Set-theoretic types for polymorphic variants
Giuseppe Castagna, Tommaso Petrucciani, Kim Ngoc Nguyen · 2016
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.