Quantified variable instantiated to eagerly to a unification variable for impredicative types

Consider the following code:

{-# LANGUAGE ImpredicativeTypes #-}

data MVector s a
data ST s a
data Vector a

v3 :: Vector Int
v3 = undefined

f :: forall s. MVector s Int -> ST s ()
f = undefined

modify :: (forall s . MVector s a -> ST s ()) -> Vector a -> Vector a
modify _ _ = undefined

main = flip modify v3 f `seq` pure ()

It produces the following error:

T.hs:16:23: error:
    • Couldn't match expected type ‘forall s. MVector s Int -> ST s ()’
                  with actual type ‘MVector s0 Int -> ST s0 ()’
    • In the third argument of ‘flip’, namely ‘f’
      In the first argument of ‘seq’, namely ‘flip modify v3 f’
      In the expression: flip modify v3 f `seq` pure ()
   |
16 | main = flip modify v3 f `seq` pure ()
   |                       ^

But f really has the required type. It just seems like the s variable is instantiated too eagerly to a unification variable.

Expected behavior

Compile without errors.

Environment

• GHC version used: 9.2.1