I speculated about a complexity problem and its relation to types. On page 104 of LotCHI (92, in print), the authors note that, in the simply-typed lambda calculus, a reduction of the type inhabitation problem to the type checking problem would show that P = PSPACE.
I also wondered if there was a Heyting algebra for higher-order polymorphic typed lambda calculi that we can use to show that some type is uninhabited. LotCHI section 12.2 gets part of the way there (The authors cover F2, I would need F3, I think.), with the answer that yes, there is such an algebra, but no, it doesn't make things so easy.