Re: [Caml-list] Oddness with recursive polymorphic variants

[Jeremy Yallop <j.d.yallop@sms.ed.ac.uk>]

Thanks for all the replies.  My current understanding is as follows:

Given the types

    type f = [`A]
    type g = [f | `C]

then the following function is not acceptable

    let k (x:f) = (x:g)

because f and g are not unifiable: they are "closed rows" with different 
fields.  There are a number of ways to "open" the row, however:

    let k (#f as x:f) = (x:g)

This one is acceptable because the pattern "#f" means "an open row that 
includes all the tags in f".  (That's its type on the rhs, anyway.  The 
pattern (and the function) will accept exactly those tags in the type 
"f").  The type annotation on the parameter doesn't affect the type of 
"x", although the compiler does check that the type of the annotation 
and of the pattern can be unified.  The case where all the tags (only 
one in this case) are enumerated is treated identically:

    let k (`A as x:f) = (x:g)

Finally, the explicit coercion (:>).  Like the acceptable patterns, this 
"opens" the row, allowing it to be unified with "g" (or, indeed, with 
any other row type whose tag parameters don't clash with those of "f").

How does that sound?

Jeremy.