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

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

On 2013/07/04, at 1:08, Alain Frisch <alain@frisch.fr> wrote:

> Btw, this is also an example where type-based disambiguation in presence of a GADT would be useful.  For instance, we currently need to write:
> 
>    match StringMap_matcher.check t with
>    | Some (StringMap_matcher.Is (s, TypEq.Eq)) -> vmap (StringMap.map (of_value ~t:s env) x)
>    | None -> ...
> 
> while one could write:
> 
>    match StringMap_matcher.check t with
>    | Some (Is (s, Eq)) -> vmap (StringMap.map (of_value ~t:s env) x)
>    | None -> ...
> 
> (see http://caml.inria.fr/mantis/view.php?id=6023 )

In theory, it would be OK to assume that all pattern-matchings may contain GADT type constructors.
The only real problem is with let's: if they contain GADTs, we must use the code for pattern-matching, which doesn't handle unused definition warnings in the same way… Having all non recursive let's go through this code would have a high impact on warnings.

If unused definition warnings could be separated from type checking this would be much easier.

> In some cases (in particular to add annotations to make sense of error messages), it would be useful to be able to name the type constructor introduced by opening the GADT to match the existential type.  (I'd put this rather high on my wish list around GADTs!)

I did to.
As Gabriel mentioned, there was a discussion about syntax on Mantis.

 http://caml.inria.fr/mantis/view.php?id=5780

As is often the case with syntax, this ended with no agreement, so there is no such feature…

Actually, the problem with syntax is a bit deeper than that.
Namely, my real concern is that currently locally abstract types cannot handle abstract row types.
I think this is a severe limitation, at least for some applications.
Maybe this problem should be solved first, as adding new syntax for existential types without solving this will only make it deeper.

	Jacques