On Feb 27, 2010, at 02:52, Guillaume Yziquel wrote:
>
> I've been struggling to have a type system where I could do the  
> following subtyping:
>
> 'a t1 :> t2  and  t2 :> 'a t1

Hm, what do you mean? Subtyping ought to be reflexive and  
antisymmetric (although the latter is rarely proved for most type  
systems), which means that your two inequations will hold if and only  
if 'a t1 = t2, regardless of recursive types.

/Andreas