Simplify treatment of heterogeneous equality

Previously, if we had a [W] (a :: k1) ~ (rhs :: k2), we would
spit out a [D] k1 ~ k2 and part the W as irreducible, hoping for
a unification. But we needn't do this. Instead, we now spit out
a [W] co :: k2 ~ k1 and then use co to cast the rhs of the original
Wanted. This means that we retain the connection between the
spat-out constraint and the original.

The problem with this new approach is that we cannot use the
casted equality for substitution; it's too like wanteds-rewriting-
wanteds. So, we forbid CTyEqCans that mention coercion holes.

All the details are in Note [Equalities with incompatible kinds]
in TcCanonical.

There are a few knock-on effects, documented where they occur.

While debugging an error in this patch, Simon and I ran into
infelicities in how patterns and matches are printed; we made
small improvements.

This patch includes mitigations for #17828, which causes spurious
pattern-match warnings. When #17828 is fixed, these lines should
be removed.

12 files changed, 442 insertions, 367 deletions

diff --git a/compiler/typecheck/Constraint.hs b/compiler/typecheck/Constraint.hs
index 4855b5c57c..20a1a7d774 100644
--- a/compiler/typecheck/Constraint.hs
+++ b/compiler/typecheck/Constraint.hs
@@ -14,7 +14,7 @@ module Constraint (
         QCInst(..), isPendingScInst,
 
         -- Canonical constraints
-        Xi, Ct(..), Cts, emptyCts, andCts, andManyCts, pprCts,
+        Xi, Ct(..), Cts, CtIrredStatus(..), emptyCts, andCts, andManyCts, pprCts,
         singleCt, listToCts, ctsElts, consCts, snocCts, extendCtsList,
         isEmptyCts, isCTyEqCan, isCFunEqCan,
         isPendingScDict, superClassesMightHelp, getPendingWantedScs,
@@ -25,7 +25,7 @@ module Constraint (
         ctEvidence, ctLoc, setCtLoc, ctPred, ctFlavour, ctEqRel, ctOrigin,
         ctEvId, mkTcEqPredLikeEv,
         mkNonCanonical, mkNonCanonicalCt, mkGivens,
-        mkIrredCt, mkInsolubleCt,
+        mkIrredCt,
         ctEvPred, ctEvLoc, ctEvOrigin, ctEvEqRel,
         ctEvExpr, ctEvTerm, ctEvCoercion, ctEvEvId,
         tyCoVarsOfCt, tyCoVarsOfCts,
@@ -145,13 +145,12 @@ data Ct
     }
 
   | CIrredCan {  -- These stand for yet-unusable predicates
-      cc_ev    :: CtEvidence,   -- See Note [Ct/evidence invariant]
-      cc_insol :: Bool   -- True  <=> definitely an error, can never be solved
-                         -- False <=> might be soluble
+      cc_ev     :: CtEvidence,   -- See Note [Ct/evidence invariant]
+      cc_status :: CtIrredStatus
 
         -- For the might-be-soluble case, the ctev_pred of the evidence is
         -- of form   (tv xi1 xi2 ... xin)   with a tyvar at the head
-        --      or   (tv1 ~ ty2)   where the CTyEqCan  kind invariant fails
+        --      or   (tv1 ~ ty2)   where the CTyEqCan  kind invariant (TyEq:K) fails
         --      or   (F tys ~ ty)  where the CFunEqCan kind invariant fails
         -- See Note [CIrredCan constraints]
 
@@ -163,19 +162,21 @@ data Ct
   | CTyEqCan {  -- tv ~ rhs
        -- Invariants:
        --   * See Note [inert_eqs: the inert equalities] in TcSMonad
-       --   * tv not in tvs(rhs)   (occurs check)
-       --   * If tv is a TauTv, then rhs has no foralls
+       --   * (TyEq:OC) tv not in deep tvs(rhs)   (occurs check)
+       --   * (TyEq:F) If tv is a TauTv, then rhs has no foralls
        --       (this avoids substituting a forall for the tyvar in other types)
-       --   * tcTypeKind ty `tcEqKind` tcTypeKind tv; Note [Ct kind invariant]
-       --   * rhs may have at most one top-level cast
-       --   * rhs (perhaps under the one cast) is *almost function-free*,
+       --   * (TyEq:K) tcTypeKind ty `tcEqKind` tcTypeKind tv; Note [Ct kind invariant]
+       --   * (TyEq:AFF) rhs (perhaps under the one cast) is *almost function-free*,
        --       See Note [Almost function-free]
-       --   * If the equality is representational, rhs has no top-level newtype
+       --   * (TyEq:N) If the equality is representational, rhs has no top-level newtype
        --     See Note [No top-level newtypes on RHS of representational
        --     equalities] in TcCanonical
-       --   * If rhs (perhaps under the cast) is also a tv, then it is oriented
+       --   * (TyEq:TV) If rhs (perhaps under the cast) is also a tv, then it is oriented
        --     to give best chance of
        --     unification happening; eg if rhs is touchable then lhs is too
+       --     See TcCanonical Note [Canonical orientation for tyvar/tyvar equality constraints]
+       --   * (TyEq:H) The RHS has no blocking coercion holes. See TcCanonical
+       --     Note [Equalities with incompatible kinds], wrinkle (2)
       cc_ev     :: CtEvidence, -- See Note [Ct/evidence invariant]
       cc_tyvar  :: TcTyVar,
       cc_rhs    :: TcType,     -- Not necessarily function-free (hence not Xi)
@@ -241,6 +242,21 @@ data HoleSort = ExprHole
               | TypeHole
                  -- ^ A hole in a type (PartialTypeSignatures)
 
+------------
+-- | Used to indicate extra information about why a CIrredCan is irreducible
+data CtIrredStatus
+  = InsolubleCIS   -- this constraint will never be solved
+  | BlockedCIS     -- this constraint is blocked on a coercion hole
+                   -- The hole will appear in the ctEvPred of the constraint with this status
+                   -- See Note [Equalities with incompatible kinds] in TcCanonical
+                   -- Wrinkle (4a)
+  | OtherCIS
+
+instance Outputable CtIrredStatus where
+  ppr InsolubleCIS = text "(insoluble)"
+  ppr BlockedCIS   = text "(blocked)"
+  ppr OtherCIS     = text "(soluble)"
+
 {- Note [Hole constraints]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 CHoleCan constraints are used for two kinds of holes,
@@ -296,7 +312,8 @@ responds True to isTypeFamilyTyCon), except (possibly)
  * under a forall, or
  * in a coercion (either in a CastTy or a CercionTy)
 
-The RHS of a CTyEqCan must be almost function-free. This is for two reasons:
+The RHS of a CTyEqCan must be almost function-free, invariant (TyEq:AFF).
+This is for two reasons:
 
 1. There cannot be a top-level function. If there were, the equality should
    really be a CFunEqCan, not a CTyEqCan.
@@ -346,11 +363,8 @@ mkNonCanonical ev = CNonCanonical { cc_ev = ev }
 mkNonCanonicalCt :: Ct -> Ct
 mkNonCanonicalCt ct = CNonCanonical { cc_ev = cc_ev ct }
 
-mkIrredCt :: CtEvidence -> Ct
-mkIrredCt ev = CIrredCan { cc_ev = ev, cc_insol = False }
-
-mkInsolubleCt :: CtEvidence -> Ct
-mkInsolubleCt ev = CIrredCan { cc_ev = ev, cc_insol = True }
+mkIrredCt :: CtIrredStatus -> CtEvidence -> Ct
+mkIrredCt status ev = CIrredCan { cc_ev = ev, cc_status = status }
 
 mkGivens :: CtLoc -> [EvId] -> [Ct]
 mkGivens loc ev_ids
@@ -409,9 +423,7 @@ instance Outputable Ct where
          CDictCan { cc_pend_sc = pend_sc }
             | pend_sc   -> text "CDictCan(psc)"
             | otherwise -> text "CDictCan"
-         CIrredCan { cc_insol = insol }
-            | insol     -> text "CIrredCan(insol)"
-            | otherwise -> text "CIrredCan(sol)"
+         CIrredCan { cc_status = status } -> text "CIrredCan" <> ppr status
          CHoleCan { cc_occ = occ } -> text "CHoleCan:" <+> ppr occ
          CQuantCan (QCI { qci_pend_sc = pend_sc })
             | pend_sc   -> text "CQuantCan(psc)"
@@ -439,14 +451,10 @@ tyCoVarsOfCtList = fvVarList . tyCoFVsOfCt
 -- | Returns free variables of constraints as a composable FV computation.
 -- See Note [Deterministic FV] in FV.
 tyCoFVsOfCt :: Ct -> FV
-tyCoFVsOfCt (CTyEqCan { cc_tyvar = tv, cc_rhs = xi })
-  = tyCoFVsOfType xi `unionFV` FV.unitFV tv
-                     `unionFV` tyCoFVsOfType (tyVarKind tv)
-tyCoFVsOfCt (CFunEqCan { cc_tyargs = tys, cc_fsk = fsk })
-  = tyCoFVsOfTypes tys `unionFV` FV.unitFV fsk
-                       `unionFV` tyCoFVsOfType (tyVarKind fsk)
-tyCoFVsOfCt (CDictCan { cc_tyargs = tys }) = tyCoFVsOfTypes tys
 tyCoFVsOfCt ct = tyCoFVsOfType (ctPred ct)
+  -- This must consult only the ctPred, so that it gets *tidied* fvs if the
+  -- constraint has been tidied. Tidying a constraint does not tidy the
+  -- fields of the Ct, only the predicate in the CtEvidence.
 
 -- | Returns free variables of a bag of constraints as a non-deterministic
 -- set. See Note [Deterministic FV] in FV.
@@ -549,18 +557,15 @@ isDroppableCt ct
 
     keep_deriv
       = case ct of
-          CHoleCan {} -> True
-          CIrredCan { cc_insol = insoluble }
-                      -> keep_eq insoluble
-          _           -> keep_eq False
+          CHoleCan {}                            -> True
+          CIrredCan { cc_status = InsolubleCIS } -> keep_eq True
+          _                                      -> keep_eq False
 
     keep_eq definitely_insoluble
        | isGivenOrigin orig    -- Arising only from givens
        = definitely_insoluble  -- Keep only definitely insoluble
        | otherwise
        = case orig of
-           KindEqOrigin {} -> True    -- See Note [Dropping derived constraints]
-
            -- See Note [Dropping derived constraints]
            -- For fundeps, drop wanted/wanted interactions
            FunDepOrigin2 {} -> True   -- Top-level/Wanted
@@ -610,12 +615,6 @@ But (tiresomely) we do keep *some* Derived constraints:
  * Type holes are derived constraints, because they have no evidence
    and we want to keep them, so we get the error report
 
- * Insoluble kind equalities (e.g. [D] * ~ (* -> *)), with
-   KindEqOrigin, may arise from a type equality a ~ Int#, say.  See
-   Note [Equalities with incompatible kinds] in TcCanonical.
-   Keeping these around produces better error messages, in practice.
-   E.g., test case dependent/should_fail/T11471
-
  * We keep most derived equalities arising from functional dependencies
       - Given/Given interactions (subset of FunDepOrigin1):
         The definitely-insoluble ones reflect unreachable code.
@@ -664,7 +663,6 @@ isDerivedCt = isDerived . ctEvidence
 
 isCTyEqCan :: Ct -> Bool
 isCTyEqCan (CTyEqCan {})  = True
-isCTyEqCan (CFunEqCan {}) = False
 isCTyEqCan _              = False
 
 isCDictCan_Maybe :: Ct -> Maybe Class
@@ -990,8 +988,8 @@ insolubleEqCt :: Ct -> Bool
 --                   True for  Int ~ F a Int
 --               but False for  Maybe Int ~ F a Int Int
 --               (where F is an arity-1 type function)
-insolubleEqCt (CIrredCan { cc_insol = insol }) = insol
-insolubleEqCt _                                = False
+insolubleEqCt (CIrredCan { cc_status = InsolubleCIS }) = True
+insolubleEqCt _                                        = False
 
 instance Outputable WantedConstraints where
   ppr (WC {wc_simple = s, wc_impl = i})
diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index 33b15aa292..7dbe32d9c0 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -16,7 +16,7 @@ import GhcPrelude
 import Constraint
 import GHC.Core.Predicate
 import TcOrigin
-import TcUnify( swapOverTyVars, metaTyVarUpdateOK )
+import TcUnify( swapOverTyVars, metaTyVarUpdateOK, MetaTyVarUpdateResult(..) )
 import TcType
 import GHC.Core.Type
 import TcFlatten
@@ -95,7 +95,7 @@ canonicalize (CNonCanonical { cc_ev = ev })
       EqPred eq_rel ty1 ty2 -> do traceTcS "canEvNC:eq" (ppr ty1 $$ ppr ty2)
                                   canEqNC    ev eq_rel ty1 ty2
       IrredPred {}          -> do traceTcS "canEvNC:irred" (ppr pred)
-                                  canIrred ev
+                                  canIrred OtherCIS ev
       ForAllPred tvs theta p -> do traceTcS "canEvNC:forall" (ppr pred)
                                    canForAllNC ev tvs theta p
   where
@@ -104,7 +104,7 @@ canonicalize (CNonCanonical { cc_ev = ev })
 canonicalize (CQuantCan (QCI { qci_ev = ev, qci_pend_sc = pend_sc }))
   = canForAll ev pend_sc
 
-canonicalize (CIrredCan { cc_ev = ev })
+canonicalize (CIrredCan { cc_ev = ev, cc_status = status })
   | EqPred eq_rel ty1 ty2 <- classifyPredType (ctEvPred ev)
   = -- For insolubles (all of which are equalities, do /not/ flatten the arguments
     -- In #14350 doing so led entire-unnecessary and ridiculously large
@@ -114,7 +114,7 @@ canonicalize (CIrredCan { cc_ev = ev })
     canEqNC ev eq_rel ty1 ty2
 
   | otherwise
-  = canIrred ev
+  = canIrred status ev
 
 canonicalize (CDictCan { cc_ev = ev, cc_class  = cls
                        , cc_tyargs = xis, cc_pend_sc = pend_sc })
@@ -704,9 +704,9 @@ See also Note [Evidence for quantified constraints] in GHC.Core.Predicate.
 ************************************************************************
 -}
 
-canIrred :: CtEvidence -> TcS (StopOrContinue Ct)
+canIrred :: CtIrredStatus -> CtEvidence -> TcS (StopOrContinue Ct)
 -- Precondition: ty not a tuple and no other evidence form
-canIrred ev
+canIrred status ev
   = do { let pred = ctEvPred ev
        ; traceTcS "can_pred" (text "IrredPred = " <+> ppr pred)
        ; (xi,co) <- flatten FM_FlattenAll ev pred -- co :: xi ~ pred
@@ -716,7 +716,7 @@ canIrred ev
            ClassPred cls tys     -> canClassNC new_ev cls tys
            EqPred eq_rel ty1 ty2 -> canEqNC new_ev eq_rel ty1 ty2
            _                     -> continueWith $
-                                    mkIrredCt new_ev } }
+                                    mkIrredCt status new_ev } }
 
 canHole :: CtEvidence -> OccName -> HoleSort -> TcS (StopOrContinue Ct)
 canHole ev occ hole_sort
@@ -984,6 +984,7 @@ can_eq_nc' True _rdr_env _envs ev ReprEq ty1 _ ty2 _
 
 -- When working with ReprEq, unwrap newtypes.
 -- See Note [Unwrap newtypes first]
+-- This must be above the TyVarTy case, in order to guarantee (TyEq:N)
 can_eq_nc' _flat rdr_env envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
   | ReprEq <- eq_rel
   , Just stuff1 <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty1
@@ -995,8 +996,10 @@ can_eq_nc' _flat rdr_env envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
 
 -- Then, get rid of casts
 can_eq_nc' flat _rdr_env _envs ev eq_rel (CastTy ty1 co1) _ ty2 ps_ty2
+  | not (isTyVarTy ty2)  -- See (3) in Note [Equalities with incompatible kinds]
   = canEqCast flat ev eq_rel NotSwapped ty1 co1 ty2 ps_ty2
 can_eq_nc' flat _rdr_env _envs ev eq_rel ty1 ps_ty1 (CastTy ty2 co2) _
+  | not (isTyVarTy ty1)  -- See (3) in Note [Equalities with incompatible kinds]
   = canEqCast flat ev eq_rel IsSwapped ty2 co2 ty1 ps_ty1
 
 -- NB: pattern match on True: we want only flat types sent to canEqTyVar.
@@ -1051,8 +1054,8 @@ can_eq_nc' False rdr_env envs ev eq_rel _ ps_ty1 _ ps_ty2
 can_eq_nc' True _rdr_env _envs ev eq_rel _ ps_ty1 _ ps_ty2
   = do { traceTcS "can_eq_nc' catch-all case" (ppr ps_ty1 $$ ppr ps_ty2)
        ; case eq_rel of -- See Note [Unsolved equalities]
-            ReprEq -> continueWith (mkIrredCt ev)
-            NomEq  -> continueWith (mkInsolubleCt ev) }
+            ReprEq -> continueWith (mkIrredCt OtherCIS ev)
+            NomEq  -> continueWith (mkIrredCt InsolubleCIS ev) }
           -- No need to call canEqFailure/canEqHardFailure because they
           -- flatten, and the types involved here are already flat
 
@@ -1478,7 +1481,7 @@ canTyConApp ev eq_rel tc1 tys1 tc2 tys2
   -- See Note [Skolem abstract data] (at tyConSkolem)
   | tyConSkolem tc1 || tyConSkolem tc2
   = do { traceTcS "canTyConApp: skolem abstract" (ppr tc1 $$ ppr tc2)
-       ; continueWith (mkIrredCt ev) }
+       ; continueWith (mkIrredCt OtherCIS ev) }
 
   -- Fail straight away for better error messages
   -- See Note [Use canEqFailure in canDecomposableTyConApp]
@@ -1752,7 +1755,7 @@ canEqFailure ev ReprEq ty1 ty2
        ; traceTcS "canEqFailure with ReprEq" $
          vcat [ ppr ev, ppr ty1, ppr ty2, ppr xi1, ppr xi2 ]
        ; new_ev <- rewriteEqEvidence ev NotSwapped xi1 xi2 co1 co2
-       ; continueWith (mkIrredCt new_ev) }
+       ; continueWith (mkIrredCt OtherCIS new_ev) }
 
 -- | Call when canonicalizing an equality fails with utterly no hope.
 canEqHardFailure :: CtEvidence
@@ -1762,7 +1765,7 @@ canEqHardFailure ev ty1 ty2
   = do { (s1, co1) <- flatten FM_SubstOnly ev ty1
        ; (s2, co2) <- flatten FM_SubstOnly ev ty2
        ; new_ev <- rewriteEqEvidence ev NotSwapped s1 s2 co1 co2
-       ; continueWith (mkInsolubleCt new_ev) }
+       ; continueWith (mkIrredCt InsolubleCIS new_ev) }
 
 {-
 Note [Decomposing TyConApps]
@@ -1948,118 +1951,61 @@ canEqTyVar ev eq_rel swapped tv1 ps_xi1 xi2 ps_xi2
   | k1 `tcEqType` k2
   = canEqTyVarHomo ev eq_rel swapped tv1 ps_xi1 xi2 ps_xi2
 
-  -- So the LHS and RHS don't have equal kinds
-  -- Note [Flattening] in TcFlatten gives us (F2), which says that
-  -- flattening is always homogeneous (doesn't change kinds). But
-  -- perhaps by flattening the kinds of the two sides of the equality
-  -- at hand makes them equal. So let's try that.
   | otherwise
-  = do { (flat_k1, k1_co) <- flattenKind loc flav k1  -- k1_co :: flat_k1 ~N kind(xi1)
-       ; (flat_k2, k2_co) <- flattenKind loc flav k2  -- k2_co :: flat_k2 ~N kind(xi2)
-       ; traceTcS "canEqTyVar tried flattening kinds"
-                  (vcat [ sep [ parens (ppr tv1 <+> dcolon <+> ppr k1)
-                              , text "~"
-                              , parens (ppr xi2 <+> dcolon <+> ppr k2) ]
-                        , ppr flat_k1
-                        , ppr k1_co
-                        , ppr flat_k2
-                        , ppr k2_co ])
-
-         -- We know the LHS is a tyvar. So let's dump all the coercions on the RHS
-         -- If flat_k1 == flat_k2, let's dump all the coercions on the RHS and
-         -- then call canEqTyVarHomo. If they don't equal, just rewriteEqEvidence
-         -- (as an optimization, so that we don't have to flatten the kinds again)
-         -- and then emit a kind equality in canEqTyVarHetero.
-         -- See Note [Equalities with incompatible kinds]
-
-       ; let role = eqRelRole eq_rel
-       ; if flat_k1 `tcEqType` flat_k2
-         then do { let rhs_kind_co = mkTcSymCo k2_co `mkTcTransCo` k1_co
-                         -- :: kind(xi2) ~N kind(xi1)
-
-                       new_rhs     = xi2 `mkCastTy` rhs_kind_co
-                       ps_rhs      = ps_xi2 `mkCastTy` rhs_kind_co
-                       rhs_co      = mkTcGReflLeftCo role xi2 rhs_kind_co
-
-                 ; new_ev <- rewriteEqEvidence ev swapped xi1 new_rhs
-                                               (mkTcReflCo role xi1) rhs_co
-                       -- NB: rewriteEqEvidence executes a swap, if any, so we're
-                       -- NotSwapped now.
-                 ; canEqTyVarHomo new_ev eq_rel NotSwapped tv1 ps_xi1 new_rhs ps_rhs }
-         else
-    do { let sym_k1_co = mkTcSymCo k1_co  -- :: kind(xi1) ~N flat_k1
-             sym_k2_co = mkTcSymCo k2_co  -- :: kind(xi2) ~N flat_k2
-
-             new_lhs = xi1 `mkCastTy` sym_k1_co  -- :: flat_k1
-             new_rhs = xi2 `mkCastTy` sym_k2_co  -- :: flat_k2
-             ps_rhs  = ps_xi2 `mkCastTy` sym_k2_co
-
-             lhs_co = mkTcGReflLeftCo role xi1 sym_k1_co
-             rhs_co = mkTcGReflLeftCo role xi2 sym_k2_co
-               -- lhs_co :: (xi1 |> sym k1_co) ~ xi1
-               -- rhs_co :: (xi2 |> sym k2_co) ~ xi2
+  = canEqTyVarHetero ev eq_rel swapped tv1 ps_xi1 k1 xi2 ps_xi2 k2
 
-       ; new_ev <- rewriteEqEvidence ev swapped new_lhs new_rhs lhs_co rhs_co
-         -- no longer swapped, due to rewriteEqEvidence
-       ; canEqTyVarHetero new_ev eq_rel tv1 sym_k1_co flat_k1 ps_xi1
-                                        new_rhs flat_k2 ps_rhs } }
   where
-    xi1 = mkTyVarTy tv1
-
     k1 = tyVarKind tv1
     k2 = tcTypeKind xi2
 
-    loc  = ctEvLoc ev
-    flav = ctEvFlavour ev
-
-canEqTyVarHetero :: CtEvidence   -- :: (tv1 |> co1 :: ki1) ~ (xi2 :: ki2)
-                 -> EqRel
-                 -> TcTyVar -> TcCoercionN -> TcKind  -- tv1 |> co1 :: ki1
-                 -> TcType            -- pretty tv1 (*without* the coercion)
-                 -> TcType -> TcKind  -- xi2 :: ki2
-                 -> TcType            -- pretty xi2
+canEqTyVarHetero :: CtEvidence         -- :: (tv1 :: ki1) ~ (xi2 :: ki2)
+                 -> EqRel -> SwapFlag
+                 -> TcTyVar -> TcType  -- tv1, pretty tv1
+                 -> TcKind             -- ki1
+                 -> TcType -> TcType   -- xi2, pretty xi2 :: ki2
+                 -> TcKind             -- ki2
                  -> TcS (StopOrContinue Ct)
-canEqTyVarHetero ev eq_rel tv1 co1 ki1 ps_tv1 xi2 ki2 ps_xi2
+canEqTyVarHetero ev eq_rel swapped tv1 ps_tv1 ki1 xi2 ps_xi2 ki2
   -- See Note [Equalities with incompatible kinds]
-  | CtGiven { ctev_evar = evar } <- ev
-    -- unswapped: tm :: (lhs :: ki1) ~ (rhs :: ki2)
-    -- swapped  : tm :: (rhs :: ki2) ~ (lhs :: ki1)
-  = do { let kind_co = mkTcKindCo (mkTcCoVarCo evar)
-       ; kind_ev <- newGivenEvVar kind_loc (kind_pty, evCoercion kind_co)
-       ; let  -- kind_ev :: (ki1 :: *) ~ (ki2 :: *)   (whether swapped or not)
+  = do { kind_co <- emit_kind_co   -- :: ki2 ~N ki1
+
+       ; let  -- kind_co :: (ki2 :: *) ~N (ki1 :: *)   (whether swapped or not)
               -- co1     :: kind(tv1) ~N ki1
-              -- homo_co :: ki2 ~N kind(tv1)
-             homo_co = mkTcSymCo (ctEvCoercion kind_ev) `mkTcTransCo` mkTcSymCo co1
-             rhs'    = mkCastTy xi2 homo_co     -- :: kind(tv1)
-             ps_rhs' = mkCastTy ps_xi2 homo_co  -- :: kind(tv1)
-             rhs_co  = mkTcGReflLeftCo role xi2 homo_co
-               -- rhs_co :: (xi2 |> homo_co :: kind(tv1)) ~ xi2
-
-             lhs'   = mkTyVarTy tv1       -- :: kind(tv1)
-             lhs_co = mkTcGReflRightCo role lhs' co1
-               -- lhs_co :: (tv1 :: kind(tv1)) ~ (tv1 |> co1 :: ki1)
-
-       ; traceTcS "Hetero equality gives rise to given kind equality"
-           (ppr kind_ev <+> dcolon <+> ppr kind_pty)
-       ; emitWorkNC [kind_ev]
-       ; type_ev <- rewriteEqEvidence ev NotSwapped lhs' rhs' lhs_co rhs_co
-       ; canEqTyVarHomo type_ev eq_rel NotSwapped tv1 ps_tv1 rhs' ps_rhs' }
+             rhs'    = xi2    `mkCastTy` kind_co   -- :: ki1
+             ps_rhs' = ps_xi2 `mkCastTy` kind_co   -- :: ki1
+             rhs_co  = mkTcGReflLeftCo role xi2 kind_co
+               -- rhs_co :: (xi2 |> kind_co) ~ xi2
 
-  -- See Note [Equalities with incompatible kinds]
-  | otherwise   -- Wanted and Derived
-                -- NB: all kind equalities are Nominal
-  = do { emitNewDerivedEq kind_loc Nominal ki1 ki2
-             -- kind_ev :: (ki1 :: *) ~ (ki2 :: *)
-       ; traceTcS "Hetero equality gives rise to derived kind equality" $
-           ppr ev
-       ; continueWith (mkIrredCt ev) }
+             lhs'   = mkTyVarTy tv1  -- same as old lhs
+             lhs_co = mkTcReflCo role lhs'
+
+       ; traceTcS "Hetero equality gives rise to kind equality"
+           (ppr kind_co <+> dcolon <+> sep [ ppr ki2, text "~#", ppr ki1 ])
+       ; type_ev <- rewriteEqEvidence ev swapped lhs' rhs' lhs_co rhs_co
 
+          -- rewriteEqEvidence carries out the swap, so we're NotSwapped any more
+       ; canEqTyVarHomo type_ev eq_rel NotSwapped tv1 ps_tv1 rhs' ps_rhs' }
   where
-    kind_pty = mkHeteroPrimEqPred liftedTypeKind liftedTypeKind ki1 ki2
-    kind_loc = mkKindLoc (mkTyVarTy tv1 `mkCastTy` co1) xi2 loc
+    emit_kind_co :: TcS CoercionN
+    emit_kind_co
+      | CtGiven { ctev_evar = evar } <- ev
+      = do { let kind_co = maybe_sym $ mkTcKindCo (mkTcCoVarCo evar)  -- :: k2 ~ k1
+           ; kind_ev <- newGivenEvVar kind_loc (kind_pty, evCoercion kind_co)
+           ; emitWorkNC [kind_ev]
+           ; return (ctEvCoercion kind_ev) }
 
-    loc  = ctev_loc ev
-    role = eqRelRole eq_rel
+      | otherwise
+      = unifyWanted kind_loc Nominal ki2 ki1
+
+    loc      = ctev_loc ev
+    role     = eqRelRole eq_rel
+    kind_loc = mkKindLoc (mkTyVarTy tv1) xi2 loc
+    kind_pty = mkHeteroPrimEqPred liftedTypeKind liftedTypeKind ki2 ki1
+
+    maybe_sym = case swapped of
+          IsSwapped  -> id         -- if the input is swapped, then we already
+                                   -- will have k2 ~ k1
+          NotSwapped -> mkTcSymCo
 
 -- guaranteed that tcTypeKind lhs == tcTypeKind rhs
 canEqTyVarHomo :: CtEvidence
@@ -2074,14 +2020,10 @@ canEqTyVarHomo ev eq_rel swapped tv1 ps_xi1 xi2 _
   = canEqReflexive ev eq_rel (mkTyVarTy tv1)
     -- we don't need to check co because it must be reflexive
 
+    -- this guarantees (TyEq:TV)
   | Just (tv2, co2) <- tcGetCastedTyVar_maybe xi2
   , swapOverTyVars tv1 tv2
   = do { traceTcS "canEqTyVar swapOver" (ppr tv1 $$ ppr tv2 $$ ppr swapped)
-         -- FM_Avoid commented out: see Note [Lazy flattening] in TcFlatten
-         -- let fmode = FE { fe_ev = ev, fe_mode = FM_Avoid tv1' True }
-         -- Flatten the RHS less vigorously, to avoid gratuitous flattening
-         -- True <=> xi2 should not itself be a type-function application
-
        ; let role    = eqRelRole eq_rel
              sym_co2 = mkTcSymCo co2
              ty1     = mkTyVarTy tv1
@@ -2112,11 +2054,17 @@ canEqTyVar2 :: DynFlags
 -- LHS is an inert type variable,
 -- and RHS is fully rewritten, but with type synonyms
 -- preserved as much as possible
+-- guaranteed that tyVarKind lhs == typeKind rhs, for (TyEq:K)
+-- the "flat" requirement guarantees (TyEq:AFF)
+-- (TyEq:N) is checked in can_eq_nc', and (TyEq:TV) is handled in canEqTyVarHomo
 canEqTyVar2 dflags ev eq_rel swapped tv1 rhs
-  | Just rhs' <- metaTyVarUpdateOK dflags tv1 rhs  -- No occurs check
+    -- this next line checks also for coercion holes; see
+    -- Note [Equalities with incompatible kinds]
+  | MTVU_OK rhs' <- mtvu  -- No occurs check
      -- Must do the occurs check even on tyvar/tyvar
      -- equalities, in case have  x ~ (y :: ..x...)
      -- #12593
+     -- guarantees (TyEq:OC), (TyEq:F), and (TyEq:H)
   = do { new_ev <- rewriteEqEvidence ev swapped lhs rhs' rewrite_co1 rewrite_co2
        ; continueWith (CTyEqCan { cc_ev = new_ev, cc_tyvar = tv1
                                 , cc_rhs = rhs', cc_eq_rel = eq_rel }) }
@@ -2125,20 +2073,30 @@ canEqTyVar2 dflags ev eq_rel swapped tv1 rhs
                -- We must not use it for further rewriting!
   = do { traceTcS "canEqTyVar2 can't unify" (ppr tv1 $$ ppr rhs)
        ; new_ev <- rewriteEqEvidence ev swapped lhs rhs rewrite_co1 rewrite_co2
-       ; if isInsolubleOccursCheck eq_rel tv1 rhs
-         then continueWith (mkInsolubleCt new_ev)
+       ; let status | isInsolubleOccursCheck eq_rel tv1 rhs
+                    = InsolubleCIS
              -- If we have a ~ [a], it is not canonical, and in particular
              -- we don't want to rewrite existing inerts with it, otherwise
              -- we'd risk divergence in the constraint solver
 
-         else continueWith (mkIrredCt new_ev) }
+                    | MTVU_HoleBlocker <- mtvu
+                    = BlockedCIS
+             -- This is the case detailed in
+             -- Note [Equalities with incompatible kinds]
+
+                    | otherwise
+                    = OtherCIS
              -- A representational equality with an occurs-check problem isn't
              -- insoluble! For example:
              --   a ~R b a
              -- We might learn that b is the newtype Id.
              -- But, the occurs-check certainly prevents the equality from being
              -- canonical, and we might loop if we were to use it in rewriting.
+
+       ; continueWith (mkIrredCt status new_ev) }
   where
+    mtvu = metaTyVarUpdateOK dflags tv1 rhs
+
     role = eqRelRole eq_rel
 
     lhs = mkTyVarTy tv1
@@ -2162,57 +2120,92 @@ What do we do when we have an equality
 
   (tv :: k1) ~ (rhs :: k2)
 
-where k1 and k2 differ? This Note explores this treacherous area.
-
-We must proceed differently here depending on whether we have a Wanted
-or a Given. Consider this:
-
- [W] w :: (alpha :: k) ~ (Int :: Type)
-
-where k is a skolem. One possible way forward is this:
-
- [W] co :: k ~ Type
- [W] w :: (alpha :: k) ~ (Int |> sym co :: k)
-
-The next step will be to unify
-
-  alpha := Int |> sym co
+where k1 and k2 differ? Easy: we create a coercion that relates k1 and
+k2 and use this to cast. To wit, from
 
-Now, consider what error we'll report if we can't solve the "co"
-wanted. Its CtOrigin is the w wanted... which now reads (after zonking)
-Int ~ Int. The user thus sees that GHC can't solve Int ~ Int, which
-is embarrassing. See #11198 for more tales of destruction.
+  [X] (tv :: k1) ~ (rhs :: k2)
 
-The reason for this odd behavior is much the same as
-Note [Wanteds do not rewrite Wanteds] in Constraint: note that the
-new `co` is a Wanted.
+we go to
 
-The solution is then not to use `co` to "rewrite" -- that is, cast -- `w`, but
-instead to keep `w` heterogeneous and irreducible. Given that we're not using
-`co`, there is no reason to collect evidence for it, so `co` is born a
-Derived, with a CtOrigin of KindEqOrigin. When the Derived is solved (by
-unification), the original wanted (`w`) will get kicked out. We thus get
+  [noDerived X] co :: k2 ~ k1
+  [X]           (tv :: k1) ~ ((rhs |> co) :: k1)
 
-[D] _ :: k ~ Type
-[W] w :: (alpha :: k) ~ (Int :: Type)
-
-Note that the Wanted is unchanged and will be irreducible. This all happens
-in canEqTyVarHetero.
-
-Note that, if we had [G] co1 :: k ~ Type available, then we never get
-to canEqTyVarHetero: canEqTyVar tries flattening the kinds first. If
-we have [G] co1 :: k ~ Type, then flattening the kind of alpha would
-rewrite k to Type, and we would end up in canEqTyVarHomo.
-
-Successive canonicalizations of the same Wanted may produce
-duplicate Deriveds. Similar duplications can happen with fundeps, and there
-seems to be no easy way to avoid. I expect this case to be rare.
+where
 
-For Givens, this problem (the Wanteds-rewriting-Wanteds action of
-a kind coercion) doesn't bite, so a heterogeneous Given gives
-rise to a Given kind equality. No Deriveds here. We thus homogenise
-the Given (see the "homo_co" in the Given case in canEqTyVarHetero) and
-carry on with a homogeneous equality constraint.
+  noDerived G = G
+  noDerived _ = W
+
+Wrinkles:
+
+ (1) The noDerived step is because Derived equalities have no evidence.
+     And yet we absolutely need evidence to be able to proceed here.
+     Given evidence will use the KindCo coercion; Wanted evidence will
+     be a coercion hole. Even a Derived hetero equality begets a Wanted
+     kind equality.
+
+ (2) Though it would be sound to do so, we must not mark the rewritten Wanted
+       [W] (tv :: k1) ~ ((rhs |> co) :: k1)
+     as canonical in the inert set. In particular, we must not unify tv.
+     If we did, the Wanted becomes a Given (effectively), and then can
+     rewrite other Wanteds. But that's bad: See Note [Wanteds to not rewrite Wanteds]
+     in Constraint. The problem is about poor error messages. See #11198 for
+     tales of destruction.
+
+     So, we have an invariant on CTyEqCan (TyEq:H) that the RHS does not have
+     any coercion holes. This is checked in metaTyVarUpdateOK. We also
+     must be sure to kick out any constraints that mention coercion holes
+     when those holes get filled in.
+
+     (2a) We don't want to do this for CoercionHoles that witness
+          CFunEqCans (that are produced by the flattener), as these will disappear
+          once we unflatten. So we remember in the CoercionHole structure
+          whether the presence of the hole should block substitution or not.
+          A bit gross, this.
+
+     (2b) We must now absolutely make sure to kick out any constraints that
+          mention a newly-filled-in coercion hole. This is done in
+          kickOutAfterFillingCoercionHole.
+
+ (3) Suppose we have [W] (a :: k1) ~ (rhs :: k2). We duly follow the
+     algorithm detailed here, producing [W] co :: k2 ~ k1, and adding
+     [W] (a :: k1) ~ ((rhs |> co) :: k1) to the irreducibles. Some time
+     later, we solve co, and fill in co's coercion hole. This kicks out
+     the irreducible as described in (2b).
+     But now, during canonicalization, we see the cast
+     and remove it, in canEqCast. By the time we get into canEqTyVar, the equality
+     is heterogeneous again, and the process repeats.
+
+     To avoid this, we don't strip casts off a type if the other type
+     in the equality is a tyvar. And this is an improvement regardless:
+     because tyvars can, generally, unify with casted types, there's no
+     reason to go through the work of stripping off the cast when the
+     cast appears opposite a tyvar. This is implemented in the cast case
+     of can_eq_nc'.
+
+ (4) Reporting an error for a constraint that is blocked only because
+     of wrinkle (2) is hard: what would we say to users? And we don't
+     really need to report, because if a constraint is blocked, then
+     there is unsolved wanted blocking it; that unsolved wanted will
+     be reported. We thus push such errors to the bottom of the queue
+     in the error-reporting code; they should never be printed.
+
+     (4a) It would seem possible to do this filtering just based on the
+          presence of a blocking coercion hole. However, this is no good,
+          as it suppresses e.g. no-instance-found errors. We thus record
+          a CtIrredStatus in CIrredCan and filter based on this status.
+          This happened in T14584. An alternative approach is to expressly
+          look for *equalities* with blocking coercion holes, but actually
+          recording the blockage in a status field seems nicer.
+
+     (4b) The error message might be printed with -fdefer-type-errors,
+          so it still must exist. This is the only reason why there is
+          a message at all. Otherwise, we could simply do nothing.
+
+Historical note:
+
+We used to do this via emitting a Derived kind equality and then parking
+the heterogeneous equality as irreducible. But this new approach is much
+more direct. And it doesn't produce duplicate Deriveds (as the old one did).
 
 Note [Type synonyms and canonicalization]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -2376,7 +2369,6 @@ rewriteEqEvidence :: CtEvidence         -- Old evidence :: olhs ~ orhs (not swap
                                         --              or orhs ~ olhs (swapped)
                   -> SwapFlag
                   -> TcType -> TcType   -- New predicate  nlhs ~ nrhs
-                                        -- Should be zonked, because we use tcTypeKind on nlhs/nrhs
                   -> TcCoercion         -- lhs_co, of type :: nlhs ~ olhs
                   -> TcCoercion         -- rhs_co, of type :: nrhs ~ orhs
                   -> TcS CtEvidence     -- Of type nlhs ~ nrhs
@@ -2411,16 +2403,21 @@ rewriteEqEvidence old_ev swapped nlhs nrhs lhs_co rhs_co
        ; newGivenEvVar loc' (new_pred, new_tm) }
 
   | CtWanted { ctev_dest = dest, ctev_nosh = si } <- old_ev
-  = do { (new_ev, hole_co) <- newWantedEq_SI si loc' (ctEvRole old_ev) nlhs nrhs
-               -- The "_SI" variant ensures that we make a new Wanted
-               -- with the same shadow-info as the existing one (#16735)
-       ; let co = maybeSym swapped $
-                  mkSymCo lhs_co
-                  `mkTransCo` hole_co
-                  `mkTransCo` rhs_co
-       ; setWantedEq dest co
-       ; traceTcS "rewriteEqEvidence" (vcat [ppr old_ev, ppr nlhs, ppr nrhs, ppr co])
-       ; return new_ev }
+  = case dest of
+      HoleDest hole ->
+        do { (new_ev, hole_co) <- newWantedEq_SI (ch_blocker hole) si loc'
+                                                 (ctEvRole old_ev) nlhs nrhs
+                   -- The "_SI" variant ensures that we make a new Wanted
+                   -- with the same shadow-info as the existing one (#16735)
+           ; let co = maybeSym swapped $
+                      mkSymCo lhs_co
+                      `mkTransCo` hole_co
+                      `mkTransCo` rhs_co
+           ; setWantedEq dest co
+           ; traceTcS "rewriteEqEvidence" (vcat [ppr old_ev, ppr nlhs, ppr nrhs, ppr co])
+           ; return new_ev }
+
+      _ -> panic "rewriteEqEvidence"
 
 #if __GLASGOW_HASKELL__ <= 810
   | otherwise
diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs
index ea859bf3a8..e889940893 100644
--- a/compiler/typecheck/TcErrors.hs
+++ b/compiler/typecheck/TcErrors.hs
@@ -28,6 +28,7 @@ import TcType
 import TcOrigin
 import GHC.Rename.Unbound ( unknownNameSuggestions )
 import GHC.Core.Type
+import GHC.Core.Coercion
 import GHC.Core.TyCo.Rep
 import GHC.Core.TyCo.Ppr  ( pprTyVars, pprWithExplicitKindsWhen, pprSourceTyCon, pprWithTYPE )
 import GHC.Core.Unify     ( tcMatchTys )
@@ -61,7 +62,6 @@ import SrcLoc
 import GHC.Driver.Session
 import ListSetOps       ( equivClasses )
 import Maybes
-import Pair
 import qualified GHC.LanguageExtensions as LangExt
 import FV ( fvVarList, unionFV )
 
@@ -549,7 +549,7 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_impl = implics })
             -- See Note [Do not report derived but soluble errors]
 
      ; mapBagM_ (reportImplic ctxt2) implics }
-            -- NB ctxt1: don't suppress inner insolubles if there's only a
+            -- NB ctxt2: don't suppress inner insolubles if there's only a
             -- wanted insoluble here; but do suppress inner insolubles
             -- if there's a *given* insoluble here (= inaccessible code)
  where
@@ -562,29 +562,36 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_impl = implics })
     -- (see TcRnTypes.insolubleCt) is caught here, otherwise
     -- we might suppress its error message, and proceed on past
     -- type checking to get a Lint error later
-    report1 = [ ("Out of scope", is_out_of_scope,    True,  mkHoleReporter tidy_cts)
-              , ("Holes",        is_hole,            False, mkHoleReporter tidy_cts)
-              , ("custom_error", is_user_type_error, True,  mkUserTypeErrorReporter)
+    report1 = [ ("Out of scope", unblocked is_out_of_scope,    True,  mkHoleReporter tidy_cts)
+              , ("Holes",        unblocked is_hole,            False, mkHoleReporter tidy_cts)
+              , ("custom_error", unblocked is_user_type_error, True,  mkUserTypeErrorReporter)
 
               , given_eq_spec
-              , ("insoluble2",   utterly_wrong,  True, mkGroupReporter mkEqErr)
-              , ("skolem eq1",   very_wrong,     True, mkSkolReporter)
-              , ("skolem eq2",   skolem_eq,      True, mkSkolReporter)
-              , ("non-tv eq",    non_tv_eq,      True, mkSkolReporter)
+              , ("insoluble2",   unblocked utterly_wrong,  True, mkGroupReporter mkEqErr)
+              , ("skolem eq1",   unblocked very_wrong,     True, mkSkolReporter)
+              , ("skolem eq2",   unblocked skolem_eq,      True, mkSkolReporter)
+              , ("non-tv eq",    unblocked non_tv_eq,      True, mkSkolReporter)
 
                   -- The only remaining equalities are alpha ~ ty,
                   -- where alpha is untouchable; and representational equalities
                   -- Prefer homogeneous equalities over hetero, because the
                   -- former might be holding up the latter.
                   -- See Note [Equalities with incompatible kinds] in TcCanonical
-              , ("Homo eqs",      is_homo_equality, True,  mkGroupReporter mkEqErr)
-              , ("Other eqs",     is_equality,      False, mkGroupReporter mkEqErr) ]
+              , ("Homo eqs",      unblocked is_homo_equality, True,  mkGroupReporter mkEqErr)
+              , ("Other eqs",     unblocked is_equality,      True,  mkGroupReporter mkEqErr)
+              , ("Blocked eqs",   is_equality,           False, mkSuppressReporter mkBlockedEqErr)]
 
     -- report2: we suppress these if there are insolubles elsewhere in the tree
     report2 = [ ("Implicit params", is_ip,           False, mkGroupReporter mkIPErr)
               , ("Irreds",          is_irred,        False, mkGroupReporter mkIrredErr)
               , ("Dicts",           is_dict,         False, mkGroupReporter mkDictErr) ]
 
+    -- also checks to make sure the constraint isn't BlockedCIS
+    -- See TcCanonical Note [Equalities with incompatible kinds], (4)
+    unblocked :: (Ct -> Pred -> Bool) -> Ct -> Pred -> Bool
+    unblocked _ (CIrredCan { cc_status = BlockedCIS }) _ = False
+    unblocked checker ct pred = checker ct pred
+
     -- rigid_nom_eq, rigid_nom_tv_eq,
     is_hole, is_dict,
       is_equality, is_ip, is_irred :: Ct -> Pred -> Bool
@@ -796,6 +803,11 @@ mkGroupReporter :: (ReportErrCtxt -> [Ct] -> TcM ErrMsg)
 mkGroupReporter mk_err ctxt cts
   = mapM_ (reportGroup mk_err ctxt . toList) (equivClasses cmp_loc cts)
 
+-- Like mkGroupReporter, but doesn't actually print error messages
+mkSuppressReporter :: (ReportErrCtxt -> [Ct] -> TcM ErrMsg) -> Reporter
+mkSuppressReporter mk_err ctxt cts
+  = mapM_ (suppressGroup mk_err ctxt . toList) (equivClasses cmp_loc cts)
+
 eq_lhs_type :: Ct -> Ct -> Bool
 eq_lhs_type ct1 ct2
   = case (classifyPredType (ctPred ct1), classifyPredType (ctPred ct2)) of
@@ -806,8 +818,7 @@ eq_lhs_type ct1 ct2
 cmp_loc :: Ct -> Ct -> Ordering
 cmp_loc ct1 ct2 = ctLocSpan (ctLoc ct1) `compare` ctLocSpan (ctLoc ct2)
 
-reportGroup :: (ReportErrCtxt -> [Ct] -> TcM ErrMsg) -> ReportErrCtxt
-            -> [Ct] -> TcM ()
+reportGroup :: (ReportErrCtxt -> [Ct] -> TcM ErrMsg) -> Reporter
 reportGroup mk_err ctxt cts =
   ASSERT( not (null cts))
   do { err <- mk_err ctxt cts
@@ -824,6 +835,14 @@ reportGroup mk_err ctxt cts =
          -- but that's hard to know for sure, and if we don't
          -- abort, we need bindings for all (e.g. #12156)
 
+-- like reportGroup, but does not actually report messages. It still adds
+-- -fdefer-type-errors bindings, though.
+suppressGroup :: (ReportErrCtxt -> [Ct] -> TcM ErrMsg) -> Reporter
+suppressGroup mk_err ctxt cts
+ = do { err <- mk_err ctxt cts
+      ; traceTc "Suppressing errors for" (ppr cts)
+      ; mapM_ (addDeferredBinding ctxt err) cts }
+
 maybeReportHoleError :: ReportErrCtxt -> Ct -> ErrMsg -> TcM ()
 -- Unlike maybeReportError, these "hole" errors are
 -- /not/ suppressed by cec_suppress.  We want to see them!
@@ -1439,10 +1458,10 @@ mkEqErr_help :: DynFlags -> ReportErrCtxt -> Report
              -> Maybe SwapFlag   -- Nothing <=> not sure
              -> TcType -> TcType -> TcM ErrMsg
 mkEqErr_help dflags ctxt report ct oriented ty1 ty2
-  | Just (tv1, co1) <- tcGetCastedTyVar_maybe ty1
-  = mkTyVarEqErr dflags ctxt report ct oriented tv1 co1 ty2
-  | Just (tv2, co2) <- tcGetCastedTyVar_maybe ty2
-  = mkTyVarEqErr dflags ctxt report ct swapped  tv2 co2 ty1
+  | Just (tv1, _) <- tcGetCastedTyVar_maybe ty1
+  = mkTyVarEqErr dflags ctxt report ct oriented tv1 ty2
+  | Just (tv2, _) <- tcGetCastedTyVar_maybe ty2
+  = mkTyVarEqErr dflags ctxt report ct swapped  tv2 ty1
   | otherwise
   = reportEqErr ctxt report ct oriented ty1 ty2
   where
@@ -1459,13 +1478,13 @@ reportEqErr ctxt report ct oriented ty1 ty2
 
 mkTyVarEqErr, mkTyVarEqErr'
   :: DynFlags -> ReportErrCtxt -> Report -> Ct
-             -> Maybe SwapFlag -> TcTyVar -> TcCoercionN -> TcType -> TcM ErrMsg
+             -> Maybe SwapFlag -> TcTyVar -> TcType -> TcM ErrMsg
 -- tv1 and ty2 are already tidied
-mkTyVarEqErr dflags ctxt report ct oriented tv1 co1 ty2
-  = do { traceTc "mkTyVarEqErr" (ppr ct $$ ppr tv1 $$ ppr co1 $$ ppr ty2)
-       ; mkTyVarEqErr' dflags ctxt report ct oriented tv1 co1 ty2 }
+mkTyVarEqErr dflags ctxt report ct oriented tv1 ty2
+  = do { traceTc "mkTyVarEqErr" (ppr ct $$ ppr tv1 $$ ppr ty2)
+       ; mkTyVarEqErr' dflags ctxt report ct oriented tv1 ty2 }
 
-mkTyVarEqErr' dflags ctxt report ct oriented tv1 co1 ty2
+mkTyVarEqErr' dflags ctxt report ct oriented tv1 ty2
   | not insoluble_occurs_check   -- See Note [Occurs check wins]
   , isUserSkolem ctxt tv1   -- ty2 won't be a meta-tyvar, or else the thing would
                             -- be oriented the other way round;
@@ -1514,23 +1533,6 @@ mkTyVarEqErr' dflags ctxt report ct oriented tv1 co1 ty2
        -- to be helpful since this is just an unimplemented feature.
        ; mkErrorMsgFromCt ctxt ct $ report { report_important = [msg] } }
 
-   -- check for heterogeneous equality next; see Note [Equalities with incompatible kinds]
-   -- in TcCanonical
-  | not (k1 `tcEqType` k2)
-  = do { let main_msg = addArising (ctOrigin ct) $
-                        vcat [ hang (text "Kind mismatch: cannot unify" <+>
-                                     parens (ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1)) <+>
-                                     text "with:")
-                                  2 (sep [ppr ty2, dcolon, ppr k2])
-                             , text "Their kinds differ." ]
-             cast_msg
-               | isTcReflexiveCo co1 = empty
-               | otherwise           = text "NB:" <+> ppr tv1 <+>
-                                       text "was casted to have kind" <+>
-                                       quotes (ppr k1)
-
-       ; mkErrorMsgFromCt ctxt ct (mconcat [important main_msg, important cast_msg, report]) }
-
   -- If the immediately-enclosing implication has 'tv' a skolem, and
   -- we know by now its an InferSkol kind of skolem, then presumably
   -- it started life as a TyVarTv, else it'd have been unified, given
@@ -1596,9 +1598,6 @@ mkTyVarEqErr' dflags ctxt report ct oriented tv1 co1 ty2
         -- Consider an ambiguous top-level constraint (a ~ F a)
         -- Not an occurs check, because F is a type function.
   where
-    Pair _ k1 = tcCoercionKind co1
-    k2        = tcTypeKind ty2
-
     ty1 = mkTyVarTy tv1
     occ_check_expand       = occCheckForErrors dflags tv1 ty2
     insoluble_occurs_check = isInsolubleOccursCheck (ctEqRel ct) tv1 ty2
@@ -1681,6 +1680,24 @@ pp_givens givens
                 2 (sep [ text "bound by" <+> ppr skol_info
                        , text "at" <+> ppr (tcl_loc (ic_env implic)) ])
 
+-- These are for the "blocked" equalities, as described in TcCanonical
+-- Note [Equalities with incompatible kinds], wrinkle (2). There should
+-- always be another unsolved wanted around, which will ordinarily suppress
+-- this message. But this can still be printed out with -fdefer-type-errors
+-- (sigh), so we must produce a message.
+mkBlockedEqErr :: ReportErrCtxt -> [Ct] -> TcM ErrMsg
+mkBlockedEqErr ctxt (ct:_) = mkErrorMsgFromCt ctxt ct report
+  where
+    report = important msg
+    msg = vcat [ hang (text "Cannot use equality for substitution:")
+                   2 (ppr (ctPred ct))
+               , text "Doing so would be ill-kinded." ]
+          -- This is a terrible message. Perhaps worse, if the user
+          -- has -fprint-explicit-kinds on, they will see that the two
+          -- sides have the same kind, as there is an invisible cast.
+          -- I really don't know how to do better.
+mkBlockedEqErr _ [] = panic "mkBlockedEqErr no constraints"
+
 {-
 Note [Suppress redundant givens during error reporting]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1724,9 +1741,9 @@ extraTyVarEqInfo :: ReportErrCtxt -> TcTyVar -> TcType -> SDoc
 extraTyVarEqInfo ctxt tv1 ty2
   = extraTyVarInfo ctxt tv1 $$ ty_extra ty2
   where
-    ty_extra ty = case tcGetTyVar_maybe ty of
-                    Just tv -> extraTyVarInfo ctxt tv
-                    Nothing -> empty
+    ty_extra ty = case tcGetCastedTyVar_maybe ty of
+                    Just (tv, _) -> extraTyVarInfo ctxt tv
+                    Nothing      -> empty
 
 extraTyVarInfo :: ReportErrCtxt -> TcTyVar -> SDoc
 extraTyVarInfo ctxt tv
@@ -2734,10 +2751,7 @@ mkAmbigMsg prepend_msg ct
 
       | otherwise -- "The type variable 't0' is ambiguous"
       = text "The" <+> what <+> text "variable" <> plural tkvs
-        <+> pprQuotedList tkvs <+> is_or_are tkvs <+> text "ambiguous"
-
-    is_or_are [_] = text "is"
-    is_or_are _   = text "are"
+        <+> pprQuotedList tkvs <+> isOrAre tkvs <+> text "ambiguous"
 
 pprSkols :: ReportErrCtxt -> [TcTyVar] -> SDoc
 pprSkols ctxt tvs
diff --git a/compiler/typecheck/TcFlatten.hs b/compiler/typecheck/TcFlatten.hs
index f467df06ce..ecad0361d3 100644
--- a/compiler/typecheck/TcFlatten.hs
+++ b/compiler/typecheck/TcFlatten.hs
@@ -104,9 +104,6 @@ Note [The flattening story]
                        then xis1 /= xis2
   i.e. at most one CFunEqCan with a particular LHS
 
-* Function applications can occur in the RHS of a CTyEqCan.  No reason
-  not allow this, and it reduces the amount of flattening that must occur.
-
 * Flattening a type (F xis):
     - If we are flattening in a Wanted/Derived constraint
       then create new [W] x : F xis ~ fmv
@@ -1801,7 +1798,7 @@ unflattenWanteds tv_eqs funeqs
                         --     bump the unification count; it is "improvement"
                         -- Note [Unflattening can force the solver to iterate]
       = ASSERT2( tyVarKind tv `eqType` tcTypeKind rhs, ppr ct )
-           -- CTyEqCan invariant should ensure this is true
+           -- CTyEqCan invariant (TyEq:K) should ensure this is true
         do { is_filled <- isFilledMetaTyVar tv
            ; elim <- case is_filled of
                False -> do { traceTcS "unflatten_eq 2" (ppr ct)
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index 8d47f4b329..9c578949f8 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -195,18 +195,30 @@ tcHsSigWcType :: UserTypeCtxt -> LHsSigWcType GhcRn -> TcM Type
 tcHsSigWcType ctxt sig_ty = tcHsSigType ctxt (dropWildCards sig_ty)
 
 kcClassSigType :: SkolemInfo -> [Located Name] -> LHsSigType GhcRn -> TcM ()
-kcClassSigType skol_info names sig_ty
-  = discardResult $
-    tcClassSigType skol_info names sig_ty
-  -- tcClassSigType does a fair amount of extra work that we don't need,
-  -- such as ordering quantified variables. But we absolutely do need
-  -- to push the level when checking method types and solve local equalities,
-  -- and so it seems easier just to call tcClassSigType than selectively
-  -- extract the lines of code from tc_hs_sig_type that we really need.
-  -- If we don't push the level, we get #16517, where GHC accepts
-  --   class C a where
-  --     meth :: forall k. Proxy (a :: k) -> ()
-  -- Note that k is local to meth -- this is hogwash.
+-- This is a special form of tcClassSigType that is used during the
+-- kind-checking phase to infer the kind of class variables. Cf. tc_hs_sig_type.
+-- Importantly, this does *not* kind-generalize. Consider
+--   class SC f where
+--     meth :: forall a (x :: f a). Proxy x -> ()
+-- When instantiating Proxy with kappa, we must unify kappa := f a. But we're
+-- still working out the kind of f, and thus f a will have a coercion in it.
+-- Coercions block unification (Note [Equalities with incompatible kinds] in
+-- TcCanonical) and so we fail to unify. If we try to kind-generalize, we'll
+-- end up promoting kappa to the top level (because kind-generalization is
+-- normally done right before adding a binding to the context), and then we
+-- can't set kappa := f a, because a is local.
+kcClassSigType skol_info names (HsIB { hsib_ext  = sig_vars
+                                     , hsib_body = hs_ty })
+  = addSigCtxt (funsSigCtxt names) hs_ty $
+    do { (tc_lvl, (wanted, (spec_tkvs, _)))
+           <- pushTcLevelM                           $
+              solveLocalEqualitiesX "kcClassSigType" $
+              bindImplicitTKBndrs_Skol sig_vars      $
+              tc_lhs_type typeLevelMode hs_ty liftedTypeKind
+
+       ; emitResidualTvConstraint skol_info Nothing spec_tkvs
+                                  tc_lvl wanted }
+kcClassSigType _ _ (XHsImplicitBndrs nec) = noExtCon nec
 
 tcClassSigType :: SkolemInfo -> [Located Name] -> LHsSigType GhcRn -> TcM Type
 -- Does not do validity checking
diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs
index ab98e650ed..4401bb7142 100644
--- a/compiler/typecheck/TcInteract.hs
+++ b/compiler/typecheck/TcInteract.hs
@@ -18,8 +18,9 @@ import TcFlatten
 import TcUnify( canSolveByUnification )
 import VarSet
 import GHC.Core.Type as Type
-import GHC.Core.InstEnv        ( DFunInstType )
-import GHC.Core.Coercion.Axiom ( sfInteractTop, sfInteractInert )
+import GHC.Core.Coercion        ( BlockSubstFlag(..) )
+import GHC.Core.InstEnv         ( DFunInstType )
+import GHC.Core.Coercion.Axiom  ( sfInteractTop, sfInteractInert )
 
 import Var
 import TcType
@@ -687,8 +688,9 @@ once had done). This problem can be tickled by typecheck/should_compile/holes.
 -- mean that (ty1 ~ ty2)
 interactIrred :: InertCans -> Ct -> TcS (StopOrContinue Ct)
 
-interactIrred inerts workItem@(CIrredCan { cc_ev = ev_w, cc_insol = insoluble })
-  | insoluble  -- For insolubles, don't allow the constraint to be dropped
+interactIrred inerts workItem@(CIrredCan { cc_ev = ev_w, cc_status = status })
+  | InsolubleCIS <- status
+               -- For insolubles, don't allow the constraint to be dropped
                -- which can happen with solveOneFromTheOther, so that
                -- we get distinct error messages with -fdefer-type-errors
                -- See Note [Do not add duplicate derived insolubles]
@@ -1639,9 +1641,9 @@ solveByUnification :: CtEvidence -> TcTyVar -> Xi -> TcS ()
 --        workItem = the new Given constraint
 --
 -- NB: No need for an occurs check here, because solveByUnification always
---     arises from a CTyEqCan, a *canonical* constraint.  Its invariants
---     say that in (a ~ xi), the type variable a does not appear in xi.
---     See TcRnTypes.Ct invariants.
+--     arises from a CTyEqCan, a *canonical* constraint.  Its invariant (TyEq:OC)
+--     says that in (a ~ xi), the type variable a does not appear in xi.
+--     See Constraint.Ct invariants.
 --
 -- Post: tv is unified (by side effect) with xi;
 --       we often write tv := xi
@@ -2102,7 +2104,8 @@ shortCutReduction old_ev fsk ax_co fam_tc tc_args
                                        `mkTcTransCo` ctEvCoercion old_ev) )
 
            Wanted {} ->
-             do { (new_ev, new_co) <- newWantedEq deeper_loc Nominal
+             -- See TcCanonical Note [Equalities with incompatible kinds] about NoBlockSubst
+             do { (new_ev, new_co) <- newWantedEq_SI NoBlockSubst WDeriv deeper_loc Nominal
                                         (mkTyConApp fam_tc tc_args) (mkTyVarTy fsk)
                 ; setWantedEq (ctev_dest old_ev) $ ax_co `mkTcTransCo` new_co
                 ; return new_ev }
diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs
index 702641a227..945f42c81d 100644
--- a/compiler/typecheck/TcMType.hs
+++ b/compiler/typecheck/TcMType.hs
@@ -184,7 +184,7 @@ newWanted :: CtOrigin -> Maybe TypeOrKind -> PredType -> TcM CtEvidence
 -- Deals with both equality and non-equality predicates
 newWanted orig t_or_k pty
   = do loc <- getCtLocM orig t_or_k
-       d <- if isEqPrimPred pty then HoleDest  <$> newCoercionHole pty
+       d <- if isEqPrimPred pty then HoleDest  <$> newCoercionHole YesBlockSubst pty
                                 else EvVarDest <$> newEvVar pty
        return $ CtWanted { ctev_dest = d
                          , ctev_pred = pty
@@ -211,8 +211,8 @@ newHoleCt hole ev ty = do
 
 cloneWanted :: Ct -> TcM Ct
 cloneWanted ct
-  | ev@(CtWanted { ctev_dest = HoleDest {}, ctev_pred = pty }) <- ctEvidence ct
-  = do { co_hole <- newCoercionHole pty
+  | ev@(CtWanted { ctev_dest = HoleDest old_hole, ctev_pred = pty }) <- ctEvidence ct
+  = do { co_hole <- newCoercionHole (ch_blocker old_hole) pty
        ; return (mkNonCanonical (ev { ctev_dest = HoleDest co_hole })) }
   | otherwise
   = return ct
@@ -262,7 +262,7 @@ emitDerivedEqs origin pairs
 -- | Emits a new equality constraint
 emitWantedEq :: CtOrigin -> TypeOrKind -> Role -> TcType -> TcType -> TcM Coercion
 emitWantedEq origin t_or_k role ty1 ty2
-  = do { hole <- newCoercionHole pty
+  = do { hole <- newCoercionHole YesBlockSubst pty
        ; loc <- getCtLocM origin (Just t_or_k)
        ; emitSimple $ mkNonCanonical $
          CtWanted { ctev_pred = pty, ctev_dest = HoleDest hole
@@ -323,12 +323,16 @@ newImplication
 ************************************************************************
 -}
 
-newCoercionHole :: TcPredType -> TcM CoercionHole
-newCoercionHole pred_ty
+newCoercionHole :: BlockSubstFlag  -- should the presence of this hole block substitution?
+                                   -- See sub-wrinkle in TcCanonical
+                                   -- Note [Equalities with incompatible kinds]
+                -> TcPredType -> TcM CoercionHole
+newCoercionHole blocker pred_ty
   = do { co_var <- newEvVar pred_ty
-       ; traceTc "New coercion hole:" (ppr co_var)
+       ; traceTc "New coercion hole:" (ppr co_var <+> ppr blocker)
        ; ref <- newMutVar Nothing
-       ; return $ CoercionHole { ch_co_var = co_var, ch_ref = ref } }
+       ; return $ CoercionHole { ch_co_var = co_var, ch_blocker = blocker
+                               , ch_ref = ref } }
 
 -- | Put a value in a coercion hole
 fillCoercionHole :: CoercionHole -> Coercion -> TcM ()
@@ -2020,9 +2024,8 @@ zonkSimples cts = do { cts' <- mapBagM zonkCt cts
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 zonkCt tries to maintain the canonical form of a Ct.  For example,
   - a CDictCan should stay a CDictCan;
-  - a CTyEqCan should stay a CTyEqCan (if the LHS stays as a variable.).
   - a CHoleCan should stay a CHoleCan
-  - a CIrredCan should stay a CIrredCan with its cc_insol flag intact
+  - a CIrredCan should stay a CIrredCan with its cc_status flag intact
 
 Why?, for example:
 - For CDictCan, the @TcSimplify.expandSuperClasses@ step, which runs after the
@@ -2035,6 +2038,11 @@ Why?, for example:
 
 - For CIrredCan we want to see if a constraint is insoluble with insolubleWC
 
+On the other hand, we change CTyEqCan to CNonCanonical, because of all of
+CTyEqCan's invariants, which can break during zonking. Besides, the constraint
+will be canonicalised again, so there is little benefit in keeping the
+CTyEqCan structure.
+
 NB: we do not expect to see any CFunEqCans, because zonkCt is only
 called on unflattened constraints.
 
@@ -2045,6 +2053,7 @@ creates e.g. a CDictCan where the cc_tyars are /not/ function free.
 -}
 
 zonkCt :: Ct -> TcM Ct
+-- See Note [zonkCt behaviour]
 zonkCt ct@(CHoleCan { cc_ev = ev })
   = do { ev' <- zonkCtEvidence ev
        ; return $ ct { cc_ev = ev' } }
@@ -2056,12 +2065,8 @@ zonkCt ct@(CDictCan { cc_ev = ev, cc_tyargs = args })
 
 zonkCt (CTyEqCan { cc_ev = ev })
   = mkNonCanonical <$> zonkCtEvidence ev
-  -- CTyEqCan has some delicate invariants that may be violated by
-  -- zonking (documented with the Ct type) , so we don't want to create
-  -- a CTyEqCan here. Besides, this will be canonicalized again anyway,
-  -- so there is very little benefit in keeping the CTyEqCan constructor.
 
-zonkCt ct@(CIrredCan { cc_ev = ev }) -- Preserve the cc_insol flag
+zonkCt ct@(CIrredCan { cc_ev = ev }) -- Preserve the cc_status flag
   = do { ev' <- zonkCtEvidence ev
        ; return (ct { cc_ev = ev' }) }
 
@@ -2264,12 +2269,8 @@ zonkTidyOrigin env orig = return (env, orig)
 ----------------
 tidyCt :: TidyEnv -> Ct -> Ct
 -- Used only in error reporting
--- Also converts it to non-canonical
 tidyCt env ct
-  = case ct of
-     CHoleCan { cc_ev = ev }
-       -> ct { cc_ev = tidy_ev env ev }
-     _ -> mkNonCanonical (tidy_ev env (ctEvidence ct))
+  = ct { cc_ev = tidy_ev env (ctEvidence ct) }
   where
     tidy_ev :: TidyEnv -> CtEvidence -> CtEvidence
      -- NB: we do not tidy the ctev_evar field because we don't
diff --git a/compiler/typecheck/TcOrigin.hs b/compiler/typecheck/TcOrigin.hs
index 37b4d9a8d9..9dc137f7d9 100644
--- a/compiler/typecheck/TcOrigin.hs
+++ b/compiler/typecheck/TcOrigin.hs
@@ -363,7 +363,7 @@ data CtOrigin
                        -- visible.) Only used for prioritizing error messages.
                  }
 
-  | KindEqOrigin  -- See Note [Equalities with incompatible kinds] in TcCanonical.
+  | KindEqOrigin
       TcType (Maybe TcType)     -- A kind equality arising from unifying these two types
       CtOrigin                  -- originally arising from this
       (Maybe TypeOrKind)        -- the level of the eq this arises from
diff --git a/compiler/typecheck/TcPluginM.hs b/compiler/typecheck/TcPluginM.hs
index 36d35e049a..c85f72c157 100644
--- a/compiler/typecheck/TcPluginM.hs
+++ b/compiler/typecheck/TcPluginM.hs
@@ -79,6 +79,7 @@ import GHC.Core.Class
 import GHC.Driver.Types
 import Outputable
 import GHC.Core.Type
+import GHC.Core.Coercion   ( BlockSubstFlag(..) )
 import Id
 import GHC.Core.InstEnv
 import FastString
@@ -179,7 +180,7 @@ newEvVar = unsafeTcPluginTcM . TcM.newEvVar
 
 -- | Create a fresh coercion hole.
 newCoercionHole :: PredType -> TcPluginM CoercionHole
-newCoercionHole = unsafeTcPluginTcM . TcM.newCoercionHole
+newCoercionHole = unsafeTcPluginTcM . TcM.newCoercionHole YesBlockSubst
 
 -- | Bind an evidence variable.  This must not be invoked from
 -- 'tcPluginInit' or 'tcPluginStop', or it will panic.
diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs
index 3fd956f87a..fe74720796 100644
--- a/compiler/typecheck/TcSMonad.hs
+++ b/compiler/typecheck/TcSMonad.hs
@@ -300,8 +300,8 @@ workListWantedCount (WL { wl_eqs = eqs, wl_rest = rest })
   = count isWantedCt eqs + count is_wanted rest
   where
     is_wanted ct
-     | CIrredCan { cc_ev = ev, cc_insol = insol } <- ct
-     = not insol && isWanted ev
+     | CIrredCan { cc_status = InsolubleCIS } <- ct
+     = False
      | otherwise
      = isWantedCt ct
 
@@ -767,6 +767,7 @@ The InertCans represents a collection of constraints with the following properti
     eg a wanted cannot rewrite a given)
 
   * CTyEqCan equalities: see Note [inert_eqs: the inert equalities]
+    Also see documentation in Constraint.Ct for a list of invariants
 
 Note [EqualCtList invariants]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -919,8 +920,8 @@ The idea is that
   with S(fw,_).
 
 * T3 is guaranteed by a simple occurs-check on the work item.
-  This is done during canonicalisation, in canEqTyVar;
-  (invariant: a CTyEqCan never has an occurs check).
+  This is done during canonicalisation, in canEqTyVar; invariant
+  (TyEq:OC) of CTyEqCan.
 
 * (K1-3) are the "kick-out" criteria.  (As stated, they are really the
   "keep" criteria.) If the current inert S contains a triple that does
@@ -1639,11 +1640,13 @@ add_item ics item@(CTyEqCan { cc_tyvar = tv, cc_ev = ev })
         , inert_count = bumpUnsolvedCount ev (inert_count ics) }
 
 add_item ics@(IC { inert_irreds = irreds, inert_count = count })
-         item@(CIrredCan { cc_ev = ev, cc_insol = insoluble })
+         item@(CIrredCan { cc_ev = ev, cc_status = status })
   = ics { inert_irreds = irreds `Bag.snocBag` item
-        , inert_count  = if insoluble
-                         then count  -- inert_count does not include insolubles
-                         else bumpUnsolvedCount ev count }
+        , inert_count  = case status of
+                           InsolubleCIS -> count
+                           _            -> bumpUnsolvedCount ev count }
+                              -- inert_count does not include insolubles
+
 
 add_item ics item@(CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys })
   = ics { inert_dicts = addDict (inert_dicts ics) cls tys item
@@ -1821,6 +1824,42 @@ kickOutAfterUnification new_tv
        ; setInertCans ics2
        ; return n_kicked }
 
+-- See Wrinkle (2b) in Note [Equalities with incompatible kinds] in TcCanonical
+kickOutAfterFillingCoercionHole :: CoercionHole -> TcS ()
+kickOutAfterFillingCoercionHole hole
+  = do { ics <- getInertCans
+       ; let (kicked_out, ics') = kick_out ics
+             n_kicked           = workListSize kicked_out
+
+       ; unless (n_kicked == 0) $
+         do { updWorkListTcS (appendWorkList kicked_out)
+            ; csTraceTcS $
+              hang (text "Kick out, hole =" <+> ppr hole)
+                 2 (vcat [ text "n-kicked =" <+> int n_kicked
+                         , text "kicked_out =" <+> ppr kicked_out
+                         , text "Residual inerts =" <+> ppr ics' ]) }
+
+       ; setInertCans ics' }
+  where
+    kick_out :: InertCans -> (WorkList, InertCans)
+    kick_out ics@(IC { inert_irreds = irreds })
+      = let (to_kick, to_keep) = partitionBag kick_ct irreds
+
+            kicked_out = extendWorkListCts (bagToList to_kick) emptyWorkList
+            ics'       = ics { inert_irreds = to_keep }
+        in
+        (kicked_out, ics')
+
+    kick_ct :: Ct -> Bool
+    -- This is not particularly efficient. Ways to do better:
+    --  1) Have a custom function that looks for a coercion hole and returns a Bool
+    --  2) Keep co-hole-blocked constraints in a separate part of the inert set,
+    --     keyed by their co-hole. (Is it possible for more than one co-hole to be
+    --     in a constraint? I doubt it.)
+    kick_ct (CIrredCan { cc_ev = ev, cc_status = BlockedCIS })
+      = coHoleCoVar hole `elemVarSet` tyCoVarsOfType (ctEvPred ev)
+    kick_ct _other = False
+
 {- Note [kickOutRewritable]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
 See also Note [inert_eqs: the inert equalities].
@@ -3200,7 +3239,10 @@ newFlattenSkolem flav loc tc xis
       | otherwise  -- Generate a [WD] for both Wanted and Derived
                    -- See Note [No Derived CFunEqCans]
       = do { fmv <- wrapTcS (TcM.newFmvTyVar fam_ty)
-           ; (ev, hole_co) <- newWantedEq loc Nominal fam_ty (mkTyVarTy fmv)
+              -- See (2a) in TcCanonical
+              -- Note [Equalities with incompatible kinds]
+           ; (ev, hole_co) <- newWantedEq_SI NoBlockSubst WDeriv loc Nominal
+                                             fam_ty (mkTyVarTy fmv)
            ; return (ev, hole_co, fmv) }
 
 ----------------------------
@@ -3386,7 +3428,7 @@ useVars co_vars
 setWantedEq :: TcEvDest -> Coercion -> TcS ()
 setWantedEq (HoleDest hole) co
   = do { useVars (coVarsOfCo co)
-       ; wrapTcS $ TcM.fillCoercionHole hole co }
+       ; fillCoercionHole hole co }
 setWantedEq (EvVarDest ev) _ = pprPanic "setWantedEq" (ppr ev)
 
 -- | Good for both equalities and non-equalities
@@ -3394,12 +3436,12 @@ setWantedEvTerm :: TcEvDest -> EvTerm -> TcS ()
 setWantedEvTerm (HoleDest hole) tm
   | Just co <- evTermCoercion_maybe tm
   = do { useVars (coVarsOfCo co)
-       ; wrapTcS $ TcM.fillCoercionHole hole co }
+       ; fillCoercionHole hole co }
   | otherwise
   = -- See Note [Yukky eq_sel for a HoleDest]
     do { let co_var = coHoleCoVar hole
        ; setEvBind (mkWantedEvBind co_var tm)
-       ; wrapTcS $ TcM.fillCoercionHole hole (mkTcCoVarCo co_var) }
+       ; fillCoercionHole hole (mkTcCoVarCo co_var) }
 
 setWantedEvTerm (EvVarDest ev_id) tm
   = setEvBind (mkWantedEvBind ev_id tm)
@@ -3423,6 +3465,11 @@ We even re-use the CoHole's Id for this binding!
 Yuk!
 -}
 
+fillCoercionHole :: CoercionHole -> Coercion -> TcS ()
+fillCoercionHole hole co
+  = do { wrapTcS $ TcM.fillCoercionHole hole co
+       ; kickOutAfterFillingCoercionHole hole }
+
 setEvBindIfWanted :: CtEvidence -> EvTerm -> TcS ()
 setEvBindIfWanted ev tm
   = case ev of
@@ -3468,13 +3515,13 @@ emitNewWantedEq loc role ty1 ty2
 -- | Make a new equality CtEvidence
 newWantedEq :: CtLoc -> Role -> TcType -> TcType
             -> TcS (CtEvidence, Coercion)
-newWantedEq = newWantedEq_SI WDeriv
+newWantedEq = newWantedEq_SI YesBlockSubst WDeriv
 
-newWantedEq_SI :: ShadowInfo -> CtLoc -> Role
+newWantedEq_SI :: BlockSubstFlag -> ShadowInfo -> CtLoc -> Role
                -> TcType -> TcType
                -> TcS (CtEvidence, Coercion)
-newWantedEq_SI si loc role ty1 ty2
-  = do { hole <- wrapTcS $ TcM.newCoercionHole pty
+newWantedEq_SI blocker si loc role ty1 ty2
+  = do { hole <- wrapTcS $ TcM.newCoercionHole blocker pty
        ; traceTcS "Emitting new coercion hole" (ppr hole <+> dcolon <+> ppr pty)
        ; return ( CtWanted { ctev_pred = pty, ctev_dest = HoleDest hole
                            , ctev_nosh = si
@@ -3520,7 +3567,7 @@ newWanted = newWanted_SI WDeriv
 newWanted_SI :: ShadowInfo -> CtLoc -> PredType -> TcS MaybeNew
 newWanted_SI si loc pty
   | Just (role, ty1, ty2) <- getEqPredTys_maybe pty
-  = Fresh . fst <$> newWantedEq_SI si loc role ty1 ty2
+  = Fresh . fst <$> newWantedEq_SI YesBlockSubst si loc role ty1 ty2
   | otherwise
   = newWantedEvVar_SI si loc pty
 
diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs
index ea95a0b4ad..868be78c68 100644
--- a/compiler/typecheck/TcSimplify.hs
+++ b/compiler/typecheck/TcSimplify.hs
@@ -2432,7 +2432,6 @@ floatEqualities skols given_ids ev_binds_var no_given_eqs
     is_float_eq_candidate ct
       | pred <- ctPred ct
       , EqPred NomEq ty1 ty2 <- classifyPredType pred
-      , tcTypeKind ty1 `tcEqType` tcTypeKind ty2
       = case (tcGetTyVar_maybe ty1, tcGetTyVar_maybe ty2) of
           (Just tv1, _) -> float_tv_eq_candidate tv1 ty2
           (_, Just tv2) -> float_tv_eq_candidate tv2 ty1
@@ -2479,19 +2478,6 @@ happen.  In particular, float out equalities that are:
      case, floating out won't help either, and it may affect grouping
      of error messages.
 
-* Homogeneous (both sides have the same kind). Why only homogeneous?
-  Because heterogeneous equalities have derived kind equalities.
-  See Note [Equalities with incompatible kinds] in TcCanonical.
-  If we float out a hetero equality, then it will spit out the same
-  derived kind equality again, which might create duplicate error
-  messages.
-
-  Instead, we do float out the kind equality (if it's worth floating
-  out, as above). If/when we solve it, we'll be able to rewrite the
-  original hetero equality to be homogeneous, and then perhaps make
-  progress / float it out. The duplicate error message was spotted in
-  typecheck/should_fail/T7368.
-
 * Nominal.  No point in floating (alpha ~R# ty), because we do not
   unify representational equalities even if alpha is touchable.
   See Note [Do not unify representational equalities] in TcInteract.
diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs
index cb3865122b..6914851144 100644
--- a/compiler/typecheck/TcUnify.hs
+++ b/compiler/typecheck/TcUnify.hs
@@ -1693,7 +1693,7 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2
   where
     go dflags cur_lvl
       | canSolveByUnification cur_lvl tv1 ty2
-      , Just ty2' <- metaTyVarUpdateOK dflags tv1 ty2
+      , MTVU_OK ty2' <- metaTyVarUpdateOK dflags tv1 ty2
       = do { co_k <- uType KindLevel kind_origin (tcTypeKind ty2') (tyVarKind tv1)
            ; traceTc "uUnfilledVar2 ok" $
              vcat [ ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1)
@@ -1762,7 +1762,7 @@ lhsPriority tv
 {- Note [TyVar/TyVar orientation]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Given (a ~ b), should we orient the CTyEqCan as (a~b) or (b~a)?
-This is a surprisingly tricky question!
+This is a surprisingly tricky question! This is invariant (TyEq:TV).
 
 The question is answered by swapOverTyVars, which is use
   - in the eager unifier, in TcUnify.uUnfilledVar1
@@ -2178,7 +2178,9 @@ with (forall k. k->*)
 
 data MetaTyVarUpdateResult a
   = MTVU_OK a
-  | MTVU_Bad     -- Forall, predicate, or type family
+  | MTVU_Bad          -- Forall, predicate, or type family
+  | MTVU_HoleBlocker  -- Blocking coercion hole
+        -- See Note [Equalities with incompatible kinds] in TcCanonical
   | MTVU_Occurs
     deriving (Functor)
 
@@ -2187,9 +2189,16 @@ instance Applicative MetaTyVarUpdateResult where
       (<*>) = ap
 
 instance Monad MetaTyVarUpdateResult where
-  MTVU_OK x    >>= k = k x
-  MTVU_Bad     >>= _ = MTVU_Bad
-  MTVU_Occurs  >>= _ = MTVU_Occurs
+  MTVU_OK x        >>= k = k x
+  MTVU_Bad         >>= _ = MTVU_Bad
+  MTVU_HoleBlocker >>= _ = MTVU_HoleBlocker
+  MTVU_Occurs      >>= _ = MTVU_Occurs
+
+instance Outputable a => Outputable (MetaTyVarUpdateResult a) where
+  ppr (MTVU_OK a)      = text "MTVU_OK" <+> ppr a
+  ppr MTVU_Bad         = text "MTVU_Bad"
+  ppr MTVU_HoleBlocker = text "MTVU_HoleBlocker"
+  ppr MTVU_Occurs      = text "MTVU_Occurs"
 
 occCheckForErrors :: DynFlags -> TcTyVar -> Type -> MetaTyVarUpdateResult ()
 -- Just for error-message generation; so we return MetaTyVarUpdateResult
@@ -2199,22 +2208,25 @@ occCheckForErrors :: DynFlags -> TcTyVar -> Type -> MetaTyVarUpdateResult ()
 --   b) there is a forall in the type (unless we have -XImpredicativeTypes)
 occCheckForErrors dflags tv ty
   = case preCheck dflags True tv ty of
-      MTVU_OK _   -> MTVU_OK ()
-      MTVU_Bad    -> MTVU_Bad
-      MTVU_Occurs -> case occCheckExpand [tv] ty of
-                       Nothing -> MTVU_Occurs
-                       Just _  -> MTVU_OK ()
+      MTVU_OK _        -> MTVU_OK ()
+      MTVU_Bad         -> MTVU_Bad
+      MTVU_HoleBlocker -> MTVU_HoleBlocker
+      MTVU_Occurs      -> case occCheckExpand [tv] ty of
+                            Nothing -> MTVU_Occurs
+                            Just _  -> MTVU_OK ()
 
 ----------------
 metaTyVarUpdateOK :: DynFlags
                   -> TcTyVar             -- tv :: k1
                   -> TcType              -- ty :: k2
-                  -> Maybe TcType        -- possibly-expanded ty
+                  -> MetaTyVarUpdateResult TcType        -- possibly-expanded ty
 -- (metaTyVarUpdateOK tv ty)
 -- We are about to update the meta-tyvar tv with ty
 -- Check (a) that tv doesn't occur in ty (occurs check)
 --       (b) that ty does not have any foralls
 --           (in the impredicative case), or type functions
+--       (c) that ty does not have any blocking coercion holes
+--           See Note [Equalities with incompatible kinds] in TcCanonical
 --
 -- We have two possible outcomes:
 -- (1) Return the type to update the type variable with,
@@ -2237,20 +2249,24 @@ metaTyVarUpdateOK dflags tv ty
   = case preCheck dflags False tv ty of
          -- False <=> type families not ok
          -- See Note [Prevent unification with type families]
-      MTVU_OK _   -> Just ty
-      MTVU_Bad    -> Nothing  -- forall, predicate, or type function
-      MTVU_Occurs -> occCheckExpand [tv] ty
+      MTVU_OK _        -> MTVU_OK ty
+      MTVU_Bad         -> MTVU_Bad          -- forall, predicate, type function
+      MTVU_HoleBlocker -> MTVU_HoleBlocker  -- coercion hole
+      MTVU_Occurs      -> case occCheckExpand [tv] ty of
+                            Just expanded_ty -> MTVU_OK expanded_ty
+                            Nothing          -> MTVU_Occurs
 
 preCheck :: DynFlags -> Bool -> TcTyVar -> TcType -> MetaTyVarUpdateResult ()
 -- A quick check for
 --   (a) a forall type (unless -XImpredicativeTypes)
 --   (b) a predicate type (unless -XImpredicativeTypes)
 --   (c) a type family
---   (d) an occurrence of the type variable (occurs check)
+--   (d) a blocking coercion hole
+--   (e) an occurrence of the type variable (occurs check)
 --
 -- For (a), (b), and (c) we check only the top level of the type, NOT
--- inside the kinds of variables it mentions.  But for (c) we do
--- look in the kinds of course.
+-- inside the kinds of variables it mentions.  For (d) we look deeply
+-- in coercions, and for (e) we do look in the kinds of course.
 
 preCheck dflags ty_fam_ok tv ty
   = fast_check ty
@@ -2292,10 +2308,13 @@ preCheck dflags ty_fam_ok tv ty
     fast_check_occ k | tv `elemVarSet` tyCoVarsOfType k = MTVU_Occurs
                      | otherwise                        = ok
 
-     -- For coercions, we are only doing an occurs check here;
      -- no bother about impredicativity in coercions, as they're
      -- inferred
-    fast_check_co co | tv `elemVarSet` tyCoVarsOfCo co = MTVU_Occurs
+    fast_check_co co | not (gopt Opt_DeferTypeErrors dflags)
+                     , badCoercionHoleCo co            = MTVU_HoleBlocker
+        -- Wrinkle (4b) in TcCanonical Note [Equalities with incompatible kinds]
+
+                     | tv `elemVarSet` tyCoVarsOfCo co = MTVU_Occurs
                      | otherwise                       = ok
 
     bad_tc :: TyCon -> Bool