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