Kill derived constraints

Co-authored by: Sam Derbyshire

Previously, GHC had three flavours of constraint:
Wanted, Given, and Derived. This removes Derived constraints.

Though serving a number of purposes, the most important role
of Derived constraints was to enable better error messages.
This job has been taken over by the new RewriterSets, as explained
in Note [Wanteds rewrite wanteds] in GHC.Tc.Types.Constraint.

Other knock-on effects:
 - Various new Notes as I learned about under-described bits of GHC

 - A reshuffling around the AST for implicit-parameter bindings,
   with better integration with TTG.

 - Various improvements around fundeps. These were caused by the
   fact that, previously, fundep constraints were all Derived,
   and Derived constraints would get dropped. Thus, an unsolved
   Derived didn't stop compilation. Without Derived, this is no
   longer possible, and so we have to be considerably more careful
   around fundeps.

 - A nice little refactoring in GHC.Tc.Errors to center the work
   on a new datatype called ErrorItem. Constraints are converted
   into ErrorItems at the start of processing, and this allows for
   a little preprocessing before the main classification.

 - This commit also cleans up the behavior in generalisation around
   functional dependencies. Now, if a variable is determined by
   functional dependencies, it will not be quantified. This change
   is user facing, but it should trim down GHC's strange behavior
   around fundeps.

 - Previously, reportWanteds did quite a bit of work, even on an empty
   WantedConstraints. This commit adds a fast path.

 - Now, GHC will unconditionally re-simplify constraints during
   quantification. See Note [Unconditionally resimplify constraints when
   quantifying], in GHC.Tc.Solver.

Close #18398.
Close #18406.
Solve the fundep-related non-confluence in #18851.
Close #19131.
Close #19137.
Close #20922.
Close #20668.
Close #19665.

-------------------------
Metric Decrease:
    LargeRecord
    T9872b
    T9872b_defer
    T9872d
    TcPlugin_RewritePerf
-------------------------

5 files changed, 187 insertions, 134 deletions

diff --git a/compiler/GHC/Tc/Errors/Hole.hs b/compiler/GHC/Tc/Errors/Hole.hs
index 4115d6b198..079bbd5df5 100644
--- a/compiler/GHC/Tc/Errors/Hole.hs
+++ b/compiler/GHC/Tc/Errors/Hole.hs
@@ -18,7 +18,7 @@ module GHC.Tc.Errors.Hole
    , getHoleFitDispConfig
    , HoleFitDispConfig (..)
    , HoleFitSortingAlg (..)
-   , relevantCts
+   , relevantCtEvidence
    , zonkSubs
 
    , sortHoleFitsByGraph
@@ -68,7 +68,8 @@ import Data.List        ( partition, sort, sortOn, nubBy )
 import Data.Graph       ( graphFromEdges, topSort )
 
 
-import GHC.Tc.Solver    ( simplifyTopWanteds, runTcSDerivedsEarlyAbort )
+import GHC.Tc.Solver    ( simplifyTopWanteds )
+import GHC.Tc.Solver.Monad ( runTcSEarlyAbort )
 import GHC.Tc.Utils.Unify ( tcSubTypeSigma )
 
 import GHC.HsToCore.Docs ( extractDocs )
@@ -189,7 +190,7 @@ Here the nested implications are just one level deep, namely:
       Given = $dShow_a1pc :: Show a_a1pa[sk:2]
       Wanted =
         WC {wc_simple =
-              [WD] $dShow_a1pe {0}:: Show a0_a1pd[tau:2] (CDictCan(psc))}
+              [W] $dShow_a1pe {0}:: Show a0_a1pd[tau:2] (CDictCan(psc))}
       Binds = EvBindsVar<a1pi>
       Needed inner = []
       Needed outer = []
@@ -218,7 +219,7 @@ needing to check whether the following constraints are soluble.
           Given = $dShow_a1pc :: Show a_a1pa[sk:2]
           Wanted =
             WC {wc_simple =
-                  [WD] $dShow_a1pe {0}:: Show a0_a1pd[tau:2] (CNonCanonical)}
+                  [W] $dShow_a1pe {0}:: Show a0_a1pd[tau:2] (CNonCanonical)}
           Binds = EvBindsVar<a1pl>
           Needed inner = []
           Needed outer = []
@@ -361,7 +362,7 @@ as is the case in
 
 Here, the hole is given type a0_a1kv[tau:1]. Then, the emitted constraint is:
 
-  [WD] $dShow_a1kw {0}:: Show a0_a1kv[tau:1] (CNonCanonical)
+  [W] $dShow_a1kw {0}:: Show a0_a1kv[tau:1] (CNonCanonical)
 
 However, when there are multiple holes, we need to be more careful. As an
 example, Let's take a look at the following code:
@@ -373,8 +374,8 @@ Here there are two holes, `_a` and `_b`. Suppose _a :: a0_a1pd[tau:2] and
 _b :: a1_a1po[tau:2]. Then, the simple constraints passed to
 findValidHoleFits are:
 
-  [[WD] $dShow_a1pe {0}:: Show a0_a1pd[tau:2] (CNonCanonical),
-    [WD] $dShow_a1pp {0}:: Show a1_a1po[tau:2] (CNonCanonical)]
+  [[W] $dShow_a1pe {0}:: Show a0_a1pd[tau:2] (CNonCanonical),
+    [W] $dShow_a1pp {0}:: Show a1_a1po[tau:2] (CNonCanonical)]
 
 When we are looking for a match for the hole `_a`, we filter the simple
 constraints to the "Relevant constraints", by throwing out any constraints
@@ -402,9 +403,9 @@ a constraint to show that `hole_ty ~ ty`, including any constraints in `ty`. For
 example, if `hole_ty = Int` and `ty = Foldable t => (a -> Bool) -> t a -> Bool`,
 we'd have `(a_a1pa[sk:1] -> Bool) -> t_t2jk[sk:1] a_a1pa[sk:1] -> Bool ~# Int`
 from the coercion, as well as `Foldable t_t2jk[sk:1]`. By adding a flag to
-`TcSEnv` and adding a `runTcSDerivedsEarlyAbort`, we can fail as soon as we hit
+`TcSEnv` and adding a `runTcSEarlyAbort`, we can fail as soon as we hit
 an insoluble constraint. Since we don't need the result in the case that it
-fails, a boolean `False` (i.e. "it didn't work" from `runTcSDerivedsEarlyAbort`)
+fails, a boolean `False` (i.e. "it didn't work" from `runTcSEarlyAbort`)
 is sufficient.
 
 We also check whether the type of the hole is an immutable type variable (i.e.
@@ -552,7 +553,7 @@ getLocalBindings tidy_orig ct_loc
 -- See Note [Valid hole fits include ...]
 findValidHoleFits :: TidyEnv        -- ^ The tidy_env for zonking
                   -> [Implication]  -- ^ Enclosing implications for givens
-                  -> [Ct]
+                  -> [CtEvidence]
                   -- ^ The  unsolved simple constraints in the implication for
                   -- the hole.
                   -> Hole
@@ -569,7 +570,7 @@ findValidHoleFits tidy_env implics simples h@(Hole { hole_sort = ExprHole _
      ; let findVLimit = if sortingAlg > HFSNoSorting then Nothing else maxVSubs
            refLevel = refLevelHoleFits dflags
            hole = TypedHole { th_relevant_cts =
-                                listToBag (relevantCts hole_ty simples)
+                                listToBag (relevantCtEvidence hole_ty simples)
                             , th_implics      = implics
                             , th_hole         = Just h }
            (candidatePlugins, fitPlugins) =
@@ -690,21 +691,20 @@ findValidHoleFits tidy_env implics simples h@(Hole { hole_sort = ExprHole _
 findValidHoleFits env _ _ _ = return (env, noValidHoleFits)
 
 -- See Note [Relevant constraints]
-relevantCts :: Type -> [Ct] -> [Ct]
-relevantCts hole_ty simples = if isEmptyVarSet (fvVarSet hole_fvs) then []
-                              else filter isRelevant simples
-  where ctFreeVarSet :: Ct -> VarSet
-        ctFreeVarSet = fvVarSet . tyCoFVsOfType . ctPred
-        hole_fvs = tyCoFVsOfType hole_ty
+relevantCtEvidence :: Type -> [CtEvidence] -> [CtEvidence]
+relevantCtEvidence hole_ty simples
+  = if isEmptyVarSet (fvVarSet hole_fvs)
+    then []
+    else filter isRelevant simples
+  where hole_fvs = tyCoFVsOfType hole_ty
         hole_fv_set = fvVarSet hole_fvs
-        anyFVMentioned :: Ct -> Bool
-        anyFVMentioned ct = ctFreeVarSet ct `intersectsVarSet` hole_fv_set
         -- We filter out those constraints that have no variables (since
         -- they won't be solved by finding a type for the type variable
         -- representing the hole) and also other holes, since we're not
         -- trying to find hole fits for many holes at once.
-        isRelevant ct = not (isEmptyVarSet (ctFreeVarSet ct))
-                        && anyFVMentioned ct
+        isRelevant ctev = not (isEmptyVarSet fvs) &&
+                          (fvs `intersectsVarSet` hole_fv_set)
+          where fvs = tyCoVarsOfCtEv ctev
 
 -- We zonk the hole fits so that the output aligns with the rest
 -- of the typed hole error message output.
@@ -962,7 +962,7 @@ tcCheckHoleFit (TypedHole {..}) hole_ty ty = discardErrs $
                           -- imp is the innermost implication
                           (imp:_) -> return (ic_tclvl imp)
      ; (wrap, wanted) <- setTcLevel innermost_lvl $ captureConstraints $
-                         tcSubTypeSigma (ExprSigCtxt NoRRC) ty hole_ty
+                         tcSubTypeSigma orig (ExprSigCtxt NoRRC) ty hole_ty
      ; traceTc "Checking hole fit {" empty
      ; traceTc "wanteds are: " $ ppr wanted
      ; if isEmptyWC wanted && isEmptyBag th_relevant_cts
@@ -971,11 +971,12 @@ tcCheckHoleFit (TypedHole {..}) hole_ty ty = discardErrs $
        else do { fresh_binds <- newTcEvBinds
                 -- The relevant constraints may contain HoleDests, so we must
                 -- take care to clone them as well (to avoid #15370).
-               ; cloned_relevants <- mapBagM cloneWanted th_relevant_cts
+               ; cloned_relevants <- mapBagM cloneWantedCtEv th_relevant_cts
                  -- We wrap the WC in the nested implications, for details, see
                  -- Note [Checking hole fits]
                ; let wrapInImpls cts = foldl (flip (setWCAndBinds fresh_binds)) cts th_implics
-                     final_wc  = wrapInImpls $ addSimples wanted cloned_relevants
+                     final_wc  = wrapInImpls $ addSimples wanted $
+                                                          mapBag mkNonCanonical cloned_relevants
                  -- We add the cloned relevants to the wanteds generated
                  -- by the call to tcSubType_NC, for details, see
                  -- Note [Relevant constraints]. There's no need to clone
@@ -983,14 +984,15 @@ tcCheckHoleFit (TypedHole {..}) hole_ty ty = discardErrs $
                  -- call to`tcSubtype_NC`.
                ; traceTc "final_wc is: " $ ppr final_wc
                  -- See Note [Speeding up valid hole-fits]
-               ; (rem, _) <- tryTc $ runTcSDerivedsEarlyAbort $ simplifyTopWanteds final_wc
+               ; (rem, _) <- tryTc $ runTcSEarlyAbort $ simplifyTopWanteds final_wc
                ; traceTc "}" empty
-               ; return (any isSolvedWC rem, wrap)
-               } }
-     where
-       setWCAndBinds :: EvBindsVar         -- Fresh ev binds var.
-                     -> Implication        -- The implication to put WC in.
-                     -> WantedConstraints  -- The WC constraints to put implic.
-                     -> WantedConstraints  -- The new constraints.
-       setWCAndBinds binds imp wc
-         = mkImplicWC $ unitBag $ imp { ic_wanted = wc , ic_binds = binds }
+               ; return (any isSolvedWC rem, wrap) } }
+  where
+    orig = ExprHoleOrigin (hole_occ <$> th_hole)
+
+    setWCAndBinds :: EvBindsVar         -- Fresh ev binds var.
+                  -> Implication        -- The implication to put WC in.
+                  -> WantedConstraints  -- The WC constraints to put implic.
+                  -> WantedConstraints  -- The new constraints.
+    setWCAndBinds binds imp wc
+      = mkImplicWC $ unitBag $ imp { ic_wanted = wc , ic_binds = binds }
diff --git a/compiler/GHC/Tc/Errors/Hole.hs-boot b/compiler/GHC/Tc/Errors/Hole.hs-boot
index 94d3f51c58..7bb50eb825 100644
--- a/compiler/GHC/Tc/Errors/Hole.hs-boot
+++ b/compiler/GHC/Tc/Errors/Hole.hs-boot
@@ -7,18 +7,18 @@ module GHC.Tc.Errors.Hole where
 import GHC.Types.Var ( Id )
 import GHC.Tc.Errors.Types ( HoleFitDispConfig, ValidHoleFits )
 import GHC.Tc.Types  ( TcM )
-import GHC.Tc.Types.Constraint ( Ct, CtLoc, Hole, Implication )
+import GHC.Tc.Types.Constraint ( CtEvidence, CtLoc, Hole, Implication )
 import GHC.Utils.Outputable ( SDoc )
 import GHC.Types.Var.Env ( TidyEnv )
 import GHC.Tc.Errors.Hole.FitTypes ( HoleFit, TypedHole, HoleFitCandidate )
-import GHC.Tc.Utils.TcType ( TcType, TcSigmaType, Type, TcTyVar )
+import GHC.Tc.Utils.TcType ( TcType, TcSigmaType, TcTyVar )
 import GHC.Tc.Types.Evidence ( HsWrapper )
 import GHC.Utils.FV ( FV )
 import Data.Bool ( Bool )
 import Data.Maybe ( Maybe )
 import Data.Int ( Int )
 
-findValidHoleFits :: TidyEnv -> [Implication] -> [Ct] -> Hole
+findValidHoleFits :: TidyEnv -> [Implication] -> [CtEvidence] -> Hole
                   -> TcM (TidyEnv, ValidHoleFits)
 
 tcCheckHoleFit :: TypedHole -> TcSigmaType -> TcSigmaType
@@ -37,7 +37,6 @@ pprHoleFit :: HoleFitDispConfig -> HoleFit -> SDoc
 getHoleFitSortingAlg :: TcM HoleFitSortingAlg
 getHoleFitDispConfig :: TcM HoleFitDispConfig
 
-relevantCts :: Type -> [Ct] -> [Ct]
 zonkSubs :: TidyEnv -> [HoleFit] -> TcM (TidyEnv, [HoleFit])
 sortHoleFitsBySize :: [HoleFit] -> TcM [HoleFit]
 sortHoleFitsByGraph :: [HoleFit] -> TcM [HoleFit]
diff --git a/compiler/GHC/Tc/Errors/Hole/FitTypes.hs b/compiler/GHC/Tc/Errors/Hole/FitTypes.hs
index 70a655db45..077bdaab18 100644
--- a/compiler/GHC/Tc/Errors/Hole/FitTypes.hs
+++ b/compiler/GHC/Tc/Errors/Hole/FitTypes.hs
@@ -19,15 +19,17 @@ import GHC.Types.Id
 import GHC.Utils.Outputable
 import GHC.Types.Name
 
+import GHC.Data.Bag
+
 import Data.Function ( on )
 
-data TypedHole = TypedHole { th_relevant_cts :: Cts
+data TypedHole = TypedHole { th_relevant_cts :: Bag CtEvidence
                            -- ^ Any relevant Cts to the hole
                            , th_implics :: [Implication]
                            -- ^ The nested implications of the hole with the
                            --   innermost implication first.
                            , th_hole :: Maybe Hole
-                           -- ^ The hole itself, if available. Only for debugging.
+                           -- ^ The hole itself, if available.
                            }
 
 instance Outputable TypedHole where
diff --git a/compiler/GHC/Tc/Errors/Ppr.hs b/compiler/GHC/Tc/Errors/Ppr.hs
index d1ea6d93e2..a736a40871 100644
--- a/compiler/GHC/Tc/Errors/Ppr.hs
+++ b/compiler/GHC/Tc/Errors/Ppr.hs
@@ -226,11 +226,17 @@ instance Diagnostic TcRnMessage where
                    <+> text "with" <+> quotes (ppr n2))
                 2 (hang (text "both bound by the partial type signature:")
                         2 (ppr fn_name <+> dcolon <+> ppr hs_ty))
-    TcRnPartialTypeSigBadQuantifier n fn_name hs_ty
+    TcRnPartialTypeSigBadQuantifier n fn_name m_unif_ty hs_ty
       -> mkSimpleDecorated $
            hang (text "Can't quantify over" <+> quotes (ppr n))
-                2 (hang (text "bound by the partial type signature:")
-                        2 (ppr fn_name <+> dcolon <+> ppr hs_ty))
+                2 (vcat [ hang (text "bound by the partial type signature:")
+                             2 (ppr fn_name <+> dcolon <+> ppr hs_ty)
+                        , extra ])
+      where
+        extra | Just rhs_ty <- m_unif_ty
+              = sep [ quotes (ppr n), text "should really be", quotes (ppr rhs_ty) ]
+              | otherwise
+              = empty
     TcRnMissingSignature what _ _ ->
       mkSimpleDecorated $
       case what of
@@ -294,9 +300,6 @@ instance Diagnostic TcRnMessage where
                    text "in the type of a term:")
                 2 (pprType ty)
            , text "(GHC does not yet support this)" ]
-    TcRnIllegalEqualConstraints ty
-      -> mkSimpleDecorated $
-           text "Illegal equational constraint" <+> pprType ty
     TcRnBadQuantPredHead ty
       -> mkSimpleDecorated $
            hang (text "Quantified predicate must have a class or type variable head:")
@@ -744,8 +747,6 @@ instance Diagnostic TcRnMessage where
       -> ErrorWithoutFlag
     TcRnVDQInTermType{}
       -> ErrorWithoutFlag
-    TcRnIllegalEqualConstraints{}
-      -> ErrorWithoutFlag
     TcRnBadQuantPredHead{}
       -> ErrorWithoutFlag
     TcRnIllegalTupleConstraint{}
@@ -982,8 +983,6 @@ instance Diagnostic TcRnMessage where
       -> noHints
     TcRnVDQInTermType{}
       -> noHints
-    TcRnIllegalEqualConstraints{}
-      -> [suggestAnyExtension [LangExt.GADTs, LangExt.TypeFamilies]]
     TcRnBadQuantPredHead{}
       -> noHints
     TcRnIllegalTupleConstraint{}
@@ -1531,7 +1530,7 @@ pprTcSolverReportMsg _ (UserTypeError ty) =
   pprUserTypeErrorTy ty
 pprTcSolverReportMsg ctxt (ReportHoleError hole err) =
   pprHoleError ctxt hole err
-pprTcSolverReportMsg _ (CannotUnifyWithPolytype ct tv1 ty2) =
+pprTcSolverReportMsg _ (CannotUnifyWithPolytype item tv1 ty2) =
   vcat [ (if isSkolemTyVar tv1
           then text "Cannot equate type variable"
           else text "Cannot instantiate unification variable")
@@ -1539,13 +1538,13 @@ pprTcSolverReportMsg _ (CannotUnifyWithPolytype ct tv1 ty2) =
        , hang (text "with a" <+> what <+> text "involving polytypes:") 2 (ppr ty2) ]
   where
     what = text $ levelString $
-           ctLocTypeOrKind_maybe (ctLoc ct) `orElse` TypeLevel
+           ctLocTypeOrKind_maybe (errorItemCtLoc item) `orElse` TypeLevel
 pprTcSolverReportMsg _
-  (Mismatch { mismatch_ea = add_ea
-            , mismatch_ct = ct
-            , mismatch_ty1 = ty1
-            , mismatch_ty2 = ty2 })
-  = addArising (ctOrigin ct) msg
+  (Mismatch { mismatch_ea   = add_ea
+            , mismatch_item = item
+            , mismatch_ty1  = ty1
+            , mismatch_ty2  = ty2 })
+  = addArising (errorItemOrigin item) msg
   where
     msg
       | (isLiftedRuntimeRep ty1 && isUnliftedRuntimeRep ty2) ||
@@ -1576,9 +1575,9 @@ pprTcSolverReportMsg _
 
     padding = length herald1 - length herald2
 
-    is_repr = case ctEqRel ct of { ReprEq -> True; NomEq -> False }
+    is_repr = case errorItemEqRel item of { ReprEq -> True; NomEq -> False }
 
-    what = levelString (ctLocTypeOrKind_maybe (ctLoc ct) `orElse` TypeLevel)
+    what = levelString (ctLocTypeOrKind_maybe (errorItemCtLoc item) `orElse` TypeLevel)
 
     conc :: [String] -> String
     conc = foldr1 add_space
@@ -1605,9 +1604,9 @@ pprTcSolverReportMsg _
 
 pprTcSolverReportMsg ctxt
   (TypeEqMismatch { teq_mismatch_ppr_explicit_kinds = ppr_explicit_kinds
-                  , teq_mismatch_ct  = ct
-                  , teq_mismatch_ty1 = ty1
-                  , teq_mismatch_ty2 = ty2
+                  , teq_mismatch_item     = item
+                  , teq_mismatch_ty1      = ty1
+                  , teq_mismatch_ty2      = ty2
                   , teq_mismatch_expected = exp
                   , teq_mismatch_actual   = act
                   , teq_mismatch_what     = mb_thing })
@@ -1628,21 +1627,21 @@ pprTcSolverReportMsg ctxt
                 Just thing -> quotes (ppr thing) <+> text "has kind"
             , quotes (pprWithTYPE act) ]
       | Just nargs_msg <- num_args_msg
-      , Right ea_msg <- mk_ea_msg ctxt (Just ct) level orig
+      , Right ea_msg <- mk_ea_msg ctxt (Just item) level orig
       = nargs_msg $$ pprTcSolverReportMsg ctxt ea_msg
       | -- pprTrace "check" (ppr ea_looks_same $$ ppr exp $$ ppr act $$ ppr ty1 $$ ppr ty2) $
         ea_looks_same ty1 ty2 exp act
-      , Right ea_msg <- mk_ea_msg ctxt (Just ct) level orig
+      , Right ea_msg <- mk_ea_msg ctxt (Just item) level orig
       = pprTcSolverReportMsg ctxt ea_msg
       -- The mismatched types are /inside/ exp and act
-      | let mismatch_err = Mismatch False ct ty1 ty2
+      | let mismatch_err = Mismatch False item ty1 ty2
             errs = case mk_ea_msg ctxt Nothing level orig of
               Left ea_info -> [ mkTcReportWithInfo mismatch_err ea_info ]
               Right ea_err -> [ mismatch_err, ea_err ]
       = vcat $ map (pprTcSolverReportMsg ctxt) errs
 
-    ct_loc = ctLoc ct
-    orig   = ctOrigin ct
+    ct_loc = errorItemCtLoc item
+    orig   = errorItemOrigin item
     level  = ctLocTypeOrKind_maybe ct_loc `orElse` TypeLevel
 
     thing_msg (Just thing) _  levity = quotes (ppr thing) <+> text "is" <+> levity
@@ -1683,7 +1682,7 @@ pprTcSolverReportMsg _ (FixedRuntimeRepError origs_and_tys) =
              ,nest 2 $ ppr ty <+> dcolon <+> pprWithTYPE (typeKind ty)]
   in
     vcat $ map (uncurry combine_origin_ty) origs_and_tys
-pprTcSolverReportMsg _ (SkolemEscape ct implic esc_skols) =
+pprTcSolverReportMsg _ (SkolemEscape item implic esc_skols) =
   let
     esc_doc = sep [ text "because" <+> what <+> text "variable" <> plural esc_skols
                 <+> pprQuotedList esc_skols
@@ -1703,7 +1702,7 @@ pprTcSolverReportMsg _ (SkolemEscape ct implic esc_skols) =
          ppr (getLclEnvLoc (ic_env implic)) ] ]
   where
     what = text $ levelString $
-           ctLocTypeOrKind_maybe (ctLoc ct) `orElse` TypeLevel
+           ctLocTypeOrKind_maybe (errorItemCtLoc item) `orElse` TypeLevel
 pprTcSolverReportMsg _ (UntouchableVariable tv implic)
   | Implic { ic_given = given, ic_info = skol_info } <- implic
   = sep [ quotes (ppr tv) <+> text "is untouchable"
@@ -1711,9 +1710,9 @@ pprTcSolverReportMsg _ (UntouchableVariable tv implic)
         , nest 2 $ text "bound by" <+> ppr skol_info
         , nest 2 $ text "at" <+>
           ppr (getLclEnvLoc (ic_env implic)) ]
-pprTcSolverReportMsg _ (BlockedEquality ct) =
+pprTcSolverReportMsg _ (BlockedEquality item) =
   vcat [ hang (text "Cannot use equality for substitution:")
-           2 (ppr (ctPred ct))
+           2 (ppr (errorItemPred item))
        , text "Doing so would be ill-kinded." ]
 pprTcSolverReportMsg _ (ExpectingMoreArguments n thing) =
   text "Expecting" <+> speakN (abs n) <+>
@@ -1722,16 +1721,16 @@ pprTcSolverReportMsg _ (ExpectingMoreArguments n thing) =
     more
      | n == 1    = text "more argument to"
      | otherwise = text "more arguments to" -- n > 1
-pprTcSolverReportMsg ctxt (UnboundImplicitParams (ct :| cts)) =
+pprTcSolverReportMsg ctxt (UnboundImplicitParams (item :| items)) =
   let givens = getUserGivens ctxt
   in if null givens
-     then addArising (ctOrigin ct) $
+     then addArising (errorItemOrigin item) $
             sep [ text "Unbound implicit parameter" <> plural preds
                 , nest 2 (pprParendTheta preds) ]
-     else pprTcSolverReportMsg ctxt (CouldNotDeduce givens (ct :| cts) Nothing)
+     else pprTcSolverReportMsg ctxt (CouldNotDeduce givens (item :| items) Nothing)
   where
-    preds = map ctPred (ct : cts)
-pprTcSolverReportMsg ctxt (CouldNotDeduce useful_givens (ct :| others) mb_extra)
+    preds = map errorItemPred (item : items)
+pprTcSolverReportMsg ctxt (CouldNotDeduce useful_givens (item :| others) mb_extra)
   = main_msg $$
      case supplementary of
       Left infos
@@ -1741,17 +1740,17 @@ pprTcSolverReportMsg ctxt (CouldNotDeduce useful_givens (ct :| others) mb_extra)
   where
     main_msg
       | null useful_givens
-      = addArising (ctOrigin ct) no_instance_msg
+      = addArising orig no_instance_msg
       | otherwise
-      = vcat [ addArising (ctOrigin ct) no_deduce_msg
+      = vcat [ addArising orig no_deduce_msg
              , vcat (pp_givens useful_givens) ]
     supplementary = case mb_extra of
       Nothing
         -> Left []
       Just (CND_Extra level ty1 ty2)
         -> mk_supplementary_ea_msg ctxt level ty1 ty2 orig
-    (wanted, wanteds) = (ctPred ct, map ctPred others)
-    orig = ctOrigin ct
+    (wanted, wanteds) = (errorItemPred item, map errorItemPred others)
+    orig = errorItemOrigin item
     no_instance_msg
       | null others
       , Just (tc, _) <- splitTyConApp_maybe wanted
@@ -1765,13 +1764,13 @@ pprTcSolverReportMsg ctxt (CouldNotDeduce useful_givens (ct :| others) mb_extra)
       = text "Could not deduce" <+> pprParendType wanted
       | otherwise
       = text "Could not deduce:" <+> pprTheta wanteds
-pprTcSolverReportMsg ctxt (AmbiguityPreventsSolvingCt ct ambigs) =
+pprTcSolverReportMsg ctxt (AmbiguityPreventsSolvingCt item ambigs) =
   pprTcSolverReportInfo ctxt (Ambiguity True ambigs) <+>
-  pprArising (ctOrigin ct) $$
-  text "prevents the constraint" <+> quotes (pprParendType $ ctPred ct)
+  pprArising (errorItemOrigin item) $$
+  text "prevents the constraint" <+> quotes (pprParendType $ errorItemPred item)
   <+> text "from being solved."
 pprTcSolverReportMsg ctxt@(CEC {cec_encl = implics})
-  (CannotResolveInstance ct unifiers candidates imp_errs suggs binds)
+  (CannotResolveInstance item unifiers candidates imp_errs suggs binds)
   =
     vcat
       [ pprTcSolverReportMsg ctxt no_inst_msg
@@ -1794,11 +1793,11 @@ pprTcSolverReportMsg ctxt@(CEC {cec_encl = implics})
       , vcat $ map ppr imp_errs
       , vcat $ map ppr suggs ]
   where
-    orig          = ctOrigin ct
-    pred          = ctPred ct
+    orig          = errorItemOrigin item
+    pred          = errorItemPred item
     (clas, tys)   = getClassPredTys pred
     -- See Note [Highlighting ambiguous type variables]
-    (ambig_kvs, ambig_tvs) = ambigTkvsOfCt ct
+    (ambig_kvs, ambig_tvs) = ambigTkvsOfTy pred
     ambigs = ambig_kvs ++ ambig_tvs
     has_ambigs = not (null ambigs)
     useful_givens = discardProvCtxtGivens orig (getUserGivensFromImplics implics)
@@ -1812,9 +1811,9 @@ pprTcSolverReportMsg ctxt@(CEC {cec_encl = implics})
     no_inst_msg :: TcSolverReportMsg
     no_inst_msg
       | lead_with_ambig
-      = AmbiguityPreventsSolvingCt ct (ambig_kvs, ambig_tvs)
+      = AmbiguityPreventsSolvingCt item (ambig_kvs, ambig_tvs)
       | otherwise
-      = CouldNotDeduce useful_givens (ct :| []) Nothing
+      = CouldNotDeduce useful_givens (item :| []) Nothing
 
     -- Report "potential instances" only when the constraint arises
     -- directly from the user's use of an overloaded function
@@ -1866,7 +1865,7 @@ pprTcSolverReportMsg ctxt@(CEC {cec_encl = implics})
       = hang (text "use a standalone 'deriving instance' declaration,")
            2 (text "so you can specify the instance context yourself")
 
-pprTcSolverReportMsg (CEC {cec_encl = implics}) (OverlappingInstances ct matches unifiers) =
+pprTcSolverReportMsg (CEC {cec_encl = implics}) (OverlappingInstances item matches unifiers) =
   vcat
     [ addArising orig $
         (text "Overlapping instances for"
@@ -1903,8 +1902,8 @@ pprTcSolverReportMsg (CEC {cec_encl = implics}) (OverlappingInstances ct matches
                            , text "when compiling the other instance declarations"]
                ])]
   where
-    orig            = ctOrigin ct
-    pred            = ctPred ct
+    orig            = errorItemOrigin item
+    pred            = errorItemPred item
     (clas, tys)     = getClassPredTys pred
     tyCoVars        = tyCoVarsOfTypesList tys
     famTyCons       = filter isFamilyTyCon $ concatMap (nonDetEltsUniqSet . tyConsOfType) tys
@@ -1926,7 +1925,7 @@ pprTcSolverReportMsg (CEC {cec_encl = implics}) (OverlappingInstances ct matches
                      Just (clas', tys') -> clas' == clas
                                           && isJust (tcMatchTys tys tys')
                      Nothing -> False
-pprTcSolverReportMsg _ (UnsafeOverlap ct matches unsafe_overlapped) =
+pprTcSolverReportMsg _ (UnsafeOverlap item matches unsafe_overlapped) =
   vcat [ addArising orig (text "Unsafe overlapping instances for"
                   <+> pprType (mkClassPred clas tys))
        , sep [text "The matching instance is:",
@@ -1939,8 +1938,8 @@ pprTcSolverReportMsg _ (UnsafeOverlap ct matches unsafe_overlapped) =
               ]
        ]
   where
-    orig        = ctOrigin ct
-    pred        = ctPred ct
+    orig        = errorItemOrigin item
+    pred        = errorItemPred item
     (clas, tys) = getClassPredTys pred
 
 {- *********************************************************************
@@ -2475,6 +2474,9 @@ pprArising :: CtOrigin -> SDoc
 -- We've done special processing for TypeEq, KindEq, givens
 pprArising (TypeEqOrigin {})         = empty
 pprArising (KindEqOrigin {})         = empty
+pprArising (AmbiguityCheckOrigin {}) = empty  -- the "In the ambiguity check" context
+                                              -- is sufficient; this would just be
+                                              -- repetitive
 pprArising orig | isGivenOrigin orig = empty
                 | otherwise          = pprCtOrigin orig
 
@@ -2614,9 +2616,10 @@ ea_looks_same ty1 ty2 exp act
       -- when the types really look the same.  However,
       -- (TYPE 'LiftedRep) and Type both print the same way.
 
-mk_ea_msg :: SolverReportErrCtxt -> Maybe Ct -> TypeOrKind -> CtOrigin -> Either [TcSolverReportInfo] TcSolverReportMsg
+mk_ea_msg :: SolverReportErrCtxt -> Maybe ErrorItem -> TypeOrKind
+          -> CtOrigin -> Either [TcSolverReportInfo] TcSolverReportMsg
 -- Constructs a "Couldn't match" message
--- The (Maybe Ct) says whether this is the main top-level message (Just)
+-- The (Maybe ErrorItem) says whether this is the main top-level message (Just)
 --     or a supplementary message (Nothing)
 mk_ea_msg ctxt at_top level
   (TypeEqOrigin { uo_actual = act, uo_expected = exp, uo_thing = mb_thing })
@@ -2625,13 +2628,13 @@ mk_ea_msg ctxt at_top level
   = Right $ KindMismatch { kmismatch_what     = thing
                          , kmismatch_expected = exp
                          , kmismatch_actual   = act }
-  | Just ct <- at_top
+  | Just item <- at_top
   , let mismatch =
           Mismatch
-            { mismatch_ea = True
-            , mismatch_ct = ct
-            , mismatch_ty1 = exp
-            , mismatch_ty2 = act }
+            { mismatch_ea   = True
+            , mismatch_item = item
+            , mismatch_ty1  = exp
+            , mismatch_ty2  = act }
   = Right $
     if expanded_syns
     then mkTcReportWithInfo mismatch [ea_expanded]
diff --git a/compiler/GHC/Tc/Errors/Types.hs b/compiler/GHC/Tc/Errors/Types.hs
index 1cea1c8d94..713232686f 100644
--- a/compiler/GHC/Tc/Errors/Types.hs
+++ b/compiler/GHC/Tc/Errors/Types.hs
@@ -36,6 +36,8 @@ module GHC.Tc.Errors.Types (
   , MissingSignature(..)
   , Exported(..)
 
+  , ErrorItem(..), errorItemOrigin, errorItemEqRel, errorItemPred, errorItemCtLoc
+
   , SolverReport(..), SolverReportSupplementary(..)
   , SolverReportWithCtxt(..)
   , SolverReportErrCtxt(..)
@@ -82,6 +84,7 @@ import GHC.Core.DataCon (DataCon)
 import GHC.Core.FamInstEnv (FamInst)
 import GHC.Core.InstEnv (ClsInst)
 import GHC.Core.PatSyn (PatSyn)
+import GHC.Core.Predicate (EqRel, predTypeEqRel)
 import GHC.Core.TyCon (TyCon, TyConFlavour)
 import GHC.Core.Type (Kind, Type, ThetaType, PredType)
 import GHC.Unit.State (UnitState)
@@ -602,9 +605,11 @@ data TcRnMessage where
      Test cases: partial-sig/should_fail/T14479
   -}
   TcRnPartialTypeSigBadQuantifier
-    :: Name -- ^ type variable being quantified
-    -> Name -- ^ function name
-    -> LHsSigWcType GhcRn -> TcRnMessage
+    :: Name   -- ^ user-written name of type variable being quantified
+    -> Name   -- ^ function name
+    -> Maybe Type   -- ^ type the variable unified with, if known
+    -> LHsSigWcType GhcRn  -- ^ partial type signature
+    -> TcRnMessage
 
   {-| TcRnMissingSignature is a warning that occurs when a top-level binding
       or a pattern synonym does not have a type signature.
@@ -798,17 +803,6 @@ data TcRnMessage where
   -}
   TcRnVDQInTermType :: !Type -> TcRnMessage
 
-  {-| TcRnIllegalEqualConstraints is an error that occurs whenever an illegal equational
-      constraint is specified.
-
-      Examples(s):
-        blah :: (forall a. a b ~ a c) => b -> c
-        blah = undefined
-
-      Test cases: typecheck/should_fail/T17563
-  -}
-  TcRnIllegalEqualConstraints :: !Type -> TcRnMessage
-
   {-| TcRnBadQuantPredHead is an error that occurs whenever a quantified predicate
       lacks a class or type variable head.
 
@@ -1875,7 +1869,10 @@ instance Outputable Exported where
   ppr IsExported    = text "IsExported"
 
 --------------------------------------------------------------------------------
--- Errors used in GHC.Tc.Errors
+--
+--     Errors used in GHC.Tc.Errors
+--
+--------------------------------------------------------------------------------
 
 {- Note [Error report]
 ~~~~~~~~~~~~~~~~~~~~~~
@@ -1971,6 +1968,56 @@ getUserGivens :: SolverReportErrCtxt -> [UserGiven]
 -- One item for each enclosing implication
 getUserGivens (CEC {cec_encl = implics}) = getUserGivensFromImplics implics
 
+----------------------------------------------------------------------------
+--
+--   ErrorItem
+--
+----------------------------------------------------------------------------
+
+-- | A predicate with its arising location; used to encapsulate a constraint
+-- that will give rise to a diagnostic.
+data ErrorItem
+-- We could perhaps use Ct here (and indeed used to do exactly that), but
+-- having a separate type gives to denote errors-in-formation gives us
+-- a nice place to do pre-processing, such as calculating ei_suppress.
+-- Perhaps some day, an ErrorItem could eventually evolve to contain
+-- the error text (or some representation of it), so we can then have all
+-- the errors together when deciding which to report.
+  = EI { ei_pred     :: PredType         -- report about this
+         -- The ei_pred field will never be an unboxed equality with
+         -- a (casted) tyvar on the right; this is guaranteed by the solver
+       , ei_evdest   :: Maybe TcEvDest   -- for Wanteds, where to put evidence
+       , ei_flavour  :: CtFlavour
+       , ei_loc      :: CtLoc
+       , ei_m_reason :: Maybe CtIrredReason  -- if this ErrorItem was made from a
+                                             -- CtIrred, this stores the reason
+       , ei_suppress :: Bool    -- Suppress because of Note [Wanteds rewrite Wanteds]
+                                -- in GHC.Tc.Constraint
+       }
+
+instance Outputable ErrorItem where
+  ppr (EI { ei_pred     = pred
+          , ei_evdest   = m_evdest
+          , ei_flavour  = flav
+          , ei_suppress = supp })
+    = pp_supp <+> ppr flav <+> pp_dest m_evdest <+> ppr pred
+    where
+      pp_dest Nothing   = empty
+      pp_dest (Just ev) = ppr ev <+> dcolon
+
+      pp_supp = if supp then text "suppress:" else empty
+
+errorItemOrigin :: ErrorItem -> CtOrigin
+errorItemOrigin = ctLocOrigin . ei_loc
+
+errorItemEqRel :: ErrorItem -> EqRel
+errorItemEqRel = predTypeEqRel . ei_pred
+
+errorItemCtLoc :: ErrorItem -> CtLoc
+errorItemCtLoc = ei_loc
+
+errorItemPred :: ErrorItem -> PredType
+errorItemPred = ei_pred
 
 {- Note [discardProvCtxtGivens]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -2068,7 +2115,7 @@ data TcSolverReportMsg
   -- | A type equality between a type variable and a polytype.
   --
   -- Test cases: T12427a, T2846b, T10194, ...
-  | CannotUnifyWithPolytype Ct TyVar Type
+  | CannotUnifyWithPolytype ErrorItem TyVar Type
 
   -- | Couldn't unify two types or kinds.
   --
@@ -2078,10 +2125,10 @@ data TcSolverReportMsg
   --
   --  Test cases: T1396, T8263, ...
   | Mismatch
-      { mismatch_ea  :: Bool -- ^ Should this be phrased in terms of expected vs actual?
-      , mismatch_ct  :: Ct   -- ^ The constraint in which the mismatch originated.
-      , mismatch_ty1 :: Type -- ^ First type (the expected type if if mismatch_ea is True)
-      , mismatch_ty2 :: Type -- ^ Second type (the actual type if mismatch_ea is True)
+      { mismatch_ea   :: Bool        -- ^ Should this be phrased in terms of expected vs actual?
+      , mismatch_item :: ErrorItem   -- ^ The constraint in which the mismatch originated.
+      , mismatch_ty1  :: Type        -- ^ First type (the expected type if if mismatch_ea is True)
+      , mismatch_ty2  :: Type        -- ^ Second type (the actual type if mismatch_ea is True)
       }
 
   -- | A type has an unexpected kind.
@@ -2099,9 +2146,9 @@ data TcSolverReportMsg
   -- Test cases: T1470, tcfail212.
   | TypeEqMismatch
       { teq_mismatch_ppr_explicit_kinds :: Bool
-      , teq_mismatch_ct  :: Ct
-      , teq_mismatch_ty1 :: Type
-      , teq_mismatch_ty2 :: Type
+      , teq_mismatch_item     :: ErrorItem
+      , teq_mismatch_ty1      :: Type
+      , teq_mismatch_ty2      :: Type
       , teq_mismatch_expected :: Type -- ^ The overall expected type
       , teq_mismatch_actual   :: Type -- ^ The overall actual type
       , teq_mismatch_what     :: Maybe TypedThing -- ^ What thing is 'teq_mismatch_actual' the kind of?
@@ -2122,7 +2169,7 @@ data TcSolverReportMsg
   --   foo (MkEx x) = x
   --
   -- Test cases: TypeSkolEscape, T11142.
-  | SkolemEscape Ct Implication [TyVar]
+  | SkolemEscape ErrorItem Implication [TyVar]
 
   -- | Trying to unify an untouchable variable, e.g. a variable from an outer scope.
   --
@@ -2133,7 +2180,7 @@ data TcSolverReportMsg
   -- beteen their kinds.
   --
   -- Test cases: none.
-  | BlockedEquality Ct
+  | BlockedEquality ErrorItem
 
   -- | Something was not applied to sufficiently many arguments.
   --
@@ -2153,7 +2200,7 @@ data TcSolverReportMsg
   --
   -- Test case: tcfail130.
   | UnboundImplicitParams
-      (NE.NonEmpty Ct)
+      (NE.NonEmpty ErrorItem)
 
   -- | Couldn't solve some Wanted constraints using the Givens.
   -- This is the most commonly used constructor, used for generic
@@ -2162,9 +2209,9 @@ data TcSolverReportMsg
      { cnd_user_givens :: [Implication]
         -- | The Wanted constraints we couldn't solve.
         --
-        -- N.B.: the 'Ct' at the head of the list has been tidied,
+        -- N.B.: the 'ErrorItem' at the head of the list has been tidied,
         -- perhaps not the others.
-     , cnd_wanted      :: NE.NonEmpty Ct
+     , cnd_wanted      :: NE.NonEmpty ErrorItem
 
        -- | Some additional info consumed by 'mk_supplementary_ea_msg'.
      , cnd_extra       :: Maybe CND_Extra
@@ -2183,7 +2230,7 @@ data TcSolverReportMsg
   --
   -- Test case: T4921.
   | AmbiguityPreventsSolvingCt
-      Ct -- ^ always a class constraint
+      ErrorItem -- ^ always a class constraint
       ([TyVar], [TyVar]) -- ^ ambiguous kind and type variables, respectively
 
   -- | Could not solve a constraint; there were several unifying candidate instances
@@ -2191,7 +2238,7 @@ data TcSolverReportMsg
   -- as possible about why we couldn't choose any instance, e.g. because of
   -- ambiguous type variables.
   | CannotResolveInstance
-    { cannotResolve_ct :: Ct
+    { cannotResolve_item         :: ErrorItem
     , cannotResolve_unifiers     :: [ClsInst]
     , cannotResolve_candidates   :: [ClsInst]
     , cannotResolve_importErrors :: [ImportError]
@@ -2205,7 +2252,7 @@ data TcSolverReportMsg
   --
   -- Test cases: tcfail118, tcfail121, tcfail218.
   | OverlappingInstances
-    { overlappingInstances_ct :: Ct
+    { overlappingInstances_item     :: ErrorItem
     , overlappingInstances_matches  :: [ClsInst]
     , overlappingInstances_unifiers :: [ClsInst] }
 
@@ -2215,7 +2262,7 @@ data TcSolverReportMsg
   --
   -- Test cases: SH_Overlap{1,2,5,6,7,11}.
   | UnsafeOverlap
-    { unsafeOverlap_ct :: Ct
+    { unsafeOverlap_item    :: ErrorItem
     , unsafeOverlap_matches :: [ClsInst]
     , unsafeOverlapped      :: [ClsInst] }