Module Inferno.Solver

module Make (X : sig ... end) (S : sig ... end) (O : sig ... end) : sig ... end

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.