This module offers a set of combinators for building constraints as well as a constraint solver. This allows the user to express a type inference problem as a constraint. Then, type inference amounts to solving this constraint. Naturally, the constraint solver produces a Boolean outcome: whether the constraint is satisfiable or unsatisfiable. Furthermore, in case the constraint is satisfiable, it also produces a semantic value, an OCaml value that is computed in a bottom-up fashion. This allows the user to perform elaboration, that is, to produce an explicitly-typed program as an outcome.