Re: [Caml-list] polymorphic variant

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

From: Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr>
> Can someone explain to me why the two following functions are typed so
> differently:
> 
> ---------------
>         Objective Caml version 3.10.0
> 
> # let f = function
>       `T, y -> y
>     | x, `T -> x
>     | `F, `F -> `F
>     | `F, _ -> `F
> ;;
> Warning U: this match case is unused.
> val f : [ `F | `T ] * [ `F | `T ] -> [ `F | `T ] = <fun>
> 
> # let g = function
>     `T, y -> y
>   | x, `T -> `F
>   | `F, `F -> `F
>   | `F, _ -> `F
> ;;
> val g : [< `F | `T ] * ([> `F | `T ] as 'a) -> 'a = <fun>
> 
> -------
> 
> The decision to close the second column seems to depend upon the
> right hand side of the pattern, which seems excluded by Jacques
> Garrigue's paper about deep pattern matching ... According to this
> paper, the second function is strangely typed. What is implemented
> in OCaml ?

It is implemented, and correctly I believe.
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