Assaf Kfoury, Harry Mairson, Franklyn Turbak, and J.B. Wells. Relating Typability and Expressiveness in Finite-Rank Intersection Type Systems. International Conference on Functional Programming (ICFP '99). ACM, 1999.
While type inference is computable at every rank, we show that its complexity grows exponentially as rank increases. Let KK(0,n)=n and KK(t+1,n)=2KK(t,n); we prove that recognizing the pure λ-terms of size n that are typable at rank k is complete for DTIME[KK(k-1,n)].
We then consider the problem of deciding whether two λ-terms typable at rank k have the same normal form, generalizing a
well-known result of Statman from simple types to finite-rank
intersection types. We show that the equivalence problem is
DTIME[KK(KK(k-1,n),2)]-complete. This relationship
between the complexity of typability and expressiveness is identical
in well-known decidable type systems such as simple types and
Hindley-Milner types, but seems to fail for System F and its
generalizations. The correspondence gives rise to a conjecture that
if T is a predicative type system where typability has
complexity t(n) and expressiveness has complexity
e(n), then t(n)=Ω(log*(e(n))).