[Caml-list] explaining polymorphic variants

[Yaron Minsky <yminsky@janestreet.com>]

A question that came up in the section of Real World OCaml on
polymorphic variants.

I'm wondering if someone can explain the error in the third definition
below.

    # let handle_a `A = "a";;
    val handle_a : [< `A ] -> string = <fun>
    # let handle_ab (x: [`A | `B ])  =
        match x with
        |`B -> "b"
        | `A as a -> handle_a a
      ;;
    val handle_ab : [ `A | `B ] -> string = <fun>
    # let handle_ab' (x: [`A | `B ])  =
        match x with
        | `B -> "b"
        | a -> handle_a a
      ;;
    Characters 86-87:
        | a -> handle_a a
                        ^
    Error: This expression has type [ `A | `B ]
           but an expression was expected of type [< `A ]
           The second variant type does not allow tag(s) `B

I understand roughly what's going on here.  In the definition of
handle_ab, there is a straightforward syntactic basis for narrowing
the type of the variable a.  In the case of handle_ab', that syntactic
basis is no longer available, and so the type of a is not narrowed.

But the question is: why isn't it narrowed based on the other
information available?  It seems in theory possible to infer the
narrower type in this case.  Does anyone have a satisfying explanation
as to why?

y