Improve error messages around kind mismatches.

Previously, when canonicalizing (or unifying, in uType) a
heterogeneous equality, we emitted a kind equality and used the
resulting coercion to cast one side of the heterogeneous equality.

While sound, this led to terrible error messages. (See the bugs
listed below.) The problem is that using the coercion built from
the emitted kind equality is a bit like a wanted rewriting a wanted.
The solution is to keep heterogeneous equalities as irreducible.

See Note [Equalities with incompatible kinds] in TcCanonical.

This commit also removes a highly suspicious switch to FM_SubstOnly
when flattening in the kinds of a type variable. I have no idea
why this was there, other than as a holdover from pre-TypeInType.
I've not left a Note because there is simply no reason I can conceive
of that the FM_SubstOnly should be there.

One challenge with this patch is that the emitted derived equalities
might get emitted several times: when a heterogeneous equality is
in an implication and then gets floated out from the implication,
the Derived is present both in and out of the implication. This
causes a duplicate error message. (Test case:
typecheck/should_fail/T7368) Solution: track the provenance of
Derived constraints and refuse to float out a constraint that has
an insoluble Derived.

Lastly, this labels one test (dependent/should_fail/RAE_T32a)
as expect_broken, because the problem is really #12919. The
different handling of constraints in this patch exposes the error.

This fixes bugs #11198, #12373, #13530, and #13610.

test cases:
typecheck/should_fail/{T8262,T8603,tcail122,T12373,T13530,T13610}

40 files changed, 538 insertions, 317 deletions

diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index be51914a27..7c061bbff4 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -563,6 +563,22 @@ can_eq_nc' _flat rdr_env envs ev ReprEq ty1 ps_ty1 ty2 _
   | Just stuff2 <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty2
   = can_eq_newtype_nc ev IsSwapped  ty2 stuff2 ty1 ps_ty1
 
+-- Now, check for tyvars. This must happen before CastTy because we need
+-- to catch casted tyvars, as the flattener might produce these,
+-- due to the fact that flattened types have flattened kinds.
+-- See Note [Flattening].
+-- Note that there can be only one cast on the tyvar because this will
+-- run after the "get rid of casts" case of can_eq_nc' function on the
+-- not-yet-flattened types.
+-- NB: pattern match on True: we want only flat types sent to canEqTyVar.
+-- See also Note [No top-level newtypes on RHS of representational equalities]
+can_eq_nc' True _rdr_env _envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
+  | Just (tv1, co1) <- getCastedTyVar_maybe ty1
+  = canEqTyVar ev eq_rel NotSwapped tv1 co1 ps_ty1 ty2 ps_ty2
+can_eq_nc' True _rdr_env _envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
+  | Just (tv2, co2) <- getCastedTyVar_maybe ty2
+  = canEqTyVar ev eq_rel IsSwapped tv2 co2 ps_ty2 ty1 ps_ty1
+
 -- Then, get rid of casts
 can_eq_nc' flat _rdr_env _envs ev eq_rel (CastTy ty1 co1) _ ty2 ps_ty2
   = canEqCast flat ev eq_rel NotSwapped ty1 co1 ty2 ps_ty2
@@ -609,14 +625,6 @@ can_eq_nc' False rdr_env envs ev eq_rel _ ps_ty1 _ ps_ty2
          `andWhenContinue` \ new_ev ->
          can_eq_nc' True rdr_env envs new_ev eq_rel xi1 xi1 xi2 xi2 }
 
--- Type variable on LHS or RHS are last.
--- NB: pattern match on True: we want only flat types sent to canEqTyVar.
--- See also Note [No top-level newtypes on RHS of representational equalities]
-can_eq_nc' True _rdr_env _envs ev eq_rel (TyVarTy tv1) ps_ty1 ty2 ps_ty2
-  = canEqTyVar ev eq_rel NotSwapped tv1 ps_ty1 ty2 ps_ty2
-can_eq_nc' True _rdr_env _envs ev eq_rel ty1 ps_ty1 (TyVarTy tv2) ps_ty2
-  = canEqTyVar ev eq_rel IsSwapped tv2 ps_ty2 ty1 ps_ty1
-
 -- We've flattened and the types don't match. Give up.
 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)
@@ -1356,19 +1364,6 @@ isInsolubleOccursCheck does.
 
 See also #10715, which induced this addition.
 
-Note [No derived kind equalities]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-When we're working with a heterogeneous derived equality
-
-  [D] (t1 :: k1) ~ (t2 :: k2)
-
-we want to homogenise to establish the kind invariant on CTyEqCans.
-But we can't emit [D] k1 ~ k2 because we wouldn't then be able to
-use the evidence in the homogenised types. So we emit a wanted
-constraint, because we do really need the evidence here.
-
-Thus: no derived kind equalities.
-
 -}
 
 canCFunEqCan :: CtEvidence
@@ -1396,54 +1391,120 @@ canCFunEqCan ev fn tys fsk
 ---------------------
 canEqTyVar :: CtEvidence          -- ev :: lhs ~ rhs
            -> EqRel -> SwapFlag
-           -> TcTyVar -> TcType   -- lhs: already flat, not a cast
-           -> TcType -> TcType    -- rhs: already flat, not a cast
+           -> TcTyVar -> CoercionN  -- tv1 |> co1
+           -> TcType                -- lhs: pretty lhs, already flat
+           -> TcType -> TcType      -- rhs: already flat
            -> TcS (StopOrContinue Ct)
-canEqTyVar ev eq_rel swapped tv1 ps_ty1 (TyVarTy tv2) _
-  | tv1 == tv2
-  = canEqReflexive ev eq_rel ps_ty1
+canEqTyVar ev eq_rel swapped tv1 co1 ps_ty1 xi2 ps_xi2
+  | k1 `eqType` k2
+  = canEqTyVarHomo ev eq_rel swapped tv1 co1 ps_ty1 xi2 ps_xi2
+
+  -- See Note [Equalities with incompatible kinds]
+  | CtGiven { ctev_evar = evar } <- ev
+    -- unswapped: tm :: (lhs :: k1) ~ (rhs :: k2)
+    -- swapped  : tm :: (rhs :: k2) ~ (lhs :: k1)
+  = do { kind_ev_id <- newBoundEvVarId kind_pty
+                                       (EvCoercion $
+                                        if isSwapped swapped
+                                        then mkTcSymCo $ mkTcKindCo $ mkTcCoVarCo evar
+                                        else             mkTcKindCo $ mkTcCoVarCo evar)
+           -- kind_ev_id :: (k1 :: *) ~ (k2 :: *)   (whether swapped or not)
+       ; let kind_ev = CtGiven { ctev_pred = kind_pty
+                               , ctev_evar = kind_ev_id
+                               , ctev_loc  = kind_loc }
+             homo_co = mkSymCo $ mkCoVarCo kind_ev_id
+             rhs'    = mkCastTy xi2 homo_co
+             ps_rhs' = mkCastTy ps_xi2 homo_co
+       ; traceTcS "Hetero equality gives rise to given kind equality"
+           (ppr kind_ev_id <+> dcolon <+> ppr kind_pty)
+       ; emitWorkNC [kind_ev]
+       ; type_ev <- newGivenEvVar loc $
+                    if isSwapped swapped
+                    then ( mkTcEqPredLikeEv ev rhs' lhs
+                         , EvCoercion $
+                           mkTcCoherenceLeftCo (mkTcCoVarCo evar) homo_co )
+                    else ( mkTcEqPredLikeEv ev lhs rhs'
+                         , EvCoercion $
+                           mkTcCoherenceRightCo (mkTcCoVarCo evar) homo_co )
+          -- unswapped: type_ev :: (lhs :: k1) ~ ((rhs |> sym kind_ev_id) :: k1)
+          -- swapped  : type_ev :: ((rhs |> sym kind_ev_id) :: k1) ~ (lhs :: k1)
+       ; canEqTyVarHomo type_ev eq_rel swapped tv1 co1 ps_ty1 rhs' ps_rhs' }
+
+  -- See Note [Equalities with incompatible kinds]
+  | otherwise   -- Wanted and Derived
+                  -- NB: all kind equalities are Nominal
+  = do { emitNewDerivedEq kind_loc Nominal k1 k2
+             -- kind_ev :: (k1 :: *) ~ (k2 :: *)
+       ; traceTcS "Hetero equality gives rise to derived kind equality" $
+           ppr ev
+       ; continueWith (CIrredEvCan { cc_ev = ev }) }
+
+  where
+    lhs = mkTyVarTy tv1 `mkCastTy` co1
+
+    Pair _ k1 = coercionKind co1
+    k2        = typeKind xi2
 
-  | swapOverTyVars tv1 tv2
+    kind_pty = mkHeteroPrimEqPred liftedTypeKind liftedTypeKind k1 k2
+    kind_loc = mkKindLoc lhs xi2 loc
+
+    loc  = ctev_loc ev
+
+-- guaranteed that typeKind lhs == typeKind rhs
+canEqTyVarHomo :: CtEvidence
+               -> EqRel -> SwapFlag
+               -> TcTyVar -> CoercionN   -- lhs: tv1 |> co1
+               -> TcType                 -- pretty lhs
+               -> TcType -> TcType       -- rhs (might not be flat)
+               -> TcS (StopOrContinue Ct)
+canEqTyVarHomo ev eq_rel swapped tv1 co1 ps_ty1 ty2 _
+  | Just (tv2, _) <- tcGetCastedTyVar_maybe ty2
+  , tv1 == tv2
+  = canEqReflexive ev eq_rel (mkTyVarTy tv1 `mkCastTy` co1)
+    -- we don't need to check co2 because its type must match co1
+
+  | Just (tv2, co2) <- tcGetCastedTyVar_maybe ty2
+  , swapOverTyVars tv1 tv2
   = do { traceTcS "canEqTyVar" (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
        ; dflags <- getDynFlags
-       ; canEqTyVar2 dflags ev eq_rel (flipSwap swapped) tv2 ps_ty1 }
+       ; canEqTyVar2 dflags ev eq_rel (flipSwap swapped) tv2 co2 ps_ty1 }
 
-canEqTyVar ev eq_rel swapped tv1 _ _ ps_ty2
+canEqTyVarHomo ev eq_rel swapped tv1 co1 _ _ ps_ty2
   = do { dflags <- getDynFlags
-       ; canEqTyVar2 dflags ev eq_rel swapped tv1 ps_ty2 }
+       ; canEqTyVar2 dflags ev eq_rel swapped tv1 co1 ps_ty2 }
 
+-- The RHS here is either not a casted tyvar, or it's a tyvar but we want
+-- to rewrite the LHS to the RHS (as per swapOverTyVars)
 canEqTyVar2 :: DynFlags
             -> CtEvidence   -- lhs ~ rhs (or, if swapped, orhs ~ olhs)
             -> EqRel
             -> SwapFlag
-            -> TcTyVar      -- lhs, flat
-            -> TcType       -- rhs, flat
+            -> TcTyVar -> CoercionN     -- lhs = tv |> co, flat
+            -> TcType                   -- rhs
             -> TcS (StopOrContinue Ct)
 -- LHS is an inert type variable,
 -- and RHS is fully rewritten, but with type synonyms
 -- preserved as much as possible
-
-canEqTyVar2 dflags ev eq_rel swapped tv1 xi2
-  | Just xi2' <- metaTyVarUpdateOK dflags tv1 xi2  -- No occurs check
+canEqTyVar2 dflags ev eq_rel swapped tv1 co1 orhs
+  | Just nrhs' <- metaTyVarUpdateOK dflags tv1 nrhs  -- No occurs check
      -- Must do the occurs check even on tyvar/tyvar
      -- equalities, in case have  x ~ (y :: ..x...)
      -- Trac #12593
-  = rewriteEqEvidence ev swapped xi1 xi2' co1 co2
+  = rewriteEqEvidence ev swapped nlhs nrhs' rewrite_co1 rewrite_co2
     `andWhenContinue` \ new_ev ->
-    homogeniseRhsKind new_ev eq_rel xi1 xi2' $ \new_new_ev xi2'' ->
-    CTyEqCan { cc_ev = new_new_ev, cc_tyvar = tv1
-             , cc_rhs = xi2'', cc_eq_rel = eq_rel }
+    continueWith (CTyEqCan { cc_ev = new_ev, cc_tyvar = tv1
+                           , cc_rhs = nrhs', cc_eq_rel = eq_rel })
 
   | otherwise  -- For some reason (occurs check, or forall) we can't unify
                -- We must not use it for further rewriting!
-  = do { traceTcS "canEqTyVar2 can't unify" (ppr tv1 $$ ppr xi2)
-       ; rewriteEqEvidence ev swapped xi1 xi2 co1 co2
+  = do { traceTcS "canEqTyVar2 can't unify" (ppr tv1 $$ ppr nrhs)
+       ; rewriteEqEvidence ev swapped nlhs nrhs rewrite_co1 rewrite_co2
          `andWhenContinue` \ new_ev ->
-         if isInsolubleOccursCheck eq_rel tv1 xi2
+         if isInsolubleOccursCheck eq_rel tv1 nrhs
          then do { emitInsoluble (mkNonCanonical new_ev)
              -- If we have a ~ [a], it is not canonical, and in particular
              -- we don't want to rewrite existing inerts with it, otherwise
@@ -1457,13 +1518,18 @@ canEqTyVar2 dflags ev eq_rel swapped tv1 xi2
              -- But, the occurs-check certainly prevents the equality from being
              -- canonical, and we might loop if we were to use it in rewriting.
          else do { traceTcS "Possibly-soluble occurs check"
-                           (ppr xi1 $$ ppr xi2)
+                           (ppr nlhs $$ ppr nrhs)
                  ; continueWith (CIrredEvCan { cc_ev = new_ev }) } }
   where
     role = eqRelRole eq_rel
-    xi1  = mkTyVarTy tv1
-    co1  = mkTcReflCo role xi1
-    co2  = mkTcReflCo role xi2
+
+    nlhs = mkTyVarTy tv1
+    nrhs = orhs `mkCastTy` mkTcSymCo co1
+
+    -- rewrite_co1 :: tv1 ~ (tv1 |> co1)
+    -- rewrite_co2 :: (rhs |> sym co1) ~ rhs
+    rewrite_co1  = mkTcReflCo role nlhs `mkTcCoherenceRightCo` co1
+    rewrite_co2  = mkTcReflCo role orhs `mkTcCoherenceLeftCo`  mkTcSymCo co1
 
 -- | Solve a reflexive equality constraint
 canEqReflexive :: CtEvidence    -- ty ~ ty
@@ -1475,75 +1541,6 @@ canEqReflexive ev eq_rel ty
                                mkTcReflCo (eqRelRole eq_rel) ty)
        ; stopWith ev "Solved by reflexivity" }
 
--- See Note [Equalities with incompatible kinds]
-homogeniseRhsKind :: CtEvidence -- ^ the evidence to homogenise
-                  -> EqRel
-                  -> TcType              -- ^ original LHS
-                  -> Xi                  -- ^ original RHS
-                  -> (CtEvidence -> Xi -> Ct)
-                           -- ^ how to build the homogenised constraint;
-                           -- the 'Xi' is the new RHS
-                  -> TcS (StopOrContinue Ct)
-homogeniseRhsKind ev eq_rel lhs rhs build_ct
-  | k1 `tcEqType` k2
-  = continueWith (build_ct ev rhs)
-
-  | CtGiven { ctev_evar = evar } <- ev
-    -- tm :: (lhs :: k1) ~ (rhs :: k2)
-  = do { kind_ev_id <- newBoundEvVarId kind_pty
-                                       (EvCoercion $
-                                        mkTcKindCo $ mkTcCoVarCo evar)
-           -- kind_ev_id :: (k1 :: *) ~# (k2 :: *)
-       ; let kind_ev = CtGiven { ctev_pred = kind_pty
-                               , ctev_evar = kind_ev_id
-                               , ctev_loc  = kind_loc }
-             homo_co = mkSymCo $ mkCoVarCo kind_ev_id
-             rhs'    = mkCastTy rhs homo_co
-       ; traceTcS "Hetero equality gives rise to given kind equality"
-           (ppr kind_ev_id <+> dcolon <+> ppr kind_pty)
-       ; emitWorkNC [kind_ev]
-       ; type_ev <- newGivenEvVar loc
-                      ( mkTcEqPredLikeEv ev lhs rhs'
-                      , EvCoercion $
-                        mkTcCoherenceRightCo (mkTcCoVarCo evar) homo_co )
-          -- type_ev :: (lhs :: k1) ~ ((rhs |> sym kind_ev_id) :: k1)
-       ; continueWith (build_ct type_ev rhs') }
-
-  | otherwise   -- Wanted and Derived. See Note [No derived kind equalities]
-    -- evar :: (lhs :: k1) ~ (rhs :: k2)
-  = do { kind_co <- emitNewWantedEq kind_loc Nominal k1 k2
-             -- kind_ev :: (k1 :: *) ~ (k2 :: *)
-       ; traceTcS "Hetero equality gives rise to wanted kind equality" $
-           ppr (kind_co)
-       ; let homo_co   = mkSymCo kind_co
-           -- homo_co :: k2 ~ k1
-             rhs'      = mkCastTy rhs homo_co
-       ; case ev of
-           CtGiven {} -> panic "homogeniseRhsKind"
-           CtDerived {} -> continueWith (build_ct (ev { ctev_pred = homo_pred })
-                                                  rhs')
-             where homo_pred = mkTcEqPredLikeEv ev lhs rhs'
-           CtWanted { ctev_dest = dest } -> do
-             { (type_ev, hole_co) <- newWantedEq loc role lhs rhs'
-                  -- type_ev :: (lhs :: k1) ~ (rhs |> sym kind_co :: k1)
-             ; setWantedEq dest
-                           (hole_co `mkTransCo`
-                            (mkReflCo role rhs
-                             `mkCoherenceLeftCo` homo_co))
-
-                -- dest := hole ; <rhs> |> homo_co :: (lhs :: k1) ~ (rhs :: k2)
-             ; continueWith (build_ct type_ev rhs') }}
-
-  where
-    k1 = typeKind lhs
-    k2 = typeKind rhs
-
-    kind_pty = mkHeteroPrimEqPred liftedTypeKind liftedTypeKind k1 k2
-    kind_loc = mkKindLoc lhs rhs loc
-
-    loc  = ctev_loc ev
-    role = eqRelRole eq_rel
-
 {-
 Note [Canonical orientation for tyvar/tyvar equality constraints]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1605,21 +1602,66 @@ the fsk.
 
 Note [Equalities with incompatible kinds]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-canEqLeaf is about to make a CTyEqCan or CFunEqCan; but both have the
-invariant that LHS and RHS satisfy the kind invariants for CTyEqCan,
-CFunEqCan.  What if we try to unify two things with incompatible
-kinds?
+What do we do when we have an equality
+
+  (tv :: k1) ~ (rhs :: k2)
+
+where k1 and k2 differ? This Note explores this treacherous area.
+
+First off, the question above is slightly the wrong question. Flattening
+a tyvar will flatten its kind (Note [Flattening] in TcFlatten); flattening
+the kind might introduce a cast. So we might have a casted tyvar on the
+left. We thus revise our test case to
+
+  (tv |> co :: k1) ~ (rhs :: k2)
+
+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
+
+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.
+
+The reason for this odd behavior is much the same as
+Note [Wanteds do not rewrite Wanteds] in TcRnTypes: note that the
+new `co` is a Wanted. 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. When the Derived is solved (by unification),
+the original wanted (`w`) will get kicked out.
+
+Note that, if we had [G] co1 :: k ~ Type available, then none of this code would
+trigger, because flattening would have rewritten k to Type. That is,
+`w` would look like [W] (alpha |> co1 :: Type) ~ (Int :: Type), and the tyvar
+case will trigger, correctly rewriting alpha to (Int |> sym co1).
 
-eg    a ~ b  where a::*, b::*->*
-or    a ~ b  where a::*, b::k, k is a kind variable
+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.
 
-The CTyEqCan compatKind invariant is important.  If we make a CTyEqCan
-for a~b, then we might well *substitute* 'b' for 'a', and that might make
-a well-kinded type ill-kinded; and that is bad (eg typeKind can crash, see
-Trac #7696).
+For Givens, this problem 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 canEqTyVar) and
+carry on with a homogeneous equality constraint.
 
-So instead for these ill-kinded equalities we homogenise the RHS of the
-equality, emitting new constraints as necessary.
+Separately, I (Richard E) spent some time pondering what to do in the case
+that we have [W] (tv |> co1 :: k1) ~ (tv |> co2 :: k2) where k1 and k2
+differ. Note that the tv is the same. (This case is handled as the first
+case in canEqTyVarHomo.) At one point, I thought we could solve this limited
+form of heterogeneous Wanted, but I then reconsidered and now treat this case
+just like any other heterogeneous Wanted.
 
 Note [Type synonyms and canonicalization]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs
index ed1eb82ce6..ea107a86da 100644
--- a/compiler/typecheck/TcErrors.hs
+++ b/compiler/typecheck/TcErrors.hs
@@ -53,6 +53,7 @@ import SrcLoc
 import DynFlags
 import ListSetOps       ( equivClasses )
 import Maybes
+import Pair
 import qualified GHC.LanguageExtensions as LangExt
 import FV ( fvVarList, unionFV )
 
@@ -478,19 +479,23 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_insol = insols, wc_impl
     -- (see TcRnTypes.trulyInsoluble) is caught here, otherwise
     -- we might suppress its error message, and proceed on past
     -- type checking to get a Lint error later
-    report1 = [ ("custom_error", is_user_type_error,
-                                                  True, mkUserTypeErrorReporter)
+    report1 = [ ("custom_error", 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)
-              , ("Out of scope", is_out_of_scope, True, mkHoleReporter)
-              , ("Holes",        is_hole,         False, mkHoleReporter)
+              , ("insoluble2 ty", utterly_wrong_ty, True, mkGroupReporter mkEqErr)
+              , ("insoluble2_ki", 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)
+              , ("Out of scope",  is_out_of_scope,  True, mkHoleReporter)
+              , ("Holes",         is_hole,          False, mkHoleReporter)
 
                   -- The only remaining equalities are alpha ~ ty,
                   -- where alpha is untouchable; and representational equalities
-              , ("Other eqs",    is_equality,     False, mkGroupReporter mkEqErr) ]
+                  -- 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) ]
 
     -- report2: we suppress these if there are insolubles elsewhere in the tree
     report2 = [ ("Implicit params", is_ip,           False, mkGroupReporter mkIPErr)
@@ -510,6 +515,12 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_insol = insols, wc_impl
     utterly_wrong _ (EqPred NomEq ty1 ty2) = isRigidTy ty1 && isRigidTy ty2
     utterly_wrong _ _                      = False
 
+     -- Like utterly_wrong, but suppress derived kind equalities
+    utterly_wrong_ty ct pred
+      = utterly_wrong ct pred && case ctOrigin ct of
+                                   KindEqOrigin {} -> False
+                                   _               -> True
+
     -- Things like (a ~N Int)
     very_wrong _ (EqPred NomEq ty1 ty2) = isSkolemTy tc_lvl ty1 && isRigidTy ty2
     very_wrong _ _                      = False
@@ -527,6 +538,9 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_insol = insols, wc_impl
 
     is_user_type_error ct _ = isUserTypeErrorCt ct
 
+    is_homo_equality _ (EqPred _ ty1 ty2) = typeKind ty1 `tcEqType` typeKind ty2
+    is_homo_equality _ _                  = False
+
     is_equality _ (EqPred {}) = True
     is_equality _ _           = False
 
@@ -1447,9 +1461,9 @@ the unsolved (t ~ Bool), t won't look like an untouchable meta-var
 any more.  So we don't assert that it is.
 -}
 
-mkEqErr :: ReportErrCtxt -> [Ct] -> TcM ErrMsg
 -- Don't have multiple equality errors from the same location
 -- E.g.   (Int,Bool) ~ (Bool,Int)   one error will do!
+mkEqErr :: ReportErrCtxt -> [Ct] -> TcM ErrMsg
 mkEqErr ctxt (ct:_) = mkEqErr1 ctxt ct
 mkEqErr _ [] = panic "mkEqErr"
 
@@ -1589,9 +1603,12 @@ 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 <- tcGetTyVar_maybe ty1 = mkTyVarEqErr dflags ctxt report ct oriented tv1 ty2
-  | Just tv2 <- tcGetTyVar_maybe ty2 = mkTyVarEqErr dflags ctxt report ct swapped  tv2 ty1
-  | otherwise                        = reportEqErr 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
+  | otherwise
+  = reportEqErr ctxt report ct oriented ty1 ty2
   where
     swapped = fmap flipSwap oriented
 
@@ -1606,13 +1623,13 @@ reportEqErr ctxt report ct oriented ty1 ty2
 
 mkTyVarEqErr, mkTyVarEqErr'
   :: DynFlags -> ReportErrCtxt -> Report -> Ct
-             -> Maybe SwapFlag -> TcTyVar -> TcType -> TcM ErrMsg
+             -> Maybe SwapFlag -> TcTyVar -> TcCoercionN -> TcType -> TcM ErrMsg
 -- tv1 and ty2 are already tidied
-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
+  = 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
+mkTyVarEqErr' dflags ctxt report ct oriented tv1 co1 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;
@@ -1661,6 +1678,23 @@ mkTyVarEqErr' dflags ctxt report ct oriented tv1 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 SigTv, else it'd have been unified, given
@@ -1706,7 +1740,7 @@ mkTyVarEqErr' dflags ctxt report ct oriented tv1 ty2
   , Implic { ic_env = env, ic_given = given
            , ic_tclvl = lvl, ic_info = skol_info } <- implic
   = ASSERT2( not (isTouchableMetaTyVar lvl tv1)
-           , ppr tv1 )  -- See Note [Error messages for untouchables]
+           , ppr tv1 $$ ppr lvl )  -- See Note [Error messages for untouchables]
     do { let msg = important $ misMatchMsg ct oriented ty1 ty2
              tclvl_extra = important $
                   nest 2 $
@@ -1725,6 +1759,9 @@ mkTyVarEqErr' dflags ctxt report ct oriented tv1 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        = typeKind ty2
+
     ty1 = mkTyVarTy tv1
     occ_check_expand       = occCheckForErrors dflags tv1 ty2
     insoluble_occurs_check = isInsolubleOccursCheck (ctEqRel ct) tv1 ty2
diff --git a/compiler/typecheck/TcEvidence.hs b/compiler/typecheck/TcEvidence.hs
index eb809ab013..4f305c6920 100644
--- a/compiler/typecheck/TcEvidence.hs
+++ b/compiler/typecheck/TcEvidence.hs
@@ -33,7 +33,7 @@ module TcEvidence (
   mkTcKindCo,
   tcCoercionKind, coVarsOfTcCo,
   mkTcCoVarCo,
-  isTcReflCo,
+  isTcReflCo, isTcReflexiveCo,
   tcCoercionRole,
   unwrapIP, wrapIP
   ) where
@@ -115,6 +115,10 @@ tcCoercionRole         :: TcCoercion -> Role
 coVarsOfTcCo           :: TcCoercion -> TcTyCoVarSet
 isTcReflCo             :: TcCoercion -> Bool
 
+-- | This version does a slow check, calculating the related types and seeing
+-- if they are equal.
+isTcReflexiveCo        :: TcCoercion -> Bool
+
 mkTcReflCo             = mkReflCo
 mkTcSymCo              = mkSymCo
 mkTcTransCo            = mkTransCo
@@ -143,7 +147,7 @@ tcCoercionKind         = coercionKind
 tcCoercionRole         = coercionRole
 coVarsOfTcCo           = coVarsOfCo
 isTcReflCo             = isReflCo
-
+isTcReflexiveCo        = isReflexiveCo
 
 {-
 %************************************************************************
diff --git a/compiler/typecheck/TcFlatten.hs b/compiler/typecheck/TcFlatten.hs
index 1bb4a7165b..69f8357a1d 100644
--- a/compiler/typecheck/TcFlatten.hs
+++ b/compiler/typecheck/TcFlatten.hs
@@ -584,7 +584,7 @@ setMode new_mode thing_inside
     else runFlatM thing_inside (env { fe_mode = new_mode })
 
 -- | Use when flattening kinds/kind coercions. See
--- Note [No derived kind equalities] in TcCanonical
+-- Note [No derived kind equalities]
 flattenKinds :: FlatM a -> FlatM a
 flattenKinds thing_inside
   = FlatM $ \env ->
@@ -717,6 +717,18 @@ soon throw out the phantoms when decomposing a TyConApp. (Or, the
 canonicaliser will emit an insoluble, in which case the unflattened version
 yields a better error message anyway.)
 
+Note [No derived kind equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We call flattenKinds in two places: in flatten_co (Note [Flattening coercions])
+and in flattenTyVar. The latter case is easier to understand; flattenKinds is
+used to flatten the kind of a flat (i.e. inert) tyvar. Flattening a kind
+naturally produces a coercion. This coercion is then used in the flattened type.
+However, danger lurks if the flattening flavour (that is, the fe_flavour of the
+FlattenEnv) is Derived: the coercion might be bottom. (This can happen when
+looks up a kindvar in the inert set only to find a Derived equality, with
+no coercion.) The solution is simple: ensure that the fe_flavour is not derived
+when flattening a kind. This is what flattenKinds does.
+
 -}
 
 {- *********************************************************************
@@ -1326,10 +1338,9 @@ flattenTyVar tv
 
            FTRNotFollowed   -- Done
              -> do { let orig_kind = tyVarKind tv
-                   ; (_new_kind, kind_co) <- setMode FM_SubstOnly $
-                                             flattenKinds $
+                   ; (_new_kind, kind_co) <- flattenKinds $
                                              flatten_one orig_kind
-                     ; let Pair _ zonked_kind = coercionKind kind_co
+                   ; let Pair _ zonked_kind = coercionKind kind_co
              -- NB: kind_co :: _new_kind ~ zonked_kind
              -- But zonked_kind is not necessarily the same as orig_kind
              -- because that may have filled-in metavars.
@@ -1339,13 +1350,13 @@ flattenTyVar tv
              -- See also Note [Flattening]
              -- An alternative would to use (zonkTcType orig_kind),
              -- but some simple measurements suggest that's a little slower
-                    ; let tv'    = setTyVarKind tv zonked_kind
-                          tv_ty' = mkTyVarTy tv'
-                          ty'    = tv_ty' `mkCastTy` mkSymCo kind_co
+                   ; let tv'    = setTyVarKind tv zonked_kind
+                         tv_ty' = mkTyVarTy tv'
+                         ty'    = tv_ty' `mkCastTy` mkSymCo kind_co
 
-                    ; role <- getRole
-                    ; return (ty', mkReflCo role tv_ty'
-                                   `mkCoherenceLeftCo` mkSymCo kind_co) } }
+                   ; role <- getRole
+                   ; return (ty', mkReflCo role tv_ty'
+                                  `mkCoherenceLeftCo` mkSymCo kind_co) } }
 
 flatten_tyvar1 :: TcTyVar -> FlatM FlattenTvResult
 -- "Flattening" a type variable means to apply the substitution to it
diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs
index 3e691c1100..2a04bf2a1c 100644
--- a/compiler/typecheck/TcRnTypes.hs
+++ b/compiler/typecheck/TcRnTypes.hs
@@ -106,7 +106,7 @@ module TcRnTypes(
         termEvidenceAllowed,
 
         CtEvidence(..), TcEvDest(..),
-        mkGivenLoc, mkKindLoc, toKindLoc,
+        mkKindLoc, toKindLoc, mkGivenLoc,
         isWanted, isGiven, isDerived, isGivenOrWDeriv,
         ctEvRole,
 
@@ -1617,7 +1617,7 @@ data Ct
        --   * tv not in tvs(rhs)   (occurs check)
        --   * If tv is a TauTv, then rhs has no foralls
        --       (this avoids substituting a forall for the tyvar in other types)
-       --   * typeKind ty `tcEqKind` typeKind tv
+       --   * typeKind ty `tcEqKind` typeKind tv; Note [Ct kind invariant]
        --   * rhs may have at most one top-level cast
        --   * rhs (perhaps under the one cast) is not necessarily function-free,
        --       but it has no top-level function.
@@ -1640,7 +1640,7 @@ data Ct
   | CFunEqCan {  -- F xis ~ fsk
        -- Invariants:
        --   * isTypeFamilyTyCon cc_fun
-       --   * typeKind (F xis) = tyVarKind fsk
+       --   * typeKind (F xis) = tyVarKind fsk; Note [Ct kind invariant]
        --   * always Nominal role
       cc_ev     :: CtEvidence,  -- See Note [Ct/evidence invariant]
       cc_fun    :: TyCon,       -- A type function
@@ -1717,6 +1717,14 @@ built (in TcCanonical).
 In contrast, the type of the evidence *term* (ctev_dest / ctev_evar) in
 the evidence may *not* be fully zonked; we are careful not to look at it
 during constraint solving. See Note [Evidence field of CtEvidence].
+
+Note [Ct kind invariant]
+~~~~~~~~~~~~~~~~~~~~~~~~
+CTyEqCan and CFunEqCan both require that the kind of the lhs matches the kind
+of the rhs. This is necessary because both constraints are used for substitutions
+during solving. If the kinds differed, then the substitution would take a well-kinded
+type to an ill-kinded one.
+
 -}
 
 mkNonCanonical :: CtEvidence -> Ct
@@ -2904,25 +2912,20 @@ The 'CtLoc' gives information about where a constraint came from.
 This is important for decent error message reporting because
 dictionaries don't appear in the original source code.
 type will evolve...
+
 -}
 
 data CtLoc = CtLoc { ctl_origin :: CtOrigin
                    , ctl_env    :: TcLclEnv
                    , ctl_t_or_k :: Maybe TypeOrKind  -- OK if we're not sure
                    , ctl_depth  :: !SubGoalDepth }
+
   -- The TcLclEnv includes particularly
   --    source location:  tcl_loc   :: RealSrcSpan
   --    context:          tcl_ctxt  :: [ErrCtxt]
   --    binder stack:     tcl_bndrs :: TcIdBinderStack
   --    level:            tcl_tclvl :: TcLevel
 
-mkGivenLoc :: TcLevel -> SkolemInfo -> TcLclEnv -> CtLoc
-mkGivenLoc tclvl skol_info env
-  = CtLoc { ctl_origin = GivenOrigin skol_info
-          , ctl_env    = env { tcl_tclvl = tclvl }
-          , ctl_t_or_k = Nothing    -- this only matters for error msgs
-          , ctl_depth  = initialSubGoalDepth }
-
 mkKindLoc :: TcType -> TcType   -- original *types* being compared
           -> CtLoc -> CtLoc
 mkKindLoc s1 s2 loc = setCtLocOrigin (toKindLoc loc)
@@ -2933,6 +2936,13 @@ mkKindLoc s1 s2 loc = setCtLocOrigin (toKindLoc loc)
 toKindLoc :: CtLoc -> CtLoc
 toKindLoc loc = loc { ctl_t_or_k = Just KindLevel }
 
+mkGivenLoc :: TcLevel -> SkolemInfo -> TcLclEnv -> CtLoc
+mkGivenLoc tclvl skol_info env
+  = CtLoc { ctl_origin = GivenOrigin skol_info
+          , ctl_env    = env { tcl_tclvl = tclvl }
+          , ctl_t_or_k = Nothing    -- this only matters for error msgs
+          , ctl_depth  = initialSubGoalDepth }
+
 ctLocEnv :: CtLoc -> TcLclEnv
 ctLocEnv = ctl_env
 
diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs
index 42c113610b..dca7f4d574 100644
--- a/compiler/typecheck/TcSimplify.hs
+++ b/compiler/typecheck/TcSimplify.hs
@@ -611,7 +611,7 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
        ; wanted_transformed_incl_derivs
             <- setTcLevel rhs_tclvl $
                runTcSWithEvBinds ev_binds_var $
-               do { let loc = mkGivenLoc rhs_tclvl UnkSkol tc_lcl_env
+               do { let loc         = mkGivenLoc rhs_tclvl UnkSkol tc_lcl_env
                         psig_givens = mkGivens loc psig_theta_vars
                   ; _ <- solveSimpleGivens psig_givens
                          -- See Note [Add signature contexts as givens]
@@ -1983,7 +1983,8 @@ floatEqualities skols no_given_eqs
        ; return ( float_eqs
                 , wanteds { wc_simple = remaining_simples } ) }
 
-usefulToFloat :: VarSet -> Ct -> Bool
+usefulToFloat :: VarSet        -- ^ the skolems in the implication
+              -> Ct -> Bool
 usefulToFloat skol_set ct   -- The constraint is un-flattened and de-canonicalised
   = is_meta_var_eq pred &&
     (tyCoVarsOfType pred `disjointVarSet` skol_set)
@@ -1995,6 +1996,7 @@ usefulToFloat skol_set ct   -- The constraint is un-flattened and de-canonicalis
       -- See Note [Which equalities to float]
     is_meta_var_eq pred
       | EqPred NomEq ty1 ty2 <- classifyPredType pred
+      , is_homogeneous ty1 ty2
       = case (tcGetTyVar_maybe ty1, tcGetTyVar_maybe ty2) of
           (Just tv1, _) -> float_tv_eq tv1 ty2
           (_, Just tv2) -> float_tv_eq tv2 ty1
@@ -2006,6 +2008,17 @@ usefulToFloat skol_set ct   -- The constraint is un-flattened and de-canonicalis
       =  isMetaTyVar tv1
       && (not (isSigTyVar tv1) || isTyVarTy ty2)
 
+    is_homogeneous ty1 ty2
+      = not has_heterogeneous_form ||  -- checking the shape is quicker
+                                       -- than looking at kinds
+        typeKind ty1 `tcEqType` typeKind ty2
+
+    has_heterogeneous_form = case ct of
+      CIrredEvCan {}   -> True
+      CNonCanonical {} -> True
+      _                -> False
+
+
 {- Note [Float equalities from under a skolem binding]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Which of the simple equalities can we float out?  Obviously, only
@@ -2035,7 +2048,7 @@ Which equalities should we float?  We want to float ones where there
 is a decent chance that floating outwards will allow unification to
 happen.  In particular:
 
-   Float out equalities of form (alpha ~ ty) or (ty ~ alpha), where
+   Float out homogeneous equalities of form (alpha ~ ty) or (ty ~ alpha), where
 
    * alpha is a meta-tyvar.
 
@@ -2043,6 +2056,15 @@ happen.  In particular:
      case, floating out won't help either, and it may affect grouping
      of error messages.
 
+Why homogeneous (i.e., the kinds of the types are the same)? 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.
+
 Note [Skolem escape]
 ~~~~~~~~~~~~~~~~~~~~
 You might worry about skolem escape with all this floating.
@@ -2177,10 +2199,8 @@ disambigGroup (default_ty:default_tys) group@(the_tv, wanteds)
     try_group
       | Just subst <- mb_subst
       = do { lcl_env <- TcS.getLclEnv
-           ; let loc = CtLoc { ctl_origin = GivenOrigin UnkSkol
-                             , ctl_env    = lcl_env
-                             , ctl_t_or_k = Nothing
-                             , ctl_depth  = initialSubGoalDepth }
+           ; tc_lvl <- TcS.getTcLevel
+           ; let loc = mkGivenLoc tc_lvl UnkSkol lcl_env
            ; wanted_evs <- mapM (newWantedEvVarNC loc . substTy subst . ctPred)
                                 wanteds
            ; fmap isEmptyWC $
diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index 7b8ff13753..c937a9f3fa 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -66,7 +66,7 @@ module TcType (
   tcRepSplitTyConApp_maybe, tcRepSplitTyConApp_maybe',
   tcTyConAppTyCon, tcTyConAppTyCon_maybe, tcTyConAppArgs,
   tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, tcRepSplitAppTy_maybe,
-  tcGetTyVar_maybe, tcGetTyVar, nextRole,
+  tcGetCastedTyVar_maybe, tcGetTyVar_maybe, tcGetTyVar, nextRole,
   tcSplitSigmaTy, tcSplitNestedSigmaTys, tcDeepSplitSigmaTy_maybe,
 
   ---------------------------------
@@ -1570,6 +1570,14 @@ tcSplitAppTys ty
                    Nothing         -> (ty,args)
 
 -----------------------
+-- | If the type is a tyvar, possibly under a cast, returns it, along
+-- with the coercion. Thus, the co is :: kind tv ~N kind type
+tcGetCastedTyVar_maybe :: Type -> Maybe (TyVar, CoercionN)
+tcGetCastedTyVar_maybe ty | Just ty' <- tcView ty = tcGetCastedTyVar_maybe ty'
+tcGetCastedTyVar_maybe (CastTy (TyVarTy tv) co) = Just (tv, co)
+tcGetCastedTyVar_maybe (TyVarTy tv)             = Just (tv, mkNomReflCo (tyVarKind tv))
+tcGetCastedTyVar_maybe _                        = Nothing
+
 tcGetTyVar_maybe :: Type -> Maybe TyVar
 tcGetTyVar_maybe ty | Just ty' <- tcView ty = tcGetTyVar_maybe ty'
 tcGetTyVar_maybe (TyVarTy tv)   = Just tv
diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs
index 1cbf5741b2..94296474b1 100644
--- a/compiler/typecheck/TcUnify.hs
+++ b/compiler/typecheck/TcUnify.hs
@@ -1529,11 +1529,16 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2
       | canSolveByUnification cur_lvl tv1 ty2
       , Just ty2' <- metaTyVarUpdateOK dflags tv1 ty2
       = do { co_k <- uType kind_origin KindLevel (typeKind ty2') (tyVarKind tv1)
-           ; co   <- updateMeta tv1 ty2' co_k
-           ; return (maybe_sym swapped co) }
+           ; if isTcReflCo co_k  -- only proceed if the kinds matched.
+
+             then do { writeMetaTyVar tv1 ty2'
+                     ; return (mkTcNomReflCo ty2') }
+             else defer } -- this cannot be solved now.
+                          -- See Note [Equalities with incompatible kinds]
+                          -- in TcCanonical
 
       | otherwise
-      = unSwap swapped (uType_defer origin t_or_k) ty1 ty2
+      = defer
                -- Occurs check or an untouchable: just defer
                -- NB: occurs check isn't necessarily fatal:
                --     eg tv1 occured in type family parameter
@@ -1541,10 +1546,7 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2
     ty1 = mkTyVarTy tv1
     kind_origin = KindEqOrigin ty1 (Just ty2) origin (Just t_or_k)
 
--- | apply sym iff swapped
-maybe_sym :: SwapFlag -> Coercion -> Coercion
-maybe_sym IsSwapped  = mkSymCo
-maybe_sym NotSwapped = id
+    defer = unSwap swapped (uType_defer origin t_or_k) ty1 ty2
 
 swapOverTyVars :: TcTyVar -> TcTyVar -> Bool
 swapOverTyVars tv1 tv2
@@ -1768,18 +1770,6 @@ lookupTcTyVar tyvar
   where
     details = tcTyVarDetails tyvar
 
--- | Fill in a meta-tyvar
-updateMeta :: TcTyVar            -- ^ tv to fill in, tv :: k1
-           -> TcType             -- ^ ty2 :: k2
-           -> Coercion           -- ^ kind_co :: k2 ~N k1
-           -> TcM Coercion       -- ^ :: tv ~N ty2 (= ty2 |> kind_co ~N ty2)
-updateMeta tv1 ty2 kind_co
-  = do { let ty2'     = ty2 `mkCastTy` kind_co
-             ty2_refl = mkNomReflCo ty2
-             co       = mkCoherenceLeftCo ty2_refl kind_co
-       ; writeMetaTyVar tv1 ty2'
-       ; return co }
-
 {-
 Note [Unifying untouchables]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index 0764d144b7..cea12abcde 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -615,8 +615,8 @@ getTyVar_maybe ty | Just ty' <- coreView ty = getTyVar_maybe ty'
                   | otherwise               = repGetTyVar_maybe ty
 
 -- | If the type is a tyvar, possibly under a cast, returns it, along
--- with the coercion. Thus, the co is :: kind tv ~R kind type
-getCastedTyVar_maybe :: Type -> Maybe (TyVar, Coercion)
+-- with the coercion. Thus, the co is :: kind tv ~N kind type
+getCastedTyVar_maybe :: Type -> Maybe (TyVar, CoercionN)
 getCastedTyVar_maybe ty | Just ty' <- coreView ty = getCastedTyVar_maybe ty'
 getCastedTyVar_maybe (CastTy (TyVarTy tv) co)     = Just (tv, co)
 getCastedTyVar_maybe (TyVarTy tv)
diff --git a/testsuite/tests/dependent/should_fail/T11471.hs b/testsuite/tests/dependent/should_fail/T11471.hs
index 19025db22b..ae09ae07bb 100644
--- a/testsuite/tests/dependent/should_fail/T11471.hs
+++ b/testsuite/tests/dependent/should_fail/T11471.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE MagicHash, PolyKinds, TypeFamilies #-}
+{-# LANGUAGE MagicHash, PolyKinds, TypeFamilies, AllowAmbiguousTypes #-}
 
 module T11471 where
 
diff --git a/testsuite/tests/dependent/should_fail/T11471.stderr b/testsuite/tests/dependent/should_fail/T11471.stderr
index 80c5fc606c..640ae6c754 100644
--- a/testsuite/tests/dependent/should_fail/T11471.stderr
+++ b/testsuite/tests/dependent/should_fail/T11471.stderr
@@ -1,19 +1,22 @@
 
 T11471.hs:15:10: error:
     • Couldn't match a lifted type with an unlifted type
-      Expected type: Proxy Int#
+      When matching types
+        a :: *
+        Int# :: TYPE 'IntRep
+      Expected type: Proxy a
         Actual type: Proxy Int#
-      Use -fprint-explicit-kinds to see the kind arguments
     • In the first argument of ‘f’, namely ‘(undefined :: Proxy Int#)’
       In the expression: f (undefined :: Proxy Int#) 3#
       In an equation for ‘bad’: bad = f (undefined :: Proxy Int#) 3#
+    • Relevant bindings include bad :: F a (bound at T11471.hs:15:1)
 
 T11471.hs:15:35: error:
     • Couldn't match a lifted type with an unlifted type
       When matching types
-        F Int# :: *
+        F a :: *
         Int# :: TYPE 'IntRep
     • In the second argument of ‘f’, namely ‘3#’
       In the expression: f (undefined :: Proxy Int#) 3#
       In an equation for ‘bad’: bad = f (undefined :: Proxy Int#) 3#
-    • Relevant bindings include bad :: F Int# (bound at T11471.hs:15:1)
+    • Relevant bindings include bad :: F a (bound at T11471.hs:15:1)
diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T
index c648f9ed1d..af3efc6716 100644
--- a/testsuite/tests/dependent/should_fail/all.T
+++ b/testsuite/tests/dependent/should_fail/all.T
@@ -1,5 +1,5 @@
 test('DepFail1', normal, compile_fail, [''])
-test('RAE_T32a', normal, compile_fail, [''])
+test('RAE_T32a', expect_broken(12919), compile_fail, [''])
 test('TypeSkolEscape', normal, compile_fail, [''])
 test('BadTelescope', normal, compile_fail, [''])
 test('BadTelescope2', normal, compile_fail, [''])
diff --git a/testsuite/tests/gadt/gadt7.stderr b/testsuite/tests/gadt/gadt7.stderr
index ea9033ac6c..bb179975fb 100644
--- a/testsuite/tests/gadt/gadt7.stderr
+++ b/testsuite/tests/gadt/gadt7.stderr
@@ -1,15 +1,15 @@
 
 gadt7.hs:16:38: error:
     • Couldn't match expected type ‘p1’ with actual type ‘p’
-        ‘p1’ is untouchable
+        ‘p’ is untouchable
           inside the constraints: a ~ Int
           bound by a pattern with constructor: K :: T Int,
                    in a case alternative
           at gadt7.hs:16:33
-      ‘p1’ is a rigid type variable bound by
-        the inferred type of i1b :: T a -> p -> p1 at gadt7.hs:16:1-44
       ‘p’ is a rigid type variable bound by
         the inferred type of i1b :: T a -> p -> p1 at gadt7.hs:16:1-44
+      ‘p1’ is a rigid type variable bound by
+        the inferred type of i1b :: T a -> p -> p1 at gadt7.hs:16:1-44
       Possible fix: add a type signature for ‘i1b’
     • In the expression: y1
       In a case alternative: K -> y1
diff --git a/testsuite/tests/ghci.debugger/scripts/break012.stdout b/testsuite/tests/ghci.debugger/scripts/break012.stdout
index 2e86b42713..5d478ae04e 100644
--- a/testsuite/tests/ghci.debugger/scripts/break012.stdout
+++ b/testsuite/tests/ghci.debugger/scripts/break012.stdout
@@ -1,14 +1,14 @@
 Stopped in Main.g, break012.hs:5:10-18
-_result :: (p, a1 -> a1, (), a -> a -> a) = _
-a :: p = _
-b :: a2 -> a2 = _
+_result :: (a1, a2 -> a2, (), a -> a -> a) = _
+a :: a1 = _
+b :: a3 -> a3 = _
 c :: () = _
 d :: a -> a -> a = _
-a :: p
-b :: a2 -> a2
+a :: a1
+b :: a3 -> a3
 c :: ()
 d :: a -> a -> a
-a = (_t1::p)
-b = (_t2::a2 -> a2)
+a = (_t1::a1)
+b = (_t2::a3 -> a3)
 c = (_t3::())
 d = (_t4::a -> a -> a)
diff --git a/testsuite/tests/indexed-types/should_fail/ExtraTcsUntch.stderr b/testsuite/tests/indexed-types/should_fail/ExtraTcsUntch.stderr
index 5bc6aca64c..f2ea8b2668 100644
--- a/testsuite/tests/indexed-types/should_fail/ExtraTcsUntch.stderr
+++ b/testsuite/tests/indexed-types/should_fail/ExtraTcsUntch.stderr
@@ -1,12 +1,12 @@
 
 ExtraTcsUntch.hs:23:18: error:
-    • Couldn't match expected type ‘F Int’ with actual type ‘[p]’
+    • Couldn't match expected type ‘F Int’ with actual type ‘[x]’
     • In the first argument of ‘h’, namely ‘[x]’
       In the expression: h [x]
       In an equation for ‘g1’: g1 _ = h [x]
     • Relevant bindings include
-        x :: p (bound at ExtraTcsUntch.hs:21:3)
-        f :: p -> ((), ((), ())) (bound at ExtraTcsUntch.hs:21:1)
+        x :: x (bound at ExtraTcsUntch.hs:21:3)
+        f :: x -> ((), ((), ())) (bound at ExtraTcsUntch.hs:21:1)
 
 ExtraTcsUntch.hs:25:38: error:
     • Couldn't match expected type ‘F Int’ with actual type ‘[[a0]]’
diff --git a/testsuite/tests/indexed-types/should_fail/T5934.stderr b/testsuite/tests/indexed-types/should_fail/T5934.stderr
index e303e54f74..21af0d868a 100644
--- a/testsuite/tests/indexed-types/should_fail/T5934.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T5934.stderr
@@ -5,16 +5,3 @@ T5934.hs:12:7: error:
         GHC doesn't yet support impredicative polymorphism
     • In the expression: 0
       In an equation for ‘run’: run = 0
-
-T5934.hs:12:7: error:
-    • Ambiguous type variable ‘a0’ arising from the literal ‘0’
-      prevents the constraint ‘(Num a0)’ from being solved.
-      Probable fix: use a type annotation to specify what ‘a0’ should be.
-      These potential instances exist:
-        instance Num Integer -- Defined in ‘GHC.Num’
-        instance Num Double -- Defined in ‘GHC.Float’
-        instance Num Float -- Defined in ‘GHC.Float’
-        ...plus two others
-        (use -fprint-potential-instances to see them all)
-    • In the expression: 0
-      In an equation for ‘run’: run = 0
diff --git a/testsuite/tests/polykinds/T12593.stderr b/testsuite/tests/polykinds/T12593.stderr
index 4b551558a1..0a1b83ad9e 100644
--- a/testsuite/tests/polykinds/T12593.stderr
+++ b/testsuite/tests/polykinds/T12593.stderr
@@ -29,3 +29,59 @@ T12593.hs:12:40: error:
         run :: k2 q =>
                Free k k1 k2 p a b
                -> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b
+
+T12593.hs:12:47: error:
+    • Couldn't match kind ‘(((k0 -> k1 -> *) -> Constraint)
+                            -> (k2 -> k3 -> *) -> *)
+                           -> Constraint’
+                     with ‘*’
+      When matching kinds
+        k :: (((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> *)
+             -> Constraint
+        k2 :: *
+    • In the first argument of ‘p’, namely ‘c’
+      In the type signature:
+        run :: k2 q =>
+               Free k k1 k2 p a b
+               -> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b
+
+T12593.hs:12:49: error:
+    • Couldn't match kind ‘((k0 -> k1 -> *) -> Constraint)
+                           -> (k2 -> k3 -> *) -> *’
+                     with ‘*’
+      When matching kinds
+        k4 :: ((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> *
+        k3 :: *
+    • In the second argument of ‘p’, namely ‘d’
+      In the type signature:
+        run :: k2 q =>
+               Free k k1 k2 p a b
+               -> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b
+
+T12593.hs:12:56: error:
+    • Couldn't match kind ‘(((k0 -> k1 -> *) -> Constraint)
+                            -> (k2 -> k3 -> *) -> *)
+                           -> Constraint’
+                     with ‘*’
+      When matching kinds
+        k :: (((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> *)
+             -> Constraint
+        k0 :: *
+    • In the first argument of ‘q’, namely ‘c’
+      In the type signature:
+        run :: k2 q =>
+               Free k k1 k2 p a b
+               -> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b
+
+T12593.hs:12:58: error:
+    • Couldn't match kind ‘((k0 -> k1 -> *) -> Constraint)
+                           -> (k2 -> k3 -> *) -> *’
+                     with ‘*’
+      When matching kinds
+        k4 :: ((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> *
+        k1 :: *
+    • In the second argument of ‘q’, namely ‘d’
+      In the type signature:
+        run :: k2 q =>
+               Free k k1 k2 p a b
+               -> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b
diff --git a/testsuite/tests/polykinds/T13555.stderr b/testsuite/tests/polykinds/T13555.stderr
index eaea0335cf..e822f6e596 100644
--- a/testsuite/tests/polykinds/T13555.stderr
+++ b/testsuite/tests/polykinds/T13555.stderr
@@ -9,26 +9,7 @@ T13555.hs:25:14: error:
                      TaggedT m Maybe (CRTInfo (GF fp d))
         at T13555.hs:25:14-79
       Expected type: TaggedT m Maybe (CRTInfo (GF fp d))
-        Actual type: TaggedT m Maybe (CRTInfo (GF fp d))
-    • When checking that instance signature for ‘crtInfo’
-        is more general than its signature in the class
-        Instance sig: forall (m :: k0).
-                      Reflects m Int =>
-                      TaggedT m Maybe (CRTInfo (GF fp d))
-           Class sig: forall k2 (m :: k2).
-                      Reflects m Int =>
-                      TaggedT m Maybe (CRTInfo (GF fp d))
-      In the instance declaration for ‘CRTrans Maybe (GF fp d)’
-
-T13555.hs:25:14: error:
-    • Could not deduce (Reflects m Int)
-      from the context: Reflects m Int
-        bound by the type signature for:
-                   crtInfo :: forall k2 (m :: k2).
-                              Reflects m Int =>
-                              TaggedT m Maybe (CRTInfo (GF fp d))
-        at T13555.hs:25:14-79
-      The type variable ‘k0’ is ambiguous
+        Actual type: TaggedT m0 Maybe (CRTInfo (GF fp d))
     • When checking that instance signature for ‘crtInfo’
         is more general than its signature in the class
         Instance sig: forall (m :: k0).
diff --git a/testsuite/tests/polykinds/T7438.stderr b/testsuite/tests/polykinds/T7438.stderr
index a198657754..6c4eec47f2 100644
--- a/testsuite/tests/polykinds/T7438.stderr
+++ b/testsuite/tests/polykinds/T7438.stderr
@@ -1,16 +1,16 @@
 
 T7438.hs:6:14: error:
     • Couldn't match expected type ‘p1’ with actual type ‘p’
-        ‘p1’ is untouchable
+        ‘p’ is untouchable
           inside the constraints: b ~ a
           bound by a pattern with constructor:
                      Nil :: forall k (a :: k). Thrist a a,
                    in an equation for ‘go’
           at T7438.hs:6:4-6
-      ‘p1’ is a rigid type variable bound by
-        the inferred type of go :: Thrist a b -> p -> p1 at T7438.hs:6:1-16
       ‘p’ is a rigid type variable bound by
         the inferred type of go :: Thrist a b -> p -> p1 at T7438.hs:6:1-16
+      ‘p1’ is a rigid type variable bound by
+        the inferred type of go :: Thrist a b -> p -> p1 at T7438.hs:6:1-16
       Possible fix: add a type signature for ‘go’
     • In the expression: acc
       In an equation for ‘go’: go Nil acc = acc
diff --git a/testsuite/tests/polykinds/T8566.stderr b/testsuite/tests/polykinds/T8566.stderr
index 1e7818c5ef..0794442edc 100644
--- a/testsuite/tests/polykinds/T8566.stderr
+++ b/testsuite/tests/polykinds/T8566.stderr
@@ -1,6 +1,6 @@
 
 T8566.hs:32:9: error:
-    • Could not deduce (C ('AA (t (I a ps)) as) ps fs0)
+    • Could not deduce (C ('AA (t1 (I a ps)) as) ps fs0)
         arising from a use of ‘c’
       from the context: C ('AA (t (I a ps)) as) ps fs
         bound by the instance declaration at T8566.hs:30:10-67
diff --git a/testsuite/tests/polykinds/T9017.stderr b/testsuite/tests/polykinds/T9017.stderr
index 79a9a4617f..d9483c8490 100644
--- a/testsuite/tests/polykinds/T9017.stderr
+++ b/testsuite/tests/polykinds/T9017.stderr
@@ -1,12 +1,16 @@
 
 T9017.hs:8:7: error:
-    • Couldn't match kind ‘k’ with ‘*’
-      ‘k’ is a rigid type variable bound by
+    • Couldn't match kind ‘k1’ with ‘*’
+      ‘k1’ is a rigid type variable bound by
         the type signature for:
           foo :: forall k k1 (a :: k -> k1 -> *) (b :: k) (m :: k -> k1).
                  a b (m b)
         at T9017.hs:7:1-16
-      When matching the kind of ‘a’
+      When matching types
+        a1 :: * -> * -> *
+        a :: k -> k1 -> *
+      Expected type: a b (m b)
+        Actual type: a1 a0 (m0 a0)
     • In the expression: arr return
       In an equation for ‘foo’: foo = arr return
     • Relevant bindings include
diff --git a/testsuite/tests/typecheck/should_fail/T12373.hs b/testsuite/tests/typecheck/should_fail/T12373.hs
new file mode 100644
index 0000000000..3f23779b82
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T12373.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE MagicHash, ScopedTypeVariables, UnboxedTuples #-}
+
+module T12373 where
+
+import GHC.MVar
+import GHC.Prim
+import GHC.Types
+
+main :: IO ()
+main = IO (\rw -> newMVar# rw) >> return ()
diff --git a/testsuite/tests/typecheck/should_fail/T12373.stderr b/testsuite/tests/typecheck/should_fail/T12373.stderr
new file mode 100644
index 0000000000..45852b8ea6
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T12373.stderr
@@ -0,0 +1,8 @@
+
+T12373.hs:10:19: error:
+    • Couldn't match a lifted type with an unlifted type
+      Expected type: (# State# RealWorld, a1 #)
+        Actual type: (# State# RealWorld, MVar# RealWorld a0 #)
+    • In the expression: newMVar# rw
+      In the first argument of ‘IO’, namely ‘(\ rw -> newMVar# rw)’
+      In the first argument of ‘(>>)’, namely ‘IO (\ rw -> newMVar# rw)’
diff --git a/testsuite/tests/typecheck/should_fail/T13530.hs b/testsuite/tests/typecheck/should_fail/T13530.hs
new file mode 100644
index 0000000000..9f95e497f2
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T13530.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE MagicHash, UnboxedTuples #-}
+
+module T13530 where
+
+import GHC.Exts
+
+g :: Int -> (# Int#, a #)
+g (I# y) = (# y, undefined #)
+
+f :: Int -> (# Int#, Int# #)
+f x = g x
diff --git a/testsuite/tests/typecheck/should_fail/T13530.stderr b/testsuite/tests/typecheck/should_fail/T13530.stderr
new file mode 100644
index 0000000000..8760bcb417
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T13530.stderr
@@ -0,0 +1,7 @@
+
+T13530.hs:11:7: error:
+    • Couldn't match a lifted type with an unlifted type
+      Expected type: (# Int#, Int# #)
+        Actual type: (# Int#, a0 #)
+    • In the expression: g x
+      In an equation for ‘f’: f x = g x
diff --git a/testsuite/tests/typecheck/should_fail/T13610.hs b/testsuite/tests/typecheck/should_fail/T13610.hs
new file mode 100644
index 0000000000..371c3388e9
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T13610.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE MagicHash #-}
+
+module T13610 where
+
+import GHC.Prim
+import GHC.Types
+
+main = do
+    let primDouble = 0.42## :: Double#
+    let double = 0.42 :: Double
+    IO (\s -> mkWeakNoFinalizer# double () s)
diff --git a/testsuite/tests/typecheck/should_fail/T13610.stderr b/testsuite/tests/typecheck/should_fail/T13610.stderr
new file mode 100644
index 0000000000..0755ce9371
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T13610.stderr
@@ -0,0 +1,14 @@
+
+T13610.hs:11:15: error:
+    • Couldn't match a lifted type with an unlifted type
+      When matching types
+        a :: *
+        Weak# () :: TYPE 'UnliftedRep
+      Expected type: (# State# RealWorld, a #)
+        Actual type: (# State# RealWorld, Weak# () #)
+    • In the expression: mkWeakNoFinalizer# double () s
+      In the first argument of ‘IO’, namely
+        ‘(\ s -> mkWeakNoFinalizer# double () s)’
+      In a stmt of a 'do' block:
+        IO (\ s -> mkWeakNoFinalizer# double () s)
+    • Relevant bindings include main :: IO a (bound at T13610.hs:8:1)
diff --git a/testsuite/tests/typecheck/should_fail/T5691.stderr b/testsuite/tests/typecheck/should_fail/T5691.stderr
index ad5c7e452f..9d4e587166 100644
--- a/testsuite/tests/typecheck/should_fail/T5691.stderr
+++ b/testsuite/tests/typecheck/should_fail/T5691.stderr
@@ -1,12 +1,12 @@
 
-T5691.hs:14:9: error:
+T5691.hs:15:24: error:
     • Couldn't match type ‘p’ with ‘PrintRuleInterp’
       Expected type: PrintRuleInterp a
         Actual type: p a
-    • When checking that the pattern signature: p a
-        fits the type of its context: PrintRuleInterp a
-      In the pattern: f :: p a
-      In an equation for ‘test’: test (f :: p a) = MkPRI $ printRule_ f
+    • In the first argument of ‘printRule_’, namely ‘f’
+      In the second argument of ‘($)’, namely ‘printRule_ f’
+      In the expression: MkPRI $ printRule_ f
+    • Relevant bindings include f :: p a (bound at T5691.hs:14:9)
 
 T5691.hs:24:10: error:
     • No instance for (Alternative RecDecParser)
diff --git a/testsuite/tests/typecheck/should_fail/T7368.stderr b/testsuite/tests/typecheck/should_fail/T7368.stderr
index f187aee61c..660ef98f26 100644
--- a/testsuite/tests/typecheck/should_fail/T7368.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7368.stderr
@@ -1,7 +1,11 @@
 
 T7368.hs:3:10: error:
     • Couldn't match kind ‘*’ with ‘* -> *’
-      When matching the kind of ‘Maybe’
+      When matching types
+        b0 :: *
+        Maybe :: * -> *
+      Expected type: a0 -> b0
+        Actual type: c0 Maybe
     • In the first argument of ‘b’, namely ‘(l Nothing)’
       In the expression: b (l Nothing)
       In an equation for ‘f’: f = b (l Nothing)
diff --git a/testsuite/tests/typecheck/should_fail/T7368a.stderr b/testsuite/tests/typecheck/should_fail/T7368a.stderr
index e55aab0e62..16c8326afe 100644
--- a/testsuite/tests/typecheck/should_fail/T7368a.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7368a.stderr
@@ -5,7 +5,7 @@ T7368a.hs:8:6: error:
         f :: * -> *
         Bad :: (* -> *) -> *
       Expected type: f (Bad f)
-        Actual type: Bad (Bad f)
+        Actual type: Bad w0
     • In the pattern: Bad x
       In an equation for ‘fun’: fun (Bad x) = True
     • Relevant bindings include
diff --git a/testsuite/tests/typecheck/should_fail/T7453.stderr b/testsuite/tests/typecheck/should_fail/T7453.stderr
index 518d6fad05..77348c357a 100644
--- a/testsuite/tests/typecheck/should_fail/T7453.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7453.stderr
@@ -1,56 +1,32 @@
 
-T7453.hs:9:15: error:
-    • Couldn't match type ‘p’ with ‘t’
+T7453.hs:10:30: error:
+    • Couldn't match expected type ‘t’ with actual type ‘p’
         because type variable ‘t’ would escape its scope
       This (rigid, skolem) type variable is bound by
         the type signature for:
           z :: forall t. Id t
         at T7453.hs:8:11-19
-      Expected type: Id t
-        Actual type: Id p
-    • In the expression: aux
-      In an equation for ‘z’:
-          z = aux
-            where
-                aux = Id v
-      In an equation for ‘cast1’:
-          cast1 v
-            = runId z
-            where
-                z :: Id t
-                z = aux
-                  where
-                      aux = Id v
+    • In the first argument of ‘Id’, namely ‘v’
+      In the expression: Id v
+      In an equation for ‘aux’: aux = Id v
     • Relevant bindings include
-        aux :: Id p (bound at T7453.hs:10:21)
+        aux :: Id t (bound at T7453.hs:10:21)
         z :: Id t (bound at T7453.hs:9:11)
         v :: p (bound at T7453.hs:7:7)
         cast1 :: p -> a (bound at T7453.hs:7:1)
 
-T7453.hs:15:15: error:
-    • Couldn't match type ‘p’ with ‘t1’
+T7453.hs:16:33: error:
+    • Couldn't match expected type ‘t1’ with actual type ‘p’
         because type variable ‘t1’ would escape its scope
       This (rigid, skolem) type variable is bound by
         the type signature for:
           z :: forall t1. () -> t1
         at T7453.hs:14:11-22
-      Expected type: () -> t1
-        Actual type: () -> p
-    • In the expression: aux
-      In an equation for ‘z’:
-          z = aux
-            where
-                aux = const v
-      In an equation for ‘cast2’:
-          cast2 v
-            = z ()
-            where
-                z :: () -> t
-                z = aux
-                  where
-                      aux = const v
+    • In the first argument of ‘const’, namely ‘v’
+      In the expression: const v
+      In an equation for ‘aux’: aux = const v
     • Relevant bindings include
-        aux :: forall b. b -> p (bound at T7453.hs:16:21)
+        aux :: b -> t1 (bound at T7453.hs:16:21)
         z :: () -> t1 (bound at T7453.hs:15:11)
         v :: p (bound at T7453.hs:13:7)
         cast2 :: p -> t (bound at T7453.hs:13:1)
diff --git a/testsuite/tests/typecheck/should_fail/T7696.stderr b/testsuite/tests/typecheck/should_fail/T7696.stderr
index eef19a5cfc..41f2296797 100644
--- a/testsuite/tests/typecheck/should_fail/T7696.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7696.stderr
@@ -1,7 +1,7 @@
 
 T7696.hs:7:6: error:
-    • Couldn't match type ‘() a0’ with ‘()’
+    • Couldn't match type ‘m0 a0’ with ‘()’
       Expected type: ((), w ())
-        Actual type: (() a0, w ())
+        Actual type: (m0 a0, t0 m0)
     • In the expression: f1
       In an equation for ‘f2’: f2 = f1
diff --git a/testsuite/tests/typecheck/should_fail/T8262.stderr b/testsuite/tests/typecheck/should_fail/T8262.stderr
index d52ee31a31..fb0d17aef5 100644
--- a/testsuite/tests/typecheck/should_fail/T8262.stderr
+++ b/testsuite/tests/typecheck/should_fail/T8262.stderr
@@ -1,7 +1,11 @@
 
 T8262.hs:5:15: error:
     • Couldn't match a lifted type with an unlifted type
-      When matching the kind of ‘GHC.Prim.Int#’
+      When matching types
+        a :: *
+        GHC.Prim.Int# :: TYPE 'GHC.Types.IntRep
     • In the first argument of ‘Just’, namely ‘(1#)’
       In the expression: Just (1#)
       In an equation for ‘foo’: foo x = Just (1#)
+    • Relevant bindings include
+        foo :: p -> Maybe a (bound at T8262.hs:5:1)
diff --git a/testsuite/tests/typecheck/should_fail/T8603.hs b/testsuite/tests/typecheck/should_fail/T8603.hs
index 90c1db3ad6..d17f246209 100644
--- a/testsuite/tests/typecheck/should_fail/T8603.hs
+++ b/testsuite/tests/typecheck/should_fail/T8603.hs
@@ -10,6 +10,10 @@ newtype RV a = RV { getPDF :: [(Rational,a)] } deriving (Show, Eq)
 instance Functor RV where
   fmap f = RV . map (\(x,y) -> (x, f y)) . getPDF
 
+instance Applicative RV where
+  pure = return
+  (<*>) = ap
+
 instance Monad RV where
   return x = RV [(1,x)]
   rv >>= f = RV $
@@ -29,4 +33,4 @@ testRVState1
   = do prize <- lift uniform [1,2,3]
        return False
 
--- lift :: (MonadTrans t, Monad m) => m a -> t m a
\ No newline at end of file
+-- lift :: (MonadTrans t, Monad m) => m a -> t m a
diff --git a/testsuite/tests/typecheck/should_fail/T8603.stderr b/testsuite/tests/typecheck/should_fail/T8603.stderr
index d87bd635c4..d22d13f92b 100644
--- a/testsuite/tests/typecheck/should_fail/T8603.stderr
+++ b/testsuite/tests/typecheck/should_fail/T8603.stderr
@@ -1,19 +1,14 @@
 
-T8603.hs:13:10: error:
-    • No instance for (Applicative RV)
-        arising from the superclasses of an instance declaration
-    • In the instance declaration for ‘Monad RV’
-
-T8603.hs:29:17: error:
+T8603.hs:33:17: error:
     • Couldn't match type ‘RV a1’ with ‘StateT s RV a0’
       Expected type: [Integer] -> StateT s RV a0
-        Actual type: (->) ((->) [a1]) (RV a1)
+        Actual type: t0 ((->) [a1]) (RV a1)
     • The function ‘lift’ is applied to two arguments,
-      but its type ‘([a1] -> RV a1) -> (->) ((->) [a1]) (RV a1)’
+      but its type ‘([a1] -> RV a1) -> t0 ((->) [a1]) (RV a1)’
       has only one
       In a stmt of a 'do' block: prize <- lift uniform [1, 2, 3]
       In the expression:
         do prize <- lift uniform [1, 2, ....]
            return False
     • Relevant bindings include
-        testRVState1 :: RVState s Bool (bound at T8603.hs:28:1)
+        testRVState1 :: RVState s Bool (bound at T8603.hs:32:1)
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 254e04b55d..06789ed71e 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -446,3 +446,6 @@ test('T13677', normal, compile_fail, [''])
 test('T13821A', expect_broken(13821), run_command, ['$MAKE -s --no-print-directory T13821A'])
 test('T13821B', expect_broken(13821), backpack_typecheck_fail, [''])
 test('T13983', normal, compile_fail, [''])
+test('T13530', normal, compile_fail, [''])
+test('T12373', normal, compile_fail, [''])
+test('T13610', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_fail/tcfail090.stderr b/testsuite/tests/typecheck/should_fail/tcfail090.stderr
index 662d7da804..efb81e8ee6 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail090.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail090.stderr
@@ -1,6 +1,8 @@
 
 tcfail090.hs:11:9: error:
     • Couldn't match a lifted type with an unlifted type
-      When matching the kind of ‘ByteArray#’
+      When matching types
+        a0 :: *
+        ByteArray# :: TYPE 'UnliftedRep
     • In the expression: my_undefined
       In an equation for ‘die’: die _ = my_undefined
diff --git a/testsuite/tests/typecheck/should_fail/tcfail122.stderr b/testsuite/tests/typecheck/should_fail/tcfail122.stderr
index a6fbc86c49..29a1576ddb 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail122.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail122.stderr
@@ -1,7 +1,11 @@
 
 tcfail122.hs:8:9: error:
-    • Couldn't match kind ‘*’ with ‘* -> *’
-      When matching the kind of ‘a’
+    • Couldn't match kind ‘* -> *’ with ‘*’
+      When matching types
+        c0 :: (* -> *) -> *
+        a :: * -> *
+      Expected type: a b
+        Actual type: c0 d0
     • In the expression:
           undefined :: forall (c :: (* -> *) -> *) (d :: * -> *). c d
       In the expression:
diff --git a/testsuite/tests/typecheck/should_fail/tcfail123.stderr b/testsuite/tests/typecheck/should_fail/tcfail123.stderr
index 8f5f0a0afe..ad512e102e 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail123.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail123.stderr
@@ -1,7 +1,18 @@
 
 tcfail123.hs:11:9: error:
     • Couldn't match a lifted type with an unlifted type
-      When matching the kind of ‘GHC.Prim.Int#’
+      When matching types
+        p0 :: *
+        GHC.Prim.Int# :: TYPE 'GHC.Types.IntRep
+    • In the first argument of ‘f’, namely ‘3#’
+      In the expression: f 3#
+      In an equation for ‘h’: h v = f 3#
+
+tcfail123.hs:11:9: error:
+    • Couldn't match a lifted type with an unlifted type
+      When matching types
+        p0 :: *
+        GHC.Prim.Int# :: TYPE 'GHC.Types.IntRep
     • In the first argument of ‘f’, namely ‘3#’
       In the expression: f 3#
       In an equation for ‘h’: h v = f 3#
diff --git a/testsuite/tests/typecheck/should_fail/tcfail200.stderr b/testsuite/tests/typecheck/should_fail/tcfail200.stderr
index 407265ee9d..fdd0e3c073 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail200.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail200.stderr
@@ -1,7 +1,11 @@
 
 tcfail200.hs:5:15: error:
     • Couldn't match a lifted type with an unlifted type
-      When matching the kind of ‘GHC.Prim.Int#’
+      When matching types
+        a1 :: *
+        GHC.Prim.Int# :: TYPE 'GHC.Types.IntRep
     • In the expression: 1#
       In the expression: (1#, 'c')
       In an equation for ‘x’: x = (1#, 'c')
+    • Relevant bindings include
+        x :: (a1, Char) (bound at tcfail200.hs:5:9)