Oddness with recursive polymorphic variants

Oddness with recursive polymorphic variants

[Jeremy Yallop]

I have two polymorphic variant types, as follows:

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

Next, I have a function from f to g:

   let s1 : f -> g = function
     | `A -> `A
     | `B b -> b

Sadly, the compiler rejects this:

     Characters 57-58:
       | `B b -> b;;
                 ^
   This expression has type f but is here used with type g
   The first variant type does not allow tag(s) `C

The error message seems odd.  Why should it matter that g has more tags 
than f, since every value of f is a value of g (by definition)?

Indeed, minor variants of the function are accepted.  Both of the 
following are ok:

   let s2 : f -> g = function
     | `A -> `A
     | `B (#f as b) -> b

   let s3 : f -> g = function
     | `A -> `A
     | `B ((`A|`B _) as b) -> b

Am I missing something, or is this a bug?

Thanks,

Jeremy.

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

[Nils Gesbert]

Jeremy Yallop <j.d.yallop@sms.ed.ac.uk> a écrit :

» I have two polymorphic variant types, as follows:
» 
»    type f = [`A | `B of f]
»    type g = [f | `C]
» 
» Next, I have a function from f to g:
» 
»    let s1 : f -> g = function
»      | `A -> `A
»      | `B b -> b
» 
» Sadly, the compiler rejects this:
» 
»      Characters 57-58:
»        | `B b -> b;;
»                  ^
»    This expression has type f but is here used with type g
»    The first variant type does not allow tag(s) `C
» 
» The error message seems odd.  Why should it matter that g has more tags 
» than f, since every value of f is a value of g (by definition)?

f is indeed a subtype of g, but to forget the precise type of b (that is, forget the information that it cannot contain the tag `C), you have to use explicit coercion, i. e. :

  let s1 : f -> g = function
     | `A -> `A
     | `B b -> (b :> g)

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

[Nils Gesbert]

Alternatively, you may also coerce directly the function :
let s1 = ((function `A -> `A | `B b -> b) :> f -> g)

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

[Jeremy Yallop]

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.

Oddness with recursive polymorphic variants

[Jeremy Yallop]

I have two polymorphic variant types, as follows:

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

Next, I have a function from f to g:

   let s1 : f -> g = function
     | `A -> `A
     | `B b -> b

Sadly, the compiler rejects this:

     Characters 57-58:
       | `B b -> b;;
                 ^
   This expression has type f but is here used with type g
   The first variant type does not allow tag(s) `C

The error message seems odd.  Why should it matter that g has more tags 
than f, since every value of f is a value of g (by definition)?

Indeed, minor variants of the function are accepted.  Both of the 
following are ok:

   let s2 : f -> g = function
     | `A -> `A
     | `B (#f as b) -> b

   let s3 : f -> g = function
     | `A -> `A
     | `B ((`A|`B _) as b) -> b

Am I missing something, or is this a bug?

Thanks,

Jeremy.