polymorphic variants and recursive functions

[Warren Harris <warrensomebody@gmail.com>]

I stumbled upon a little puzzle that I can't quite work out. I'm  
trying to use polymorphic variants as phantom types and in one  
particular situation involving a polymorphic type with an invariant  
type parameter (Lwt.t) the compiler is unhappy with a set of mutually  
recursive functions. I can appreciate at some level that an invariant  
type parameter will cause the phantom types to become unsatisfied, but  
in this particular case my sense is that they should be satisfiable,  
and feel that I might be overlooking an appropriate coercion. Perhaps  
someone here can lend a hand...


Here's the best I can do at creating a simple example: First, here's  
the case the works... I would like a family of constructors, including  
two higher-order ones, 'arr' and 'obj', such that 'arr' can only be  
constructed from 'obj' instances:

let obj (v:[> `V]) : [`O|`V] = `V
let arr (v:[> `O]) : [`V]    = `V
let v0 : [`V]                = `V

This works as expected:

let ok1 = obj v0
let ok2 = arr (obj v0)
let ok3 = obj (arr (obj v0))

and fails as expected:

let fail1 = arr v0
                   ^^
This expression has type [ `V ] but is here used with type [> `O ]
The first variant type does not allow tag(s) `O

I can now use these constructors in conjunction with some mutually- 
recursive functions (coercions are needed):

let rec eval = function
   | `Arr v -> (eval_arr v : [`V]    :> [> `V])
   | `Obj v -> (eval_obj v : [`V|`O] :> [> `V])
and eval_arr v = arr (eval_obj v)
and eval_obj v = obj (eval v)

although oddly, the coercions don't seem to affect the final type of  
eval:

val eval : ([< `Arr of 'a | `Obj of 'a ] as 'a) -> [ `O | `V ] = <fun>
val eval_arr : ([< `Arr of 'a | `Obj of 'a ] as 'a) -> [ `V ] = <fun>
val eval_obj : ([< `Arr of 'a | `Obj of 'a ] as 'a) -> [ `O | `V ] =  
<fun>



Now the case that doesn't work: Introducing 'a Lwt.t into the above:

open Lwt
let obj (v:[> `V]) : [`O|`V] Lwt.t = return `V
let arr (v:[> `O]) : [`V] Lwt.t    = return `V
let v0 : [`V] Lwt.t                = return `V

let ok1 = v0 >>= obj
let ok2 = v0 >>= obj >>= arr
let ok3 = v0 >>= obj >>= arr >>= obj
(*let fail1 = v0 >>= arr*)

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



Any suggestions would be much appreciated,

Warren