Where is the inner m quantified over?

@pash writes:

there's really no such thing as an "unquantified" type signature in Haskell.

Here's a program:

{-# LANGUAGE Haskell98, ScopedTypeVariables, InstanceSigs #-}
module Identity where

newtype IdentityT f a = IdentityT { runIdentityT :: f a }

instance Functor m => Functor (IdentityT m) where
    fmap f (IdentityT m) = IdentityT (fmap f m)

instance Applicative m => Applicative (IdentityT m) where
    pure x = IdentityT (pure x)
    IdentityT a <*> IdentityT b = IdentityT (a <*> b)

instance Monad m => Monad (IdentityT m) where
    (>>=) :: forall a b. IdentityT m a -> (a -> IdentityT m b) -> IdentityT m b
    IdentityT m >>= k =
      let
        f :: a -> m b
        f x =
          let IdentityT ran = k x
           in ran
      in
      IdentityT (f =<< m)

I can compile it with GHC 9.10.1 using ghc -c Identity.hs -fforce-recomp.

But note how the m isn't explicitly quantified over using a forall. I want to add the explicit quantification. Where does the inference algorithm add it? I thought it would add it to either the signature for f or for =<<. But if I add quantifications in either of those places, the program no longer compiles.

How do I remove implicit quantifications from the program?

either the signature for f or for =<<.

Since the instance head is where m is first used, that is where the forall would be.

instance forall m. Monad m => Monad (IdentityT m) where

But note that the m in the signature of f isn't necessarily the same in the original program, since ScopedTypeVariables only applies if the m is forall'd. So if you add the scoping of the outer m (by using forall), the inner m is now constrained to be the same... I don't understand how come compilation fails if you change the inner type-level m to be n instead, i.e. f :: a -> n b.

EDIT: It seems that instance heads are treated specially, and the type variables may always be scoped there, if ScopedTypeVariables is on.