A (small) correction, I forgot to write the base case that will allow 
for termination:

> 
> Unify (first:TYPE, second: TYPE)
>    will return true on Unification false if not.
> 
> 1. Start
> 2. let t1 = repr first
>    let t2 = repr second

   2.5  if t1 equals t2
	   return true
> 
> 3. match (t1.kind, t2.kind) with
> 
>    case (Integer, Integer) ->
>            return true
> 
>    case (Tvar, _ )  ->
>            t1.link = Some t2
>            return true
> 
>    case (_, Tvar) ->
>            t2.link = Some t1
>            return true
> 
>    case (Record, Record) ->
> 
>            if the record lengths don't match
>               return false
> 
>         t1.link = t2  (***** linked speculatively *****)
> 
>            for each i in 0 to t1.components.size()
>               Unify (t1.components[i], t2.components[i])
>               if Unification fails,
>             t1.link = None
>             unlink all types that were linked until now
>             return false
>           endif
> 
>            for each i in 0 to t1.typeArgs.size()
>               Unify (t1.typeArgs[i], t2.typeArgs[i])
>               if Unification fails,
>             unlink all types that were linked until now
>             return false
>           endif
> 
>        return true
> 
>    case (_, _)  ->
>            return false
> 
> 4. Stop

Swaroop.