Generalized algebraic datatypes, or GADTs, extend usual sum types in two ways: constraints on type parameters may change depending on the value constructor, and some type variables may be existentially quantified. They are described in chapter 7.
(Introduced in OCaml 4.00)
Refutation cases. (Introduced in OCaml 4.03)
Explicit naming of existentials. (Introduced in OCaml 4.13.0)