Lambda the Ultimate

Trevor Jim’s System P₂ types the same terms as the second-rank System F₂, but function arguments can only be typed as (finite) intersections of simple types. This restriction is reasonable and also seems to correspond neatly to the inner workings of a compiler which specializes polymorphic functions for every usage (such as Rust’s, IIRC). What do we lose, relative to F₂? Here are the things that I can think of (in fact, they also apply to unrestricted System P, which prohibits universal quantifiers in negative positions):

• The ST monad of Peyton Jones et al. famously uses second-rank universal quantification to prevent imperative state from leaking outside, by defining runST :: forall a. (forall s. ST s a) -> a and threading the dummy parameter s through all related imperative things — e. g., imperative variables are accessed by readSTRef :: STRef s a -> ST s a and writeSTRef :: a -> STRef s a -> ST s (). Dynamic event switching in reactive-banana is guaranteed free of time leaks using a similar mechanism. (It sort of makes sense that we lose this: it is difficult to see how a universally quantified type could be inferred for any argument. Though…)
• Induction principles for non-regular datatypes have rank-2 types (always?). It seems to me that so do types defined using Haskell’s ExistentialQuantification extension.

Anything else?

Side note: What is then the class of all datatypes whose induction principles fit into P₂? Is it interesting or any bigger than that for HM? I don’t understand what intersections could mean as eliminator arguments.