> What about:
>
>     # type void = { v: 'a. 'a };;
>     type void = { v : 'a. 'a; }
>     # let rec vv = { v = vv };;
>     This field value has type 'a which is less general than 'b. 'b
>   
Now that's a very nice solution. You give the impredicative coding of 
the void type (forall 'a. 'a) by boxing it into record type.

You get void_elim withouth cheating :
  let void_elim x = x.v

It is the good solution if you work with the original syntax (and it's 
absolutely equivalent to the dual definition in term of empty variant 
which you can write in the revised syntax).

Well spotted.


Arnaud Spiwack