Dear all,
I don’t understand why the following type definition is not accepted:
type +_ u = U : 'a -> 'a list u
Error: In this GADT definition, the variance of some parameter
cannot be checked
Could someone explain what’s going wrong here? Thanks!
To me it seems that 'a is contravariant but 'a list is covariant, which looks like conflicting variance requirements. And just to confirm, if we remove the variance annotation, the error goes away.
I don’t think that 'a appears in contravariant position here, because of two vague arguments:
type +'a t = U of 'a
(not sure though this analogy is worth something)
type +_ t = U : ('a -> int) -> 'a t
Error: In this definition, expected parameter variances are not satisfied.
The 1st type parameter was expected to be covariant,
but it is injective contravariant.
And also:
type +_ t = U : 'a -> 'a t
works…
I think this is a limitation of the type checker. I agree that the type parameter is covariant because 'a list has the same variance as 'a and 'a is in a covariant position in U.
The variance of type parameters for GADTs is a far more complex question than for ordinary variants. In particular, the usual criteria that a type parameter which only appears in covariant positions is covariant is inapplicable.
Indeed, consider for instance,
type (_,_) eq = Eq: ('a,'a) eq
The two type parameters of eq only appear in covariant or contravariant positions (because they don’t appear at all). However, (< >, <x:int>) eq is not a subtype of (< x:int>, <x:int>) eq. In other words, eq must be invariant in its two type parameters.
Right now, to avoid this complexity the typechecker consider that for GADTs only type parameters that are never constrained (in other words maps exactly to ordinary variants) might be covariant or contravariant. For instance:
type (+'a,_) pair= P:'a * 'a -> ('a,int) pair;;
All other type parameters are considered invariant. Since your example is constraining the type parameter to _ list it falls in this category.
Cristal clear, thanks!