Which languages, if any, implement rank-2 parametric polymorphism and why not ML?

Question

In section 23.8 of his book Types and Programming Languages, Benjamin C. Pierce writes the following:

Another well-studied restriction of System F is rank-2 polymorphism, introduced by Leivant (1983) [...]. A type is said to be of rank 2 if no path from its root to a ∀ quantifier passes to the left of 2 or more arrows, when the type is drawn as a tree. [...] In the rank-2 system, all types are restricted to be of rank 2. This system is slightly more powerful than the prenex (ML) fragment, in the sense that it can assign types to more untyped lambda-terms.

Kfoury and Tiuryn (1990) proved that the complexity of type reconstruction for the rank-2 fragment of System F is identical to that of ML (i.e, DExptime-complete). Kfoury and Wells (1999) gave the first correct type reconstruction algorithm for the rank 2 system and showed that type reconstruction for ranks 3 and higher of system F is undecidable.

So type inference for rank-2 polymorphism is known to be decidable and an algorithm has been known since 1999. Haskell supports with its RankNTypes language extension, but it enables rank-n polymorphism.

1. Which languages, if any, implement rank-2 parametric polymorphism but not System F?

2. Since type inference is decidable and has not a worst complexity, why have neither SML nor OCaml extended polymorphism to rank-2?

3. Why do we not see and read more about rank-2 polymorphism in the wild?

Nitramine

that doesn't directly answer your question, but Haskell has Rank2Types - RankNTypes is a generalization of this but it's possible to only opt into n = 2. – Enclosure

On 2: SML has been "frozen" since 1997. I don't expect it to gain any new features, ever. I also wouldn't expect this to find its way into OCaml until some grad student at INRIA wants to do it. – Gouty

There are extensions of ML to higher-ranked type systems, like MLF and HMF. They give up on complete inference, requiring annotations in some circumstances. And OCaml's polymorphic fields allow encoding rank-n polymorphism anyway (at some syntactic cost). – Whet

Many OO languages apparently implement rank-2 polymorphism: Java and C# according to this answer https://mcmap.net/q/47174/-what-is-the-purpose-of-rank2types – Inconsiderate

OCaml has first-class polymorphism, i.e., can express arbitrary rank. But it requires wrapping in records, objects, or modules to aid typing. So Rank 2 is available, but not with full type inference. It's probably not worth making a special case for that. – Numbersnumbfish

For reference: I think the first paper is this one, and the second one is that one (it is from 1994, not 1999, maybe a typo in Pierce’s book?). Perhaps also relevant is that paper which describes the semi-explicit approach adopted by OCaml. – Lietman