Note [GND and QuantifiedConstraints]

Consider the following example from #15290:

  class C m where
    join :: m (m a) -> m a

  newtype T m a = MkT (m a)

  deriving instance
    (C m, forall p q. Coercible p q => Coercible (m p) (m q)) =>
    C (T m)

The code that GHC used to generate for this was:

  instance (C m, forall p q. Coercible p q => Coercible (m p) (m q)) =>
      C (T m) where
    join = coerce @(forall a.   m   (m a) ->   m a)
                  @(forall a. T m (T m a) -> T m a)
                  join

This instantiates `coerce` at a polymorphic type, a form of impredicative
polymorphism, so we're already on thin ice. And in fact the ice breaks,
as we'll explain:

The call to `coerce` gives rise to:

  Coercible (forall a.   m   (m a) ->   m a)
            (forall a. T m (T m a) -> T m a)

And that simplified to the following implication constraint:

  forall a <no-ev>. m (T m a) ~R# m (m a)

But because this constraint is under a `forall`, inside a type, we have to
prove it *without computing any term evidence* (hence the <no-ev>). Alas, we
*must* generate a term-level evidence binding in order to instantiate the
quantified constraint! In response, GHC currently chooses not to use such
a quantified constraint.
See Note [Instances in no-evidence implications] in GHC.Tc.Solver.Equality.

But this isn't the death knell for combining QuantifiedConstraints with GND.
On the contrary, if we generate GND bindings in a slightly different way, then
we can avoid this situation altogether. Instead of applying `coerce` to two
polymorphic types, we instead use a type abstraction to bind the type
variables, and omit the `forall`s in the type applications. More concretely, we
generate the following code instead:

  instance (C m, forall p q. Coercible p q => Coercible (m p) (m q)) =>
      C (T m) where
    join @a = coerce @(  m   (m a) ->   m a)
                     @(T m (T m a) -> T m a)
                     join

Now the visible type arguments are both monotypes, so we don't need any of this
funny quantified constraint instantiation business. While this particular
example no longer uses impredicative instantiation, we still need to enable
ImpredicativeTypes to typecheck GND-generated code for class methods with
higher-rank types. See Note [Newtype-deriving instances].

You might think that that second @(T m (T m a) -> T m a) argument is redundant
with the type information provided by the class, but in fact leaving it off
will break the following example (from the T12616 test case):

  type m ~> n = forall a. m a -> n a
  data StateT s m a = ...
  newtype OtherStateT s m a = OtherStateT (StateT s m a)

  class MonadTrans t where
    lift :: (Monad m) => m ~> t m

  instance MonadTrans (StateT s)

  instance MonadTrans (OtherStateT s) where
    lift @m = coerce @(m ~> StateT s m)
                     lift

That is because we still need to instantiate the second argument of
coerce with a polytype, and we can only do that with VTA or QuickLook.