Constraint simplification loop now depends on `ExpansionFuel`wip/T21909

instead of a boolean flag for `CDictCan.cc_pend_sc`.
Pending givens get a fuel of 3 while Wanted and quantified constraints get a fuel of 1.
This helps pending given constraints to keep up with pending wanted constraints in case of
`UndecidableSuperClasses` and superclass expansions while simplifying the infered type.

Adds 3 dynamic flags for controlling the fuels for each type of constraints
`-fgivens-expansion-fuel` for givens `-fwanteds-expansion-fuel` for wanteds and `-fqcs-expansion-fuel` for quantified constraints

Fixes #21909
Added Tests T21909, T21909b
Added Note [Expanding Recursive Superclasses and ExpansionFuel]

11 files changed, 331 insertions, 98 deletions

diff --git a/compiler/GHC/Core/Class.hs b/compiler/GHC/Core/Class.hs
index 9ad470e9da..1b46f66fca 100644
--- a/compiler/GHC/Core/Class.hs
+++ b/compiler/GHC/Core/Class.hs
@@ -17,8 +17,8 @@ module GHC.Core.Class (
         mkClass, mkAbstractClass, classTyVars, classArity,
         classKey, className, classATs, classATItems, classTyCon, classMethods,
         classOpItems, classBigSig, classExtraBigSig, classTvsFds, classSCTheta,
-        classAllSelIds, classSCSelId, classSCSelIds, classMinimalDef, classHasFds,
-        isAbstractClass,
+        classHasSCs, classAllSelIds, classSCSelId, classSCSelIds, classMinimalDef,
+        classHasFds, isAbstractClass,
     ) where
 
 import GHC.Prelude
@@ -295,6 +295,9 @@ classSCTheta (Class { classBody = ConcreteClass { cls_sc_theta = theta_stuff }})
   = theta_stuff
 classSCTheta _ = []
 
+classHasSCs :: Class -> Bool
+classHasSCs cls = not (null (classSCTheta cls))
+
 classTvsFds :: Class -> ([TyVar], [FunDep TyVar])
 classTvsFds c = (classTyVars c, classFunDeps c)
 
diff --git a/compiler/GHC/Driver/Session.hs b/compiler/GHC/Driver/Session.hs
index 2ad09bc7c6..20fcc3f6fe 100644
--- a/compiler/GHC/Driver/Session.hs
+++ b/compiler/GHC/Driver/Session.hs
@@ -517,7 +517,15 @@ data DynFlags = DynFlags {
   reductionDepth        :: IntWithInf,   -- ^ Typechecker maximum stack depth
   solverIterations      :: IntWithInf,   -- ^ Number of iterations in the constraints solver
                                          --   Typically only 1 is needed
-
+  givensFuel            :: Int,          -- ^ Number of layers of superclass expansion for givens
+                                         --   Should be < solverIterations
+                                         --   See Note [Expanding Recursive Superclasses and ExpansionFuel]
+  wantedsFuel           :: Int,          -- ^ Number of layers of superclass expansion for wanteds
+                                         --   Should be < givensFuel
+                                         --   See Note [Expanding Recursive Superclasses and ExpansionFuel]
+  qcsFuel                :: Int,          -- ^ Number of layers of superclass expansion for quantified constraints
+                                         --   Should be < givensFuel
+                                         --   See Note [Expanding Recursive Superclasses and ExpansionFuel]
   homeUnitId_             :: UnitId,                 -- ^ Target home unit-id
   homeUnitInstanceOf_     :: Maybe UnitId,           -- ^ Id of the unit to instantiate
   homeUnitInstantiations_ :: [(ModuleName, Module)], -- ^ Module instantiations
@@ -1148,6 +1156,9 @@ defaultDynFlags mySettings =
         mainFunIs               = Nothing,
         reductionDepth          = treatZeroAsInf mAX_REDUCTION_DEPTH,
         solverIterations        = treatZeroAsInf mAX_SOLVER_ITERATIONS,
+        givensFuel              = mAX_GIVENS_FUEL,
+        wantedsFuel             = mAX_WANTEDS_FUEL,
+        qcsFuel                 = mAX_QC_FUEL,
 
         homeUnitId_             = mainUnitId,
         homeUnitInstanceOf_     = Nothing,
@@ -2733,6 +2744,12 @@ dynamic_flags_deps = [
       (intSuffix (\n d -> d { reductionDepth = treatZeroAsInf n }))
   , make_ord_flag defFlag "fconstraint-solver-iterations"
       (intSuffix (\n d -> d { solverIterations = treatZeroAsInf n }))
+  , make_ord_flag defFlag "fgivens-expansion-fuel"
+      (intSuffix (\n d -> d { givensFuel = n }))
+  , make_ord_flag defFlag "fwanteds-expansion-fuel"
+      (intSuffix (\n d -> d { wantedsFuel = n }))
+  , make_ord_flag defFlag "fqcs-expansion-fuel"
+      (intSuffix (\n d -> d { qcsFuel = n }))
   , (Deprecated, defFlag "fcontext-stack"
       (intSuffixM (\n d ->
        do { deprecate $ "use -freduction-depth=" ++ show n ++ " instead"
diff --git a/compiler/GHC/Settings/Constants.hs b/compiler/GHC/Settings/Constants.hs
index f2ceea8517..0c0e460ab6 100644
--- a/compiler/GHC/Settings/Constants.hs
+++ b/compiler/GHC/Settings/Constants.hs
@@ -30,6 +30,27 @@ mAX_REDUCTION_DEPTH = 200
 mAX_SOLVER_ITERATIONS :: Int
 mAX_SOLVER_ITERATIONS = 4
 
+-- | In case of loopy quantified costraints constraints,
+--   how many times should we allow superclass expansions
+--   Should be less than mAX_SOLVER_ITERATIONS
+--   See Note [Expanding Recursive Superclasses and ExpansionFuel]
+mAX_QC_FUEL :: Int
+mAX_QC_FUEL = 3
+
+-- | In case of loopy wanted constraints,
+--   how many times should we allow superclass expansions
+--   Should be less than mAX_GIVENS_FUEL
+-- See Note [Expanding Recursive Superclasses and ExpansionFuel]
+mAX_WANTEDS_FUEL :: Int
+mAX_WANTEDS_FUEL = 1
+
+-- | In case of loopy given constraints,
+--   how many times should we allow superclass expansions
+--   Should be less than max_SOLVER_ITERATIONS
+-- See Note [Expanding Recursive Superclasses and ExpansionFuel]
+mAX_GIVENS_FUEL :: Int
+mAX_GIVENS_FUEL = 3
+
 wORD64_SIZE :: Int
 wORD64_SIZE = 8
 
diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs
index f113820c02..81fa86aea4 100644
--- a/compiler/GHC/Tc/Solver.hs
+++ b/compiler/GHC/Tc/Solver.hs
@@ -2338,6 +2338,10 @@ maybe_simplify_again n limit unif_happened wc@(WC { wc_simple = simples })
     do { new_given  <- makeSuperClasses pending_given
        ; new_wanted <- makeSuperClasses pending_wanted
        ; solveSimpleGivens new_given -- Add the new Givens to the inert set
+       ; traceTcS "maybe_simplify_again" (vcat [ text "pending_given" <+> ppr pending_given
+                                               , text "new_given" <+> ppr new_given
+                                               , text "pending_wanted" <+> ppr pending_wanted
+                                               , text "new_wanted" <+> ppr new_wanted ])
        ; simplify_loop n limit (not (null pending_given)) $
          wc { wc_simple = simples1 `unionBags` listToBag new_wanted } } }
          -- (not (null pending_given)): see Note [Superclass iteration]
@@ -2366,6 +2370,73 @@ superclasses.  In that case we check whether the new Wanteds actually led to
 any new unifications, and iterate the implications only if so.
 -}
 
+{- Note [Expanding Recursive Superclasses and ExpansionFuel]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider the class declaration (T21909)
+
+    class C [a] => C a where
+       foo :: a -> Int
+
+and suppose during type inference we obtain an implication constraint:
+
+    forall a. C a => C [[a]]
+
+To solve this implication constraint, we first expand one layer of the superclass
+of Given constraints, but not for Wanted constraints.
+(See Note [Eagerly expand given superclasses] and Note [Why adding superclasses can help]
+in GHC.Tc.Solver.Canonical.) We thus get:
+
+    [G] g1 :: C a
+    [G] g2 :: C [a]    -- new superclass layer from g1
+    [W] w1 :: C [[a]]
+
+Now, we cannot solve `w1` directly from `g1` or `g2` as we may not have
+any instances for C. So we expand a layer of superclasses of each Wanteds and Givens
+that we haven't expanded yet.
+This is done in `maybe_simplify_again`. And we get:
+
+    [G] g1 :: C a
+    [G] g2 :: C [a]
+    [G] g3 :: C [[a]]    -- new superclass layer from g2, can solve w1
+    [W] w1 :: C [[a]]
+    [W] w2 :: C [[[a]]]  -- new superclass layer from w1, not solvable
+
+Now, although we can solve `w1` using `g3` (obtained from expanding `g2`),
+we have a new wanted constraint `w2` (obtained from expanding `w1`) that cannot be solved.
+We thus make another go at solving in `maybe_simplify_again` by expanding more
+layers of superclasses. This looping is futile as Givens will never be able to catch up with Wanteds.
+
+Side Note: In principle we don't actually need to /solve/ `w2`, as it is a superclass of `w1`
+but we only expand it to expose any functional dependencies (see Note [The superclass story])
+But `w2` is a wanted constraint, so we will try to solve it like any other,
+even though ultimately we will discard its evidence.
+
+Solution: Simply bound the maximum number of layers of expansion for
+Givens and Wanteds, with ExpansionFuel.  Give the Givens more fuel
+(say 3 layers) than the Wanteds (say 1 layer). Now the Givens will
+win.  The Wanteds don't need much fuel: we are only expanding at all
+to expose functional dependencies, and wantedFuel=1 means we will
+expand a full recursive layer.  If the superclass hierarchy is
+non-recursive (the normal case) one layer is therefore full expansion.
+
+The default value for wantedFuel = Constants.max_WANTEDS_FUEL = 1.
+The default value for givenFuel  = Constants.max_GIVENS_FUEL = 3.
+Both are configurable via the `-fgivens-fuel` and `-fwanteds-fuel`
+compiler flags.
+
+There are two preconditions for the default fuel values:
+   (1) default givenFuel >= default wantedsFuel
+   (2) default givenFuel < solverIterations
+
+Precondition (1) ensures that we expand givens at least as many times as we expand wanted constraints
+preferably givenFuel > wantedsFuel to avoid issues like T21909 while
+the precondition (2) ensures that we do not reach the solver iteration limit and fail with a
+more meaningful error message
+
+This also applies for quantified constraints; see `-fqcs-fuel` compiler flag and `QCI.qci_pend_sc` field.
+-}
+
+
 solveNestedImplications :: Bag Implication
                         -> TcS (Bag Implication)
 -- Precondition: the TcS inerts may contain unsolved simples which have
diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs
index b5c65df24a..bef422c9a2 100644
--- a/compiler/GHC/Tc/Solver/Canonical.hs
+++ b/compiler/GHC/Tc/Solver/Canonical.hs
@@ -59,7 +59,7 @@ import Control.Monad
 import Data.Maybe ( isJust, isNothing )
 import Data.List  ( zip4 )
 import GHC.Types.Basic
-
+import GHC.Driver.Session ( givensFuel, wantedsFuel, qcsFuel )
 import qualified Data.Semigroup as S
 import Data.Bifunctor ( bimap )
 
@@ -154,9 +154,13 @@ canClassNC :: CtEvidence -> Class -> [Type] -> TcS (StopOrContinue Ct)
 -- Precondition: EvVar is class evidence
 canClassNC ev cls tys
   | isGiven ev  -- See Note [Eagerly expand given superclasses]
-  = do { sc_cts <- mkStrictSuperClasses ev [] [] cls tys
+  = do { dflags <- getDynFlags
+       ; sc_cts <- mkStrictSuperClasses (givensFuel dflags) ev [] [] cls tys
+                           -- givensFuel dflags: See Note [Expanding Recursive Superclasses and ExpansionFuel]
        ; emitWork sc_cts
-       ; canClass ev cls tys False }
+       ; canClass ev cls tys doNotExpand }
+                           -- doNotExpand: We have already expanded superclasses for /this/ dict
+                           -- so set the fuel to doNotExpand to avoid repeating expansion
 
   | CtWanted { ctev_rewriters = rewriters } <- ev
   , Just ip_name <- isCallStackPred cls tys
@@ -168,7 +172,7 @@ canClassNC ev cls tys
   -- and Note [Solving CallStack constraints] in GHC.Tc.Solver.Types
   = do { -- First we emit a new constraint that will capture the
          -- given CallStack.
-       ; let new_loc = setCtLocOrigin loc (IPOccOrigin (HsIPName ip_name))
+         let new_loc = setCtLocOrigin loc (IPOccOrigin (HsIPName ip_name))
                             -- We change the origin to IPOccOrigin so
                             -- this rule does not fire again.
                             -- See Note [Overview of implicit CallStacks]
@@ -182,14 +186,20 @@ canClassNC ev cls tys
                                   (ctLocSpan loc) (ctEvExpr new_ev)
        ; solveCallStack ev ev_cs
 
-       ; canClass new_ev cls tys False -- No superclasses
+       ; canClass new_ev cls tys doNotExpand
+                              -- doNotExpand: No superclasses for class CallStack
+                              -- See invariants in CDictCan.cc_pend_sc
        }
 
   | otherwise
-  = canClass ev cls tys (has_scs cls)
+  = do { dflags <- getDynFlags
+       ; let fuel | classHasSCs cls = wantedsFuel dflags
+                  | otherwise   = doNotExpand
+                  -- See Invariants in `CCDictCan.cc_pend_sc`
+       ; canClass ev cls tys fuel
+       }
 
   where
-    has_scs cls = not (null (classSCTheta cls))
     loc  = ctEvLoc ev
     orig = ctLocOrigin loc
     pred = ctEvPred ev
@@ -206,7 +216,7 @@ solveCallStack ev ev_cs = do
 
 canClass :: CtEvidence
          -> Class -> [Type]
-         -> Bool            -- True <=> un-explored superclasses
+         -> ExpansionFuel            -- n > 0 <=> un-explored superclasses
          -> TcS (StopOrContinue Ct)
 -- Precondition: EvVar is class evidence
 
@@ -307,10 +317,11 @@ So here's the plan:
 4. Go round to (2) again.  This loop (2,3,4) is implemented
    in GHC.Tc.Solver.simpl_loop.
 
-The cc_pend_sc flag in a CDictCan records whether the superclasses of
+The cc_pend_sc field in a CDictCan records whether the superclasses of
 this constraint have been expanded.  Specifically, in Step 3 we only
-expand superclasses for constraints with cc_pend_sc set to true (i.e.
-isPendingScDict holds).
+expand superclasses for constraints with cc_pend_sc > 0
+(i.e. isPendingScDict holds).
+See Note [Expanding Recursive Superclasses and ExpansionFuel]
 
 Why do we do this?  Two reasons:
 
@@ -337,7 +348,8 @@ our strategy.  Consider
   f :: C a => a -> Bool
   f x = x==x
 Then canClassNC gets the [G] d1: C a constraint, and eager emits superclasses
-G] d2: D a, [G] d3: C a (psc).  (The "psc" means it has its sc_pend flag set.)
+G] d2: D a, [G] d3: C a (psc).  (The "psc" means it has its cc_pend_sc has pending
+expansion fuel.)
 When processing d3 we find a match with d1 in the inert set, and we always
 keep the inert item (d1) if possible: see Note [Replacement vs keeping] in
 GHC.Tc.Solver.Interact.  So d3 dies a quick, happy death.
@@ -484,7 +496,6 @@ the sc_theta_ids at all. So our final construction is
 
 makeSuperClasses :: [Ct] -> TcS [Ct]
 -- Returns strict superclasses, transitively, see Note [The superclass story]
--- See Note [The superclass story]
 -- The loop-breaking here follows Note [Expanding superclasses] in GHC.Tc.Utils.TcType
 -- Specifically, for an incoming (C t) constraint, we return all of (C t)'s
 --    superclasses, up to /and including/ the first repetition of C
@@ -493,39 +504,45 @@ makeSuperClasses :: [Ct] -> TcS [Ct]
 --           class C [a] => D a
 -- makeSuperClasses (C x) will return (D x, C [x])
 --
--- NB: the incoming constraints have had their cc_pend_sc flag already
---     flipped to False, by isPendingScDict, so we are /obliged/ to at
---     least produce the immediate superclasses
+-- NB: the incoming constraint's superclass will consume a unit of fuel
+-- Preconditions on `cts`: 1. They are either `CDictCan` or `CQuantCan`
+--                         2. Their fuel (stored in cc_pend_sc or qci_pend_sc) is > 0
 makeSuperClasses cts = concatMapM go cts
   where
-    go (CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys })
-      = mkStrictSuperClasses ev [] [] cls tys
-    go (CQuantCan (QCI { qci_pred = pred, qci_ev = ev }))
+    go (CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys, cc_pend_sc = fuel })
+      = assertFuelPreconditionStrict fuel $ -- fuel needs to be more than 0 always
+        mkStrictSuperClasses fuel ev [] [] cls tys
+    go (CQuantCan (QCI { qci_pred = pred, qci_ev = ev, qci_pend_sc = fuel }))
       = assertPpr (isClassPred pred) (ppr pred) $  -- The cts should all have
                                                    -- class pred heads
-        mkStrictSuperClasses ev tvs theta cls tys
+        assertFuelPreconditionStrict fuel $ -- fuel needs to be more than 0 always
+        mkStrictSuperClasses fuel ev tvs theta cls tys
       where
         (tvs, theta, cls, tys) = tcSplitDFunTy (ctEvPred ev)
     go ct = pprPanic "makeSuperClasses" (ppr ct)
 
 mkStrictSuperClasses
-    :: CtEvidence
+    :: ExpansionFuel -> CtEvidence
     -> [TyVar] -> ThetaType  -- These two args are non-empty only when taking
                              -- superclasses of a /quantified/ constraint
     -> Class -> [Type] -> TcS [Ct]
 -- Return constraints for the strict superclasses of
 --   ev :: forall as. theta => cls tys
-mkStrictSuperClasses ev tvs theta cls tys
-  = mk_strict_superclasses (unitNameSet (className cls))
+-- Precondition: fuel > 0
+-- Postcondition: fuel for recursive superclass ct is one unit less than cls fuel
+mkStrictSuperClasses fuel ev tvs theta cls tys
+  = mk_strict_superclasses (consumeFuel fuel) (unitNameSet (className cls))
                            ev tvs theta cls tys
 
-mk_strict_superclasses :: NameSet -> CtEvidence
+mk_strict_superclasses :: ExpansionFuel -> NameSet -> CtEvidence
                        -> [TyVar] -> ThetaType
                        -> Class -> [Type] -> TcS [Ct]
 -- Always return the immediate superclasses of (cls tys);
 -- and expand their superclasses, provided none of them are in rec_clss
 -- nor are repeated
-mk_strict_superclasses rec_clss (CtGiven { ctev_evar = evar, ctev_loc = loc })
+-- The caller of this function is supposed to perform fuel book keeping
+-- Precondition: fuel >= 0
+mk_strict_superclasses fuel rec_clss (CtGiven { ctev_evar = evar, ctev_loc = loc })
                        tvs theta cls tys
   = concatMapM do_one_given $
     classSCSelIds cls
@@ -543,7 +560,8 @@ mk_strict_superclasses rec_clss (CtGiven { ctev_evar = evar, ctev_loc = loc })
       | otherwise
       = do { given_ev <- newGivenEvVar sc_loc $
                          mk_given_desc sel_id sc_pred
-           ; mk_superclasses rec_clss given_ev tvs theta sc_pred }
+           ; assertFuelPrecondition fuel
+             $ mk_superclasses fuel rec_clss given_ev tvs theta sc_pred }
       where
         sc_pred = classMethodInstTy sel_id tys
 
@@ -604,7 +622,7 @@ mk_strict_superclasses rec_clss (CtGiven { ctev_evar = evar, ctev_loc = loc })
     newly_blocked (InstSkol _ head_size) = isJust (this_size `ltPatersonSize` head_size)
     newly_blocked _                      = False
 
-mk_strict_superclasses rec_clss ev tvs theta cls tys
+mk_strict_superclasses fuel rec_clss ev tvs theta cls tys
   | all noFreeVarsOfType tys
   = return [] -- Wanteds with no variables yield no superclass constraints.
               -- See Note [Improvement from Ground Wanteds]
@@ -619,7 +637,7 @@ mk_strict_superclasses rec_clss ev tvs theta cls tys
     do_one sc_pred
       = do { traceTcS "mk_strict_superclasses Wanted" (ppr (mkClassPred cls tys) $$ ppr sc_pred)
            ; sc_ev <- newWantedNC loc (ctEvRewriters ev) sc_pred
-           ; mk_superclasses rec_clss sc_ev [] [] sc_pred }
+           ; mk_superclasses fuel rec_clss sc_ev [] [] sc_pred }
 
 {- Note [Improvement from Ground Wanteds]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -634,46 +652,53 @@ dependencies.  See Note [Why adding superclasses can help] above.
 But no variables means no improvement; case closed.
 -}
 
-mk_superclasses :: NameSet -> CtEvidence
+mk_superclasses :: ExpansionFuel -> NameSet -> CtEvidence
                 -> [TyVar] -> ThetaType -> PredType -> TcS [Ct]
 -- Return this constraint, plus its superclasses, if any
-mk_superclasses rec_clss ev tvs theta pred
+-- Precondition: fuel >= 0
+mk_superclasses fuel rec_clss ev tvs theta pred
   | ClassPred cls tys <- classifyPredType pred
-  = mk_superclasses_of rec_clss ev tvs theta cls tys
+  = assertFuelPrecondition fuel $
+    mk_superclasses_of fuel rec_clss ev tvs theta cls tys
 
   | otherwise   -- Superclass is not a class predicate
   = return [mkNonCanonical ev]
 
-mk_superclasses_of :: NameSet -> CtEvidence
+mk_superclasses_of :: ExpansionFuel -> NameSet -> CtEvidence
                    -> [TyVar] -> ThetaType -> Class -> [Type]
                    -> TcS [Ct]
 -- Always return this class constraint,
 -- and expand its superclasses
-mk_superclasses_of rec_clss ev tvs theta cls tys
+-- Precondition: fuel >= 0
+mk_superclasses_of fuel rec_clss ev tvs theta cls tys
   | loop_found = do { traceTcS "mk_superclasses_of: loop" (ppr cls <+> ppr tys)
-                    ; return [this_ct] }  -- cc_pend_sc of this_ct = True
+                    ; assertFuelPrecondition fuel $ return [mk_this_ct fuel] }
+                                                  -- cc_pend_sc of returning ct = fuel
   | otherwise  = do { traceTcS "mk_superclasses_of" (vcat [ ppr cls <+> ppr tys
                                                           , ppr (isCTupleClass cls)
                                                           , ppr rec_clss
                                                           ])
-                    ; sc_cts <- mk_strict_superclasses rec_clss' ev tvs theta cls tys
-                    ; return (this_ct : sc_cts) }
-                                   -- cc_pend_sc of this_ct = False
+                    ; sc_cts <- assertFuelPrecondition fuel $
+                                mk_strict_superclasses fuel rec_clss' ev tvs theta cls tys
+                    ; return (mk_this_ct doNotExpand : sc_cts) }
+                                      -- doNotExpand: we have expanded this cls's superclasses, so
+                                      -- exhaust the associated constraint's fuel,
+                                      -- to avoid duplicate work
   where
     cls_nm     = className cls
     loop_found = not (isCTupleClass cls) && cls_nm `elemNameSet` rec_clss
                  -- Tuples never contribute to recursion, and can be nested
     rec_clss'  = rec_clss `extendNameSet` cls_nm
-
-    this_ct | null tvs, null theta
-            = CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys
-                       , cc_pend_sc = loop_found }
-                 -- NB: If there is a loop, we cut off, so we have not
-                 --     added the superclasses, hence cc_pend_sc = True
-            | otherwise
-            = CQuantCan (QCI { qci_tvs = tvs, qci_pred = mkClassPred cls tys
-                             , qci_ev = ev
-                             , qci_pend_sc = loop_found })
+    mk_this_ct :: ExpansionFuel -> Ct
+    mk_this_ct fuel | null tvs, null theta
+                    = CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys
+                               , cc_pend_sc = fuel }
+                    -- NB: If there is a loop, we cut off, so we have not
+                    --     added the superclasses, hence cc_pend_sc = fuel
+                    | otherwise
+                    = CQuantCan (QCI { qci_tvs = tvs, qci_pred = mkClassPred cls tys
+                                     , qci_ev = ev
+                                     , qci_pend_sc = fuel })
 
 
 {- Note [Equality superclasses in quantified constraints]
@@ -828,19 +853,28 @@ canForAllNC :: CtEvidence -> [TyVar] -> TcThetaType -> TcPredType
 canForAllNC ev tvs theta pred
   | isGiven ev  -- See Note [Eagerly expand given superclasses]
   , Just (cls, tys) <- cls_pred_tys_maybe
-  = do { sc_cts <- mkStrictSuperClasses ev tvs theta cls tys
+  = do { dflags <- getDynFlags
+       ; sc_cts <- mkStrictSuperClasses (givensFuel dflags) ev tvs theta cls tys
+       -- givensFuel dflags: See Note [Expanding Recursive Superclasses and ExpansionFuel]
        ; emitWork sc_cts
-       ; canForAll ev False }
+       ; canForAll ev doNotExpand }
+       -- doNotExpand: as we have already (eagerly) expanded superclasses for this class
 
   | otherwise
-  = canForAll ev (isJust cls_pred_tys_maybe)
-
+  = do { dflags <- getDynFlags
+       ; let fuel | Just (cls, _) <- cls_pred_tys_maybe
+                  , classHasSCs cls = qcsFuel dflags
+                  -- See invariants (a) and (b) in QCI.qci_pend_sc
+                  -- qcsFuel dflags: See Note [Expanding Recursive Superclasses and ExpansionFuel]
+                  -- See Note [Quantified constraints]
+                  | otherwise = doNotExpand
+       ; canForAll ev fuel }
   where
     cls_pred_tys_maybe = getClassPredTys_maybe pred
 
-canForAll :: CtEvidence -> Bool -> TcS (StopOrContinue Ct)
+canForAll :: CtEvidence -> ExpansionFuel -> TcS (StopOrContinue Ct)
 -- We have a constraint (forall as. blah => C tys)
-canForAll ev pend_sc
+canForAll ev fuel
   = do { -- First rewrite it to apply the current substitution
          let pred = ctEvPred ev
        ; (redn, rewriters) <- rewrite ev pred
@@ -850,14 +884,14 @@ canForAll ev pend_sc
          -- (It takes a lot less code to rewrite before decomposing.)
        ; case classifyPredType (ctEvPred new_ev) of
            ForAllPred tvs theta pred
-              -> solveForAll new_ev tvs theta pred pend_sc
+              -> solveForAll new_ev tvs theta pred fuel
            _  -> pprPanic "canForAll" (ppr new_ev)
     } }
 
-solveForAll :: CtEvidence -> [TyVar] -> TcThetaType -> PredType -> Bool
+solveForAll :: CtEvidence -> [TyVar] -> TcThetaType -> PredType -> ExpansionFuel
             -> TcS (StopOrContinue Ct)
 solveForAll ev@(CtWanted { ctev_dest = dest, ctev_rewriters = rewriters, ctev_loc = loc })
-            tvs theta pred _pend_sc
+            tvs theta pred _fuel
   = -- See Note [Solving a Wanted forall-constraint]
     setLclEnv (ctLocEnv loc) $
     -- This setLclEnv is important: the emitImplicationTcS uses that
@@ -903,12 +937,12 @@ solveForAll ev@(CtWanted { ctev_dest = dest, ctev_rewriters = rewriters, ctev_lo
                       _                 -> pSizeType pred
 
  -- See Note [Solving a Given forall-constraint]
-solveForAll ev@(CtGiven {}) tvs _theta pred pend_sc
+solveForAll ev@(CtGiven {}) tvs _theta pred fuel
   = do { addInertForAll qci
        ; stopWith ev "Given forall-constraint" }
   where
     qci = QCI { qci_ev = ev, qci_tvs = tvs
-              , qci_pred = pred, qci_pend_sc = pend_sc }
+              , qci_pred = pred, qci_pend_sc = fuel }
 
 {- Note [Solving a Wanted forall-constraint]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs
index ad4e10ebf6..5fdd4df702 100644
--- a/compiler/GHC/Tc/Solver/Monad.hs
+++ b/compiler/GHC/Tc/Solver/Monad.hs
@@ -513,10 +513,13 @@ getInertGivens
        ; return (filter isGivenCt all_cts) }
 
 getPendingGivenScs :: TcS [Ct]
--- Find all inert Given dictionaries, or quantified constraints,
---     whose cc_pend_sc flag is True
---     and that belong to the current level
--- Set their cc_pend_sc flag to False in the inert set, and return that Ct
+-- Find all inert Given dictionaries, or quantified constraints, such that
+--     1. cc_pend_sc flag has fuel strictly > 0
+--     2. belongs to the current level
+-- For each such dictionary:
+-- * Return it (with unmodified cc_pend_sc) in sc_pending
+-- * Modify the dict in the inert set to have cc_pend_sc = doNotExpand
+--   to record that we have expanded superclasses for this dict
 getPendingGivenScs = do { lvl <- getTcLevel
                         ; updRetInertCans (get_sc_pending lvl) }
 
@@ -530,29 +533,33 @@ get_sc_pending this_lvl ic@(IC { inert_dicts = dicts, inert_insts = insts })
     sc_pending = sc_pend_insts ++ sc_pend_dicts
 
     sc_pend_dicts = foldDicts get_pending dicts []
-    dicts' = foldr add dicts sc_pend_dicts
+    dicts' = foldr exhaustAndAdd dicts sc_pend_dicts
 
     (sc_pend_insts, insts') = mapAccumL get_pending_inst [] insts
 
-    get_pending :: Ct -> [Ct] -> [Ct]  -- Get dicts with cc_pend_sc = True
-                                       -- but flipping the flag
+    get_pending :: Ct -> [Ct] -> [Ct]  -- Get dicts with cc_pend_sc > 0
     get_pending dict dicts
-        | Just dict' <- pendingScDict_maybe dict
+        | isPendingScDict dict
         , belongs_to_this_level (ctEvidence dict)
-        = dict' : dicts
+        = dict : dicts
         | otherwise
         = dicts
 
-    add :: Ct -> DictMap Ct -> DictMap Ct
-    add ct@(CDictCan { cc_class = cls, cc_tyargs = tys }) dicts
-        = addDict dicts cls tys ct
-    add ct _ = pprPanic "getPendingScDicts" (ppr ct)
+    exhaustAndAdd :: Ct -> DictMap Ct -> DictMap Ct
+    exhaustAndAdd ct@(CDictCan { cc_class = cls, cc_tyargs = tys }) dicts
+    -- exhaust the fuel for this constraint before adding it as
+    -- we don't want to expand these constraints again
+        = addDict dicts cls tys (ct {cc_pend_sc = doNotExpand})
+    exhaustAndAdd ct _ = pprPanic "getPendingScDicts" (ppr ct)
 
     get_pending_inst :: [Ct] -> QCInst -> ([Ct], QCInst)
     get_pending_inst cts qci@(QCI { qci_ev = ev })
        | Just qci' <- pendingScInst_maybe qci
        , belongs_to_this_level ev
-       = (CQuantCan qci' : cts, qci')
+       = (CQuantCan qci : cts, qci')
+       -- qci' have their fuel exhausted
+       -- we don't want to expand these constraints again
+       -- qci is expanded
        | otherwise
        = (cts, qci)
 
diff --git a/compiler/GHC/Tc/Types/Constraint.hs b/compiler/GHC/Tc/Types/Constraint.hs
index bd66282b24..d10c4394f6 100644
--- a/compiler/GHC/Tc/Types/Constraint.hs
+++ b/compiler/GHC/Tc/Types/Constraint.hs
@@ -11,6 +11,8 @@ module GHC.Tc.Types.Constraint (
 
         -- Canonical constraints
         Xi, Ct(..), Cts,
+        ExpansionFuel, doNotExpand, consumeFuel, pendingFuel,
+        assertFuelPrecondition, assertFuelPreconditionStrict,
         emptyCts, andCts, andManyCts, pprCts,
         singleCt, listToCts, ctsElts, consCts, snocCts, extendCtsList,
         isEmptyCts,
@@ -138,8 +140,6 @@ import Data.Word  ( Word8 )
 import Data.List  ( intersperse )
 
 
-
-
 {-
 ************************************************************************
 *                                                                      *
@@ -191,6 +191,37 @@ type Xi = TcType
 
 type Cts = Bag Ct
 
+-- | Says how many layers of superclasses can we expand.
+--   Invariant: ExpansionFuel should always be >= 0
+-- see Note [Expanding Recursive Superclasses and ExpansionFuel]
+type ExpansionFuel = Int
+
+-- | Do not expand superclasses any further
+doNotExpand :: ExpansionFuel
+doNotExpand = 0
+
+-- | Consumes one unit of fuel.
+--   Precondition: fuel > 0
+consumeFuel :: ExpansionFuel -> ExpansionFuel
+consumeFuel fuel = assertFuelPreconditionStrict fuel $ fuel - 1
+
+-- | Returns True if we have any fuel left for superclass expansion
+pendingFuel :: ExpansionFuel -> Bool
+pendingFuel n = n > 0
+
+insufficientFuelError :: SDoc
+insufficientFuelError = text "Superclass expansion fuel should be > 0"
+
+-- | asserts if fuel is non-negative
+assertFuelPrecondition :: ExpansionFuel -> a -> a
+{-# INLINE assertFuelPrecondition #-}
+assertFuelPrecondition fuel = assertPpr (fuel >= 0) insufficientFuelError
+
+-- | asserts if fuel is strictly greater than 0
+assertFuelPreconditionStrict :: ExpansionFuel -> a -> a
+{-# INLINE assertFuelPreconditionStrict #-}
+assertFuelPreconditionStrict fuel = assertPpr (pendingFuel fuel) insufficientFuelError
+
 data Ct
   -- Atomic canonical constraints
   = CDictCan {  -- e.g.  Num ty
@@ -199,11 +230,12 @@ data Ct
       cc_class  :: Class,
       cc_tyargs :: [Xi],   -- cc_tyargs are rewritten w.r.t. inerts, so Xi
 
-      cc_pend_sc :: Bool
+      cc_pend_sc :: ExpansionFuel
           -- See Note [The superclass story] in GHC.Tc.Solver.Canonical
-          -- True <=> (a) cc_class has superclasses
-          --          (b) we have not (yet) added those
-          --              superclasses as Givens
+          -- See Note [Expanding Recursive Superclasses and ExpansionFuel] in GHC.Tc.Solver
+          -- Invariants: cc_pend_sc > 0 <=>
+          --                    (a) cc_class has superclasses
+          --                    (b) those superclasses are not yet explored
     }
 
   | CIrredCan {  -- These stand for yet-unusable predicates
@@ -273,8 +305,13 @@ data QCInst  -- A much simplified version of ClsInst
                                  -- Always Given
         , qci_tvs  :: [TcTyVar]  -- The tvs
         , qci_pred :: TcPredType -- The ty
-        , qci_pend_sc :: Bool    -- Same as cc_pend_sc flag in CDictCan
-                                 -- Invariant: True => qci_pred is a ClassPred
+        , qci_pend_sc :: ExpansionFuel
+             -- Invariants: qci_pend_sc > 0 =>
+             --       (a) qci_pred is a ClassPred
+             --       (b) this class has superclass(es), and
+             --       (c) the superclass(es) are not explored yet
+             -- Same as cc_pend_sc flag in CDictCan
+             -- See Note [Expanding Recursive Superclasses and ExpansionFuel] in GHC.Tc.Solver
     }
 
 instance Outputable QCInst where
@@ -673,11 +710,11 @@ instance Outputable Ct where
          CEqCan {}        -> text "CEqCan"
          CNonCanonical {} -> text "CNonCanonical"
          CDictCan { cc_pend_sc = psc }
-            | psc          -> text "CDictCan(psc)"
-            | otherwise    -> text "CDictCan"
+            | psc > 0       -> text "CDictCan" <> parens (text "psc" <+> ppr psc)
+            | otherwise     -> text "CDictCan"
          CIrredCan { cc_reason = reason } -> text "CIrredCan" <> ppr reason
-         CQuantCan (QCI { qci_pend_sc = pend_sc })
-            | pend_sc   -> text "CQuantCan(psc)"
+         CQuantCan (QCI { qci_pend_sc = psc })
+            | psc > 0  -> text "CQuantCan"  <> parens (text "psc" <+> ppr psc)
             | otherwise -> text "CQuantCan"
 
 -----------------------------------
@@ -893,23 +930,24 @@ isUserTypeError pred = case getUserTypeErrorMsg pred of
                              _      -> False
 
 isPendingScDict :: Ct -> Bool
-isPendingScDict (CDictCan { cc_pend_sc = psc }) = psc
--- Says whether this is a CDictCan with cc_pend_sc is True;
+isPendingScDict (CDictCan { cc_pend_sc = f }) = pendingFuel f
+-- Says whether this is a CDictCan with cc_pend_sc has positive fuel;
 -- 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
-pendingScDict_maybe ct@(CDictCan { cc_pend_sc = True })
-                      = Just (ct { cc_pend_sc = False })
+-- Says whether this is a CDictCan with cc_pend_sc has fuel left,
+-- AND if so exhausts the fuel so that they are not expanded again
+pendingScDict_maybe ct@(CDictCan { cc_pend_sc = f })
+  | pendingFuel f = Just (ct { cc_pend_sc = doNotExpand })
+  | otherwise     = Nothing
 pendingScDict_maybe _ = Nothing
 
 pendingScInst_maybe :: QCInst -> Maybe QCInst
 -- Same as isPendingScDict, but for QCInsts
-pendingScInst_maybe qci@(QCI { qci_pend_sc = True })
-                      = Just (qci { qci_pend_sc = False })
-pendingScInst_maybe _ = Nothing
+pendingScInst_maybe qci@(QCI { qci_pend_sc = f })
+  | pendingFuel f = Just (qci { qci_pend_sc = doNotExpand })
+  | otherwise     = Nothing
 
 superClassesMightHelp :: WantedConstraints -> Bool
 -- ^ True if taking superclasses of givens, or of wanteds (to perhaps
@@ -928,11 +966,12 @@ superClassesMightHelp (WC { wc_simple = simples, wc_impl = implics })
     is_ip _                             = False
 
 getPendingWantedScs :: Cts -> ([Ct], Cts)
+-- in the return values [Ct] has original fuel while Cts has fuel exhausted
 getPendingWantedScs simples
   = mapAccumBagL get [] simples
   where
-    get acc ct | Just ct' <- pendingScDict_maybe ct
-               = (ct':acc, ct')
+    get acc ct | Just ct_exhausted <- pendingScDict_maybe ct
+               = (ct:acc, ct_exhausted)
                | otherwise
                = (acc,     ct)
 
diff --git a/docs/users_guide/expected-undocumented-flags.txt b/docs/users_guide/expected-undocumented-flags.txt
index 1e8cd4f4cc..6fa3f2f27d 100644
--- a/docs/users_guide/expected-undocumented-flags.txt
+++ b/docs/users_guide/expected-undocumented-flags.txt
@@ -33,6 +33,9 @@
 -fbang-patterns
 -fbuilding-cabal-package
 -fconstraint-solver-iterations
+-fgivens-expansion-fuel
+-fwanteds-expansion-fuel
+-fqcs-expansion-fuel
 -fcontext-stack
 -fcross-module-specialize
 -fdiagnostics-color=always
diff --git a/testsuite/tests/typecheck/should_compile/T21909.hs b/testsuite/tests/typecheck/should_compile/T21909.hs
new file mode 100644
index 0000000000..2485134703
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T21909.hs
@@ -0,0 +1,24 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
+
+module T21909 where
+
+import Data.Kind
+
+class (Monad m, MyMonad (Inner m)) => MyMonad m where
+  type Inner m :: Type -> Type
+  foo :: m Int
+
+works :: MyMonad m => m String
+works = show <$> ((+ 1) <$> foo)
+
+fails :: MyMonad m => m String
+fails = show <$> fooPlusOne
+  where
+    fooPlusOne = (+ 1) <$> foo
+
+alsoFails :: MyMonad m => m String
+alsoFails =
+  let fooPlusOne = (+ 1) <$> foo
+   in show <$> fooPlusOne
diff --git a/testsuite/tests/typecheck/should_compile/T21909b.hs b/testsuite/tests/typecheck/should_compile/T21909b.hs
new file mode 100644
index 0000000000..3e02ae45f5
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T21909b.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE UndecidableSuperClasses, FunctionalDependencies, MultiParamTypeClasses, GADTs #-}
+
+module T21909b where
+
+class C [a] => C a where
+  foo :: a -> Int
+
+bar :: C a => a -> Int
+bar x = foolocal x
+  where
+    foolocal a = foo a
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 2c6debc98f..327dd93675 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -864,3 +864,5 @@ test('T22924', normal, compile, [''])
 test('T22985a', normal, compile, ['-O'])
 test('T22985b', normal, compile, [''])
 test('T23018', normal, compile, [''])
+test('T21909', normal, compile, [''])
+test('T21909b', normal, compile, [''])
\ No newline at end of file