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

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

I have now committed in trunk a fix to PR#5985.
You can use it to test whether your codebase runs into problems.
You can either obtain it from subversion directly
	svn checkout http://caml.inria.fr/svn/ocaml/trunk
or use opam to do it for you.

I checked that at least Core itself compiles without problems.

Again, if you run into problems, you can try branches/non-vanishing,
which allows you to annotate some abstract types are injective.

Jacques Garrigue

On 2013/04/29, at 19:52, Jacques Garrigue <garrigue@math.nagoya-u.ac.jp> wrote:

> Dear Camlers,
> 
> First, let me reiterate my request for feedback:
> 
> What I want to know is whether anybody is using GADTs in a way that
> would be broken if we disallow type variables under abstract types
> (other  than the predefined ones) in the return type of GADTs.
> I.e., for instance defining a type witness type involving such abstract types.
> 
> This is really the question I want you all to answer.
> 
> If this is not the case, we can safely prohibit that at this point, and take
> our time to think about the solution.