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

[Alain Frisch <alain@frisch.fr>]

On 04/29/2013 12:52 PM, Jacques Garrigue wrote:
> Again, the defect of such a mode is that it is going to apply to everything, including functors.
> A functor compiled in this mode might be not be applicable to some modules, whereas there was
> no reason from the beginning to require injectivity there.
>
> And just using variance to change the behavior is not going to work well:
> a standard practice is to explicitly define module types for the input and output of
> the functor. We want the output types to be injective, but we don't really need such
> requirement for the input types. But they are just module type definitions…
> (See hashtbl.mli for instance for this pattern.)

These are interesting arguments against the "injective by default" mode 
(explicit non-injectivity annotations).  I did not think about the 
consequences on functors indeed.  In practice, though, it might be ok to 
annotate, if needed, some module types used as functor arguments with 
non-injectivity annotations (or more precisely "not-necessarily 
injective" annotations).  But this certainly deserves some careful thinking.

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?


-- Alain