matchLocalInst: do domination analysis

When multiple Given quantified constraints match a Wanted, and there is
a quantified constraint that dominates all others, we now pick it
to solve the Wanted.

See Note [Use only the best matching quantified constraint].

For example:

  [G] d1: forall a b. ( Eq a, Num b, C a b  ) => D a b
  [G] d2: forall a  .                C a Int  => D a Int
  [W] {w}: D a Int

When solving the Wanted, we find that both Givens match, but we pick
the second, because it has a weaker precondition, C a Int, compared
to (Eq a, Num Int, C a Int). We thus say that d2 dominates d1;
see Note [When does a quantified instance dominate another?].

This domination test is done purely in terms of superclass expansion,
in the function GHC.Tc.Solver.Interact.impliedBySCs. We don't attempt
to do a full round of constraint solving; this simple check suffices
for now.

Fixes #22216 and #22223

13 files changed, 368 insertions, 90 deletions

diff --git a/compiler/GHC/Tc/Solver/InertSet.hs b/compiler/GHC/Tc/Solver/InertSet.hs
index c1f173ee14..e95a1debff 100644
--- a/compiler/GHC/Tc/Solver/InertSet.hs
+++ b/compiler/GHC/Tc/Solver/InertSet.hs
@@ -1558,23 +1558,28 @@ matchableGivens loc_w pred_w inerts@(IS { inert_cans = inert_cans })
     matchable_given :: Ct -> Bool
     matchable_given ct
       | CtGiven { ctev_loc = loc_g, ctev_pred = pred_g } <- ctEvidence ct
-      = mightEqualLater inerts pred_g loc_g pred_w loc_w
+      = isJust $ mightEqualLater inerts pred_g loc_g pred_w loc_w
 
       | otherwise
       = False
 
-mightEqualLater :: InertSet -> TcPredType -> CtLoc -> TcPredType -> CtLoc -> Bool
+mightEqualLater :: InertSet -> TcPredType -> CtLoc -> TcPredType -> CtLoc -> Maybe Subst
 -- See Note [What might equal later?]
 -- Used to implement logic in Note [Instance and Given overlap] in GHC.Tc.Solver.Interact
 mightEqualLater inert_set given_pred given_loc wanted_pred wanted_loc
   | prohibitedSuperClassSolve given_loc wanted_loc
-  = False
+  = Nothing
 
   | otherwise
   = case tcUnifyTysFG bind_fun [flattened_given] [flattened_wanted] of
-      SurelyApart              -> False  -- types that are surely apart do not equal later
-      MaybeApart MARInfinite _ -> False  -- see Example 7 in the Note.
-      _                        -> True
+      Unifiable subst
+        -> Just subst
+      MaybeApart reason subst
+        | MARInfinite <- reason -- see Example 7 in the Note.
+        -> Nothing
+        | otherwise
+        -> Just subst
+      SurelyApart -> Nothing
 
   where
     in_scope  = mkInScopeSet $ tyCoVarsOfTypes [given_pred, wanted_pred]
diff --git a/compiler/GHC/Tc/Solver/Interact.hs b/compiler/GHC/Tc/Solver/Interact.hs
index 59723cfe70..37bf3a9f1d 100644
--- a/compiler/GHC/Tc/Solver/Interact.hs
+++ b/compiler/GHC/Tc/Solver/Interact.hs
@@ -50,6 +50,7 @@ import GHC.Types.Var.Env
 
 import qualified Data.Semigroup as S
 import Control.Monad
+import Data.Maybe ( listToMaybe, mapMaybe )
 import GHC.Data.Pair (Pair(..))
 import GHC.Types.Unique( hasKey )
 import GHC.Driver.Session
@@ -2470,109 +2471,236 @@ matchLocalInst :: TcPredType -> CtLoc -> TcS ClsInstResult
 matchLocalInst pred loc
   = do { inerts@(IS { inert_cans = ics }) <- getTcSInerts
        ; case match_local_inst inerts (inert_insts ics) of
-           ([], Nothing) -> do { traceTcS "No local instance for" (ppr pred)
-                               ; return NoInstance }
-
-             -- See Note [Use only the best local instance] about
-             -- superclass depths
-           (matches, unifs)
-             | [(dfun_ev, inst_tys)] <- best_matches
-             , maybe True (> min_sc_depth) unifs
-             -> do { let dfun_id = ctEvEvId dfun_ev
-                   ; (tys, theta) <- instDFunType dfun_id inst_tys
-                   ; let result = OneInst { cir_new_theta = theta
-                                          , cir_mk_ev     = evDFunApp dfun_id tys
-                                          , cir_what      = LocalInstance }
-                   ; traceTcS "Best local inst found:" (ppr result)
-                   ; traceTcS "All local insts:" (ppr matches)
-                   ; return result }
-
-             | otherwise
-             -> do { traceTcS "Multiple local instances for" (ppr pred)
-                   ; return NotSure }
-
-             where
-               extract_depth = sc_depth . ctEvLoc . fst
-               min_sc_depth = minimum (map extract_depth matches)
-               best_matches = filter ((== min_sc_depth) . extract_depth) matches }
+          { ([], []) -> do { traceTcS "No local instance for" (ppr pred)
+                           ; return NoInstance }
+          ; (matches, unifs) ->
+    do { matches <- mapM mk_instDFun matches
+       ; unifs   <- mapM mk_instDFun unifs
+         -- See Note [Use only the best matching quantified constraint]
+       ; case dominatingMatch matches of
+          { Just (dfun_id, tys, theta)
+            | all ((theta `impliedBySCs`) . thdOf3) unifs
+            ->
+            do { let result = OneInst { cir_new_theta = theta
+                                      , cir_mk_ev     = evDFunApp dfun_id tys
+                                      , cir_what      = LocalInstance }
+               ; traceTcS "Best local instance found:" $
+                  vcat [ text "pred:" <+> ppr pred
+                       , text "result:" <+> ppr result
+                       , text "matches:" <+> ppr matches
+                       , text "unifs:" <+> ppr unifs ]
+               ; return result }
+
+          ; mb_best ->
+            do { traceTcS "Multiple local instances; not committing to any"
+                  $ vcat [ text "pred:" <+> ppr pred
+                         , text "matches:" <+> ppr matches
+                         , text "unifs:" <+> ppr unifs
+                         , text "best_match:" <+> ppr mb_best ]
+               ; return NotSure }}}}}
   where
     pred_tv_set = tyCoVarsOfType pred
 
-    sc_depth :: CtLoc -> Int
-    sc_depth ctloc = case ctLocOrigin ctloc of
-      InstSCOrigin depth _  -> depth
-      OtherSCOrigin depth _ -> depth
-      _                     -> 0
+    mk_instDFun :: (CtEvidence, [DFunInstType]) -> TcS InstDFun
+    mk_instDFun (ev, tys) =
+      let dfun_id = ctEvEvId ev
+      in do { (tys, theta) <- instDFunType (ctEvEvId ev) tys
+            ; return (dfun_id, tys, theta) }
 
-    -- See Note [Use only the best local instance] about superclass depths
+    -- Compute matching and unifying local instances
     match_local_inst :: InertSet
                      -> [QCInst]
                      -> ( [(CtEvidence, [DFunInstType])]
-                        , Maybe Int )   -- Nothing ==> no unifying local insts
-                                        -- Just n ==> unifying local insts, with
-                                        --            minimum superclass depth
-                                        --            of n
+                        , [(CtEvidence, [DFunInstType])] )
     match_local_inst _inerts []
-      = ([], Nothing)
-    match_local_inst inerts (qci@(QCI { qci_tvs = qtvs, qci_pred = qpred
-                               , qci_ev = qev })
-                             : qcis)
+      = ([], [])
+    match_local_inst inerts (qci@(QCI { qci_tvs  = qtvs
+                                      , qci_pred = qpred
+                                      , qci_ev   = qev })
+                            :qcis)
       | let in_scope = mkInScopeSet (qtv_set `unionVarSet` pred_tv_set)
       , Just tv_subst <- ruleMatchTyKiX qtv_set (mkRnEnv2 in_scope)
                                         emptyTvSubstEnv qpred pred
       , let match = (qev, map (lookupVarEnv tv_subst) qtvs)
-      = (match:matches, unif)
+      = (match:matches, unifs)
 
       | otherwise
       = assertPpr (disjointVarSet qtv_set (tyCoVarsOfType pred))
                   (ppr qci $$ ppr pred)
             -- ASSERT: unification relies on the
             -- quantified variables being fresh
-        (matches, unif `combine` this_unif)
+        (matches, this_unif `combine` unifs)
       where
         qloc = ctEvLoc qev
         qtv_set = mkVarSet qtvs
+        (matches, unifs) = match_local_inst inerts qcis
         this_unif
-          | mightEqualLater inerts qpred qloc pred loc = Just (sc_depth qloc)
-          | otherwise = Nothing
-        (matches, unif) = match_local_inst inerts qcis
+          | Just subst <- mightEqualLater inerts qpred qloc pred loc
+          = Just (qev, map  (lookupTyVar subst) qtvs)
+          | otherwise
+          = Nothing
 
-        combine Nothing  Nothing    = Nothing
-        combine (Just n) Nothing    = Just n
-        combine Nothing  (Just n)   = Just n
-        combine (Just n1) (Just n2) = Just (n1 `min` n2)
+        combine Nothing  us = us
+        combine (Just u) us = u : us
 
-{- Note [Use only the best local instance]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+-- | Instance dictionary function and type.
+type InstDFun = (DFunId, [TcType], TcThetaType)
+
+-- | Try to find a local quantified instance that dominates all others,
+-- i.e. which has a weaker instance context than all the others.
+--
+-- See Note [Use only the best matching quantified constraint].
+dominatingMatch :: [InstDFun] -> Maybe InstDFun
+dominatingMatch matches =
+  listToMaybe $ mapMaybe (uncurry go) (holes matches)
+  -- listToMaybe: arbitrarily pick any one context that is weaker than
+  -- all others, e.g. so that we can handle [Eq a, Num a] vs [Num a, Eq a]
+  -- (see test case T22223).
+
+  where
+    go :: InstDFun -> [InstDFun] -> Maybe InstDFun
+    go this [] = Just this
+    go this@(_,_,this_theta) ((_,_,other_theta):others)
+      | this_theta `impliedBySCs` other_theta
+      = go this others
+      | otherwise
+      = Nothing
+
+-- | Whether a collection of constraints is implied by another collection,
+-- according to a simple superclass check.
+--
+-- See Note [When does a quantified instance dominate another?].
+impliedBySCs :: TcThetaType -> TcThetaType -> Bool
+impliedBySCs c1 c2 = all in_c2 c1
+  where
+    in_c2 :: TcPredType -> Bool
+    in_c2 pred = any (pred `eqType`) c2_expanded
+
+    c2_expanded :: [TcPredType]  -- Includes all superclasses
+    c2_expanded = [ q | p <- c2, q <- p : transSuperClasses p ]
+
+
+{- Note [When does a quantified instance dominate another?]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When matching local quantified instances, it's useful to be able to pick
+the one with the weakest precondition, e.g. if one has both
+
+  [G] d1: forall a b. ( Eq a, Num b, C a b  ) => D a b
+  [G] d2: forall a  .                C a Int  => D a Int
+  [W] {w}: D a Int
+
+Then it makes sense to use d2 to solve w, as doing so we end up with a strictly
+weaker proof obligation of `C a Int`, compared to `(Eq a, Num Int, C a Int)`
+were we to use d1.
+
+In theory, to compute whether one context implies another, we would need to
+recursively invoke the constraint solver. This is expensive, so we instead do
+a simple check using superclasses, implemented in impliedBySCs.
+
+Examples:
+
+ - [Eq a] is implied by [Ord a]
+ - [Ord a] is not implied by [Eq a],
+ - any context is implied by itself,
+ - the empty context is implied by any context.
+
+Note [Use only the best matching quantified constraint]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider (#20582) the ambiguity check for
   (forall a. Ord (m a), forall a. Semigroup a => Eq (m a)) => m Int
 
 Because of eager expansion of given superclasses, we get
-  [G] forall a. Ord (m a)
-  [G] forall a. Eq (m a)
-  [G] forall a. Semigroup a => Eq (m a)
+  [G] d1: forall a. Ord (m a)
+  [G] d2: forall a. Eq (m a)
+  [G] d3: forall a. Semigroup a => Eq (m a)
 
-  [W] forall a. Ord (m a)
-  [W] forall a. Semigroup a => Eq (m a)
+  [W] {w1}: forall a. Ord (m a)
+  [W] {w2}: forall a. Semigroup a => Eq (m a)
 
 The first wanted is solved straightforwardly. But the second wanted
-matches *two* local instances. Our general rule around multiple local
+matches *two* local instances: d2 and d3. Our general rule around multiple local
 instances is that we refuse to commit to any of them. However, that
 means that our type fails the ambiguity check. That's bad: the type
 is perfectly fine. (This actually came up in the wild, in the streamly
 library.)
 
-The solution is to prefer local instances with fewer superclass selections.
-So, matchLocalInst is careful to whittle down the matches only to the
-ones with the shallowest superclass depth, and also to worry about unifying
-local instances that are at that depth (or less).
+The solution is to prefer local instances which are easier to prove, meaning
+that they have a weaker precondition. In this case, the empty context
+of d2 is a weaker constraint than the "Semigroup a" context of d3, so we prefer
+using it when proving w2. This allows us to pass the ambiguity check here.
+
+Our criterion for solving a Wanted by matching local quantified instances is
+thus as follows:
+
+  - There is a matching local quantified instance that dominates all others
+    matches, in the sense of [When does a quantified instance dominate another?].
+    Any such match do, we pick it arbitrarily (the T22223 example below says why).
+  - This local quantified instance also dominates all the unifiers, as we
+    wouldn't want to commit to a single match when we might have multiple,
+    genuinely different matches after further unification takes place.
+
+Some other examples:
+
+
+  #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 ...
+
+  Here, in f's RHS, there are two identical quantified constraints
+  available, one via the superclasses of C and one via the superclasses
+  of D. Given that each implies the other, we pick one arbitrarily.
+
+
+  #22216:
+
+    class Eq a
+    class Eq a => Ord a
+    class (forall b. Eq b => Eq (f b)) => Eq1 f
+    class (Eq1 f, forall b. Ord b => Ord (f b)) => Ord1 f
+
+  Suppose we have
+
+    [G] d1: Ord1 f
+    [G] d2: Eq a
+    [W] {w}: Eq (f a)
+
+  Superclass expansion of d1 gives us:
+
+    [G] d3 : Eq1 f
+    [G] d4 : forall b. Ord b => Ord (f b)
+
+  expanding d4 and d5 gives us, respectively:
+
+    [G] d5 : forall b. Eq  b => Eq (f b)
+    [G] d6 : forall b. Ord b => Eq (f b)
+
+  Now we have two matching local instances that we could use when solving the
+  Wanted. However, it's obviously silly to use d6, given that d5 provides us with
+  as much information, with a strictly weaker precondition. So we pick d5 to solve
+  w. If we chose d6, we would get [W] Ord a, which in this case we can't solve.
+
+
+  #22223:
 
-By preferring these shallower local instances, we can use the last given
-listed above and pass the ambiguity check.
+    [G] forall a b. (Eq a, Ord b) => C a b
+    [G] forall a b. (Ord b, Eq a) => C a b
+    [W] C x y
 
-The instance-depth mechanism uses the same superclass depth
-information as described in Note [Replacement vs keeping], 2a.
+  Here we should be free to pick either quantified constraint, as they are
+  equivalent up to re-ordering of the constraints in the context.
+  See also Note [Do not add duplicate quantified instances]
+  in GHC.Tc.Solver.Monad.
 
-Test case: typecheck/should_compile/T20582.
+Test cases:
+  typecheck/should_compile/T20582
+  quantified-constraints/T15244
+  quantified-constraints/T22216{a,b,c,d,e}
+  quantified-constraints/T22223
 
+Historical note: a previous solution was to instead pick the local instance
+with the least superclass depth (see Note [Replacement vs keeping]),
+but that doesn't work for the example from #22216.
 -}
diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs
index 7eb1df9649..63b5aee2b4 100644
--- a/compiler/GHC/Tc/Solver/Monad.hs
+++ b/compiler/GHC/Tc/Solver/Monad.hs
@@ -220,21 +220,17 @@ addInertForAll new_qci
 
 {- Note [Do not add duplicate quantified instances]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider this (#15244):
+As an optimisation, we avoid adding duplicate quantified instances to the
+inert set; we use a simple duplicate check using tcEqType for simplicity,
+even though it doesn't account for superficial differences, e.g. it will count
+the following two constraints as different (#22223):
 
-  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 ...
+  - forall a b. C a b
+  - forall b a. C a b
 
-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.
+The main logic that allows us to pick local instances, even in the presence of
+duplicates, is explained in Note [Use only the best matching quantified constraint]
+in GHC.Tc.Solver.Interact.
 -}
 
 {- *********************************************************************
diff --git a/compiler/GHC/Tc/Types/Origin.hs b/compiler/GHC/Tc/Types/Origin.hs
index 7d257f4763..ce16837805 100644
--- a/compiler/GHC/Tc/Types/Origin.hs
+++ b/compiler/GHC/Tc/Types/Origin.hs
@@ -464,8 +464,7 @@ data CtOrigin
   -- have 'InstSCOrigin' origin.
   | InstSCOrigin ScDepth      -- ^ The number of superclass selections necessary to
                               -- get this constraint; see Note [Replacement vs keeping]
-                              -- and Note [Use only the best local instance], both in
-                              -- GHC.Tc.Solver.Interact
+                              -- in GHC.Tc.Solver.Interact
                  TypeSize     -- ^ If @(C ty1 .. tyn)@ is the largest class from
                               --    which we made a superclass selection in the chain,
                               --    then @TypeSize = sizeTypes [ty1, .., tyn]@
@@ -478,12 +477,13 @@ data CtOrigin
   --      f = e
   -- When typechecking body of 'f', the superclasses of the Given (Foo a)
   -- will have 'OtherSCOrigin'.
-  -- Needed for Note [Replacement vs keeping] and
-  -- Note [Use only the best local instance], both in GHC.Tc.Solver.Interact.
+  --
+  -- Needed for Note [Replacement vs keeping] in GHC.Tc.Solver.Interact.
   | OtherSCOrigin ScDepth -- ^ The number of superclass selections necessary to
                           -- get this constraint
-                  SkolemInfoAnon   -- ^ Where the sub-class constraint arose from
-                               -- (used only for printing)
+                  SkolemInfoAnon
+                    -- ^ Where the sub-class constraint arose from
+                    -- (used only for printing)
 
   -- All the others are for *wanted* constraints
 
diff --git a/compiler/GHC/Utils/Misc.hs b/compiler/GHC/Utils/Misc.hs
index 2701565cc8..49f85d7d6a 100644
--- a/compiler/GHC/Utils/Misc.hs
+++ b/compiler/GHC/Utils/Misc.hs
@@ -43,6 +43,8 @@ module GHC.Utils.Misc (
 
         chunkList,
 
+        holes,
+
         changeLast,
         mapLastM,
 
@@ -506,6 +508,13 @@ chunkList :: Int -> [a] -> [[a]]
 chunkList _ [] = []
 chunkList n xs = as : chunkList n bs where (as,bs) = splitAt n xs
 
+-- | Compute all the ways of removing a single element from a list.
+--
+--  > holes [1,2,3] = [(1, [2,3]), (2, [1,3]), (3, [1,2])]
+holes :: [a] -> [(a, [a])]
+holes []     = []
+holes (x:xs) = (x, xs) : mapSnd (x:) (holes xs)
+
 -- | Replace the last element of a list with another element.
 changeLast :: [a] -> a -> [a]
 changeLast []     _  = panic "changeLast"
diff --git a/docs/users_guide/9.6.1-notes.rst b/docs/users_guide/9.6.1-notes.rst
index f66ba9e06a..54f4a3fed2 100644
--- a/docs/users_guide/9.6.1-notes.rst
+++ b/docs/users_guide/9.6.1-notes.rst
@@ -68,6 +68,16 @@ Language
   :extension:`TypeData`. This extension permits ``type data`` declarations
   as a more fine-grained alternative to :extension:`DataKinds`.
 
+- GHC now does a better job of solving constraints in the presence of multiple
+  matching quantified constraints. For example, if we want to solve
+  ``C a b Int`` and we have matching quantified constraints: ::
+
+    forall x y z. (Ord x, Enum y, Num z) => C x y z
+    forall u v. (Enum v, Eq u) => C u v Int
+
+  Then GHC will use the second quantified constraint to solve ``C a b Int``,
+  as it has a strictly weaker precondition.
+
 Compiler
 ~~~~~~~~
 
diff --git a/testsuite/tests/quantified-constraints/T22216a.hs b/testsuite/tests/quantified-constraints/T22216a.hs
new file mode 100644
index 0000000000..f8df47d73d
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T22216a.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE QuantifiedConstraints, UndecidableInstances #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+
+module T22216a where
+
+class Eq a
+class Eq a => Ord a
+
+class (forall b. Eq b => Eq (f b)) => Eq1 f
+class (Eq1 f, forall b. Ord b => Ord (f b)) => Ord1 f
+
+foo :: (Ord a, Ord1 f) => (Eq (f a) => r) -> r
+foo r = r
diff --git a/testsuite/tests/quantified-constraints/T22216b.hs b/testsuite/tests/quantified-constraints/T22216b.hs
new file mode 100644
index 0000000000..6a2e5082a3
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T22216b.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE StandaloneDeriving #-}
+
+module T22216b where
+
+import Data.Functor.Classes
+
+newtype T f a = MkT (f a)
+  deriving ( Eq, Ord, Eq1
+           , Ord1
+           )
diff --git a/testsuite/tests/quantified-constraints/T22216c.hs b/testsuite/tests/quantified-constraints/T22216c.hs
new file mode 100644
index 0000000000..262522832a
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T22216c.hs
@@ -0,0 +1,23 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module T22216c where
+
+import Prelude (Bool, Ordering)
+
+class Eq a where
+class Eq a => Ord a where
+class (forall a. Eq a => Eq (f a)) => Eq1 f where
+
+class (Eq1 f, forall a. Ord a => Ord (f a)) => Ord1 f where
+  liftCompare :: (a -> b -> Ordering) -> f a -> f b -> Ordering
+
+instance Eq  (T f a)
+instance Ord (T f a)
+instance Eq1 (T f)
+
+newtype T f a = MkT (f a)
+  deriving Ord1
diff --git a/testsuite/tests/quantified-constraints/T22216d.hs b/testsuite/tests/quantified-constraints/T22216d.hs
new file mode 100644
index 0000000000..94dfbcb7ee
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T22216d.hs
@@ -0,0 +1,33 @@
+{-# LANGUAGE QuantifiedConstraints #-}
+
+module T22216d where
+
+class (forall a. Eq a => Eq (f a)) => Eq1 f where
+  liftEq :: (a -> b -> Bool) -> f a -> f b -> Bool
+
+eq1 :: (Eq1 f, Eq a) => f a -> f a -> Bool
+eq1 = liftEq (==)
+
+class (Eq1 f, forall a. Ord a => Ord (f a)) => Ord1 f where
+  liftCompare :: (a -> b -> Ordering) -> f a -> f b -> Ordering
+
+compare1 :: (Ord1 f, Ord a) => f a -> f a -> Ordering
+compare1 = liftCompare compare
+
+data Cofree f a = a :< f (Cofree f a)
+
+instance (Eq1 f, Eq a) => Eq (Cofree f a) where
+  (==) = eq1
+
+instance (Eq1 f) => Eq1 (Cofree f) where
+  liftEq eq = go
+    where
+      go (a :< as) (b :< bs) = eq a b && liftEq go as bs
+
+instance (Ord1 f, Ord a) => Ord (Cofree f a) where
+  compare = compare1
+
+instance (Ord1 f) => Ord1 (Cofree f) where
+  liftCompare cmp = go
+    where
+      go (a :< as) (b :< bs) = cmp a b `mappend` liftCompare go as bs
diff --git a/testsuite/tests/quantified-constraints/T22216e.hs b/testsuite/tests/quantified-constraints/T22216e.hs
new file mode 100644
index 0000000000..7d6a6dd009
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T22216e.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE QuantifiedConstraints, UndecidableInstances #-}
+{-# LANGUAGE RankNTypes #-}
+
+module T22216e where
+
+import Data.Kind
+
+type C :: Type -> Type -> Constraint
+type D :: Type -> Type -> Constraint
+
+class C a b
+instance C () Int
+class D a b
+
+foo :: ( forall a b. ( Eq a, Num b, C a b  ) => D a b
+       , forall a  .                C a Int  => D a Int
+       )
+    => ( D () Int => r ) -> r
+foo r = r
diff --git a/testsuite/tests/quantified-constraints/T22223.hs b/testsuite/tests/quantified-constraints/T22223.hs
new file mode 100644
index 0000000000..3bccb6745b
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T22223.hs
@@ -0,0 +1,24 @@
+{-# LANGUAGE AllowAmbiguousTypes, RankNTypes, QuantifiedConstraints #-}
+
+module T22223 where
+
+import Data.Kind
+
+type C :: Type -> Type -> Constraint
+class C a b
+
+-- Change the order of quantification
+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
+
+-- Permute the constraints in the context
+bar :: ( forall a b. (Eq a, Ord b) => C a b
+       , forall a b. (Ord b, Eq a) => C a b
+       , Eq x
+       , Ord y )
+    => ( C x y => r ) -> r
+bar r = r
diff --git a/testsuite/tests/quantified-constraints/all.T b/testsuite/tests/quantified-constraints/all.T
index 00d66e55a8..fba21ff79d 100644
--- a/testsuite/tests/quantified-constraints/all.T
+++ b/testsuite/tests/quantified-constraints/all.T
@@ -34,3 +34,9 @@ test('T19921', normal, compile_fail, [''])
 test('T16474', normal, compile_fail, [''])
 test('T21006', normal, compile_fail, [''])
 test('T21037', normal, compile, [''])
+test('T22216a', normal, compile, [''])
+test('T22216b', normal, compile, [''])
+test('T22216c', normal, compile, [''])
+test('T22216d', normal, compile, [''])
+test('T22216e', normal, compile, [''])
+test('T22223', normal, compile, [''])