Hi,

> If the risk of confusion with constructors-as-functions is deemed
> problematic, a syntax like
>    App of ('a -> 'b) t * 'a t : 'b t
> seems OK too.
> Actually this would have the advantage of allowing the scope of
> existential variables to be explicit. I.e. one could write
>   App of 'a. ('a -> 'b) t * 'a t : 'b t

I find this new syntax preferable too.  As I just mentioned in my reply to
Stefan Monnier, my main criticism to the currently implemented GADT syntax
is that type constructors are declared in a curried way, despite the fact
that they cannot actually be partially applied.  This breaks an assumption
that is otherwise consistent throughout the language, and I think we can
all agree that adding caveats and exceptions to a language specification
is something that should be avoided as much as possible (and is often the
symptom of a bad specification).

Best regards,
Dario Teixeira