Inferno is an OCaml library for constraint-based type inference and elaboration. Its constraint solver performs first-order unification and handles Hindley-Milner polymorphism. The constraints carry semantic actions that facilitate elaboration, which is the process of constructing an explicitly-typed term.
The constraint solver API provided by the functor Inferno.Solver.Make is public.
The documentation of the following modules is made available as an aid to understanding the code. However, these modules should not directly be used outside Inferno; their API is subject to change.
Inferno has been written by François Pottier and is described in the paper Hindley-Milner elaboration in applicative style (ICFP 2014).
Since 2020, Inferno has benefited from many contributions by Olivier Martinot and Gabriel Scherer. See in particular Quantified Applicatives: API design for type-inference constraints (ML Family Workshop 2020).