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 ?

Regards,
-- 
Christophe Raffalli
Universite de Savoie
Batiment Le Chablais, bureau 21
73376 Le Bourget-du-Lac Cedex

tel: (33) 4 79 75 81 03
fax: (33) 4 79 75 87 42
mail: Christophe.Raffalli@univ-savoie.fr
www: http://www.lama.univ-savoie.fr/~RAFFALLI
---------------------------------------------
IMPORTANT: this mail is signed using PGP/MIME
At least Enigmail/Mozilla, mutt or evolution 
can check this signature. The public key is
stored on www.keyserver.net
---------------------------------------------