On typability for rank-2 intersection types with polymorphic recursion

We show that typability for a natural form of polymorphic recursive typing for rank-2 intersection types is undecidable. Our proof involves characterizing typability as a conte-xtfree language (CFL) graph problem, which may be of independent interest, and reduction from the boundedness problemfor Turing machines. We also show a property of the type system which, in conjunction with the undecidability result, disproves a misconception about the MilnerMycroft type system. We also show undecidability of a related program analysis problem.