> For instance, [<  `A of int] and [< `A of bool] are unifiable, giving [< `A of int & bool],

OK ... this means you can write (I tested in 3.11.2) :

# type ('a,'b,'c) inter = [< `A of 'b & 'c] as 'a;;
type ('a, 'b, 'c) inter = 'a constraint 'a = [< `A of 'b & 'c ]

which seems to be a type isomorphic to the intersection type of 'b and 'c ...

does this mean we can play with intersection type in OCaml (using some type cast because
intersection type is undecidable ...)

In other word : can we encode system D in OCaml ?

Cheers,
Christophe


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