Complexity of type inference in the simply typed lambda calculus

Question

A similar question was answered here: Is simply typed lambda calculus equivalent to primitive recursive functions

What I conclude from the answers is that the complexity is that of the extended polynomials, but this refers to what can be computed in the STLC, not of type checking expressions in the STLC.

This link provides an algorithm for type-checking. It is claimed that type checking is linear time in an answer to this question: Complexity of type-checking in relation to complexity of normalization

Also, a survey of algorithms that do type inference for STLC, using unification occurs here, but no complexity result is given.

Answer 1

Type inference for simply typed lambda calculus is complete for polynomial time, as elegantly explained in section 1 of Harry Mairson's Linear lambda calculus and PTIME-completeness.

To be a bit more precise, here "type inference" is taken to mean the problem of computing the principal simple type of an untyped lambda term. This is strictly speaking a functional problem ("Given a term $t$, compute its principal type"), but Mairson shows that the corresponding decision problem ("Given a term $t$ and type $A$, is $A$ the principal type of $t$?") is PTIME-hard, by reduction from the circuit value problem. This implies PTIME-completeness, since simple type inference can be performed efficiently using first-order unification. Moreover, Mairson's encoding of the circuit value problem has the property that the terms representing boolean circuits are affine (variables used at most once), and in Section 2 of the paper he gives another encoding that produces linear terms (variables used exactly once). So his proof implies PTIME-completeness of simple type inference even when restricted to affine/linear lambda terms.