Complexity of type inference in the simply typed lambda calculus
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 &quot;type inference&quot; is taken to mean the problem of computing the principal simple type of an untyped lambda term. This is strictly speaking a functional problem (&quot;Given a term $t$, compute its principal type&quot;), but Mairson shows that the corresponding decision problem (&quot;Given a term $t$ and type $A$, is $A$ the principal type of $t$?&quot;) 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.