On Wed, Mar 25, 2009 at 02:39:28PM -0700, Warren Harris wrote:
> let rec eval = function
>   | `Arr v -> (eval_arr v : [`V] Lwt.t    :> [> `V] Lwt.t)
>   | `Obj v -> (eval_obj v : [`V|`O] Lwt.t :> [> `V] Lwt.t)
> and eval_arr v = eval_obj v >>= arr
> and eval_obj v = eval v >>= obj
>
>     | `Obj v -> (eval_obj v : [`V|`O] Lwt.t :> [> `V] Lwt.t)
>                  ^^^^^^^^^^
> This expression has type [ `O | `V ] Lwt.t but is here used with type
>   [ `V ] Lwt.t
> The second variant type does not allow tag(s) `O

The Lwt.t type is abstract and invariant since no annotation has been given
for the type variable (you'd need it to be  type +'a t):

# let a : [`O] Lwt.t = return `O;;
val a : [ `O ] Lwt.t = <abstr>
# (a :> [`O | `V] Lwt.t);;
Error: Type [ `O ] Lwt.t is not a subtype of type [ `O | `V ] Lwt.t 
The first variant type does not allow tag(s) `V

In your example, [> `V] Lwt.t  in the second line becomes 
   [`V] Lwt.t,
(the type variable is not covariant) and you cannot do  
   [`V | `O] Lwt.t :> [`V] Lwt.t
in the third line.

Unfortunately, the type variable is in both variant and contravariant position
in the definition of Lwt.t...

-- 
Mauricio Fernandez  -   http://eigenclass.org