Refactor the treatment of loopy superclass dicts

This patch completely re-engineers how we deal with loopy superclass
dictionaries in instance declarations. It fixes #20666 and #19690

The highlights are

* Recognise that the loopy-superclass business should use precisely
  the Paterson conditions.  This is much much nicer.  See
  Note [Recursive superclasses] in GHC.Tc.TyCl.Instance

* With that in mind, define "Paterson-smaller" in
  Note [Paterson conditions] in GHC.Tc.Validity, and the new
  data type `PatersonSize` in GHC.Tc.Utils.TcType, along with
  functions to compute and compare PatsonSizes

* Use the new PatersonSize stuff when solving superclass constraints
  See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance

* In GHC.Tc.Solver.Monad.lookupInInerts, add a missing call to
  prohibitedSuperClassSolve.  This was the original cause of #20666.

* Treat (TypeError "stuff") as having PatersonSize zero. See
  Note [Paterson size for type family applications] in GHC.Tc.Utils.TcType.

* ...

compiler/GHC/Core/InstEnv.hs

@@ -232,10 +232,8 @@ pprInstances ispecs = vcat (map pprInstance ispecs)
 
 instanceHead :: ClsInst -> ([TyVar], Class, [Type])
 -- Returns the head, using the fresh tyvars from the ClsInst
-instanceHead (ClsInst { is_tvs = tvs, is_tys = tys, is_dfun = dfun })
+instanceHead (ClsInst { is_tvs = tvs, is_cls = cls, is_tys = tys })
    = (tvs, cls, tys)
-   where
-     (_, _, cls, _) = tcSplitDFunTy (idType dfun)
 
 -- | Collects the names of concrete types and type constructors that make
 -- up the head of a class instance. For instance, given `class Foo a b`:

compiler/GHC/Core/TyCo/FVs.hs

@@ -31,7 +31,7 @@ module GHC.Core.TyCo.FVs
         noFreeVarsOfType, noFreeVarsOfTypes, noFreeVarsOfCo,
 
         -- * Free type constructors
-        tyConsOfType,
+        tyConsOfType, tyConsOfTypes,
 
         -- * Free vars with visible/invisible separate
         visVarsOfTypes, visVarsOfType,
@@ -1069,7 +1069,7 @@ tyConsOfType ty
      go ty | Just ty' <- coreView ty = go ty'
      go (TyVarTy {})                = emptyUniqSet
      go (LitTy {})                  = emptyUniqSet
-     go (TyConApp tc tys)           = go_tc tc `unionUniqSets` go_s tys
+     go (TyConApp tc tys)           = go_tc tc `unionUniqSets` tyConsOfTypes tys
      go (AppTy a b)                 = go a `unionUniqSets` go b
      go (FunTy af w a b)            = go w `unionUniqSets`
                                       go a `unionUniqSets` go b
@@ -1108,12 +1108,13 @@ tyConsOfType ty
         -- this last case can happen from the tyConsOfType used from
         -- checkTauTvUpdate
 
-     go_s tys     = foldr (unionUniqSets . go)     emptyUniqSet tys
      go_cos cos   = foldr (unionUniqSets . go_co)  emptyUniqSet cos
 
      go_tc tc = unitUniqSet tc
      go_ax ax = go_tc $ coAxiomTyCon ax
 
+tyConsOfTypes :: [Type] -> UniqSet TyCon
+tyConsOfTypes tys = foldr (unionUniqSets . tyConsOfType) emptyUniqSet tys
 
 {- **********************************************************************
 *                                                                       *

compiler/GHC/Tc/Deriv.hs

@@ -28,7 +28,7 @@ import GHC.Tc.Deriv.Utils
 import GHC.Tc.TyCl.Class( instDeclCtxt3, tcATDefault )
 import GHC.Tc.Utils.Env
 import GHC.Tc.Deriv.Generate
-import GHC.Tc.Validity( allDistinctTyVars, checkValidInstHead )
+import GHC.Tc.Validity( checkValidInstHead )
 import GHC.Core.InstEnv
 import GHC.Tc.Utils.Instantiate
 import GHC.Core.FamInstEnv

compiler/GHC/Tc/Deriv/Infer.hs

@@ -51,7 +51,6 @@ import GHC.Utils.Misc
 
 import GHC.Types.Basic
 import GHC.Types.Var
-import GHC.Types.Var.Set
 
 import GHC.Data.Bag
 
@@ -701,7 +700,7 @@ simplifyInstanceContexts infer_specs
                                     current_solns infer_specs
            ; new_solns <- checkNoErrs $
                           extendLocalInstEnv inst_specs $
-                          mapM gen_soln infer_specs
+                          mapM simplifyDeriv infer_specs
 
            ; if (current_solns `eqSolution` new_solns) then
                 return [ setDerivSpecTheta soln spec
@@ -713,24 +712,6 @@ simplifyInstanceContexts infer_specs
        -- Canonicalise for comparison
        -- See Note [Deterministic simplifyInstanceContexts]
     canSolution = map (sortBy nonDetCmpType)
-    ------------------------------------------------------------------
-    gen_soln :: DerivSpec ThetaSpec -> TcM ThetaType
-    gen_soln (DS { ds_loc = loc, ds_tvs = tyvars
-                 , ds_cls = clas, ds_tys = inst_tys, ds_theta = deriv_rhs
-                 , ds_skol_info = skol_info, ds_user_ctxt = user_ctxt })
-      = setSrcSpan loc  $
-        addErrCtxt (derivInstCtxt the_pred) $
-        do { theta <- simplifyDeriv skol_info user_ctxt tyvars deriv_rhs
-                -- checkValidInstance tyvars theta clas inst_tys
-                -- Not necessary; see Note [Exotic derived instance contexts]
-
-           ; traceTc "GHC.Tc.Deriv" (ppr deriv_rhs $$ ppr theta)
-                -- Claim: the result instance declaration is guaranteed valid
-                -- Hence no need to call:
-                --   checkValidInstance tyvars theta clas inst_tys
-           ; return theta }
-      where
-        the_pred = mkClassPred clas inst_tys
 
 derivInstCtxt :: PredType -> SDoc
 derivInstCtxt pred
@@ -744,29 +725,27 @@ derivInstCtxt pred
 ***********************************************************************************
 -}
 
+
 -- | Given @instance (wanted) => C inst_ty@, simplify 'wanted' as much
 -- as possible. Fail if not possible.
-simplifyDeriv :: SkolemInfo -- ^ The 'SkolemInfo' used to skolemise the
-                            -- 'TcTyVar' arguments
-              -> UserTypeCtxt -- ^ Used to inform error messages as to whether
-                              -- we are in a @deriving@ clause or a standalone
-                              -- @deriving@ declaration
-              -> [TcTyVar]  -- ^ The tyvars bound by @inst_ty@.
-              -> ThetaSpec -- ^ The constraints to solve and simplify
+simplifyDeriv :: DerivSpec ThetaSpec
               -> TcM ThetaType -- ^ Needed constraints (after simplification),
                                -- i.e. @['PredType']@.
-simplifyDeriv skol_info user_ctxt tvs theta
-  = do { let skol_set = mkVarSet tvs
-
+simplifyDeriv (DS { ds_loc = loc, ds_tvs = tvs
+                  , ds_cls = clas, ds_tys = inst_tys, ds_theta = deriv_rhs
+                  , ds_skol_info = skol_info, ds_user_ctxt = user_ctxt })
+  = setSrcSpan loc  $
+    addErrCtxt (derivInstCtxt (mkClassPred clas inst_tys)) $
+    do {
        -- See [STEP DAC BUILD]
        -- Generate the implication constraints, one for each method, to solve
        -- with the skolemized variables.  Start "one level down" because
        -- we are going to wrap the result in an implication with tvs,
        -- in step [DAC RESIDUAL]
-       ; (tc_lvl, wanteds) <- captureThetaSpecConstraints user_ctxt theta
+       ; (tc_lvl, wanteds) <- captureThetaSpecConstraints user_ctxt deriv_rhs
 
        ; traceTc "simplifyDeriv inputs" $
-         vcat [ pprTyVars tvs $$ ppr theta $$ ppr wanteds, ppr skol_info ]
+         vcat [ pprTyVars tvs $$ ppr deriv_rhs $$ ppr wanteds, ppr skol_info ]
 
        -- See [STEP DAC SOLVE]
        -- Simplify the constraints, starting at the same level at which
@@ -783,6 +762,7 @@ simplifyDeriv skol_info user_ctxt tvs theta
        -- From the simplified constraints extract a subset 'good' that will
        -- become the context 'min_theta' for the derived instance.
        ; let residual_simple = approximateWC True solved_wanteds
+             head_size       = pSizeClassPred clas inst_tys
              good = mapMaybeBag get_good residual_simple
 
              -- Returns @Just p@ (where @p@ is the type of the Ct) if a Ct is
@@ -791,10 +771,8 @@ simplifyDeriv skol_info user_ctxt tvs theta
              -- See Note [Exotic derived instance contexts] for what
              -- constitutes an exotic constraint.
              get_good :: Ct -> Maybe PredType
-             get_good ct | validDerivPred skol_set p
-                         = Just p
-                         | otherwise
-                         = Nothing
+             get_good ct | validDerivPred head_size p = Just p
+                         | otherwise                  = Nothing
                where p = ctPred ct
 
        ; traceTc "simplifyDeriv outputs" $
@@ -824,6 +802,13 @@ simplifyDeriv skol_info user_ctxt tvs theta
        -- in this line of code.
        ; simplifyTopImplic leftover_implic
 
+       ; traceTc "GHC.Tc.Deriv" (ppr deriv_rhs $$ ppr min_theta)
+
+         -- Claim: the result instance declaration is guaranteed valid
+         -- Hence no need to call:
+         --     checkValidInstance tyvars theta clas inst_tys
+         -- See Note [Exotic derived instance contexts]
+
        ; return min_theta }
 
 {-

compiler/GHC/Tc/Errors.hs

@@ -391,7 +391,7 @@ reportImplic ctxt implic@(Implic { ic_skols  = tvs
 
 warnRedundantConstraints :: SolverReportErrCtxt -> TcLclEnv -> SkolemInfoAnon -> [EvVar] -> TcM ()
 -- See Note [Tracking redundant constraints] in GHC.Tc.Solver
-warnRedundantConstraints ctxt env info ev_vars
+warnRedundantConstraints ctxt env info redundant_evs
  | null redundant_evs
  = return ()
 
@@ -423,18 +423,6 @@ warnRedundantConstraints ctxt env info ev_vars
                 []
           ; reportDiagnostic msg }
 
-   redundant_evs =
-       filterOut is_type_error $
-       case info of -- See Note [Redundant constraints in instance decls]
-         InstSkol -> filterOut (improving . idType) ev_vars
-         _        -> ev_vars
-
-   -- See #15232
-   is_type_error = isJust . userTypeError_maybe . idType
-
-   improving pred -- (transSuperClasses p) does not include p
-     = any isImprovementPred (pred : transSuperClasses pred)
-
 reportBadTelescope :: SolverReportErrCtxt -> TcLclEnv -> SkolemInfoAnon -> [TcTyVar] -> TcM ()
 reportBadTelescope ctxt env (ForAllSkol telescope) skols
   = do { msg <- mkErrorReport
@@ -449,23 +437,6 @@ reportBadTelescope ctxt env (ForAllSkol telescope) skols
 reportBadTelescope _ _ skol_info skols
   = pprPanic "reportBadTelescope" (ppr skol_info $$ ppr skols)
 
-{- Note [Redundant constraints in instance decls]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-For instance declarations, we don't report unused givens if
-they can give rise to improvement.  Example (#10100):
-    class Add a b ab | a b -> ab, a ab -> b
-    instance Add Zero b b
-    instance Add a b ab => Add (Succ a) b (Succ ab)
-The context (Add a b ab) for the instance is clearly unused in terms
-of evidence, since the dictionary has no fields.  But it is still
-needed!  With the context, a wanted constraint
-   Add (Succ Zero) beta (Succ Zero)
-we will reduce to (Add Zero beta Zero), and thence we get beta := Zero.
-But without the context we won't find beta := Zero.
-
-This only matters in instance declarations..
--}
-
 -- | Should we completely ignore this constraint in error reporting?
 -- It *must* be the case that any constraint for which this returns True
 -- somehow causes an error to be reported elsewhere.

compiler/GHC/Tc/Errors/Ppr.hs

@@ -2618,7 +2618,7 @@ pprTcSolverReportMsg ctxt@(CEC {cec_encl = implics})
             -- Don't suggest fixes for the provided context of a pattern
             -- synonym; the right fix is to bind more in the pattern
         show_fixes (ctxtFixes has_ambigs pred implics
-                    ++ drv_fixes)
+                    ++ drv_fixes ++ naked_sc_fixes)
       , ppWhen (not (null candidates))
         (hang (text "There are instances for similar types:")
             2 (vcat (map ppr candidates)))
@@ -2689,7 +2689,7 @@ pprTcSolverReportMsg ctxt@(CEC {cec_encl = implics})
                    StandAloneDerivOrigin              -> [drv_fix True]
                    DerivOriginDC _ _       standalone -> [drv_fix standalone]
                    DerivOriginCoerce _ _ _ standalone -> [drv_fix standalone]
-                   _                -> []
+                   _                                  -> []
 
     drv_fix standalone_wildcard
       | standalone_wildcard
@@ -2698,6 +2698,25 @@ pprTcSolverReportMsg ctxt@(CEC {cec_encl = implics})
       = hang (text "use a standalone 'deriving instance' declaration,")
            2 (text "so you can specify the instance context yourself")
 
+    -- naked_sc_fix: try to produce a helpful error message for
+    -- superclass constraints caught by the subtleties described by
+    -- Note [Recursive superclasses] in GHC.TyCl.Instance
+    naked_sc_fixes
+      | ScOrigin _ NakedSc <- orig  -- A superclass wanted with no instance decls used yet
+      , any non_tyvar_preds useful_givens  -- Some non-tyvar givens
+      = [vcat [ text "If the constraint looks soluble from a superclass of the instance context,"
+              , text "read 'Undecidable instances and loopy superclasses' in the user manual" ]]
+      | otherwise = []
+
+    non_tyvar_preds :: UserGiven -> Bool
+    non_tyvar_preds = any non_tyvar_pred . ic_given
+
+    non_tyvar_pred :: EvVar -> Bool
+    -- Tells if the Given is of form (C ty1 .. tyn), where the tys are not all tyvars
+    non_tyvar_pred given = case getClassPredTys_maybe (idType given) of
+                             Just (_, tys) -> not (all isTyVarTy tys)
+                             Nothing       -> False
+
 pprTcSolverReportMsg (CEC {cec_encl = implics}) (OverlappingInstances item matches unifiers) =
   vcat
     [ addArising ct_loc $
@@ -3529,7 +3548,7 @@ show_fixes (f:fs) = sep [ text "Possible fix:"
 ctxtFixes :: Bool -> PredType -> [Implication] -> [SDoc]
 ctxtFixes has_ambig_tvs pred implics
   | not has_ambig_tvs
-  , isTyVarClassPred pred
+  , isTyVarClassPred pred   -- Don't suggest adding (Eq T) to the context, say
   , (skol:skols) <- usefulContext implics pred
   , let what | null skols
              , SigSkol (PatSynCtxt {}) _ _ <- skol

compiler/GHC/Tc/Gen/HsType.hs

@@ -664,7 +664,9 @@ tcDerivStrategy mb_lds
     tc_deriv_strategy (NewtypeStrategy  _) = boring_case (NewtypeStrategy  noExtField)
     tc_deriv_strategy (ViaStrategy hs_sig)
       = do { ty <- tcTopLHsType DerivClauseCtxt hs_sig
-           ; rec { (via_tvs, via_pred) <- tcSkolemiseInvisibleBndrs (DerivSkol via_pred) ty}
+             -- rec {..}: see Note [Keeping SkolemInfo inside a SkolemTv]
+             --           in GHC.Tc.Utils.TcType
+           ; rec { (via_tvs, via_pred) <- tcSkolemiseInvisibleBndrs (DerivSkol via_pred) ty }
            ; pure (ViaStrategy via_pred, via_tvs) }
 
     boring_case :: ds -> TcM (ds, [a])

compiler/GHC/Tc/Solver.hs

@@ -73,7 +73,7 @@ import Control.Monad
 import Data.Foldable      ( toList )
 import Data.List          ( partition )
 import Data.List.NonEmpty ( NonEmpty(..) )
-import GHC.Data.Maybe     ( mapMaybe )
+import GHC.Data.Maybe     ( mapMaybe, isJust )
 
 {-
 *********************************************************************************
@@ -1199,10 +1199,12 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
        -- NB: bound_theta are constraints we want to quantify over,
        --     including the psig_theta, which we always quantify over
        -- NB: bound_theta are fully zonked
+       -- rec {..}: see Note [Keeping SkolemInfo inside a SkolemTv]
+       --           in GHC.Tc.Utils.TcType
        ; rec { (qtvs, bound_theta, co_vars) <- decideQuantification skol_info infer_mode rhs_tclvl
                                                      name_taus partial_sigs
                                                      quant_pred_candidates
-             ;  bound_theta_vars <- mapM TcM.newEvVar bound_theta
+             ; bound_theta_vars <- mapM TcM.newEvVar bound_theta
 
              ; let full_theta = map idType bound_theta_vars
              ; skol_info <- mkSkolemInfo (InferSkol [ (name, mkSigmaTy [] full_theta ty)
@@ -2490,18 +2492,7 @@ setImplicationStatus implic@(Implic { ic_status     = status
 
       ; bad_telescope <- checkBadTelescope implic
 
-      ; let (used_givens, unused_givens)
-              | warnRedundantGivens info
-              = partition (`elemVarSet` need_inner) givens
-              | otherwise = (givens, [])   -- None to report
-
-            minimal_used_givens = mkMinimalBySCs evVarPred used_givens
-            is_minimal = (`elemVarSet` mkVarSet minimal_used_givens)
-
-            warn_givens
-              | not (null unused_givens) = unused_givens
-              | warnRedundantGivens info = filterOut is_minimal used_givens
-              | otherwise                = []
+      ; let warn_givens = findUnnecessaryGivens info need_inner givens
 
             discard_entire_implication  -- Can we discard the entire implication?
               =  null warn_givens           -- No warning from this implication
@@ -2541,6 +2532,67 @@ setImplicationStatus implic@(Implic { ic_status     = status
      | otherwise
      = True        -- Otherwise, keep it
 
+findUnnecessaryGivens :: SkolemInfoAnon -> VarSet -> [EvVar] -> [EvVar]
+findUnnecessaryGivens info need_inner givens
+  | not (warnRedundantGivens info)   -- Don't report redundant constraints at all
+  = []
+
+  | not (null unused_givens)         -- Some givens are literally unused
+  = unused_givens
+
+   | otherwise                       -- All givens are used, but some might
+   = redundant_givens                -- still be redundant e.g. (Eq a, Ord a)
+
+  where
+    in_instance_decl = case info of { InstSkol {} -> True; _ -> False }
+                       -- See Note [Redundant constraints in instance decls]
+
+    unused_givens = filterOut is_used givens
+
+    is_used given =   is_type_error given
+                  ||  (given `elemVarSet` need_inner)
+                  ||  (in_instance_decl && is_improving (idType given))
+
+    minimal_givens = mkMinimalBySCs evVarPred givens
+    is_minimal = (`elemVarSet` mkVarSet minimal_givens)
+    redundant_givens
+      | in_instance_decl = []
+      | otherwise        = filterOut is_minimal givens
+
+    -- See #15232
+    is_type_error = isJust . userTypeError_maybe . idType
+
+    is_improving pred -- (transSuperClasses p) does not include p
+      = any isImprovementPred (pred : transSuperClasses pred)
+
+{- Note [Redundant constraints in instance decls]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Instance declarations are special in two ways:
+
+* We don't report unused givens if they can give rise to improvement.
+  Example (#10100):
+    class Add a b ab | a b -> ab, a ab -> b
+    instance Add Zero b b
+    instance Add a b ab => Add (Succ a) b (Succ ab)
+  The context (Add a b ab) for the instance is clearly unused in terms
+  of evidence, since the dictionary has no fields.  But it is still
+  needed!  With the context, a wanted constraint
+     Add (Succ Zero) beta (Succ Zero)
+  we will reduce to (Add Zero beta Zero), and thence we get beta := Zero.
+  But without the context we won't find beta := Zero.
+
+  This only matters in instance declarations.
+
+* We don't report givens that are a superclass of another given. E.g.
+       class Ord r => UserOfRegs r a where ...
+       instance (Ord r, UserOfRegs r CmmReg) => UserOfRegs r CmmExpr where
+  The (Ord r) is not redundant, even though it is a superclass of
+  (UserOfRegs r CmmReg).  See Note [Recursive superclasses] in GHC.Tc.TyCl.Instance.
+
+  Again this is specific to instance declarations.
+-}
+
+
 checkBadTelescope :: Implication -> TcS Bool
 -- True <=> the skolems form a bad telescope
 -- See Note [Checking telescopes] in GHC.Tc.Types.Constraint

compiler/GHC/Tc/Solver/Canonical.hs

 {-# LANGUAGE CPP #-}
 {-# LANGUAGE DeriveFunctor #-}
 {-# LANGUAGE MultiWayIf #-}
+{-# LANGUAGE RecursiveDo #-}
 
 module GHC.Tc.Solver.Canonical(
      canonicalize,
@@ -530,7 +531,7 @@ mk_strict_superclasses rec_clss (CtGiven { ctev_evar = evar, ctev_loc = loc })
     classSCSelIds cls
   where
     dict_ids  = mkTemplateLocals theta
-    size      = sizeTypes tys
+    this_size = pSizeClassPred cls tys
 
     do_one_given sel_id
       | isUnliftedType sc_pred
@@ -570,37 +571,38 @@ mk_strict_superclasses rec_clss (CtGiven { ctev_evar = evar, ctev_loc = loc })
             `App` (evId evar `mkVarApps` (tvs ++ dict_ids))
             `mkVarApps` sc_tvs
 
-    sc_loc
-       | isCTupleClass cls
-       = loc   -- For tuple predicates, just take them apart, without
-               -- adding their (large) size into the chain.  When we
-               -- get down to a base predicate, we'll include its size.
-               -- #10335
-
-       |  isEqPredClass cls
-       || cls `hasKey` coercibleTyConKey
-       = loc   -- The only superclasses of ~, ~~, and Coercible are primitive
-               -- equalities, and they don't use the InstSCOrigin mechanism
-               -- detailed in Note [Solving superclass constraints] in
-               -- GHC.Tc.TyCl.Instance. Skip for a tiny performance win.
-
-         -- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance
-         -- for explanation of InstSCOrigin and Note [Replacement vs keeping] in
-         -- GHC.Tc.Solver.Interact for why we need OtherSCOrigin and depths
-       | otherwise
-       = loc { ctl_origin = new_orig }
-       where
-         new_orig = case ctLocOrigin loc of
-            -- these cases are when we have something that's already a superclass constraint
-           InstSCOrigin  sc_depth n  -> InstSCOrigin  (sc_depth + 1) (n `max` size)
-           OtherSCOrigin sc_depth si -> OtherSCOrigin (sc_depth + 1) si
-
-            -- these cases do not already have a superclass constraint: depth starts at 1
-           GivenOrigin InstSkol      -> InstSCOrigin  1 size
-           GivenOrigin other_skol    -> OtherSCOrigin 1 other_skol
-
-           other_orig                -> pprPanic "Given constraint without given origin" $
-                                        ppr evar $$ ppr other_orig
+    sc_loc | isCTupleClass cls
+           = loc   -- For tuple predicates, just take them apart, without
+                   -- adding their (large) size into the chain.  When we
+                   -- get down to a base predicate, we'll include its size.
+                   -- #10335
+
+           |  isEqPredClass cls || cls `hasKey` coercibleTyConKey
+           = loc   -- The only superclasses of ~, ~~, and Coercible are primitive
+                   -- equalities, and they don't use the GivenSCOrigin mechanism
+                   -- detailed in Note [Solving superclass constraints] in
+                   -- GHC.Tc.TyCl.Instance. Skip for a tiny performance win.
+
+           | otherwise
+           = loc { ctl_origin = mk_sc_origin (ctLocOrigin loc) }
+
+    -- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance
+    -- for explanation of GivenSCOrigin and Note [Replacement vs keeping] in
+    -- GHC.Tc.Solver.Interact for why we need depths
+    mk_sc_origin :: CtOrigin -> CtOrigin
+    mk_sc_origin (GivenSCOrigin skol_info sc_depth already_blocked)
+      = GivenSCOrigin skol_info (sc_depth + 1)
+                      (already_blocked || newly_blocked skol_info)
+
+    mk_sc_origin (GivenOrigin skol_info)
+      = -- These cases do not already have a superclass constraint: depth starts at 1
+        GivenSCOrigin skol_info 1 (newly_blocked skol_info)
+
+    mk_sc_origin other_orig = pprPanic "Given constraint without given origin" $
+                              ppr evar $$ ppr other_orig
+
+    newly_blocked (InstSkol _ head_size) = isJust (this_size `ltPatersonSize` head_size)
+    newly_blocked _                      = False
 
 mk_strict_superclasses rec_clss ev tvs theta cls tys
   | all noFreeVarsOfType tys
@@ -861,16 +863,27 @@ solveForAll ev@(CtWanted { ctev_dest = dest, ctev_rewriters = rewriters, ctev_lo
     -- This setLclEnv is important: the emitImplicationTcS uses that
     -- TcLclEnv for the implication, and that in turn sets the location
     -- for the Givens when solving the constraint (#21006)
-    do { skol_info <- mkSkolemInfo QuantCtxtSkol
-       ; let empty_subst = mkEmptySubst $ mkInScopeSet $
+    do { let empty_subst = mkEmptySubst $ mkInScopeSet $
                            tyCoVarsOfTypes (pred:theta) `delVarSetList` tvs
-       ; (subst, skol_tvs) <- tcInstSkolTyVarsX skol_info empty_subst tvs
-       ; given_ev_vars <- mapM newEvVar (substTheta subst theta)
-
+             is_qc = IsQC (ctLocOrigin loc)
+
+         -- rec {..}: see Note [Keeping SkolemInfo inside a SkolemTv]
+         --           in GHC.Tc.Utils.TcType
+         -- Very like the code in tcSkolDFunType
+       ; rec { skol_info <- mkSkolemInfo skol_info_anon
+             ; (subst, skol_tvs) <- tcInstSkolTyVarsX skol_info empty_subst tvs
+             ; let inst_pred  = substTy    subst pred
+                   inst_theta = substTheta subst theta
+                   skol_info_anon = InstSkol is_qc (get_size inst_pred) }
+
+       ; given_ev_vars <- mapM newEvVar inst_theta
        ; (lvl, (w_id, wanteds))
              <- pushLevelNoWorkList (ppr skol_info) $
-                do { wanted_ev <- newWantedEvVarNC loc rewriters $
-                                  substTy subst pred
+                do { let loc' = setCtLocOrigin loc (ScOrigin is_qc NakedSc)
+                         -- Set the thing to prove to have a ScOrigin, so we are
+                         -- careful about its termination checks.
+                         -- See (QC-INV) in Note [Solving a Wanted forall-constraint]
+                   ; wanted_ev <- newWantedEvVarNC loc' rewriters inst_pred
                    ; return ( ctEvEvId wanted_ev
                             , unitBag (mkNonCanonical wanted_ev)) }
 
@@ -882,6 +895,12 @@ solveForAll ev@(CtWanted { ctev_dest = dest, ctev_rewriters = rewriters, ctev_lo
               , et_binds = ev_binds, et_body = w_id }
 
       ; stopWith ev "Wanted forall-constraint" }
+  where
+    -- Getting the size of the head is a bit horrible
+    -- because of the special treament for class predicates
+    get_size pred = case classifyPredType pred of
+                      ClassPred cls tys -> pSizeClassPred cls tys
+                      _                 -> pSizeType pred
 
  -- See Note [Solving a Given forall-constraint]
 solveForAll ev@(CtGiven {}) tvs _theta pred pend_sc
@@ -902,6 +921,23 @@ and discharge df thus:
 where <binds> is filled in by solving the implication constraint.
 All the machinery is to hand; there is little to do.
 
+The tricky point is about termination: see #19690.  We want to maintain
+the invariant (QC-INV):
+
+  (QC-INV) Every quantified constraint returns a non-bottom dictionary
+
+just as every top-level instance declaration guarantees to return a non-bottom
+dictionary.  But as #19690 shows, it is possible to get a bottom dicionary
+by superclass selection if we aren't careful.  The situation is very similar
+to that described in Note [Recursive superclasses] in GHC.Tc.TyCl.Instance;
+and we use the same solution:
+
+* Give the Givens a CtOrigin of (GivenOrigin (InstSkol IsQC head_size))
+* Give the Wanted a CtOrigin of (ScOrigin IsQC NakedSc)
+
+Both of these things are done in solveForAll.  Now the mechanism described
+in Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance takes over.
+
 Note [Solving a Given forall-constraint]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 For a Given constraint

compiler/GHC/Tc/Solver/InertSet.hs

@@ -1633,12 +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 -> CtLoc -> Bool
--- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance
-prohibitedSuperClassSolve from_loc solve_loc
-  | InstSCOrigin _ given_size <- ctLocOrigin from_loc
-  , ScOrigin wanted_size <- ctLocOrigin solve_loc
-  = given_size >= wanted_size
+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)
+prohibitedSuperClassSolve given_loc wanted_loc
+  | GivenSCOrigin _ _ blocked <- ctLocOrigin given_loc
+  , blocked
+  , ScOrigin _ NakedSc <- ctLocOrigin wanted_loc
+  = True    -- Prohibited if the Wanted is a superclass
+            -- and the Given has come via a superclass selection from
+            -- a predicate bigger than the head
   | otherwise
   = False
 

compiler/GHC/Tc/Solver/Interact.hs

@@ -6,8 +6,7 @@ module GHC.Tc.Solver.Interact (
   ) where
 
 import GHC.Prelude
-import GHC.Types.Basic ( SwapFlag(..),
-                         infinity, IntWithInf, intGtLimit )
+import GHC.Types.Basic ( SwapFlag(..), IntWithInf, intGtLimit )
 import GHC.Tc.Solver.Canonical
 import GHC.Types.Var.Set
 
@@ -520,17 +519,18 @@ solveOneFromTheOther ct_i 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
+     loc_i  = ctEvLoc ev_i
+     loc_w  = ctEvLoc ev_w
+     orig_i = ctLocOrigin loc_i
+     orig_w = ctLocOrigin loc_w
+     lvl_i  = ctLocLevel loc_i
+     lvl_w  = ctLocLevel loc_w
 
      is_psc_w = isPendingScDict ct_w
      is_psc_i = isPendingScDict ct_i