[Caml-list] Typing of recursive function with polymorphic variants

[Vincent Jacques <vincent@vincent-jacques.net>]

Hello,

utop # let rec f1 = function
  | `A x -> f1 x
  | `B -> `B;;
val f1 : ([< `A of 'a | `B ] as 'a) -> [> `B ] = <fun>

utop # let rec f2 = function
  | `A x -> f2 (f2 x)
  | `B -> `B;;
val f2 : ([< `A of 'a | `B > `B ] as 'a) -> 'a = <fun>

but I can *see* that f2 never returns an `A so I would give it the
same type as f1.

1) Would I be right or am I missing something?

2) Assuming I'm right, can you please give me hints about this
limitation of the typing algorithm?
I have a basic understanding of the W typing algorithm. Assuming that
a similar algorithm is used for polymorphic variants, I imagine that
when I call f2 (f2 x), f2's return type is "unified" with f2's
parameter type. Why is this needed?

3) The type of f2 is more generic than the type of f1. Could I use
type annotations to help the typing algorithm choose a more specific
type?

I tried to annotate f3 (f3 x) but I get different behaviors in utop
and in the compiler. I'm lost :)

utop # let rec f3 = function
  | `A x -> ((f3 (f3 x)):[`B])
  | `B -> `B;;
Error: This pattern matches values of type [? `A of [ `B ] ]
    but a pattern was expected which matches values of type [ `B ]
    The second variant type does not allow tag(s) `A

In a .ml file:

let rec f3 = function
  | `A x -> ((f3 (f3 x)):[`B])
  | `B -> `B

let () = f3

Error: This expression has type [ `B ] -> [ `B ]
    but an expression was expected of type unit

Thank you for your help,
-- 
Vincent Jacques
http://vincent-jacques.net

"S'il n'y a pas de solution, c'est qu'il n'y a pas de problème"
            Devise Shadock