2.6 KiB



  • Support for rigid variables, that is, variables that cannot be unified with other rigid variables or with older flexible variables. These variables are introduced by the new combinators letr1 and letrn. The exception VariableScopeEscape, which is raised when a rigid variable escapes its scope, is also new.

  • Incompatible changes to the solver's high-level API. The module Inferno.SolverHi has been renamed to Inferno.Solver. The combinators (^&), map, ($$), and (^^) have been removed. The combinator construct has been renamed shallow. The combinator build has been renamed deep. The combinator witness has been renamed decode. The combinator instance_ has been removed.

  • New functions pprint and print. These functions allow printing a constraint. They can be useful for debugging purposes.

  • Performance improvements.

  • Improved documentation.


  • Incompatible changes to the solver's high-level API. The concept of a binder has been introduced, and OCaml's binding operators let@, let+, and+ are now used, so as to make it easier to build constraints. (Contributed by Olivier Martinot and Gabriel Scherer.) The types of the combinators exist and construct have been simplified. The new combinator witness can be used to get access to the witness (that is, the final decoded type) for a type variable.


  • In the solver's high-level API, introduce a new combinator range, which allows annotating a constraint with a range of source code positions. Incompatible change: the exceptions Unbound, Unify, and Cycle now carry a range.

  • In the solver's high-level API, define the type deep_ty of deep types, and introduce a new function build, which converts a deep type into a type variable, allowing it to appear in a constraint.

  • In the solver's high-level API, introduce a new function instance_. This is a variant of instance. This function is more convenient (and more efficient) than instance when one does not need to know how a type scheme was instantiated.


  • Change the signature SolverSig.OUTPUT so as to make tyvar an abstract type. An injection function solver_tyvar : int -> tyvar is introduced.

  • Add n-ary products to the System F demo. (Contributed by Gabriel Scherer and Olivier Martinot.)

  • Some cleanup in the directory structure.


  • Use dune instead of ocamlbuild. All necessary library files should now be properly installed (which was not the case in the previous version).


  • First release of Inferno as an opam package.