GADT constructor syntax

[Jacques Le Normand <rathereasy@gmail.com>]

Dear caml-list,
I would like to start a constructive discussion on the syntax of GADT
constructors of the ocaml gadt branch, which can be found at:

https://sites.google.com/site/ocamlgadt/

There are two separate issues:

1) general constructor form

option a)

type _ t =
        TrueLit : bool t
      | IntLit of int : int lit

option b)

type _ t =
      TrueLit : bool t
    | IntLit : int -> int lit

I'm open to other options. The branch has used option b) from the
start, but I've just switched to option a) to see what it's like

Personal opinion:

I slightly prefer option b), because it makes it clear that it's a
gadt constructor right from the start. This is useful because the type
variables in gadt constructors are independent of the type parameters
of the type, consider:

type 'a t = Foo of 'a : 'b t

this, counter intuitively, creates a constructor Foo of type forall 'd
'e. 'd t -> 'e t.

2) explicit quantification of existential variables

option a)

leave existential variables implicitly quantified. For example:

type _ u = Bar of 'a t : u
or
type _ u = Bar :  'a t -> u

option b)

specifically quantify existential variables. For example:

type _ u = Bar of 'a. 'a t : u
or
type _ u = Bar : 'a. 'a t -> u

Currently, the branch uses option a).

Personal opinion: I prefer option b). This is for four reasons:

I) the scope of the explicitly quantified variable is not clear. For
example, how do you interpret:

type _ u = Bar of 'a. 'a : 'a t
or
type _ u = Bar : 'a. 'a -> 'a t

In one interpretation bar has type forall 'a 'b. 'a -> 'b t and in
another interpretation it has type forall 'a. 'a -> 'a t. My
inclination would be to flag it as an error.

II)

In the example of option b), the 'a variable is quantified as a
universal variable but, in patterns, it is used as an existential
variable. This is something I found very confusing in Haskell where
they actually use the 'forall' keyword.

III) option a) is the current Haskell GADT syntax and I've never heard
anyone complain about it

IIII) I don't see how option b) improves either readability or bug prevention

I look forward to hearing your opinions.

--Jacques Le Normand