Fix #14729 by making the normaliser homogeneous

This ports the fix to #12919 to the normaliser. (#12919 was about
the flattener.) Because the fix is involved, this is done by
moving the critical piece of code to Coercion, and then calling
this from both the flattener and the normaliser.

The key bit is: simplifying type families in a type is always
a *homogeneous* operation. See #12919 for a discussion of why
this is the Right Way to simplify type families.

Also fixes #15549.

test case: dependent/should_compile/T14729{,kind}
           typecheck/should_compile/T15549[ab]

13 files changed, 636 insertions, 371 deletions

diff --git a/compiler/deSugar/Check.hs b/compiler/deSugar/Check.hs
index c1c260d0c8..81832c8982 100644
--- a/compiler/deSugar/Check.hs
+++ b/compiler/deSugar/Check.hs
@@ -491,6 +491,10 @@ pmTopNormaliseType_maybe :: FamInstEnvs -> Bag EvVar -> Type
 -- Behaves exactly like `topNormaliseType_maybe`, but instead of returning a
 -- coercion, it returns useful information for issuing pattern matching
 -- warnings. See Note [Type normalisation for EmptyCase] for details.
+--
+-- NB: Normalisation can potentially change kinds, if the head of the type
+-- is a type family with a variable result kind. I (Richard E) can't think
+-- of a way to cause trouble here, though.
 pmTopNormaliseType_maybe env ty_cs typ
   = do (_, mb_typ') <- liftD $ initTcDsForSolver $ tcNormalise ty_cs typ
          -- Before proceeding, we chuck typ into the constraint solver, in case
@@ -536,7 +540,7 @@ pmTopNormaliseType_maybe env ty_cs typ
 
     tyFamStepper :: NormaliseStepper ([Type] -> [Type], [DataCon] -> [DataCon])
     tyFamStepper rec_nts tc tys  -- Try to step a type/data family
-      = let (_args_co, ntys) = normaliseTcArgs env Representational tc tys in
+      = let (_args_co, ntys, _res_co) = normaliseTcArgs env Representational tc tys in
           -- NB: It's OK to use normaliseTcArgs here instead of
           -- normalise_tc_args (which takes the LiftingContext described
           -- in Note [Normalising types]) because the reduceTyFamApp below
@@ -747,7 +751,7 @@ then
       type we get if we rewrite type families but not data families or
       newtypes.
   (b) dcs is the list of data constructors "skipped", every time we normalise a
-      newtype to it's core representation, we keep track of the source data
+      newtype to its core representation, we keep track of the source data
       constructor.
   (c) core_ty is the rewritten type. That is,
         pmTopNormaliseType_maybe env ty_cs ty = Just (src_ty, dcs, core_ty)
diff --git a/compiler/typecheck/TcFlatten.hs b/compiler/typecheck/TcFlatten.hs
index b3c41a5711..2a0fc7a33a 100644
--- a/compiler/typecheck/TcFlatten.hs
+++ b/compiler/typecheck/TcFlatten.hs
@@ -25,10 +25,10 @@ import Outputable
 import TcSMonad as TcS
 import BasicTypes( SwapFlag(..) )
 
-import Pair
 import Util
 import Bag
 import Control.Monad
+import MonadUtils    ( zipWith3M )
 
 import Control.Arrow ( first )
 
@@ -891,233 +891,6 @@ 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.
-
 Note [flatten_exact_fam_app_fully performance]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
@@ -1168,7 +941,6 @@ flatten_args :: [TyCoBinder] -> Bool -- Binders, and True iff any of them are
 -- 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
              any_named_bndrs
              orig_inner_ki
@@ -1236,7 +1008,7 @@ flatten_args_fast orig_binders orig_inner_ki orig_roles orig_tys
           --   mkCastTy x (Refl _ _) = x
           --   mkTcGReflLeftCo _ ty (Refl _ _) `mkTransCo` co = co
           --
-          -- Also, no need to check isAnonTyCoBinder or isNamedTyCoBinder, since
+          -- Also, no need to check isAnonTyCoBinder or isNamedBinder, since
           -- we've already established that they're all anonymous.
           Nominal          -> setEqRel NomEq  $ flatten_one ty
           Representational -> setEqRel ReprEq $ flatten_one ty
@@ -1258,111 +1030,42 @@ flatten_args_fast orig_binders orig_inner_ki orig_roles orig_tys
 flatten_args_slow :: [TyCoBinder] -> Kind -> TcTyCoVarSet
                   -> [Role] -> [Type]
                   -> FlatM ([Xi], [Coercion], CoercionN)
-flatten_args_slow orig_binders orig_inner_ki orig_fvs orig_roles orig_tys
-  = go [] [] orig_lc orig_binders orig_inner_ki orig_roles orig_tys
+flatten_args_slow binders inner_ki fvs roles tys
+-- Arguments used dependently must be flattened with proper coercions, but
+-- we're not guaranteed to get a proper coercion when flattening with the
+-- "Derived" flavour. So we must call noBogusCoercions when flattening arguments
+-- corresponding to binders that are dependent. However, we might legitimately
+-- have *more* arguments than binders, in the case that the inner_ki is a variable
+-- that gets instantiated with a Π-type. We conservatively choose not to produce
+-- bogus coercions for these, too. Note that this might miss an opportunity for
+-- a Derived rewriting a Derived. The solution would be to generate evidence for
+-- Deriveds, thus avoiding this whole noBogusCoercions idea. See also
+-- Note [No derived kind equalities]
+  = do { flattened_args <- zipWith3M fl (map isNamedBinder binders ++ repeat True)
+                                        roles tys
+       ; return (simplifyArgsWorker binders inner_ki fvs roles flattened_args) }
   where
-    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
-       -> [TyCoBinder]    -- 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 = mkTyCoPiTys 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 isNamedTyCoBinder binder
-                                   then noBogusCoercions $ flatten_one ty
-                                   else                    flatten_one ty
-
-               Representational -> ASSERT( isAnonTyCoBinder binder )
-                                   setEqRel ReprEq $ flatten_one ty
-
-               Phantom          -> -- See Note [Phantoms in the flattener]
-                                   ASSERT( isAnonTyCoBinder binder )
-                                   do { ty <- liftTcS $ zonkTcType ty
-                                      ; return (ty, mkReflCo Phantom ty) }
-
-             -- By Note [Flattening] invariant (F2),
-             -- tcTypeKind(xi) = tcTypeKind(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).
-             --
-             -- The bangs here have been observed to improve performance
-             -- significantly in optimized builds.
-           ; let kind_co = mkTcSymCo $
-                   liftCoSubst Nominal lc (tyCoBinderType binder)
-                 !casted_xi = xi `mkCastTy` kind_co
-                 casted_co =  mkTcCoherenceLeftCo role xi kind_co co
-
-             -- now, extend the lifting context with the new binding
-                 !new_lc | Just tv <- tyCoBinderVar_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 co1_kind              = coercionKind co1
-                 (arg_cos, res_co)     = decomposePiCos co1 co1_kind tys
-                 casted_tys            = ASSERT2( equalLength tys arg_cos
-                                                , ppr tys $$ ppr arg_cos )
-                                         zipWith mkCastTy tys arg_cos
-                    -- In general decomposePiCos can return fewer cos than tys,
-                    -- but not here; see "If we're at all well-typed..."
-                    -- in Note [Last case in flatten_args].  Hence the ASSERT.
-                 zapped_lc             = zapLiftingContext lc
-                 Pair flattened_kind _ = co1_kind
-                 (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 = zipWith3 mkTcGReflRightCo
-                                roles
-                                casted_tys
-                                (map mkTcSymCo arg_cos)
-                 cos' = zipWith mkTransCo cos_out cos
-
-           ; return (xis_out, cos', res_co_out `mkTcTransCo` res_co) }
-
-    go _ _ _ _ _ _ _ = pprPanic
-        "flatten_args wandered into deeper water than usual" (vcat [])
-           -- This debug information is commented out because leaving it in
-           -- causes a ~2% increase in allocations in T9872d.
-           -- That's independent of the analagous case in flatten_args_fast:
-           -- each of these causes a 2% increase on its own, so commenting them
-           -- both out gives a 4% decrease in T9872d.
-           {-
-
-             (vcat [ppr orig_binders,
-                    ppr orig_inner_ki,
-                    ppr (take 10 orig_roles), -- often infinite!
-                    ppr orig_tys])
-           -}
+    {-# INLINE fl #-}
+    fl :: Bool   -- must we ensure to produce a real coercion here?
+                  -- see comment at top of function
+       -> Role -> Type -> FlatM (Xi, Coercion)
+    fl True  r ty = noBogusCoercions $ fl1 r ty
+    fl False r ty =                    fl1 r ty
+
+    {-# INLINE fl1 #-}
+    fl1 :: Role -> Type -> FlatM (Xi, Coercion)
+    fl1 Nominal ty
+      = setEqRel NomEq $
+        flatten_one ty
+
+    fl1 Representational ty
+      = setEqRel ReprEq $
+        flatten_one ty
+
+    fl1 Phantom ty
+    -- See Note [Phantoms in the flattener]
+      = do { ty <- liftTcS $ zonkTcType ty
+           ; return (ty, mkReflCo Phantom ty) }
 
 ------------------
 flatten_one :: TcType -> FlatM (Xi, Coercion)
diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs
index ff0c9c5e9e..701c674aaf 100644
--- a/compiler/types/Coercion.hs
+++ b/compiler/types/Coercion.hs
@@ -2,7 +2,8 @@
 (c) The University of Glasgow 2006
 -}
 
-{-# LANGUAGE RankNTypes, CPP, MultiWayIf, FlexibleContexts #-}
+{-# LANGUAGE RankNTypes, CPP, MultiWayIf, FlexibleContexts, BangPatterns,
+             ScopedTypeVariables #-}
 
 -- | Module for (a) type kinds and (b) type coercions,
 -- as used in System FC. See 'CoreSyn.Expr' for
@@ -29,7 +30,7 @@ module Coercion (
         mkAxInstRHS, mkUnbranchedAxInstRHS,
         mkAxInstLHS, mkUnbranchedAxInstLHS,
         mkPiCo, mkPiCos, mkCoCast,
-        mkSymCo, mkTransCo,
+        mkSymCo, mkTransCo, mkTransMCo,
         mkNthCo, nthCoRole, mkLRCo,
         mkInstCo, mkAppCo, mkAppCos, mkTyConAppCo, mkFunCo,
         mkForAllCo, mkForAllCos, mkHomoForAllCos,
@@ -106,7 +107,9 @@ module Coercion (
         tidyCo, tidyCos,
 
         -- * Other
-        promoteCoercion, buildCoercion
+        promoteCoercion, buildCoercion,
+
+        simplifyArgsWorker
        ) where
 
 #include "HsVersions.h"
@@ -978,6 +981,12 @@ mkTransCo (GRefl r t1 (MCo co1)) (GRefl _ _ (MCo co2))
   = GRefl r t1 (MCo $ mkTransCo co1 co2)
 mkTransCo co1 co2                 = TransCo co1 co2
 
+-- | Compose two MCoercions via transitivity
+mkTransMCo :: MCoercion -> MCoercion -> MCoercion
+mkTransMCo MRefl     co2       = co2
+mkTransMCo co1       MRefl     = co1
+mkTransMCo (MCo co1) (MCo co2) = MCo (mkTransCo co1 co2)
+
 mkNthCo :: HasDebugCallStack
         => Role  -- The role of the coercion you're creating
         -> Int   -- Zero-indexed
@@ -1137,7 +1146,7 @@ mkGReflLeftCo r ty co
     -- instead of @isReflCo@
   | otherwise    = mkSymCo $ GRefl r ty (MCo co)
 
--- | Given @ty :: k1@, @co :: k1 ~ k2@, @co2:: ty ~ ty'@,
+-- | Given @ty :: k1@, @co :: k1 ~ k2@, @co2:: ty ~r ty'@,
 -- produces @co' :: (ty |> co) ~r ty'
 -- It is not only a utility function, but it saves allocation when co
 -- is a GRefl coercion.
@@ -1146,7 +1155,7 @@ mkCoherenceLeftCo r ty co co2
   | isGReflCo co = co2
   | otherwise = (mkSymCo $ GRefl r ty (MCo co)) `mkTransCo` co2
 
--- | Given @ty :: k1@, @co :: k1 ~ k2@, @co2:: ty' ~ ty@,
+-- | Given @ty :: k1@, @co :: k1 ~ k2@, @co2:: ty' ~r ty@,
 -- produces @co' :: ty' ~r (ty |> co)
 -- It is not only a utility function, but it saves allocation when co
 -- is a GRefl coercion.
@@ -2426,3 +2435,382 @@ buildCoercion orig_ty1 orig_ty2 = go orig_ty1 orig_ty2
     go ty1 ty2
       = pprPanic "buildKindCoercion" (vcat [ ppr orig_ty1, ppr orig_ty2
                                            , ppr ty1, ppr ty2 ])
+
+{-
+%************************************************************************
+%*                                                                      *
+       Simplifying types
+%*                                                                      *
+%************************************************************************
+
+The function below morally belongs in TcFlatten, but it is used also in
+FamInstEnv, and so lives here.
+
+Note [simplifyArgsWorker]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+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
+
+The first step is to flatten all the arguments. This is done before calling
+simplifyArgsWorker. We start from
+
+  a
+  b
+  Just a c
+  Right a b d
+  False
+
+and get
+
+  (fa,                             co1 :: fa ~ a)
+  (fb,                             co2 :: fb ~ b)
+  (Just fa (fc |> aco) |> co6,     co3 :: (Just fa (fc |> aco) |> co6) ~ (Just a c))
+  (Right fa fb (fd |> bco) |> co7, co4 :: (Right fa fb (fd |> bco) |> co7) ~ (Right a b d))
+  (False,                          co5 :: False ~ False)
+
+where
+  co6 :: Maybe fa ~ Maybe a
+  co7 :: Either fa fb ~ Either a b
+
+We now process the flattened args in left-to-right order. The first two args
+need no further processing. But now consider the third argument. Let f3 = the flattened
+result, Just fa (fc |> aco) |> co6.
+This f3 flattened argument has 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). We must cast this argument.
+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 co1. We can thus know the
+coercion needed for the 3rd argument is (Maybe (sym co1)), thus building
+(f3 |> Maybe (sym co1))
+
+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 (co1
+and co2, 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. Extend the (empty) LC with [j |-> co1]. No new casting must be done,
+     because the binder associated with the first argument has a closed type (no
+     variables).
+
+  2. Extend the LC with [k |-> co2]. No casting to do.
+
+  3. Lifting the kind (Maybe j) with our LC
+     yields co8 :: Maybe fa ~ Maybe a. Use (f3 |> sym co8) as the argument to
+     F.
+
+  4. Lifting the kind (Either j k) with our LC
+     yields co9 :: Either fa fb ~ Either a b. Use (f4 |> sym co9) as the 4th
+     argument to F, where f4 is the flattened form of argument 4, written above.
+
+  5. We lift Bool with our LC, getting <Bool>;
+     casting has no effect.
+
+We're now almost done, but the new application (F fa fb (f3 |> sym co8) (f4 > sym co9) 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 (in this case, [sym bco])
+is returned as the third return value from simplifyArgsWorker.
+
+Note [Last case in simplifyArgsWorker]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In writing simplifyArgsWorker's `go`, we know here that args 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.
+
+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
+
+First, we flatten all the arguments (before simplifyArgsWorker), like so:
+
+    (forall j. j -> Type, co1 :: (forall j. j -> Type) ~
+                                 (forall (j :: Star). (j |> axStar) -> Star))  -- 1
+    (Proxy |> co,         co2 :: (Proxy |> co) ~ (Proxy |> co))                -- 2
+    (Bool |> sym axStar,  co3 :: (Bool |> sym axStar) ~ (bo |> sym axStar))    -- 3
+    (False |> sym bc,     co4 :: (False |> sym bc) ~ (NoWay |> sym bc))        -- 4
+
+Then we do the process described in Note [simplifyArgsWorker].
+
+1. Lifting Type (the kind of the first arg) gives us a reflexive coercion, so we
+   don't use it. But we do build a lifting context [k -> co1] (where co1 is a
+   result of flattening an argument, written above).
+
+2. Lifting k gives us co1, so the second argument becomes (Proxy |> co |> sym co1).
+   This is not a dependent argument, so we don't extend the lifting context.
+
+Now we need to deal with argument (3). After flattening, should we tack on a homogenizing
+coercion? The way we normally tell is to lift the kind of the binder.
+But 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 at least one binder.
+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.) Because the flattened types have unflattened kinds (because
+flattening is homogeneous), passing the list of flattened types to decomposePiCos
+just won't do: later arguments' kinds won't be as expected. So we need to get
+the *unflattened* types to pass to decomposePiCos. We can do this easily enough
+by taking the kind of the argument coercions, passed in originally.
+
+(Alternative 1: We could re-engineer decomposePiCos to deal with this situation.
+But that function is already gnarly, and taking the right-hand types is correct
+at its other call sites, which are much more common than this one.)
+
+(Alternative 2: We could avoid calling decomposePiCos entirely, integrating its
+behavior into simplifyArgsWorker. This would work, I think, but then all of the
+complication of decomposePiCos would end up layered on top of all the complication
+here. Please, no.)
+
+(Alternative 3: We could pass the unflattened arguments into simplifyArgsWorker
+so that we don't have to recreate them. But that would complicate the interface
+of this function to handle a very dark, dark corner case. Better to keep our
+demons to ourselves here instead of exposing them to callers. This decision is
+easily reversed if there is ever any performance trouble due to the call of
+coercionKind.)
+
+So we now call
+
+  decomposePiCos co1
+                 (Pair (forall j. j -> Type) (forall (j :: Star). (j |> axStar) -> Star))
+                 [bo |> sym axStar, NoWay |> sym bc]
+
+to get
+
+  co5 :: Star ~ Type
+  co6 :: (j |> axStar) ~ (j |> co5), substituted to
+                              (bo |> sym axStar |> axStar) ~ (bo |> sym axStar |> co5)
+                           == bo ~ bo
+  res_co :: Type ~ Star
+
+We then use these casts on (the flattened) (3) and (4) to get
+
+  (Bool |> sym axStar |> co5 :: Type)   -- (C3)
+  (False |> sym bc |> co6    :: bo)     -- (C4)
+
+We can simplify to
+
+  Bool                        -- (C3)
+  (False |> sym bc :: bo)     -- (C4)
+
+Of course, we still must do the processing in Note [simplifyArgsWorker] to finish
+the job. We thus want to recur. Our new function kind is the left-hand type of
+co1 (gotten, recall, by lifting the variable k that was the return kind of the
+original function). Why the left-hand type (as opposed to the right-hand type)?
+Because we have casted all the arguments according to decomposePiCos, which gets
+us from the right-hand type to the left-hand one. We thus recur with that new
+function kind, zapping our lifting context, because we have essentially applied
+it.
+
+This recursive call returns ([Bool, False], [...], Refl). The Bool and False
+are the correct arguments we wish to return. But we must be careful about the
+result coercion: our new, flattened application will have kind Type, but we
+want to make sure that the result coercion casts this back to Star. (Why?
+Because we started with an application of kind Star, and flattening is homogeneous.)
+
+So, we have to twiddle the result coercion appropriately.
+
+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.
+
+Whew.
+
+-}
+
+
+-- This is shared between the flattener and the normaliser in FamInstEnv.
+-- See Note [simplifyArgsWorker]
+{-# INLINE simplifyArgsWorker #-}
+simplifyArgsWorker :: [TyCoBinder] -> Kind
+                       -- the binders & result kind (not a Π-type) of the function applied to the args
+                       -- list of binders can be shorter or longer than the list of args
+                   -> TyCoVarSet   -- free vars of the args
+                   -> [Role]   -- list of roles, r
+                   -> [(Type, Coercion)] -- flattened type arguments, arg
+                                         -- each comes with the coercion used to flatten it,
+                                         -- with co :: flattened_type ~ original_type
+                   -> ([Type], [Coercion], CoercionN)
+-- Returns (xis, cos, res_co), where each co :: xi ~ arg,
+-- and res_co :: kind (f xis) ~ kind (f tys), where f is the function applied to the args
+-- Precondition: if f :: forall bndrs. inner_ki (where bndrs and inner_ki are passed in),
+-- then (f orig_tys) is well kinded. Note that (f flattened_tys) might *not* be well-kinded.
+-- Massaging the flattened_tys in order to make (f flattened_tys) well-kinded is what this
+-- function is all about. That is, (f xis), where xis are the returned arguments, *is*
+-- well kinded.
+simplifyArgsWorker orig_ki_binders orig_inner_ki orig_fvs
+                   orig_roles orig_simplified_args
+  = go [] [] orig_lc orig_ki_binders orig_inner_ki orig_roles orig_simplified_args
+  where
+    orig_lc = emptyLiftingContext $ mkInScopeSet $ orig_fvs
+
+    go :: [Type]      -- 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
+       -> [TyCoBinder]    -- Unsubsted binders of function's kind
+       -> Kind        -- Unsubsted result kind of function (not a Pi-type)
+       -> [Role]      -- Roles at which to flatten these ...
+       -> [(Type, Coercion)]  -- flattened arguments, with their flattening coercions
+       -> ([Type], [Coercion], CoercionN)
+    go acc_xis acc_cos lc binders inner_ki _ []
+      = (reverse acc_xis, reverse acc_cos, kind_co)
+      where
+        final_kind = mkTyCoPiTys binders inner_ki
+        kind_co = liftCoSubst Nominal lc final_kind
+
+    go acc_xis acc_cos lc (binder:binders) inner_ki (role:roles) ((xi,co):args)
+      = -- By Note [Flattening] in TcFlatten invariant (F2),
+         -- tcTypeKind(xi) = tcTypeKind(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).
+         --
+         -- The bangs here have been observed to improve performance
+         -- significantly in optimized builds.
+         let kind_co = mkSymCo $
+               liftCoSubst Nominal lc (tyCoBinderType binder)
+             !casted_xi = xi `mkCastTy` kind_co
+             casted_co =  mkCoherenceLeftCo role xi kind_co co
+
+         -- now, extend the lifting context with the new binding
+             !new_lc | Just tv <- tyCoBinderVar_maybe binder
+                     = extendLiftingContextAndInScope lc tv casted_co
+                     | otherwise
+                     = lc
+         in
+         go (casted_xi : acc_xis)
+            (casted_co : acc_cos)
+            new_lc
+            binders
+            inner_ki
+            roles
+            args
+
+
+      -- See Note [Last case in simplifyArgsWorker]
+    go acc_xis acc_cos lc [] inner_ki roles args
+      | Just k   <- getTyVar_maybe inner_ki
+      , Just co1 <- liftCoSubstTyVar lc Nominal k
+      = let co1_kind              = coercionKind co1
+            unflattened_tys       = map (pSnd . coercionKind . snd) args
+            (arg_cos, res_co)     = decomposePiCos co1 co1_kind unflattened_tys
+            casted_args           = ASSERT2( equalLength args arg_cos
+                                           , ppr args $$ ppr arg_cos )
+                                    [ (casted_xi, casted_co)
+                                    | ((xi, co), arg_co, role) <- zip3 args arg_cos roles
+                                    , let casted_xi = xi `mkCastTy` arg_co
+                                          casted_co = mkCoherenceLeftCo role xi arg_co co ]
+               -- In general decomposePiCos can return fewer cos than tys,
+               -- but not here; because we're well typed, there will be enough
+               -- binders. Note that decomposePiCos does substitutions, so even
+               -- if the original substitution results in something ending with
+               -- ... -> k, that k will be substituted to perhaps reveal more
+               -- binders.
+            zapped_lc             = zapLiftingContext lc
+            Pair flattened_kind _ = co1_kind
+            (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_args
+        in
+        (xis_out, cos_out, res_co_out `mkTransCo` res_co)
+
+    go _ _ _ _ _ _ _ = panic
+        "simplifyArgsWorker wandered into deeper water than usual"
+           -- This debug information is commented out because leaving it in
+           -- causes a ~2% increase in allocations in T9872d.
+           -- That's independent of the analagous case in flatten_args_fast
+           -- in TcFlatten:
+           -- each of these causes a 2% increase on its own, so commenting them
+           -- both out gives a 4% decrease in T9872d.
+           {-
+
+             (vcat [ppr orig_binders,
+                    ppr orig_inner_ki,
+                    ppr (take 10 orig_roles), -- often infinite!
+                    ppr orig_tys])
+           -}
diff --git a/compiler/types/FamInstEnv.hs b/compiler/types/FamInstEnv.hs
index d721ad2873..1c9727aaec 100644
--- a/compiler/types/FamInstEnv.hs
+++ b/compiler/types/FamInstEnv.hs
@@ -2,7 +2,7 @@
 --
 -- FamInstEnv: Type checked family instance declarations
 
-{-# LANGUAGE CPP, GADTs, ScopedTypeVariables, BangPatterns #-}
+{-# LANGUAGE CPP, GADTs, ScopedTypeVariables, BangPatterns, TupleSections #-}
 
 module FamInstEnv (
         FamInst(..), FamFlavor(..), famInstAxiom, famInstTyCon, famInstRHS,
@@ -60,7 +60,6 @@ import Var
 import Pair
 import SrcLoc
 import FastString
-import MonadUtils
 import Control.Monad
 import Data.List( mapAccumL )
 import Data.Array( Array, assocs )
@@ -1268,16 +1267,33 @@ topNormaliseType_maybe :: FamInstEnvs -> Type -> Maybe (Coercion, Type)
 --
 -- However, ty' can be something like (Maybe (F ty)), where
 -- (F ty) is a redex.
-
+--
+-- Always operates homogeneously: the returned type has the same kind as the
+-- original type, and the returned coercion is always homogeneous.
 topNormaliseType_maybe env ty
-  = topNormaliseTypeX stepper mkTransCo ty
+  = do { ((co, mkind_co), nty) <- topNormaliseTypeX stepper combine ty
+       ; return $ case mkind_co of
+           MRefl       -> (co, nty)
+           MCo kind_co -> let nty_casted = nty `mkCastTy` mkSymCo kind_co
+                              final_co   = mkCoherenceRightCo Representational nty
+                                                              (mkSymCo kind_co) co
+                          in (final_co, nty_casted) }
   where
-    stepper = unwrapNewTypeStepper `composeSteppers` tyFamStepper
+    stepper = unwrapNewTypeStepper' `composeSteppers` tyFamStepper
+
+    combine (c1, mc1) (c2, mc2) = (c1 `mkTransCo` c2, mc1 `mkTransMCo` mc2)
+
+    unwrapNewTypeStepper' :: NormaliseStepper (Coercion, MCoercionN)
+    unwrapNewTypeStepper' rec_nts tc tys
+      = mapStepResult (, MRefl) $ unwrapNewTypeStepper rec_nts tc tys
 
+      -- second coercion below is the kind coercion relating the original type's kind
+      -- to the normalised type's kind
+    tyFamStepper :: NormaliseStepper (Coercion, MCoercionN)
     tyFamStepper rec_nts tc tys  -- Try to step a type/data family
-      = let (args_co, ntys) = normaliseTcArgs env Representational tc tys in
+      = let (args_co, ntys, res_co) = normaliseTcArgs env Representational tc tys in
         case reduceTyFamApp_maybe env Representational tc ntys of
-          Just (co, rhs) -> NS_Step rec_nts rhs (args_co `mkTransCo` co)
+          Just (co, rhs) -> NS_Step rec_nts rhs (args_co `mkTransCo` co, MCo res_co)
           _              -> NS_Done
 
 ---------------
@@ -1301,21 +1317,36 @@ normalise_tc_app tc tys
   = -- A type-family application
     do { env <- getEnv
        ; role <- getRole
-       ; (args_co, ntys) <- normalise_tc_args tc tys
+       ; (args_co, ntys, res_co) <- normalise_tc_args tc tys
        ; case reduceTyFamApp_maybe env role tc ntys of
            Just (first_co, ty')
              -> do { (rest_co,nty) <- normalise_type ty'
-                   ; return ( args_co `mkTransCo` first_co `mkTransCo` rest_co
-                            , nty ) }
+                   ; return (assemble_result role nty
+                                             (args_co `mkTransCo` first_co `mkTransCo` rest_co)
+                                             res_co) }
            _ -> -- No unique matching family instance exists;
                 -- we do not do anything
-                return (args_co, mkTyConApp tc ntys) }
+                return (assemble_result role (mkTyConApp tc ntys) args_co res_co) }
 
   | otherwise
   = -- A synonym with no type families in the RHS; or data type etc
     -- Just normalise the arguments and rebuild
-    do { (args_co, ntys) <- normalise_tc_args tc tys
-       ; return (args_co, mkTyConApp tc ntys) }
+    do { (args_co, ntys, res_co) <- normalise_tc_args tc tys
+       ; role <- getRole
+       ; return (assemble_result role (mkTyConApp tc ntys) args_co res_co) }
+
+  where
+    assemble_result :: Role       -- r, ambient role in NormM monad
+                    -> Type       -- nty, result type, possibly of changed kind
+                    -> Coercion   -- orig_ty ~r nty, possibly heterogeneous
+                    -> CoercionN  -- typeKind(orig_ty) ~N typeKind(nty)
+                    -> (Coercion, Type)   -- (co :: orig_ty ~r nty_casted, nty_casted)
+                                          -- where nty_casted has same kind as orig_ty
+    assemble_result r nty orig_to_nty kind_co
+      = ( final_co, nty_old_kind )
+      where
+        nty_old_kind = nty `mkCastTy` mkSymCo kind_co
+        final_co     = mkCoherenceRightCo r nty (mkSymCo kind_co) orig_to_nty
 
 ---------------
 -- | Normalise arguments to a tycon
@@ -1323,21 +1354,23 @@ normaliseTcArgs :: FamInstEnvs          -- ^ env't with family instances
                 -> Role                 -- ^ desired role of output coercion
                 -> TyCon                -- ^ tc
                 -> [Type]               -- ^ tys
-                -> (Coercion, [Type])   -- ^ co :: tc tys ~ tc new_tys
+                -> (Coercion, [Type], CoercionN)
+                                        -- ^ co :: tc tys ~ tc new_tys
+                                        -- NB: co might not be homogeneous
+                                        -- last coercion :: kind(tc tys) ~ kind(tc new_tys)
 normaliseTcArgs env role tc tys
   = initNormM env role (tyCoVarsOfTypes tys) $
     normalise_tc_args tc tys
 
 normalise_tc_args :: TyCon -> [Type]             -- tc tys
-                  -> NormM (Coercion, [Type])    -- (co, new_tys), where
-                                                 -- co :: tc tys ~ tc new_tys
+                  -> NormM (Coercion, [Type], CoercionN)
+                  -- (co, new_tys), where
+                  -- co :: tc tys ~ tc new_tys; might not be homogeneous
+                  -- res_co :: typeKind(tc tys) ~N typeKind(tc new_tys)
 normalise_tc_args tc tys
   = do { role <- getRole
-       ; (cois, ntys) <- zipWithAndUnzipM normalise_type_role
-                                          tys (tyConRolesX role tc)
-       ; return (mkTyConAppCo role tc cois, ntys) }
-  where
-    normalise_type_role ty r = withRole r $ normalise_type ty
+       ; (args_cos, nargs, res_co) <- normalise_args (tyConKind tc) (tyConRolesX role tc) tys
+       ; return (mkTyConAppCo role tc args_cos, nargs, res_co) }
 
 ---------------
 normaliseType :: FamInstEnvs
@@ -1363,10 +1396,9 @@ normalise_type ty
     go (TyConApp tc tys) = normalise_tc_app tc tys
     go ty@(LitTy {})     = do { r <- getRole
                               ; return (mkReflCo r ty, ty) }
-    go (AppTy ty1 ty2)
-      = do { (co,  nty1) <- go ty1
-           ; (arg, nty2) <- withRole Nominal $ go ty2
-           ; return (mkAppCo co arg, mkAppTy nty1 nty2) }
+
+    go (AppTy ty1 ty2) = go_app_tys ty1 [ty2]
+
     go (FunTy ty1 ty2)
       = do { (co1, nty1) <- go ty1
            ; (co2, nty2) <- go ty2
@@ -1393,6 +1425,57 @@ normalise_type ty
                          co right_co
                     , mkCoercionTy right_co ) }
 
+    go_app_tys :: Type   -- function
+               -> [Type] -- args
+               -> NormM (Coercion, Type)
+    -- cf. TcFlatten.flatten_app_ty_args
+    go_app_tys (AppTy ty1 ty2) tys = go_app_tys ty1 (ty2 : tys)
+    go_app_tys fun_ty arg_tys
+      = do { (fun_co, nfun) <- go fun_ty
+           ; case tcSplitTyConApp_maybe nfun of
+               Just (tc, xis) ->
+                 do { (second_co, nty) <- go (mkTyConApp tc (xis ++ arg_tys))
+                   -- flatten_app_ty_args avoids redundantly processing the xis,
+                   -- but that's a much more performance-sensitive function.
+                   -- This type normalisation is not called in a loop.
+                    ; return (mkAppCos fun_co (map mkNomReflCo arg_tys) `mkTransCo` second_co, nty) }
+               Nothing ->
+                 do { (args_cos, nargs, res_co) <- normalise_args (typeKind nfun)
+                                                                  (repeat Nominal)
+                                                                  arg_tys
+                    ; role <- getRole
+                    ; let nty = mkAppTys nfun nargs
+                          nco = mkAppCos fun_co args_cos
+                          nty_casted = nty `mkCastTy` mkSymCo res_co
+                          final_co = mkCoherenceRightCo role nty (mkSymCo res_co) nco
+                    ; return (final_co, nty_casted) } }
+
+normalise_args :: Kind    -- of the function
+               -> [Role]  -- roles at which to normalise args
+               -> [Type]  -- args
+               -> NormM ([Coercion], [Type], Coercion)
+-- returns (cos, xis, res_co), where each xi is the normalised
+-- version of the corresponding type, each co is orig_arg ~ xi,
+-- and the res_co :: kind(f orig_args) ~ kind(f xis)
+-- NB: The xis might *not* have the same kinds as the input types,
+-- but the resulting application *will* be well-kinded
+-- cf. TcFlatten.flatten_args_slow
+normalise_args fun_ki roles args
+  = do { normed_args <- zipWithM normalise1 roles args
+       ; let (xis, cos, res_co) = simplifyArgsWorker ki_binders inner_ki fvs roles normed_args
+       ; return (map mkSymCo cos, xis, mkSymCo res_co) }
+  where
+    (ki_binders, inner_ki) = splitPiTys fun_ki
+    fvs = tyCoVarsOfTypes args
+
+    -- flattener conventions are different from ours
+    impedance_match :: NormM (Coercion, Type) -> NormM (Type, Coercion)
+    impedance_match action = do { (co, ty) <- action
+                                ; return (ty, mkSymCo co) }
+
+    normalise1 role ty
+      = impedance_match $ withRole role $ normalise_type ty
+
 normalise_tyvar :: TyVar -> NormM (Coercion, Type)
 normalise_tyvar tv
   = ASSERT( isTyVar tv )
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index 2fd060a7f4..e0ceb24b06 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -99,7 +99,7 @@ module Type (
         mkTyCoVarBinder, mkTyCoVarBinders,
         mkTyVarBinders,
         mkAnonBinder,
-        isAnonTyCoBinder, isNamedTyCoBinder,
+        isAnonTyCoBinder,
         binderVar, binderVars, binderType, binderArgFlag,
         tyCoBinderType, tyCoBinderVar_maybe,
         tyBinderType,
@@ -1681,10 +1681,6 @@ isAnonTyCoBinder :: TyCoBinder -> Bool
 isAnonTyCoBinder (Named {}) = False
 isAnonTyCoBinder (Anon {})  = True
 
-isNamedTyCoBinder :: TyCoBinder -> Bool
-isNamedTyCoBinder (Named {}) = True
-isNamedTyCoBinder (Anon {})  = False
-
 tyCoBinderVar_maybe :: TyCoBinder -> Maybe TyCoVar
 tyCoBinderVar_maybe (Named tv) = Just $ binderVar tv
 tyCoBinderVar_maybe _          = Nothing
diff --git a/testsuite/tests/dependent/should_compile/T14729.hs b/testsuite/tests/dependent/should_compile/T14729.hs
new file mode 100644
index 0000000000..4d0bd8a173
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T14729.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE ExplicitForAll, PolyKinds, TypeFamilies, DataKinds #-}
+
+module T14729 where
+
+import Data.Kind
+
+data P k :: k -> Type
+
+type family F a
+type instance F Int = Bool
+
+x :: forall (x :: Bool). P (F Int) x
+x = undefined
+
+y = x
diff --git a/testsuite/tests/dependent/should_compile/T14729.stderr b/testsuite/tests/dependent/should_compile/T14729.stderr
new file mode 100644
index 0000000000..dcf441ce8a
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T14729.stderr
@@ -0,0 +1,15 @@
+TYPE SIGNATURES
+  x :: forall (x :: Bool). P (F Int) (x |> Sym (T14729.D:R:FInt[0]))
+  y :: forall (x :: Bool). P Bool x
+TYPE CONSTRUCTORS
+  type family F{1} :: * -> *
+    roles nominal
+  data type P{2} :: forall k -> k -> *
+    roles nominal phantom
+COERCION AXIOMS
+  axiom T14729.D:R:FInt :: F Int = Bool
+FAMILY INSTANCES
+  type instance F Int = Bool -- Defined at T14729.hs:10:15
+Dependent modules: []
+Dependent packages: [base-4.12.0.0, ghc-prim-0.5.3,
+                     integer-gmp-1.0.2.0]
diff --git a/testsuite/tests/dependent/should_compile/T14729kind.script b/testsuite/tests/dependent/should_compile/T14729kind.script
new file mode 100644
index 0000000000..4847c94d46
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T14729kind.script
@@ -0,0 +1,6 @@
+:seti -XPolyKinds -XDataKinds -XExplicitForAll -XTypeFamilies
+import Data.Kind
+data P k :: k -> Type
+type family F a
+type instance F Int = Bool
+:kind! forall (x :: Bool). P (F Int) x
diff --git a/testsuite/tests/dependent/should_compile/T14729kind.stdout b/testsuite/tests/dependent/should_compile/T14729kind.stdout
new file mode 100644
index 0000000000..c4c3e2243c
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T14729kind.stdout
@@ -0,0 +1,2 @@
+forall (x :: Bool). P (F Int) x :: *
+= P Bool x
diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index 31a853b61e..fa39c9a69a 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -64,3 +64,5 @@ test('T15076', normal, compile, [''])
 test('T15076b', normal, compile, [''])
 test('T15076c', normal, compile, [''])
 test('T15829', normal, compile, [''])
+test('T14729', normal, compile, ['-ddump-types -fprint-typechecker-elaboration -fprint-explicit-coercions'])
+test('T14729kind', normal, ghci_script, ['T14729kind.script'])
diff --git a/testsuite/tests/typecheck/should_compile/T15549a.hs b/testsuite/tests/typecheck/should_compile/T15549a.hs
new file mode 100644
index 0000000000..4737ad2491
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T15549a.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE DataKinds #-}
+module T15549a where
+
+import Data.Proxy
+import Data.Void
+
+data family Sing (a :: k)
+data instance Sing (z :: Void)
+
+type family Rep a
+class SGeneric a where
+  sTo :: forall (r :: Rep a). Sing r -> Proxy a
+
+type instance Rep Void = Void
+instance SGeneric Void where
+  sTo x = case x of
diff --git a/testsuite/tests/typecheck/should_compile/T15549b.hs b/testsuite/tests/typecheck/should_compile/T15549b.hs
new file mode 100644
index 0000000000..ffd4c51d53
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T15549b.hs
@@ -0,0 +1,29 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE DataKinds #-}
+
+module T15549b where
+
+import Data.Kind (Type)
+
+newtype Identity a = Identity a
+newtype Par1 a = Par1 a
+
+data family Sing :: forall k. k -> Type
+data instance Sing :: forall k. k -> Type
+
+type family Rep1 (f :: Type -> Type) :: Type -> Type
+type instance Rep1 Identity = Par1
+
+type family From1 (z :: f a) :: Rep1 f a
+type instance From1 ('Identity x) = 'Par1 x
+
+und :: a
+und = und
+
+f :: forall (a :: Type) (x :: Identity a).  Sing x
+f = g
+    where g :: forall (a :: Type) (f :: Type -> Type) (x :: f a). Sing x
+          g = seq (und :: Sing (From1 x)) und
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 7a08e21e23..3ee0a9f6d4 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -663,3 +663,5 @@ test('T14761c', normal, compile, [''])
 test('T16008', normal, compile, [''])
 test('T16033', normal, compile, [''])
 test('T16141', normal, compile, ['-O'])
+test('T15549a', normal, compile, [''])
+test('T15549b', normal, compile, [''])