Inferno

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.

Public API

The constraint solver API provided by the functor Inferno.Solver.Make is public.

Private API

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.

• term structure that the unifier can exploit;
• the unifier;
• the occurs check;
• the type decoders;
• the generalization machinery.

History and Acknowledgements

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).