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).

To clarify again: modulo variable capture! That is, the pattern

> type X =
>  | Branch of 'a. Y : X

will be different (unless 'a is not used in Y nor X).