QuantifiedConstraints: GHC does doesn't discharge constraints if they are quantified

This came up on a reddit thread,

{-# Language QuantifiedConstraints #-}

class (forall aa. Functor (bi aa)) => Bifunctor bi where
  first :: (a -> a') -> (bi a b -> bi a' b)

bimap :: Bifunctor bi => (a -> a') -> (b -> b') -> (bi a b -> bi a' b')
bimap f g = first f . fmap g

This is the type we want for bimap even if we mix & match Bifunctor and Functor. We already know that we can fmap @(bi xx) for any xx but this is not the inferred type.

Instead GHC infers a type (tidied up) with a superfluous Functor constraint

bimap :: (Bifunctor bi, Functor (bi a)) => (a -> a') -> (b -> b') -> (bi a b -> bi a' b')

Indeed post-composing with a superfluous fmap @(bi a') id incurs yet another Functor constraint

bimap :: (Bifunctor bi, Functor (bi a), Functor (bi a')) => (a -> a') -> (b -> b') -> (bi a b -> bi a' b')
bimap f g = fmap id . first f . fmap g

A terminology question, I'm not sure how to phrase what GHC isn't doing to the Functor constraints: ‘discharge’?