Introduce warning for loopy superclass solve

Commit aed1974e completely re-engineered the treatment of loopy
superclass dictionaries in instance declarations. Unfortunately,
it has the potential to break (albeit in a rather minor way) user code.

To alleviate migration concerns, this commit re-introduces the old
behaviour. Any reliance on this old behaviour triggers a warning,
controlled by `-Wloopy-superclass-solve`. The warning text explains
that GHC might produce bottoming evidence, and provides a migration
strategy.

This allows us to provide a graceful migration period, alerting users
when they are relying on this unsound behaviour.

Fixes #22912 #22891 #20666 #22894 #22905

26 files changed, 342 insertions, 100 deletions

diff --git a/compiler/GHC/Driver/Flags.hs b/compiler/GHC/Driver/Flags.hs
index 982d2e2f45..756d75f630 100644
--- a/compiler/GHC/Driver/Flags.hs
+++ b/compiler/GHC/Driver/Flags.hs
@@ -631,6 +631,7 @@ data WarningFlag =
    | Opt_WarnGADTMonoLocalBinds                      -- Since 9.4
    | Opt_WarnTypeEqualityOutOfScope                  -- Since 9.4
    | Opt_WarnTypeEqualityRequiresOperators           -- Since 9.4
+   | Opt_WarnLoopySuperclassSolve                    -- Since 9.6
    | Opt_WarnTermVariableCapture                     -- Since 9.8
    deriving (Eq, Ord, Show, Enum)
 
@@ -737,6 +738,7 @@ warnFlagNames wflag = case wflag of
   Opt_WarnUnicodeBidirectionalFormatCharacters    -> "unicode-bidirectional-format-characters" :| []
   Opt_WarnGADTMonoLocalBinds                      -> "gadt-mono-local-binds" :| []
   Opt_WarnTypeEqualityOutOfScope                  -> "type-equality-out-of-scope" :| []
+  Opt_WarnLoopySuperclassSolve                    -> "loopy-superclass-solve" :| []
   Opt_WarnTypeEqualityRequiresOperators           -> "type-equality-requires-operators" :| []
 
 -- -----------------------------------------------------------------------------
@@ -853,6 +855,7 @@ standardWarnings -- see Note [Documenting warning flags]
         Opt_WarnForallIdentifier,
         Opt_WarnUnicodeBidirectionalFormatCharacters,
         Opt_WarnGADTMonoLocalBinds,
+        Opt_WarnLoopySuperclassSolve,
         Opt_WarnTypeEqualityRequiresOperators
       ]
 
diff --git a/compiler/GHC/Tc/Errors/Ppr.hs b/compiler/GHC/Tc/Errors/Ppr.hs
index 9880c13a9c..10d1c60fb1 100644
--- a/compiler/GHC/Tc/Errors/Ppr.hs
+++ b/compiler/GHC/Tc/Errors/Ppr.hs
@@ -8,6 +8,7 @@
 {-# LANGUAGE TypeFamilies #-}
 
 {-# OPTIONS_GHC -fno-warn-orphans #-} -- instance Diagnostic TcRnMessage
+{-# LANGUAGE InstanceSigs #-}
 
 module GHC.Tc.Errors.Ppr
   ( pprTypeDoesNotHaveFixedRuntimeRep
@@ -1305,7 +1306,18 @@ instance Diagnostic TcRnMessage where
            , text "Combine alternative minimal complete definitions with `|'" ]
       where
         sigs = sig1 : sig2 : otherSigs
-
+    TcRnLoopySuperclassSolve wtd_loc wtd_pty ->
+      mkSimpleDecorated $ vcat [ header, warning, user_manual ]
+      where
+        header, warning, user_manual :: SDoc
+        header
+          = vcat [ text "I am solving the constraint" <+> quotes (ppr wtd_pty) <> comma
+                 , nest 2 $ pprCtOrigin (ctLocOrigin wtd_loc) <> comma
+                 , text "in a way that might turn out to loop at runtime." ]
+        warning
+          = vcat [ text "Future versions of GHC will turn this warning into an error." ]
+        user_manual =
+          vcat [ text "See the user manual, § Undecidable instances and loopy superclasses." ]
 
   diagnosticReason = \case
     TcRnUnknownMessage m
@@ -1734,6 +1746,8 @@ instance Diagnostic TcRnMessage where
       -> ErrorWithoutFlag
     TcRnDuplicateMinimalSig{}
       -> ErrorWithoutFlag
+    TcRnLoopySuperclassSolve{}
+      -> WarningWithFlag Opt_WarnLoopySuperclassSolve
 
   diagnosticHints = \case
     TcRnUnknownMessage m
@@ -2173,6 +2187,13 @@ instance Diagnostic TcRnMessage where
       -> noHints
     TcRnDuplicateMinimalSig{}
       -> noHints
+    TcRnLoopySuperclassSolve wtd_loc wtd_pty
+      -> [LoopySuperclassSolveHint wtd_pty cls_or_qc]
+      where
+        cls_or_qc :: ClsInstOrQC
+        cls_or_qc = case ctLocOrigin wtd_loc of
+          ScOrigin c_or_q _ -> c_or_q
+          _                 -> IsClsInst -- shouldn't happen
 
   diagnosticCode = constructorCode
 
diff --git a/compiler/GHC/Tc/Errors/Types.hs b/compiler/GHC/Tc/Errors/Types.hs
index c1b8461839..e2707b4aa4 100644
--- a/compiler/GHC/Tc/Errors/Types.hs
+++ b/compiler/GHC/Tc/Errors/Types.hs
@@ -2924,6 +2924,23 @@ data TcRnMessage where
   -}
   TcRnDuplicateMinimalSig :: LSig GhcPs -> LSig GhcPs -> [LSig GhcPs] -> TcRnMessage
 
+  {-| TcRnLoopySuperclassSolve is a warning, controlled by @-Wloopy-superclass-solve@,
+      that is triggered when GHC solves a constraint in a possibly-loopy way,
+      violating the class instance termination rules described in the section
+      "Undecidable instances and loopy superclasses" of the user's guide.
+
+      Example:
+
+        class Foo f
+        class Foo f => Bar f g
+        instance Bar f f => Bar f (h k)
+
+      Test cases: T20666, T20666{a,b}, T22891, T22912.
+  -}
+  TcRnLoopySuperclassSolve :: CtLoc    -- ^ Wanted 'CtLoc'
+                           -> PredType -- ^ Wanted 'PredType'
+                           -> TcRnMessage
+
   deriving Generic
 
 -- | Things forbidden in @type data@ declarations.
diff --git a/compiler/GHC/Tc/Solver/InertSet.hs b/compiler/GHC/Tc/Solver/InertSet.hs
index 5dc3431b9a..60b422e1fc 100644
--- a/compiler/GHC/Tc/Solver/InertSet.hs
+++ b/compiler/GHC/Tc/Solver/InertSet.hs
@@ -1633,10 +1633,17 @@ mightEqualLater inert_set given_pred given_loc wanted_pred wanted_loc
       = False
     can_unify lhs_tv _other _rhs_ty = mentions_meta_ty_var lhs_tv
 
-prohibitedSuperClassSolve :: CtLoc    -- ^ is it loopy to use this one ...
-                          -> CtLoc    -- ^ ... to solve this one?
-                          -> Bool     -- ^ True ==> don't solve it
--- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance, (sc2)
+-- | Is it (potentially) loopy to use the first @ct1@ to solve @ct2@?
+--
+-- Necessary (but not sufficient) conditions for this function to return @True@:
+--
+--   - @ct1@ and @ct2@ both arise from superclass expansion,
+--   - @ct1@ is a Given and @ct2@ is a Wanted.
+--
+-- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance, (sc2).
+prohibitedSuperClassSolve :: CtLoc -- ^ is it loopy to use this one ...
+                          -> CtLoc -- ^ ... to solve this one?
+                          -> Bool  -- ^ True ==> don't solve it
 prohibitedSuperClassSolve given_loc wanted_loc
   | GivenSCOrigin _ _ blocked <- ctLocOrigin given_loc
   , blocked
diff --git a/compiler/GHC/Tc/Solver/Interact.hs b/compiler/GHC/Tc/Solver/Interact.hs
index e69e7ae0fe..df53e39fcd 100644
--- a/compiler/GHC/Tc/Solver/Interact.hs
+++ b/compiler/GHC/Tc/Solver/Interact.hs
@@ -449,7 +449,7 @@ instance Outputable InteractResult where
 
 solveOneFromTheOther :: Ct  -- Inert    (Dict or Irred)
                      -> Ct  -- WorkItem (same predicate as inert)
-                     -> TcS InteractResult
+                     -> InteractResult
 -- Precondition:
 -- * inert and work item represent evidence for the /same/ predicate
 -- * Both are CDictCan or CIrredCan
@@ -461,28 +461,28 @@ solveOneFromTheOther :: Ct  -- Inert    (Dict or Irred)
 solveOneFromTheOther ct_i ct_w
   | CtWanted { ctev_loc = loc_w } <- ev_w
   , prohibitedSuperClassSolve loc_i loc_w
+  -- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance
   = -- Inert must be Given
-    do { traceTcS "prohibitedClassSolve1" (ppr ev_i $$ ppr ev_w)
-       ; return KeepWork }
+    KeepWork
 
   | CtWanted {} <- ev_w
   = -- Inert is Given or Wanted
     case ev_i of
-      CtGiven {} -> return KeepInert
+      CtGiven {} -> 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
+        | not is_psc_i, is_psc_w     -> KeepInert
+        | is_psc_i,     not is_psc_w -> 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
+        | not is_wsc_orig_i, is_wsc_orig_w     -> KeepInert
+        | is_wsc_orig_i,     not is_wsc_orig_w -> KeepWork
 
         -- otherwise, just choose the lower span
         -- reason: if we have something like (abs 1) (where the
@@ -490,29 +490,28 @@ solveOneFromTheOther ct_i ct_w
         -- 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
+        | ((<) `on` ctLocSpan) loc_i loc_w -> KeepInert
+        | otherwise                        -> KeepWork
 
   -- From here on the work-item is Given
 
   | CtWanted { ctev_loc = loc_i } <- ev_i
   , prohibitedSuperClassSolve loc_w loc_i
-  = do { traceTcS "prohibitedClassSolve2" (ppr ev_i $$ ppr ev_w)
-       ; return KeepInert }      -- Just discard the un-usable Given
-                                 -- This never actually happens because
-                                 -- Givens get processed first
+  = KeepInert   -- Just discard the un-usable Given
+                -- This never actually happens because
+                -- Givens get processed first
 
   | CtWanted {} <- ev_i
-  = return KeepWork
+  = KeepWork
 
   -- From here on both are Given
   -- See Note [Replacement vs keeping]
 
   | lvl_i == lvl_w
-  = return same_level_strategy
+  = same_level_strategy
 
   | otherwise   -- Both are Given, levels differ
-  = return different_level_strategy
+  = different_level_strategy
   where
      ev_i  = ctEvidence ct_i
      ev_w  = ctEvidence ct_w
@@ -662,14 +661,12 @@ interactIrred inerts ct_w@(CIrredCan { cc_ev = ev_w, cc_reason = reason })
   , ((ct_i, swap) : _rest) <- bagToList matching_irreds
         -- See Note [Multiple matching irreds]
   , let ev_i = ctEvidence ct_i
-  = do { what_next <- solveOneFromTheOther ct_i ct_w
-       ; traceTcS "iteractIrred" $
+  = do { traceTcS "iteractIrred" $
          vcat [ text "wanted:" <+> (ppr ct_w $$ ppr (ctOrigin ct_w))
-              , text "inert: " <+> (ppr ct_i $$ ppr (ctOrigin ct_i))
-              , ppr what_next ]
-       ; case what_next of
+              , text "inert: " <+> (ppr ct_i $$ ppr (ctOrigin ct_i)) ]
+       ; case solveOneFromTheOther ct_i ct_w of
             KeepInert -> do { setEvBindIfWanted ev_w (swap_me swap ev_i)
-                            ; return (Stop ev_w (text "Irred equal" <+> parens (ppr what_next))) }
+                            ; return (Stop ev_w (text "Irred equal:KeepInert" <+> ppr ct_w)) }
             KeepWork ->  do { setEvBindIfWanted ev_i (swap_me swap ev_w)
                             ; updInertIrreds (\_ -> others)
                             ; continueWith ct_w } }
@@ -1007,7 +1004,9 @@ and Given/instance fundeps entirely.
 interactDict :: InertCans -> Ct -> TcS (StopOrContinue Ct)
 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
+  , let ev_i  = ctEvidence ct_i
+        loc_i = ctEvLoc ev_i
+        loc_w = ctEvLoc ev_w
   = -- There is a matching dictionary in the inert set
     do { -- First to try to solve it /completely/ from top level instances
          -- See Note [Shortcut solving]
@@ -1015,16 +1014,24 @@ interactDict inerts ct_w@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs = t
        ; short_cut_worked <- shortCutSolver dflags ev_w ev_i
        ; if short_cut_worked
          then stopWith ev_w "interactDict/solved from instance"
-         else
 
-    do { -- Ths short-cut solver didn't fire, so we
-         -- solve ev_w from the matching inert ev_i we found
-         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)
+         -- Next see if we are in "loopy-superclass" land.  If so,
+         -- we don't want to replace the (Given) inert with the
+         -- (Wanted) work-item, or vice versa; we want to hang on
+         -- to both, and try to solve the work-item via an instance.
+         -- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance
+         else if prohibitedSuperClassSolve loc_i loc_w
+         then continueWith ct_w
+         else
+    do { -- The short-cut solver didn't fire, and loopy superclasses
+         -- are dealt with, so we can either solve
+         -- the inert from the work-item or vice-versa.
+       ; case solveOneFromTheOther ct_i ct_w of
+           KeepInert -> do { traceTcS "lookupInertDict:KeepInert" (ppr ct_w)
+                           ; setEvBindIfWanted ev_w (ctEvTerm ev_i)
+                           ; return $ Stop ev_w (text "Dict equal" <+> ppr ct_w) }
+           KeepWork  -> do { traceTcS "lookupInertDict:KeepWork" (ppr ct_w)
+                           ; setEvBindIfWanted ev_i (ctEvTerm ev_w)
                            ; updInertDicts $ \ ds -> delDict ds cls tys
                            ; continueWith ct_w } } }
 
@@ -1894,7 +1901,7 @@ as the fundeps.
 #7875 is a case in point.
 -}
 
-doTopFundepImprovement :: Ct -> TcS (StopOrContinue Ct)
+doTopFundepImprovement :: Ct -> TcS ()
 -- Try to functional-dependency improvement between the constraint
 -- and the top-level instance declarations
 -- See Note [Fundeps with instances, and equality orientation]
@@ -1904,8 +1911,7 @@ doTopFundepImprovement work_item@(CDictCan { cc_ev = ev, cc_class = cls
   = do { traceTcS "try_fundeps" (ppr work_item)
        ; instEnvs <- getInstEnvs
        ; let fundep_eqns = improveFromInstEnv instEnvs mk_ct_loc cls xis
-       ; emitFunDepWanteds (ctEvRewriters ev) fundep_eqns
-       ; continueWith work_item }
+       ; emitFunDepWanteds (ctEvRewriters ev) fundep_eqns }
   where
      dict_pred   = mkClassPred cls xis
      dict_loc    = ctEvLoc ev
@@ -2276,14 +2282,35 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = ev, cc_class = cls
                         ; chooseInstance work_item lkup_res }
                _  -> -- NoInstance or NotSure
                      -- We didn't solve it; so try functional dependencies with
-                     -- the instance environment, and return
-                     doTopFundepImprovement work_item }
+                     -- the instance environment
+                     do { doTopFundepImprovement work_item
+                        ; tryLastResortProhibitedSuperclass inerts work_item } }
    where
      dict_loc = ctEvLoc ev
 
 
 doTopReactDict _ w = pprPanic "doTopReactDict" (ppr w)
 
+-- | As a last resort, we TEMPORARILY allow a prohibited superclass solve,
+-- emitting a loud warning when doing so: we might be creating non-terminating
+-- evidence (as we are in T22912 for example).
+--
+-- See Note [Migrating away from loopy superclass solving] in GHC.Tc.TyCl.Instance.
+tryLastResortProhibitedSuperclass :: InertSet -> Ct -> TcS (StopOrContinue Ct)
+tryLastResortProhibitedSuperclass inerts
+    work_item@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs = xis })
+  | let loc_w  = ctEvLoc ev_w
+        orig_w = ctLocOrigin loc_w
+  , ScOrigin _ NakedSc <- orig_w   -- work_item is definitely Wanted
+  , Just ct_i <- lookupInertDict (inert_cans inerts) loc_w cls xis
+  , let ev_i = ctEvidence ct_i
+  , isGiven ev_i
+  = do { setEvBindIfWanted ev_w (ctEvTerm ev_i)
+       ; ctLocWarnTcS loc_w $
+         TcRnLoopySuperclassSolve loc_w (ctPred work_item)
+       ; return $ Stop ev_w (text "Loopy superclass") }
+tryLastResortProhibitedSuperclass _ work_item
+  = continueWith work_item
 
 chooseInstance :: Ct -> ClsInstResult -> TcS (StopOrContinue Ct)
 chooseInstance work_item
diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs
index b9a9354eff..7ff59baf4e 100644
--- a/compiler/GHC/Tc/Solver/Monad.hs
+++ b/compiler/GHC/Tc/Solver/Monad.hs
@@ -15,7 +15,7 @@ module GHC.Tc.Solver.Monad (
 
     -- The TcS monad
     TcS, runTcS, runTcSEarlyAbort, runTcSWithEvBinds, runTcSInerts,
-    failTcS, warnTcS, addErrTcS, wrapTcS,
+    failTcS, warnTcS, addErrTcS, wrapTcS, ctLocWarnTcS,
     runTcSEqualities,
     nestTcS, nestImplicTcS, setEvBindsTcS,
     emitImplicationTcS, emitTvImplicationTcS,
@@ -673,16 +673,18 @@ lookupInInerts :: CtLoc -> TcPredType -> TcS (Maybe CtEvidence)
 lookupInInerts loc pty
   | ClassPred cls tys <- classifyPredType pty
   = do { inerts <- getTcSInerts
-       ; return $ -- Maybe monad
-                  do { found_ev <-
-                         lookupSolvedDict inerts loc cls tys `mplus`
-                         fmap ctEvidence (lookupInertDict (inert_cans inerts) loc cls tys)
-                     ; guard (not (prohibitedSuperClassSolve (ctEvLoc found_ev) loc))
-                      -- We're about to "solve" the wanted we're looking up, so we
-                      -- must make sure doing so wouldn't run afoul of
-                      -- Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance.
-                      -- Forgetting this led to #20666.
-                     ; return found_ev }}
+       ; let mb_solved = lookupSolvedDict inerts loc cls tys
+             mb_inert  = fmap ctEvidence (lookupInertDict (inert_cans inerts) loc cls tys)
+       ; return $ do -- Maybe monad
+            found_ev <- mb_solved `mplus` mb_inert
+
+            -- We're about to "solve" the wanted we're looking up, so we
+            -- must make sure doing so wouldn't run afoul of
+            -- Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance.
+            -- Forgetting this led to #20666.
+            guard $ not (prohibitedSuperClassSolve (ctEvLoc found_ev) loc)
+
+            return found_ev }
   | otherwise -- NB: No caching for equalities, IPs, holes, or errors
   = return Nothing
 
@@ -855,6 +857,10 @@ warnTcS msg  = wrapTcS (TcM.addDiagnostic msg)
 addErrTcS    = wrapTcS . TcM.addErr
 panicTcS doc = pprPanic "GHC.Tc.Solver.Canonical" doc
 
+-- | Emit a warning within the 'TcS' monad at the location given by the 'CtLoc'.
+ctLocWarnTcS :: CtLoc -> TcRnMessage -> TcS ()
+ctLocWarnTcS loc msg = wrapTcS $ TcM.setCtLocM loc $ TcM.addDiagnostic msg
+
 traceTcS :: String -> SDoc -> TcS ()
 traceTcS herald doc = wrapTcS (TcM.traceTc herald doc)
 {-# INLINE traceTcS #-}  -- see Note [INLINE conditional tracing utilities]
diff --git a/compiler/GHC/Tc/TyCl/Instance.hs b/compiler/GHC/Tc/TyCl/Instance.hs
index 3d9b5dd550..9213ceeab2 100644
--- a/compiler/GHC/Tc/TyCl/Instance.hs
+++ b/compiler/GHC/Tc/TyCl/Instance.hs
@@ -1661,6 +1661,20 @@ Answer:
     superclass selection, except at a smaller type.  This test is
     implemented by GHC.Tc.Solver.InertSet.prohibitedSuperClassSolve
 
+Note [Migrating away from loopy superclass solving]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The logic from Note [Solving superclass constraints] was implemented in GHC 9.6.
+However, we want to provide a migration strategy for users, to avoid suddenly
+breaking their code going when upgrading to GHC 9.6. To this effect, we temporarily
+continue to allow the constraint solver to create these potentially non-terminating
+solutions, but emit a loud warning when doing so: see
+GHC.Tc.Solver.Interact.tryLastResortProhibitedSuperclass.
+
+Users can silence the warning by manually adding the necessary constraint to the
+context. GHC will then keep this user-written Given, dropping the Given arising
+from superclass expansion which has greater SC depth, as explained in
+Note [Replacement vs keeping] in GHC.Tc.Solver.Interact.
+
 Note [Silent superclass arguments] (historical interest only)
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 NB1: this note describes our *old* solution to the
diff --git a/compiler/GHC/Tc/Types/Origin.hs-boot b/compiler/GHC/Tc/Types/Origin.hs-boot
index eecb8cb490..a84c44cf4a 100644
--- a/compiler/GHC/Tc/Types/Origin.hs-boot
+++ b/compiler/GHC/Tc/Types/Origin.hs-boot
@@ -7,4 +7,8 @@ data SkolemInfo
 data FixedRuntimeRepContext
 data FixedRuntimeRepOrigin
 
+data CtOrigin
+data ClsInstOrQC = IsClsInst
+                 | IsQC CtOrigin
+
 unkSkol :: HasCallStack => SkolemInfo
diff --git a/compiler/GHC/Types/Error/Codes.hs b/compiler/GHC/Types/Error/Codes.hs
index d7b57113ee..bae5e1ccfb 100644
--- a/compiler/GHC/Types/Error/Codes.hs
+++ b/compiler/GHC/Types/Error/Codes.hs
@@ -512,6 +512,7 @@ type family GhcDiagnosticCode c = n | n -> c where
   GhcDiagnosticCode "TcRnUnexpectedDefaultSig"                      = 40700
   GhcDiagnosticCode "TcRnBindInBootFile"                            = 11247
   GhcDiagnosticCode "TcRnDuplicateMinimalSig"                       = 85346
+  GhcDiagnosticCode "TcRnLoopySuperclassSolve"                      = 36038
 
   -- IllegalNewtypeReason
   GhcDiagnosticCode "DoesNotHaveSingleField"                        = 23517
diff --git a/compiler/GHC/Types/Hint.hs b/compiler/GHC/Types/Hint.hs
index 9f897feb7f..654d798ef7 100644
--- a/compiler/GHC/Types/Hint.hs
+++ b/compiler/GHC/Types/Hint.hs
@@ -32,11 +32,13 @@ import GHC.Unit.Module (ModuleName, Module)
 import GHC.Hs.Extension (GhcTc)
 import GHC.Core.Coercion
 import GHC.Core.FamInstEnv (FamFlavor)
+import GHC.Core.Type (PredType)
 import GHC.Types.Fixity (LexicalFixity(..))
 import GHC.Types.Name (Name, NameSpace, OccName (occNameFS), isSymOcc, nameOccName)
 import GHC.Types.Name.Reader (RdrName (Unqual), ImpDeclSpec)
 import GHC.Types.SrcLoc (SrcSpan)
 import GHC.Types.Basic (Activation, RuleName)
+import {-# SOURCE #-} GHC.Tc.Types.Origin ( ClsInstOrQC(..) )
 import GHC.Parser.Errors.Basic
 import {-# SOURCE #-} Language.Haskell.Syntax.Expr
 import GHC.Unit.Module.Imported (ImportedModsVal)
@@ -429,6 +431,8 @@ data GhcHint
     -}
   | SuggestRenameTypeVariable
 
+  | LoopySuperclassSolveHint PredType ClsInstOrQC
+
 -- | An 'InstantiationSuggestion' for a '.hsig' file. This is generated
 -- by GHC in case of a 'DriverUnexpectedSignature' and suggests a way
 -- to instantiate a particular signature, where the first argument is
diff --git a/compiler/GHC/Types/Hint/Ppr.hs b/compiler/GHC/Types/Hint/Ppr.hs
index 96fbd9f74f..32e1b38bb2 100644
--- a/compiler/GHC/Types/Hint/Ppr.hs
+++ b/compiler/GHC/Types/Hint/Ppr.hs
@@ -14,6 +14,7 @@ import GHC.Types.Hint
 
 import GHC.Core.FamInstEnv (FamFlavor(..))
 import GHC.Hs.Expr ()   -- instance Outputable
+import {-# SOURCE #-} GHC.Tc.Types.Origin ( ClsInstOrQC(..) )
 import GHC.Types.Id
 import GHC.Types.Name (NameSpace, pprDefinedAt, occNameSpace, pprNameSpace, isValNameSpace, nameModule)
 import GHC.Types.Name.Reader (RdrName,ImpDeclSpec (..), rdrNameOcc, rdrNameSpace)
@@ -214,6 +215,14 @@ instance Outputable GhcHint where
            mod = nameModule name
     SuggestRenameTypeVariable
       -> text "Consider renaming the type variable."
+    LoopySuperclassSolveHint pty cls_or_qc
+      -> vcat [ text "Add the constraint" <+> quotes (ppr pty) <+> text "to the" <+> what <> comma
+              , text "even though it seems logically implied by other constraints in the context." ]
+        where
+          what :: SDoc
+          what = case cls_or_qc of
+            IsClsInst -> text "instance context"
+            IsQC {}   -> text "context of the quantified constraint"
 
 perhapsAsPat :: SDoc
 perhapsAsPat = text "Perhaps you meant an as-pattern, which must not be surrounded by whitespace"
diff --git a/docs/users_guide/9.6.1-notes.rst b/docs/users_guide/9.6.1-notes.rst
index 34e7723092..36067df41c 100644
--- a/docs/users_guide/9.6.1-notes.rst
+++ b/docs/users_guide/9.6.1-notes.rst
@@ -3,10 +3,36 @@
 Version 9.6.1
 ==============
 
-
 Language
 ~~~~~~~~
 
+- GHC is now more conservative when solving constraints that arise from
+  superclass expansion in terms of other constraints that also arise from
+  superclass expansion.
+
+  For example: ::
+
+    class C a
+    class C a => D a b
+    instance D a a => D a b
+
+  When typechecking the instance, we need to also solve the constraints arising
+  from the superclasses of ``D``; in this case, we need ``C a``. We could obtain
+  evidence for this constraint by expanding the superclasses of the context,
+  as ``D a a`` also has a superclass context of ``C a``.
+  However, is it unsound to do so in general, as we might be assuming precisely
+  the predicate we want to prove! This can lead to programs that loop at runtime.
+
+  When such potentially-loopy situations arise, GHC now emits a warning.
+  In future releases, this behaviour will no longer be supported, and the
+  typechecker will outright refuse to solve these constraints, emitting a
+  ``Could not deduce`` error.
+
+  In practice, you should be able to fix these issues by adding the necessary
+  constraint to the context, e.g. for the above example: ::
+
+    instance (C a, D a a) => D a b
+
 - Record updates for GADTs and other existential datatypes are now
   fully supported.
 
diff --git a/docs/users_guide/using-warnings.rst b/docs/users_guide/using-warnings.rst
index 2c70006a7c..3624a63384 100644
--- a/docs/users_guide/using-warnings.rst
+++ b/docs/users_guide/using-warnings.rst
@@ -2319,6 +2319,22 @@ of ``-W(no-)*``.
     triggered whenever this happens, and can be addressed by enabling the
     extension.
 
+.. ghc-flag:: -Wloopy-superclass-solve
+    :shortdesc: warn when creating potentially-loopy superclass constraint evidence
+    :type: dynamic
+    :reverse: -Wno-loopy-superclass-solve
+
+    :since: 9.6.1
+
+    As explained in :ref:`undecidable_instances`, when using
+    :extension:`UndecidableInstances` it is possible for GHC to construct
+    non-terminating evidence for certain superclass constraints.
+
+    This behaviour is scheduled to be removed in a future GHC version.
+    In the meantime, GHC emits this warning to inform users of potential
+    non-termination. Users can manually add the required constraint to the context
+    to avoid the problem (thus silencing the warning).
+
 .. ghc-flag:: -Wterm-variable-capture
     :shortdesc: warn when an implicitly quantified type variable captures a term's name
     :type: dynamic
diff --git a/testsuite/tests/quantified-constraints/all.T b/testsuite/tests/quantified-constraints/all.T
index b3d0eb920f..d3bfe6e07e 100644
--- a/testsuite/tests/quantified-constraints/all.T
+++ b/testsuite/tests/quantified-constraints/all.T
@@ -41,3 +41,4 @@ test('T22216d', normal, compile, [''])
 test('T22216e', normal, compile, [''])
 test('T22223', normal, compile, [''])
 test('T19690', normal, compile_fail, [''])
+
diff --git a/testsuite/tests/typecheck/should_compile/T20666b.hs b/testsuite/tests/typecheck/should_compile/T20666b.hs
new file mode 100644
index 0000000000..7a655b73c9
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T20666b.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module T20666b where
+
+type family F a
+
+class Eq (F a) => D a
+class Eq (F a) => C a
+
+instance D [a] => C [a]
+
diff --git a/testsuite/tests/typecheck/should_compile/T20666b.stderr b/testsuite/tests/typecheck/should_compile/T20666b.stderr
new file mode 100644
index 0000000000..322c6850ea
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T20666b.stderr
@@ -0,0 +1,10 @@
+
+T20666b.hs:11:10: warning: [GHC-36038] [-Wloopy-superclass-solve (in -Wdefault)]
+    I am solving the constraint ‘Eq (F [a])’,
+      arising from the superclasses of an instance declaration,
+    in a way that might turn out to loop at runtime.
+    Future versions of GHC will turn this warning into an error.
+    See the user manual, § Undecidable instances and loopy superclasses.
+    Suggested fix:
+      Add the constraint ‘Eq (F [a])’ to the instance context,
+      even though it seems logically implied by other constraints in the context.
diff --git a/testsuite/tests/typecheck/should_compile/T22891.hs b/testsuite/tests/typecheck/should_compile/T22891.hs
new file mode 100644
index 0000000000..ad6b473395
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T22891.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+module T22891 where
+
+class Foo f
+
+class Foo f => Bar f g
+
+instance Bar f f => Bar f (h k)
diff --git a/testsuite/tests/typecheck/should_compile/T22891.stderr b/testsuite/tests/typecheck/should_compile/T22891.stderr
new file mode 100644
index 0000000000..a0bdc1649b
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T22891.stderr
@@ -0,0 +1,10 @@
+
+T22891.hs:9:10: warning: [GHC-36038] [-Wloopy-superclass-solve (in -Wdefault)]
+    I am solving the constraint ‘Foo f’,
+      arising from the superclasses of an instance declaration,
+    in a way that might turn out to loop at runtime.
+    Future versions of GHC will turn this warning into an error.
+    See the user manual, § Undecidable instances and loopy superclasses.
+    Suggested fix:
+      Add the constraint ‘Foo f’ to the instance context,
+      even though it seems logically implied by other constraints in the context.
diff --git a/testsuite/tests/typecheck/should_compile/T22912.hs b/testsuite/tests/typecheck/should_compile/T22912.hs
new file mode 100644
index 0000000000..994a8022ef
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T22912.hs
@@ -0,0 +1,26 @@
+{-# LANGUAGE MonoLocalBinds          #-}
+{-# LANGUAGE QuantifiedConstraints   #-}
+{-# LANGUAGE ScopedTypeVariables     #-}
+{-# LANGUAGE UndecidableInstances    #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
+
+module T22912 where
+
+
+class    c => Exactly c
+instance c => Exactly c
+class    c => Implies c
+
+data Dict c = c => Dict
+
+anythingDict :: forall c. Dict c
+anythingDict = go
+  where
+    go :: (Exactly (Implies c) => Implies c) => Dict c
+    go = Dict
+
+-- This is clearly wrong: we shouldn't be able to produce evidence
+-- for any constraint whatsoever! However, GHC can be tricked into
+-- producing a bottom dictionary.
+-- This test checks that it emits an appropriate warning when doing so,
+-- to allow users to adapt their code before we plug the hole completely.
diff --git a/testsuite/tests/typecheck/should_compile/T22912.stderr b/testsuite/tests/typecheck/should_compile/T22912.stderr
new file mode 100644
index 0000000000..b53614baff
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T22912.stderr
@@ -0,0 +1,12 @@
+
+T22912.hs:17:16: warning: [GHC-36038] [-Wloopy-superclass-solve (in -Wdefault)]
+    I am solving the constraint ‘Implies c’,
+      arising from the head of a quantified constraint
+      arising from a use of ‘go’,
+    in a way that might turn out to loop at runtime.
+    Future versions of GHC will turn this warning into an error.
+    See the user manual, § Undecidable instances and loopy superclasses.
+    Suggested fix:
+      Add the constraint ‘Implies
+                            c’ to the context of the quantified constraint,
+      even though it seems logically implied by other constraints in the context.
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 07d39cebd3..ff603bbcf3 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -857,3 +857,6 @@ test('T22647', normal, compile, [''])
 test('T19577', normal, compile, [''])
 test('T22383', normal, compile, [''])
 test('T21501', normal, compile, [''])
+test('T20666b', normal, compile, [''])
+test('T22891', normal, compile, [''])
+test('T22912', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/T20666.stderr b/testsuite/tests/typecheck/should_fail/T20666.stderr
index bc2aad5497..46d0fafcc4 100644
--- a/testsuite/tests/typecheck/should_fail/T20666.stderr
+++ b/testsuite/tests/typecheck/should_fail/T20666.stderr
@@ -1,20 +1,20 @@
 
-T20666.hs:13:10: error: [GHC-39999]
-    • Could not deduce ‘Show (T c)’
-        arising from the superclasses of an instance declaration
-      from the context: (D d, c ~ S d)
-        bound by the instance declaration at T20666.hs:13:10-31
-      Possible fix:
-        If the constraint looks soluble from a superclass of the instance context,
-        read 'Undecidable instances and loopy superclasses' in the user manual
-    • In the instance declaration for ‘C1 c’
+T20666.hs:13:10: warning: [GHC-36038] [-Wloopy-superclass-solve (in -Wdefault)]
+    I am solving the constraint ‘Show (T c)’,
+      arising from the superclasses of an instance declaration,
+    in a way that might turn out to loop at runtime.
+    Future versions of GHC will turn this warning into an error.
+    See the user manual, § Undecidable instances and loopy superclasses.
+    Suggested fix:
+      Add the constraint ‘Show (T c)’ to the instance context,
+      even though it seems logically implied by other constraints in the context.
 
-T20666.hs:17:10: error: [GHC-39999]
-    • Could not deduce ‘Show (T c)’
-        arising from the superclasses of an instance declaration
-      from the context: (D d, c ~ S d, c' ~ c)
-        bound by the instance declaration at T20666.hs:17:10-40
-      Possible fix:
-        If the constraint looks soluble from a superclass of the instance context,
-        read 'Undecidable instances and loopy superclasses' in the user manual
-    • In the instance declaration for ‘C2 c'’
+T20666.hs:17:10: warning: [GHC-36038] [-Wloopy-superclass-solve (in -Wdefault)]
+    I am solving the constraint ‘Show (T c)’,
+      arising from the superclasses of an instance declaration,
+    in a way that might turn out to loop at runtime.
+    Future versions of GHC will turn this warning into an error.
+    See the user manual, § Undecidable instances and loopy superclasses.
+    Suggested fix:
+      Add the constraint ‘Show (T c)’ to the instance context,
+      even though it seems logically implied by other constraints in the context.
diff --git a/testsuite/tests/typecheck/should_fail/T20666a.stderr b/testsuite/tests/typecheck/should_fail/T20666a.stderr
index 4192b88807..bed585dcd2 100644
--- a/testsuite/tests/typecheck/should_fail/T20666a.stderr
+++ b/testsuite/tests/typecheck/should_fail/T20666a.stderr
@@ -1,10 +1,10 @@
 
-T20666a.hs:11:10: error: [GHC-39999]
-    • Could not deduce ‘Eq (F [a])’
-        arising from the superclasses of an instance declaration
-      from the context: D [a]
-        bound by the instance declaration at T20666a.hs:11:10-23
-      Possible fix:
-        If the constraint looks soluble from a superclass of the instance context,
-        read 'Undecidable instances and loopy superclasses' in the user manual
-    • In the instance declaration for ‘C [a]’
+T20666a.hs:11:10: warning: [GHC-36038] [-Wloopy-superclass-solve (in -Wdefault)]
+    I am solving the constraint ‘Eq (F [a])’,
+      arising from the superclasses of an instance declaration,
+    in a way that might turn out to loop at runtime.
+    Future versions of GHC will turn this warning into an error.
+    See the user manual, § Undecidable instances and loopy superclasses.
+    Suggested fix:
+      Add the constraint ‘Eq (F [a])’ to the instance context,
+      even though it seems logically implied by other constraints in the context.
diff --git a/testsuite/tests/typecheck/should_fail/T6161.stderr b/testsuite/tests/typecheck/should_fail/T6161.stderr
index 71c7455abd..c1daab09df 100644
--- a/testsuite/tests/typecheck/should_fail/T6161.stderr
+++ b/testsuite/tests/typecheck/should_fail/T6161.stderr
@@ -1,7 +1,10 @@
 
-T6161.hs:19:10: error: [GHC-39999]
-    • Could not deduce ‘Super (Fam a)’
-        arising from the superclasses of an instance declaration
-      from the context: Foo a
-        bound by the instance declaration at T6161.hs:19:10-31
-    • In the instance declaration for ‘Duper (Fam a)’
+T6161.hs:19:10: warning: [GHC-36038] [-Wloopy-superclass-solve (in -Wdefault)]
+    I am solving the constraint ‘Super (Fam a)’,
+      arising from the superclasses of an instance declaration,
+    in a way that might turn out to loop at runtime.
+    Future versions of GHC will turn this warning into an error.
+    See the user manual, § Undecidable instances and loopy superclasses.
+    Suggested fix:
+      Add the constraint ‘Super (Fam a)’ to the instance context,
+      even though it seems logically implied by other constraints in the context.
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index a7e9f6a678..f8a3db350c 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -241,7 +241,7 @@ test('tcfail215', normal, compile_fail, [''])
 test('tcfail216', normal, compile_fail, [''])
 test('tcfail217', normal, compile_fail, [''])
 test('tcfail218', normal, compile_fail, [''])
-test('tcfail223', normal, compile_fail, [''])
+test('tcfail223', normal, compile, ['']) # To become compile_fail after migration period (see #22912)
 test('tcfail224', normal, compile_fail, [''])
 test('tcfail225', normal, compile_fail, [''])
 
@@ -294,7 +294,7 @@ test('T19187a', normal, compile_fail, [''])
 test('T2534', normal, compile_fail, [''])
 test('T7175', normal, compile_fail, [''])
 test('T7210', normal, compile_fail, [''])
-test('T6161', normal, compile_fail, [''])
+test('T6161', normal, compile, [''])       # To become compile_fail after migration period (see #22912)
 test('T7368', normal, compile_fail, [''])
 test('T7264', normal, compile_fail, [''])
 test('T6069', normal, compile_fail, [''])
@@ -665,5 +665,5 @@ test('T21530a', normal, compile_fail, [''])
 test('T21530b', normal, compile_fail, [''])
 test('T22570', normal, compile_fail, [''])
 test('T22645', normal, compile_fail, [''])
-test('T20666', normal, compile_fail, [''])
-test('T20666a', normal, compile_fail, [''])
+test('T20666', normal, compile, [''])   # To become compile_fail after migration period (see #22912)
+test('T20666a', normal, compile, [''])  # To become compile_fail after migration period (see #22912)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail223.stderr b/testsuite/tests/typecheck/should_fail/tcfail223.stderr
index d3173adde7..8201c8839f 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail223.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail223.stderr
@@ -1,9 +1,10 @@
 
-tcfail223.hs:10:10: error: [GHC-39999]
-    • Could not deduce ‘Class1 a’
-        arising from the superclasses of an instance declaration
-      from the context: Class3 a
-        bound by the instance declaration at tcfail223.hs:10:10-29
-      Possible fix:
-        add (Class1 a) to the context of the instance declaration
-    • In the instance declaration for ‘Class2 a’
+tcfail223.hs:10:10: warning: [GHC-36038] [-Wloopy-superclass-solve (in -Wdefault)]
+    I am solving the constraint ‘Class1 a’,
+      arising from the superclasses of an instance declaration,
+    in a way that might turn out to loop at runtime.
+    Future versions of GHC will turn this warning into an error.
+    See the user manual, § Undecidable instances and loopy superclasses.
+    Suggested fix:
+      Add the constraint ‘Class1 a’ to the instance context,
+      even though it seems logically implied by other constraints in the context.