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

6 files changed, 235 insertions, 306 deletions

diff --git a/compiler/GHC/Tc/Utils/Concrete.hs b/compiler/GHC/Tc/Utils/Concrete.hs
index 0b20a1af9d..bee886a58f 100644
--- a/compiler/GHC/Tc/Utils/Concrete.hs
+++ b/compiler/GHC/Tc/Utils/Concrete.hs
@@ -15,8 +15,8 @@ import GHC.Core.Coercion
 import GHC.Core.TyCo.Rep
 
 import GHC.Tc.Utils.Monad
-import GHC.Tc.Utils.TcType  ( TcType, mkTyConApp )
-import GHC.Tc.Utils.TcMType ( newCoercionHole, newFlexiTyVarTy )
+import GHC.Tc.Utils.TcType  ( mkTyConApp )
+import GHC.Tc.Utils.TcMType
 import GHC.Tc.Types.Constraint
 import GHC.Tc.Types.Evidence
 import GHC.Tc.Types.Origin ( CtOrigin(..), FRROrigin(..), WpFunOrigin(..) )
@@ -402,11 +402,6 @@ There are, however, some interactions to take into account:
       Examples: backpack/should_run/T13955.bkp, rep-poly/RepPolyBackpack2.
 -}
 
--- | A coercion hole used to store evidence for `Concrete#` constraints.
---
--- See Note [The Concrete mechanism].
-type ConcreteHole = CoercionHole
-
 -- | Evidence for a `Concrete#` constraint:
 -- essentially a 'ConcreteHole' (a coercion hole) that will be filled later,
 -- except:
@@ -458,42 +453,32 @@ hasFixedRuntimeRep frrOrig ty
           -- Create a new Wanted 'Concrete#' constraint and emit it.
           | otherwise
           -> do { loc <- getCtLocM (FixedRuntimeRepOrigin ty frrOrig) (Just KindLevel)
-                ; (hole, ct_ev) <- newConcretePrimWanted loc ki
+                ; (hole, _, ct_ev) <- newConcretePrimWanted loc ki
                 ; emitSimple $ mkNonCanonical ct_ev
                 ; return $ ConcreteHoleEvidence hole } }
   where
     ki :: Kind
     ki = typeKind ty
 
--- | Create a new (initially unfilled) coercion hole,
--- to hold evidence for a @'Concrete#' (ty :: ki)@ constraint.
-newConcreteHole :: Kind -- ^ Kind of the thing we want to ensure is concrete (e.g. 'runtimeRepTy')
-                -> Type -- ^ Thing we want to ensure is concrete (e.g. some 'RuntimeRep')
-                -> TcM ConcreteHole
-newConcreteHole ki ty
-  = do { concrete_ty <- newFlexiTyVarTy ki
-       ; let co_ty = mkHeteroPrimEqPred ki ki ty concrete_ty
-       ; newCoercionHole co_ty }
-
 -- | Create a new 'Concrete#' constraint.
-newConcretePrimWanted :: CtLoc -> Type -> TcM (ConcreteHole, CtEvidence)
+-- Returns the evidence, a metavariable which will be filled in with a
+-- guaranteed-concrete type, and a Wanted CtEvidence
+newConcretePrimWanted :: CtLoc -> Type -> TcM (ConcreteHole, TcType, CtEvidence)
 newConcretePrimWanted loc ty
   = do { let
            ki :: Kind
            ki = typeKind ty
-       ; hole <- newConcreteHole ki ty
+       ; (hole, concrete_ty) <- newConcreteHole ki ty
        ; let
            wantedCtEv :: CtEvidence
            wantedCtEv =
              CtWanted
                { ctev_dest = HoleDest hole
                , ctev_pred = mkTyConApp concretePrimTyCon [ki, ty]
-               , ctev_nosh = WOnly -- WOnly, because Derived Concrete# constraints
-                                   -- aren't useful: solving a Concrete# constraint
-                                   -- can't cause any unification to take place.
+               , ctev_rewriters = emptyRewriterSet
                , ctev_loc  = loc
                }
-        ; return (hole, wantedCtEv) }
+        ; return (hole, concrete_ty, wantedCtEv) }
 
 {-***********************************************************************
 *                                                                       *
diff --git a/compiler/GHC/Tc/Utils/Monad.hs b/compiler/GHC/Tc/Utils/Monad.hs
index 72670e6b06..a2720bc4e1 100644
--- a/compiler/GHC/Tc/Utils/Monad.hs
+++ b/compiler/GHC/Tc/Utils/Monad.hs
@@ -1261,10 +1261,10 @@ popErrCtxt = updLclEnv (\ env@(TcLclEnv { tcl_ctxt = ctxt }) ->
 getCtLocM :: CtOrigin -> Maybe TypeOrKind -> TcM CtLoc
 getCtLocM origin t_or_k
   = do { env <- getLclEnv
-       ; return (CtLoc { ctl_origin = origin
-                       , ctl_env    = env
-                       , ctl_t_or_k = t_or_k
-                       , ctl_depth  = initialSubGoalDepth }) }
+       ; return (CtLoc { ctl_origin   = origin
+                       , ctl_env      = env
+                       , ctl_t_or_k   = t_or_k
+                       , ctl_depth    = initialSubGoalDepth }) }
 
 setCtLocM :: CtLoc -> TcM a -> TcM a
 -- Set the SrcSpan and error context from the CtLoc
diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs
index 1ece974166..3c978b511c 100644
--- a/compiler/GHC/Tc/Utils/TcMType.hs
+++ b/compiler/GHC/Tc/Utils/TcMType.hs
@@ -37,9 +37,9 @@ module GHC.Tc.Utils.TcMType (
   --------------------------------
   -- Creating new evidence variables
   newEvVar, newEvVars, newDict,
-  newWantedWithLoc, newWanted, newWanteds, cloneWanted, cloneWC,
+  newWantedWithLoc, newWanted, newWanteds, cloneWanted, cloneWC, cloneWantedCtEv,
   emitWanted, emitWantedEq, emitWantedEvVar, emitWantedEvVars,
-  emitDerivedEqs,
+  emitWantedEqs,
   newTcEvBinds, newNoTcEvBinds, addTcEvBind,
   emitNewExprHole,
 
@@ -47,6 +47,8 @@ module GHC.Tc.Utils.TcMType (
   unpackCoercionHole, unpackCoercionHole_maybe,
   checkCoercionHole,
 
+  ConcreteHole, newConcreteHole,
+
   newImplication,
 
   --------------------------------
@@ -97,6 +99,10 @@ module GHC.Tc.Utils.TcMType (
   ------------------------------
   -- Representation polymorphism
   checkTypeHasFixedRuntimeRep,
+
+  ------------------------------
+  -- Other
+  anyUnfilledCoercionHoles
   ) where
 
 import GHC.Prelude
@@ -192,12 +198,15 @@ newEvVar ty = do { name <- newSysName (predTypeOccName ty)
 -- | Create a new Wanted constraint with the given 'CtLoc'.
 newWantedWithLoc :: CtLoc -> PredType -> TcM CtEvidence
 newWantedWithLoc loc pty
-  = do d <- if isEqPrimPred pty then HoleDest  <$> newCoercionHole pty
-                                else EvVarDest <$> newEvVar pty
-       return $ CtWanted { ctev_dest = d
-                         , ctev_pred = pty
-                         , ctev_nosh = WDeriv
-                         , ctev_loc  = loc }
+  = do d <- case classifyPredType pty of
+              EqPred {} -> HoleDest  <$> newCoercionHole pty
+              SpecialPred ConcretePrimPred ty ->
+                HoleDest <$> (fst <$> newConcreteHole (typeKind ty) ty)
+              _ -> EvVarDest <$> newEvVar pty
+       return $ CtWanted { ctev_dest      = d
+                         , ctev_pred      = pty
+                         , ctev_loc       = loc
+                         , ctev_rewriters = emptyRewriterSet }
 
 -- | Create a new Wanted constraint with the given 'CtOrigin', and
 -- location information taken from the 'TcM' environment.
@@ -216,13 +225,20 @@ newWanteds orig = mapM (newWanted orig Nothing)
 -- Cloning constraints
 ----------------------------------------------
 
-cloneWanted :: Ct -> TcM Ct
-cloneWanted ct
-  | ev@(CtWanted { ctev_pred = pty, ctev_dest = HoleDest _ }) <- ctEvidence ct
+cloneWantedCtEv :: CtEvidence -> TcM CtEvidence
+cloneWantedCtEv ctev@(CtWanted { ctev_pred = pty, ctev_dest = HoleDest _ })
+  | isEqPrimPred pty
   = do { co_hole <- newCoercionHole pty
-       ; return (mkNonCanonical (ev { ctev_dest = HoleDest co_hole })) }
+       ; return (ctev { ctev_dest = HoleDest co_hole }) }
+  | SpecialPred ConcretePrimPred ty <- classifyPredType pty
+  = do { (co_hole, _) <- newConcreteHole (typeKind ty) ty
+       ; return (ctev { ctev_dest = HoleDest co_hole }) }
   | otherwise
-  = return ct
+  = pprPanic "cloneWantedCtEv" (ppr pty)
+cloneWantedCtEv ctev = return ctev
+
+cloneWanted :: Ct -> TcM Ct
+cloneWanted ct = mkNonCanonical <$> cloneWantedCtEv (ctEvidence ct)
 
 cloneWC :: WantedConstraints -> TcM WantedConstraints
 -- Clone all the evidence bindings in
@@ -252,19 +268,13 @@ emitWanted origin pty
        ; emitSimple $ mkNonCanonical ev
        ; return $ ctEvTerm ev }
 
-emitDerivedEqs :: CtOrigin -> [(TcType,TcType)] -> TcM ()
--- Emit some new derived nominal equalities
-emitDerivedEqs origin pairs
+emitWantedEqs :: CtOrigin -> [(TcType,TcType)] -> TcM ()
+-- Emit some new wanted nominal equalities
+emitWantedEqs origin pairs
   | null pairs
   = return ()
   | otherwise
-  = do { loc <- getCtLocM origin Nothing
-       ; emitSimples (listToBag (map (mk_one loc) pairs)) }
-  where
-    mk_one loc (ty1, ty2)
-       = mkNonCanonical $
-         CtDerived { ctev_pred = mkPrimEqPred ty1 ty2
-                   , ctev_loc = loc }
+  = mapM_ (uncurry (emitWantedEq origin TypeLevel Nominal)) pairs
 
 -- | Emits a new equality constraint
 emitWantedEq :: CtOrigin -> TypeOrKind -> Role -> TcType -> TcType -> TcM Coercion
@@ -272,8 +282,10 @@ emitWantedEq origin t_or_k role ty1 ty2
   = do { hole <- newCoercionHole pty
        ; loc <- getCtLocM origin (Just t_or_k)
        ; emitSimple $ mkNonCanonical $
-         CtWanted { ctev_pred = pty, ctev_dest = HoleDest hole
-                  , ctev_nosh = WDeriv, ctev_loc = loc }
+         CtWanted { ctev_pred = pty
+                  , ctev_dest = HoleDest hole
+                  , ctev_loc = loc
+                  , ctev_rewriters = rewriterSetFromTypes [ty1, ty2] }
        ; return (HoleCo hole) }
   where
     pty = mkPrimEqPredRole role ty1 ty2
@@ -284,10 +296,10 @@ emitWantedEvVar :: CtOrigin -> TcPredType -> TcM EvVar
 emitWantedEvVar origin ty
   = do { new_cv <- newEvVar ty
        ; loc <- getCtLocM origin Nothing
-       ; let ctev = CtWanted { ctev_dest = EvVarDest new_cv
-                             , ctev_pred = ty
-                             , ctev_nosh = WDeriv
-                             , ctev_loc  = loc }
+       ; let ctev = CtWanted { ctev_dest      = EvVarDest new_cv
+                             , ctev_pred      = ty
+                             , ctev_loc       = loc
+                             , ctev_rewriters = emptyRewriterSet }
        ; emitSimple $ mkNonCanonical ctev
        ; return new_cv }
 
@@ -302,7 +314,7 @@ emitNewExprHole occ ty
        ; ref <- newTcRef (pprPanic "unfilled unbound-variable evidence" (ppr u))
        ; let her = HER ref ty u
 
-       ; loc <- getCtLocM (ExprHoleOrigin occ) (Just TypeLevel)
+       ; loc <- getCtLocM (ExprHoleOrigin (Just occ)) (Just TypeLevel)
 
        ; let hole = Hole { hole_sort = ExprHole her
                          , hole_occ  = occ
@@ -353,7 +365,7 @@ newImplication
 newCoercionHole :: TcPredType -> TcM CoercionHole
 newCoercionHole pred_ty
   = do { co_var <- newEvVar pred_ty
-       ; traceTc "New coercion hole:" (ppr co_var)
+       ; traceTc "New coercion hole:" (ppr co_var <+> dcolon <+> ppr pred_ty)
        ; ref <- newMutVar Nothing
        ; return $ CoercionHole { ch_co_var = co_var, ch_ref = ref } }
 
@@ -411,6 +423,24 @@ checkCoercionHole cv co
              | otherwise
              = False
 
+-- | A coercion hole used to store evidence for `Concrete#` constraints.
+--
+-- See Note [The Concrete mechanism].
+type ConcreteHole = CoercionHole
+
+-- | Create a new (initially unfilled) coercion hole,
+-- to hold evidence for a @'Concrete#' (ty :: ki)@ constraint.
+newConcreteHole :: Kind -- ^ Kind of the thing we want to ensure is concrete (e.g. 'runtimeRepTy')
+                -> Type -- ^ Thing we want to ensure is concrete (e.g. some 'RuntimeRep')
+                -> TcM (ConcreteHole, TcType)
+                  -- ^ where to put the evidence, and a metavariable to store
+                  -- the concrete type
+newConcreteHole ki ty
+  = do { concrete_ty <- newFlexiTyVarTy ki
+       ; let co_ty = mkHeteroPrimEqPred ki ki ty concrete_ty
+       ; hole <- newCoercionHole co_ty
+       ; return (hole, concrete_ty) }
+
 {- **********************************************************************
 *
                       ExpType functions
@@ -2465,14 +2495,11 @@ zonkSkolemInfoAnon (InferSkol ntys) = do { ntys' <- mapM do_one ntys
 zonkSkolemInfoAnon skol_info = return skol_info
 
 {-
-%************************************************************************
-%*                                                                      *
-\subsection{Zonking -- the main work-horses: zonkTcType, zonkTcTyVar}
+************************************************************************
 *                                                                      *
-*              For internal use only!                                  *
+     Zonking -- the main work-horses: zonkTcType, zonkTcTyVar
 *                                                                      *
 ************************************************************************
-
 -}
 
 -- For unbound, mutable tyvars, zonkType uses the function given to it
@@ -2620,13 +2647,21 @@ zonkTidyOrigin env (KindEqOrigin ty1 ty2 orig t_or_k)
        ; return (env3, KindEqOrigin ty1' ty2' orig' t_or_k) }
 zonkTidyOrigin env (FunDepOrigin1 p1 o1 l1 p2 o2 l2)
   = do { (env1, p1') <- zonkTidyTcType env  p1
-       ; (env2, p2') <- zonkTidyTcType env1 p2
-       ; return (env2, FunDepOrigin1 p1' o1 l1 p2' o2 l2) }
+       ; (env2, o1') <- zonkTidyOrigin env1 o1
+       ; (env3, p2') <- zonkTidyTcType env2 p2
+       ; (env4, o2') <- zonkTidyOrigin env3 o2
+       ; return (env4, FunDepOrigin1 p1' o1' l1 p2' o2' l2) }
 zonkTidyOrigin env (FunDepOrigin2 p1 o1 p2 l2)
   = do { (env1, p1') <- zonkTidyTcType env  p1
        ; (env2, p2') <- zonkTidyTcType env1 p2
        ; (env3, o1') <- zonkTidyOrigin env2 o1
        ; return (env3, FunDepOrigin2 p1' o1' p2' l2) }
+zonkTidyOrigin env (InjTFOrigin1 pred1 orig1 loc1 pred2 orig2 loc2)
+  = do { (env1, pred1') <- zonkTidyTcType env  pred1
+       ; (env2, orig1') <- zonkTidyOrigin env1 orig1
+       ; (env3, pred2') <- zonkTidyTcType env2 pred2
+       ; (env4, orig2') <- zonkTidyOrigin env3 orig2
+       ; return (env4, InjTFOrigin1 pred1' orig1' loc1 pred2' orig2' loc2) }
 zonkTidyOrigin env (CycleBreakerOrigin orig)
   = do { (env1, orig') <- zonkTidyOrigin env orig
        ; return (env1, CycleBreakerOrigin orig') }
@@ -2636,6 +2671,10 @@ zonkTidyOrigin env (InstProvidedOrigin mod cls_inst)
 zonkTidyOrigin env (FixedRuntimeRepOrigin ty frr_orig)
   = do { (env1, ty') <- zonkTidyTcType env ty
        ; return (env1, FixedRuntimeRepOrigin ty' frr_orig)}
+zonkTidyOrigin env (WantedSuperclassOrigin pty orig)
+  = do { (env1, pty')  <- zonkTidyTcType env pty
+       ; (env2, orig') <- zonkTidyOrigin env1 orig
+       ; return (env2, WantedSuperclassOrigin pty' orig') }
 zonkTidyOrigin env orig = return (env, orig)
 
 zonkTidyOrigins :: TidyEnv -> [CtOrigin] -> TcM (TidyEnv, [CtOrigin])
@@ -2644,13 +2683,14 @@ zonkTidyOrigins = mapAccumLM zonkTidyOrigin
 ----------------
 tidyCt :: TidyEnv -> Ct -> Ct
 -- Used only in error reporting
-tidyCt env ct
-  = ct { cc_ev = tidy_ev (ctEvidence ct) }
-  where
-    tidy_ev :: CtEvidence -> CtEvidence
+tidyCt env ct = ct { cc_ev = tidyCtEvidence env (ctEvidence ct) }
+
+tidyCtEvidence :: TidyEnv -> CtEvidence -> CtEvidence
      -- NB: we do not tidy the ctev_evar field because we don't
      --     show it in error messages
-    tidy_ev ctev = ctev { ctev_pred = tidyType env (ctev_pred ctev) }
+tidyCtEvidence env ctev = ctev { ctev_pred = tidyType env ty }
+  where
+    ty  = ctev_pred ctev
 
 tidyHole :: TidyEnv -> Hole -> Hole
 tidyHole env h@(Hole { hole_ty = ty }) = h { hole_ty = tidyType env ty }
@@ -2728,3 +2768,49 @@ naughtyQuantification orig_ty tv escapees
                         ]
 
        ; failWithTcM (env, msg) }
+
+{-
+************************************************************************
+*                                                                      *
+             Checking for coercion holes
+*                                                                      *
+************************************************************************
+-}
+
+-- | Check whether any coercion hole in a RewriterSet is still unsolved.
+-- Does this by recursively looking through filled coercion holes until
+-- one is found that is not yet filled in, at which point this aborts.
+anyUnfilledCoercionHoles :: RewriterSet -> TcM Bool
+anyUnfilledCoercionHoles (RewriterSet set)
+  = nonDetStrictFoldUniqSet go (return False) set
+     -- this does not introduce non-determinism, because the only
+     -- monadic action is to read, and the combining function is
+     -- commutative
+  where
+    go :: CoercionHole -> TcM Bool -> TcM Bool
+    go hole m_acc = m_acc <||> check_hole hole
+
+    check_hole :: CoercionHole -> TcM Bool
+    check_hole hole = do { m_co <- unpackCoercionHole_maybe hole
+                         ; case m_co of
+                             Nothing -> return True  -- unfilled hole
+                             Just co -> unUCHM (check_co co) }
+
+    check_ty :: Type -> UnfilledCoercionHoleMonoid
+    check_co :: Coercion -> UnfilledCoercionHoleMonoid
+    (check_ty, _, check_co, _) = foldTyCo folder ()
+
+    folder :: TyCoFolder () UnfilledCoercionHoleMonoid
+    folder = TyCoFolder { tcf_view  = noView
+                        , tcf_tyvar = \ _ tv -> check_ty (tyVarKind tv)
+                        , tcf_covar = \ _ cv -> check_ty (varType cv)
+                        , tcf_hole  = \ _ -> UCHM . check_hole
+                        , tcf_tycobinder = \ _ _ _ -> () }
+
+newtype UnfilledCoercionHoleMonoid = UCHM { unUCHM :: TcM Bool }
+
+instance Semigroup UnfilledCoercionHoleMonoid where
+  UCHM l <> UCHM r = UCHM (l <||> r)
+
+instance Monoid UnfilledCoercionHoleMonoid where
+  mempty = UCHM (return False)
diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs
index ae35cea3a2..807ad0ab56 100644
--- a/compiler/GHC/Tc/Utils/TcType.hs
+++ b/compiler/GHC/Tc/Utils/TcType.hs
@@ -92,11 +92,12 @@ module GHC.Tc.Utils.TcType (
   orphNamesOfType, orphNamesOfCo,
   orphNamesOfTypes, orphNamesOfCoCon,
   getDFunTyKey, evVarPred,
+  ambigTkvsOfTy,
 
   ---------------------------------
   -- Predicate types
   mkMinimalBySCs, transSuperClasses,
-  pickQuantifiablePreds, pickCapturedPreds,
+  pickCapturedPreds,
   immSuperClasses, boxEqPred,
   isImprovementPred,
 
@@ -105,7 +106,7 @@ module GHC.Tc.Utils.TcType (
 
   -- * Finding "exact" (non-dead) type variables
   exactTyCoVarsOfType, exactTyCoVarsOfTypes,
-  anyRewritableTyVar, anyRewritableTyFamApp, anyRewritableCanEqLHS,
+  anyRewritableTyVar, anyRewritableTyFamApp,
 
   ---------------------------------
   -- Foreign import and export
@@ -231,6 +232,7 @@ import qualified GHC.LanguageExtensions as LangExt
 
 import Data.IORef
 import Data.List.NonEmpty( NonEmpty(..) )
+import Data.List ( partition )
 import {-# SOURCE #-} GHC.Tc.Types.Origin ( unkSkol, SkolemInfo )
 
 
@@ -847,15 +849,14 @@ isTyFamFree :: Type -> Bool
 -- ^ Check that a type does not contain any type family applications.
 isTyFamFree = null . tcTyFamInsts
 
-any_rewritable :: Bool    -- Ignore casts and coercions
-               -> EqRel   -- Ambient role
+any_rewritable :: EqRel   -- Ambient role
                -> (EqRel -> TcTyVar -> Bool)           -- check tyvar
                -> (EqRel -> TyCon -> [TcType] -> Bool) -- check type family
                -> (TyCon -> Bool)                      -- expand type synonym?
                -> TcType -> Bool
 -- Checks every tyvar and tyconapp (not including FunTys) within a type,
 -- ORing the results of the predicates above together
--- Do not look inside casts and coercions if 'ignore_cos' is True
+-- Do not look inside casts and coercions
 -- See Note [anyRewritableTyVar must be role-aware]
 --
 -- This looks like it should use foldTyCo, but that function is
@@ -864,7 +865,7 @@ any_rewritable :: Bool    -- Ignore casts and coercions
 --
 -- See Note [Rewritable] in GHC.Tc.Solver.InertSet for a specification for this function.
 {-# INLINE any_rewritable #-} -- this allows specialization of predicates
-any_rewritable ignore_cos role tv_pred tc_pred should_expand
+any_rewritable role tv_pred tc_pred should_expand
   = go role emptyVarSet
   where
     go_tv rl bvs tv | tv `elemVarSet` bvs = False
@@ -890,8 +891,8 @@ any_rewritable ignore_cos role tv_pred tc_pred should_expand
       where arg_rep = getRuntimeRep arg -- forgetting these causes #17024
             res_rep = getRuntimeRep res
     go rl bvs (ForAllTy tv ty)   = go rl (bvs `extendVarSet` binderVar tv) ty
-    go rl bvs (CastTy ty co)     = go rl bvs ty || go_co rl bvs co
-    go rl bvs (CoercionTy co)    = go_co rl bvs co  -- ToDo: check
+    go rl bvs (CastTy ty _)      = go rl bvs ty
+    go _  _   (CoercionTy _)     = False
 
     go_tc NomEq  bvs _  tys = any (go NomEq bvs) tys
     go_tc ReprEq bvs tc tys = any (go_arg bvs)
@@ -901,19 +902,12 @@ any_rewritable ignore_cos role tv_pred tc_pred should_expand
     go_arg bvs (Representational, ty) = go ReprEq bvs ty
     go_arg _   (Phantom,          _)  = False  -- We never rewrite with phantoms
 
-    go_co rl bvs co
-      | ignore_cos = False
-      | otherwise  = anyVarSet (go_tv rl bvs) (tyCoVarsOfCo co)
-      -- We don't have an equivalent of anyRewritableTyVar for coercions
-      -- (at least not yet) so take the free vars and test them
-
-anyRewritableTyVar :: Bool     -- Ignore casts and coercions
-                   -> EqRel    -- Ambient role
+anyRewritableTyVar :: EqRel    -- Ambient role
                    -> (EqRel -> TcTyVar -> Bool)  -- check tyvar
                    -> TcType -> Bool
 -- See Note [Rewritable] in GHC.Tc.Solver.InertSet for a specification for this function.
-anyRewritableTyVar ignore_cos role pred
-  = any_rewritable ignore_cos role pred
+anyRewritableTyVar role pred
+  = any_rewritable role pred
       (\ _ _ _ -> False) -- no special check for tyconapps
                          -- (this False is ORed with other results, so it
                          --  really means "do nothing special"; the arguments
@@ -930,18 +924,7 @@ anyRewritableTyFamApp :: EqRel   -- Ambient role
   -- always ignores casts & coercions
 -- See Note [Rewritable] in GHC.Tc.Solver.InertSet for a specification for this function.
 anyRewritableTyFamApp role check_tyconapp
-  = any_rewritable True role (\ _ _ -> False) check_tyconapp (not . isFamFreeTyCon)
-
--- This version is used by shouldSplitWD. It *does* look in casts
--- and coercions, and it always expands type synonyms whose RHSs mention
--- type families.
--- See Note [Rewritable] in GHC.Tc.Solver.InertSet for a specification for this function.
-anyRewritableCanEqLHS :: EqRel   -- Ambient role
-                      -> (EqRel -> TcTyVar -> Bool)            -- check tyvar
-                      -> (EqRel -> TyCon -> [TcType] -> Bool)  -- check type family
-                      -> TcType -> Bool
-anyRewritableCanEqLHS role check_tyvar check_tyconapp
-  = any_rewritable False role check_tyvar check_tyconapp (not . isFamFreeTyCon)
+  = any_rewritable role (\ _ _ -> False) check_tyconapp (not . isFamFreeTyCon)
 
 {- Note [anyRewritableTyVar must be role-aware]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1170,6 +1153,16 @@ findDupTyVarTvs prs
     eq_snd (_,tv1) (_,tv2) = tv1 == tv2
     mk_result_prs ((n1,_) :| xs) = map (\(n2,_) -> (n1,n2)) xs
 
+-- | Returns the (kind, type) variables in a type that are
+-- as-yet-unknown: metavariables and RuntimeUnks
+ambigTkvsOfTy :: TcType -> ([Var],[Var])
+ambigTkvsOfTy ty
+  = partition (`elemVarSet` dep_tkv_set) ambig_tkvs
+  where
+    tkvs        = tyCoVarsOfTypeList ty
+    ambig_tkvs  = filter isAmbiguousTyVar tkvs
+    dep_tkv_set = tyCoVarsOfTypes (map tyVarKind tkvs)
+
 {-
 ************************************************************************
 *                                                                      *
@@ -1774,71 +1767,7 @@ evVarPred var = varType var
   -- partial signatures, (isEvVarType kappa) will return False. But
   -- nothing is wrong.  So I just removed the ASSERT.
 
-------------------
--- | When inferring types, should we quantify over a given predicate?
--- Generally true of classes; generally false of equality constraints.
--- Equality constraints that mention quantified type variables and
--- implicit variables complicate the story. See Notes
--- [Inheriting implicit parameters] and [Quantifying over equality constraints]
-pickQuantifiablePreds
-  :: TyVarSet           -- Quantifying over these
-  -> TcThetaType        -- Proposed constraints to quantify
-  -> TcThetaType        -- A subset that we can actually quantify
--- This function decides whether a particular constraint should be
--- quantified over, given the type variables that are being quantified
-pickQuantifiablePreds qtvs theta
-  = let flex_ctxt = True in  -- Quantify over non-tyvar constraints, even without
-                             -- -XFlexibleContexts: see #10608, #10351
-         -- flex_ctxt <- xoptM Opt_FlexibleContexts
-    mapMaybe (pick_me flex_ctxt) theta
-  where
-    pick_me flex_ctxt pred
-      = case classifyPredType pred of
-
-          ClassPred cls tys
-            | Just {} <- isCallStackPred cls tys
-              -- NEVER infer a CallStack constraint.  Otherwise we let
-              -- the constraints bubble up to be solved from the outer
-              -- context, or be defaulted when we reach the top-level.
-              -- See Note [Overview of implicit CallStacks]
-            -> Nothing
-
-            | isIPClass cls
-            -> Just pred -- See Note [Inheriting implicit parameters]
-
-            | pick_cls_pred flex_ctxt cls tys
-            -> Just pred
-
-          EqPred eq_rel ty1 ty2
-            | quantify_equality eq_rel ty1 ty2
-            , Just (cls, tys) <- boxEqPred eq_rel ty1 ty2
-              -- boxEqPred: See Note [Lift equality constraints when quantifying]
-            , pick_cls_pred flex_ctxt cls tys
-            -> Just (mkClassPred cls tys)
-
-          IrredPred ty
-            | tyCoVarsOfType ty `intersectsVarSet` qtvs
-            -> Just pred
-
-          _ -> Nothing
-
-
-    pick_cls_pred flex_ctxt cls tys
-      = tyCoVarsOfTypes tys `intersectsVarSet` qtvs
-        && (checkValidClsArgs flex_ctxt cls tys)
-           -- Only quantify over predicates that checkValidType
-           -- will pass!  See #10351.
-
-    -- See Note [Quantifying over equality constraints]
-    quantify_equality NomEq  ty1 ty2 = quant_fun ty1 || quant_fun ty2
-    quantify_equality ReprEq _   _   = True
-
-    quant_fun ty
-      = case tcSplitTyConApp_maybe ty of
-          Just (tc, tys) | isTypeFamilyTyCon tc
-                         -> tyCoVarsOfTypes tys `intersectsVarSet` qtvs
-          _ -> False
-
+---------------------------
 boxEqPred :: EqRel -> Type -> Type -> Maybe (Class, [Type])
 -- Given (t1 ~# t2) or (t1 ~R# t2) return the boxed version
 --       (t1 ~ t2)  or (t1 `Coercible` t2)
@@ -2013,71 +1942,6 @@ Notice that
 
 See also GHC.Tc.TyCl.Utils.checkClassCycles.
 
-Note [Lift equality constraints when quantifying]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We can't quantify over a constraint (t1 ~# t2) because that isn't a
-predicate type; see Note [Types for coercions, predicates, and evidence]
-in GHC.Core.TyCo.Rep.
-
-So we have to 'lift' it to (t1 ~ t2).  Similarly (~R#) must be lifted
-to Coercible.
-
-This tiresome lifting is the reason that pick_me (in
-pickQuantifiablePreds) returns a Maybe rather than a Bool.
-
-Note [Quantifying over equality constraints]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Should we quantify over an equality constraint (s ~ t)?  In general, we don't.
-Doing so may simply postpone a type error from the function definition site to
-its call site.  (At worst, imagine (Int ~ Bool)).
-
-However, consider this
-         forall a. (F [a] ~ Int) => blah
-Should we quantify over the (F [a] ~ Int)?  Perhaps yes, because at the call
-site we will know 'a', and perhaps we have instance  F [Bool] = Int.
-So we *do* quantify over a type-family equality where the arguments mention
-the quantified variables.
-
-Note [Inheriting implicit parameters]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider this:
-
-        f x = (x::Int) + ?y
-
-where f is *not* a top-level binding.
-From the RHS of f we'll get the constraint (?y::Int).
-There are two types we might infer for f:
-
-        f :: Int -> Int
-
-(so we get ?y from the context of f's definition), or
-
-        f :: (?y::Int) => Int -> Int
-
-At first you might think the first was better, because then
-?y behaves like a free variable of the definition, rather than
-having to be passed at each call site.  But of course, the WHOLE
-IDEA is that ?y should be passed at each call site (that's what
-dynamic binding means) so we'd better infer the second.
-
-BOTTOM LINE: when *inferring types* you must quantify over implicit
-parameters, *even if* they don't mention the bound type variables.
-Reason: because implicit parameters, uniquely, have local instance
-declarations. See pickQuantifiablePreds.
-
-Note [Quantifying over equality constraints]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Should we quantify over an equality constraint (s ~ t)?  In general, we don't.
-Doing so may simply postpone a type error from the function definition site to
-its call site.  (At worst, imagine (Int ~ Bool)).
-
-However, consider this
-         forall a. (F [a] ~ Int) => blah
-Should we quantify over the (F [a] ~ Int).  Perhaps yes, because at the call
-site we will know 'a', and perhaps we have instance  F [Bool] = Int.
-So we *do* quantify over a type-family equality where the arguments mention
-the quantified variables.
-
 ************************************************************************
 *                                                                      *
       Classifying types
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
diff --git a/compiler/GHC/Tc/Utils/Zonk.hs b/compiler/GHC/Tc/Utils/Zonk.hs
index 436543b095..ba6c98905f 100644
--- a/compiler/GHC/Tc/Utils/Zonk.hs
+++ b/compiler/GHC/Tc/Utils/Zonk.hs
@@ -68,7 +68,6 @@ import GHC.Utils.Outputable
 import GHC.Utils.Misc
 import GHC.Utils.Panic
 import GHC.Utils.Panic.Plain
-import GHC.Utils.Constants (debugIsOn)
 
 import GHC.Core.Multiplicity
 import GHC.Core
@@ -511,14 +510,14 @@ zonkLocalBinds env (HsIPBinds x (IPBinds dict_binds binds )) = do
     new_binds <- mapM (wrapLocMA zonk_ip_bind) binds
     let
         env1 = extendIdZonkEnvRec env
-                 [ n | (L _ (IPBind _ (Right n) _)) <- new_binds]
+                 [ n | (L _ (IPBind n _ _)) <- new_binds]
     (env2, new_dict_binds) <- zonkTcEvBinds env1 dict_binds
     return (env2, HsIPBinds x (IPBinds new_dict_binds new_binds))
   where
-    zonk_ip_bind (IPBind x n e)
-        = do n' <- mapIPNameTc (zonkIdBndr env) n
+    zonk_ip_bind (IPBind dict_id n e)
+        = do dict_id' <- zonkIdBndr env dict_id
              e' <- zonkLExpr env e
-             return (IPBind x n' e')
+             return (IPBind dict_id' n e')
 
 ---------------------------------------------
 zonkRecMonoBinds :: ZonkEnv -> LHsBinds GhcTc -> TcM (ZonkEnv, LHsBinds GhcTc)
@@ -1318,13 +1317,6 @@ zonkRecUpdFields env = mapM zonk_rbind
            ; return (L l (fld { hfbLHS = fmap ambiguousFieldOcc new_id
                               , hfbRHS = new_expr })) }
 
--------------------------------------------------------------------------
-mapIPNameTc :: (a -> TcM b) -> Either (LocatedAn NoEpAnns  HsIPName) a
-            -> TcM (Either (LocatedAn NoEpAnns HsIPName) b)
-mapIPNameTc _ (Left x)  = return (Left x)
-mapIPNameTc f (Right x) = do r <- f x
-                             return (Right r)
-
 {-
 ************************************************************************
 *                                                                      *
@@ -1833,6 +1825,13 @@ commitFlexi flexi tv zonked_kind
       SkolemiseFlexi  -> return (mkTyVarTy (mkTyVar name zonked_kind))
 
       DefaultFlexi
+          -- Normally, RuntimeRep variables are defaulted in TcMType.defaultTyVar
+          -- But that sees only type variables that appear in, say, an inferred type
+          -- Defaulting here in the zonker is needed to catch e.g.
+          --    y :: Bool
+          --    y = (\x -> True) undefined
+          -- We need *some* known RuntimeRep for the x and undefined, but no one
+          -- will choose it until we get here, in the zonker.
         | isRuntimeRepTy zonked_kind
         -> do { traceTc "Defaulting flexi tyvar to LiftedRep:" (pprTyVar tv)
               ; return liftedRepTy }
@@ -1877,11 +1876,6 @@ zonkCoHole env hole@(CoercionHole { ch_ref = ref, ch_co_var = cv })
               -- (undeferred) type errors. Originally, I put in a panic
               -- here, but that caused too many uses of `failIfErrsM`.
            Nothing -> do { traceTc "Zonking unfilled coercion hole" (ppr hole)
-                         ; when debugIsOn $
-                           whenNoErrs $
-                           massertPpr False
-                                      (text "Type-correct unfilled coercion hole"
-                                       <+> ppr hole)
                          ; cv' <- zonkCoVar cv
                          ; return $ mkCoVarCo cv' } }
                              -- This will be an out-of-scope variable, but keeping