Note [Do not add duplicate quantified instances] is simplistic, causing rejection of programs

Copied wholesale from !2283 (comment 242042):

Consider

{-# LANGUAGE QuantifiedConstraints, ConstraintKinds,
             ExistentialQuantification #-}

module Bug where

class C1 a

class (forall z. C1 z) => C2 y
class (forall y. C2 y) => C3 x

data Dict c = c => Dict

foo :: (C2 a, C3 a) => a -> Dict (C1 a)
foo _ = Dict

Amazingly, with either C2 a or C3 a, foo is accepted. But with both, it is rejected.

The problem is that, after eagerly expanding superclasses of quantified constraints (that's the new bit), we end up with

[G] g1 :: forall z. C1 z     -- from the C2 a constraint
[G] g2 :: forall y z. C1 z   -- from the C3 a constraint

So when we want to solve C1 a, we don't know which quantified constraint to use, and so we stop. (Also strange: g2 is quantified over the unused y. It's clear where this comes from, and it seems harmless, but it's a bit strange. This detail is not salient. It is not the reason we're struggling here.) This has been seen before, in another guise: #15244 (closed). And we have

{- Note [Do not add duplicate quantified instances]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this (#15244):

  f :: (C g, D g) => ....
  class S g => C g where ...
  class S g => D g where ...
  class (forall a. Eq a => Eq (g a)) => S g where ...

Then in f's RHS there are two identical quantified constraints
available, one via the superclasses of C and one via the superclasses
of D.  The two are identical, and it seems wrong to reject the program
because of that. But without doing duplicate-elimination we will have
two matching QCInsts when we try to solve constraints arising from f's
RHS.

The simplest thing is simply to eliminate duplicates, which we do here.
-}

which is duly implemented. However, here, we don't have duplicates -- we have near-duplicates, which are not caught by the simple (tcEqType) check.

I wonder if the way forward is to really try to "solve" quantified instances. That is, before labeling them inert, we try to interact them with inerts. Then, we might discover that one constraint is implied by another, which will get rid of this problem (and replace that Note).