polymorphic variant

[Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr>]

[-- Attachment #1.1: Type: text/plain, Size: 1312 bytes --]

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
---------------------------------------------


[-- Attachment #1.2: Christophe.Raffalli.vcf --]
[-- Type: text/x-vcard, Size: 310 bytes --]

begin:vcard
fn:Christophe Raffalli
n:Raffalli;Christophe
org:LAMA (UMR 5127)
email;internet:christophe.raffalli@univ-savoie.fr
title;quoted-printable:Ma=C3=AEtre de conf=C3=A9rences
tel;work:+33 4 79 75 81 03
note:http://www.lama.univ-savoie.fr/~raffalli
x-mozilla-html:TRUE
version:2.1
end:vcard


[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 249 bytes --]