[Caml-list] Variance of GADT parameters

[Gabriel Scherer <gabriel.scherer@gmail.com>]

I've been playing with GADTs and noticed that the condition on
parameter variance is very restrictive.

The two following examples fail:

  type +_ const =
  | Const : int -> int expr

  type +_ expr =
  | Const : 'a -> 'a expr
  | Prod : 'a expr * 'b expr -> ('a * 'b) expr

  Error: In this GADT definition, the variance of some parameter
  cannot be checked

I looked at the source, and this is what I could infer of the current
typer behavior: parameter variance check will fail (on non-invariant
parameters) as soon as they appear *instantiated* (not just
a variable) in one of the GADT branch return type. The two examples
above fail for this reason: `const` parameter is instantiated with int
and `expr` with ('a * 'b).

Would it be possible to relax this condition a bit? Intuitively, I
would say that:
1. variables that do not appear in the instantiations of the return
   type always satisfy their variance constraint (for the branch)
2. variables that appear covariantly in the instantiations of the
   return type should satisfy their constraints on the argument types
3. variables that appaear contravariantly should satisfy the
   *reversed* constraints on the argument type

For example, with a GADT having some argument type σ('a) using
a variable instantiated in its return type :

  type +_ t = | C : σ('a) -> ('a -> unit) t

If α ≤ β, then α t ≤ β t only if α, β are of the form α' → unit, β' →
unit, so α' *≥* β' and α t ≤ β t only if σ(α') ≤ σ(β'), that is 'a
appears *contravariantly* in σ.

Is the above condition sound? It would allow my two examples above. If
not, or if it's not reasonable to implement, is there a weaker
condition that would make those example work?

Having a powerful enough variance inference is important if we want to
use GADTs to implement abstract data types – that's how I ran into
this problem.