Quantified constraints with different order of quantification but otherwise identical are not considered the same

This ticket arose as a side conversation of #22216 (closed).

The following program is currently rejected:

{-# LANGUAGE AllowAmbiguousTypes, RankNTypes, QuantifiedConstraints #-}

module T22223 where

class C a b

foo :: ( forall a b. (Eq a, Ord b) => C a b
       , forall b a. (Eq a, Ord b) => C a b
       , Eq x
       , Ord y )
    => ( C x y => r ) -> r
foo r = r

• Could not deduce (C x y) arising from a use of ‘r’
  from the context: (forall a b. (Eq a, Ord b) => C a b,
                     forall b a. (Eq a, Ord b) => C a b, Eq x, Ord y)
    bound by the type signature for:
               foo :: forall x y r.
                      (forall a b. (Eq a, Ord b) => C a b,
                       forall b a. (Eq a, Ord b) => C a b, Eq x, Ord y) =>
                      (C x y => r) -> r
    at T22223.hs:(7,1)-(11,26)
• In the expression: r
  In an equation for ‘foo’: foo r = r

(See also #20468 (closed) for the poor error message.)

Removing either of the quantified constraints in the type signature of foo allows the program to be accepted.

This is because GHC adds two different Given quantified constraints to the inert set, because the quantification order is different (see GHC.Tc.Solver.Monad.addInertForAll.same_qci). This means that GHC doesn't know which one to use when trying to solve [W] C x y when typechecking the body of foo, and thus refrains from solving [W] C x y entirely.

This is in contrast to the following program, which does work (as the QCs are indeed recognised as duplicates of eachother, and thus only one is retained in the inert set):

{-# LANGUAGE AllowAmbiguousTypes, RankNTypes, QuantifiedConstraints #-}

module T22223_yes where

class C a b

foo :: ( forall a b. (Eq a, Ord b) => C a b
       , forall u v. (Eq u, Ord v) => C u v
       , Eq x
       , Ord y )
    => ( C x y => r ) -> r
foo r = r