Say I want to create a GADT
t for terms, the latter being of 3 different sorts (say
f). Now is there a way to state than one constructor may only accept
es? I know how to do this with two different constructors (see
Ite_e below) but I wondered if there is another good practice to handle this kind of situations (from what I gathered, using polymorphic variants for
eand then playing with subtyping is discouraged when using GADTs).
type e (* expressions *) type f (* formulas *) type a (* arithmetic terms *) type 'a t = Num : int -> a t | Sort : string -> e t | True : f t | False : f t | All : string * e t * f t -> f t | Ite_f : f t * f t * f t -> f t (* can I get a *single* Ite constructor *) | Ite_e : f t * e t * e t -> e t