I'm not sure I see the point of this long discussion between Lukasz and Jacques.
It seems everybody agree that it is a good idea to explicitely quantify the constructor-specific type variables.
The question Jacques raised is wether, when we write (| Foo of 'a . S : T) or (| Foo : 'a . S -> T), the 'a is quantified on S only, or on both S and T.
It think we all agree that, for semantical reasons, quantification should be scoped over both S and T. However, the (of S : T) syntax does not make it very obvious, and this should be rightfully considered as a defect of this syntax.
I'm under the impression that your intense debate is about the edge case where :
1. we don't use explicit quantification of constructor-specific variables
2. we reuse the type parameter variables in the type of a GADT constructor (so they're implicitly shadowed by the implicit quantifications, or maybe not)
If we reject possibly 1. (and ask for explicit quantification), all is well. If you want to consider option 1., then I think the edge case 2. is evil and shoud result in a warning.
On Sun, Dec 5, 2010 at 9:25 AM, Lukasz Stafiniak
<lukstafi@gmail.com> wrote:
On Sun, Dec 5, 2010 at 9:10 AM, Lukasz Stafiniak <
lukstafi@gmail.com> wrote:
>
> shouldn't mean that Embed is "basically" Embed of int : int term. My
> position is that if a type variable should be treated as local to a
> branch, it should be explicitly quantified (using the dot notation,
> for example "Ignore of 'a. 'a : int term", without any exceptions to
> "existential" variables). And that the patterns
>
> type X =
> | Branch of Y
>
> and
>
> type X =
> | Branch of Y : X
>
> should be equivalent (where X could for example be 'a term).
> type X =
> | Branch of 'a. Y : X
will be different (unless 'a is not used in Y nor X).