Re: polymorphic variants and promotion

[Remi Vanicat <vanicat@debian.org>]

"Johannes Kanig" <johannes.kanig@lri.fr> writes:

> 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

Well, you have to explicitly coerce :

let h a = function                                              
      | [] -> g a                                                 
      | xs -> (List.fold_left f a xs : [ `A of _ ] :> [> `A of _ | `B of _ ]) ;;

What I don't understand is why this :

let h a = function                                              
      | [] -> g a                                                 
      | xs -> (List.fold_left f a xs :> [> `A of _ | `B of _ ]) ;;

do not work ? I understood that we need to explicitly coerce, but the 
[ `A of _ ] is just the information the compiler will find by itself,
why must we give it to it again ?

-- 
Rémi Vanicat