From: Swaroop Sridhar <swaroop.sridhar@gmail.com>

> Thanks for the clarification. In order to ensure that I understand you 
> correctly, can you please look into the following unification algorithm 
> and see if it is reasonably correct?

There is a problem with your algorithm:
the way you check the unf field is buggy (you dereference both sides),
but this seems a trivial a trivial error.
More importantly, even corrected it will fail when unifying a loop of
length 3 with a loop of length 2:
   t1 = (int * (int * 'a) as 'a)
   t2 = (int * (int * (int * 'b)) as 'b)
when you reach the inner 'b, you have already unrolled t1, so it also
has its unf field set, but not to t2...

The approach in ocaml is simpler: link at each type node, so that
already unified types will look equal. As a result, after unification
you have only a loop of length 1.

> > A few years ago, infinite loops were a commonly reported bug :-)
> 
> I read a couple of postings about this issue. I understand that one can 
> hurt oneself with a type being parameterized itself. I also read that 
> the type system needs to deal with this in order to support objects. 
> Aren't recursive types necessary even to do a simple linked list like:
> 
> type llist = {contents: int; link : mutable llist}

Note in this case: the definition of llist is nominal, so this type is
only iso-recursive, which is much easier to handle.
The difficulties only appears with
  type llist = < contents: int; link : llist >

Jacques Garrigue