Interesting use cases for universal quantifiers in rank 2?

Trevor Jim’s System P2 types the same terms as the second-rank System F2, 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 F2? 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 P2? Is it interesting or any bigger than that for HM? I don’t understand what intersections could mean as eliminator arguments.