From: Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr>
> > The above behaviour was correctly explained by Martin Jambon, but I'll
> > add some detail:
> > The type of f is actually an instance of the type of g, where the
> > first and second columns of the pattern were unified. The reason for
> > that is that in f the 1st line returns the 2nd column, and the 2nd
> > line the first column. Since the return type has to be unique, this
> > unifies x and y, i.e. the 1st and 2nd columns.
> >
> > I hope this clarifies the situation.
> >
> > Jacques Garrigue
> >   
> OK, I understand. But I would prefer if the decision to close or not the
> pattern (and therefore
> make the last case useless) did not depend upon the right members ...

So actually you didn't understand :-)
The point here is that the typing for the pattern matching is
determined completely independently of the right members. This is only
afterwards that some extra unifications may happen, as is always the
case with type inference. This is not a "decision", but a natural
consequence of the type system.
The warning about the useless case is actually a clever trick: rather
than immediately checking for useless cases after checking the pattern
matching, it waits for the whole expression to be typed, in order to
be more accurate.

In some way what you are saying is a bit like:

# let f (x : [> `A]) (y : [> `B]) = ignore [x;y] ;;
val f : ([> `A | `B ] as 'a) -> 'a -> unit = <fun>

Why are the types for x and y unified, I'd much prefere them to be
independent...

By the way, as Martin Jambon explained, you can protect you variables
against type propagation with the "as" syntax.

# let f (`A as x) (`B as y) = [x;y];;
val f : [< `A ] -> [< `B ] -> [> `A | `B ] list = <fun>


Jacques Garrigue