Be more careful in GHC.Tc.Solver.Interact.solveOneFromTheOther

We were failing to account for the cc_pend_sc flag in this
important function, with the result that we expanded superclasses
forever.

Fixes #22516.

6 files changed, 162 insertions, 56 deletions

diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs
index 41ae8fab36..33ee8e854c 100644
--- a/compiler/GHC/Tc/Solver/Canonical.hs
+++ b/compiler/GHC/Tc/Solver/Canonical.hs
@@ -1815,8 +1815,8 @@ only about /completeness/.
 
 Note [Decomposing newtypes a bit more aggressively]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-c.f. https://github.com/ghc-proposals/ghc-proposals/pull/549
-and discussion on !9282.
+c.f. https://github.com/ghc-proposals/ghc-proposals/pull/549,
+issue #22441, and discussion on !9282.
 
 Consider [G] c, [W] (IO Int) ~R (IO Age)
 where IO is abstract, and
diff --git a/compiler/GHC/Tc/Solver/Interact.hs b/compiler/GHC/Tc/Solver/Interact.hs
index 37c8dd6d01..c3aa2d2695 100644
--- a/compiler/GHC/Tc/Solver/Interact.hs
+++ b/compiler/GHC/Tc/Solver/Interact.hs
@@ -448,8 +448,8 @@ instance Outputable InteractResult where
   ppr KeepInert = text "keep inert"
   ppr KeepWork  = text "keep work-item"
 
-solveOneFromTheOther :: CtEvidence  -- Inert    (Dict or Irred)
-                     -> CtEvidence  -- WorkItem (same predicate as inert)
+solveOneFromTheOther :: Ct  -- Inert    (Dict or Irred)
+                     -> Ct  -- WorkItem (same predicate as inert)
                      -> TcS InteractResult
 -- Precondition:
 -- * inert and work item represent evidence for the /same/ predicate
@@ -459,23 +459,40 @@ solveOneFromTheOther :: CtEvidence  -- Inert    (Dict or Irred)
 -- although we don't rewrite wanteds with wanteds, we can combine
 -- two wanteds into one by solving one from the other
 
-solveOneFromTheOther ev_i ev_w
+solveOneFromTheOther ct_i ct_w
   | CtWanted { ctev_loc = loc_w } <- ev_w
   , prohibitedSuperClassSolve loc_i loc_w
-  = -- inert must be Given
+  = -- Inert must be Given
     do { traceTcS "prohibitedClassSolve1" (ppr ev_i $$ ppr ev_w)
        ; return KeepWork }
 
   | CtWanted {} <- ev_w
-       -- Inert is Given or Wanted
-  = return $ case ev_i of
-               CtWanted {} -> choose_better_loc
-                 -- both are Wanted; choice of which to keep is
-                 -- arbitrary. So we look at the context to choose
-                 -- which would make a better error message
+  = -- Inert is Given or Wanted
+    case ev_i of
+      CtGiven {} -> return KeepInert
+        -- work is Wanted; inert is Given: easy choice.
+
+      CtWanted {} -- Both are Wanted
+        -- If only one has no pending superclasses, use it
+        -- Otherwise we can get infinite superclass expansion (#22516)
+        -- in silly cases like   class C T b => C a b where ...
+        | not is_psc_i, is_psc_w     -> return KeepInert
+        | is_psc_i,     not is_psc_w -> return KeepWork
+
+        -- If only one is a WantedSuperclassOrigin (arising from expanding
+        -- a Wanted class constraint), keep the other: wanted superclasses
+        -- may be unexpected by users
+        | not is_wsc_orig_i, is_wsc_orig_w     -> return KeepInert
+        | is_wsc_orig_i,     not is_wsc_orig_w -> return KeepWork
 
-               _           -> KeepInert
-                 -- work is Wanted; inert is Given: easy choice.
+        -- otherwise, just choose the lower span
+        -- reason: if we have something like (abs 1) (where the
+        -- Num constraint cannot be satisfied), it's better to
+        -- get an error about abs than about 1.
+        -- This test might become more elaborate if we see an
+        -- opportunity to improve the error messages
+        | ((<) `on` ctLocSpan) loc_i loc_w -> return KeepInert
+        | otherwise                        -> return KeepWork
 
   -- From here on the work-item is Given
 
@@ -498,31 +515,21 @@ solveOneFromTheOther ev_i ev_w
   | otherwise   -- Both are Given, levels differ
   = return different_level_strategy
   where
+     ev_i  = ctEvidence ct_i
+     ev_w  = ctEvidence ct_w
+
      pred  = ctEvPred ev_i
+
      loc_i = ctEvLoc ev_i
      loc_w = ctEvLoc ev_w
      lvl_i = ctLocLevel loc_i
      lvl_w = ctLocLevel loc_w
 
-     choose_better_loc
-       -- if only one is a WantedSuperclassOrigin (arising from expanding
-       -- a Wanted class constraint), keep the other: wanted superclasses
-       -- may be unexpected by users
-       | is_wanted_superclass_loc loc_i
-       , not (is_wanted_superclass_loc loc_w) = KeepWork
-
-       | not (is_wanted_superclass_loc loc_i)
-       , is_wanted_superclass_loc loc_w = KeepInert
-
-        -- otherwise, just choose the lower span
-        -- reason: if we have something like (abs 1) (where the
-        -- Num constraint cannot be satisfied), it's better to
-        -- get an error about abs than about 1.
-        -- This test might become more elaborate if we see an
-        -- opportunity to improve the error messages
-       | ((<) `on` ctLocSpan) loc_i loc_w = KeepInert
-       | otherwise                        = KeepWork
+     is_psc_w = isPendingScDict ct_w
+     is_psc_i = isPendingScDict ct_i
 
+     is_wsc_orig_i = is_wanted_superclass_loc loc_i
+     is_wsc_orig_w = is_wanted_superclass_loc loc_w
      is_wanted_superclass_loc = isWantedSuperclassOrigin . ctLocOrigin
 
      different_level_strategy  -- Both Given
@@ -650,28 +657,28 @@ once had done). This problem can be tickled by typecheck/should_compile/holes.
 -- mean that (ty1 ~ ty2)
 interactIrred :: InertCans -> Ct -> TcS (StopOrContinue Ct)
 
-interactIrred inerts workItem@(CIrredCan { cc_ev = ev_w, cc_reason = reason })
+interactIrred inerts ct_w@(CIrredCan { cc_ev = ev_w, cc_reason = reason })
   | isInsolubleReason reason
                -- For insolubles, don't allow the constraint to be dropped
                -- which can happen with solveOneFromTheOther, so that
                -- we get distinct error messages with -fdefer-type-errors
-  = continueWith workItem
+  = continueWith ct_w
 
   | let (matching_irreds, others) = findMatchingIrreds (inert_irreds inerts) ev_w
   , ((ct_i, swap) : _rest) <- bagToList matching_irreds
         -- See Note [Multiple matching irreds]
   , let ev_i = ctEvidence ct_i
-  = do { what_next <- solveOneFromTheOther ev_i ev_w
-       ; traceTcS "iteractIrred" (ppr workItem $$ ppr what_next $$ ppr ct_i)
+  = do { what_next <- solveOneFromTheOther ct_i ct_w
+       ; traceTcS "iteractIrred" (ppr ct_w $$ ppr what_next $$ ppr ct_i)
        ; case what_next of
             KeepInert -> do { setEvBindIfWanted ev_w (swap_me swap ev_i)
                             ; return (Stop ev_w (text "Irred equal" <+> parens (ppr what_next))) }
             KeepWork ->  do { setEvBindIfWanted ev_i (swap_me swap ev_w)
                             ; updInertIrreds (\_ -> others)
-                            ; continueWith workItem } }
+                            ; continueWith ct_w } }
 
   | otherwise
-  = continueWith workItem
+  = continueWith ct_w
 
   where
     swap_me :: SwapFlag -> CtEvidence -> EvTerm
@@ -1001,7 +1008,7 @@ and Given/instance fundeps entirely.
 -}
 
 interactDict :: InertCans -> Ct -> TcS (StopOrContinue Ct)
-interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs = tys })
+interactDict inerts ct_w@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs = tys })
   | Just ct_i <- lookupInertDict inerts (ctEvLoc ev_w) cls tys
   , let ev_i = ctEvidence ct_i
   = -- There is a matching dictionary in the inert set
@@ -1015,22 +1022,22 @@ interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs
 
     do { -- Ths short-cut solver didn't fire, so we
          -- solve ev_w from the matching inert ev_i we found
-         what_next <- solveOneFromTheOther ev_i ev_w
+         what_next <- solveOneFromTheOther ct_i ct_w
        ; traceTcS "lookupInertDict" (ppr what_next)
        ; case what_next of
            KeepInert -> do { setEvBindIfWanted ev_w (ctEvTerm ev_i)
                            ; return $ Stop ev_w (text "Dict equal" <+> parens (ppr what_next)) }
            KeepWork  -> do { setEvBindIfWanted ev_i (ctEvTerm ev_w)
                            ; updInertDicts $ \ ds -> delDict ds cls tys
-                           ; continueWith workItem } } }
+                           ; continueWith ct_w } } }
 
   | cls `hasKey` ipClassKey
   , isGiven ev_w
-  = interactGivenIP inerts workItem
+  = interactGivenIP inerts ct_w
 
   | otherwise
   = do { addFunDepWork inerts ev_w cls
-       ; continueWith workItem  }
+       ; continueWith ct_w  }
 
 interactDict _ wi = pprPanic "interactDict" (ppr wi)
 
diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs
index 12b6fcc69f..67c90dcd80 100644
--- a/compiler/GHC/Tc/Solver/Monad.hs
+++ b/compiler/GHC/Tc/Solver/Monad.hs
@@ -536,7 +536,7 @@ get_sc_pending this_lvl ic@(IC { inert_dicts = dicts, inert_insts = insts })
     get_pending :: Ct -> [Ct] -> [Ct]  -- Get dicts with cc_pend_sc = True
                                        -- but flipping the flag
     get_pending dict dicts
-        | Just dict' <- isPendingScDict dict
+        | Just dict' <- pendingScDict_maybe dict
         , belongs_to_this_level (ctEvidence dict)
         = dict' : dicts
         | otherwise
@@ -549,7 +549,7 @@ get_sc_pending this_lvl ic@(IC { inert_dicts = dicts, inert_insts = insts })
 
     get_pending_inst :: [Ct] -> QCInst -> ([Ct], QCInst)
     get_pending_inst cts qci@(QCI { qci_ev = ev })
-       | Just qci' <- isPendingScInst qci
+       | Just qci' <- pendingScInst_maybe qci
        , belongs_to_this_level ev
        = (CQuantCan qci' : cts, qci')
        | otherwise
diff --git a/compiler/GHC/Tc/Types/Constraint.hs b/compiler/GHC/Tc/Types/Constraint.hs
index a876522913..62412cdb65 100644
--- a/compiler/GHC/Tc/Types/Constraint.hs
+++ b/compiler/GHC/Tc/Types/Constraint.hs
@@ -7,14 +7,15 @@
 -- in the type-checker and constraint solver.
 module GHC.Tc.Types.Constraint (
         -- QCInst
-        QCInst(..), isPendingScInst,
+        QCInst(..), pendingScInst_maybe,
 
         -- Canonical constraints
         Xi, Ct(..), Cts,
         emptyCts, andCts, andManyCts, pprCts,
         singleCt, listToCts, ctsElts, consCts, snocCts, extendCtsList,
         isEmptyCts,
-        isPendingScDict, superClassesMightHelp, getPendingWantedScs,
+        isPendingScDict, pendingScDict_maybe,
+        superClassesMightHelp, getPendingWantedScs,
         isWantedCt, isGivenCt,
         isUserTypeError, getUserTypeErrorMsg,
         ctEvidence, ctLoc, ctPred, ctFlavour, ctEqRel, ctOrigin,
@@ -890,18 +891,24 @@ isUserTypeError pred = case getUserTypeErrorMsg pred of
                              Just _ -> True
                              _      -> False
 
-isPendingScDict :: Ct -> Maybe Ct
+isPendingScDict :: Ct -> Bool
+isPendingScDict (CDictCan { cc_pend_sc = psc }) = psc
+-- Says whether this is a CDictCan with cc_pend_sc is True;
+-- i.e. pending un-expanded superclasses
+isPendingScDict _ = False
+
+pendingScDict_maybe :: Ct -> Maybe Ct
 -- Says whether this is a CDictCan with cc_pend_sc is True,
 -- AND if so flips the flag
-isPendingScDict ct@(CDictCan { cc_pend_sc = True })
-                  = Just (ct { cc_pend_sc = False })
-isPendingScDict _ = Nothing
+pendingScDict_maybe ct@(CDictCan { cc_pend_sc = True })
+                      = Just (ct { cc_pend_sc = False })
+pendingScDict_maybe _ = Nothing
 
-isPendingScInst :: QCInst -> Maybe QCInst
+pendingScInst_maybe :: QCInst -> Maybe QCInst
 -- Same as isPendingScDict, but for QCInsts
-isPendingScInst qci@(QCI { qci_pend_sc = True })
-                  = Just (qci { qci_pend_sc = False })
-isPendingScInst _ = Nothing
+pendingScInst_maybe qci@(QCI { qci_pend_sc = True })
+                      = Just (qci { qci_pend_sc = False })
+pendingScInst_maybe _ = Nothing
 
 superClassesMightHelp :: WantedConstraints -> Bool
 -- ^ True if taking superclasses of givens, or of wanteds (to perhaps
@@ -923,7 +930,7 @@ getPendingWantedScs :: Cts -> ([Ct], Cts)
 getPendingWantedScs simples
   = mapAccumBagL get [] simples
   where
-    get acc ct | Just ct' <- isPendingScDict ct
+    get acc ct | Just ct' <- pendingScDict_maybe ct
                = (ct':acc, ct')
                | otherwise
                = (acc,     ct)
diff --git a/testsuite/tests/typecheck/should_compile/T22516.hs b/testsuite/tests/typecheck/should_compile/T22516.hs
new file mode 100644
index 0000000000..6bc481d3ee
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T22516.hs
@@ -0,0 +1,91 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
+module Bug where
+
+import Data.Kind (Constraint, Type)
+
+data D a
+
+f :: Generic (D a) => ()
+f = ()
+
+type family
+  AllF (c :: k -> Constraint) (xs :: [k]) :: Constraint where
+  AllF _c '[]       = ()
+  AllF  c (x ': xs) = (c x, All c xs)
+
+class (AllF c xs, SListI xs) => All (c :: k -> Constraint) (xs :: [k]) where
+
+type SListI = All Top
+
+class Top x
+instance Top x
+
+class All SListI (Code a) => Generic a where
+  type Code a :: [[Type]]
+
+
+{-
+  final wc = WC {wc_impl =
+                   Implic {
+                     TcLevel = 1
+                     Skolems = k_aG9[sk:1] (a_aGa[sk:1] :: k_aG9[sk:1])
+                     Given-eqs = LocalGivenEqs
+                     Status = Unsolved
+                     Given = $dGeneric_aGb :: Generic (D a_aGa[sk:1])
+                     Wanted =
+                       WC {wc_simple =
+                             [W] irred_aGo {0}:: AllF
+                                                   SListI (Code (D a_aGe[tau:1])) (CIrredCan(irred))
+                             [W] irred_aGu {0}:: AllF
+                                                   Top (Code (D a_aGe[tau:1])) (CIrredCan(irred))
+                             [W] $dGeneric_aGf {0}:: Generic (D a_aGe[tau:1]) (CDictCan)
+                             [W] $dAll_aGn {0}:: All SListI (Code (D a_aGe[tau:1])) (CDictCan)
+                             [W] $dAll_aGv {0}:: All
+                                                   Top (Code (D a_aGe[tau:1])) (CDictCan(psc))}
+                     Binds = EvBindsVar<aGg>
+                     the type signature for:
+                       f :: forall {k} (a :: k). Generic (D a) => () }}
+
+
+
+--------------------------
+-- Given
+[G] Generic (D a)
+==> superclass
+[G] All SListI (Code (D a))   =  All (All Top) (Code (D a))
+==> superclass
+[G] AllF SLIstI (Code (D a))  =  AllF (All Top) (Code (D a))
+[G] SListI (Code (D a))       =  All Top (Code (D a))    {loop}
+
+Next iteration
+===>
+[G] AllF Top (Code (D a))
+[G] SListI (Code (D a))       = All Top (Code (D a))  (already there)
+
+--------------------------
+-- Wanted
+[W] Generic (D a)
+==> superclass
+[W] All SListI (Code (D a))   =  All (All Top) (Code (D a))
+==> superclass
+[W] AllF SLIstI (Code (D a))  =  AllF (All Top) (Code (D a))
+[W] SListI (Code (D a))       =  All Top (Code (D a))    {loop}
+
+Next iteration
+===>
+[W] AllF Top (Code (D a))
+[W] SListI (Code (D a))       = All Top (Code (D a))  (already there)
+
+-}
\ No newline at end of file
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 6413034c05..1f1e7d8d1f 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -852,3 +852,4 @@ test('T21951b', normal, compile, ['-Wredundant-strictness-flags'])
 test('T21550', normal, compile, [''])
 test('T22310', normal, compile, [''])
 test('T22331', normal, compile, [''])
+test('T22516', normal, compile, [''])