Hello.

I've been struggling to have a type system where I could do the 
following subtyping:

'a t1 :> t2  and  t2 :> 'a t1

So I've tried to do the following:

> yziquel@seldon:~$ ocaml
>         Objective Caml version 3.11.2
> 
> # #rectypes;;
> # module Q = struct
>     type -'a e
>     type 'a q = private w
>     and w = w e
>     and 'a r = 'a q e
>   end;;
> module Q :
>   sig type -'a e type 'a q = private w and w = w e and 'a r = 'a q e end

It almost seems to work:

> # let f x = (x : Q.w Q.e :> 'a Q.q Q.e);;
> val f : Q.w Q.e -> 'a Q.q Q.e = <fun>
> # let f' x = (x : Q.w :> 'a Q.r);;
> val f' : Q.w -> 'a Q.r = <fun>
> # let g x = (x : 'a Q.q :> Q.w);;
> val g : 'a Q.q -> Q.w = <fun>

We can subtype from 'a Q.q to Q.w and from Q.w to 'a Q.r. So I now only 
need to equate 'a Q.r with 'a Q.q in one way or another...

I therefore tried the following, unsuccessfully:

> # module W = struct
>     type -'a e = ('a -> unit) q
>     and 'a q = private w
>     and w = w e
>     and 'a r = 'a q e
>   end;;
> Error: The type abbreviation q is cyclic
> # 

What's going wrong? And how can one get to do the proposed recursive 
subtyping?

-- 
      Guillaume Yziquel
http://yziquel.homelinux.org/