I recently came across the 1995 paper Safety analysis versus type inference (pdf link) by Palsberg and Schartzbach that contrasts unification-based type inference and static analysis methods based on control-flow analysis. According to the paper:In unification based type inference each identifier is related to a type variable ranging over type schemes, such as $int$ and $\forall a b . a \rightarrow b$. In control-flow static analysis the identifiers get related to variables ranging over what primitive types and other values in the source program can flow into the identifier.Unification-based type inference is local and can be performed one module at a time. Control-flow analysis tends to be global and require the whole program to be analyzed at once.Damas-Milner unification is a linear time algorithm (for typical programs) while control-flow analysis tends to have worse case running times that are cubic or worse (and at least quadratic in practice).Control-flow analysis can reason about program safety more precisely than unification-based inference (for example, it can detect some instances of dead code)My question is: is this classification complete or are there other kinds of type inference that they did not mention?
Can type inference be classified in two groups: unification-based and control-flow-based?
pl.programming languages;type theory;type systems;type inference
Perhaps an even better way to see type inference is as a specialization of a single framework: Abstract Interpretation (abbreviated AI).  The hallmark of most unification-based type inference algorithms is that they generate the principal type for a term; translated into AI terms, this means that you never need to widen, nor do you need to go to power domains to find the answer.  Unification turns out to be the 'join' operation -- there is also a nice categorical interpretation of unification which is even more enlightening.Several comments shed light on this as well: all algorithms can be better understood in terms of generating then solving systems of constraints.  Unification is indeed eager, and constraint-solving (and that includes control-flow based approaches) tend to be lazier.Perhaps an even better way to see type inference is as an alternate interpreter for a program: rather than producing values, it produces types.  It is very easy to see type inference as a form a partial evaluation.  Perhaps an easy introduction to that circle of ideas is via Aaron Stump's A rewriting view of simple typing.