> The code of Caml Light is not 'just' the
> Hindley/Milner/Robinson kind of thing, though there are
> similarities.

There are a number of tricks in the efficient implementation of type
inference that you won't find in Hindley, Milner, nor Robinson, indeed.
Some are described in Cardelli's paper "Basic polymorphic type-checking",
Science of computer programming, 8(2). 

The Caml Light typechecker also uses "levels" on type variables to
implement generalization efficiently. This folklore trick is described
in Weis and Leroy's book "Le langage Caml" (in French, unfortunately),
and also (but much more abstractly) in some publications by Didier
Remy. I believe Didier is on the list, so maybe he can provide more
references.

> What are dangerous type variables

A type analysis to prevent polymorphic mutable structures (e.g.
polymorphic references), similar in purpose to imperative type
variables but much superior in my opinion. See my POPL 91 paper and
my PhD thesis (available on
ftp.inria.fr:INRIA/Projects/cristal/Xavier.Leroy).

> and why does
> the type checker include two unification algorithms?

I don't understand what you're alluding to. Where is the second algorithm?

- Xavier Leroy