Why doesn't this code type-check in Haskell, given that ((forall b. [b]) -> Bool) is more polymorphic than ((forall a. a) -> Bool)?

I'm working with higher-ranked types in Haskell and based on Peyton Jones' Practical Type Inference for Arbitrary-Rank Types), I expect the following function to type-check since ((forall b. [b]) -> Bool) appears to be more polymorphic than ((forall a. a) -> Bool).

Here's my code:

fun :: ((forall b. [b]) -> Bool) -> ((forall a. a) -> Bool)
fun arg = arg

However, GHC rejects it with a type error.

I also tried

fun2 :: (forall a.a -> Bool) -> (forall b.[b] -> Bool)
fun2 arg = arg

which compiled successfully, and it is consistent with the fact that (forall a.a -> Bool) is more polymorphic than (forall b. [b] -> Bool). But I do not understand why fun function that I defined previously does not type check.

As Naïm Favier says in their comment: "Turn on DeepSubsumption.", this will change the subsumption rules that GHC uses, and thus introduce the deep skolemization:

GHC will instead automatically rewrite expressions like f x of type ty1 -> ty2 to become (\ (y :: ty1) -> f x y) ; this is called eta-expansion. See Section 4.6 of Practical type inference for arbitrary-rank types, where this process is called “deep skolemisation”.

which is indeed what the paper "Practical type inference for arbitrary-rank types" on page 21 is talking about:

Hence, perhaps we can solve the problem by enriching the definition of subsumption, so that the type systems of Figure 5 and 6 admit the same programs. That is the reason for the new subsumption judgement ⊢^dsk, defined in Figure 7. This relation subsumes ⊢^ol; it relates strictly more types.