polymorphic variants and promotion

["Johannes Kanig" <johannes.kanig@lri.fr>]

[-- Attachment #1: Type: text/plain, Size: 1547 bytes --]

Hi,

I ran into the following problem using polymorphic variants. Suppose I have
2 functions f and g (the function definitions don't make much sense - they
are just there for typing purposes) :

# let f (`A a) (`A i) = `A i ;;
val f : [< `A of 'a ] -> [< `A of 'b ] -> [> `A of 'b ] = <fun>
# let g (`A a) = (`B a) ;;
val g : [< `A of 'a ] -> [> `B of 'a ] = <fun>

For simplicity I assume that the type variables all instantiate to "int".
Now, I want to construct a function h that takes an accumulator a and a list
of `A's (for example [`A 1; `A 2; ...]) that produces either an object of
type `A of int or an object of type `B of int in the following way:

# let h a = function
    | [] -> g a
    | xs -> List.fold_left f a xs;;

But this doesn't type:

This expression has type [ `A of 'a ] but is here used with type
  [> `B of 'a ]
The first variant type does not allow tag(s) `B

I understand that the fold_left fixes the type of f the result of f to [`A
of int] instead of [>`A of int]. The example as above can be easily repaired
by replacing the second branch of the pattern matching by:

let `A _ as x = List.fold_left f a xs in x

which is fair enough (thanks to Romain Bardou for pointing this out).

What I don't understand is why the promotion of [`A of int] to [> `A of int]
is not possible in general:

# `A 1;;
- : [> `A of int ] = `A 1
# (`A 1 : [`A of int]) ;;
- : [ `A of int ] = `A 1
# ((`A 1 : [`A of int]) : [> `A of int]) ;;
- : [ `A of int ] = `A 1

Does anyone have an answer?

-- 
Johannes Kanig
johannes.kanig@lri.fr

[-- Attachment #2: Type: text/html, Size: 1874 bytes --]