Re-do superclass solving (again); fixes #10423

TcInstDcls.tcSuperClasses was getting increasingly baroque as a
succession of tickets (#10423 being the latest) pointed out that
my cunning plan was not so cunning.

The big issue is how to restrict the evidence that we generate
for superclass constraints in an instance declaration to avoid
superclass loops.  See Note [Recursive superclasses] in TcInstDcls
which explains the plan.

The question is how to implement the plan.  The new implementation is
much neater, and is described in Note [Solving superclass constraints]
in TcInstDcls.

7 files changed, 233 insertions, 231 deletions

diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index 1383bdd909..e5a7587113 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -320,7 +320,17 @@ newSCWorkFromFlavored flavor cls xis
   = return ()
 
   | CtGiven { ctev_evar = evar, ctev_loc = loc } <- flavor
-  = do { given_evs <- newGivenEvVars loc (mkEvScSelectors (EvId evar) cls xis)
+  = do { let size = sizePred (mkClassPred cls xis)
+             loc' = case ctLocOrigin loc of
+                       GivenOrigin InstSkol
+                         -> loc { ctl_origin = GivenOrigin (InstSC size) }
+                       GivenOrigin (InstSC n)
+                         -> loc { ctl_origin = GivenOrigin (InstSC (n `max` size)) }
+                       _ -> loc
+                    -- See Note [Solving superclass constraints] in TcInstDcls
+                    -- for explantation of loc'
+
+       ; given_evs <- newGivenEvVars loc' (mkEvScSelectors (EvId evar) cls xis)
        ; emitWorkNC given_evs }
 
   | isEmptyVarSet (tyVarsOfTypes xis)
diff --git a/compiler/typecheck/TcInstDcls.hs b/compiler/typecheck/TcInstDcls.hs
index de5df6ae53..f2607a4295 100644
--- a/compiler/typecheck/TcInstDcls.hs
+++ b/compiler/typecheck/TcInstDcls.hs
@@ -32,7 +32,7 @@ import TcDeriv
 import TcEnv
 import TcHsType
 import TcUnify
-import Coercion   ( pprCoAxiom, isReflCo, mkSymCo, mkSubCo )
+import Coercion   ( pprCoAxiom {- , isReflCo, mkSymCo, mkSubCo -} )
 import MkCore     ( nO_METHOD_BINDING_ERROR_ID )
 import Type
 import TcEvidence
@@ -43,8 +43,8 @@ import Class
 import Var
 import VarEnv
 import VarSet
-import PrelNames  ( typeableClassName, genericClassNames
-                  , knownNatClassName, knownSymbolClassName )
+import PrelNames  ( typeableClassName, genericClassNames )
+--                   , knownNatClassName, knownSymbolClassName )
 import Bag
 import BasicTypes
 import DynFlags
@@ -993,55 +993,15 @@ tcSuperClasses :: DFunId -> Class -> [TcTyVar] -> [EvVar] -> [TcType]
 -- See Note [Recursive superclasses] for why this is so hard!
 -- In effect, be build a special-purpose solver for the first step
 -- of solving each superclass constraint
-tcSuperClasses dfun_id cls tyvars dfun_evs inst_tys dfun_ev_binds fam_envs sc_theta
-  = do { traceTc "tcSuperClasses" (ppr cls $$ ppr inst_tys $$ ppr given_cls_preds)
-       ; (ids, binds, implics) <- mapAndUnzip3M tc_super (zip sc_theta [fIRST_TAG..])
+tcSuperClasses dfun_id cls tyvars dfun_evs inst_tys dfun_ev_binds _fam_envs sc_theta
+  = do { (ids, binds, implics) <- mapAndUnzip3M tc_super (zip sc_theta [fIRST_TAG..])
        ; return (ids, listToBag binds, listToBag implics) }
   where
-    loc     = getSrcSpan dfun_id
-    head_size = sizeTypes inst_tys
-
-    ------------
-    given_cls_preds :: [(TcPredType, EvTerm)] -- (type of that ev_term, ev_term)
-    -- given_cls_preds is the list of (type, ev_term) that can be derived
-    -- from the dfun_evs, using the rules (sc1) and (sc2) of
-    -- Note [Recursive superclasses] below
-    -- When solving for superclasses, we search this list
-    given_cls_preds
-      = [ ev_pr | dfun_ev <- dfun_evs
-                , ev_pr <- super_classes (idType dfun_ev, EvId dfun_ev) ]
-
-    ------------
-    super_classes ev_pair
-      = case classifyPredType pred of
-          ClassPred cls tys -> (pred, ev_tm) : super_classes_help ev_tm cls tys
-          _                 -> []
-      where
-        (pred, ev_tm) = normalise_pr ev_pair
-
-    ------------
-    super_classes_help :: EvTerm -> Class -> [TcType] -> [(TcPredType, EvTerm)]
-    super_classes_help ev_tm cls tys  -- ev_tm :: cls tys
-      | not (isCTupleClass cls)
-      , sizeTypes tys >= head_size  -- Here is where we test for
-      = []                          -- a smaller dictionary
-      | otherwise
-      = concatMap super_classes (mkEvScSelectors ev_tm cls tys)
-
-    ------------
-    normalise_pr :: (TcPredType, EvTerm) -> (TcPredType, EvTerm)
-    -- Normalise type functions as much as possible
-    normalise_pr (pred, ev_tm)
-      | isReflCo norm_co = (pred,      ev_tm)
-      | otherwise        = (norm_pred, mkEvCast ev_tm tc_co)
-      where
-        (norm_co, norm_pred) = normaliseType fam_envs Nominal pred
-        tc_co = TcCoercion (mkSubCo norm_co)
-
-    ------------
+    loc = getSrcSpan dfun_id
+    size = sizePred (mkClassPred cls inst_tys)
     tc_super (sc_pred, n)
-      = do { (sc_implic, sc_ev_id) <- checkInstConstraints $
-                                      emit_sc_pred fam_envs sc_pred
+      = do { (sc_implic, sc_ev_id) <- checkInstConstraints $ \_ ->
+                                      emitWanted (ScOrigin size) sc_pred
 
            ; sc_top_name <- newName (mkSuperDictAuxOcc n (getOccName cls))
            ; let sc_top_ty = mkForAllTys tyvars (mkPiTypes dfun_evs sc_pred)
@@ -1057,68 +1017,6 @@ tcSuperClasses dfun_id cls tyvars dfun_evs inst_tys dfun_ev_binds fam_envs sc_th
                                  , abs_binds    = emptyBag }
            ; return (sc_top_id, L loc bind, sc_implic) }
 
-    -------------------
-    emit_sc_pred fam_envs sc_pred ev_binds
-      | (sc_co, norm_sc_pred) <- normaliseType fam_envs Nominal sc_pred
-                                 -- sc_co :: sc_pred ~ norm_sc_pred
-      , ClassPred cls tys <- classifyPredType norm_sc_pred
-      , not (usesCustomSolver cls)
-        -- Some classes (e.g., `Typeable`, `KnownNat`) have custom solving
-        -- rules, which is why we exclude it from the short cut,
-        -- and fall through to calling the solver.
-
-      = do { sc_ev_tm <- emit_sc_cls_pred norm_sc_pred cls tys
-           ; sc_ev_id <- newEvVar sc_pred
-           ; let tc_co = TcCoercion (mkSubCo (mkSymCo sc_co))
-           ; addTcEvBind ev_binds (mkWantedEvBind sc_ev_id (mkEvCast sc_ev_tm tc_co))
-               -- This is where we set the evidence for the superclass, and do so
-               -- (very unusually) *outside the solver*.  That's why
-               -- checkInstConstraints passes in the evidence bindings
-           ; return sc_ev_id }
-
-      | otherwise
-      = do { sc_ev_id <- emitWanted ScOrigin sc_pred
-           ; traceTc "tcSuperClass 4" (ppr sc_pred $$ ppr sc_ev_id)
-           ; return sc_ev_id }
-
-    -------------------
-    emit_sc_cls_pred sc_pred cls tys
-      | (ev_tm:_) <- [ ev_tm | (ev_ty, ev_tm) <- given_cls_preds
-                             , ev_ty `tcEqType` sc_pred ]
-      = do { traceTc "tcSuperClass 1" (ppr sc_pred $$ ppr ev_tm)
-           ; return ev_tm }
-
-      | otherwise
-      = do { inst_envs <- tcGetInstEnvs
-           ; case lookupInstEnv False inst_envs cls tys of
-               ([(ispec, dfun_inst_tys)], [], _) -- A single match
-                 -> do { let dfun_id = instanceDFunId ispec
-                       ; (inst_tys, inst_theta) <- instDFunType dfun_id dfun_inst_tys
-                       ; arg_evs  <- emitWanteds ScOrigin inst_theta
-                       ; let dict_app = EvDFunApp dfun_id inst_tys arg_evs
-                       ; traceTc "tcSuperClass 2" (ppr sc_pred $$ ppr dict_app)
-                       ; return dict_app }
-
-               _ -> -- No instance, so we want to report an error
-                    -- Emitting it as an 'insoluble' prevents the solver
-                    -- attempting to solve it (which might, wrongly, succeed)
-                    do { sc_ev <- newWanted ScOrigin sc_pred
-                       ; emitInsoluble (mkNonCanonical sc_ev)
-                       ; traceTc "tcSuperClass 3" (ppr sc_pred $$ ppr sc_ev)
-                       ; return (ctEvTerm sc_ev) } }
-
-
-
--- | Do we use a custom solver, which is safe to use when solving super-class
--- constraints.
-usesCustomSolver :: Class -> Bool
-usesCustomSolver cls = name == typeableClassName
-                    || name == knownNatClassName
-                    || name == knownSymbolClassName
-  where
-  name = className cls
-
-
 -------------------
 checkInstConstraints :: (EvBindsVar -> TcM result)
                      -> TcM (Implication, result)
@@ -1153,7 +1051,6 @@ encountered in practice.
 
 See also tests tcrun020, tcrun021, tcrun033
 
-
 ----- THE PROBLEM --------
 The problem is that it is all too easy to create a class whose
 superclass is bottom when it should not be.
@@ -1239,8 +1136,39 @@ that is *not* smaller than the target so we can't take *its*
 superclasses.  As a result the program is rightly rejected, unless you
 add (Super (Fam a)) to the context of (i3).
 
-Note [Silent superclass arguments] (historical interest)
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Note [Solving superclass constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+How do we ensure that every superclass witness is generated by
+one of (sc1) (sc2) or (sc3) in Note [Recursive superclases].
+Answer:
+
+  * Superclass "wanted" constraints have CtOrigin of (ScOrigin size)
+    where 'size' is the size of the instance declaration. e.g.
+          class C a => D a where...
+          instance blah => D [a] where ...
+    The wanted superclass constraint for C [a] has origin
+    ScOrigin size, where size = size( D [a] ).
+
+  * (sc1) When we rewrite such a wanted constraint, it retains its
+    origin.  But if we apply an instance declaration, we can set the
+    origin to (ScOrigin infinity), thus lifting any restrictions by
+    making prohibitedSuperClassSolve return False.
+
+  * (sc2) ScOrigin wanted constraints can't be solved from a
+    superclass selection, except at a smaller type.  This test is
+    implemented by TcInteract.prohibitedSuperClassSolve
+
+  * The "given" constraints of an instance decl have CtOrigin
+    GivenOrigin InstSkol.
+
+  * When we make a superclass selection from InstSkol we use
+    a SkolemInfo of (InstSC size), where 'size' is the size of
+    the constraint whose superclass we are taking.  An similarly
+    when taking the superclass of an InstSC.  This is implemented
+    in TcCanonical.newSCWorkFromFlavored
+
+Note [Silent superclass arguments] (historical interest only)
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 NB1: this note describes our *old* solution to the
      recursive-superclass problem. I'm keeping the Note
      for now, just as institutional memory.
diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs
index 18a798fc62..5a550b4530 100644
--- a/compiler/typecheck/TcInteract.hs
+++ b/compiler/typecheck/TcInteract.hs
@@ -8,7 +8,7 @@ module TcInteract (
 
 #include "HsVersions.h"
 
-import BasicTypes ()
+import BasicTypes ( infinity )
 import HsTypes ( hsIPNameFS )
 import FastString
 import TcCanonical
@@ -762,11 +762,21 @@ solveOneFromTheOther ev_i ev_w
                    -- so it's safe to continue on from this point
   = return (IRDelete, False)
 
-  | CtWanted { ctev_evar = ev_id } <- ev_w
+  | CtWanted { ctev_loc = loc_w } <- ev_w
+  , prohibitedSuperClassSolve (ctEvLoc ev_i) loc_w
+  = return (IRDelete, False)
+
+  | CtWanted { ctev_evar = ev_id } <- ev_w   -- Inert is Given or Wanted
   = do { setWantedEvBind ev_id (ctEvTerm ev_i)
        ; return (IRKeep, True) }
 
-  | CtWanted { ctev_evar = ev_id } <- ev_i
+  | CtWanted { ctev_loc = loc_i } <- ev_i   -- Work item is Given
+  , prohibitedSuperClassSolve (ctEvLoc ev_w) loc_i
+  = return (IRKeep, False)  -- Just discard the un-usable Given
+                            -- This never actually happens because
+                            -- Givens get processed first
+
+  | CtWanted { ctev_evar = ev_id } <- ev_i   -- Work item is Given
   = do { setWantedEvBind ev_id (ctEvTerm ev_w)
        ; return (IRReplace, True) }
 
@@ -774,51 +784,84 @@ solveOneFromTheOther ev_i ev_w
   -- See Note [Replacement vs keeping]
   | lvl_i == lvl_w
   = do { binds <- getTcEvBindsMap
-       ; if has_binding binds ev_w && not (has_binding binds ev_i)
-         then return (IRReplace, True)
-         else return (IRKeep,    True) }
+       ; return (same_level_strategy binds, True) }
 
-   | otherwise   -- Both are Given
-   = return (if use_replacement then IRReplace else IRKeep, True)
-   where
+  | otherwise   -- Both are Given, levels differ
+  = return (different_level_strategy, True)
+  where
      pred  = ctEvPred ev_i
      loc_i = ctEvLoc ev_i
      loc_w = ctEvLoc ev_w
      lvl_i = ctLocLevel loc_i
      lvl_w = ctLocLevel loc_w
 
+     different_level_strategy
+       | isIPPred pred, lvl_w > lvl_i = IRReplace
+       | lvl_w < lvl_i                = IRReplace
+       | otherwise                    = IRKeep
+
+     same_level_strategy binds        -- Both Given
+       | GivenOrigin (InstSC s_i) <- ctLocOrigin loc_i
+       = case ctLocOrigin loc_w of
+            GivenOrigin (InstSC s_w) | s_w < s_i -> IRReplace
+                                     | otherwise -> IRKeep
+            _                                    -> IRReplace
+
+       | GivenOrigin (InstSC {}) <- ctLocOrigin loc_w
+       = IRKeep
+
+       | has_binding binds ev_w
+       , not (has_binding binds ev_i)
+       = IRReplace
+
+       | otherwise = IRKeep
+
      has_binding binds ev = isJust (lookupEvBind binds (ctEvId ev))
 
-     use_replacement
-       | isIPPred pred = lvl_w > lvl_i
-       | otherwise     = lvl_w < lvl_i
+prohibitedSuperClassSolve :: CtLoc -> CtLoc -> Bool
+-- See Note [Solving superclass constraints] in TcInstDcls
+prohibitedSuperClassSolve from_loc solve_loc
+  | GivenOrigin (InstSC given_size) <- ctLocOrigin from_loc
+  , ScOrigin wanted_size <- ctLocOrigin solve_loc
+  = given_size >= wanted_size
+  | otherwise
+  = False
 
 {-
 Note [Replacement vs keeping]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 When we have two Given constraints both of type (C tys), say, which should
-we keep?
+we keep?  More subtle than you might think!
 
-  * For implicit parameters we want to keep the innermost (deepest)
-    one, so that it overrides the outer one.
-    See Note [Shadowing of Implicit Parameters]
+  * Constraints come from different levels (different_level_strategy)
 
-  * For everything else, we want to keep the outermost one.  Reason: that
-    makes it more likely that the inner one will turn out to be unused,
-    and can be reported as redundant.  See Note [Tracking redundant constraints]
-    in TcSimplify.
+      - For implicit parameters we want to keep the innermost (deepest)
+        one, so that it overrides the outer one.
+        See Note [Shadowing of Implicit Parameters]
 
-    It transpires that using the outermost one is reponsible for an
-    8% performance improvement in nofib cryptarithm2, compared to
-    just rolling the dice.  I didn't investigate why.
+      - For everything else, we want to keep the outermost one.  Reason: that
+        makes it more likely that the inner one will turn out to be unused,
+        and can be reported as redundant.  See Note [Tracking redundant constraints]
+        in TcSimplify.
 
-  * If there is no "outermost" one, we keep the one that has a non-trivial
-    evidence binding.  Note [Tracking redundant constraints] again.
-    Example:  f :: (Eq a, Ord a) => blah
-    then we may find [G] sc_sel (d1::Ord a) :: Eq a
-                     [G] d2 :: Eq a
-    We want to discard d2 in favour of the superclass selection from
-    the Ord dictionary.
+        It transpires that using the outermost one is reponsible for an
+        8% performance improvement in nofib cryptarithm2, compared to
+        just rolling the dice.  I didn't investigate why.
+
+  * Constaints coming from the same level (i.e. same implication)
+
+       - Always get rid of InstSC ones if possible, since they are less
+         useful for solving.  If both are InstSC, choose the one with
+         the smallest TypeSize
+         See Note [Solving superclass constraints] in TcInstDcls
+
+       - Keep the one that has a non-trivial evidence binding.
+         Note [Tracking redundant constraints] again.
+            Example:  f :: (Eq a, Ord a) => blah
+            then we may find [G] sc_sel (d1::Ord a) :: Eq a
+                             [G] d2 :: Eq a
+            We want to discard d2 in favour of the superclass selection from
+            the Ord dictionary.
 
   * Finally, when there is still a choice, use IRKeep rather than
     IRReplace, to avoid unnecesary munging of the inert set.
@@ -1595,7 +1638,14 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls
      dict_pred   = mkClassPred cls xis
      dict_loc    = ctEvLoc fl
      dict_origin = ctLocOrigin dict_loc
-     deeper_loc  = bumpCtLocDepth dict_loc
+     deeper_loc  = zap_origin (bumpCtLocDepth dict_loc)
+
+     zap_origin loc  -- After applying an instance we can set ScOrigin to
+                     -- infinity, so that prohibitedSuperClassSolve never fires
+       | ScOrigin {} <- dict_origin
+       = setCtLocOrigin loc (ScOrigin infinity)
+       | otherwise
+       = loc
 
      solve_from_instance :: [TcPredType] -> ([EvId] -> EvTerm) -> TcS (StopOrContinue Ct)
       -- Precondition: evidence term matches the predicate workItem
@@ -1992,7 +2042,7 @@ matchClassInst :: DynFlags -> InertSet -> Class -> [Type] -> CtLoc -> TcS Lookup
 -- First check whether there is an in-scope Given that could
 -- match this constraint.  In that case, do not use top-level
 -- instances.  See Note [Instance and Given overlap]
-matchClassInst dflags inerts clas tys _
+matchClassInst dflags inerts clas tys loc
   | not (xopt Opt_IncoherentInstances dflags)
   , not (isEmptyBag matchable_givens)
   = do { traceTcS "Delaying instance application" $
@@ -2007,8 +2057,9 @@ matchClassInst dflags inerts clas tys _
 
      matchable_given ct
        | CDictCan { cc_class = clas_g, cc_tyargs = sys, cc_ev = fl } <- ct
-       , isGiven fl
+       , CtGiven { ctev_loc = loc_g } <- fl
        , Just {} <- tcUnifyTys bind_meta_tv tys sys
+       , not (prohibitedSuperClassSolve loc_g loc)
        = ASSERT( clas_g == clas ) True
      matchable_given _ = False
 
diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs
index 5262e186f0..a70759fa7d 100644
--- a/compiler/typecheck/TcRnTypes.hs
+++ b/compiler/typecheck/TcRnTypes.hs
@@ -1966,7 +1966,13 @@ data SkolemInfo
 
         -- The rest are for non-scoped skolems
   | ClsSkol Class       -- Bound at a class decl
+
   | InstSkol            -- Bound at an instance decl
+  | InstSC TypeSize     -- A "given" constraint obtained by superclass selection
+                        -- from an InstSkol, giving the largest class from
+                        -- which we made a superclass selection in the chain
+                        -- See Note [Solving superclass constraints] in TcInstDcls
+
   | DataSkol            -- Bound at a data type declaration
   | FamInstSkol         -- Bound at a family instance decl
   | PatSkol             -- An existential type variable bound by a pattern for
@@ -2006,6 +2012,7 @@ pprSkolInfo (IPSkol ips)      = ptext (sLit "the implicit-parameter binding") <>
                                 <+> pprWithCommas ppr ips
 pprSkolInfo (ClsSkol cls)     = ptext (sLit "the class declaration for") <+> quotes (ppr cls)
 pprSkolInfo InstSkol          = ptext (sLit "the instance declaration")
+pprSkolInfo (InstSC n)        = ptext (sLit "the instance declaration") <> ifPprDebug (parens (ppr n))
 pprSkolInfo DataSkol          = ptext (sLit "a data type declaration")
 pprSkolInfo FamInstSkol       = ptext (sLit "a family instance declaration")
 pprSkolInfo BracketSkol       = ptext (sLit "a Template Haskell bracket")
@@ -2087,7 +2094,10 @@ data CtOrigin
   | RecordUpdOrigin
   | ViewPatOrigin
 
-  | ScOrigin            -- Typechecking superclasses of an instance declaration
+  | ScOrigin TypeSize   -- Typechecking superclasses of an instance declaration
+                        -- whose head has the given size
+                        -- See Note [Solving superclass constraints] in TcInstDcls
+
   | DerivOrigin         -- Typechecking deriving
   | DerivOriginDC DataCon Int
                         -- Checking constraints arising from this data con and field index
@@ -2186,7 +2196,8 @@ pprCtO (PArrSeqOrigin seq)   = hsep [ptext (sLit "the parallel array sequence"),
 pprCtO SectionOrigin         = ptext (sLit "an operator section")
 pprCtO TupleOrigin           = ptext (sLit "a tuple")
 pprCtO NegateOrigin          = ptext (sLit "a use of syntactic negation")
-pprCtO ScOrigin              = ptext (sLit "the superclasses of an instance declaration")
+pprCtO (ScOrigin n)          = ptext (sLit "the superclasses of an instance declaration") 
+                               <> ifPprDebug (parens (ppr n))
 pprCtO DerivOrigin           = ptext (sLit "the 'deriving' clause of a data type declaration")
 pprCtO StandAloneDerivOrigin = ptext (sLit "a 'deriving' declaration")
 pprCtO DefaultOrigin         = ptext (sLit "a 'default' declaration")
diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs
index ee0740f8e4..4deba5b15e 100644
--- a/compiler/typecheck/TcSimplify.hs
+++ b/compiler/typecheck/TcSimplify.hs
@@ -1074,8 +1074,8 @@ warnRedundantGivens (SigSkol ctxt _)
        FunSigCtxt _ warn_redundant -> warn_redundant
        ExprSigCtxt                 -> True
        _                           -> False
-warnRedundantGivens InstSkol = True
-warnRedundantGivens _        = False
+warnRedundantGivens (InstSkol {}) = True
+warnRedundantGivens _             = False
 
 neededEvVars :: EvBindMap -> VarSet -> VarSet
 -- Find all the evidence variables that are "needed",
diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index 9ce14497b7..208441bdda 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -146,7 +146,9 @@ module TcType (
 
   pprKind, pprParendKind, pprSigmaType,
   pprType, pprParendType, pprTypeApp, pprTyThingCategory,
-  pprTheta, pprThetaArrowTy, pprClassPred
+  pprTheta, pprThetaArrowTy, pprClassPred,
+
+  TypeSize, sizePred, sizeType, sizeTypes
 
   ) where
 
@@ -1793,3 +1795,80 @@ In turn that means you can't write
 Reason: the back end falls over with panic "primRepHint:VoidRep";
         and there is no compelling reason to permit it
 -}
+
+{-
+************************************************************************
+*                                                                      *
+        The "Paterson size" of a type
+*                                                                      *
+************************************************************************
+-}
+
+{-
+Note [Paterson conditions on PredTypes]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We are considering whether *class* constraints terminate
+(see Note [Paterson conditions]). Precisely, the Paterson conditions
+would have us check that "the constraint has fewer constructors and variables
+(taken together and counting repetitions) than the head.".
+
+However, we can be a bit more refined by looking at which kind of constraint
+this actually is. There are two main tricks:
+
+ 1. It seems like it should be OK not to count the tuple type constructor
+    for a PredType like (Show a, Eq a) :: Constraint, since we don't
+    count the "implicit" tuple in the ThetaType itself.
+
+    In fact, the Paterson test just checks *each component* of the top level
+    ThetaType against the size bound, one at a time. By analogy, it should be
+    OK to return the size of the *largest* tuple component as the size of the
+    whole tuple.
+
+ 2. Once we get into an implicit parameter or equality we
+    can't get back to a class constraint, so it's safe
+    to say "size 0".  See Trac #4200.
+
+NB: we don't want to detect PredTypes in sizeType (and then call
+sizePred on them), or we might get an infinite loop if that PredType
+is irreducible. See Trac #5581.
+-}
+
+type TypeSize = IntWithInf
+
+sizeType :: Type -> TypeSize
+-- Size of a type: the number of variables and constructors
+sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
+sizeType (TyVarTy {})      = 1
+sizeType (TyConApp tc tys)
+  | isTypeFamilyTyCon tc   = infinity  -- Type-family applications can
+                                       -- expand to any arbitrary size
+  | otherwise              = sizeTypes tys + 1
+sizeType (LitTy {})        = 1
+sizeType (FunTy arg res)   = sizeType arg + sizeType res + 1
+sizeType (AppTy fun arg)   = sizeType fun + sizeType arg
+sizeType (ForAllTy _ ty)   = sizeType ty
+
+sizeTypes :: [Type] -> TypeSize
+-- IA0_NOTE: Avoid kinds.
+sizeTypes xs = sum (map sizeType tys)
+  where tys = filter (not . isKind) xs
+
+-- Note [Size of a predicate]
+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~
+-- We are considering whether class constraints terminate.
+-- Equality constraints and constraints for the implicit
+-- parameter class always termiante so it is safe to say "size 0".
+-- (Implicit parameter constraints always terminate because
+-- there are no instances for them---they are only solved by
+-- "local instances" in expressions).
+-- See Trac #4200.
+sizePred :: PredType -> TypeSize
+sizePred p
+  = case classifyPredType p of
+      ClassPred cls tys
+        | isIPClass cls     -> 0  -- See Note [Size of a predicate]
+        | isCTupleClass cls -> maximum (0 : map sizePred tys)
+        | otherwise         -> sizeTypes tys
+      EqPred {}             -> 0  -- See Note [Size of a predicate]
+      IrredPred ty          -> sizeType ty
+
diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index 370cad2e2d..826b3093e4 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -11,7 +11,7 @@ module TcValidity (
   checkValidTheta, checkValidFamPats,
   checkValidInstance, validDerivPred,
   checkInstTermination, checkValidTyFamInst, checkTyFamFreeness,
-  checkConsistentFamInst, sizeTypes,
+  checkConsistentFamInst,
   arityErr, badATErr
   ) where
 
@@ -45,7 +45,6 @@ import Util
 import ListSetOps
 import SrcLoc
 import Outputable
-import BasicTypes       ( IntWithInf, infinity )
 import FastString
 
 import Control.Monad
@@ -1298,82 +1297,6 @@ famPatErr fam_tc tvs pats
 {-
 ************************************************************************
 *                                                                      *
-        The "Paterson size" of a type
-*                                                                      *
-************************************************************************
--}
-
-{-
-Note [Paterson conditions on PredTypes]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We are considering whether *class* constraints terminate
-(see Note [Paterson conditions]). Precisely, the Paterson conditions
-would have us check that "the constraint has fewer constructors and variables
-(taken together and counting repetitions) than the head.".
-
-However, we can be a bit more refined by looking at which kind of constraint
-this actually is. There are two main tricks:
-
- 1. It seems like it should be OK not to count the tuple type constructor
-    for a PredType like (Show a, Eq a) :: Constraint, since we don't
-    count the "implicit" tuple in the ThetaType itself.
-
-    In fact, the Paterson test just checks *each component* of the top level
-    ThetaType against the size bound, one at a time. By analogy, it should be
-    OK to return the size of the *largest* tuple component as the size of the
-    whole tuple.
-
- 2. Once we get into an implicit parameter or equality we
-    can't get back to a class constraint, so it's safe
-    to say "size 0".  See Trac #4200.
-
-NB: we don't want to detect PredTypes in sizeType (and then call
-sizePred on them), or we might get an infinite loop if that PredType
-is irreducible. See Trac #5581.
--}
-
-type TypeSize = IntWithInf
-
-sizeType :: Type -> TypeSize
--- Size of a type: the number of variables and constructors
-sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
-sizeType (TyVarTy {})      = 1
-sizeType (TyConApp tc tys)
-  | isTypeFamilyTyCon tc   = infinity  -- Type-family applications can
-                                       -- expand to any arbitrary size
-  | otherwise              = sizeTypes tys + 1
-sizeType (LitTy {})        = 1
-sizeType (FunTy arg res)   = sizeType arg + sizeType res + 1
-sizeType (AppTy fun arg)   = sizeType fun + sizeType arg
-sizeType (ForAllTy _ ty)   = sizeType ty
-
-sizeTypes :: [Type] -> TypeSize
--- IA0_NOTE: Avoid kinds.
-sizeTypes xs = sum (map sizeType tys)
-  where tys = filter (not . isKind) xs
-
--- Note [Size of a predicate]
--- ~~~~~~~~~~~~~~~~~~~~~~~~~~
--- We are considering whether class constraints terminate.
--- Equality constraints and constraints for the implicit
--- parameter class always termiante so it is safe to say "size 0".
--- (Implicit parameter constraints always terminate because
--- there are no instances for them---they are only solved by
--- "local instances" in expressions).
--- See Trac #4200.
-sizePred :: PredType -> TypeSize
-sizePred p
-  = case classifyPredType p of
-      ClassPred cls tys
-        | isIPClass cls     -> 0  -- See Note [Size of a predicate]
-        | isCTupleClass cls -> maximum (0 : map sizePred tys)
-        | otherwise         -> sizeTypes tys
-      EqPred {}             -> 0  -- See Note [Size of a predicate]
-      IrredPred ty          -> sizeType ty
-
-{-
-************************************************************************
-*                                                                      *
 \subsection{Auxiliary functions}
 *                                                                      *
 ************************************************************************