# Type Inference

We use a kind of Hindley-Milner algorithm to infer types.
Two main constraints are to be respected:

- compatibility with TPTP (THF/TFF1), which forces parametric polymorphism
- flexibility for the meta-prover

We also have interesting extensions such as extensible records.

## Sketch of the algorithm

The algorithm takes as input a `PrologTerm.t`, i.e. an unscoped, untyped
AST with some annotations (`PrologTerm.Column (t,ty)`) and a signature.
The signature is used (and updated) to map constants to their types.

Only declared constants can be polymorphic, because when we meet
a new symbol (or a variable) that is applied to arguments, there is no
**syntactic** way to know which arguments are terms and which are types.
Therefore they are all assumed to be terms unless the signature specifies
the converse explicitely.

For `HOTerm` inference, application is left-parenthesed, so when a symbol
requires `n` type arguments and `m` term arguments, we assume the `n` first
arguments to be types.