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

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

On 2013/04/30, at 17:02, Alain Frisch <alain@frisch.fr> wrote:

> On 04/30/2013 09:56 AM, Jacques Garrigue wrote:
>> On 2013/04/30, at 15:59, Alain Frisch <alain@frisch.fr> wrote:
>> 
>>> It's reassuring to see that the conservative solution (not assuming injectivity of user defined abstract types) does not seem too bad for now, even if not very satisfying.
>>> 
>>> I'm only concerned with:
>>> 
>>>> 3) The problem I describe in my first mail. I.e. when defining a type,
>>>>   if you use type variables appearing in constrained type parameters,
>>>>   you need the type constructors leading to the type variables to be
>>>>   injective. This is PR#5985, and it is only fixed in branches/non-vanishing.
>>> 
>>> Do you think that fixing this unsoundness (without injectivity annotations) would lead to reject existing programs?
>> 
>> Potentially yes.
>> But I don't know how it is in practice for code existing now.
>> Hence my question.
> 
> Apart from GADTs, does your patch address the unsoundness with type constraints?

Sure, this is exactly the same mechanism.

The only other thing it does is a slight strengthening of variance checking.

Consider the type
   type 'a t = T                   (* 'a bi-variant and injective *)
   type 'a u = 'a t -> 'a t    (* 'a t occurs both at positive and negative positions *)

Originally, the parameter of u would have been bi-variant (or unrestricted)
since it is bi-variant in the definition of t.
However it is now invariant.
The reason is that you can only change it by subtyping in t, and u doesn't allow subtyping.
This is a reasonable restriction, and it is necessary to allow some GADT
definitions where we use concrete types as indices.

Jacques Garrigue