Module Logtk.TypeInference

Type Inference

This module is used for two things that overlap:

• inferring the types of symbols that have not been declared (e.g. in "fof" or "cnf" TPTP statements) so as to enrich a Signature
• converting untyped terms or formulas into typed formulas, by inferring the exact type of each subterm (and possibly inferring type parameters).

In this context, generalizing type variables means that if some ID.t whose type was unknown and its type still contains variables after the type inference, those variables are quantified instead of being bound to a default type (typically .Type.i).

For instance: say f is not declared and occurs in the term f(f(nil)) with the declared constructor nil : list(A). The inferred type for f should be something like list(B) -> list(B).

• If we generalize, we declare that f : list(A) -> list(A) (for all A).
• If we don't, we declare that f : list($i) -> list($i).

Here we use a single scope when we unify and substitute type variables, the scope 0.

Many functions will use an Error monad to make errors explicit. The error type is or_error. The module CCError in containers can be used to deal with errors (including monadic operators).