From: Keiko Nakata <keiko@kurims.kyoto-u.ac.jp>

> I think that it is not easy to know when to apply eta-expansion, 
> namely, to replace a type name with its underlying definition.
> 
> For instance, to check equivalence betweeen the types t and s below:
>  type t = < m : t * t >
>  type 'a tuple = 'a * 'a
>  type s = < m : s tuple >
> 
> the algorithm should memorize that t * t and s tuple are equivalent,
> and then expands s tupl into s * s  
> so as to check between t * t and s * s? 

No need to memorize equivalences: s tuple expands at its head to s * s.
The type checker guarantees that it is always safe to expand the head
of a type (i.e., definitions are well-founded.)
But you're right that abbreviations complicate the unification
algorithm a lot.
In order for unification to succeed above, t must expand to
(< m: 'a * 'a> as 'a), and s too. But to print nicely types we must
keep the abbreviations. This is done by memoizing expansions inside 
the abbreviations themselves. I.e., the expansion of t is actually:
  (< m : t[t='a] * t[t='a] > as 'a)
and that of s is
  (< m : s[s='b] tuple[s='b]> as 'b)
where [t='a] is an internal annotation to the abbreviation. So when
unifying, you can actually check the underlying type of an
abbreviation. But maintaining these abbreviations is rather
involved...
Fo instance abbreviations must be propagated:
  type u = <m : w> and w = u * u
will expand to
  (<m : w[u='a]> as 'a)
so that, if we expand w, we fall back to
  (<m : u[u='a] * u[u='a]>)

Jacques Garrigue