In this lecture we study the semantics and implementation of type checking with constraints. We study the declarative semantics of constraints by means of constraint satisfaction: given a model (solution), does is the constraint satisfied under that model? And we study the implementation of constraint solvers as a rewrite system that simplifies constraints to basic unification, scope graph, and name resolution constraints. Finally, we study unification, its properties, a naive algorithm, and efficient implementation using union-find.
The PDF of the slides with builds are useful for the union-find section.