Unify is not recursive anymore, it just adds constraints to the queue
Unify builds a graph of primitive constraints. However there is a bug.

assert in Ctx.subst_ctx fails because somewhere along the line we
screwed up something. The most likely culprit is add_substitution
in unify.ml.
Debugging graphs
Small improvement to comments
Fixed a bug that kept accumulating constraints.
Fixed a bug that kept generating substitutions of non-parameter dirts and regions.
Fixed a bug that ignored the expansion of type parameters.

For example, [[]] now has the correct type 'a list list
Added a computation of the transitive closure.
Added computation of positive and negative parameters in a type.
Added garbage collection, but now we remove too much.
Merge branch 'effect-system' of github.com:andrejbauer/eff into effect-system
Fixed a bug that deleted too much constraints in let inference.

There is still one left in let-rec inference.
Added invariance for types in recursive definitions, but it is not enough.
Merge branch 'effect-system' of https://github.com/andrejbauer/eff into effect-system
Even more garbage collection.
Transitive closure now works correctly.
Fixed a bug with incorrect constraints in patterns.
Removed some unnecessary constraints in let-rec.
Added Ty.variablize, which creates a variable only version of a type that is used in unification with parameters.

The name is horrible, I agree.
Further relaxed constraints in Infer.infer_let_rec