Refactor the treatment of loopy superclass dictswip/T20666

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.

* Treat the head of a Wanted quantified constraint in the same way
  as the superclass of an instance decl; this is what fixes #19690.
  See GHC.Tc.Solver.Canonical Note [Solving a Wanted forall-constraint]
  (Thanks to Matthew Craven for this insight.)

  This entailed refactoring the GivenSc constructor of CtOrigin a bit,
  to say whether it comes from an instance decl or quantified constraint.

* Some refactoring way in which redundant constraints are reported; we
  don't want to complain about the extra, apparently-redundant
  constraints that we must add to an instance decl because of the
  loopy-superclass thing.  I moved some work from GHC.Tc.Errors to
  GHC.Tc.Solver.

* Add a new section to the user manual to describe the loopy
  superclass issue and what rules it follows.

4 files changed, 136 insertions, 84 deletions

diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs
index 33ee8e854c..02ce8115ad 100644
--- a/compiler/GHC/Tc/Solver/Canonical.hs
+++ b/compiler/GHC/Tc/Solver/Canonical.hs
@@ -1,6 +1,7 @@
 {-# 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
diff --git a/compiler/GHC/Tc/Solver/InertSet.hs b/compiler/GHC/Tc/Solver/InertSet.hs
index b3dcb3f5b1..5dc3431b9a 100644
--- a/compiler/GHC/Tc/Solver/InertSet.hs
+++ b/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
 
diff --git a/compiler/GHC/Tc/Solver/Interact.hs b/compiler/GHC/Tc/Solver/Interact.hs
index c3aa2d2695..e69e7ae0fe 100644
--- a/compiler/GHC/Tc/Solver/Interact.hs
+++ b/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
 
-     is_wsc_orig_i = is_wanted_superclass_loc loc_i
-     is_wsc_orig_w = is_wanted_superclass_loc loc_w
-     is_wanted_superclass_loc = isWantedSuperclassOrigin . ctLocOrigin
+     is_wsc_orig_i = isWantedSuperclassOrigin orig_i
+     is_wsc_orig_w = isWantedSuperclassOrigin orig_w
 
      different_level_strategy  -- Both Given
        | isIPLikePred pred = if lvl_w > lvl_i then KeepWork  else KeepInert
@@ -539,27 +539,20 @@ solveOneFromTheOther ct_i ct_w
        -- For the isIPLikePred case see Note [Shadowing of Implicit Parameters]
 
      same_level_strategy -- Both Given
-       = case (ctLocOrigin loc_i, ctLocOrigin loc_w) of
-              -- case 2(a) from Note [Replacement vs keeping]
-           (InstSCOrigin _depth_i size_i, InstSCOrigin _depth_w size_w)
-             | size_w < size_i -> KeepWork
-             | otherwise       -> KeepInert
+       = case (orig_i, orig_w) of
 
-              -- case 2(c) from Note [Replacement vs keeping]
-           (InstSCOrigin depth_i _, OtherSCOrigin depth_w _)  -> choose_shallower depth_i depth_w
-           (OtherSCOrigin depth_i _, InstSCOrigin depth_w _)  -> choose_shallower depth_i depth_w
-           (OtherSCOrigin depth_i _, OtherSCOrigin depth_w _) -> choose_shallower depth_i depth_w
+           (GivenSCOrigin _ depth_i blocked_i, GivenSCOrigin _ depth_w blocked_w)
+             | blocked_i, not blocked_w -> KeepWork  -- Case 2(a) from
+             | not blocked_i, blocked_w -> KeepInert -- Note [Replacement vs keeping]
 
-              -- case 2(b) from Note [Replacement vs keeping]
-           (InstSCOrigin {}, _)                         -> KeepWork
-           (OtherSCOrigin {}, _)                        -> KeepWork
+             -- Both blocked or both not blocked
 
-             -- case 2(d) from Note [Replacement vs keeping]
-           _                                      -> KeepInert
+             | depth_w < depth_i -> KeepWork   -- Case 2(c) from
+             | otherwise         -> KeepInert  -- Note [Replacement vs keeping]
 
-     choose_shallower depth_i depth_w | depth_w < depth_i = KeepWork
-                                      | otherwise         = KeepInert
-       -- favor KeepInert in the equals case, according to 2(d) from the Note
+           (GivenSCOrigin {}, _) -> KeepWork  -- Case 2(b) from Note [Replacement vs keeping]
+
+           _ -> KeepInert  -- Case 2(d) from Note [Replacement vs keeping]
 
 {-
 Note [Replacement vs keeping]
@@ -585,7 +578,7 @@ solveOneFromTheOther.
 
   2) Constraints coming from the same level (i.e. same implication)
 
-       (a) If both are InstSCOrigin, choose the one with the smallest TypeSize,
+       (a) If both are GivenSCOrigin, choose the one that is unblocked if possible
            according to Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance.
 
        (b) Prefer constraints that are not superclass selections. Example:
@@ -601,11 +594,12 @@ solveOneFromTheOther.
            Getting this wrong was #20602. See also
            Note [Tracking redundant constraints] in GHC.Tc.Solver.
 
-       (c) If both are superclass selections (but not both InstSCOrigin), choose the one
-           with the shallower superclass-selection depth, in the hope of identifying
-           more correct redundant constraints. This is really a generalization of
-           point (b), because the superclass depth of a non-superclass
-           constraint is 0.
+       (c) If both are GivenSCOrigin, chooose the one with the shallower
+           superclass-selection depth, in the hope of identifying more correct
+           redundant constraints. This is really a generalization of point (b),
+           because the superclass depth of a non-superclass constraint is 0.
+
+           (If the levels differ, we definitely won't have both with GivenSCOrigin.)
 
        (d) Finally, when there is still a choice, use KeepInert rather than
            KeepWork, for two reasons:
@@ -669,7 +663,10 @@ interactIrred inerts ct_w@(CIrredCan { cc_ev = ev_w, cc_reason = reason })
         -- See Note [Multiple matching irreds]
   , let ev_i = ctEvidence ct_i
   = do { what_next <- solveOneFromTheOther ct_i ct_w
-       ; traceTcS "iteractIrred" (ppr ct_w $$ ppr what_next $$ ppr ct_i)
+       ; 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
             KeepInert -> do { setEvBindIfWanted ev_w (swap_me swap ev_i)
                             ; return (Stop ev_w (text "Irred equal" <+> parens (ppr what_next))) }
@@ -2326,9 +2323,11 @@ checkInstanceOK loc what pred
      origin     = ctLocOrigin loc
 
      zap_origin loc  -- After applying an instance we can set ScOrigin to
-                     -- infinity, so that prohibitedSuperClassSolve never fires
-       | ScOrigin {} <- origin
-       = setCtLocOrigin loc (ScOrigin infinity)
+                     -- NotNakedSc, so that prohibitedSuperClassSolve never fires
+                     -- See Note [Solving superclass constraints] in
+                     -- GHC.Tc.TyCl.Instance, (sc1).
+       | ScOrigin what _ <- origin
+       = setCtLocOrigin loc (ScOrigin what NotNakedSc)
        | otherwise
        = loc
 
diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs
index 67c90dcd80..b5cf81ad9d 100644
--- a/compiler/GHC/Tc/Solver/Monad.hs
+++ b/compiler/GHC/Tc/Solver/Monad.hs
@@ -672,8 +672,16 @@ lookupInInerts :: CtLoc -> TcPredType -> TcS (Maybe CtEvidence)
 lookupInInerts loc pty
   | ClassPred cls tys <- classifyPredType pty
   = do { inerts <- getTcSInerts
-       ; return (lookupSolvedDict inerts loc cls tys `mplus`
-                 fmap ctEvidence (lookupInertDict (inert_cans inerts) loc cls tys)) }
+       ; 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 }}
   | otherwise -- NB: No caching for equalities, IPs, holes, or errors
   = return Nothing
 
@@ -783,7 +791,11 @@ data TcSEnv
     }
 
 ---------------
-newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a } deriving (Functor)
+newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a }
+  deriving (Functor)
+
+instance MonadFix TcS where
+  mfix k = TcS $ \env -> mfix (\x -> unTcS (k x) env)
 
 -- | Smart constructor for 'TcS', as describe in Note [The one-shot state
 -- monad trick] in "GHC.Utils.Monad".