Re: [Caml-list] Request for feedback: A problem with injectivity and GADTs

[Leo White <lpw25@cam.ac.uk>]

>>>       type 'a t = T;;
>>>       type _ g = G : 'a -> 'a t g;;
>>
>> I don't see why this could not be allowed without the restriction you
>> propose. I thought that this was rejected in 4.00 because 4.00 used
>> bi-variance as an (unsafe) approximation of non-injective. Since we now
>> track injectivity separately from variance g be accepted (with 'a covariant).
>
> In our work, this GADT definition would be accepted, and:
> (1) matching on the constructor G does not give any information on the
> value of the existential type 'a
> (2) the parameter of g (not 'a, the one marked _ above) may marked
> covariant or invariant, because the constructor t is upward-closed but
> not downward-closed (private types)

I don't think the argument to G needs to be given an existential type,
as long as the parameter of g is marked invariant.

The parameter to g should be marked invariant for two reasons:
1) It is constrained in the result type of a GADT constructor which, as
discussed on this list previously, forces it to be invariant (at least
for now, see Gabriel's paper for further details).
2) Marking it as anything other than invariant, would entail marking
'a as bi-variant, when it is in fact covariant.

This second reason also occurs in types with constraints, for example:

  type 'a s = 'b constraint 'a = 'b t

here 'b is covariant (used in covariant and bi-variant positions), but
marking 'a as any variance other than invariant would entail marking 'b
as bi-variant.