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 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.

I have now committed the fix in trunk, so people can try it.

A reason the impact is going to be limited, is that usually when defining
a GADT for type witnesses, one only lists predefined types, and uses
another mechanism for user defined types, like what is done in Core.
If you use a mechanism based on equality witnesses, (lack of) injectivity
already came in the way before, so this is not a new phenomenon.

For other applications of GADTs, you are defining type indices yourself,
so you just have to be careful to use concrete types instead of abstract types.

Jacques Garrigue