Intersection types are an example where the theory is in its full generality undecidable, and where applications in useful PLs tends to use only low-rank intersection types.

See https://en.wikipedia.org/wiki/Intersection_type_discipline