> But this similar type has no problem: > type 'a field = Int of int > let a = Int 3 > let b = Int (1 + 2) This is the relaxed value restriction: `field` is covariant in it's parameter which means that the type variable is only used in covariant positions and so can be generalized even though the expression is not a value. > Both a and b receive the same generalized type. Why does the GADT > style prevent this from occuring? OCaml currently just assumes that types defined with GADT syntax are invariant because checking of variance with GADTs is more difficult. If you annotate your type as covariant then it behaves the same: type +_ field = Int : int -> 'a field let a = Int 3 let b = Int (1 + 2) gives: type +_ field = Int : int -> 'a field val a : 'a field = Int 3 val b : 'a field = Int 3 Regards, Leo