Introduce local type variables in patterns

[garrigue]

This is a first step towards having local type variables, whose level is chosen from their introduction point.
This is a very simple (but partial) solution to the existential naming problem (#7074).
Due to conflicts, the syntax is <'a 'b> pattern.

Here is a simple example using GADTs:

type _ ty = Int : int ty
type dyn = Dyn : 'a ty * 'a -> dyn
let f = function <'a> Dyn (w,(x:'a)) -> 3

[gasche]

I think it would be nice to reach a form of consensus (among the people who expressed interest in the topic before: @lpw25, @yallop, @alainfrisch, you and myself; for example) before implementing things -- or maybe to clearly mark implementations as prototypes for experiment.

Since this discussion was resurrected last week, @yallop, @lpw25 and myself have expressed support the form Constructor (type <var> <var>) <pattern with annotations>. (A form of compromise / consensus-building comes from dropping the idea of positional type variables.) You proposed instead a slightly different proposal, (type <var> <var>) Constructor<pattern with annotations>, but now the PR implements something fairly different.

Personally I am not very enthusiastic about the introduction of yet another pair of delimiters. I already find ['a, 'b] in classes fairly ugly when I have to use it, and this is much closer to the rest of the language (objects are already bathing in foreign syntax, GADTs programs use rather classic pattern-matching). If we can have (type a b) (before or after the constructor; personally I would have a preference for after) without weird delimiters, maybe this is a reason to favor type names instead of type variables? (In addition to the rather convincing points of @craigfe in #7074 (comment) .)

[garrigue]

As I said, this is experimental, and the delimiters < and > are not here to stay, I was just looking for a quick way to make menhir happy.
To be more precise, this quick PR is the result of trying to start implementing 2(3), and realising this was going to be really hard. So I started by something much simpler to see how it would work.

Independently of that, the problem of the scoping of unification type variables is a long standing one too. Solving it in a way that makes such examples work would certainly be nice.

[lpw25]

I'm closing this since the alternative #9584 has been merged.

[garrigue]

Actually, #9584 does not subsume this.
#9584 allows to name the existential variables introduced by a constructor (using a very restrictive syntax), but it does not allow to bind a type containing them to a named type variable, due to scoping reasons.
The goal of this PR is precisely to overcome those scoping problems.