Using abstract types as type-level tags is a dangerous anti-pattern, since the typechecker can only prove that they are not equal inside the current module. To make clear that the values are not intended to be used it is better to define private constructor:
type empty = private Empty_tag
type nonempty = private Nonempty_tag
which keeps a proof that the type two types are not equal available to the typechecker because Empty_tag ≠ Nonempty_tag.
GADTs are generalized because they introduce the possibility to have existentially quantified type variable in the argument of the constructors:
type any_list = Any: 'a list -> any_list
and to refine the constructed type in function of the constructor
type _ numty =
| Int: int num
| Float: float num
In other words, observing a constructor allow you to learn type equality about the type in the corresponding case.
Both features are not possible with a standard ADT . (The two features are partially independent, and before the final design GADTs, they were separate discussions on how to have existential quantification in variant types, but the feature was very easy to add to GADTs as “constructors + type equations” so
both features were introduced in the same package) .
Going back to the type equality aspect, this is why the eq type constructor,
type (_,_) eq =
| Eq: ('a,'a) eq
is in many way the quintessential GADT, which can be used to encode other GADTs.
For instance, the above numty is equivalent to
type 'a numty' =
| Int' of ('a,int) eq
| Float' of ('a,float) eq
To check that the two types are equivalent, we can write a zero function for both types:
let zero: type n. n numty -> n = function
| Int -> 0
| Float -> 0.
let zero': type n. n numty' -> n = function
| Int' Eq -> 0
| Float' Eq -> 0.