Nested quantified constraints don't work

Consider this, spun off from #14860:

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE InstanceSigs #-}
module Foo where

class    (forall c. c ~ T a => Show (c b)) => ShowT a b
instance Show (T a b) => ShowT a b

class (forall b. Show b => ShowT a b) => C a where
  type family T a :: * -> *

data D a = MkD (T a Int)

instance C a => Show (D a) where
  showsPrec p (MkD x)
    = (showParen (p > 10) $ showString "MkD " . showsPrec 11 x)

When typechecking the final instance decl we get

T14860a.hs:22:49: error:
    • Could not deduce (Show (T a Int))
        arising from a use of ‘showsPrec’
      from the context: C a
        bound by the instance declaration at T14860a.hs:20:10-26

but this is bogus. We have

g1: [G] C a                                          -- Given by the instance
g2: [G] forall b. Show b => ShowT a b                -- Superclass of g1
g3: [G] forall b c. (Show b, c ~ T a) => Show (c b)  -- Superclass of g2

w1: [W] Show (T a Int)   -- Wanted by the rhs of showsPrec

Well, that wanted should match g3! But it doesn't because g3 ends up with a funny type

g3: [G] forall b. Show b => forall c. (Show b, c ~ T a) => Show (c b)

and that doens't work well at all.

Should not be hard to fix this.

EDIT: In the end, we don't think we really should accept this program, because it purports to solve Show (a b) for any a and b -- an unlikely proposition. But the current (now that !2283 (closed) has landed) error message complains about default methods, which is poor form. We should fix the error message.