Fix #12919 by making the flattener homegeneous.

This changes a key invariant of the flattener. Previously,
flattening a type meant flattening its kind as well. But now,
flattening is always homogeneous -- that is, the kind of the
flattened type is the same as the kind of the input type.
This is achieved by various wizardry in the TcFlatten.flatten_many
function, as described in Note [flatten_many].

There are several knock-on effects, including some refactoring
in the canonicalizer to take proper advantage of the flattener's
changed behavior. In particular, the tyvar case of can_eq_nc' no
longer needs to take casts into account.

Another effect is that flattening a tyconapp might change it
into a casted tyconapp. This might happen if the result kind
of the tycon contains a variable, and that variable changes
during flattening. Because the flattener is homogeneous, it tacks
on a cast to keep the tyconapp kind the same. However, this
is problematic when flattening CFunEqCans, which need to have
an uncasted tyconapp on the LHS and must remain homogeneous.
The solution is a more involved canCFunEqCan, described in
Note [canCFunEqCan].

This patch fixes #13643 (as tested in typecheck/should_compile/T13643)
and the panic in typecheck/should_compile/T13822 (as reported in #14024).
Actually, there were two bugs in T13822: the first was just some
incorrect logic in tryFill (part of the unflattener) -- also fixed
in this patch -- and the other was the main bug fixed in this ticket.

The changes in this patch exposed a long-standing flaw in OptCoercion,
in that breaking apart an AppCo sometimes has unexpected effects on
kinds. See new Note [EtaAppCo] in OptCoercion, which explains the
problem and fix.

Also here is a reversion of the major change in
09bf135ace55ce2572bf4168124d631e386c64bb, affecting ctEvCoercion.
It turns out that making the flattener homogeneous changes the
invariants on the algorithm, making the change in that patch
no longer necessary.

This patch also fixes:
  #14038 (dependent/should_compile/T14038)
  #13910 (dependent/should_compile/T13910)
  #13938 (dependent/should_compile/T13938)
  #14441 (typecheck/should_compile/T14441)
  #14556 (dependent/should_compile/T14556)
  #14720 (dependent/should_compile/T14720)
  #14749 (typecheck/should_compile/T14749)

Sadly, this patch negatively affects performance of type-family-
heavy code. The following patch fixes these performance degradations.
However, the performance fixes are somewhat invasive and so I've
kept them as a separate patch, labeling this one as [skip ci] so
that validation doesn't fail on the performance cases.

24 files changed, 1408 insertions, 655 deletions

diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index 5618824ed5..8e6e18f917 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -185,8 +185,9 @@ canClass :: CtEvidence
 canClass ev cls tys pend_sc
   =   -- all classes do *nominal* matching
     ASSERT2( ctEvRole ev == Nominal, ppr ev $$ ppr cls $$ ppr tys )
-    do { (xis, cos) <- flattenManyNom ev tys
-       ; let co = mkTcTyConAppCo Nominal (classTyCon cls) cos
+    do { (xis, cos, _kind_co) <- flattenArgsNom ev cls_tc tys
+       ; MASSERT( isTcReflCo _kind_co )
+       ; let co = mkTcTyConAppCo Nominal cls_tc cos
              xi = mkClassPred cls xis
              mk_ct new_ev = CDictCan { cc_ev = new_ev
                                      , cc_tyargs = xis
@@ -196,6 +197,8 @@ canClass ev cls tys pend_sc
        ; traceTcS "canClass" (vcat [ ppr ev
                                    , ppr xi, ppr mb ])
        ; return (fmap mk_ct mb) }
+  where
+    cls_tc = classTyCon cls
 
 {- Note [The superclass story]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -634,28 +637,19 @@ 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
 can_eq_nc' flat _rdr_env _envs ev eq_rel ty1 ps_ty1 (CastTy ty2 co2) _
   = canEqCast flat ev eq_rel IsSwapped ty2 co2 ty1 ps_ty1
 
+-- 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
+
 ----------------------
 -- Otherwise try to decompose
 ----------------------
@@ -692,9 +686,8 @@ can_eq_nc' True _rdr_env _envs ev eq_rel ty1 _ (AppTy t2 s2) _
 can_eq_nc' False rdr_env envs ev eq_rel _ ps_ty1 _ ps_ty2
   = do { (xi1, co1) <- flatten FM_FlattenAll ev ps_ty1
        ; (xi2, co2) <- flatten FM_FlattenAll ev ps_ty2
-       ; rewriteEqEvidence ev NotSwapped xi1 xi2 co1 co2
-         `andWhenContinue` \ new_ev ->
-         can_eq_nc' True rdr_env envs new_ev eq_rel xi1 xi1 xi2 xi2 }
+       ; new_ev <- rewriteEqEvidence ev NotSwapped xi1 xi2 co1 co2
+       ; can_eq_nc' True rdr_env envs new_ev eq_rel xi1 xi1 xi2 xi2 }
 
 -- 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
@@ -976,10 +969,9 @@ can_eq_newtype_nc ev swapped ty1 ((gres, co), ty1') ty2 ps_ty2
            -- we have actually used the newtype constructor here, so
            -- make sure we don't warn about importing it!
 
-       ; rewriteEqEvidence ev swapped ty1' ps_ty2
-                           (mkTcSymCo co) (mkTcReflCo Representational ps_ty2)
-         `andWhenContinue` \ new_ev ->
-         can_eq_nc False new_ev ReprEq ty1' ty1' ty2 ps_ty2 }
+       ; new_ev <- rewriteEqEvidence ev swapped ty1' ps_ty2
+                                     (mkTcSymCo co) (mkTcReflCo Representational ps_ty2)
+       ; can_eq_nc False new_ev ReprEq ty1' ty1' ty2 ps_ty2 }
 
 ---------
 -- ^ Decompose a type application.
@@ -1012,6 +1004,15 @@ can_eq_app ev NomEq s1 t1 s2 t2
        ; let co = mkAppCo co_s co_t
        ; setWantedEq dest co
        ; stopWith ev "Decomposed [W] AppTy" }
+
+    -- If there is a ForAll/(->) mismatch, the use of the Left coercion
+    -- below is ill-typed, potentially leading to a panic in splitTyConApp
+    -- Test case: typecheck/should_run/Typeable1
+    -- We could also include this mismatch check above (for W and D), but it's slow
+    -- and we'll get a better error message not doing it
+  | s1k `mismatches` s2k
+  = canEqHardFailure ev (s1 `mkAppTy` t1) (s2 `mkAppTy` t2)
+
   | CtGiven { ctev_evar = evar, ctev_loc = loc } <- ev
   = do { let co   = mkTcCoVarCo evar
              co_s = mkTcLRCo CLeft  co
@@ -1022,8 +1023,14 @@ can_eq_app ev NomEq s1 t1 s2 t2
                                      , evCoercion co_t )
        ; emitWorkNC [evar_t]
        ; canEqNC evar_s NomEq s1 s2 }
-  | otherwise  -- Can't happen
-  = error "can_eq_app"
+
+  where
+    s1k = typeKind s1
+    s2k = typeKind s2
+
+    k1 `mismatches` k2
+      =  isForAllTy k1 && not (isForAllTy k2)
+      || not (isForAllTy k1) && isForAllTy k2
 
 -----------------------
 -- | Break apart an equality over a casted type
@@ -1039,12 +1046,10 @@ canEqCast flat ev eq_rel swapped ty1 co1 ty2 ps_ty2
   = do { traceTcS "Decomposing cast" (vcat [ ppr ev
                                            , ppr ty1 <+> text "|>" <+> ppr co1
                                            , ppr ps_ty2 ])
-       ; rewriteEqEvidence ev swapped ty1 ps_ty2
-                           (mkTcReflCo role ty1
-                              `mkTcCoherenceRightCo` co1)
-                           (mkTcReflCo role ps_ty2)
-         `andWhenContinue` \ new_ev ->
-         can_eq_nc flat new_ev eq_rel ty1 ty1 ty2 ps_ty2 }
+       ; new_ev <- rewriteEqEvidence ev swapped ty1 ps_ty2
+                                     (mkTcReflCo role ty1 `mkTcCoherenceRightCo` co1)
+                                     (mkTcReflCo role ps_ty2)
+       ; can_eq_nc flat new_ev eq_rel ty1 ty1 ty2 ps_ty2 }
   where
     role = eqRelRole eq_rel
 
@@ -1328,9 +1333,8 @@ canEqFailure ev ReprEq ty1 ty2
             -- new equalities become available
        ; traceTcS "canEqFailure with ReprEq" $
          vcat [ ppr ev, ppr ty1, ppr ty2, ppr xi1, ppr xi2 ]
-       ; rewriteEqEvidence ev NotSwapped xi1 xi2 co1 co2
-         `andWhenContinue` \ new_ev ->
-         continueWith (mkIrredCt new_ev) }
+       ; new_ev <- rewriteEqEvidence ev NotSwapped xi1 xi2 co1 co2
+       ; continueWith (mkIrredCt new_ev) }
 
 -- | Call when canonicalizing an equality fails with utterly no hope.
 canEqHardFailure :: CtEvidence
@@ -1339,9 +1343,8 @@ canEqHardFailure :: CtEvidence
 canEqHardFailure ev ty1 ty2
   = do { (s1, co1) <- flatten FM_SubstOnly ev ty1
        ; (s2, co2) <- flatten FM_SubstOnly ev ty2
-       ; rewriteEqEvidence ev NotSwapped s1 s2 co1 co2
-         `andWhenContinue` \ new_ev ->
-         continueWith (mkInsolubleCt new_ev) }
+       ; new_ev <- rewriteEqEvidence ev NotSwapped s1 s2 co1 co2
+       ; continueWith (mkInsolubleCt new_ev) }
 
 {-
 Note [Decomposing TyConApps]
@@ -1444,6 +1447,20 @@ isInsolubleOccursCheck does.
 
 See also #10715, which induced this addition.
 
+Note [canCFunEqCan]
+~~~~~~~~~~~~~~~~~~~
+Flattening the arguments to a type family can change the kind of the type
+family application. As an easy example, consider (Any k) where (k ~ Type)
+is in the inert set. The original (Any k :: k) becomes (Any Type :: Type).
+The problem here is that the fsk in the CFunEqCan will have the old kind.
+
+The solution is to come up with a new fsk/fmv of the right kind. For
+givens, this is easy: just introduce a new fsk and update the flat-cache
+with the new one. For wanteds, we want to solve the old one if favor of
+the new one, so we use dischargeFmv. This also kicks out constraints
+from the inert set; this behavior is correct, as the kind-change may
+allow more constraints to be solved.
+
 -}
 
 canCFunEqCan :: CtEvidence
@@ -1455,107 +1472,206 @@ canCFunEqCan :: CtEvidence
 -- and the RHS is a fsk, which we must *not* substitute.
 -- So just substitute in the LHS
 canCFunEqCan ev fn tys fsk
-  = do { (tys', cos) <- flattenManyNom ev tys
+  = do { (tys', cos, kind_co) <- flattenArgsNom ev fn tys
                         -- cos :: tys' ~ tys
        ; let lhs_co  = mkTcTyConAppCo Nominal fn cos
                         -- :: F tys' ~ F tys
              new_lhs = mkTyConApp fn tys'
-             fsk_ty  = mkTyVarTy fsk
-       ; rewriteEqEvidence ev NotSwapped new_lhs fsk_ty
-                           lhs_co (mkTcNomReflCo fsk_ty)
-         `andWhenContinue` \ ev' ->
-    do { extendFlatCache fn tys' (ctEvCoercion ev', fsk_ty, ctEvFlavour ev')
+
+             flav    = ctEvFlavour ev
+       ; (ev', fsk')
+              -- See Note [canCFunEqCan]
+           <- if isTcReflCo kind_co
+              then do { let fsk_ty = mkTyVarTy fsk
+                      ; ev' <- rewriteEqEvidence ev NotSwapped new_lhs fsk_ty
+                                                 lhs_co (mkTcNomReflCo fsk_ty)
+                      ; return (ev', fsk) }
+              else do { (ev', new_co, new_fsk)
+                          <- newFlattenSkolem flav (ctEvLoc ev) fn tys'
+                      ; case flav of
+                          Given -> return () -- nothing more to do.
+                                             -- NB: new_co is stored within ev',
+                                             -- and will be put in the flat_cache below
+                          _     -> do { let xi = mkTyVarTy new_fsk `mkCastTy` kind_co
+                                               -- sym lhs_co :: F tys ~ F tys'
+                                               -- new_co     :: F tys' ~ new_fsk
+                                               -- co         :: F tys ~ (new_fsk |> kind_co)
+                                            co = mkTcSymCo lhs_co `mkTcTransCo`
+                                                 (new_co `mkTcCoherenceRightCo` kind_co)
+
+                                      ; traceTcS "Discharging fmv due to hetero flattening" empty
+                                      ; dischargeFmv ev fsk co xi }
+                      ; return (ev', new_fsk) }
+
+       ; extendFlatCache fn tys' (ctEvCoercion ev', mkTyVarTy fsk', ctEvFlavour ev')
        ; continueWith (CFunEqCan { cc_ev = ev', cc_fun = fn
-                                 , cc_tyargs = tys', cc_fsk = fsk }) } }
+                                 , cc_tyargs = tys', cc_fsk = fsk' }) }
 
 ---------------------
 canEqTyVar :: CtEvidence          -- ev :: lhs ~ rhs
            -> EqRel -> SwapFlag
-           -> TcTyVar -> CoercionN  -- tv1 |> co1
+           -> TcTyVar               -- tv1
            -> TcType                -- lhs: pretty lhs, already flat
            -> TcType -> TcType      -- rhs: already flat
            -> TcS (StopOrContinue Ct)
-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
+canEqTyVar ev eq_rel swapped tv1 ps_ty1 xi2 ps_xi2
+  | k1 `tcEqType` k2
+  = canEqTyVarHomo ev eq_rel swapped tv1 ps_ty1 xi2 ps_xi2
+
+         -- 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      = mkTcReflCo role xi2 `mkTcCoherenceLeftCo` 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_ty1 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 = mkReflCo role xi1 `mkTcCoherenceLeftCo` sym_k1_co
+             rhs_co = mkReflCo role xi2 `mkTcCoherenceLeftCo` sym_k2_co
+               -- lhs_co :: (xi1 |> sym k1_co) ~ xi1
+               -- rhs_co :: (xi2 |> sym k2_co) ~ xi2
+
+       ; 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_ty1
+                                        new_rhs flat_k2 ps_rhs } }
+  where
+    xi1 = mkTyVarTy tv1
 
+    k1 = tyVarKind tv1
+    k2 = typeKind 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
+                 -> TcS (StopOrContinue Ct)
+canEqTyVarHetero ev eq_rel tv1 co1 ki1 ps_tv1 xi2 ki2 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)
+    -- unswapped: tm :: (lhs :: ki1) ~ (rhs :: ki2)
+    -- swapped  : tm :: (rhs :: ki2) ~ (lhs :: ki1)
   = 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)
+                                       (evCoercion $ mkTcKindCo $ mkTcCoVarCo evar)
+           -- kind_ev_id :: (ki1 :: *) ~ (ki2 :: *)   (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
+              -- co1     :: kind(tv1) ~N ki1
+              -- homo_co :: ki2 ~N kind(tv1)
+             homo_co = mkTcSymCo (mkCoVarCo kind_ev_id) `mkTcTransCo` mkTcSymCo co1
+
+             rhs'    = mkCastTy xi2 homo_co     -- :: kind(tv1)
+             ps_rhs' = mkCastTy ps_xi2 homo_co  -- :: kind(tv1)
+             rhs_co  = mkReflCo role xi2 `mkTcCoherenceLeftCo` homo_co
+               -- rhs_co :: (xi2 |> homo_co :: kind(tv1)) ~ xi2
+
+             lhs'   = mkTyVarTy tv1       -- :: kind(tv1)
+             lhs_co = mkReflCo role lhs' `mkTcCoherenceRightCo` co1
+               -- lhs_co :: (tv1 :: kind(tv1)) ~ (tv1 |> co1 :: ki1)
+
        ; 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' }
+       ; type_ev <- rewriteEqEvidence ev NotSwapped lhs' rhs' lhs_co rhs_co
+       ; canEqTyVarHomo type_ev eq_rel NotSwapped tv1 ps_tv1 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 :: *)
+  = 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) }
 
   where
-    lhs = mkTyVarTy tv1 `mkCastTy` co1
-
-    Pair _ k1 = coercionKind co1
-    k2        = typeKind xi2
-
-    kind_pty = mkHeteroPrimEqPred liftedTypeKind liftedTypeKind k1 k2
-    kind_loc = mkKindLoc lhs xi2 loc
+    kind_pty = mkHeteroPrimEqPred liftedTypeKind liftedTypeKind ki1 ki2
+    kind_loc = mkKindLoc (mkTyVarTy tv1 `mkCastTy` co1) xi2 loc
 
     loc  = ctev_loc ev
+    role = eqRelRole eq_rel
 
 -- guaranteed that typeKind lhs == typeKind rhs
 canEqTyVarHomo :: CtEvidence
                -> EqRel -> SwapFlag
-               -> TcTyVar -> CoercionN   -- lhs: tv1 |> co1
+               -> TcTyVar                -- lhs: tv1
                -> TcType                 -- pretty lhs
                -> TcType -> TcType       -- rhs (might not be flat)
                -> TcS (StopOrContinue Ct)
-canEqTyVarHomo ev eq_rel swapped tv1 co1 ps_ty1 ty2 _
+canEqTyVarHomo ev eq_rel swapped tv1 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
+  = canEqReflexive ev eq_rel (mkTyVarTy tv1)
+    -- we don't need to check co because it must be reflexive
 
   | Just (tv2, co2) <- tcGetCastedTyVar_maybe ty2
   , swapOverTyVars tv1 tv2
-  = do { traceTcS "canEqTyVar" (ppr tv1 $$ ppr tv2 $$ ppr swapped)
+  = 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
+             new_lhs = ty1 `mkCastTy` sym_co2
+             lhs_co  = mkReflCo role ty1 `mkTcCoherenceLeftCo` sym_co2
+
+             new_rhs = mkTyVarTy tv2
+             rhs_co  = mkReflCo role new_rhs `mkTcCoherenceRightCo` co2
+
+       ; new_ev <- rewriteEqEvidence ev swapped new_lhs new_rhs lhs_co rhs_co
+
        ; dflags <- getDynFlags
-       ; canEqTyVar2 dflags ev eq_rel (flipSwap swapped) tv2 co2 ps_ty1 }
+       ; canEqTyVar2 dflags new_ev eq_rel IsSwapped tv2 (ps_ty1 `mkCastTy` sym_co2) }
 
-canEqTyVarHomo ev eq_rel swapped tv1 co1 _ _ ps_ty2
+canEqTyVarHomo ev eq_rel swapped tv1 _ _ ps_ty2
   = do { dflags <- getDynFlags
-       ; canEqTyVar2 dflags ev eq_rel swapped tv1 co1 ps_ty2 }
+       ; canEqTyVar2 dflags ev eq_rel swapped tv1 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)
@@ -1563,28 +1679,26 @@ canEqTyVar2 :: DynFlags
             -> CtEvidence   -- lhs ~ rhs (or, if swapped, orhs ~ olhs)
             -> EqRel
             -> SwapFlag
-            -> TcTyVar -> CoercionN     -- lhs = tv |> co, flat
+            -> TcTyVar                  -- lhs = tv, 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 co1 orhs
-  | Just nrhs' <- metaTyVarUpdateOK dflags tv1 nrhs  -- No occurs check
+canEqTyVar2 dflags ev eq_rel swapped tv1 rhs
+  | Just rhs' <- metaTyVarUpdateOK dflags tv1 rhs  -- No occurs check
      -- Must do the occurs check even on tyvar/tyvar
      -- equalities, in case have  x ~ (y :: ..x...)
      -- Trac #12593
-  = rewriteEqEvidence ev swapped nlhs nrhs' rewrite_co1 rewrite_co2
-    `andWhenContinue` \ new_ev ->
-    continueWith (CTyEqCan { cc_ev = new_ev, cc_tyvar = tv1
-                           , cc_rhs = nrhs', cc_eq_rel = eq_rel })
+  = 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 }) }
 
   | 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 nrhs)
-       ; rewriteEqEvidence ev swapped nlhs nrhs rewrite_co1 rewrite_co2
-         `andWhenContinue` \ new_ev ->
-         if isInsolubleOccursCheck eq_rel tv1 nrhs
+  = 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)
              -- If we have a ~ [a], it is not canonical, and in particular
              -- we don't want to rewrite existing inerts with it, otherwise
@@ -1600,13 +1714,10 @@ canEqTyVar2 dflags ev eq_rel swapped tv1 co1 orhs
   where
     role = eqRelRole eq_rel
 
-    nlhs = mkTyVarTy tv1
-    nrhs = orhs `mkCastTy` mkTcSymCo co1
+    lhs = mkTyVarTy tv1
 
-    -- 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
+    rewrite_co1  = mkTcReflCo role lhs
+    rewrite_co2  = mkTcReflCo role rhs
 
 -- | Solve a reflexive equality constraint
 canEqReflexive :: CtEvidence    -- ty ~ ty
@@ -1896,7 +2007,7 @@ rewriteEqEvidence :: CtEvidence         -- Old evidence :: olhs ~ orhs (not swap
                                         -- Should be zonked, because we use typeKind on nlhs/nrhs
                   -> TcCoercion         -- lhs_co, of type :: nlhs ~ olhs
                   -> TcCoercion         -- rhs_co, of type :: nrhs ~ orhs
-                  -> TcS (StopOrContinue CtEvidence)  -- Of type nlhs ~ nrhs
+                  -> TcS CtEvidence     -- Of type nlhs ~ nrhs
 -- For (rewriteEqEvidence (Given g olhs orhs) False nlhs nrhs lhs_co rhs_co)
 -- we generate
 -- If not swapped
@@ -1914,19 +2025,18 @@ rewriteEqEvidence :: CtEvidence         -- Old evidence :: olhs ~ orhs (not swap
 -- It's all a form of rewwriteEvidence, specialised for equalities
 rewriteEqEvidence old_ev swapped nlhs nrhs lhs_co rhs_co
   | CtDerived {} <- old_ev  -- Don't force the evidence for a Derived
-  = continueWith (old_ev { ctev_pred = new_pred })
+  = return (old_ev { ctev_pred = new_pred })
 
   | NotSwapped <- swapped
   , isTcReflCo lhs_co      -- See Note [Rewriting with Refl]
   , isTcReflCo rhs_co
-  = continueWith (old_ev { ctev_pred = new_pred })
+  = return (old_ev { ctev_pred = new_pred })
 
   | CtGiven { ctev_evar = old_evar } <- old_ev
   = do { let new_tm = evCoercion (lhs_co
                                   `mkTcTransCo` maybeSym swapped (mkTcCoVarCo old_evar)
                                   `mkTcTransCo` mkTcSymCo rhs_co)
-       ; new_ev <- newGivenEvVar loc' (new_pred, new_tm)
-       ; continueWith new_ev }
+       ; newGivenEvVar loc' (new_pred, new_tm) }
 
   | CtWanted { ctev_dest = dest } <- old_ev
   = do { (new_ev, hole_co) <- newWantedEq loc' (ctEvRole old_ev) nlhs nrhs
@@ -1936,7 +2046,7 @@ rewriteEqEvidence old_ev swapped nlhs nrhs lhs_co rhs_co
                   `mkTransCo` rhs_co
        ; setWantedEq dest co
        ; traceTcS "rewriteEqEvidence" (vcat [ppr old_ev, ppr nlhs, ppr nrhs, ppr co])
-       ; continueWith new_ev }
+       ; return new_ev }
 
   | otherwise
   = panic "rewriteEvidence"
@@ -1956,7 +2066,7 @@ When decomposing equalities we often create new wanted constraints for
 Similar remarks apply for Derived.
 
 Rather than making an equality test (which traverses the structure of the
-type, perhaps fruitlessly, unifyWanted traverses the common structure, and
+type, perhaps fruitlessly), unifyWanted traverses the common structure, and
 bales out when it finds a difference by creating a new Wanted constraint.
 But where it succeeds in finding common structure, it just builds a coercion
 to reflect it.
diff --git a/compiler/typecheck/TcFlatten.hs b/compiler/typecheck/TcFlatten.hs
index ec0c2de504..0700ae8849 100644
--- a/compiler/typecheck/TcFlatten.hs
+++ b/compiler/typecheck/TcFlatten.hs
@@ -2,7 +2,7 @@
 
 module TcFlatten(
    FlattenMode(..),
-   flatten, flattenManyNom,
+   flatten, flattenKind, flattenArgsNom,
 
    unflattenWanteds
  ) where
@@ -20,17 +20,16 @@ import TyCon
 import TyCoRep   -- performs delicate algorithm on types
 import Coercion
 import Var
+import VarSet
 import VarEnv
 import Outputable
 import TcSMonad as TcS
 import BasicTypes( SwapFlag(..) )
 
+import Pair
 import Util
 import Bag
-import Pair
 import Control.Monad
-import MonadUtils ( zipWithAndUnzipM )
-import GHC.Exts ( inline )
 
 import Control.Arrow ( first )
 
@@ -57,7 +56,7 @@ Note [The flattening story]
 
    - A unification flatten-skolem, fmv, stands for the as-yet-unknown
      type to which (F xis) will eventually reduce.  It is filled in
-     only by dischargeFmv.
+
 
    - All fsk/fmv variables are "untouchable".  To make it simple to test,
      we simply give them TcLevel=0.  This means that in a CTyVarEq, say,
@@ -479,13 +478,6 @@ eqFlattenMode FM_SubstOnly  FM_SubstOnly  = True
 --  FM_Avoid tv1 b1 `eq` FM_Avoid tv2 b2 = tv1 == tv2 && b1 == b2
 eqFlattenMode _  _ = False
 
-mkFlattenEnv :: FlattenMode -> CtEvidence -> FlatWorkListRef -> FlattenEnv
-mkFlattenEnv fm ctev ref = FE { fe_mode    = fm
-                              , fe_loc     = ctEvLoc ctev
-                              , fe_flavour = ctEvFlavour ctev
-                              , fe_eq_rel  = ctEvEqRel ctev
-                              , fe_work    = ref }
-
 -- | The 'FlatM' monad is a wrapper around 'TcS' with the following
 -- extra capabilities: (1) it offers access to a 'FlattenEnv';
 -- and (2) it maintains the flattening worklist.
@@ -513,15 +505,23 @@ emitFlatWork :: Ct -> FlatM ()
 -- See Note [The flattening work list]
 emitFlatWork ct = FlatM $ \env -> updTcRef (fe_work env) (ct :)
 
-runFlatten :: FlattenMode -> CtEvidence -> FlatM a -> TcS a
+-- convenient wrapper when you have a CtEvidence describing
+-- the flattening operation
+runFlattenCtEv :: FlattenMode -> CtEvidence -> FlatM a -> TcS a
+runFlattenCtEv mode ev
+  = runFlatten mode (ctEvLoc ev) (ctEvFlavour ev) (ctEvEqRel ev)
+
 -- Run thing_inside (which does flattening), and put all
 -- the work it generates onto the main work list
 -- See Note [The flattening work list]
--- NB: The returned evidence is always the same as the original, but with
--- perhaps a new CtLoc
-runFlatten mode ev thing_inside
+runFlatten :: FlattenMode -> CtLoc -> CtFlavour -> EqRel -> FlatM a -> TcS a
+runFlatten mode loc flav eq_rel thing_inside
   = do { flat_ref <- newTcRef []
-       ; let fmode = mkFlattenEnv mode ev flat_ref
+       ; let fmode = FE { fe_mode = mode
+                        , fe_loc  = loc
+                        , fe_flavour = flav
+                        , fe_eq_rel = eq_rel
+                        , fe_work = flat_ref }
        ; res <- runFlatM thing_inside fmode
        ; new_flats <- readTcRef flat_ref
        ; updWorkListTcS (add_flats new_flats)
@@ -585,16 +585,18 @@ setMode new_mode thing_inside
     then runFlatM thing_inside env
     else runFlatM thing_inside (env { fe_mode = new_mode })
 
--- | Use when flattening kinds/kind coercions. See
+-- | Make sure that flattening actually produces a coercion (in other
+-- words, make sure our flavour is not Derived)
 -- Note [No derived kind equalities]
-flattenKinds :: FlatM a -> FlatM a
-flattenKinds thing_inside
+noBogusCoercions :: FlatM a -> FlatM a
+noBogusCoercions thing_inside
   = FlatM $ \env ->
     let kind_flav = case fe_flavour env of
-                      Given -> Given
-                      _     -> Wanted WDeriv
+                      Derived -> Wanted WDeriv
+                      other   -> other
     in
-    runFlatM thing_inside (env { fe_eq_rel = NomEq, fe_flavour = kind_flav })
+    runFlatM thing_inside (env { fe_flavour = kind_flav })
+
 
 bumpDepth :: FlatM a -> FlatM a
 bumpDepth (FlatM thing_inside)
@@ -721,15 +723,11 @@ 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.
+A kind-level coercion can appear in types, via mkCastTy. So, whenever
+we are generating a coercion in a dependent context (in other words,
+in a kind) we need to make sure that our flavour is never Derived
+(as Derived constraints have no evidence). The noBogusCoercions function
+changes the flavour from Derived just for this purpose.
 
 -}
 
@@ -746,21 +744,36 @@ flatten :: FlattenMode -> CtEvidence -> TcType
         -> TcS (Xi, TcCoercion)
 flatten mode ev ty
   = do { traceTcS "flatten {" (ppr mode <+> ppr ty)
-       ; (ty', co) <- runFlatten mode ev (flatten_one ty)
+       ; (ty', co) <- runFlattenCtEv mode ev (flatten_one ty)
        ; traceTcS "flatten }" (ppr ty')
        ; return (ty', co) }
 
-flattenManyNom :: CtEvidence -> [TcType] -> TcS ([Xi], [TcCoercion])
+-- specialized to flattening kinds: never Derived, always Nominal
+-- See Note [No derived kind equalities]
+flattenKind :: CtLoc -> CtFlavour -> TcType -> TcS (Xi, TcCoercionN)
+flattenKind loc flav ty
+  = do { traceTcS "flattenKind {" (ppr flav <+> ppr ty)
+       ; let flav' = case flav of
+                       Derived -> Wanted WDeriv  -- the WDeriv/WOnly choice matters not
+                       _       -> flav
+       ; (ty', co) <- runFlatten FM_FlattenAll loc flav' NomEq (flatten_one ty)
+       ; traceTcS "flattenKind }" (ppr ty' $$ ppr co) -- co is never a panic
+       ; return (ty', co) }
+
+flattenArgsNom :: CtEvidence -> TyCon -> [TcType] -> TcS ([Xi], [TcCoercion], TcCoercionN)
 -- Externally-callable, hence runFlatten
--- Flatten a bunch of types all at once; in fact they are
--- always the arguments of a saturated type-family, so
+-- Flatten a vector of types all at once; in fact they are
+-- always the arguments of type family or class, so
 --      ctEvFlavour ev = Nominal
 -- and we want to flatten all at nominal role
-flattenManyNom ev tys
-  = do { traceTcS "flatten_many {" (vcat (map ppr tys))
-       ; (tys', cos) <- runFlatten FM_FlattenAll ev (flatten_many_nom tys)
+-- The kind passed in is the kind of the type family or class, call it T
+-- The last coercion returned has type (typeKind(T xis) ~N typeKind(T tys))
+flattenArgsNom ev tc tys
+  = do { traceTcS "flatten_args {" (vcat (map ppr tys))
+       ; (tys', cos, kind_co)
+           <- runFlattenCtEv FM_FlattenAll ev (flatten_args_tc tc (repeat Nominal) tys)
        ; traceTcS "flatten }" (vcat (map ppr tys'))
-       ; return (tys', cos) }
+       ; return (tys', cos, kind_co) }
 
 
 {- *********************************************************************
@@ -778,6 +791,11 @@ flattenManyNom ev tys
          has no filled-in metavariables
       co :: xi ~ ty
 
+Key invariants:
+  (F0) co :: xi ~ zonk(ty)
+  (F1) typeKind(xi) succeeds and returns a fully zonked kind
+  (F2) typeKind(xi) `eqType` zonk(typeKind(ty))
+
 Note that it is flatten's job to flatten *every type function it sees*.
 flatten is only called on *arguments* to type functions, by canEqGiven.
 
@@ -787,9 +805,10 @@ Flattening also:
 
 Because flattening zonks and the returned coercion ("co" above) is also
 zonked, it's possible that (co :: xi ~ ty) isn't quite true. So, instead,
-we can rely on these facts:
+we can rely on this fact:
+
   (F1) typeKind(xi) succeeds and returns a fully zonked kind
-  (F2) co :: xi ~ zonk(ty)
+
 Note that the left-hand type of co is *always* precisely xi. The right-hand
 type may or may not be ty, however: if ty has unzonked filled-in metavariables,
 then the right-hand type of co will be the zonked version of ty.
@@ -798,45 +817,16 @@ occasionally have to explicitly zonk, when (co :: xi ~ ty) is important
 even before we zonk the whole program. For example, see the FTRNotFollowed
 case in flattenTyVar.
 
-Why have these invariants on flattening? Really, they're both to ensure
-invariant (F1), which is a Good Thing because we sometimes use typeKind
+Why have these invariants on flattening? Because we sometimes use typeKind
 during canonicalisation, and we want this kind to be zonked (e.g., see
-TcCanonical.homogeniseRhsKind). Invariant (F2) is needed solely to support
-(F1). It is relied on in one place:
-
- - The FTRNotFollowed case in flattenTyVar. Here, we have a tyvar
- that cannot be reduced any further (that is, no equality over the tyvar
- is in the inert set such that the inert equality can rewrite the constraint
- at hand, and it is not a filled-in metavariable).
- But its kind might still not be flat,
- if it mentions a type family or a variable that can be rewritten. Flattened
- types have flattened kinds (see below), so we must flatten the kind. Here is
- an example:
-
-   let kappa be a filled-in metavariable such that kappa := k.
-   [G] co :: k ~ Type
-
-   We are flattening
-     a :: kappa
-   where a is a skolem.
-
- We end up in the FTRNotFollowed case, but we need to flatten the kind kappa.
- Flattening kappa yields (Type, kind_co), where kind_co :: Type ~ k. Note that the
- right-hand type of kind_co is *not* kappa, because (F1) tells us it's zonk(kappa),
- which is k. Now, we return (a |> sym kind_co). If we are to uphold (F1), then
- the right-hand type of (sym kind_co) had better be fully zonked. In other words,
- the left-hand type of kind_co needs to be zonked... which is precisely what (F2)
- guarantees.
-
-In order to support (F2), we require that ctEvCoercion, when called on a
-zonked CtEvidence, always returns a zonked coercion. See Note [Given in
-ctEvCoercion]. This requirement comes into play in flatten_tyvar2. (I suppose
-we could move the logic from ctEvCoercion to flatten_tyvar2, but it's much
-easier to do in ctEvCoercion.)
-
-Flattening a type also means flattening its kind. In the case of a type
-variable whose kind mentions a type family, this might mean that the result
-of flattening has a cast in it.
+TcCanonical.canEqTyVar).
+
+Flattening is always homogeneous. That is, the kind of the result of flattening is
+always the same as the kind of the input, modulo zonking. More formally:
+
+  (F2) typeKind(xi) `eqType` zonk(typeKind(ty))
+
+This invariant means that the kind of a flattened type might not itself be flat.
 
 Recall that in comments we use alpha[flat = ty] to represent a
 flattening skolem variable alpha which has been generated to stand in
@@ -863,12 +853,12 @@ transitive expansion contains any type function applications.  If so,
 it expands the synonym and proceeds; if not, it simply returns the
 unexpanded synonym.
 
-Note [flatten_many performance]
+Note [flatten_args performance]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-In programs with lots of type-level evaluation, flatten_many becomes
+In programs with lots of type-level evaluation, flatten_args becomes
 part of a tight loop. For example, see test perf/compiler/T9872a, which
-calls flatten_many a whopping 7,106,808 times. It is thus important
-that flatten_many be efficient.
+calls flatten_args a whopping 7,106,808 times. It is thus important
+that flatten_args be efficient.
 
 Performance testing showed that the current implementation is indeed
 efficient. It's critically important that zipWithAndUnzipM be
@@ -879,8 +869,8 @@ it. On test T9872a, here are the allocation stats (Dec 16, 2014):
  * Specialized, uninlined:       6,639,253,488 bytes allocated in the heap
  * Specialized, inlined:         6,281,539,792 bytes allocated in the heap
 
-To improve performance even further, flatten_many_nom is split off
-from flatten_many, as nominal equality is the common case. This would
+To improve performance even further, flatten_args_nom is split off
+from flatten_args, as nominal equality is the common case. This would
 be natural to write using mapAndUnzipM, but even inlined, that function
 is not as performant as a hand-written loop.
 
@@ -893,32 +883,331 @@ and T5321Fun.
 If we need to make this yet more performant, a possible way forward is to
 duplicate the flattener code for the nominal case, and make that case
 faster. This doesn't seem quite worth it, yet.
+
+Note [flatten_args]
+~~~~~~~~~~~~~~~~~~~
+Invariant (F2) of Note [Flattening] says that flattening is homogeneous.
+This causes some trouble when flattening a function applied to a telescope
+of arguments, perhaps with dependency. For example, suppose
+
+  type family F :: forall (j :: Type) (k :: Type). Maybe j -> Either j k -> Bool -> [k]
+
+and we wish to flatten the args of (with kind applications explicit)
+
+  F a b (Just a c) (Right a b d) False
+
+where all variables are skolems and
+
+  a :: Type
+  b :: Type
+  c :: a
+  d :: k
+
+  [G] aco :: a ~ fa
+  [G] bco :: b ~ fb
+  [G] cco :: c ~ fc
+  [G] dco :: d ~ fd
+
+We process the args in left-to-right order. The first two args are easy:
+
+  (sym aco, fa) <- flatten a
+  (sym bco, fb) <- flatten b
+
+But now consider flattening (Just a c :: Maybe a). Regardless of how this
+flattens, the result will have kind (Maybe a), due to (F2). And yet, when
+we build the application (F fa fb ...), we need this argument to have kind
+(Maybe fa), not (Maybe a). Suppose (Just a c) flattens to f3 (the "3" is
+because it's the 3rd argument). We know f3 :: Maybe a. In order to get f3
+to have kind Maybe fa, we must cast it. The coercion to use is determined
+by the kind of F: we see in F's kind that the third argument has kind
+Maybe j. Critically, we also know that the argument corresponding to j
+(in our example, a) flattened with a coercion (sym aco). We can thus
+know the coercion needed for the 3rd argument is (Maybe aco).
+
+More generally, we must use the Lifting Lemma, as implemented in
+Coercion.liftCoSubst. As we work left-to-right, any variable that is a
+dependent parameter (j and k, in our example) gets mapped in a lifting context
+to the coercion that is output from flattening the corresponding argument (aco
+and bco, in our example). Then, after flattening later arguments, we lift the
+kind of these arguments in the lifting context that we've be building up.
+This coercion is then used to keep the result of flattening well-kinded.
+
+Working through our example, this is what happens:
+
+  1. Flatten a, getting (sym aco, fa). Extend the (empty) LC with [j |-> sym aco]
+
+  2. Flatten b, getting (sym bco, fb). Extend the LC with [k |-> sym bco].
+
+  3. Flatten (Just a c), getting (co3, f3). Lifting the kind (Maybe j) with our LC
+     yields lco3 :: Maybe fa ~ Maybe a. Use (f3 |> sym lco3) as the argument to
+     F.
+
+  4. Flatten (Right a b d), getting (co4, f4). Lifting the kind (Either j k) with our LC
+     yields lco4 :: Either fa fb ~ Either a b. Use (f4 |> sym lco4) as the 4th
+     argument to F.
+
+  5. Flatten False, getting (<False>, False). We lift Bool with our LC, getting <Bool>;
+     casting has no effect. (Indeed we lifted and casted with no effect for steps 1 and 2, as well.)
+
+We're now almost done, but the new application (F fa fb (f3 |> sym lco3) (f4
+|> sym lco4) False) has the wrong kind. Its kind is [fb], instead of the original [b].
+So we must use our LC one last time to lift the result kind [k], getting res_co :: [fb] ~ [b], and
+we cast our result.
+
+Accordingly, the final result is
+
+  F fa fb (Just fa (fc |> aco) |> Maybe (sym aco) |> sym (Maybe (sym aco)))
+          (Right fa fb (fd |> bco) |> Either (sym aco) (sym bco) |> sym (Either (sym aco) (sym bco)))
+          False
+            |> [sym bco]
+
+The res_co is returned as the third return value from flatten_args.
+
+Note [Last case in flatten_args]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In writing flatten_args's `go`, we know here that tys cannot be empty,
+because that case is first. We've run out of
+binders. But perhaps inner_ki is a tyvar that has been instantiated with a
+Π-type. I believe this, today, this Π-type must be an ordinary function.
+But tomorrow, we may allow, say, visible type application in types. And
+it's best to be prepared.
+
+Here is an example.
+
+  a :: forall (k :: Type). k -> k
+  type family Star
+  Proxy :: forall j. j -> Type
+  axStar :: Star ~ Type
+  type family NoWay :: Bool
+  axNoWay :: NoWay ~ False
+  bo :: Type
+  [G] bc :: bo ~ Bool   (in inert set)
+
+  co :: (forall j. j -> Type) ~ (forall (j :: Star). (j |> axStar) -> Star)
+  co = forall (j :: sym axStar). (<j> -> sym axStar)
+
+  We are flattening:
+  a (forall (j :: Star). (j |> axStar) -> Star)   -- 1
+    (Proxy |> co)                                 -- 2
+    (bo |> sym axStar)                            -- 3
+    (NoWay |> sym bc)                             -- 4
+      :: Star
+
+Flattening (1) gives us
+    (forall j. j -> Type)
+    co1 :: (forall j. j -> Type) ~ (forall (j :: Star). (j |> axStar) -> Star)
+We also extend the lifting context with
+    k |-> co1
+
+Flattening (2) gives us
+    (Proxy |> co)
+But building (a (forall j. j -> Type) Proxy) would be ill-kinded. So we cast the
+result of flattening by sym co1, to get
+    (Proxy |> co |> sym co1)
+Happily, co and co1 cancel each other out, leaving us with
+    Proxy
+    co2 :: Proxy ~ (Proxy |> co)
+
+Now we need to flatten (3). After flattening, should we tack on a homogenizing
+coercion? The way we normally tell is to look at the kind of `a`. (See Note
+[flatten_args].) Here, the remainder of the kind of `a` that we're left with
+after processing two arguments is just `k`.
+
+The way forward is look up k in the lifting context, getting co1. If we're at
+all well-typed, co1 will be a coercion between Π-types, with enough binders on
+both sides to accommodate any remaining arguments in flatten_args. So, let's
+decompose co1 with decomposePiCos. This decomposition needs arguments to use
+to instantiate any kind parameters. Look at the type of co1. If we just
+decomposed it, we would end up with coercions whose types include j, which is
+out of scope here. Accordingly, decomposePiCos takes a list of types whose
+kinds are the *right-hand* types in the decomposed coercion. (See comments on
+decomposePiCos, which also reverses the orientation of the coercions.)
+The right-hand types are the unflattened ones -- conveniently what we have to
+hand.
+
+So we now call
+
+  decomposePiCos (forall j. j -> Type)
+                 [bo |> sym axStar, NoWay |> sym bc]
+                 co1
+
+to get
+
+  co3 :: Star ~ Type
+  co4 :: (j |> axStar) ~ (j |> co3), substituted to
+                              (bo |> sym axStar |> axStar) ~ (bo |> sym axStar |> co3)
+                           == bo ~ bo
+  res_co :: Type ~ Star -- this one's not reversed in decomposePiCos
+
+We then use these casts on (3) and (4) to get
+
+  (bo |> sym axStar |> co3 :: Type)   -- (C3)
+  (NoWay |> sym bc |> co4 :: bo)      -- (C4)
+
+We can simplify to
+
+  bo                          -- (C3)
+  (NoWay |> sym bc :: bo)     -- (C4)
+
+Now, to flatten (C3) and (C4), we still need to keep track of dependency.
+We know the type of the function applied to (C3) and (C4) must be
+(forall j. j -> Type), the flattened type
+associated with k (the final type in the kind of `a`.) (We discard the lifting
+context up to this point; as we've already substituted k, the domain of the
+lifting context we used for (1) and (2), away.)
+
+We now flatten (C3) to get
+  Bool                        -- F3
+  co5 :: Bool ~ bo
+and flatten (C4) to get
+  (False |> sym bc)
+Like we did when flattening (2), we need to cast the result of flattening
+(4), by lifting the type j with a lifting context containing
+[j |-> co5]. This lifting yields co5.
+We cast the result of flattening (C4) by sym co5 (this is the normal
+cast-after-flattening; see Note [flatten_args]):
+  (False |> sym bc |> sym co5)
+which is really just
+  False                       -- F4
+  co4 :: False ~ (NoWay |> sym bc)
+
+Now, we build up the result
+
+  a (forall j. j -> Type)
+    Proxy
+    Bool
+    False
+      |> res_co
+
+Let's check whether this is well-typed. We know
+
+  a :: forall (k :: Type). k -> k
+
+  a (forall j. j -> Type) :: (forall j. j -> Type) -> forall j. j -> Type
+
+  a (forall j. j -> Type)
+    Proxy
+      :: forall j. j -> Type
+
+  a (forall j. j -> Type)
+    Proxy
+    Bool
+      :: Bool -> Type
+
+  a (forall j. j -> Type)
+    Proxy
+    Bool
+    False
+      :: Type
+
+  a (forall j. j -> Type)
+    Proxy
+    Bool
+    False
+     |> res_co
+     :: Star
+
+as desired. (Why do we want Star? Because we started with something of kind Star!)
+
+Whew.
+
 -}
 
-flatten_many :: [Role] -> [Type] -> FlatM ([Xi], [Coercion])
+flatten_args_tc :: TyCon -> [Role] -> [Type] -> FlatM ([Xi], [Coercion], CoercionN)
+flatten_args_tc tc = flatten_args (bndrs `chkAppend` inner_bndrs) inner_ki emptyVarSet
+                                                 -- NB: TyCon kinds are always closed
+  where
+    bndrs                   = tyConBindersTyBinders (tyConBinders tc)
+    (inner_bndrs, inner_ki) = splitPiTys (tyConResKind tc)
+      -- it's possible that the result kind has arrows (for, e.g., a type family)
+      -- so we must split it
+
+flatten_args :: [TyBinder] -> Kind -> TcTyCoVarSet -- function kind; kind's free vars
+             -> [Role] -> [Type]   -- these are in 1-to-1 correspondence
+             -> FlatM ([Xi], [Coercion], CoercionN)
 -- Coercions :: Xi ~ Type, at roles given
--- Returns True iff (no flattening happened)
--- NB: The EvVar inside the 'fe_ev :: CtEvidence' is unused,
---     we merely want (a) Given/Solved/Derived/Wanted info
---                    (b) the GivenLoc/WantedLoc for when we create new evidence
-flatten_many roles tys
--- See Note [flatten_many performance]
-  = inline zipWithAndUnzipM go roles tys
+-- Third coercion :: typeKind(fun xis) ~N typeKind(fun tys)
+-- That is, the third coercion relates the kind of some function (whose kind is
+-- passed as the first parameter) instantiated at xis to the kind of that function
+-- instantiated at the tys. This is useful in keeping flattening homoegeneous.
+-- The list of roles must be at least as long as the list of types.
+-- See Note [flatten_args]
+flatten_args orig_binders orig_inner_ki orig_fvs orig_roles orig_tys
+  = go [] [] orig_lc orig_binders orig_inner_ki orig_roles orig_tys
   where
-    go Nominal          ty = setEqRel NomEq  $ flatten_one ty
-    go Representational ty = setEqRel ReprEq $ flatten_one ty
-    go Phantom          ty = -- See Note [Phantoms in the flattener]
-                             do { ty <- liftTcS $ zonkTcType ty
-                                ; return ( ty, mkReflCo Phantom ty ) }
-
--- | Like 'flatten_many', but assumes that every role is nominal.
-flatten_many_nom :: [Type] -> FlatM ([Xi], [Coercion])
-flatten_many_nom [] = return ([], [])
--- See Note [flatten_many performance]
-flatten_many_nom (ty:tys)
-  = do { (xi, co) <- flatten_one ty
-       ; (xis, cos) <- flatten_many_nom tys
-       ; return (xi:xis, co:cos) }
+    orig_lc = emptyLiftingContext $ mkInScopeSet $ orig_fvs
+
+    go :: [Xi]        -- Xis accumulator, in reverse order
+       -> [Coercion]  -- Coercions accumulator, in reverse order
+                      -- These are in 1-to-1 correspondence
+       -> LiftingContext  -- mapping from tyvars to flattening coercions
+       -> [TyBinder]  -- Unsubsted binders of function's kind
+       -> Kind        -- Unsubsted result kind of function (not a Pi-type)
+       -> [Role]      -- Roles at which to flatten these ...
+       -> [Type]      -- ... unflattened types
+       -> FlatM ([Xi], [Coercion], CoercionN)
+    go acc_xis acc_cos lc binders inner_ki _ []
+      = return (reverse acc_xis, reverse acc_cos, kind_co)
+      where
+        final_kind = mkPiTys binders inner_ki
+        kind_co    = liftCoSubst Nominal lc final_kind
+
+    go acc_xis acc_cos lc (binder:binders) inner_ki (role:roles) (ty:tys)
+      = do { (xi, co) <- case role of
+               Nominal          -> setEqRel NomEq $
+                                   if isNamedTyBinder binder
+                                   then noBogusCoercions $ flatten_one ty
+                                   else                    flatten_one ty
+
+               Representational -> ASSERT( isAnonTyBinder binder )
+                                   setEqRel ReprEq $ flatten_one ty
+
+               Phantom          -> -- See Note [Phantoms in the flattener]
+                                   ASSERT( isAnonTyBinder binder )
+                                   do { ty <- liftTcS $ zonkTcType ty
+                                      ; return (ty, mkReflCo Phantom ty) }
+
+             -- By Note [Flattening] invariant (F2), typeKind(xi) = typeKind(ty).
+             -- But, it's possible that xi will be used as an argument to a function
+             -- whose kind is different, if earlier arguments have been flattened
+             -- to new types. We thus need a coercion (kind_co :: old_kind ~ new_kind).
+           ; let kind_co = mkTcSymCo $ liftCoSubst Nominal lc (tyBinderType binder)
+                 casted_xi = xi `mkCastTy` kind_co
+                 casted_co = co `mkTcCoherenceLeftCo` kind_co
+
+             -- now, extend the lifting context with the new binding
+                 new_lc | Just tv <- tyBinderVar_maybe binder
+                        = extendLiftingContextAndInScope lc tv casted_co
+                        | otherwise
+                        = lc
+
+           ; go (casted_xi : acc_xis) (casted_co : acc_cos) new_lc binders inner_ki roles tys }
+
+      -- See Note [Last case in flatten_args]
+    go acc_xis acc_cos lc [] inner_ki roles tys
+      | Just k   <- tcGetTyVar_maybe inner_ki
+      , Just co1 <- liftCoSubstTyVar lc Nominal k
+      = do { let Pair flattened_kind _ = coercionKind co1
+                 (arg_cos, res_co)     = decomposePiCos flattened_kind tys co1
+                 casted_tys            = zipWith mkCastTy tys arg_cos
+                 zapped_lc             = zapLiftingContext lc
+                 (bndrs, new_inner)    = splitPiTys flattened_kind
+
+           ; (xis_out, cos_out, res_co_out)
+               <- go acc_xis acc_cos zapped_lc bndrs new_inner roles casted_tys
+           -- cos_out :: xis_out ~ casted_tys
+           -- we need to return cos :: xis_out ~ tys
+           ; let cos = zipWith mkTcCoherenceRightCo cos_out (map mkTcSymCo arg_cos)
+
+
+           ; return (xis_out, cos, res_co_out `mkTcTransCo` res_co) }
+
+    go _ _ _ _ _ _ _ = pprPanic "flatten_args wandered into deeper water than usual"
+                                     (vcat [ppr orig_binders,
+                                            ppr orig_inner_ki,
+                                            ppr (take 10 orig_roles),  -- often infinite!
+                                            ppr orig_tys])
+
 ------------------
 flatten_one :: TcType -> FlatM (Xi, Coercion)
 -- Flatten a type to get rid of type function applications, returning
@@ -936,32 +1225,7 @@ flatten_one (TyVarTy tv)
   = flattenTyVar tv
 
 flatten_one (AppTy ty1 ty2)
-  = do { (xi1,co1) <- flatten_one ty1
-       ; eq_rel <- getEqRel
-       ; case (eq_rel, nextRole xi1) of
-           -- We need nextRole here because although ty1 definitely
-           -- isn't a TyConApp, xi1 might be.
-           -- ToDo: but can such a substitution change roles??
-           (NomEq,  _)                -> flatten_rhs xi1 co1 NomEq
-           (ReprEq, Nominal)          -> flatten_rhs xi1 co1 NomEq
-           (ReprEq, Representational) -> flatten_rhs xi1 co1 ReprEq
-           (ReprEq, Phantom)          -> -- See Note [Phantoms in the flattener]
-             do { ty2 <- liftTcS $ zonkTcType ty2
-                ; return ( mkAppTy xi1 ty2
-                         , mkAppCo co1 (mkNomReflCo ty2)) } }
-  where
-    flatten_rhs xi1 co1 eq_rel2
-      = do { (xi2,co2) <- setEqRel eq_rel2 $ flatten_one ty2
-           ; role1 <- getRole
-           ; let role2 = eqRelRole eq_rel2
-           ; traceFlat "flatten/appty"
-                       (ppr ty1 $$ ppr ty2 $$ ppr xi1 $$
-                        ppr xi2 $$ ppr role1 $$ ppr role2)
-
-           ; return ( mkAppTy xi1 xi2
-                    , mkTransAppCo role1 co1 xi1 ty1
-                                   role2 co2 xi2 ty2
-                                   role1 ) }  -- output should match fmode
+  = flatten_app_tys ty1 [ty2]
 
 flatten_one (TyConApp tc tys)
   -- Expand type synonyms that mention type families
@@ -1019,88 +1283,90 @@ flatten_one (CastTy ty g)
 
 flatten_one (CoercionTy co) = first mkCoercionTy <$> flatten_co co
 
--- | "Flatten" a coercion. Really, just flatten the types that it coerces
--- between and then use transitivity. See Note [Flattening coercions]
+-- | "Flatten" a coercion. Really, just zonk it so we can uphold
+-- (F1) of Note [Flattening]
 flatten_co :: Coercion -> FlatM (Coercion, Coercion)
 flatten_co co
-  = do { co <- liftTcS $ zonkCo co  -- see Note [Zonking when flattening a coercion]
-       ; let (Pair ty1 ty2, role) = coercionKindRole co
-       ; (co1, co2) <- flattenKinds $
-                       do { (_, co1) <- flatten_one ty1
-                          ; (_, co2) <- flatten_one ty2
-                          ; return (co1, co2) }
-       ; let co' = downgradeRole role Nominal co1 `mkTransCo`
-                   co `mkTransCo`
-                   mkSymCo (downgradeRole role Nominal co2)
-             -- kco :: (ty1' ~r ty2') ~N (ty1 ~r ty2)
-             kco = mkTyConAppCo Nominal (equalityTyCon role)
-                     [ mkKindCo co1, mkKindCo co2, co1, co2 ]
-       ; traceFlat "flatten_co" (vcat [ ppr co, ppr co1, ppr co2, ppr co' ])
+  = do { co <- liftTcS $ zonkCo co
        ; env_role <- getRole
-       ; return (co', mkProofIrrelCo env_role kco co' co) }
+       ; return (co, mkTcReflCo env_role (mkCoercionTy co)) }
+
+-- flatten (nested) AppTys
+flatten_app_tys :: Type -> [Type] -> FlatM (Xi, Coercion)
+-- commoning up nested applications allows us to look up the function's kind
+-- only once. Without commoning up like this, we would spend a quadratic amount
+-- of time looking up functions' types
+flatten_app_tys (AppTy ty1 ty2) tys = flatten_app_tys ty1 (ty2:tys)
+flatten_app_tys fun_ty arg_tys
+  = do { (fun_xi, fun_co) <- flatten_one fun_ty
+       ; flatten_app_ty_args fun_xi fun_co arg_tys }
+
+-- Given a flattened function (with the coercion produced by flattening) and
+-- a bunch of unflattened arguments, flatten the arguments and apply
+flatten_app_ty_args :: Xi -> Coercion -> [Type] -> FlatM (Xi, Coercion)
+flatten_app_ty_args fun_xi fun_co []
+  -- this will be a common case when called from flatten_fam_app, so shortcut
+  = return (fun_xi, fun_co)
+flatten_app_ty_args fun_xi fun_co arg_tys
+  = do { (xi, co, kind_co) <- case tcSplitTyConApp_maybe fun_xi of
+           Just (tc, xis) ->
+             do { let tc_roles  = tyConRolesRepresentational tc
+                      arg_roles = dropList xis tc_roles
+                ; (arg_xis, arg_cos, kind_co)
+                    <- flatten_vector (typeKind fun_xi) arg_roles arg_tys
+
+                  -- Here, we have fun_co :: T xi1 xi2 ~ ty
+                  -- and we need to apply fun_co to the arg_cos. The problem is that
+                  -- using mkAppCo is wrong because that function expects its second
+                  -- coercion to be Nominal, and the arg_cos might not be. The solution
+                  -- is to use transitivity: T <xi1> <xi2> arg_cos ;; fun_co <arg_tys>
+                ; eq_rel <- getEqRel
+                ; let app_xi = mkTyConApp tc (xis ++ arg_xis)
+                      app_co = case eq_rel of
+                        NomEq  -> mkAppCos fun_co arg_cos
+                        ReprEq -> mkTcTyConAppCo Representational tc
+                                    (zipWith mkReflCo tc_roles xis ++ arg_cos)
+                                  `mkTcTransCo`
+                                  mkAppCos fun_co (map mkNomReflCo arg_tys)
+                ; return (app_xi, app_co, kind_co) }
+           Nothing ->
+             do { (arg_xis, arg_cos, kind_co)
+                    <- flatten_vector (typeKind fun_xi) (repeat Nominal) arg_tys
+                ; return (mkAppTys fun_xi arg_xis, mkAppCos fun_co arg_cos, kind_co) }
+
+       ; return (homogenise_result xi co kind_co) }
 
 flatten_ty_con_app :: TyCon -> [TcType] -> FlatM (Xi, Coercion)
 flatten_ty_con_app tc tys
+  = do { role <- getRole
+       ; (xis, cos, kind_co) <- flatten_args_tc tc (tyConRolesX role tc) tys
+       ; let tyconapp_xi = mkTyConApp tc xis
+             tyconapp_co = mkTyConAppCo role tc cos
+       ; return (homogenise_result tyconapp_xi tyconapp_co kind_co) }
+
+-- Make the result of flattening homogeneous (Note [Flattening] (F2))
+homogenise_result :: Xi              -- a flattened type
+                  -> Coercion        -- :: xi ~ original ty
+                  -> CoercionN       -- kind_co :: typeKind(xi) ~N typeKind(ty)
+                  -> (Xi, Coercion)  -- (xi |> kind_co, (xi |> kind_co) ~ original ty)
+homogenise_result xi co kind_co
+  = (xi `mkCastTy` kind_co, co `mkTcCoherenceLeftCo` kind_co)
+
+-- Flatten a vector (list of arguments).
+flatten_vector :: Kind   -- of the function being applied to these arguments
+               -> [Role] -- If we're flatten w.r.t. ReprEq, what roles do the args have?
+               -> [Type] -- the args to flatten
+               -> FlatM ([Xi], [Coercion], CoercionN)
+flatten_vector ki roles tys
   = do { eq_rel <- getEqRel
-       ; let role = eqRelRole eq_rel
-       ; (xis, cos) <- case eq_rel of
-                         NomEq  -> flatten_many_nom tys
-                         ReprEq -> flatten_many (tyConRolesRepresentational tc) tys
-       ; return (mkTyConApp tc xis, mkTyConAppCo role tc cos) }
+       ; case eq_rel of
+           NomEq  -> flatten_args bndrs inner_ki fvs (repeat Nominal) tys
+           ReprEq -> flatten_args bndrs inner_ki fvs roles            tys }
+  where
+    (bndrs, inner_ki) = tcSplitPiTys ki
+    fvs               = tyCoVarsOfType ki
 
 {-
-Note [Flattening coercions]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Because a flattened type has a flattened kind, we also must "flatten"
-coercions as we walk through a type. Otherwise, the "from" type of
-the coercion might not match the (now flattened) kind of the type
-that it's casting. flatten_co does the work, taking a coercion of
-type (ty1 ~ ty2) and flattening it to have type (fty1 ~ fty2),
-where flatten(ty1) = fty1 and flatten(ty2) = fty2.
-
-In other words:
-
-  If  r1 is a role
-      co :: s ~r1 t
-      flatten_co co = (fco, kco)
-      r2 is the role in the FlatM
-
-  then
-      fco :: fs ~r1 ft
-      fs, ft are flattened types
-      kco :: fco ~r2 co
-
-The second return value of flatten_co is always a ProofIrrelCo. As
-such, it doesn't contain any information the caller doesn't have and
-might not be necessary in whatever comes next.
-
-Note that a flattened coercion might have unzonked metavariables or
-type functions in it -- but its *kind* will not. Instead of just flattening
-the kinds and using mkTransCo, we could actually flatten the coercion
-structurally. But doing so seems harder than simply flattening the types.
-
-Note [Zonking when flattening a coercion]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-The first step in flatten_co (see Note [Flattening coercions]) is to
-zonk the input. This is necessary because we want to ensure the following
-invariants (c.f. the invariants (F1) and (F2) in Note [Flattening])
-  If
-    (co', kco) <- flatten_co co
-  Then
-    (FC1) coercionKind(co') succeeds and produces a fully zonked pair of kinds
-    (FC2) kco :: co' ~ zonk(co)
-We must zonk to ensure (1). This is because fco is built by using mkTransCo
-to build up on the input co. But if the only action that happens during
-flattening ty1 and ty2 is to zonk metavariables, the coercions returned
-(co1 and co2) will be reflexive. The mkTransCo calls will drop the reflexive
-coercions and co' will be the same as co -- with unzonked kinds.
-
-These invariants are necessary to uphold (F1) and (F2) in the CastTy and
-CoercionTy cases.
-
-We zonk right at the beginning to avoid duplicating work when flattening the
-ty1 and ty2.
-
 Note [Flattening synonyms]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 Not expanding synonyms aggressively improves error messages, and
@@ -1151,58 +1417,39 @@ flatten_fam_app :: TyCon -> [TcType] -> FlatM (Xi, Coercion)
 flatten_fam_app tc tys  -- Can be over-saturated
     = ASSERT2( tys `lengthAtLeast` tyConArity tc
              , ppr tc $$ ppr (tyConArity tc) $$ ppr tys)
+
+      do { mode <- getMode
+         ; case mode of
+             { FM_SubstOnly  -> flatten_ty_con_app tc tys
+             ; FM_FlattenAll ->
+
                  -- Type functions are saturated
                  -- The type function might be *over* saturated
                  -- in which case the remaining arguments should
                  -- be dealt with by AppTys
       do { let (tys1, tys_rest) = splitAt (tyConArity tc) tys
-         ; (xi1, co1) <- flatten_exact_fam_app tc tys1
+         ; (xi1, co1) <- flatten_exact_fam_app_fully tc tys1
                -- co1 :: xi1 ~ F tys1
 
-               -- all Nominal roles b/c the tycon is oversaturated
-         ; (xis_rest, cos_rest) <- flatten_many (repeat Nominal) tys_rest
-               -- cos_res :: xis_rest ~ tys_rest
-
-         ; return ( mkAppTys xi1 xis_rest   -- NB mkAppTys: rhs_xi might not be a type variable
-                                            --    cf Trac #5655
-                  , mkAppCos co1 cos_rest
-                            -- (rhs_xi :: F xis) ; (F cos :: F xis ~ F tys)
-                  ) }
-
-flatten_exact_fam_app, flatten_exact_fam_app_fully ::
-  TyCon -> [TcType] -> FlatM (Xi, Coercion)
-
-flatten_exact_fam_app tc tys
-  = do { mode <- getMode
-       ; role <- getRole
-       ; case mode of
-               -- These roles are always going to be Nominal for now,
-               -- but not if #8177 is implemented
-           FM_SubstOnly -> do { let roles = tyConRolesX role tc
-                              ; (xis, cos) <- flatten_many roles tys
-                              ; return ( mkTyConApp tc xis
-                                       , mkTyConAppCo role tc cos ) }
-
-           FM_FlattenAll -> flatten_exact_fam_app_fully tc tys }
-
---       FM_Avoid tv flat_top ->
---         do { (xis, cos) <- flatten_many fmode roles tys
---            ; if flat_top || tv `elemVarSet` tyCoVarsOfTypes xis
---              then flatten_exact_fam_app_fully fmode tc tys
---              else return ( mkTyConApp tc xis
---                          , mkTcTyConAppCo (feRole fmode) tc cos ) }
+         ; flatten_app_ty_args xi1 co1 tys_rest } } }
 
+-- the [TcType] exactly saturate the TyCon
+flatten_exact_fam_app_fully :: TyCon -> [TcType] -> FlatM (Xi, Coercion)
 flatten_exact_fam_app_fully tc tys
   -- See Note [Reduce type family applications eagerly]
-  = try_to_reduce tc tys False id $
+     -- the following typeKind should never be evaluated, as it's just used in
+     -- casting, and casts by refl are dropped
+  = try_to_reduce tc tys (mkNomReflCo (typeKind (mkTyConApp tc tys))) False id $
     do { -- First, flatten the arguments
-       ; (xis, cos) <- setEqRel NomEq    $
-                       flatten_many_nom tys
+       ; (xis, cos, kind_co)
+           <- setEqRel NomEq $  -- just do this once, instead of for each arg
+              flatten_args_tc tc (repeat Nominal) tys
+              -- kind_co :: typeKind(F xis) ~N typeKind(F tys)
        ; eq_rel   <- getEqRel
        ; cur_flav <- getFlavour
        ; let role   = eqRelRole eq_rel
              ret_co = mkTyConAppCo role tc cos
-              -- ret_co :: F xis ~ F tys
+              -- ret_co :: F xis ~ F tys; might be heterogeneous
 
         -- Now, look in the cache
        ; mb_ct <- liftTcS $ lookupFlatCache tc xis
@@ -1216,15 +1463,15 @@ flatten_exact_fam_app_fully tc tys
                    ; (fsk_xi, fsk_co) <- flatten_one rhs_ty
                           -- The fsk may already have been unified, so flatten it
                           -- fsk_co :: fsk_xi ~ fsk
-                   ; return ( fsk_xi
-                            , fsk_co `mkTransCo`
+                   ; return ( fsk_xi `mkCastTy` kind_co
+                            , (fsk_co `mkTcCoherenceLeftCo` kind_co) `mkTransCo`
                               maybeSubCo eq_rel (mkSymCo co) `mkTransCo`
                               ret_co ) }
                                     -- :: fsk_xi ~ F xis
 
            -- Try to reduce the family application right now
            -- See Note [Reduce type family applications eagerly]
-           _ -> try_to_reduce tc xis True (`mkTransCo` ret_co) $
+           _ -> try_to_reduce tc xis kind_co True (`mkTransCo` ret_co) $
                 do { loc <- getLoc
                    ; (ev, co, fsk) <- liftTcS $ newFlattenSkolem cur_flav loc tc xis
 
@@ -1241,22 +1488,27 @@ flatten_exact_fam_app_fully tc tys
 
                    -- NB: fsk's kind is already flattend because
                    --     the xis are flattened
-                   ; return (mkTyVarTy fsk, maybeSubCo eq_rel (mkSymCo co)
-                                            `mkTransCo` ret_co ) }
+                   ; return ( mkTyVarTy fsk `mkCastTy` kind_co
+                            , (maybeSubCo eq_rel (mkSymCo co) `mkTcCoherenceLeftCo` kind_co)
+                              `mkTransCo` ret_co ) }
         }
 
   where
     try_to_reduce :: TyCon   -- F, family tycon
                   -> [Type]  -- args, not necessarily flattened
+                  -> CoercionN -- kind_co :: typeKind(F args) ~N typeKind(F orig_args), where
+                               -- orig_args is what was passed to the outer function
                   -> Bool    -- add to the flat cache?
-                  -> (   Coercion     -- :: xi ~ F args
+                  -> (   Coercion     -- :: (xi |> kind_co) ~ F args
                       -> Coercion )   -- what to return from outer function
                   -> FlatM (Xi, Coercion)  -- continuation upon failure
                   -> FlatM (Xi, Coercion)
-    try_to_reduce tc tys cache update_co k
+    try_to_reduce tc tys kind_co cache update_co k
       = do { checkStackDepth (mkTyConApp tc tys)
            ; mb_match <- liftTcS $ matchFam tc tys
            ; case mb_match of
+                 -- NB: norm_co will always be homogeneous. All type families
+                 -- are homogeneous.
                Just (norm_co, norm_ty)
                  -> do { traceFlat "Eager T.F. reduction success" $
                          vcat [ ppr tc, ppr tys, ppr norm_ty
@@ -1272,7 +1524,8 @@ flatten_exact_fam_app_fully tc tys
                        ; when (cache && eq_rel == NomEq) $
                          liftTcS $
                          extendFlatCache tc tys ( co, xi, flavour )
-                       ; return ( xi, update_co $ mkSymCo co ) }
+                       ; return ( xi `mkCastTy` kind_co
+                                , update_co $ (mkSymCo co `mkTcCoherenceLeftCo` kind_co) ) }
                Nothing -> k }
 
 {- Note [Reduce type family applications eagerly]
@@ -1341,27 +1594,12 @@ flattenTyVar tv
                    -- ; traceFlat "flattenTyVar2" (ppr tv $$ ppr ty2)
                    ; return (ty2, co2 `mkTransCo` co1) }
 
-           FTRNotFollowed   -- Done
-             -> do { let orig_kind = tyVarKind tv
-                   ; (_new_kind, kind_co) <- flattenKinds $
-                                             flatten_one orig_kind
-                   ; 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.
-             -- Moreover the returned Xi type must be well-kinded
-             -- (e.g. in canEqTyVarTyVar we use getCastedTyVar_maybe)
-             -- If you remove it, then e.g. dependent/should_fail/T11407 panics
-             -- 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
-
+           FTRNotFollowed   -- Done, but make sure the kind is zonked
+                            -- Note [Flattening] invariant (F1)
+             -> do { tv' <- liftTcS $ updateTyVarKindM zonkTcType tv
                    ; role <- getRole
-                   ; return (ty', mkReflCo role tv_ty'
-                                  `mkCoherenceLeftCo` mkSymCo kind_co) } }
+                   ; let ty' = mkTyVarTy tv'
+                   ; return (ty', mkTcReflCo role ty') } }
 
 flatten_tyvar1 :: TcTyVar -> FlatM FlattenTvResult
 -- "Flattening" a type variable means to apply the substitution to it
diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs
index d0bcddf19f..c724333ddd 100644
--- a/compiler/typecheck/TcInteract.hs
+++ b/compiler/typecheck/TcInteract.hs
@@ -1597,7 +1597,7 @@ interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv
        ; if canSolveByUnification tclvl tv rhs
          then do { solveByUnification ev tv rhs
                  ; n_kicked <- kickOutAfterUnification tv
-                 ; return (Stop ev (text "Solved by unification" <+> ppr_kicked n_kicked)) }
+                 ; return (Stop ev (text "Solved by unification" <+> pprKicked n_kicked)) }
 
          else unsolved_inert }
 
@@ -1640,10 +1640,6 @@ solveByUnification wd tv xi
        ; unifyTyVar tv xi
        ; setEvBindIfWanted wd (evCoercion (mkTcNomReflCo xi)) }
 
-ppr_kicked :: Int -> SDoc
-ppr_kicked 0 = empty
-ppr_kicked n = parens (int n <+> text "kicked out")
-
 {- Note [Avoid double unifications]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 The spontaneous solver has to return a given which mentions the unified unification
@@ -1961,59 +1957,34 @@ improve_top_fun_eqs fam_envs fam_tc args rhs_ty
 shortCutReduction :: CtEvidence -> TcTyVar -> TcCoercion
                   -> TyCon -> [TcType] -> TcS (StopOrContinue Ct)
 -- See Note [Top-level reductions for type functions]
+-- Previously, we flattened the tc_args here, but there's no need to do so.
+-- And, if we did, this function would have all the complication of
+-- TcCanonical.canCFunEqCan. See Note [canCFunEqCan]
 shortCutReduction old_ev fsk ax_co fam_tc tc_args
   = ASSERT( ctEvEqRel old_ev == NomEq)
-    do { (xis, cos) <- flattenManyNom old_ev tc_args
                -- ax_co :: F args ~ G tc_args
-               -- cos   :: xis ~ tc_args
                -- old_ev :: F args ~ fsk
-               -- G cos ; sym ax_co ; old_ev :: G xis ~ fsk
-
-       ; new_ev <- case ctEvFlavour old_ev of
+    do { new_ev <- case ctEvFlavour old_ev of
            Given -> newGivenEvVar deeper_loc
-                         ( mkPrimEqPred (mkTyConApp fam_tc xis) (mkTyVarTy fsk)
-                         , evCoercion (mkTcTyConAppCo Nominal fam_tc cos
-                                        `mkTcTransCo` mkTcSymCo ax_co
-                                        `mkTcTransCo` ctEvCoercion old_ev) )
+                         ( mkPrimEqPred (mkTyConApp fam_tc tc_args) (mkTyVarTy fsk)
+                         , evCoercion (mkTcSymCo ax_co
+                                       `mkTcTransCo` ctEvCoercion old_ev) )
 
            Wanted {} ->
              do { (new_ev, new_co) <- newWantedEq deeper_loc Nominal
-                                        (mkTyConApp fam_tc xis) (mkTyVarTy fsk)
-                ; setWantedEq (ctev_dest old_ev) $
-                     ax_co `mkTcTransCo` mkTcSymCo (mkTcTyConAppCo Nominal
-                                                      fam_tc cos)
-                           `mkTcTransCo` new_co
+                                        (mkTyConApp fam_tc tc_args) (mkTyVarTy fsk)
+                ; setWantedEq (ctev_dest old_ev) $ ax_co `mkTcTransCo` new_co
                 ; return new_ev }
 
            Derived -> pprPanic "shortCutReduction" (ppr old_ev)
 
        ; let new_ct = CFunEqCan { cc_ev = new_ev, cc_fun = fam_tc
-                                , cc_tyargs = xis, cc_fsk = fsk }
+                                , cc_tyargs = tc_args, cc_fsk = fsk }
        ; updWorkListTcS (extendWorkListFunEq new_ct)
        ; stopWith old_ev "Fun/Top (shortcut)" }
   where
     deeper_loc = bumpCtLocDepth (ctEvLoc old_ev)
 
-dischargeFmv :: CtEvidence -> TcTyVar -> TcCoercion -> TcType -> TcS ()
--- (dischargeFmv x fmv co ty)
---     [W] ev :: F tys ~ fmv
---         co :: F tys ~ xi
--- Precondition: fmv is not filled, and fmv `notElem` xi
---               ev is Wanted
---
--- Then set fmv := xi,
---      set ev  := co
---      kick out any inert things that are now rewritable
---
--- Does not evaluate 'co' if 'ev' is Derived
-dischargeFmv ev@(CtWanted { ctev_dest = dest }) fmv co xi
-  = ASSERT2( not (fmv `elemVarSet` tyCoVarsOfType xi), ppr ev $$ ppr fmv $$ ppr xi )
-    do { setWantedEvTerm dest (EvExpr (evCoercion co))
-       ; unflattenFmv fmv xi
-       ; n_kicked <- kickOutAfterUnification fmv
-       ; traceTcS "dischargeFmv" (ppr fmv <+> equals <+> ppr xi $$ ppr_kicked n_kicked) }
-dischargeFmv ev _ _ _ = pprPanic "dischargeFmv" (ppr ev)
-
 {- Note [Top-level reductions for type functions]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 c.f. Note [The flattening story] in TcFlatten
diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs
index 4de99b522f..8f74f55c03 100644
--- a/compiler/typecheck/TcMType.hs
+++ b/compiler/typecheck/TcMType.hs
@@ -697,9 +697,11 @@ writeMetaTyVarRef tyvar ref ty
   = do { meta_details <- readMutVar ref;
        -- Zonk kinds to allow the error check to work
        ; zonked_tv_kind <- zonkTcType tv_kind
-       ; zonked_ty_kind <- zonkTcType ty_kind
-       ; let kind_check_ok = isPredTy tv_kind  -- Don't check kinds for updates
-                                               -- to coercion variables.  Why not??
+       ; zonked_ty      <- zonkTcType ty
+       ; let zonked_ty_kind = typeKind zonked_ty  -- need to zonk even before typeKind;
+                                                  -- otherwise, we can panic in piResultTy
+             kind_check_ok = isPredTy tv_kind  -- Don't check kinds for updates
+                                               -- to coercion variables. TODO (RAE): Why not?
                           || isConstraintKind zonked_tv_kind
                           || tcEqKind zonked_ty_kind zonked_tv_kind
              -- Hack alert! isConstraintKind: see TcHsType
@@ -708,7 +710,7 @@ writeMetaTyVarRef tyvar ref ty
              kind_msg = hang (text "Ill-kinded update to meta tyvar")
                            2 (    ppr tyvar <+> text "::" <+> (ppr tv_kind $$ ppr zonked_tv_kind)
                               <+> text ":="
-                              <+> ppr ty <+> text "::" <+> (ppr ty_kind $$ ppr zonked_ty_kind) )
+                              <+> ppr ty <+> text "::" <+> (ppr zonked_ty_kind) )
 
        ; traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
 
@@ -726,7 +728,6 @@ writeMetaTyVarRef tyvar ref ty
        ; writeMutVar ref (Indirect ty) }
   where
     tv_kind = tyVarKind tyvar
-    ty_kind = typeKind ty
 
     tv_lvl = tcTyVarLevel tyvar
     ty_lvl = tcTypeLevel ty
diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs
index 00c2256fe0..f66077de0e 100644
--- a/compiler/typecheck/TcRnTypes.hs
+++ b/compiler/typecheck/TcRnTypes.hs
@@ -2648,15 +2648,6 @@ For Givens we make new EvVars and bind them immediately. Two main reasons:
 
 So a Given has EvVar inside it rather than (as previously) an EvTerm.
 
-Note [Given in ctEvCoercion]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-When retrieving the evidence from a Given equality, we update the type of the EvVar
-from the ctev_pred field. In Note [Evidence field of CtEvidence], we claim that
-the type of the evidence is never looked at -- but this isn't true in the case of
-a coercion that is used in a type. (See the comments in Note [Flattening] in TcFlatten
-about the FTRNotFollowed case of flattenTyVar.) So, right here where we are retrieving
-the coercion from a Given, we update the type to make sure it's zonked.
-
 -}
 
 -- | A place for type-checking evidence to go after it is generated.
@@ -2713,11 +2704,9 @@ ctEvExpr :: CtEvidence -> EvExpr
 ctEvExpr ev@(CtWanted { ctev_dest = HoleDest _ }) = evCoercion $ ctEvCoercion ev
 ctEvExpr ev = evId (ctEvEvId ev)
 
--- Always returns a coercion whose type is precisely ctev_pred of the CtEvidence.
--- See also Note [Given in ctEvCoercion]
 ctEvCoercion :: CtEvidence -> Coercion
-ctEvCoercion (CtGiven { ctev_pred = pred_ty, ctev_evar = ev_id })
-  = mkTcCoVarCo (setVarType ev_id pred_ty)  -- See Note [Given in ctEvCoercion]
+ctEvCoercion (CtGiven { ctev_evar = ev_id })
+  = mkTcCoVarCo ev_id
 ctEvCoercion (CtWanted { ctev_dest = dest })
   | HoleDest hole <- dest
   = -- ctEvCoercion is only called on type equalities
diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs
index 0db75095f1..c89a1976bd 100644
--- a/compiler/typecheck/TcSMonad.hs
+++ b/compiler/typecheck/TcSMonad.hs
@@ -82,6 +82,7 @@ module TcSMonad (
 
     -- The flattening cache
     lookupFlatCache, extendFlatCache, newFlattenSkolem,            -- Flatten skolems
+    dischargeFmv, pprKicked,
 
     -- Inert CFunEqCans
     updInertFunEqs, findFunEq,
@@ -1134,8 +1135,78 @@ work?
   because even tyvars in the casts and coercions could give
   an infinite loop if we don't expose it
 
+* CIrredCan: Yes if the inert set can rewrite the constraint.
+  We used to think splitting irreds was unnecessary, but
+  see Note [Splitting Irred WD constraints]
+
 * Others: nothing is gained by splitting.
 
+Note [Splitting Irred WD constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Splitting Irred constraints can make a difference. Here is the
+scenario:
+
+  a[sk] :: F v     -- F is a type family
+  beta :: alpha
+
+  work item: [WD] a ~ beta
+
+This is heterogeneous, so we try flattening the kinds.
+
+  co :: F v ~ fmv
+  [WD] (a |> co) ~ beta
+
+This is still hetero, so we emit a kind equality and make the work item an
+inert Irred.
+
+  work item: [D] fmv ~ alpha
+  inert: [WD] (a |> co) ~ beta (CIrredCan)
+
+Can't make progress on the work item. Add to inert set. This kicks out the
+old inert, because a [D] can rewrite a [WD].
+
+  work item: [WD] (a |> co) ~ beta
+  inert: [D] fmv ~ alpha (CTyEqCan)
+
+Can't make progress on this work item either (although GHC tries by
+decomposing the cast and reflattening... but that doesn't make a difference),
+which is still hetero. Emit a new kind equality and add to inert set. But,
+critically, we split the Irred.
+
+  work list:
+   [D] fmv ~ alpha (CTyEqCan)
+   [D] (a |> co) ~ beta (CIrred) -- this one was split off
+  inert:
+   [W] (a |> co) ~ beta
+   [D] fmv ~ alpha
+
+We quickly solve the first work item, as it's the same as an inert.
+
+  work item: [D] (a |> co) ~ beta
+  inert:
+   [W] (a |> co) ~ beta
+   [D] fmv ~ alpha
+
+We decompose the cast, yielding
+
+  [D] a ~ beta
+
+We then flatten the kinds. The lhs kind is F v, which flattens to fmv which
+then rewrites to alpha.
+
+  co' :: F v ~ alpha
+  [D] (a |> co') ~ beta
+
+Now this equality is homo-kinded. So we swizzle it around to
+
+  [D] beta ~ (a |> co')
+
+and set beta := a |> co', and go home happy.
+
+If we don't split the Irreds, we loop. This is all dangerously subtle.
+
+This is triggered by test case typecheck/should_compile/SplitWD.
+
 Note [Examples of how Derived shadows helps completeness]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Trac #10009, a very nasty example:
@@ -1298,7 +1369,9 @@ shouldSplitWD inert_eqs (CTyEqCan { cc_tyvar = tv, cc_rhs = ty
   || anyRewritableTyVar False eq_rel (canRewriteTv inert_eqs) ty
   -- NB False: do not ignore casts and coercions
   -- See Note [Splitting WD constraints]
-  where
+
+shouldSplitWD inert_eqs (CIrredCan { cc_ev = ev })
+  = anyRewritableTyVar False (ctEvEqRel ev) (canRewriteTv inert_eqs) (ctEvPred ev)
 
 shouldSplitWD _ _ = False   -- No point in splitting otherwise
 
@@ -2954,6 +3027,30 @@ demoteUnfilledFmv fmv
                    do { tv_ty <- TcM.newFlexiTyVarTy (tyVarKind fmv)
                       ; TcM.writeMetaTyVar fmv tv_ty } }
 
+-----------------------------
+dischargeFmv :: CtEvidence -> TcTyVar -> TcCoercion -> TcType -> TcS ()
+-- (dischargeFmv x fmv co ty)
+--     [W] ev :: F tys ~ fmv
+--         co :: F tys ~ xi
+-- Precondition: fmv is not filled, and fmv `notElem` xi
+--               ev is Wanted
+--
+-- Then set fmv := xi,
+--      set ev  := co
+--      kick out any inert things that are now rewritable
+--
+-- Does not evaluate 'co' if 'ev' is Derived
+dischargeFmv ev@(CtWanted { ctev_dest = dest }) fmv co xi
+  = ASSERT2( not (fmv `elemVarSet` tyCoVarsOfType xi), ppr ev $$ ppr fmv $$ ppr xi )
+    do { setWantedEvTerm dest (EvExpr (evCoercion co))
+       ; unflattenFmv fmv xi
+       ; n_kicked <- kickOutAfterUnification fmv
+       ; traceTcS "dischargeFmv" (ppr fmv <+> equals <+> ppr xi $$ pprKicked n_kicked) }
+dischargeFmv ev _ _ _ = pprPanic "dischargeFmv" (ppr ev)
+
+pprKicked :: Int -> SDoc
+pprKicked 0 = empty
+pprKicked n = parens (int n <+> text "kicked out")
 
 {- *********************************************************************
 *                                                                      *
@@ -3212,4 +3309,3 @@ from which we get the implication
    (forall a. t1 ~ t2)
 See TcSMonad.deferTcSForAllEq
 -}
-
diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index d378fcb85c..f15f704f70 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -68,7 +68,7 @@ module TcType (
   tcTyConAppTyCon, tcTyConAppTyCon_maybe, tcTyConAppArgs,
   tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, tcRepSplitAppTy_maybe,
   tcRepGetNumAppTys,
-  tcGetCastedTyVar_maybe, tcGetTyVar_maybe, tcGetTyVar, nextRole,
+  tcGetCastedTyVar_maybe, tcGetTyVar_maybe, tcGetTyVar,
   tcSplitSigmaTy, tcSplitNestedSigmaTys, tcDeepSplitSigmaTy_maybe,
 
   ---------------------------------
diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs
index 7a7918c250..af984752d9 100644
--- a/compiler/types/Coercion.hs
+++ b/compiler/types/Coercion.hs
@@ -28,7 +28,7 @@ module Coercion (
         mkAxInstRHS, mkUnbranchedAxInstRHS,
         mkAxInstLHS, mkUnbranchedAxInstLHS,
         mkPiCo, mkPiCos, mkCoCast,
-        mkSymCo, mkTransCo, mkTransAppCo,
+        mkSymCo, mkTransCo,
         mkNthCo, mkLRCo,
         mkInstCo, mkAppCo, mkAppCos, mkTyConAppCo, mkFunCo, mkFunCos,
         mkForAllCo, mkForAllCos, mkHomoForAllCos, mkHomoForAllCos_NoRefl,
@@ -48,7 +48,7 @@ module Coercion (
         mapStepResult, unwrapNewTypeStepper,
         topNormaliseNewType_maybe, topNormaliseTypeX,
 
-        decomposeCo, decomposeFunCo, getCoVar_maybe,
+        decomposeCo, decomposeFunCo, decomposePiCos, getCoVar_maybe,
         splitTyConAppCo_maybe,
         splitAppCo_maybe,
         splitFunCo_maybe,
@@ -79,7 +79,7 @@ module Coercion (
 
         -- ** Lifting
         liftCoSubst, liftCoSubstTyVar, liftCoSubstWith, liftCoSubstWithEx,
-        emptyLiftingContext, extendLiftingContext,
+        emptyLiftingContext, extendLiftingContext, extendLiftingContextAndInScope,
         liftCoSubstVarBndrCallback, isMappedByLC,
 
         mkSubstLiftingContext, zapLiftingContext,
@@ -102,7 +102,7 @@ module Coercion (
         tidyCo, tidyCos,
 
         -- * Other
-        promoteCoercion
+        promoteCoercion, buildCoercion
        ) where
 
 #include "HsVersions.h"
@@ -115,6 +115,7 @@ import TyCon
 import CoAxiom
 import Var
 import VarEnv
+import VarSet
 import Name hiding ( varName )
 import Util
 import BasicTypes
@@ -244,6 +245,64 @@ decomposeFunCo co = ASSERT2( all_ok, ppr co )
     Pair s1t1 s2t2 = coercionKind co
     all_ok = isFunTy s1t1 && isFunTy s2t2
 
+-- | Decompose a function coercion, either a dependent one or a non-dependent one.
+-- This is useful when you are trying to build (ty1 |> co) ty2 ty3 ... tyn, but
+-- you are pulling the coercions to the right. For example of why you might want
+-- to do so, see Note [Respecting definitional equality] in TyCoRep.
+-- This might return *fewer* coercions than there are arguments, if the kind provided
+-- doesn't have enough binders.
+-- The types passed in are the ty2 ... tyn. If the results are (arg_cos, res_co),
+-- then you should build
+-- @(ty1 (ty2 |> arg_cos1) (ty3 |> arg_cos2) ... (tym |> arg_com)|> res_co) tym+1 ... tyn@.
+decomposePiCos :: Kind  -- of the function (ty1), used only to tell -> from ∀ from other
+               -> [Type] -> CoercionN -> ([CoercionN], CoercionN)
+decomposePiCos orig_kind orig_args orig_co = go [] orig_subst orig_kind orig_args orig_co
+  where
+    orig_subst = mkEmptyTCvSubst $ mkInScopeSet $ tyCoVarsOfTypes (orig_kind : orig_args)
+                                                  `unionVarSet` tyCoVarsOfCo orig_co
+
+    go :: [CoercionN]   -- accumulator for argument coercions, reversed
+       -> TCvSubst      -- instantiating substitution
+       -> Kind          -- of the function being applied (unsubsted)
+       -> [Type]        -- arguments to that function
+       -> CoercionN     -- coercion originally applied to the function
+       -> ([CoercionN], Coercion)
+    go acc_arg_cos subst  ki  (ty:tys) co
+      | Just (kv, inner_ki) <- splitForAllTy_maybe ki
+        -- know     co :: (forall a:s1.t1) ~ (forall b:s2.t2)
+        --    function :: forall a:s1.t1   (the function is not passed to decomposePiCos)
+        --          ty :: s2
+        -- need arg_co :: s2 ~ s1
+        --      res_co :: t1[ty |> arg_co / a] ~ t2[ty / b]
+      = let arg_co = mkNthCo 0 (mkSymCo co)
+            res_co = mkInstCo co (mkNomReflCo ty `mkCoherenceLeftCo` arg_co)
+            subst' = extendTCvSubst subst kv ty
+        in
+        go (arg_co : acc_arg_cos) subst' inner_ki tys res_co
+
+      | Just (_arg_ki, res_ki) <- splitFunTy_maybe ki
+        -- know     co :: (s1 -> t1) ~ (s2 -> t2)
+        --    function :: s1 -> t1
+        --          ty :: s2
+        -- need arg_co :: s2 ~ s1
+        --      res_co :: t1 ~ t2
+      = let (sym_arg_co, res_co) = decomposeFunCo co
+            arg_co               = mkSymCo sym_arg_co
+        in
+        go (arg_co : acc_arg_cos) subst res_ki tys res_co
+
+      | let substed_ki = substTy subst ki
+      , isPiTy substed_ki
+        -- This might happen if we have to substitute in order to see that the kind
+        -- is a Π-type.
+      = let subst'     = zapTCvSubst subst
+        in
+        go acc_arg_cos subst' substed_ki (ty:tys) co
+
+      -- tys might not be empty, if the left-hand type of the original coercion
+      -- didn't have enough binders
+    go acc_arg_cos _subst _ki _tys co = (reverse acc_arg_cos, co)
+
 -- | Attempts to obtain the type variable underlying a 'Coercion'
 getCoVar_maybe :: Coercion -> Maybe CoVar
 getCoVar_maybe (CoVarCo cv) = Just cv
@@ -449,41 +508,6 @@ One might ask: shouldn't downgradeRole_maybe just use setNominalRole_maybe as
 appropriate? I (Richard E.) have decided not to do this, because upgrading a
 role is bizarre and a caller should have to ask for this behavior explicitly.
 
-Note [mkTransAppCo]
-~~~~~~~~~~~~~~~~~~~
-Suppose we have
-
-  co1 :: a ~R Maybe
-  co2 :: b ~R Int
-
-and we want
-
-  co3 :: a b ~R Maybe Int
-
-This seems sensible enough. But, we can't let (co3 = co1 co2), because
-that's ill-roled! Note that mkAppCo requires a *nominal* second coercion.
-
-The way around this is to use transitivity:
-
-  co3 = (co1 <b>_N) ; (Maybe co2) :: a b ~R Maybe Int
-
-Or, it's possible everything is the other way around:
-
-  co1' :: Maybe ~R a
-  co2' :: Int   ~R b
-
-and we want
-
-  co3' :: Maybe Int ~R a b
-
-then
-
-  co3' = (Maybe co2') ; (co1' <b>_N)
-
-This is exactly what `mkTransAppCo` builds for us. Information for all
-the arguments tends to be to hand at call sites, so it's quicker than
-using, say, coercionKind.
-
 -}
 
 mkReflCo :: Role -> Type -> Coercion
@@ -569,68 +593,6 @@ mkAppCos :: Coercion
          -> Coercion
 mkAppCos co1 cos = foldl mkAppCo co1 cos
 
--- | Like `mkAppCo`, but allows the second coercion to be other than
--- nominal. See Note [mkTransAppCo]. Role r3 cannot be more stringent
--- than either r1 or r2.
-mkTransAppCo :: Role         -- ^ r1
-             -> Coercion     -- ^ co1 :: ty1a ~r1 ty1b
-             -> Type         -- ^ ty1a
-             -> Type         -- ^ ty1b
-             -> Role         -- ^ r2
-             -> Coercion     -- ^ co2 :: ty2a ~r2 ty2b
-             -> Type         -- ^ ty2a
-             -> Type         -- ^ ty2b
-             -> Role         -- ^ r3
-             -> Coercion     -- ^ :: ty1a ty2a ~r3 ty1b ty2b
-mkTransAppCo r1 co1 ty1a ty1b r2 co2 ty2a ty2b r3
--- How incredibly fiddly! Is there a better way??
-  = case (r1, r2, r3) of
-      (_,                _,                Phantom)
-        -> mkPhantomCo kind_co (mkAppTy ty1a ty2a) (mkAppTy ty1b ty2b)
-        where -- ty1a :: k1a -> k2a
-              -- ty1b :: k1b -> k2b
-              -- ty2a :: k1a
-              -- ty2b :: k1b
-              -- ty1a ty2a :: k2a
-              -- ty1b ty2b :: k2b
-              kind_co1 = mkKindCo co1        -- :: k1a -> k2a ~N k1b -> k2b
-              kind_co  = mkNthCo 1 kind_co1  -- :: k2a ~N k2b
-
-      (_,                _,                Nominal)
-        -> ASSERT( r1 == Nominal && r2 == Nominal )
-           mkAppCo co1 co2
-      (Nominal,          Nominal,          Representational)
-        -> mkSubCo (mkAppCo co1 co2)
-      (_,                Nominal,          Representational)
-        -> ASSERT( r1 == Representational )
-           mkAppCo co1 co2
-      (Nominal,          Representational, Representational)
-        -> go (mkSubCo co1)
-      (_               , _,                Representational)
-        -> ASSERT( r1 == Representational && r2 == Representational )
-           go co1
-  where
-    go co1_repr
-      | Just (tc1b, tys1b) <- splitTyConApp_maybe ty1b
-      , nextRole ty1b == r2
-      = (mkAppCo co1_repr (mkNomReflCo ty2a)) `mkTransCo`
-        (mkTyConAppCo Representational tc1b
-           (zipWith mkReflCo (tyConRolesRepresentational tc1b) tys1b
-            ++ [co2]))
-
-      | Just (tc1a, tys1a) <- splitTyConApp_maybe ty1a
-      , nextRole ty1a == r2
-      = (mkTyConAppCo Representational tc1a
-           (zipWith mkReflCo (tyConRolesRepresentational tc1a) tys1a
-            ++ [co2]))
-        `mkTransCo`
-        (mkAppCo co1_repr (mkNomReflCo ty2b))
-
-      | otherwise
-      = pprPanic "mkTransAppCo" (vcat [ ppr r1, ppr co1, ppr ty1a, ppr ty1b
-                                      , ppr r2, ppr co2, ppr ty2a, ppr ty2b
-                                      , ppr r3 ])
-
 -- | Make a Coercion from a tyvar, a kind coercion, and a body coercion.
 -- The kind of the tyvar should be the left-hand kind of the kind coercion.
 mkForAllCo :: TyVar -> Coercion -> Coercion -> Coercion
@@ -1444,10 +1406,20 @@ extendLiftingContext :: LiftingContext  -- ^ original LC
                      -> TyVar           -- ^ new variable to map...
                      -> Coercion        -- ^ ...to this lifted version
                      -> LiftingContext
+    -- mappings to reflexive coercions are just substitutions
+extendLiftingContext (LC subst env) tv (Refl _ ty) = LC (extendTvSubst subst tv ty) env
 extendLiftingContext (LC subst env) tv arg
   = ASSERT( isTyVar tv )
     LC subst (extendVarEnv env tv arg)
 
+-- | Extend a lifting context with a new mapping, and extend the in-scope set
+extendLiftingContextAndInScope :: LiftingContext  -- ^ Original LC
+                               -> TyVar           -- ^ new variable to map...
+                               -> Coercion        -- ^ to this coercion
+                               -> LiftingContext
+extendLiftingContextAndInScope (LC subst env) tv co
+  = extendLiftingContext (LC (extendTCvInScopeSet subst (tyCoVarsOfCo co)) env) tv co
+
 -- | Extend a lifting context with existential-variable bindings.
 -- This follows the lifting context extension definition in the
 -- "FC with Explicit Kind Equality" paper.
@@ -1880,3 +1852,64 @@ So it's very important to do the substitution simultaneously;
 cf Type.piResultTys (which in fact we call here).
 
 -}
+
+-- | Assuming that two types are the same, ignoring coercions, find
+-- a nominal coercion between the types. This is useful when optimizing
+-- transitivity over coercion applications, where splitting two
+-- AppCos might yield different kinds. See Note [EtaAppCo] in OptCoercion.
+buildCoercion :: Type -> Type -> CoercionN
+buildCoercion orig_ty1 orig_ty2 = go orig_ty1 orig_ty2
+  where
+    go ty1 ty2 | Just ty1' <- coreView ty1 = go ty1' ty2
+               | Just ty2' <- coreView ty2 = go ty1 ty2'
+
+    go (CastTy ty1 co) ty2
+      = go ty1 ty2 `mkCoherenceLeftCo` co
+
+    go ty1 (CastTy ty2 co)
+      = go ty1 ty2 `mkCoherenceRightCo` co
+
+    go ty1@(TyVarTy tv1) _tyvarty
+      = ASSERT( case _tyvarty of
+                  { TyVarTy tv2 -> tv1 == tv2
+                  ; _           -> False      } )
+        mkNomReflCo ty1
+
+    go (FunTy arg1 res1) (FunTy arg2 res2)
+      = mkFunCo Nominal (go arg1 arg2) (go res1 res2)
+
+    go (TyConApp tc1 args1) (TyConApp tc2 args2)
+      = ASSERT( tc1 == tc2 )
+        mkTyConAppCo Nominal tc1 (zipWith go args1 args2)
+
+    go (AppTy ty1a ty1b) ty2
+      | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2
+      = mkAppCo (go ty1a ty2a) (go ty1b ty2b)
+
+    go ty1 (AppTy ty2a ty2b)
+      | Just (ty1a, ty1b) <- repSplitAppTy_maybe ty1
+      = mkAppCo (go ty1a ty2a) (go ty1b ty2b)
+
+    go (ForAllTy (TvBndr tv1 _flag1) ty1) (ForAllTy (TvBndr tv2 _flag2) ty2)
+      = let kind_co  = go (tyVarKind tv1) (tyVarKind tv2)
+            in_scope = mkInScopeSet $ tyCoVarsOfType ty2 `unionVarSet` tyCoVarsOfCo kind_co
+            ty2'     = substTyWithInScope in_scope [tv2]
+                                                   [mkTyVarTy tv1 `mkCastTy` kind_co]
+                                                   ty2
+        in
+        mkForAllCo tv1 kind_co (go ty1 ty2')
+
+    go ty1@(LitTy lit1) _lit2
+      = ASSERT( case _lit2 of
+                  { LitTy lit2 -> lit1 == lit2
+                  ; _          -> False        } )
+        mkNomReflCo ty1
+
+    go (CoercionTy co1) (CoercionTy co2)
+      = mkProofIrrelCo Nominal kind_co co1 co2
+      where
+        kind_co = go (coercionType co1) (coercionType co2)
+
+    go ty1 ty2
+      = pprPanic "buildKindCoercion" (vcat [ ppr orig_ty1, ppr orig_ty2
+                                           , ppr ty1, ppr ty2 ])
diff --git a/compiler/types/Coercion.hs-boot b/compiler/types/Coercion.hs-boot
index 2eed58038c..1508e6fb10 100644
--- a/compiler/types/Coercion.hs-boot
+++ b/compiler/types/Coercion.hs-boot
@@ -37,6 +37,7 @@ mkFunCos :: Role -> [Coercion] -> Coercion -> Coercion
 
 isReflCo :: Coercion -> Bool
 isReflexiveCo :: Coercion -> Bool
+decomposePiCos :: Kind -> [Type] -> Coercion -> ([Coercion], Coercion)
 coVarKindsTypesRole :: CoVar -> (Kind, Kind, Type, Type, Role)
 coVarRole :: CoVar -> Role
 
diff --git a/compiler/types/OptCoercion.hs b/compiler/types/OptCoercion.hs
index 24dc8a4344..11aeb932cc 100644
--- a/compiler/types/OptCoercion.hs
+++ b/compiler/types/OptCoercion.hs
@@ -93,8 +93,8 @@ optCoercion env co
         (Pair in_ty1  in_ty2,  in_role)  = coercionKindRole co
         (Pair out_ty1 out_ty2, out_role) = coercionKindRole out_co
     in
-    ASSERT2( substTyUnchecked env in_ty1 `eqType` out_ty1 &&
-             substTyUnchecked env in_ty2 `eqType` out_ty2 &&
+    ASSERT2( substTy env in_ty1 `eqType` out_ty1 &&
+             substTy env in_ty2 `eqType` out_ty2 &&
              in_role == out_role
            , text "optCoercion changed types!"
              $$ hang (text "in_co:") 2 (ppr co)
@@ -596,15 +596,11 @@ opt_trans_rule is co1 co2@(TyConAppCo r tc cos2)
 
 opt_trans_rule is co1@(AppCo co1a co1b) co2
   | Just (co2a,co2b) <- etaAppCo_maybe co2
-  = fireTransRule "EtaAppL" co1 co2 $
-    mkAppCo (opt_trans is co1a co2a)
-            (opt_trans is co1b co2b)
+  = opt_trans_rule_app is co1 co2 co1a [co1b] co2a [co2b]
 
 opt_trans_rule is co1 co2@(AppCo co2a co2b)
   | Just (co1a,co1b) <- etaAppCo_maybe co1
-  = fireTransRule "EtaAppR" co1 co2 $
-    mkAppCo (opt_trans is co1a co2a)
-            (opt_trans is co1b co2b)
+  = opt_trans_rule_app is co1 co2 co1a [co1b] co2a [co2b]
 
 -- Push transitivity inside forall
 opt_trans_rule is co1 co2
@@ -698,10 +694,45 @@ opt_trans_rule _ co1 co2        -- Identity rule
 
 opt_trans_rule _ _ _ = Nothing
 
+-- See Note [EtaAppCo]
+opt_trans_rule_app :: InScopeSet
+                   -> Coercion   -- original left-hand coercion (printing only)
+                   -> Coercion   -- original right-hand coercion (printing only)
+                   -> Coercion   -- left-hand coercion "function"
+                   -> [Coercion] -- left-hand coercion "args"
+                   -> Coercion   -- right-hand coercion "function"
+                   -> [Coercion] -- right-hand coercion "args"
+                   -> Maybe Coercion
+opt_trans_rule_app is orig_co1 orig_co2 co1a co1bs co2a co2bs
+  | AppCo co1aa co1ab <- co1a
+  , Just (co2aa, co2ab) <- etaAppCo_maybe co2a
+  = opt_trans_rule_app is orig_co1 orig_co2 co1aa (co1ab:co1bs) co2aa (co2ab:co2bs)
+
+  | AppCo co2aa co2ab <- co2a
+  , Just (co1aa, co1ab) <- etaAppCo_maybe co1a
+  = opt_trans_rule_app is orig_co1 orig_co2 co1aa (co1ab:co1bs) co2aa (co2ab:co2bs)
+
+  | otherwise
+  = ASSERT( co1bs `equalLength` co2bs )
+    fireTransRule ("EtaApps:" ++ show (length co1bs)) orig_co1 orig_co2 $
+    let Pair _ rt1a = coercionKind co1a
+        Pair lt2a _ = coercionKind co2a
+
+        Pair _ rt1bs = traverse coercionKind co1bs
+        Pair lt2bs _ = traverse coercionKind co2bs
+
+        kcoa = mkKindCo $ buildCoercion lt2a rt1a
+        kcobs = map mkKindCo $ zipWith buildCoercion lt2bs rt1bs
+
+        co2a' = mkCoherenceLeftCo co2a kcoa
+        co2bs' = zipWith mkCoherenceLeftCo co2bs kcobs
+    in
+    mkAppCos (opt_trans is co1a co2a')
+             (zipWith (opt_trans is) co1bs co2bs')
+
 fireTransRule :: String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
 fireTransRule _rule _co1 _co2 res
-  = -- pprTrace ("Trans rule fired: " ++ _rule) (vcat [ppr _co1, ppr _co2, ppr res]) $
-    Just res
+  = Just res
 
 {-
 Note [Conflict checking with AxiomInstCo]
@@ -758,6 +789,65 @@ that (Id Int) and (Id Bool) are Surely Apart, as they're headed by type
 families. At the time of writing, I (Richard Eisenberg) couldn't think of
 a way of detecting this any more efficient than just building the optimised
 coercion and checking.
+
+Note [EtaAppCo]
+~~~~~~~~~~~~~~~
+Suppose we're trying to optimize (co1a co1b ; co2a co2b). Ideally, we'd
+like to rewrite this to (co1a ; co2a) (co1b ; co2b). The problem is that
+the resultant coercions might not be well kinded. Here is an example (things
+labeled with x don't matter in this example):
+
+  k1 :: Type
+  k2 :: Type
+
+  a :: k1 -> Type
+  b :: k1
+
+  h :: k1 ~ k2
+
+  co1a :: x1 ~ (a |> (h -> <Type>)
+  co1b :: x2 ~ (b |> h)
+
+  co2a :: a ~ x3
+  co2b :: b ~ x4
+
+First, convince yourself of the following:
+
+  co1a co1b :: x1 x2 ~ (a |> (h -> <Type>)) (b |> h)
+  co2a co2b :: a b   ~ x3 x4
+
+  (a |> (h -> <Type>)) (b |> h) `eqType` a b
+
+That last fact is due to Note [Non-trivial definitional equality] in TyCoRep,
+where we ignore coercions in types as long as two types' kinds are the same.
+In our case, we meet this last condition, because
+
+  (a |> (h -> <Type>)) (b |> h) :: Type
+    and
+  a b :: Type
+
+So the input coercion (co1a co1b ; co2a co2b) is well-formed. But the
+suggested output coercions (co1a ; co2a) and (co1b ; co2b) are not -- the
+kinds don't match up.
+
+The solution here is to twiddle the kinds in the output coercions. First, we
+need to find coercions
+
+  ak :: kind(a |> (h -> <Type>)) ~ kind(a)
+  bk :: kind(b |> h)             ~ kind(b)
+
+This can be done with mkKindCo and buildCoercion. The latter assumes two
+types are identical modulo casts and builds a coercion between them.
+
+Then, we build (co1a ; co2a |> sym ak) and (co1b ; co2b |> sym bk) as the
+output coercions. These are well-kinded. (We cast the right-hand coercion
+because mkCoherenceLeftCo is smaller than mkCoherenceRightCo.)
+
+Also, note that all of this is done after accumulated any nested AppCo
+parameters. This step is to avoid quadratic behavior in calling coercionKind.
+
+The problem described here was first found in dependent/should_compile/dynamic-paper.
+
 -}
 
 -- | Check to make sure that an AxInstCo is internally consistent.
diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs
index 1082b5036d..9028460078 100644
--- a/compiler/types/TyCoRep.hs
+++ b/compiler/types/TyCoRep.hs
@@ -265,8 +265,10 @@ data Type
         Type
         Type            -- ^ Type application to something other than a 'TyCon'. Parameters:
                         --
-                        --  1) Function: must /not/ be a 'TyConApp',
+                        --  1) Function: must /not/ be a 'TyConApp' or 'CastTy',
                         --     must be another 'AppTy', or 'TyVarTy'
+                        --     See Note [Respecting definitional equality] (EQ1) about the
+                        --     no 'CastTy' requirement
                         --
                         --  2) Argument type
 
@@ -299,8 +301,8 @@ data Type
         Type
         KindCoercion  -- ^ A kind cast. The coercion is always nominal.
                       -- INVARIANT: The cast is never refl.
-                      -- INVARIANT: The cast is "pushed down" as far as it
-                      -- can go. See Note [Pushing down casts]
+                      -- INVARIANT: The Type is not a CastTy (use TransCo instead)
+                      -- See Note [Respecting definitional equality] (EQ2) and (EQ3)
 
   | CoercionTy
         Coercion    -- ^ Injection of a Coercion into a type
@@ -340,19 +342,12 @@ kinds or types.
 
 This kind instantiation only happens in TyConApp currently.
 
-Note [Pushing down casts]
-~~~~~~~~~~~~~~~~~~~~~~~~~
-Suppose we have (a :: k1 -> *), (b :: k1), and (co :: * ~ q).
-The type (a b |> co) is `eqType` to ((a |> co') b), where
-co' = (->) <k1> co. Thus, to make this visible to functions
-that inspect types, we always push down coercions, preferring
-the second form. Note that this also applies to TyConApps!
-
 Note [Non-trivial definitional equality]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Is Int |> <*> the same as Int? YES! In order to reduce headaches,
-we decide that any reflexive casts in types are just ignored. More
-generally, the `eqType` function, which defines Core's type equality
+we decide that any reflexive casts in types are just ignored.
+(Indeed they must be. See Note [Respecting definitional equality].)
+More generally, the `eqType` function, which defines Core's type equality
 relation, ignores casts and coercion arguments, as long as the
 two types have the same kind. This allows us to be a little sloppier
 in keeping track of coercions, which is a good thing. It also means
@@ -385,6 +380,9 @@ The effect of this all is that eqType, the implementation of the implicit
 equality check, can use any homogeneous relation that is smaller than ~, as
 those rules must also be admissible.
 
+A more drawn out argument around all of this is presented in Section 7.2 of
+Richard E's thesis (http://cs.brynmawr.edu/~rae/papers/2016/thesis/eisenberg-thesis.pdf).
+
 What would go wrong if we insisted on the casts matching? See the beginning of
 Section 8 in the unpublished paper above. Theoretically, nothing at all goes
 wrong. But in practical terms, getting the coercions right proved to be
@@ -405,10 +403,67 @@ constructors and destructors in Type respect whatever relation is chosen.
 
 Another helpful principle with eqType is this:
 
- ** If (t1 eqType t2) then I can replace t1 by t2 anywhere. **
+ (EQ) If (t1 `eqType` t2) then I can replace t1 by t2 anywhere.
 
 This principle also tells us that eqType must relate only types with the
 same kinds.
+
+Note [Respecting definitional equality]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Note [Non-trivial definitional equality] introduces the property (EQ).
+How is this upheld?
+
+Any function that pattern matches on all the constructors will have to
+consider the possibility of CastTy. Presumably, those functions will handle
+CastTy appropriately and we'll be OK.
+
+More dangerous are the splitXXX functions. Let's focus on splitTyConApp.
+We don't want it to fail on (T a b c |> co). Happily, if we have
+  (T a b c |> co) `eqType` (T d e f)
+then co must be reflexive. Why? eqType checks that the kinds are equal, as
+well as checking that (a `eqType` d), (b `eqType` e), and (c `eqType` f).
+By the kind check, we know that (T a b c |> co) and (T d e f) have the same
+kind. So the only way that co could be non-reflexive is for (T a b c) to have
+a different kind than (T d e f). But because T's kind is closed (all tycon kinds
+are closed), the only way for this to happen is that one of the arguments has
+to differ, leading to a contradiction. Thus, co is reflexive.
+
+Accordingly, by eliminating reflexive casts, splitTyConApp need not worry
+about outermost casts to uphold (EQ). Eliminating reflexive casts is done
+in mkCastTy.
+
+Unforunately, that's not the end of the story. Consider comparing
+  (T a b c)      =?       (T a b |> (co -> <Type>)) (c |> co)
+These two types have the same kind (Type), but the left type is a TyConApp
+while the right type is not. To handle this case, we say that the right-hand
+type is ill-formed, requiring an AppTy never to have a casted TyConApp
+on its left. It is easy enough to pull around the coercions to maintain
+this invariant, as done in Type.mkAppTy. In the example above, trying to
+form the right-hand type will instead yield (T a b (c |> co |> sym co) |> <Type>).
+Both the casts there are reflexive and will be dropped. Huzzah.
+
+This idea of pulling coercions to the right works for splitAppTy as well.
+
+However, there is one hiccup: it's possible that a coercion doesn't relate two
+Pi-types. For example, if we have @type family Fun a b where Fun a b = a -> b@,
+then we might have (T :: Fun Type Type) and (T |> axFun) Int. That axFun can't
+be pulled to the right. But we don't need to pull it: (T |> axFun) Int is not
+`eqType` to any proper TyConApp -- thus, leaving it where it is doesn't violate
+our (EQ) property.
+
+Lastly, in order to detect reflexive casts reliably, we must make sure not
+to have nested casts: we update (t |> co1 |> co2) to (t |> (co1 `TransCo` co2)).
+
+In sum, in order to uphold (EQ), we need the following three invariants:
+
+  (EQ1) No decomposable CastTy to the left of an AppTy, where a decomposable
+        cast is one that relates either a FunTy to a FunTy or a
+        ForAllTy to a ForAllTy.
+  (EQ2) No reflexive casts in CastTy.
+  (EQ3) No nested CastTys.
+
+These invariants are all documented above, in the declaration for Type.
+
 -}
 
 {- **********************************************************************
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index 3ee8a4abea..bd5f0ccd98 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -30,7 +30,7 @@ module Type (
         mkTyConApp, mkTyConTy,
         tyConAppTyCon_maybe, tyConAppTyConPicky_maybe,
         tyConAppArgs_maybe, tyConAppTyCon, tyConAppArgs,
-        splitTyConApp_maybe, splitTyConApp, tyConAppArgN, nextRole,
+        splitTyConApp_maybe, splitTyConApp, tyConAppArgN,
         tcRepSplitTyConApp_maybe, tcSplitTyConApp_maybe,
         splitListTyConApp_maybe,
         repSplitTyConApp_maybe,
@@ -92,7 +92,7 @@ module Type (
         mkAnonBinder,
         isAnonTyBinder, isNamedTyBinder,
         binderVar, binderVars, binderKind, binderArgFlag,
-        tyBinderType,
+        tyBinderType, tyBinderVar_maybe,
         binderRelevantType_maybe, caseBinder,
         isVisibleArgFlag, isInvisibleArgFlag, isVisibleBinder, isInvisibleBinder,
         tyConBindersTyBinders,
@@ -659,6 +659,11 @@ the type checker (e.g. when matching type-function equations).
 
 -- | Applies a type to another, as in e.g. @k a@
 mkAppTy :: Type -> Type -> Type
+  -- See Note [Respecting definitional equality], invariant (EQ1).
+mkAppTy (CastTy fun_ty co) arg_ty
+  | ([arg_co], res_co) <- decomposePiCos (typeKind fun_ty) [arg_ty] co
+  = (fun_ty `mkAppTy` (arg_ty `mkCastTy` arg_co)) `mkCastTy` res_co
+
 mkAppTy (TyConApp tc tys) ty2 = mkTyConApp tc (tys ++ [ty2])
 mkAppTy ty1               ty2 = AppTy ty1 ty2
         -- Note that the TyConApp could be an
@@ -672,6 +677,15 @@ mkAppTy ty1               ty2 = AppTy ty1 ty2
 
 mkAppTys :: Type -> [Type] -> Type
 mkAppTys ty1                []   = ty1
+mkAppTys (CastTy fun_ty co) arg_tys  -- much more efficient then nested mkAppTy
+                                     -- Why do this? See (EQ1) of
+                                     -- Note [Respecting definitional equality]
+                                     -- in TyCoRep
+  = foldl AppTy ((mkAppTys fun_ty casted_arg_tys) `mkCastTy` res_co) leftovers
+  where
+    (arg_cos, res_co) = decomposePiCos (typeKind fun_ty) arg_tys co
+    (args_to_cast, leftovers) = splitAtList arg_cos arg_tys
+    casted_arg_tys = zipWith mkCastTy args_to_cast arg_cos
 mkAppTys (TyConApp tc tys1) tys2 = mkTyConApp tc (tys1 ++ tys2)
 mkAppTys ty1                tys2 = foldl AppTy ty1 tys2
 
@@ -1126,20 +1140,6 @@ splitListTyConApp_maybe ty = case splitTyConApp_maybe ty of
   Just (tc,[e]) | tc == listTyCon -> Just e
   _other                          -> Nothing
 
--- | What is the role assigned to the next parameter of this type? Usually,
--- this will be 'Nominal', but if the type is a 'TyConApp', we may be able to
--- do better. The type does *not* have to be well-kinded when applied for this
--- to work!
-nextRole :: Type -> Role
-nextRole ty
-  | Just (tc, tys) <- splitTyConApp_maybe ty
-  , let num_tys = length tys
-  , num_tys < tyConArity tc
-  = tyConRoles tc `getNth` num_tys
-
-  | otherwise
-  = Nominal
-
 newTyConInstRhs :: TyCon -> [Type] -> Type
 -- ^ Unwrap one 'layer' of newtype on a type constructor and its
 -- arguments, using an eta-reduced version of the @newtype@ if possible.
@@ -1156,47 +1156,6 @@ newTyConInstRhs tycon tys
                            ~~~~~~
 A casted type has its *kind* casted into something new.
 
-Note [No reflexive casts in types]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-As far as possible, we would like to maintain the following property:
-
-  (*) If (t1 `eqType` t2), then t1 and t2 are treated identically within GHC.
-
-The (*) property is very useful, because we have a tendency to compare two
-types to see if they're equal, and then arbitrarily choose one. We don't
-want this arbitrary choice to then matter later on. Maintaining (*) means
-that every function that looks at a structure of a type must think about
-casts. In places where we directly pattern-match, this consideration is
-forced by consideration of the CastTy constructor.
-
-But, when we call a splitXXX function, it's easy to ignore the possibility
-of casts. In particular, splitTyConApp is used extensively, and we don't
-want it to fail on (T a b c |> co). Happily, if we have
-  (T a b c |> co) `eqType` (T d e f)
-then co must be reflexive. Why? eqType checks that the kinds are equal, as
-well as checking that (a `eqType` d), (b `eqType` e), and (c `eqType` f).
-By the kind check, we know that (T a b c |> co) and (T d e f) have the same
-kind. So the only way that co could be non-reflexive is for (T a b c) to have
-a different kind than (T d e f). But because T's kind is closed (all tycon kinds
-are closed), the only way for this to happen is that one of the arguments has
-to differ, leading to a contradiction. Thus, co is reflexive.
-
-Accordingly, by eliminating reflexive casts, splitTyConApp need not worry
-about outermost casts to uphold (*).
-
-Unfortunately, that's not the end of the story. Consider comparing
-  (T a b c)      =?       (T a b |> (co -> <Type>)) (c |> sym co)
-These two types have the same kind (Type), but the left type is a TyConApp
-while the right type is not. To handle this case, we will have to implement
-some variant of the dreaded KPush algorithm (c.f. CoreOpt.pushCoDataCon).
-This stone is left unturned for now, meaning that we don't yet uphold (*).
-
-The other place where (*) will be hard to guarantee is in splitAppTy, because
-I (Richard E) can't think of a way to push coercions into AppTys. The good
-news here is that splitAppTy is not used all that much, and so all clients of
-that function can simply be told to use splitCastTy as well, in order to
-uphold (*). This, too, is left undone, for now.
-
 -}
 
 splitCastTy_maybe :: Type -> Maybe (Type, Coercion)
@@ -1206,16 +1165,17 @@ splitCastTy_maybe _                            = Nothing
 
 -- | Make a 'CastTy'. The Coercion must be nominal. Checks the
 -- Coercion for reflexivity, dropping it if it's reflexive.
--- See Note [No reflexive casts in types]
+-- See Note [Respecting definitional equality] in TyCoRep
 mkCastTy :: Type -> Coercion -> Type
-mkCastTy ty co | isReflexiveCo co = ty
+mkCastTy ty co | isReflexiveCo co = ty  -- (EQ2) from the Note
 -- NB: Do the slow check here. This is important to keep the splitXXX
 -- functions working properly. Otherwise, we may end up with something
 -- like (((->) |> something_reflexive_but_not_obviously_so) biz baz)
 -- fails under splitFunTy_maybe. This happened with the cheaper check
 -- in test dependent/should_compile/dynamic-paper.
 
-mkCastTy (CastTy ty co1) co2 = mkCastTy ty (co1 `mkTransCo` co2)
+mkCastTy (CastTy ty co1) co2 = mkCastTy ty (co1 `mkTransCo` co2) -- (EQ3) from the Note
+                          -- call mkCastTy again for the reflexivity check
 mkCastTy ty co = CastTy ty co
 
 tyConBindersTyBinders :: [TyConBinder] -> [TyBinder]
@@ -1495,6 +1455,10 @@ isNamedTyBinder :: TyBinder -> Bool
 isNamedTyBinder (Named {}) = True
 isNamedTyBinder (Anon {})  = False
 
+tyBinderVar_maybe :: TyBinder -> Maybe TyVar
+tyBinderVar_maybe (Named tv) = Just $ binderVar tv
+tyBinderVar_maybe _          = Nothing
+
 tyBinderType :: TyBinder -> Type
 -- Barely used
 tyBinderType (Named tvb) = binderKind tvb
diff --git a/testsuite/tests/dependent/should_compile/T14556.hs b/testsuite/tests/dependent/should_compile/T14556.hs
new file mode 100644
index 0000000000..eebbdca888
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T14556.hs
@@ -0,0 +1,38 @@
+{-# Language UndecidableInstances, DataKinds, TypeOperators, KindSignatures, PolyKinds, TypeInType, TypeFamilies, GADTs, LambdaCase, ScopedTypeVariables #-}
+
+module T14556 where
+
+import Data.Kind
+import Data.Proxy
+
+data Fn a b where
+  IdSym :: Fn Type Type
+
+type family
+  (@@) (f::Fn k k') (a::k)::k' where
+  IdSym @@ a = a
+
+data KIND = X | FNARR KIND KIND
+
+data TY :: KIND -> Type where
+  ID    :: TY (FNARR X X)
+  FNAPP :: TY (FNARR k k') -> TY k -> TY k'
+
+data TyRep (kind::KIND) :: TY kind -> Type where
+  TID    :: TyRep (FNARR X X)  ID
+  TFnApp :: TyRep (FNARR k k') f
+         -> TyRep k            a
+         -> TyRep k'           (FNAPP f a)
+
+type family
+  IK (kind::KIND) :: Type where
+  IK X            = Type
+  IK (FNARR k k') = Fn (IK k) (IK k')
+
+type family
+  IT (ty::TY kind) :: IK kind where
+  IT ID          = IdSym
+  IT (FNAPP f x) = IT f @@ IT x
+
+zero :: TyRep X a -> IT a
+zero = undefined
diff --git a/testsuite/tests/dependent/should_compile/T14720.hs b/testsuite/tests/dependent/should_compile/T14720.hs
new file mode 100644
index 0000000000..c26a184689
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T14720.hs
@@ -0,0 +1,44 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+module T14720 where
+
+import Data.Kind (Type)
+import Data.Type.Equality ((:~:)(..), sym, trans)
+import Data.Void
+
+data family Sing (z :: k)
+
+class Generic (a :: Type) where
+    type Rep a :: Type
+    from :: a -> Rep a
+    to :: Rep a -> a
+
+class PGeneric (a :: Type) where
+  type PFrom (x :: a)     :: Rep a
+  type PTo   (x :: Rep a) :: a
+
+class SGeneric k where
+  sFrom :: forall (a :: k).     Sing a -> Sing (PFrom a)
+  sTo   :: forall (a :: Rep k). Sing a -> Sing (PTo a :: k)
+
+class (PGeneric k, SGeneric k) => VGeneric k where
+  sTof  :: forall (a :: k).     Sing a -> PTo (PFrom a) :~: a
+  sFot  :: forall (a :: Rep k). Sing a -> PFrom (PTo a :: k) :~: a
+
+data Decision a = Proved a
+                | Disproved (a -> Void)
+
+class SDecide k where
+  (%~) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b)
+  default (%~) :: forall (a :: k) (b :: k). (VGeneric k, SDecide (Rep k))
+               => Sing a -> Sing b -> Decision (a :~: b)
+  s1 %~ s2 = case sFrom s1 %~ sFrom s2 of
+    Proved (Refl :: PFrom a :~: PFrom b) ->
+      case (sTof s1, sTof s2) of
+          (Refl, Refl) -> Proved Refl
+    Disproved contra -> Disproved (\Refl -> contra Refl)
diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index 684602cc94..ab7ab3c8df 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -25,7 +25,9 @@ test('T11966', normal, compile, [''])
 test('T12442', normal, compile, [''])
 test('T13538', normal, compile, [''])
 test('T12176', normal, compile, [''])
-test('T14038', expect_broken(14038), compile, [''])
+test('T14038', normal, compile, [''])
 test('T12742', normal, compile, [''])
-test('T13910', expect_broken(13910), compile, [''])
-test('T13938', expect_broken(13938), compile, [''])
+test('T13910', normal, compile, [''])
+test('T13938', normal, compile, [''])
+test('T14556', normal, compile, [''])
+test('T14720', normal, compile, [''])
diff --git a/testsuite/tests/dependent/should_fail/RAE_T32a.stderr b/testsuite/tests/dependent/should_fail/RAE_T32a.stderr
index cb94dd2854..046a1e1aa4 100644
--- a/testsuite/tests/dependent/should_fail/RAE_T32a.stderr
+++ b/testsuite/tests/dependent/should_fail/RAE_T32a.stderr
@@ -1,19 +1,18 @@
 
 RAE_T32a.hs:28:1: error:
-    Too many parameters to Sing:
-      x is unexpected;
-      expected only two parameters
-    In the data instance declaration for ‘Sing’
+    • Expected kind ‘k0 -> *’,
+        but ‘Sing Sigma (Sigma p r)’ has kind ‘*’
+    • In the data instance declaration for ‘Sing’
 
 RAE_T32a.hs:28:20: error:
-    Expecting two more arguments to ‘Sigma’
-    Expected a type, but
-    ‘Sigma’ has kind
-    ‘forall p -> TyPi p (MkStar p) -> *’
-    In the first argument of ‘Sing’, namely ‘Sigma’
-    In the data instance declaration for ‘Sing’
+    • Expecting two more arguments to ‘Sigma’
+      Expected a type, but
+      ‘Sigma’ has kind
+      ‘forall p -> TyPi p (MkStar p) -> *’
+    • In the first argument of ‘Sing’, namely ‘Sigma’
+      In the data instance declaration for ‘Sing’
 
 RAE_T32a.hs:28:27: error:
-    Expected kind ‘Sigma’, but ‘Sigma p r’ has kind ‘*’
-    In the second argument of ‘Sing’, namely ‘(Sigma p r)’
-    In the data instance declaration for ‘Sing’
+    • Expected kind ‘Sigma’, but ‘Sigma p r’ has kind ‘*’
+    • In the second argument of ‘Sing’, namely ‘(Sigma p r)’
+      In the data instance declaration for ‘Sing’
diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T
index 4eb426419d..e28b2df5cd 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', expect_broken(12919), compile_fail, [''])
+test('RAE_T32a', normal, compile_fail, [''])
 test('TypeSkolEscape', normal, compile_fail, [''])
 test('BadTelescope', normal, compile_fail, [''])
 test('BadTelescope2', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_compile/SplitWD.hs b/testsuite/tests/typecheck/should_compile/SplitWD.hs
new file mode 100644
index 0000000000..370b077b6e
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/SplitWD.hs
@@ -0,0 +1,55 @@
+{-# LANGUAGE ScopedTypeVariables, TypeInType, TypeOperators,
+             TypeFamilies, GADTs, StandaloneDeriving #-}
+
+module SplitWD where
+
+import Data.Kind ( Type )
+
+data Nat = Zero | Succ Nat
+
+type family a + b where
+  Zero + b = b
+  Succ a + b = Succ (a + b)
+infixl 6 +
+
+data Vec :: Type -> Nat -> Type where
+  VNil :: Vec a Zero
+  (:>) :: a -> Vec a n -> Vec a (Succ n)
+infixr 5 :>
+
+type family (xs :: Vec a n) +++ (ys :: Vec a m) :: Vec a (n + m) where
+  VNil +++ ys = ys
+  (x :> xs) +++ ys = x :> (xs +++ ys)
+infixr 5 +++
+
+data Exp :: Vec Type n -> Type -> Type where
+  Var :: Elem xs x -> Exp xs x
+
+data Elem :: forall a n. Vec a n -> a -> Type where
+  Here :: Elem (x :> xs) x
+  There :: Elem xs x -> Elem (y :> xs) x
+
+-- | @Length xs@ is a runtime witness for how long a vector @xs@ is.
+-- @LZ :: Length xs@ says that @xs@ is empty.
+-- @LS len :: Length xs@ tells you that @xs@ has one more element
+-- than @len@ says.
+-- A term of type @Length xs@ also serves as a proxy for @xs@.
+data Length :: forall a n. Vec a n -> Type where
+  LZ :: Length VNil
+  LS :: Length xs -> Length (x :> xs)
+
+deriving instance Show (Length xs)
+
+-- | Convert an expression typed in one context to one typed in a larger
+-- context. Operationally, this amounts to de Bruijn index shifting.
+-- As a proposition, this is the weakening lemma.
+shift :: forall ts2 t ty. Exp ts2 ty -> Exp (t :> ts2) ty
+shift = go LZ
+  where
+    go :: forall ts1 ty. Length ts1 -> Exp (ts1 +++ ts2) ty -> Exp (ts1 +++ t :> ts2) ty
+    go l_ts1 (Var v)          = Var (shift_elem l_ts1 v)
+
+    shift_elem :: Length ts1 -> Elem (ts1 +++ ts2) x
+               -> Elem (ts1 +++ t :> ts2) x
+    shift_elem = undefined
+
diff --git a/testsuite/tests/typecheck/should_compile/T13643.hs b/testsuite/tests/typecheck/should_compile/T13643.hs
new file mode 100644
index 0000000000..d7cf1342c8
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T13643.hs
@@ -0,0 +1,22 @@
+{-# Language TypeFamilyDependencies #-}
+{-# Language RankNTypes             #-}
+{-# Language KindSignatures         #-}
+{-# Language DataKinds              #-}
+{-# Language TypeInType             #-}
+{-# Language GADTs                  #-}
+
+import Data.Kind (Type)
+
+data Code = I
+
+type family
+  Interp (a :: Code) = (res :: Type) | res -> a where
+  Interp I = Bool
+
+data T :: forall a. Interp a -> Type where
+  MkNat :: T False
+
+instance Show (T a) where show _ = "MkNat"
+
+main = do
+  print MkNat
diff --git a/testsuite/tests/typecheck/should_compile/T14441.hs b/testsuite/tests/typecheck/should_compile/T14441.hs
new file mode 100644
index 0000000000..047de1659f
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T14441.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+module T14441 where
+
+import Data.Kind
+
+type family Demote (k :: Type) :: Type
+type family DemoteX (a :: k) :: Demote k
+
+data Prox (a :: k) = P
+
+type instance Demote (Prox (a :: k)) = Prox (DemoteX a)
+$(return [])
+type instance DemoteX P = P
diff --git a/testsuite/tests/typecheck/should_compile/T14749.hs b/testsuite/tests/typecheck/should_compile/T14749.hs
new file mode 100644
index 0000000000..79bcce66ff
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T14749.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE GADTs, TypeOperators, DataKinds, TypeFamilies, TypeInType #-}
+
+module T14749 where
+
+import Data.Kind
+
+data KIND = STAR | KIND :> KIND
+
+data Ty :: KIND -> Type where
+  TMaybe :: Ty (STAR :> STAR)
+  TApp   :: Ty (a :> b) -> (Ty a -> Ty b)
+
+type family IK (k :: KIND) = (res :: Type) where
+  IK STAR   = Type
+  IK (a:>b) = IK a -> IK b
+
+type family I (t :: Ty k) = (res :: IK k)  where
+  I TMaybe     = Maybe
+  I (TApp f a) = (I f) (I a)
+
+data TyRep (k :: KIND) (t :: Ty k) where
+  TyMaybe :: TyRep (STAR:>STAR) TMaybe
+  TyApp   :: TyRep (a:>b) f -> TyRep a x -> TyRep b (TApp f x)
+
+zero :: TyRep STAR a -> I a
+zero x = case x of
+            TyApp TyMaybe _ -> Nothing
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 9a2ce73263..f4b7fe6aeb 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -536,7 +536,7 @@ test('T12797', normal, compile, [''])
 test('T12850', normal, compile, [''])
 test('T12911', normal, compile, [''])
 test('T12925', normal, compile, [''])
-test('T12919', expect_broken(12919), compile, [''])
+test('T12919', normal, compile, [''])
 test('T12936', normal, compile, [''])
 test('T13050', normal, compile, ['-fdefer-type-errors -fno-max-valid-substitutions'])
 test('T13083', normal, compile, [''])
@@ -568,7 +568,7 @@ test('T13651a', normal, compile, [''])
 test('T13680', normal, compile, [''])
 test('T13785', normal, compile, [''])
 test('T13804', normal, compile, [''])
-test('T13822', expect_broken(14749), compile, [''])
+test('T13822', normal, compile, [''])
 test('T13848', normal, compile, [''])
 test('T13871', normal, compile, [''])
 test('T13879', normal, compile, [''])
@@ -599,3 +599,7 @@ test('T14763', normal, compile, [''])
 test('T14811', normal, compile, [''])
 test('T14934', [extra_files(['T14934.hs', 'T14934a.hs'])], run_command,
                ['$MAKE -s --no-print-directory T14934'])
+test('T13643', normal, compile, [''])
+test('SplitWD', expect_broken(14119), compile, [''])
+test('T14441', normal, compile, [''])
+test('T14749', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/T12373.stderr b/testsuite/tests/typecheck/should_fail/T12373.stderr
index d3a4bb5e65..a2568d75f9 100644
--- a/testsuite/tests/typecheck/should_fail/T12373.stderr
+++ b/testsuite/tests/typecheck/should_fail/T12373.stderr
@@ -2,10 +2,10 @@
 T12373.hs:10:19: error:
     • Couldn't match a lifted type with an unlifted type
       When matching types
-        a1 :: *
-        MVar# RealWorld a0 :: TYPE 'UnliftedRep
-      Expected type: (# State# RealWorld, a1 #)
-        Actual type: (# State# RealWorld, MVar# RealWorld a0 #)
+        a0 :: *
+        MVar# RealWorld a1 :: TYPE 'UnliftedRep
+      Expected type: (# State# RealWorld, a0 #)
+        Actual type: (# State# RealWorld, MVar# RealWorld a1 #)
     • 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_run/Typeable1.stderr b/testsuite/tests/typecheck/should_run/Typeable1.stderr
index 65f6fd4645..63f02dbeb6 100644
--- a/testsuite/tests/typecheck/should_run/Typeable1.stderr
+++ b/testsuite/tests/typecheck/should_run/Typeable1.stderr
@@ -1,7 +1,6 @@
 
 Typeable1.hs:22:5: error:
-    • Couldn't match kind ‘* -> (* -> *) -> (* -> *) -> * -> *’
-                     with ‘forall k. (* -> *) -> (k -> *) -> k -> *’
+    • Couldn't match type ‘ComposeK’ with ‘a3 b3’
       Inaccessible code in
         a pattern with pattern synonym:
           App :: forall k2 (t :: k2).