We investigate finite-rank intersection type systems, analyzing the complexity of their type inference problems and their relation to the problem of recognizing semantically equivalent terms. Intersection types allow something of type τ

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)=2 ^{KK(t,n)}*; we prove
that recognizing the pure λ-terms of size

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))).*