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