Typechecking of recursive variants

[Judicael Courant <Judicael.Courant@lri.fr>]

Hello,

I do not understand the following behavior of the typechecker :
match x 4 with `X z -> z | `Y -> assert false;;
- : [ `Y | `X of '_a] as 'a = `X (`X (`X `Y))

        Objective Caml version 3.00

# let rec x n = if n = 0 then `Y else `X (x (n-1));;
val x : int -> ([> `Y | `X of 'a] as 'a) = <fun>
# x 3;;
- : _[> `Y | `X of '_a] as 'a = `X (`X (`X `Y))
# match x 4 with `X z -> z | `Y -> assert false;;
- : [ `Y | `X of '_a] as 'a = `X (`X (`X `Y))


What do these underscores mean ? Anything to do with monomorphic type
variables ? Why is not there any ">" at the beginning of the latest
type ?

Judicaël.
-- 
Judicael.Courant@lri.fr, http://www.lri.fr/~jcourant/
(+33) (0)1 69 15 64 85
"Montre moi des morceaux de ton monde, et je te montrerai le mien"
Tim, matricule #929, condamné à mort.
http://rozenn.picard.free.fr/tim.html