How high are the higher types that appear in practice? This is admittedly a rather naively put and vague question, and I'm not sure how much more specific I want or can make it, but I'll try.

By "practice" I mean surely in actual programming practice (of which I embarrassingly don't know much), but also in mathematical practice, whenever certain higher-type objects are employed as examples or counterexamples within arguments.

By the "height" of a type, I don't mean to include the obvious and natural arbitrariness involved in objects like, say, the fixpoint functional (in fact, in the spirit of the question, I would prefer to understand this as a type $2$ object "up to parameter types", so to speak). A better example of what I mean would be the well-known (from mathematical practice, at least) fan functional, of type $((\mathbb{N} \to \mathbb{B}) \to \mathbb{N}) \to \mathbb{N}$, given by
$$
\lambda f. \mu m. \forall_{\alpha, \beta}
\left(
\forall_{n &lt; m} \alpha(n) = \beta(n) \to f(\alpha) = f(\beta)
\right) \ ,
$$
where $f : (\mathbb{N} \to \mathbb{B}) \to \mathbb{N}$ and $\alpha, \beta : \mathbb{N} \to \mathbb{B}$.

My questions: Are there any objects of yet higher type than $3$ (possibly "up to parameter types") that are naturally used in the literature? In practice?
Okasaki's Functional Pearl, "Even Higher-Order Functions for Parsing or Why Would Anyone Ever Want To Use a Sixth-Order Function?" answers this question with a type of order 6.