Kill derived constraintswip/derived-refactor

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
-------------------------

1 files changed, 58 insertions, 58 deletions

diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs
index 1ff6c044dc..4a5ef151b7 100644
--- a/compiler/GHC/Tc/Utils/Unify.hs
+++ b/compiler/GHC/Tc/Utils/Unify.hs
@@ -556,8 +556,7 @@ tcSubTypePat :: CtOrigin -> UserTypeCtxt
 -- If wrap = tc_sub_type_et t1 t2
 --    => wrap :: t1 ~> t2
 tcSubTypePat inst_orig ctxt (Check ty_actual) ty_expected
-  = do { dflags <- getDynFlags
-       ; tc_sub_type dflags unifyTypeET inst_orig ctxt ty_actual ty_expected }
+  = tc_sub_type unifyTypeET inst_orig ctxt ty_actual ty_expected
 
 tcSubTypePat _ _ (Infer inf_res) ty_expected
   = do { co <- fillInferResult ty_expected inf_res
@@ -584,9 +583,8 @@ tcSubTypeNC :: CtOrigin          -- ^ Used when instantiating
             -> TcM HsWrapper
 tcSubTypeNC inst_orig ctxt m_thing ty_actual res_ty
   = case res_ty of
-      Check ty_expected -> do { dflags <- getDynFlags
-                              ; tc_sub_type dflags (unifyType m_thing) inst_orig ctxt
-                                            ty_actual ty_expected }
+      Check ty_expected -> tc_sub_type (unifyType m_thing) inst_orig ctxt
+                                       ty_actual ty_expected
 
       Infer inf_res -> do { (wrap, rho) <- topInstantiate inst_orig ty_actual
                                    -- See Note [Instantiation of InferResult]
@@ -631,22 +629,18 @@ command. See Note [Implementing :type] in GHC.Tc.Module.
 -}
 
 ---------------
-tcSubTypeSigma :: UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
+tcSubTypeSigma :: CtOrigin       -- where did the actual type arise / why are we
+                                 -- doing this subtype check?
+               -> UserTypeCtxt   -- where did the expected type arise?
+               -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
 -- External entry point, but no ExpTypes on either side
 -- Checks that actual <= expected
 -- Returns HsWrapper :: actual ~ expected
-tcSubTypeSigma ctxt ty_actual ty_expected
-  = do { dflags <- getDynFlags
-       ; tc_sub_type dflags (unifyType Nothing) eq_orig ctxt ty_actual ty_expected }
-  where
-    eq_orig = TypeEqOrigin { uo_actual   = ty_actual
-                           , uo_expected = ty_expected
-                           , uo_thing    = Nothing
-                           , uo_visible  = True }
+tcSubTypeSigma orig ctxt ty_actual ty_expected
+  = tc_sub_type (unifyType Nothing) orig ctxt ty_actual ty_expected
 
 ---------------
-tc_sub_type :: DynFlags
-            -> (TcType -> TcType -> TcM TcCoercionN)  -- How to unify
+tc_sub_type :: (TcType -> TcType -> TcM TcCoercionN)  -- How to unify
             -> CtOrigin       -- Used when instantiating
             -> UserTypeCtxt   -- Used when skolemising
             -> TcSigmaType    -- Actual; a sigma-type
@@ -655,7 +649,7 @@ tc_sub_type :: DynFlags
 -- Checks that actual_ty is more polymorphic than expected_ty
 -- If wrap = tc_sub_type t1 t2
 --    => wrap :: t1 ~> t2
-tc_sub_type dflags unify inst_orig ctxt ty_actual ty_expected
+tc_sub_type unify inst_orig ctxt ty_actual ty_expected
   | definitely_poly ty_expected      -- See Note [Don't skolemise unnecessarily]
   , not (possibly_poly ty_actual)
   = do { traceTc "tc_sub_type (drop to equality)" $
@@ -683,7 +677,7 @@ tc_sub_type dflags unify inst_orig ctxt ty_actual ty_expected
       | (tvs, theta, tau) <- tcSplitSigmaTy ty
       , (tv:_) <- tvs
       , null theta
-      , checkTyVarEq dflags tv tau `cterHasProblem` cteInsolubleOccurs
+      , checkTyVarEq tv tau `cterHasProblem` cteInsolubleOccurs
       = True
       | otherwise
       = False
@@ -1067,7 +1061,7 @@ take care:
   can yield /very/ confusing error messages, because we can get
       [W] C Int b1    -- from f_blah
       [W] C Int b2    -- from g_blan
-  and fundpes can yield [D] b1 ~ b2, even though the two functions have
+  and fundpes can yield [W] b1 ~ b2, even though the two functions have
   literally nothing to do with each other.  #14185 is an example.
   Building an implication keeps them separate.
 -}
@@ -1447,15 +1441,14 @@ uUnfilledVar2 :: CtOrigin
               -> TcTauType      -- Type 2, zonked
               -> TcM Coercion
 uUnfilledVar2 origin t_or_k swapped tv1 ty2
-  = do { dflags  <- getDynFlags
-       ; cur_lvl <- getTcLevel
-       ; go dflags cur_lvl }
+  = do { cur_lvl <- getTcLevel
+       ; go cur_lvl }
   where
-    go dflags cur_lvl
+    go cur_lvl
       | isTouchableMetaTyVar cur_lvl tv1
            -- See Note [Unification preconditions], (UNTOUCHABLE) wrinkles
       , canSolveByUnification (metaTyVarInfo tv1) ty2
-      , cterHasNoProblem (checkTyVarEq dflags tv1 ty2)
+      , cterHasNoProblem (checkTyVarEq tv1 ty2)
            -- See Note [Prevent unification with type families]
       = do { co_k <- uType KindLevel kind_origin (tcTypeKind ty2) (tyVarKind tv1)
            ; traceTc "uUnfilledVar2 ok" $
@@ -1471,7 +1464,8 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2
                      ; return (mkTcNomReflCo ty2) }
 
              else defer } -- This cannot be solved now.  See GHC.Tc.Solver.Canonical
-                          -- Note [Equalities with incompatible kinds]
+                          -- Note [Equalities with incompatible kinds] for how
+                          -- this will be dealt with in the solver
 
       | otherwise
       = do { traceTc "uUnfilledVar2 not ok" (ppr tv1 $$ ppr ty2)
@@ -1485,14 +1479,20 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2
 
     defer = unSwap swapped (uType_defer t_or_k origin) ty1 ty2
 
-canSolveByUnification :: MetaInfo -> TcType -> Bool
--- See Note [Unification preconditions, (TYVAR-TV)]
+-- | Checks (TYVAR-TV) and (COERCION-HOLE) of Note [Unification preconditions];
+-- returns True if these conditions are satisfied. But see the Note for other
+-- preconditions, too.
+canSolveByUnification :: MetaInfo -> TcType  -- zonked
+                      -> Bool
+canSolveByUnification _    xi
+  | hasCoercionHoleTy xi   -- (COERCION-HOLE) check
+  = False
 canSolveByUnification info xi
   = case info of
       CycleBreakerTv -> False
       TyVarTv -> case tcGetTyVar_maybe xi of
                    Nothing -> False
-                   Just tv -> case tcTyVarDetails tv of
+                   Just tv -> case tcTyVarDetails tv of -- (TYVAR-TV) wrinkle
                                  MetaTv { mtv_info = info }
                                             -> case info of
                                                  TyVarTv -> True
@@ -1552,7 +1552,7 @@ unify alpha := ty?
 This note only applied to /homogeneous/ equalities, in which both
 sides have the same kind.
 
-There are three reasons not to unify:
+There are four reasons not to unify:
 
 1. (SKOL-ESC) Skolem-escape
    Consider the constraint
@@ -1590,8 +1590,22 @@ There are three reasons not to unify:
 
    * CycleBreakerTv: never unified, except by restoreTyVarCycles.
 
+4. (COERCION-HOLE) Confusing coercion holes
+   Suppose our equality is
+     (alpha :: k) ~ (Int |> {co})
+   where co :: Type ~ k is an unsolved wanted. Note that this
+   equality is homogeneous; both sides have kind k. Unifying here
+   is sensible, but it can lead to very confusing error messages.
+   It's very much like a Wanted rewriting a Wanted. Even worse,
+   unifying a variable essentially turns an equality into a Given,
+   and so we could not use the tracking mechansim in
+   Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint.
+   We thus simply do not unify in this case.
+
+   This is expanded as Wrinkle (2) in Note [Equalities with incompatible kinds]
+   in GHC.Tc.Solver.Canonical.
 
-Needless to say, all three have wrinkles:
+Needless to say, all there are wrinkles:
 
 * (SKOL-ESC) Promotion.  Given alpha[n] ~ ty, what if beta[k] is free
   in 'ty', where beta is a unification variable, and k>n?  'beta'
@@ -1653,7 +1667,7 @@ So we look for a positive reason to swap, using a three-step test:
   Generally speaking we always try to put a MetaTv on the left
   in preference to SkolemTv or RuntimeUnkTv:
      a) Because the MetaTv may be touchable and can be unified
-     b) Even if it's not touchable, GHC.Tc.Solver.floatEqualities
+     b) Even if it's not touchable, GHC.Tc.Solver.floatConstraints
         looks for meta tyvars on the left
 
   Tie-breaking rules for MetaTvs:
@@ -1909,23 +1923,22 @@ with (forall k. k->*)
 
 ----------------
 {-# NOINLINE checkTyVarEq #-}  -- checkTyVarEq becomes big after the `inline` fires
-checkTyVarEq :: DynFlags -> TcTyVar -> TcType -> CheckTyEqResult
-checkTyVarEq dflags tv ty
-  = inline checkTypeEq dflags (TyVarLHS tv) ty
+checkTyVarEq :: TcTyVar -> TcType -> CheckTyEqResult
+checkTyVarEq tv ty
+  = inline checkTypeEq (TyVarLHS tv) ty
     -- inline checkTypeEq so that the `case`s over the CanEqLHS get blasted away
 
 {-# NOINLINE checkTyFamEq #-}  -- checkTyFamEq becomes big after the `inline` fires
-checkTyFamEq :: DynFlags
-             -> TyCon     -- type function
+checkTyFamEq :: TyCon     -- type function
              -> [TcType]  -- args, exactly saturated
              -> TcType    -- RHS
              -> CheckTyEqResult   -- always drops cteTypeFamily
-checkTyFamEq dflags fun_tc fun_args ty
-  = inline checkTypeEq dflags (TyFamLHS fun_tc fun_args) ty
+checkTyFamEq fun_tc fun_args ty
+  = inline checkTypeEq (TyFamLHS fun_tc fun_args) ty
     `cterRemoveProblem` cteTypeFamily
     -- inline checkTypeEq so that the `case`s over the CanEqLHS get blasted away
 
-checkTypeEq :: DynFlags -> CanEqLHS -> TcType -> CheckTyEqResult
+checkTypeEq :: CanEqLHS -> TcType -> CheckTyEqResult
 -- If cteHasNoProblem (checkTypeEq dflags lhs rhs), then lhs ~ rhs
 -- is a canonical CEqCan.
 --
@@ -1933,8 +1946,7 @@ checkTypeEq :: DynFlags -> CanEqLHS -> TcType -> CheckTyEqResult
 --   (a) a forall type (forall a. blah)
 --   (b) a predicate type (c => ty)
 --   (c) a type family; see Note [Prevent unification with type families]
---   (d) a blocking coercion hole
---   (e) an occurrence of the LHS (occurs check)
+--   (d) an occurrence of the LHS (occurs check)
 --
 -- Note that an occurs-check does not mean "definite error".  For example
 --   type family F a
@@ -1945,20 +1957,18 @@ checkTypeEq :: DynFlags -> CanEqLHS -> TcType -> CheckTyEqResult
 -- certainly can't unify b0 := F b0
 --
 -- For (a), (b), and (c) we check only the top level of the type, NOT
--- inside the kinds of variables it mentions.  For (d) we look deeply
--- in coercions when the LHS is a tyvar (but skip coercions for type family
--- LHSs), and for (e) see Note [CEqCan occurs check] in GHC.Tc.Types.Constraint.
+-- inside the kinds of variables it mentions, and for (d) see
+-- Note [CEqCan occurs check] in GHC.Tc.Types.Constraint.
 --
 -- checkTypeEq is called from
 --    * checkTyFamEq, checkTyVarEq (which inline it to specialise away the
 --      case-analysis on 'lhs')
 --    * checkEqCanLHSFinish, which does not know the form of 'lhs'
-checkTypeEq dflags lhs ty
+checkTypeEq lhs ty
   = go ty
   where
     impredicative    = cteProblem cteImpredicative
     type_family      = cteProblem cteTypeFamily
-    hole_blocker     = cteProblem cteHoleBlocker
     insoluble_occurs = cteProblem cteInsolubleOccurs
     soluble_occurs   = cteProblem cteSolubleOccurs
 
@@ -2029,21 +2039,11 @@ checkTypeEq dflags lhs ty
      -- inferred
     go_co co | TyVarLHS tv <- lhs
              , tv `elemVarSet` tyCoVarsOfCo co
-             = soluble_occurs S.<> maybe_hole_blocker
+             = soluble_occurs
 
         -- Don't check coercions for type families; see commentary at top of function
              | otherwise
-             = maybe_hole_blocker
-      where
-        -- See GHC.Tc.Solver.Canonical Note [Equalities with incompatible kinds]
-        -- Wrinkle (2) about this case in general, Wrinkle (4b) about the check for
-        -- deferred type errors
-        maybe_hole_blocker | not (gopt Opt_DeferTypeErrors dflags)
-                           , hasCoercionHoleCo co
-                           = hole_blocker
-
-                           | otherwise
-                           = cteOK
+             = cteOK
 
     check_tc :: TyCon -> CheckTyEqResult
     check_tc