Use Reductions to keep track of rewritings

We define Reduction = Reduction Coercion !Type.
A reduction of the form 'Reduction co new_ty' witnesses an
equality ty ~co~> new_ty.
That is, the rewriting happens left-to-right: the right-hand-side
type of the coercion is the rewritten type, and the left-hand-side
type the original type.
Sticking to this convention makes the codebase more consistent,
helping to avoid certain applications of SymCo.

This replaces the parts of the codebase which represented reductions as
pairs, (Coercion,Type) or (Type,Coercion).

Reduction being strict in the Type argument improves performance
in some programs that rewrite many type families (such as T9872).

Fixes #20161

-------------------------
Metric Decrease:
  T5321Fun
    T9872a
    T9872b
    T9872c
    T9872d
-------------------------

21 files changed, 1410 insertions, 919 deletions

diff --git a/compiler/GHC/Core/Coercion.hs b/compiler/GHC/Core/Coercion.hs
index aa0cf29754..ac09b0a7c4 100644
--- a/compiler/GHC/Core/Coercion.hs
+++ b/compiler/GHC/Core/Coercion.hs
@@ -122,8 +122,6 @@ module GHC.Core.Coercion (
 
         multToCo,
 
-        simplifyArgsWorker,
-
         hasCoercionHoleTy, hasCoercionHoleCo,
         HoleSet, coercionHolesOfType, coercionHolesOfCo
        ) where
@@ -1069,7 +1067,7 @@ mkTransCo co1 co2 | isReflCo co1 = co2
                   | isReflCo co2 = co1
 mkTransCo (GRefl r t1 (MCo co1)) (GRefl _ _ (MCo co2))
   = GRefl r t1 (MCo $ mkTransCo co1 co2)
-mkTransCo co1 co2                 = TransCo co1 co2
+mkTransCo co1 co2                = TransCo co1 co2
 
 mkNthCo :: HasDebugCallStack
         => Role  -- The role of the coercion you're creating
@@ -1323,7 +1321,7 @@ mkAxiomRuleCo = AxiomRuleCo
 
 -- | Make a "coercion between coercions".
 mkProofIrrelCo :: Role       -- ^ role of the created coercion, "r"
-               -> Coercion   -- ^ :: phi1 ~N phi2
+               -> CoercionN  -- ^ :: phi1 ~N phi2
                -> Coercion   -- ^ g1 :: phi1
                -> Coercion   -- ^ g2 :: phi2
                -> Coercion   -- ^ :: g1 ~r g2
@@ -1790,7 +1788,8 @@ unwrapNewTypeStepper rec_nts tc tys
 -- then ty ~ev1~ t1 ~ev2~ t2 ... ~evn~ ty'
 -- and ev = ev1 `plus` ev2 `plus` ... `plus` evn
 -- If it returns Nothing then no newtype unwrapping could happen
-topNormaliseTypeX :: NormaliseStepper ev -> (ev -> ev -> ev)
+topNormaliseTypeX :: NormaliseStepper ev
+                  -> (ev -> ev -> ev)
                   -> Type -> Maybe (ev, Type)
 topNormaliseTypeX stepper plus ty
  | Just (tc, tys) <- splitTyConApp_maybe ty
@@ -2114,11 +2113,20 @@ liftCoSubstTyVar (LC subst env) r v
 {- Note [liftCoSubstVarBndr]
 
 callback:
-  We want 'liftCoSubstVarBndrUsing' to be general enough to be reused in
-  FamInstEnv, therefore the input arg 'fun' returns a pair with polymorphic type
-  in snd.
-  However in 'liftCoSubstVarBndr', we don't need the snd, so we use unit and
-  ignore the fourth component of the return value.
+  'liftCoSubstVarBndrUsing' needs to be general enough to work in two
+  situations:
+
+    - in this module, which manipulates 'Coercion's, and
+    - in GHC.Core.FamInstEnv, where we work with 'Reduction's, which contain
+      a coercion as well as a type.
+
+  To achieve this, we require that the return type of the 'callback' function
+  contain a coercion within it. This is witnessed by the first argument
+  to 'liftCoSubstVarBndrUsing': a getter, which allows us to retrieve
+  the coercion inside the return type. Thus:
+
+    - in this module, we simply pass 'id' as the getter,
+    - in GHC.Core.FamInstEnv, we pass 'reductionCoercion' as the getter.
 
 liftCoSubstTyVarBndrUsing:
   Given
@@ -2152,52 +2160,56 @@ liftCoSubstCoVarBndrUsing:
 liftCoSubstVarBndr :: LiftingContext -> TyCoVar
                    -> (LiftingContext, TyCoVar, Coercion)
 liftCoSubstVarBndr lc tv
-  = let (lc', tv', h, _) = liftCoSubstVarBndrUsing callback lc tv in
-    (lc', tv', h)
+  = liftCoSubstVarBndrUsing id callback lc tv
   where
-    callback lc' ty' = (ty_co_subst lc' Nominal ty', ())
+    callback lc' ty' = ty_co_subst lc' Nominal ty'
 
 -- the callback must produce a nominal coercion
-liftCoSubstVarBndrUsing :: (LiftingContext -> Type -> (CoercionN, a))
-                           -> LiftingContext -> TyCoVar
-                           -> (LiftingContext, TyCoVar, CoercionN, a)
-liftCoSubstVarBndrUsing fun lc old_var
+liftCoSubstVarBndrUsing :: (r -> CoercionN)              -- ^ coercion getter
+                        -> (LiftingContext -> Type -> r) -- ^ callback
+                        -> LiftingContext -> TyCoVar
+                        -> (LiftingContext, TyCoVar, r)
+liftCoSubstVarBndrUsing view_co fun lc old_var
   | isTyVar old_var
-  = liftCoSubstTyVarBndrUsing fun lc old_var
+  = liftCoSubstTyVarBndrUsing view_co fun lc old_var
   | otherwise
-  = liftCoSubstCoVarBndrUsing fun lc old_var
+  = liftCoSubstCoVarBndrUsing view_co fun lc old_var
 
 -- Works for tyvar binder
-liftCoSubstTyVarBndrUsing :: (LiftingContext -> Type -> (CoercionN, a))
-                           -> LiftingContext -> TyVar
-                           -> (LiftingContext, TyVar, CoercionN, a)
-liftCoSubstTyVarBndrUsing fun lc@(LC subst cenv) old_var
+liftCoSubstTyVarBndrUsing :: (r -> CoercionN)              -- ^ coercion getter
+                          -> (LiftingContext -> Type -> r) -- ^ callback
+                          -> LiftingContext -> TyVar
+                          -> (LiftingContext, TyVar, r)
+liftCoSubstTyVarBndrUsing view_co fun lc@(LC subst cenv) old_var
   = assert (isTyVar old_var) $
     ( LC (subst `extendTCvInScope` new_var) new_cenv
-    , new_var, eta, stuff )
+    , new_var, stuff )
   where
-    old_kind     = tyVarKind old_var
-    (eta, stuff) = fun lc old_kind
-    k1           = coercionLKind eta
-    new_var      = uniqAway (getTCvInScope subst) (setVarType old_var k1)
+    old_kind = tyVarKind old_var
+    stuff    = fun lc old_kind
+    eta      = view_co stuff
+    k1       = coercionLKind eta
+    new_var  = uniqAway (getTCvInScope subst) (setVarType old_var k1)
 
     lifted   = mkGReflRightCo Nominal (TyVarTy new_var) eta
                -- :: new_var ~ new_var |> eta
     new_cenv = extendVarEnv cenv old_var lifted
 
 -- Works for covar binder
-liftCoSubstCoVarBndrUsing :: (LiftingContext -> Type -> (CoercionN, a))
-                           -> LiftingContext -> CoVar
-                           -> (LiftingContext, CoVar, CoercionN, a)
-liftCoSubstCoVarBndrUsing fun lc@(LC subst cenv) old_var
+liftCoSubstCoVarBndrUsing :: (r -> CoercionN)              -- ^ coercion getter
+                          -> (LiftingContext -> Type -> r) -- ^ callback
+                          -> LiftingContext -> CoVar
+                          -> (LiftingContext, CoVar, r)
+liftCoSubstCoVarBndrUsing view_co fun lc@(LC subst cenv) old_var
   = assert (isCoVar old_var) $
     ( LC (subst `extendTCvInScope` new_var) new_cenv
-    , new_var, kind_co, stuff )
+    , new_var, stuff )
   where
-    old_kind     = coVarKind old_var
-    (eta, stuff) = fun lc old_kind
-    k1           = coercionLKind eta
-    new_var      = uniqAway (getTCvInScope subst) (setVarType old_var k1)
+    old_kind = coVarKind old_var
+    stuff    = fun lc old_kind
+    eta      = view_co stuff
+    k1       = coercionLKind eta
+    new_var  = uniqAway (getTCvInScope subst) (setVarType old_var k1)
 
     -- old_var :: s1  ~r s2
     -- eta     :: (s1' ~r s2') ~N (t1 ~r t2)
@@ -2205,7 +2217,6 @@ liftCoSubstCoVarBndrUsing fun lc@(LC subst cenv) old_var
     -- eta2    :: s2' ~r t2
     -- co1     :: s1' ~r s2'
     -- co2     :: t1  ~r t2
-    -- kind_co :: (s1' ~r s2') ~N (t1 ~r t2)
     -- lifted  :: co1 ~N co2
 
     role   = coVarRole old_var
@@ -2215,10 +2226,7 @@ liftCoSubstCoVarBndrUsing fun lc@(LC subst cenv) old_var
 
     co1     = mkCoVarCo new_var
     co2     = mkSymCo eta1 `mkTransCo` co1 `mkTransCo` eta2
-    kind_co = mkTyConAppCo Nominal (equalityTyCon role)
-                           [ mkKindCo co1, mkKindCo co2
-                           , co1         , co2          ]
-    lifted  = mkProofIrrelCo Nominal kind_co co1 co2
+    lifted  = mkProofIrrelCo Nominal eta co1 co2
 
     new_cenv = extendVarEnv cenv old_var lifted
 
@@ -2697,401 +2705,6 @@ buildCoercion orig_ty1 orig_ty2 = go orig_ty1 orig_ty2
       = pprPanic "buildKindCoercion" (vcat [ ppr orig_ty1, ppr orig_ty2
                                            , ppr ty1, ppr ty2 ])
 
-{-
-%************************************************************************
-%*                                                                      *
-       Simplifying types
-%*                                                                      *
-%************************************************************************
-
-The function below morally belongs in GHC.Tc.Solver.Rewrite, but it is used also in
-FamInstEnv, and so lives here.
-
-Note [simplifyArgsWorker]
-~~~~~~~~~~~~~~~~~~~~~~~~~
-Invariant (F2) of Note [Rewriting] in GHC.Tc.Solver.Rewrite says that
-rewriting is homogeneous.
-This causes some trouble when rewriting 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 rewrite 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 rewrite 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 rewritten args in left-to-right order. The first two args
-need no further processing. But now consider the third argument. Let f3 = the rewritten
-result, Just fa (fc |> aco) |> co6.
-This f3 rewritten 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) rewrote 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 rewriting the corresponding argument (co1
-and co2, in our example). Then, after rewriting 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 rewriting 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 rewritten 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 rewriting:
-  a (forall (j :: Star). (j |> axStar) -> Star)   -- 1
-    (Proxy |> co)                                 -- 2
-    (bo |> sym axStar)                            -- 3
-    (NoWay |> sym bc)                             -- 4
-      :: Star
-
-First, we rewrite 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 rewriting 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).
-The way we normally proceed is to lift the kind of the binder, to see whether
-it's dependent.
-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 rewritten types have unrewritten kinds (because
-rewriting is homogeneous), passing the list of rewritten types to decomposePiCos
-just won't do: later arguments' kinds won't be as expected. So we need to get
-the *unrewritten* 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 unrewritten 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 rewritten) (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, rewritten 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 rewriting 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.
-
-Historical note: I (Richard E) once thought that the final part of the kind
-had to be a variable k (as in the example above). But it might not be: it could
-be an application of a variable. Here is the example:
-
-  let f :: forall (a :: Type) (b :: a -> Type). b (Any @a)
-      k :: Type
-      x :: k
-
-  rewrite (f @Type @((->) k) x)
-
-After instantiating [a |-> Type, b |-> ((->) k)], we see that `b (Any @a)`
-is `k -> Any @a`, and thus the third argument of `x :: k` is well-kinded.
-
--}
-
-
--- This is shared between the rewriter and the normaliser in GHC.Core.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)] -- rewritten type arguments, arg
-                                         -- each comes with the coercion used to rewrite it,
-                                         -- with co :: rewritten_type ~ original_type
-                   -> ([Type], [Coercion], MCoercionN)
--- 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 rewritten_tys) might *not* be well-kinded.
--- Massaging the rewritten_tys in order to make (f rewritten_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 rewriting coercions
-       -> [TyCoBinder]    -- Unsubsted binders of function's kind
-       -> Kind        -- Unsubsted result kind of function (not a Pi-type)
-       -> [Role]      -- Roles at which to rewrite these ...
-       -> [(Type, Coercion)]  -- rewritten arguments, with their rewriting coercions
-       -> ([Type], [Coercion], MCoercionN)
-    go acc_xis acc_cos !lc binders inner_ki _ []
-        -- The !lc makes the function strict in the lifting context
-        -- which means GHC can unbox that pair.  A modest win.
-      = (reverse acc_xis, reverse acc_cos, kind_co)
-      where
-        final_kind = mkPiTys binders inner_ki
-        kind_co | noFreeVarsOfType final_kind = MRefl
-                | otherwise                   = MCo $ liftCoSubst Nominal lc final_kind
-
-    go acc_xis acc_cos lc (binder:binders) inner_ki (role:roles) ((xi,co):args)
-      = -- By Note [Rewriting] in GHC.Tc.Solver.Rewrite 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 rewritten 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; see #18502
-         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
-      = let co1 = liftCoSubst Nominal lc inner_ki
-            co1_kind              = coercionKind co1
-            unrewritten_tys       = map (coercionRKind . snd) args
-            (arg_cos, res_co)     = decomposePiCos co1 co1_kind unrewritten_tys
-            casted_args           = assertPpr (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 rewritten_kind _ = co1_kind
-            (bndrs, new_inner)    = splitPiTys rewritten_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 `mkTransMCoL` 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 analogous case in rewrite_args_fast
-           -- in GHC.Tc.Solver.Rewrite:
-           -- 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/GHC/Core/FamInstEnv.hs b/compiler/GHC/Core/FamInstEnv.hs
index 5429a2ec4a..c1715cc270 100644
--- a/compiler/GHC/Core/FamInstEnv.hs
+++ b/compiler/GHC/Core/FamInstEnv.hs
@@ -45,6 +45,7 @@ import GHC.Core.TyCo.Rep
 import GHC.Core.TyCon
 import GHC.Core.Coercion
 import GHC.Core.Coercion.Axiom
+import GHC.Core.Reduction
 import GHC.Types.Var.Set
 import GHC.Types.Var.Env
 import GHC.Types.Name
@@ -1099,7 +1100,7 @@ but we also need to handle closed ones when normalising a type:
 reduceTyFamApp_maybe :: FamInstEnvs
                      -> Role              -- Desired role of result coercion
                      -> TyCon -> [Type]
-                     -> Maybe (Coercion, Type)
+                     -> Maybe Reduction
 -- Attempt to do a *one-step* reduction of a type-family application
 --    but *not* newtypes
 -- Works on type-synonym families always; data-families only if
@@ -1130,20 +1131,18 @@ reduceTyFamApp_maybe envs role tc tys
       -- NB: Allow multiple matches because of compatible overlap
 
   = let co = mkUnbranchedAxInstCo role ax inst_tys inst_cos
-        ty = coercionRKind co
-    in Just (co, ty)
+    in Just $ coercionRedn co
 
   | Just ax <- isClosedSynFamilyTyConWithAxiom_maybe tc
   , Just (ind, inst_tys, inst_cos) <- chooseBranch ax tys
   = let co = mkAxInstCo role ax ind inst_tys inst_cos
-        ty = coercionRKind co
-    in Just (co, ty)
+    in Just $ coercionRedn co
 
   | Just ax           <- isBuiltInSynFamTyCon_maybe tc
   , Just (coax,ts,ty) <- sfMatchFam ax tys
   , role == coaxrRole coax
   = let co = mkAxiomRuleCo coax (zipWith mkReflCo (coaxrAsmpRoles coax) ts)
-    in Just (co, ty)
+    in Just $ mkReduction co ty
 
   | otherwise
   = Nothing
@@ -1274,11 +1273,12 @@ case by that route too, but it hasn't happened in practice yet!
 -}
 
 topNormaliseType :: FamInstEnvs -> Type -> Type
-topNormaliseType env ty = case topNormaliseType_maybe env ty of
-                            Just (_co, ty') -> ty'
-                            Nothing         -> ty
+topNormaliseType env ty
+  = case topNormaliseType_maybe env ty of
+      Just redn -> reductionReducedType redn
+      Nothing   -> ty
 
-topNormaliseType_maybe :: FamInstEnvs -> Type -> Maybe (Coercion, Type)
+topNormaliseType_maybe :: FamInstEnvs -> Type -> Maybe Reduction
 
 -- ^ Get rid of *outermost* (or toplevel)
 --      * type function redex
@@ -1297,12 +1297,8 @@ topNormaliseType_maybe :: FamInstEnvs -> Type -> Maybe (Coercion, Type)
 -- original type, and the returned coercion is always homogeneous.
 topNormaliseType_maybe env 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) }
+       ; let hredn = mkHetReduction (mkReduction co nty) mkind_co
+       ; return $ homogeniseHetRedn Representational hredn }
   where
     stepper = unwrapNewTypeStepper' `composeSteppers` tyFamStepper
 
@@ -1317,18 +1313,19 @@ topNormaliseType_maybe env ty
     tyFamStepper :: NormaliseStepper (Coercion, MCoercionN)
     tyFamStepper rec_nts tc tys  -- Try to step a type/data family
       = case topReduceTyFamApp_maybe env tc tys of
-          Just (co, rhs, res_co) -> NS_Step rec_nts rhs (co, res_co)
-          _                      -> NS_Done
+          Just (HetReduction (Reduction co rhs) res_co)
+            -> NS_Step rec_nts rhs (co, res_co)
+          _ -> NS_Done
 
 ---------------
-normaliseTcApp :: FamInstEnvs -> Role -> TyCon -> [Type] -> (Coercion, Type)
+normaliseTcApp :: FamInstEnvs -> Role -> TyCon -> [Type] -> Reduction
 -- See comments on normaliseType for the arguments of this function
 normaliseTcApp env role tc tys
   = initNormM env role (tyCoVarsOfTypes tys) $
     normalise_tc_app tc tys
 
 -- See Note [Normalising types] about the LiftingContext
-normalise_tc_app :: TyCon -> [Type] -> NormM (Coercion, Type)
+normalise_tc_app :: TyCon -> [Type] -> NormM Reduction
 normalise_tc_app tc tys
   | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc tys
   , not (isFamFreeTyCon tc)  -- Expand and try again
@@ -1341,76 +1338,70 @@ normalise_tc_app tc tys
   = -- A type-family application
     do { env <- getEnv
        ; role <- getRole
-       ; (args_co, ntys, res_co) <- normalise_tc_args tc tys
+       ; ArgsReductions redns@(Reductions args_cos 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 (assemble_result role nty
-                                             (args_co `mkTransCo` first_co `mkTransCo` rest_co)
-                                             res_co) }
+           Just redn1
+             -> do { redn2 <- normalise_reduction redn1
+                   ; let redn3 = mkTyConAppCo role tc args_cos `mkTransRedn` redn2
+                   ; return $ assemble_result role redn3 res_co }
            _ -> -- No unique matching family instance exists;
                 -- we do not do anything
-                return (assemble_result role (mkTyConApp tc ntys) args_co res_co) }
+                return $
+                  assemble_result role (mkTyConAppRedn role tc redns) 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, res_co) <- normalise_tc_args tc tys
+    do { ArgsReductions redns res_co <- normalise_tc_args tc tys
        ; role <- getRole
-       ; return (assemble_result role (mkTyConApp tc ntys) args_co res_co) }
+       ; return $
+            assemble_result role (mkTyConAppRedn role tc redns) 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
+                    -> Reduction  -- orig_ty ~r nty, possibly heterogeneous (nty possibly of changed kind)
                     -> MCoercionN -- 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 `mkCastTyMCo` mkSymMCo kind_co
-        final_co     = mkCoherenceRightMCo r nty (mkSymMCo kind_co) orig_to_nty
+                    -> Reduction  -- orig_ty ~r nty_casted
+                                  -- where nty_casted has same kind as orig_ty
+    assemble_result r redn kind_co
+      = mkCoherenceRightMRedn r redn (mkSymMCo kind_co)
 
 ---------------
 -- | Try to simplify a type-family application, by *one* step
--- If topReduceTyFamApp_maybe env r F tys = Just (co, rhs, res_co)
+-- If topReduceTyFamApp_maybe env r F tys = Just (HetReduction (Reduction co rhs) res_co)
 -- then    co     :: F tys ~R# rhs
 --         res_co :: typeKind(F tys) ~ typeKind(rhs)
 -- Type families and data families; always Representational role
 topReduceTyFamApp_maybe :: FamInstEnvs -> TyCon -> [Type]
-                        -> Maybe (Coercion, Type, MCoercion)
+                        -> Maybe HetReduction
 topReduceTyFamApp_maybe envs fam_tc arg_tys
   | isFamilyTyCon fam_tc   -- type families and data families
-  , Just (co, rhs) <- reduceTyFamApp_maybe envs role fam_tc ntys
-  = Just (args_co `mkTransCo` co, rhs, res_co)
+  , Just redn <- reduceTyFamApp_maybe envs role fam_tc ntys
+  = Just $
+      mkHetReduction
+        (mkTyConAppCo role fam_tc args_cos `mkTransRedn` redn)
+        res_co
   | otherwise
   = Nothing
   where
     role = Representational
-    (args_co, ntys, res_co) = initNormM envs role (tyCoVarsOfTypes arg_tys) $
-                              normalise_tc_args fam_tc arg_tys
-
-normalise_tc_args :: TyCon -> [Type]             -- tc tys
-                  -> NormM (Coercion, [Type], MCoercionN)
-                  -- (co, new_tys), where
-                  -- co :: tc tys ~ tc new_tys; might not be homogeneous
-                  -- res_co :: typeKind(tc tys) ~N typeKind(tc new_tys)
+    ArgsReductions (Reductions args_cos ntys) res_co
+      = initNormM envs role (tyCoVarsOfTypes arg_tys)
+      $ normalise_tc_args fam_tc arg_tys
+
+normalise_tc_args :: TyCon -> [Type] -> NormM ArgsReductions
 normalise_tc_args tc tys
   = do { role <- getRole
-       ; (args_cos, nargs, res_co) <- normalise_args (tyConKind tc) (tyConRolesX role tc) tys
-       ; return (mkTyConAppCo role tc args_cos, nargs, res_co) }
+       ; normalise_args (tyConKind tc) (tyConRolesX role tc) tys }
 
 ---------------
 normaliseType :: FamInstEnvs
               -> Role  -- desired role of coercion
-              -> Type -> (Coercion, Type)
+              -> Type -> Reduction
 normaliseType env role ty
   = initNormM env role (tyCoVarsOfType ty) $ normalise_type ty
 
-normalise_type :: Type                     -- old type
-               -> NormM (Coercion, Type)   -- (coercion, new type), where
-                                           -- co :: old-type ~ new_type
+normalise_type :: Type -> NormM Reduction
 -- Normalise the input type, by eliminating *all* type-function redexes
 -- but *not* newtypes (which are visible to the programmer)
 -- Returns with Refl if nothing happens
@@ -1422,106 +1413,105 @@ normalise_type :: Type                     -- old type
 normalise_type ty
   = go ty
   where
+    go :: Type -> NormM Reduction
     go (TyConApp tc tys) = normalise_tc_app tc tys
-    go ty@(LitTy {})     = do { r <- getRole
-                              ; return (mkReflCo r ty, ty) }
+    go ty@(LitTy {})
+      = do { r <- getRole
+           ; return $ mkReflRedn r ty }
     go (AppTy ty1 ty2) = go_app_tys ty1 [ty2]
 
-    go ty@(FunTy { ft_mult = w, ft_arg = ty1, ft_res = ty2 })
-      = do { (co1, nty1) <- go ty1
-           ; (co2, nty2) <- go ty2
-           ; (wco, wty) <- withRole Nominal $ go w
+    go (FunTy { ft_af = vis, ft_mult = w, ft_arg = ty1, ft_res = ty2 })
+      = do { arg_redn <- go ty1
+           ; res_redn <- go ty2
+           ; w_redn <- withRole Nominal $ go w
            ; r <- getRole
-           ; return (mkFunCo r wco co1 co2, ty { ft_mult = wty, ft_arg = nty1, ft_res = nty2 }) }
+           ; return $ mkFunRedn r vis w_redn arg_redn res_redn }
     go (ForAllTy (Bndr tcvar vis) ty)
-      = do { (lc', tv', h, ki') <- normalise_var_bndr tcvar
-           ; (co, nty)          <- withLC lc' $ normalise_type ty
-           ; let tv2 = setTyVarKind tv' ki'
-           ; return (mkForAllCo tv' h co, ForAllTy (Bndr tv2 vis) nty) }
+      = do { (lc', tv', k_redn) <- normalise_var_bndr tcvar
+           ; redn <- withLC lc' $ normalise_type ty
+           ; return $ mkForAllRedn vis tv' k_redn redn }
     go (TyVarTy tv)    = normalise_tyvar tv
     go (CastTy ty co)
-      = do { (nco, nty) <- go ty
+      = do { redn <- go ty
            ; lc <- getLC
            ; let co' = substRightCo lc co
-           ; return (castCoercionKind2 nco Nominal ty nty co co'
-                    , mkCastTy nty co') }
+           ; return $ mkCastRedn2 Nominal ty co redn co'
+             --       ^^^^^^^^^^^ uses castCoercionKind2
+           }
     go (CoercionTy co)
       = do { lc <- getLC
            ; r <- getRole
-           ; let right_co = substRightCo lc co
-           ; return ( mkProofIrrelCo r
-                         (liftCoSubst Nominal lc (coercionType co))
-                         co right_co
-                    , mkCoercionTy right_co ) }
+           ; let kco = liftCoSubst Nominal lc (coercionType co)
+                 co' = substRightCo lc co
+           ; return $ mkProofIrrelRedn r kco co co' }
 
     go_app_tys :: Type   -- function
                -> [Type] -- args
-               -> NormM (Coercion, Type)
+               -> NormM Reduction
     -- cf. GHC.Tc.Solver.Rewrite.rewrite_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
+      = do { fun_redn@(Reduction fun_co nfun) <- go fun_ty
            ; case tcSplitTyConApp_maybe nfun of
                Just (tc, xis) ->
-                 do { (second_co, nty) <- go (mkTyConApp tc (xis ++ arg_tys))
+                 do { redn <- go (mkTyConApp tc (xis ++ arg_tys))
                    -- rewrite_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) }
+                    ; return $
+                        mkAppCos fun_co (map mkNomReflCo arg_tys) `mkTransRedn` redn }
                Nothing ->
-                 do { (args_cos, nargs, res_co) <- normalise_args (typeKind nfun)
-                                                                  (repeat Nominal)
-                                                                  arg_tys
+                 do { ArgsReductions redns 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 `mkCastTyMCo` mkSymMCo res_co
-                          final_co = mkCoherenceRightMCo role nty (mkSymMCo res_co) nco
-                    ; return (final_co, nty_casted) } }
+                    ; return $
+                        mkCoherenceRightMRedn role
+                          (mkAppRedns fun_redn redns)
+                          (mkSymMCo res_co) } }
 
 normalise_args :: Kind    -- of the function
                -> [Role]  -- roles at which to normalise args
                -> [Type]  -- args
-               -> NormM ([Coercion], [Type], MCoercion)
--- 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)
+               -> NormM ArgsReductions
+-- returns ArgsReductions (Reductions cos xis) res_co,
+-- where each xi is the normalised version of the corresponding type,
+-- each co is orig_arg ~ xi, and 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. GHC.Tc.Solver.Rewrite.rewrite_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, mkSymMCo res_co) }
+       ; return $ simplifyArgsWorker ki_binders inner_ki fvs roles normed_args }
   where
     (ki_binders, inner_ki) = splitPiTys fun_ki
     fvs = tyCoVarsOfTypes args
 
-    -- rewriter 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
+      = withRole role $ normalise_type ty
 
-normalise_tyvar :: TyVar -> NormM (Coercion, Type)
+normalise_tyvar :: TyVar -> NormM Reduction
 normalise_tyvar tv
   = assert (isTyVar tv) $
     do { lc <- getLC
        ; r  <- getRole
        ; return $ case liftCoSubstTyVar lc r tv of
-           Just co -> (co, coercionRKind co)
-           Nothing -> (mkReflCo r ty, ty) }
-  where ty = mkTyVarTy tv
+           Just co -> coercionRedn co
+           Nothing -> mkReflRedn r (mkTyVarTy tv) }
+
+normalise_reduction :: Reduction -> NormM Reduction
+normalise_reduction (Reduction co ty)
+  = do { redn' <- normalise_type ty
+       ; return $ co `mkTransRedn` redn' }
 
-normalise_var_bndr :: TyCoVar -> NormM (LiftingContext, TyCoVar, Coercion, Kind)
+normalise_var_bndr :: TyCoVar -> NormM (LiftingContext, TyCoVar, Reduction)
 normalise_var_bndr tcvar
   -- works for both tvar and covar
   = do { lc1 <- getLC
        ; env <- getEnv
        ; let callback lc ki = runNormM (normalise_type ki) env lc Nominal
-       ; return $ liftCoSubstVarBndrUsing callback lc1 tcvar }
+       ; return $ liftCoSubstVarBndrUsing reductionCoercion callback lc1 tcvar }
 
 -- | a monad for the normalisation functions, reading 'FamInstEnvs',
 -- a 'LiftingContext', and a 'Role'.
diff --git a/compiler/GHC/Core/Opt/Simplify.hs b/compiler/GHC/Core/Opt/Simplify.hs
index f7853a551a..11b0b50036 100644
--- a/compiler/GHC/Core/Opt/Simplify.hs
+++ b/compiler/GHC/Core/Opt/Simplify.hs
@@ -25,6 +25,7 @@ import GHC.Core.Opt.OccurAnal ( occurAnalyseExpr )
 import GHC.Core.Make       ( FloatBind, mkImpossibleExpr, castBottomExpr )
 import qualified GHC.Core.Make
 import GHC.Core.Coercion hiding ( substCo, substCoVar )
+import GHC.Core.Reduction
 import GHC.Core.Coercion.Opt    ( optCoercion )
 import GHC.Core.FamInstEnv      ( FamInstEnv, topNormaliseType_maybe )
 import GHC.Core.DataCon
@@ -3054,7 +3055,7 @@ improveSeq :: (FamInstEnv, FamInstEnv) -> SimplEnv
            -> SimplM (SimplEnv, OutExpr, OutId)
 -- Note [Improving seq]
 improveSeq fam_envs env scrut case_bndr case_bndr1 [Alt DEFAULT _ _]
-  | Just (co, ty2) <- topNormaliseType_maybe fam_envs (idType case_bndr1)
+  | Just (Reduction co ty2) <- topNormaliseType_maybe fam_envs (idType case_bndr1)
   = do { case_bndr2 <- newId (fsLit "nt") Many ty2
         ; let rhs  = DoneEx (Var case_bndr2 `Cast` mkSymCo co) Nothing
               env2 = extendIdSubst env case_bndr rhs
diff --git a/compiler/GHC/Core/Opt/WorkWrap/Utils.hs b/compiler/GHC/Core/Opt/WorkWrap/Utils.hs
index c3e708c60d..beafa01b1c 100644
--- a/compiler/GHC/Core/Opt/WorkWrap/Utils.hs
+++ b/compiler/GHC/Core/Opt/WorkWrap/Utils.hs
@@ -30,6 +30,7 @@ import GHC.Core.Type
 import GHC.Core.Multiplicity
 import GHC.Core.Predicate ( isClassPred )
 import GHC.Core.Coercion
+import GHC.Core.Reduction
 import GHC.Core.FamInstEnv
 import GHC.Core.TyCon
 import GHC.Core.TyCon.RecWalk
@@ -1239,7 +1240,7 @@ findTypeShape fam_envs ty
        = TsUnk
 
     go_tc rec_tc tc tc_args
-       | Just (_, rhs, _) <- topReduceTyFamApp_maybe fam_envs tc tc_args
+       | Just (HetReduction (Reduction _ rhs) _) <- topReduceTyFamApp_maybe fam_envs tc tc_args
        = go rec_tc rhs
 
        | Just con <- tyConSingleAlgDataCon_maybe tc
diff --git a/compiler/GHC/Core/Reduction.hs b/compiler/GHC/Core/Reduction.hs
new file mode 100644
index 0000000000..254b4420e1
--- /dev/null
+++ b/compiler/GHC/Core/Reduction.hs
@@ -0,0 +1,892 @@
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE FlexibleContexts #-}
+
+module GHC.Core.Reduction
+  (
+     -- * Reductions
+     Reduction(..), ReductionN, ReductionR, HetReduction(..),
+     Reductions(..),
+     mkReduction, mkReductions, mkHetReduction, coercionRedn,
+     reductionOriginalType,
+     downgradeRedn, mkSubRedn,
+     mkTransRedn, mkCoherenceRightRedn, mkCoherenceRightMRedn,
+     mkCastRedn1, mkCastRedn2,
+     mkReflRedn, mkGReflRightRedn, mkGReflRightMRedn,
+     mkGReflLeftRedn, mkGReflLeftMRedn,
+     mkAppRedn, mkAppRedns, mkFunRedn,
+     mkForAllRedn, mkHomoForAllRedn, mkTyConAppRedn, mkClassPredRedn,
+     mkProofIrrelRedn, mkReflCoRedn,
+     homogeniseHetRedn,
+     unzipRedns,
+
+     -- * Rewriting type arguments
+     ArgsReductions(..),
+     simplifyArgsWorker
+
+  ) where
+
+import GHC.Prelude
+
+import GHC.Core.Class      ( Class(classTyCon) )
+import GHC.Core.Coercion
+import GHC.Core.Predicate  ( mkClassPred )
+import GHC.Core.TyCon      ( TyCon )
+import GHC.Core.Type
+
+import GHC.Data.Pair       ( Pair(Pair) )
+
+import GHC.Types.Var       ( setTyVarKind )
+import GHC.Types.Var.Env   ( mkInScopeSet )
+import GHC.Types.Var.Set   ( TyCoVarSet )
+
+import GHC.Utils.Misc      ( HasDebugCallStack, equalLength )
+import GHC.Utils.Outputable
+import GHC.Utils.Panic     ( assertPpr, panic )
+
+{-
+%************************************************************************
+%*                                                                      *
+      Reductions
+%*                                                                      *
+%************************************************************************
+
+Note [The Reduction type]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+Many functions in the type-checker rewrite a type, using Given type equalitie
+or type-family reductions, and return a Reduction, which is just a pair of the
+coercion and the RHS type of the coercion:
+  data Reduction = Reduction Coercion !Type
+
+The order of the arguments to the constructor serves as a reminder
+of what the Type is.  In
+    Reduction co ty
+`ty` appears to the right of `co`, reminding us that we must have:
+    co :: unrewritten_ty ~ ty
+
+Example functions that use this datatype:
+   GHC.Core.FamInstEnv.topNormaliseType_maybe
+     :: FamInstEnvs -> Type -> Maybe Reduction
+   GHC.Tc.Solver.Rewrite.rewrite
+     :: CtEvidence -> TcType -> TcS Reduction
+
+Having Reduction as a data type, with a strict Type field, rather than using
+a pair (Coercion,Type) gives several advantages (see #20161)
+* The strictness in Type improved performance in rewriting of type families
+  (around 2.5% improvement in T9872),
+* Compared to the situation before, it gives improved consistency around
+  orientation of rewritings, as a Reduction is always left-to-right
+  (the coercion's RHS type is always the type stored in the 'Reduction').
+  No more 'mkSymCo's needed to convert between left-to-right and right-to-left.
+
+One could imagine storing the LHS type of the coercion in the Reduction as well,
+but in fact `reductionOriginalType` is very seldom used, so it's not worth it.
+-}
+
+-- | A 'Reduction' is the result of an operation that rewrites a type @ty_in@.
+-- The 'Reduction' includes the rewritten type @ty_out@ and a 'Coercion' @co@
+-- such that @co :: ty_in ~ ty_out@, where the role of the coercion is determined
+-- by the context. That is, the LHS type of the coercion is the original type
+-- @ty_in@, while its RHS type is the rewritten type @ty_out@.
+--
+-- A Reduction is always homogeneous, unless it is wrapped inside a 'HetReduction',
+-- which separately stores the kind coercion.
+--
+-- See Note [The Reduction type].
+data Reduction =
+  Reduction
+    { reductionCoercion    :: Coercion
+    , reductionReducedType :: !Type
+    }
+-- N.B. the 'Coercion' field must be lazy: see for instance GHC.Tc.Solver.Rewrite.rewrite_tyvar2
+-- which returns an error in the 'Coercion' field when dealing with a Derived constraint
+-- (which is OK as this Coercion gets ignored later).
+-- We might want to revisit the strictness once Deriveds are removed.
+
+-- | Stores a heterogeneous reduction.
+--
+-- The stored kind coercion must relate the kinds of the
+-- stored reduction. That is, in @HetReduction (Reduction co xi) kco@,
+-- we must have:
+--
+-- >  co :: ty ~ xi
+-- > kco :: typeKind ty ~ typeKind xi
+data HetReduction =
+  HetReduction
+    Reduction
+    MCoercionN
+  -- N.B. strictness annotations don't seem to make a difference here
+
+-- | Create a heterogeneous reduction.
+--
+-- Pre-condition: the provided kind coercion (second argument)
+-- relates the kinds of the stored reduction.
+-- That is, if the coercion stored in the 'Reduction' is of the form
+--
+-- > co :: ty ~ xi
+--
+-- Then the kind coercion supplied must be of the form:
+--
+-- > kco :: typeKind ty ~ typeKind xi
+mkHetReduction :: Reduction  -- ^ heterogeneous reduction
+               -> MCoercionN -- ^ kind coercion
+               -> HetReduction
+mkHetReduction redn mco = HetReduction redn mco
+{-# INLINE mkHetReduction #-}
+
+-- | Homogenise a heterogeneous reduction.
+--
+-- Given @HetReduction (Reduction co xi) kco@, with
+--
+-- >  co :: ty ~ xi
+-- > kco :: typeKind(ty) ~ typeKind(xi)
+--
+-- this returns the homogeneous reduction:
+--
+-- > hco :: ty ~ ( xi |> sym kco )
+homogeniseHetRedn :: Role -> HetReduction -> Reduction
+homogeniseHetRedn role (HetReduction redn kco)
+  = mkCoherenceRightMRedn role redn (mkSymMCo kco)
+{-# INLINE homogeniseHetRedn #-}
+
+-- | Create a 'Reduction' from a pair of a 'Coercion' and a 'Type.
+--
+-- Pre-condition: the RHS type of the coercion matches the provided type
+-- (perhaps up to zonking).
+--
+-- Use 'coercionRedn' when you only have the coercion.
+mkReduction :: Coercion -> Type -> Reduction
+mkReduction co ty = Reduction co ty
+{-# INLINE mkReduction #-}
+
+instance Outputable Reduction where
+  ppr redn =
+    braces $ vcat
+      [ text "reductionOriginalType:" <+> ppr (reductionOriginalType redn)
+      , text " reductionReducedType:" <+> ppr (reductionReducedType redn)
+      , text "    reductionCoercion:" <+> ppr (reductionCoercion redn)
+      ]
+
+-- | A 'Reduction' in which the 'Coercion' has 'Nominal' role.
+type ReductionN = Reduction
+
+-- | A 'Reduction' in which the 'Coercion' has 'Representational' role.
+type ReductionR = Reduction
+
+-- | Get the original, unreduced type corresponding to a 'Reduction'.
+--
+-- This is obtained by computing the LHS kind of the stored coercion,
+-- which may be slow.
+reductionOriginalType :: Reduction -> Type
+reductionOriginalType = coercionLKind . reductionCoercion
+{-# INLINE reductionOriginalType #-}
+
+-- | Turn a 'Coercion' into a 'Reduction'
+-- by inspecting the RHS type of the coercion.
+--
+-- Prefer using 'mkReduction' when you already know
+-- the RHS type of the coercion, to avoid computing it anew.
+coercionRedn :: Coercion -> Reduction
+coercionRedn co = Reduction co (coercionRKind co)
+{-# INLINE coercionRedn #-}
+
+-- | Downgrade the role of the coercion stored in the 'Reduction'.
+downgradeRedn :: Role -- ^ desired role
+              -> Role -- ^ current role
+              -> Reduction
+              -> Reduction
+downgradeRedn new_role old_role redn@(Reduction co _)
+  = redn { reductionCoercion = downgradeRole new_role old_role co }
+{-# INLINE downgradeRedn #-}
+
+-- | Downgrade the role of the coercion stored in the 'Reduction',
+-- from 'Nominal' to 'Representational'.
+mkSubRedn :: Reduction -> Reduction
+mkSubRedn redn@(Reduction co _) = redn { reductionCoercion = mkSubCo co }
+{-# INLINE mkSubRedn #-}
+
+-- | Compose a reduction with a coercion on the left.
+--
+-- Pre-condition: the provided coercion's RHS type must match the LHS type
+-- of the coercion that is stored in the reduction.
+mkTransRedn :: Coercion -> Reduction -> Reduction
+mkTransRedn co1 redn@(Reduction co2 _)
+  = redn { reductionCoercion = co1 `mkTransCo` co2 }
+{-# INLINE mkTransRedn #-}
+
+-- | The reflexive reduction.
+mkReflRedn :: Role -> Type -> Reduction
+mkReflRedn r ty = mkReduction (mkReflCo r ty) ty
+
+-- | Create a 'Reduction' from a kind cast, in which
+-- the casted type is the rewritten type.
+--
+-- Given @ty :: k1@, @mco :: k1 ~ k2@,
+-- produces the 'Reduction' @ty ~res_co~> (ty |> mco)@
+-- at the given 'Role'.
+mkGReflRightRedn :: Role -> Type -> CoercionN -> Reduction
+mkGReflRightRedn role ty co
+  = mkReduction
+      (mkGReflRightCo role ty co)
+      (mkCastTy ty co)
+{-# INLINE mkGReflRightRedn #-}
+
+-- | Create a 'Reduction' from a kind cast, in which
+-- the casted type is the rewritten type.
+--
+-- Given @ty :: k1@, @mco :: k1 ~ k2@,
+-- produces the 'Reduction' @ty ~res_co~> (ty |> mco)@
+-- at the given 'Role'.
+mkGReflRightMRedn :: Role -> Type -> MCoercionN -> Reduction
+mkGReflRightMRedn role ty mco
+  = mkReduction
+      (mkGReflRightMCo role ty mco)
+      (mkCastTyMCo ty mco)
+{-# INLINE mkGReflRightMRedn #-}
+
+-- | Create a 'Reduction' from a kind cast, in which
+-- the casted type is the original (non-rewritten) type.
+--
+-- Given @ty :: k1@, @mco :: k1 ~ k2@,
+-- produces the 'Reduction' @(ty |> mco) ~res_co~> ty@
+-- at the given 'Role'.
+mkGReflLeftRedn :: Role -> Type -> CoercionN -> Reduction
+mkGReflLeftRedn role ty co
+  = mkReduction
+      (mkGReflLeftCo role ty co)
+      ty
+{-# INLINE mkGReflLeftRedn #-}
+
+-- | Create a 'Reduction' from a kind cast, in which
+-- the casted type is the original (non-rewritten) type.
+--
+-- Given @ty :: k1@, @mco :: k1 ~ k2@,
+-- produces the 'Reduction' @(ty |> mco) ~res_co~> ty@
+-- at the given 'Role'.
+mkGReflLeftMRedn :: Role -> Type -> MCoercionN -> Reduction
+mkGReflLeftMRedn role ty mco
+  = mkReduction
+      (mkGReflLeftMCo role ty mco)
+      ty
+{-# INLINE mkGReflLeftMRedn #-}
+
+-- | Apply a cast to the result of a 'Reduction'.
+--
+-- Given a 'Reduction' @ty1 ~co1~> (ty2 :: k2)@ and a kind coercion @kco@
+-- with LHS kind @k2@, produce a new 'Reduction' @ty1 ~co2~> ( ty2 |> kco )@
+-- of the given 'Role' (which must match the role of the coercion stored
+-- in the 'Reduction' argument).
+mkCoherenceRightRedn :: Role -> Reduction -> CoercionN -> Reduction
+mkCoherenceRightRedn r (Reduction co1 ty2) kco
+  = mkReduction
+      (mkCoherenceRightCo r ty2 kco co1)
+      (mkCastTy ty2 kco)
+{-# INLINE mkCoherenceRightRedn #-}
+
+-- | Apply a cast to the result of a 'Reduction', using an 'MCoercionN'.
+--
+-- Given a 'Reduction' @ty1 ~co1~> (ty2 :: k2)@ and a kind coercion @mco@
+-- with LHS kind @k2@, produce a new 'Reduction' @ty1 ~co2~> ( ty2 |> mco )@
+-- of the given 'Role' (which must match the role of the coercion stored
+-- in the 'Reduction' argument).
+mkCoherenceRightMRedn :: Role -> Reduction -> MCoercionN -> Reduction
+mkCoherenceRightMRedn r (Reduction co1 ty2) kco
+  = mkReduction
+      (mkCoherenceRightMCo r ty2 kco co1)
+      (mkCastTyMCo ty2 kco)
+{-# INLINE mkCoherenceRightMRedn #-}
+
+-- | Apply a cast to a 'Reduction', casting both the original and the reduced type.
+--
+-- Given @cast_co@ and 'Reduction' @ty ~co~> xi@, this function returns
+-- the 'Reduction' @(ty |> cast_co) ~return_co~> (xi |> cast_co)@
+-- of the given 'Role' (which must match the role of the coercion stored
+-- in the 'Reduction' argument).
+--
+-- Pre-condition: the 'Type' passed in is the same as the LHS type
+-- of the coercion stored in the 'Reduction'.
+mkCastRedn1 :: Role
+            -> Type      -- ^ original type
+            -> CoercionN -- ^ coercion to cast with
+            -> Reduction -- ^ rewritten type, with rewriting coercion
+            -> Reduction
+mkCastRedn1 r ty cast_co (Reduction co xi)
+  -- co :: ty ~r ty'
+  -- return_co :: (ty |> cast_co) ~r (ty' |> cast_co)
+  = mkReduction
+      (castCoercionKind1 co r ty xi cast_co)
+      (mkCastTy xi cast_co)
+{-# INLINE mkCastRedn1 #-}
+
+-- | Apply casts on both sides of a 'Reduction' (of the given 'Role').
+--
+-- Use 'mkCastRedn1' when you want to cast both the original and reduced types
+-- in a 'Reduction' using the same coercion.
+--
+-- Pre-condition: the 'Type' passed in is the same as the LHS type
+-- of the coercion stored in the 'Reduction'.
+mkCastRedn2 :: Role
+            -> Type      -- ^ original type
+            -> CoercionN -- ^ coercion to cast with on the left
+            -> Reduction -- ^ rewritten type, with rewriting coercion
+            -> CoercionN -- ^ coercion to cast with on the right
+            -> Reduction
+mkCastRedn2 r ty cast_co (Reduction nco nty) cast_co'
+  = mkReduction
+      (castCoercionKind2 nco r ty nty cast_co cast_co')
+      (mkCastTy nty cast_co')
+{-# INLINE mkCastRedn2 #-}
+
+-- | Apply one 'Reduction' to another.
+--
+-- Combines 'mkAppCo' and 'mkAppTy`.
+mkAppRedn :: Reduction -> Reduction -> Reduction
+mkAppRedn (Reduction co1 ty1) (Reduction co2 ty2)
+  = mkReduction (mkAppCo co1 co2) (mkAppTy ty1 ty2)
+{-# INLINE mkAppRedn #-}
+
+-- | Create a function 'Reduction'.
+--
+-- Combines 'mkFunCo' and 'mkFunTy'.
+mkFunRedn :: Role
+          -> AnonArgFlag
+          -> ReductionN -- ^ multiplicity reduction
+          -> Reduction  -- ^ argument reduction
+          -> Reduction  -- ^ result reduction
+          -> Reduction
+mkFunRedn r vis
+  (Reduction w_co w_ty)
+  (Reduction arg_co arg_ty)
+  (Reduction res_co res_ty)
+    = mkReduction
+        (mkFunCo r w_co arg_co res_co)
+        (mkFunTy vis w_ty arg_ty res_ty)
+{-# INLINE mkFunRedn #-}
+
+-- | Create a 'Reduction' associated to a Π type,
+-- from a kind 'Reduction' and a body 'Reduction'.
+--
+-- Combines 'mkForAllCo' and 'mkForAllTy'.
+mkForAllRedn :: ArgFlag
+             -> TyVar
+             -> ReductionN -- ^ kind reduction
+             -> Reduction  -- ^ body reduction
+             -> Reduction
+mkForAllRedn vis tv1 (Reduction h ki') (Reduction co ty)
+  = mkReduction
+      (mkForAllCo tv1 h co)
+      (mkForAllTy tv2 vis ty)
+  where
+    tv2 = setTyVarKind tv1 ki'
+{-# INLINE mkForAllRedn #-}
+
+-- | Create a 'Reduction' of a quantified type from a
+-- 'Reduction' of the body.
+--
+-- Combines 'mkHomoForAllCos' and 'mkForAllTys'.
+mkHomoForAllRedn :: [TyVarBinder] -> Reduction -> Reduction
+mkHomoForAllRedn bndrs (Reduction co ty)
+  = mkReduction
+      (mkHomoForAllCos (binderVars bndrs) co)
+      (mkForAllTys bndrs ty)
+{-# INLINE mkHomoForAllRedn #-}
+
+-- | Create a 'Reduction' from a coercion between coercions.
+--
+-- Combines 'mkProofIrrelCo' and 'mkCoercionTy'.
+mkProofIrrelRedn :: Role      -- ^ role of the created coercion, "r"
+                 -> CoercionN -- ^ co :: phi1 ~N phi2
+                 -> Coercion  -- ^ g1 :: phi1
+                 -> Coercion  -- ^ g2 :: phi2
+                 -> Reduction -- ^ res_co :: g1 ~r g2
+mkProofIrrelRedn role co g1 g2
+  = mkReduction
+      (mkProofIrrelCo role co g1 g2)
+      (mkCoercionTy g2)
+{-# INLINE mkProofIrrelRedn #-}
+
+-- | Create a reflexive 'Reduction' whose RHS is the given 'Coercion',
+-- with the specified 'Role'.
+mkReflCoRedn :: Role -> Coercion -> Reduction
+mkReflCoRedn role co
+  = mkReduction
+      (mkReflCo role co_ty)
+      co_ty
+  where
+    co_ty = mkCoercionTy co
+{-# INLINE mkReflCoRedn #-}
+
+-- | A collection of 'Reduction's where the coercions and the types are stored separately.
+--
+-- Use 'unzipRedns' to obtain 'Reductions' from a list of 'Reduction's.
+--
+-- This datatype is used in 'mkAppRedns', 'mkClassPredRedns' and 'mkTyConAppRedn',
+-- which expect separate types and coercions.
+--
+-- Invariant: the two stored lists are of the same length,
+-- and the RHS type of each coercion is the corresponding type.
+data Reductions = Reductions [Coercion] [Type]
+
+-- | Create 'Reductions' from individual lists of coercions and types.
+--
+-- The lists should be of the same length, and the RHS type of each coercion
+-- should match the specified type in the other list.
+mkReductions :: [Coercion] -> [Type] -> Reductions
+mkReductions cos tys = Reductions cos tys
+{-# INLINE mkReductions #-}
+
+-- | Combines 'mkAppCos' and 'mkAppTys'.
+mkAppRedns :: Reduction -> Reductions -> Reduction
+mkAppRedns (Reduction co ty) (Reductions cos tys)
+  = mkReduction (mkAppCos co cos) (mkAppTys ty tys)
+{-# INLINE mkAppRedns #-}
+
+-- | 'TyConAppCo' for 'Reduction's: combines 'mkTyConAppCo' and `mkTyConApp`.
+mkTyConAppRedn :: Role -> TyCon -> Reductions -> Reduction
+mkTyConAppRedn role tc (Reductions cos tys)
+  = mkReduction (mkTyConAppCo role tc cos) (mkTyConApp tc tys)
+{-# INLINE mkTyConAppRedn #-}
+
+-- | Reduce the arguments of a 'Class' 'TyCon'.
+mkClassPredRedn :: Class -> Reductions -> Reduction
+mkClassPredRedn cls (Reductions cos tys)
+  = mkReduction
+      (mkTyConAppCo Nominal (classTyCon cls) cos)
+      (mkClassPred cls tys)
+{-# INLINE mkClassPredRedn #-}
+
+-- | Obtain 'Reductions' from a list of 'Reduction's by unzipping.
+unzipRedns :: [Reduction] -> Reductions
+unzipRedns = foldr accRedn (Reductions [] [])
+  where
+    accRedn :: Reduction -> Reductions -> Reductions
+    accRedn (Reduction co xi) (Reductions cos xis)
+      = Reductions (co:cos) (xi:xis)
+{-# INLINE unzipRedns #-}
+-- NB: this function is currently used in two locations:
+--
+-- - GHC.Tc.Gen.Foreign.normaliseFfiType', with one call of the form:
+--
+--   unzipRedns <$> zipWithM f tys roles
+--
+-- - GHC.Tc.Solver.Monad.breakTyVarCycle_maybe, with two calls of the form:
+--
+--   unzipRedns <$> mapM f tys
+--
+-- It is possible to write 'mapAndUnzipM' functions to handle these cases,
+-- but the above locations aren't performance critical, so it was deemed
+-- to not be worth it.
+
+{-
+%************************************************************************
+%*                                                                      *
+       Simplifying types
+%*                                                                      *
+%************************************************************************
+
+The function below morally belongs in GHC.Tc.Solver.Rewrite, but it is used also in
+FamInstEnv, and so lives here.
+
+Note [simplifyArgsWorker]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+Invariant (F2) of Note [Rewriting] in GHC.Tc.Solver.Rewrite says that
+rewriting is homogeneous.
+This causes some trouble when rewriting 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 rewrite 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 :: b
+
+  [G] aco :: a ~ fa
+  [G] bco :: b ~ fb
+  [G] cco :: c ~ fc
+  [G] dco :: d ~ fd
+
+The first step is to rewrite all the arguments. This is done before calling
+simplifyArgsWorker. We start from
+
+  a
+  b
+  Just @a c
+  Right @a @b d
+  False
+
+and get left-to-right reductions whose coercions are as follows:
+
+  co1 :: a ~ fa
+  co2 :: b ~ fb
+  co3 :: (Just @a c) ~ (Just @fa (fc |> aco) |> co6)
+  co4 :: (Right @a @b d) ~ (Right @fa @fb (fd |> bco) |> co7)
+  co5 :: False ~ False
+
+where
+  co6 = Maybe (sym aco) :: Maybe fa ~ Maybe a
+  co7 = Either (sym aco) (sym bco) :: Either fa fb ~ Either a b
+
+We now process the rewritten args in left-to-right order. The first two args
+need no further processing. But now consider the third argument. Let f3 = the rewritten
+result, Just fa (fc |> aco) |> co6.
+This f3 rewritten argument has kind (Maybe a), due to homogeneity of rewriting (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) rewrote with a coercion co1. We can thus know the
+coercion needed for the 3rd argument is (Maybe co1), thus building
+(f3 |> Maybe 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 rewriting the corresponding argument (co1
+and co2, in our example). Then, after rewriting 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 rewriting 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 a ~ Maybe fa. Use (f3 |> co8) as the argument to F.
+
+  4. Lifting the kind (Either j k) with our LC
+     yields co9 :: Either a b ~ Either fa fb. Use (f4 |> co9) as the 4th
+     argument to F, where f4 is the rewritten 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 |> co8) (f4 |> 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 the third component of the
+tuple returned by 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
+  Proxy :: forall j. j -> Type
+  type family Star
+  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 rewriting:
+  a (forall (j :: Star). (j |> axStar) -> Star)   -- 1
+    (Proxy |> co)                                 -- 2
+    (bo |> sym axStar)                            -- 3
+    (NoWay |> sym bc)                             -- 4
+      :: Star
+
+First, we rewrite all the arguments (before simplifyArgsWorker), like so:
+
+    co1 :: (forall (j :: Star). (j |> axStar) -> Star) ~ (forall j. j -> Type) -- 1
+    co2 :: (Proxy |> co) ~ (Proxy |> co)                                       -- 2
+    co3 :: (bo |> sym axStar) ~ (Bool |> sym axStar)                           -- 3
+    co4 :: (NoWay |> sym bc) ~ (False |> 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 rewriting an argument, written above).
+
+2. Lifting k gives us co1, so the second argument becomes (Proxy |> co |> co1).
+   This is not a dependent argument, so we don't extend the lifting context.
+
+Now we need to deal with argument (3).
+The way we normally proceed is to lift the kind of the binder, to see whether
+it's dependent.
+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 *unrewritten* types in the decomposed coercion. (See comments on
+decomposePiCos.) Because the rewritten types have unrewritten kinds (because
+rewriting is homogeneous), passing the list of rewritten types to decomposePiCos
+just won't do: later arguments' kinds won't be as expected. So we need to get
+the *unrewritten* 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 other call sites of decomposePiCos
+would suffer from the change, even though they 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 unrewritten 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 :: Star). (j |> axStar) -> Star) (forall j. j -> Type))
+                 [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 rewritten) (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, rewritten 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 rewriting 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.
+
+Historical note: I (Richard E) once thought that the final part of the kind
+had to be a variable k (as in the example above). But it might not be: it could
+be an application of a variable. Here is the example:
+
+  let f :: forall (a :: Type) (b :: a -> Type). b (Any @a)
+      k :: Type
+      x :: k
+
+  rewrite (f @Type @((->) k) x)
+
+After instantiating [a |-> Type, b |-> ((->) k)], we see that `b (Any @a)`
+is `k -> Any @a`, and thus the third argument of `x :: k` is well-kinded.
+
+-}
+
+-- | Stores 'Reductions' as well as a kind coercion.
+--
+-- Used when rewriting arguments to a type function @f@.
+--
+-- Invariant:
+--   when the stored reductions are of the form
+--     co_i :: ty_i ~ xi_i,
+--   the kind coercion is of the form
+--      kco :: typeKind (f ty_1 ... ty_n) ~ typeKind (f xi_1 ... xi_n)
+--
+-- The type function @f@ depends on context.
+data ArgsReductions =
+  ArgsReductions
+    {-# UNPACK #-} !Reductions
+    !MCoercionN
+  -- The strictness annotations and UNPACK pragma here are crucial
+  -- to getting good performance in simplifyArgsWorker's tight loop.
+
+-- This is shared between the rewriter and the normaliser in GHC.Core.FamInstEnv.
+-- See Note [simplifyArgsWorker]
+{-# INLINE simplifyArgsWorker #-}
+-- NB. INLINE yields a ~1% decrease in allocations in T9872d compared to INLINEABLE
+-- This function is only called in two locations, so the amount of code duplication
+-- should be rather reasonable despite the size of the function.
+simplifyArgsWorker :: HasDebugCallStack
+                   => [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
+                   -> [Reduction]  -- rewritten type arguments, arg_i
+                                   -- each comes with the coercion used to rewrite it,
+                                   -- arg_co_i :: ty_i ~ arg_i
+                   -> ArgsReductions
+-- Returns ArgsReductions (Reductions cos xis) res_co, where co_i :: ty_i ~ xi_i,
+-- and res_co :: kind (f ty_1 ... ty_n) ~ kind (f xi_1 ... xi_n), where f is the function
+-- that we are applying.
+-- Precondition: if f :: forall bndrs. inner_ki (where bndrs and inner_ki are passed in),
+-- then (f ty_1 ... ty_n) is well kinded. Note that (f arg_1 ... arg_n) might *not* be well-kinded.
+-- Massaging the arg_i in order to make the function application well-kinded is what this
+-- function is all about. That is, (f xi_1 ... xi_n), where xi_i 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 :: LiftingContext  -- mapping from tyvars to rewriting coercions
+       -> [TyCoBinder]    -- Unsubsted binders of function's kind
+       -> Kind        -- Unsubsted result kind of function (not a Pi-type)
+       -> [Role]      -- Roles at which to rewrite these ...
+       -> [Reduction] -- rewritten arguments, with their rewriting coercions
+       -> ArgsReductions
+    go !lc binders inner_ki _ []
+        -- The !lc makes the function strict in the lifting context
+        -- which means GHC can unbox that pair.  A modest win.
+      = ArgsReductions
+          (mkReductions [] [])
+          kind_co
+      where
+        final_kind = mkPiTys binders inner_ki
+        kind_co | noFreeVarsOfType final_kind = MRefl
+                | otherwise                   = MCo $ liftCoSubst Nominal lc final_kind
+
+    go lc (binder:binders) inner_ki (role:roles) (arg_redn:arg_redns)
+      =  -- We rewrite an argument ty with arg_redn = Reduction arg_co arg
+         -- By Note [Rewriting] in GHC.Tc.Solver.Rewrite invariant (F2),
+         -- tcTypeKind(ty) = tcTypeKind(arg).
+         -- However, it is possible that arg will be used as an argument to a function
+         -- whose kind is different, if earlier arguments have been rewritten.
+         -- We thus need to compose the reduction with a kind coercion to ensure
+         -- well-kindedness (see the call to mkCoherenceRightRedn below).
+         --
+         -- The bangs here have been observed to improve performance
+         -- significantly in optimized builds; see #18502
+         let !kind_co = liftCoSubst Nominal lc (tyCoBinderType binder)
+             !(Reduction casted_co casted_xi)
+                      = mkCoherenceRightRedn role arg_redn kind_co
+         -- now, extend the lifting context with the new binding
+             !new_lc | Just tv <- tyCoBinderVar_maybe binder
+                     = extendLiftingContextAndInScope lc tv casted_co
+                     | otherwise
+                     = lc
+             !(ArgsReductions (Reductions cos xis) final_kind_co)
+               = go new_lc binders inner_ki roles arg_redns
+         in ArgsReductions
+              (Reductions (casted_co:cos) (casted_xi:xis))
+              final_kind_co
+
+    -- See Note [Last case in simplifyArgsWorker]
+    go lc [] inner_ki roles arg_redns
+      = let co1 = liftCoSubst Nominal lc inner_ki
+            co1_kind              = coercionKind co1
+            unrewritten_tys       = map reductionOriginalType arg_redns
+            (arg_cos, res_co)     = decomposePiCos co1 co1_kind unrewritten_tys
+            casted_args           = assertPpr (equalLength arg_redns arg_cos)
+                                              (ppr arg_redns $$ ppr arg_cos)
+                                  $ zipWith3 mkCoherenceRightRedn roles arg_redns arg_cos
+               -- 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 rewritten_kind _ = co1_kind
+            (bndrs, new_inner)    = splitPiTys rewritten_kind
+
+            ArgsReductions redns_out res_co_out
+              = go zapped_lc bndrs new_inner roles casted_args
+        in
+          ArgsReductions redns_out (res_co `mkTransMCoR` res_co_out)
+
+    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 analogous case in rewrite_args_fast
+           -- in GHC.Tc.Solver.Rewrite:
+           -- 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/GHC/Core/Utils.hs b/compiler/GHC/Core/Utils.hs
index 602981e597..b2af755e78 100644
--- a/compiler/GHC/Core/Utils.hs
+++ b/compiler/GHC/Core/Utils.hs
@@ -76,6 +76,7 @@ import GHC.Core.FamInstEnv
 import GHC.Core.Predicate
 import GHC.Core.TyCo.Rep( TyCoBinder(..), TyBinder )
 import GHC.Core.Coercion
+import GHC.Core.Reduction
 import GHC.Core.TyCon
 import GHC.Core.Multiplicity
 
@@ -2632,8 +2633,8 @@ isEmptyTy ty
 -- coercions via 'topNormaliseType_maybe'. Hence the \"norm\" prefix.
 normSplitTyConApp_maybe :: FamInstEnvs -> Type -> Maybe (TyCon, [Type], Coercion)
 normSplitTyConApp_maybe fam_envs ty
-  | let (co, ty1) = topNormaliseType_maybe fam_envs ty
-                    `orElse` (mkRepReflCo ty, ty)
+  | let Reduction co ty1 = topNormaliseType_maybe fam_envs ty
+                           `orElse` (mkReflRedn Representational ty)
   , Just (tc, tc_args) <- splitTyConApp_maybe ty1
   = Just (tc, tc_args, co)
 normSplitTyConApp_maybe _ _ = Nothing
diff --git a/compiler/GHC/HsToCore/Match/Literal.hs b/compiler/GHC/HsToCore/Match/Literal.hs
index d8da036dba..545346e998 100644
--- a/compiler/GHC/HsToCore/Match/Literal.hs
+++ b/compiler/GHC/HsToCore/Match/Literal.hs
@@ -41,6 +41,7 @@ import GHC.Types.SourceText
 import GHC.Core
 import GHC.Core.Make
 import GHC.Core.TyCon
+import GHC.Core.Reduction ( Reduction(..) )
 import GHC.Core.DataCon
 import GHC.Tc.Utils.Zonk ( shortCutLit )
 import GHC.Tc.Utils.TcType
@@ -466,7 +467,9 @@ getNormalisedTyconName fam_envs (i,ty)
     | otherwise = Nothing
   where
     normaliseNominal :: FamInstEnvs -> Type -> Type
-    normaliseNominal fam_envs ty = snd $ normaliseType fam_envs Nominal ty
+    normaliseNominal fam_envs ty
+      = reductionReducedType
+      $ normaliseType fam_envs Nominal ty
 
 -- | Convert a pair (Integer, Type) to (Integer, Name) without normalising
 -- the type
diff --git a/compiler/GHC/HsToCore/Pmc/Solver.hs b/compiler/GHC/HsToCore/Pmc/Solver.hs
index 1b6121f31f..e0d5c63698 100644
--- a/compiler/GHC/HsToCore/Pmc/Solver.hs
+++ b/compiler/GHC/HsToCore/Pmc/Solver.hs
@@ -78,6 +78,7 @@ import GHC.Core.Type
 import GHC.Tc.Solver   (tcNormalise, tcCheckGivens, tcCheckWanteds)
 import GHC.Core.Unify    (tcMatchTy)
 import GHC.Core.Coercion
+import GHC.Core.Reduction
 import GHC.HsToCore.Monad hiding (foldlM)
 import GHC.Tc.Instance.Family
 import GHC.Core.FamInstEnv
@@ -376,8 +377,9 @@ pmTopNormaliseType (TySt _ inert) typ
     tyFamStepper :: FamInstEnvs -> NormaliseStepper ([Type] -> [Type], a -> a)
     tyFamStepper env rec_nts tc tys  -- Try to step a type/data family
       = case topReduceTyFamApp_maybe env tc tys of
-          Just (_, rhs, _) -> NS_Step rec_nts rhs ((rhs:), id)
-          _                -> NS_Done
+          Just (HetReduction (Reduction _ rhs) _)
+            -> NS_Step rec_nts rhs ((rhs:), id)
+          _ -> NS_Done
 
 -- | Returns 'True' if the argument 'Type' is a fully saturated application of
 -- a closed type constructor.
diff --git a/compiler/GHC/Tc/Gen/Bind.hs b/compiler/GHC/Tc/Gen/Bind.hs
index 8a83b5540f..01dcd48952 100644
--- a/compiler/GHC/Tc/Gen/Bind.hs
+++ b/compiler/GHC/Tc/Gen/Bind.hs
@@ -44,6 +44,7 @@ import GHC.Tc.Types.Evidence
 import GHC.Tc.Gen.HsType
 import GHC.Tc.Gen.Pat
 import GHC.Tc.Utils.TcMType
+import GHC.Core.Reduction ( Reduction(..) )
 import GHC.Core.Multiplicity
 import GHC.Core.FamInstEnv( normaliseType )
 import GHC.Tc.Instance.Family( tcGetFamInstEnvs )
@@ -829,7 +830,7 @@ mkInferredPolyId insoluble qtvs inferred_theta poly_name mb_sig_inst mono_ty
                    -- a duplicate ambiguity error.  There is a similar
                    -- checkNoErrs for complete type signatures too.
     do { fam_envs <- tcGetFamInstEnvs
-       ; let (_co, mono_ty') = normaliseType fam_envs Nominal mono_ty
+       ; let mono_ty' = reductionReducedType $ normaliseType fam_envs Nominal mono_ty
                -- Unification may not have normalised the type,
                -- so do it here to make it as uncomplicated as possible.
                -- Example: f :: [F Int] -> Bool
diff --git a/compiler/GHC/Tc/Gen/Foreign.hs b/compiler/GHC/Tc/Gen/Foreign.hs
index 4204071b7d..b1c38a7166 100644
--- a/compiler/GHC/Tc/Gen/Foreign.hs
+++ b/compiler/GHC/Tc/Gen/Foreign.hs
@@ -48,6 +48,7 @@ import GHC.Tc.Utils.Env
 import GHC.Tc.Instance.Family
 import GHC.Core.FamInstEnv
 import GHC.Core.Coercion
+import GHC.Core.Reduction
 import GHC.Core.Type
 import GHC.Core.Multiplicity
 import GHC.Types.ForeignCall
@@ -70,7 +71,11 @@ import GHC.Data.Bag
 import GHC.Driver.Hooks
 import qualified GHC.LanguageExtensions as LangExt
 
-import Control.Monad
+import Control.Monad ( zipWithM )
+import Control.Monad.Trans.Writer.CPS
+  ( WriterT, runWriterT, tell )
+import Control.Monad.Trans.Class
+  ( lift )
 
 -- Defines a binding
 isForeignImport :: forall name. UnXRec name => LForeignDecl name -> Bool
@@ -107,15 +112,15 @@ an AppTy will be marshalable.
 -- we are only allowed to look through newtypes if the constructor is
 -- in scope.  We return a bag of all the newtype constructors thus found.
 -- Always returns a Representational coercion
-normaliseFfiType :: Type -> TcM (Coercion, Type, Bag GlobalRdrElt)
+normaliseFfiType :: Type -> TcM (Reduction, Bag GlobalRdrElt)
 normaliseFfiType ty
     = do fam_envs <- tcGetFamInstEnvs
          normaliseFfiType' fam_envs ty
 
-normaliseFfiType' :: FamInstEnvs -> Type -> TcM (Coercion, Type, Bag GlobalRdrElt)
-normaliseFfiType' env ty0 = go Representational initRecTc ty0
+normaliseFfiType' :: FamInstEnvs -> Type -> TcM (Reduction, Bag GlobalRdrElt)
+normaliseFfiType' env ty0 = runWriterT $ go Representational initRecTc ty0
   where
-    go :: Role -> RecTcChecker -> Type -> TcM (Coercion, Type, Bag GlobalRdrElt)
+    go :: Role -> RecTcChecker -> Type -> WriterT (Bag GlobalRdrElt) TcM Reduction
     go role rec_nts ty
       | Just ty' <- tcView ty     -- Expand synonyms
       = go role rec_nts ty'
@@ -125,15 +130,14 @@ normaliseFfiType' env ty0 = go Representational initRecTc ty0
 
       | (bndrs, inner_ty) <- splitForAllTyCoVarBinders ty
       , not (null bndrs)
-      = do (coi, nty1, gres1) <- go role rec_nts inner_ty
-           return ( mkHomoForAllCos (binderVars bndrs) coi
-                  , mkForAllTys bndrs nty1, gres1 )
+      = do redn <- go role rec_nts inner_ty
+           return $ mkHomoForAllRedn bndrs redn
 
       | otherwise -- see Note [Don't recur in normaliseFfiType']
-      = return (mkReflCo role ty, ty, emptyBag)
+      = return $ mkReflRedn role ty
 
     go_tc_app :: Role -> RecTcChecker -> TyCon -> [Type]
-              -> TcM (Coercion, Type, Bag GlobalRdrElt)
+              -> WriterT (Bag GlobalRdrElt) TcM Reduction
     go_tc_app role rec_nts tc tys
         -- We don't want to look through the IO newtype, even if it is
         -- in scope, so we have a special case for it:
@@ -148,32 +152,34 @@ normaliseFfiType' env ty0 = go Representational initRecTc ty0
                    --   Here, we don't reject the type for being recursive.
                    -- If this is a recursive newtype then it will normally
                    -- be rejected later as not being a valid FFI type.
-        = do { rdr_env <- getGlobalRdrEnv
+        = do { rdr_env <- lift $ getGlobalRdrEnv
              ; case checkNewtypeFFI rdr_env tc of
                  Nothing  -> nothing
-                 Just gre -> do { (co', ty', gres) <- go role rec_nts' nt_rhs
-                                ; return (mkTransCo nt_co co', ty', gre `consBag` gres) } }
+                 Just gre ->
+                   do { redn <- go role rec_nts' nt_rhs
+                      ; tell (unitBag gre)
+                      ; return $ nt_co `mkTransRedn` redn } }
 
         | isFamilyTyCon tc              -- Expand open tycons
-        , (co, ty) <- normaliseTcApp env role tc tys
+        , Reduction co ty <- normaliseTcApp env role tc tys
         , not (isReflexiveCo co)
-        = do (co', ty', gres) <- go role rec_nts ty
-             return (mkTransCo co co', ty', gres)
+        = do redn <- go role rec_nts ty
+             return $ co `mkTransRedn` redn
 
         | otherwise
         = nothing -- see Note [Don't recur in normaliseFfiType']
         where
           tc_key = getUnique tc
           children_only
-            = do xs <- zipWithM (\ty r -> go r rec_nts ty) tys (tyConRolesX role tc)
-                 let (cos, tys', gres) = unzip3 xs
-                 return ( mkTyConAppCo role tc cos
-                        , mkTyConApp tc tys', unionManyBags gres)
+            = do { args <- unzipRedns <$>
+                            zipWithM ( \ ty r -> go r rec_nts ty )
+                                     tys (tyConRolesX role tc)
+                 ; return $ mkTyConAppRedn role tc args }
           nt_co  = mkUnbranchedAxInstCo role (newTyConCo tc) tys []
           nt_rhs = newTyConInstRhs tc tys
 
           ty      = mkTyConApp tc tys
-          nothing = return (mkReflCo role ty, ty, emptyBag)
+          nothing = return $ mkReflRedn role ty
 
 checkNewtypeFFI :: GlobalRdrEnv -> TyCon -> Maybe GlobalRdrElt
 checkNewtypeFFI rdr_env tc
@@ -236,7 +242,7 @@ tcFImport (L dloc fo@(ForeignImport { fd_name = L nloc nm, fd_sig_ty = hs_ty
                                     , fd_fi = imp_decl }))
   = setSrcSpanA dloc $ addErrCtxt (foreignDeclCtxt fo)  $
     do { sig_ty <- tcHsSigType (ForSigCtxt nm) hs_ty
-       ; (norm_co, norm_sig_ty, gres) <- normaliseFfiType sig_ty
+       ; (Reduction norm_co norm_sig_ty, gres) <- normaliseFfiType sig_ty
        ; let
            -- Drop the foralls before inspecting the
            -- structure of the foreign type.
@@ -389,7 +395,7 @@ tcFExport fo@(ForeignExport { fd_name = L loc nm, fd_sig_ty = hs_ty, fd_fe = spe
     sig_ty <- tcHsSigType (ForSigCtxt nm) hs_ty
     rhs <- tcCheckPolyExpr (nlHsVar nm) sig_ty
 
-    (norm_co, norm_sig_ty, gres) <- normaliseFfiType sig_ty
+    (Reduction norm_co norm_sig_ty, gres) <- normaliseFfiType sig_ty
 
     spec' <- tcCheckFEType norm_sig_ty spec
 
@@ -406,7 +412,8 @@ tcFExport fo@(ForeignExport { fd_name = L loc nm, fd_sig_ty = hs_ty, fd_fe = spe
     return ( mkVarBind id rhs
            , ForeignExport { fd_name = L loc id
                            , fd_sig_ty = undefined
-                           , fd_e_ext = norm_co, fd_fe = spec' }
+                           , fd_e_ext = norm_co
+                           , fd_fe = spec' }
            , gres)
 tcFExport d = pprPanic "tcFExport" (ppr d)
 
diff --git a/compiler/GHC/Tc/Instance/Family.hs b/compiler/GHC/Tc/Instance/Family.hs
index 4818fd9ad9..a7cdb3d507 100644
--- a/compiler/GHC/Tc/Instance/Family.hs
+++ b/compiler/GHC/Tc/Instance/Family.hs
@@ -534,7 +534,7 @@ tcLookupDataFamInst_maybe fam_inst_envs tc tc_args
 -- It does not look through type families.
 -- It does not normalise arguments to a tycon.
 --
--- If the result is Just (rep_ty, (co, gres), rep_ty), then
+-- If the result is Just ((gres, co), rep_ty), then
 --    co : ty ~R rep_ty
 --    gres are the GREs for the data constructors that
 --                          had to be in scope
diff --git a/compiler/GHC/Tc/Module.hs b/compiler/GHC/Tc/Module.hs
index 696e8dc8a3..f458605c14 100644
--- a/compiler/GHC/Tc/Module.hs
+++ b/compiler/GHC/Tc/Module.hs
@@ -119,6 +119,7 @@ import GHC.Core.DataCon
 import GHC.Core.Type
 import GHC.Core.Class
 import GHC.Core.Coercion.Axiom
+import GHC.Core.Reduction ( Reduction(..) )
 import GHC.Core.Unify( RoughMatchTc(..) )
 import GHC.Core.FamInstEnv
    ( FamInst, pprFamInst, famInstsRepTyCons
@@ -2589,7 +2590,7 @@ tcRnExpr hsc_env mode rdr_expr
     fam_envs <- tcGetFamInstEnvs ;
     -- normaliseType returns a coercion which we discard, so the Role is
     -- irrelevant
-    return (snd (normaliseType fam_envs Nominal ty))
+    return (reductionReducedType (normaliseType fam_envs Nominal ty))
     }
   where
     -- Optionally instantiate the type of the expression
@@ -2676,7 +2677,7 @@ tcRnType hsc_env flexi normalise rdr_type
        --   normaliseType: expand type-family applications
        --   expandTypeSynonyms: expand type synonyms (#18828)
        ; fam_envs <- tcGetFamInstEnvs
-       ; let ty' | normalise = expandTypeSynonyms $ snd $
+       ; let ty' | normalise = expandTypeSynonyms $ reductionReducedType $
                                normaliseType fam_envs Nominal ty
                  | otherwise = ty
 
diff --git a/compiler/GHC/Tc/Plugin.hs b/compiler/GHC/Tc/Plugin.hs
index 0674f69903..78a0ebd16a 100644
--- a/compiler/GHC/Tc/Plugin.hs
+++ b/compiler/GHC/Tc/Plugin.hs
@@ -67,13 +67,14 @@ import GHC.Tc.Utils.Monad      ( TcGblEnv, TcLclEnv, TcPluginM
 import GHC.Tc.Types.Constraint ( Ct, CtLoc, CtEvidence(..), ctLocOrigin )
 import GHC.Tc.Utils.TcMType    ( TcTyVar, TcType )
 import GHC.Tc.Utils.Env        ( TcTyThing )
-import GHC.Tc.Types.Evidence   ( TcCoercion, CoercionHole, EvTerm(..)
+import GHC.Tc.Types.Evidence   ( CoercionHole, EvTerm(..)
                                , EvExpr, EvBind, mkGivenEvBind )
 import GHC.Types.Var           ( EvVar )
 
 import GHC.Unit.Module
 import GHC.Types.Name
 import GHC.Types.TyThing
+import GHC.Core.Reduction ( Reduction )
 import GHC.Core.TyCon
 import GHC.Core.DataCon
 import GHC.Core.Class
@@ -142,7 +143,7 @@ getFamInstEnvs :: TcPluginM (FamInstEnv, FamInstEnv)
 getFamInstEnvs = unsafeTcPluginTcM TcM.tcGetFamInstEnvs
 
 matchFam :: TyCon -> [Type]
-         -> TcPluginM (Maybe (TcCoercion, TcType))
+         -> TcPluginM (Maybe Reduction)
 matchFam tycon args = unsafeTcPluginTcM $ TcS.matchFamTcM tycon args
 
 newUnique :: TcPluginM Unique
diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs
index 162ef60cbc..e8c4ee82e2 100644
--- a/compiler/GHC/Tc/Solver/Canonical.hs
+++ b/compiler/GHC/Tc/Solver/Canonical.hs
@@ -29,6 +29,7 @@ import GHC.Core.Multiplicity
 import GHC.Core.TyCo.Rep   -- cleverly decomposes types, good for completeness checking
 import GHC.Core.Coercion
 import GHC.Core.Coercion.Axiom
+import GHC.Core.Reduction
 import GHC.Core
 import GHC.Types.Id( mkTemplateLocals )
 import GHC.Core.FamInstEnv ( FamInstEnvs )
@@ -209,15 +210,15 @@ canClass :: CtEvidence
 canClass ev cls tys pend_sc fds
   =   -- all classes do *nominal* matching
     assertPpr (ctEvRole ev == Nominal) (ppr ev $$ ppr cls $$ ppr tys) $
-    do { (xis, cos) <- rewriteArgsNom ev cls_tc tys
-       ; let co = mkTcTyConAppCo Nominal cls_tc cos
-             xi = mkClassPred cls xis
+    do { redns@(Reductions _ xis) <- rewriteArgsNom ev cls_tc tys
+       ; let redn@(Reduction _ xi) = mkClassPredRedn cls redns
              mk_ct new_ev = CDictCan { cc_ev = new_ev
                                      , cc_tyargs = xis
                                      , cc_class = cls
                                      , cc_pend_sc = pend_sc
                                      , cc_fundeps = fds }
-       ; mb <- rewriteEvidence ev xi co
+       ; mb <- rewriteEvidence ev redn
+
        ; traceTcS "canClass" (vcat [ ppr ev
                                    , ppr xi, ppr mb ])
        ; return (fmap mk_ct mb) }
@@ -709,8 +710,8 @@ canIrred :: CtEvidence -> TcS (StopOrContinue Ct)
 canIrred ev
   = do { let pred = ctEvPred ev
        ; traceTcS "can_pred" (text "IrredPred = " <+> ppr pred)
-       ; (xi,co) <- rewrite ev pred -- co :: xi ~ pred
-       ; rewriteEvidence ev xi co `andWhenContinue` \ new_ev ->
+       ; redn <- rewrite ev pred
+       ; rewriteEvidence ev redn `andWhenContinue` \ new_ev ->
 
     do { -- Re-classify, in case rewriting has improved its shape
          -- Code is like the canNC, except
@@ -824,8 +825,8 @@ canForAll :: CtEvidence -> Bool -> TcS (StopOrContinue Ct)
 canForAll ev pend_sc
   = do { -- First rewrite it to apply the current substitution
          let pred = ctEvPred ev
-       ; (xi,co) <- rewrite ev pred -- co :: xi ~ pred
-       ; rewriteEvidence ev xi co `andWhenContinue` \ new_ev ->
+       ; redn <- rewrite ev pred
+       ; rewriteEvidence ev redn `andWhenContinue` \ new_ev ->
 
     do { -- Now decompose into its pieces and solve it
          -- (It takes a lot less code to rewrite before decomposing.)
@@ -1058,9 +1059,9 @@ can_eq_nc' True _rdr_env _envs ev NomEq ty1 _ ty2 _
 
 -- No similarity in type structure detected. Rewrite and try again.
 can_eq_nc' False rdr_env envs ev eq_rel _ ps_ty1 _ ps_ty2
-  = do { (xi1, co1) <- rewrite ev ps_ty1
-       ; (xi2, co2) <- rewrite ev ps_ty2
-       ; new_ev <- rewriteEqEvidence ev NotSwapped xi1 xi2 co1 co2
+  = do { redn1@(Reduction _ xi1) <- rewrite ev ps_ty1
+       ; redn2@(Reduction _ xi2) <- rewrite ev ps_ty2
+       ; new_ev <- rewriteEqEvidence ev NotSwapped redn1 redn2
        ; can_eq_nc' True rdr_env envs new_ev eq_rel xi1 xi1 xi2 xi2 }
 
 ----------------------------
@@ -1459,9 +1460,9 @@ can_eq_newtype_nc :: CtEvidence           -- ^ :: ty1 ~ ty2
                   -> TcType               -- ^ ty2
                   -> TcType               -- ^ ty2, with type synonyms
                   -> TcS (StopOrContinue Ct)
-can_eq_newtype_nc ev swapped ty1 ((gres, co), ty1') ty2 ps_ty2
+can_eq_newtype_nc ev swapped ty1 ((gres, co1), ty1') ty2 ps_ty2
   = do { traceTcS "can_eq_newtype_nc" $
-         vcat [ ppr ev, ppr swapped, ppr co, ppr gres, ppr ty1', ppr ty2 ]
+         vcat [ ppr ev, ppr swapped, ppr co1, ppr gres, ppr ty1', ppr ty2 ]
 
          -- check for blowing our stack:
          -- See Note [Newtypes can blow the stack]
@@ -1477,8 +1478,11 @@ can_eq_newtype_nc ev swapped ty1 ((gres, co), ty1') ty2 ps_ty2
          -- module, don't warn about it being unused.
          -- See Note [Tracking unused binding and imports] in GHC.Tc.Utils.
 
-       ; new_ev <- rewriteEqEvidence ev swapped ty1' ps_ty2
-                                     (mkTcSymCo co) (mkTcReflCo Representational ps_ty2)
+       ; let redn1 = mkReduction co1 ty1'
+
+       ; new_ev <- rewriteEqEvidence ev swapped
+                     redn1
+                     (mkReflRedn Representational ps_ty2)
        ; can_eq_nc False new_ev ReprEq ty1' ty1' ty2 ps_ty2 }
   where
     gre_list = bagToList gres
@@ -1553,9 +1557,9 @@ canEqCast rewritten ev eq_rel swapped ty1 co1 ty2 ps_ty2
   = do { traceTcS "Decomposing cast" (vcat [ ppr ev
                                            , ppr ty1 <+> text "|>" <+> ppr co1
                                            , ppr ps_ty2 ])
-       ; new_ev <- rewriteEqEvidence ev swapped ty1 ps_ty2
-                                     (mkTcGReflRightCo role ty1 co1)
-                                     (mkTcReflCo role ps_ty2)
+       ; new_ev <- rewriteEqEvidence ev swapped
+                      (mkGReflLeftRedn role ty1 co1)
+                      (mkReflRedn role ps_ty2)
        ; can_eq_nc rewritten new_ev eq_rel ty1 ty1 ty2 ps_ty2 }
   where
     role = eqRelRole eq_rel
@@ -1912,14 +1916,14 @@ canEqFailure :: CtEvidence -> EqRel
 canEqFailure ev NomEq ty1 ty2
   = canEqHardFailure ev ty1 ty2
 canEqFailure ev ReprEq ty1 ty2
-  = do { (xi1, co1) <- rewrite ev ty1
-       ; (xi2, co2) <- rewrite ev ty2
+  = do { redn1 <- rewrite ev ty1
+       ; redn2 <- rewrite ev ty2
             -- We must rewrite the types before putting them in the
             -- inert set, so that we are sure to kick them out when
             -- new equalities become available
        ; traceTcS "canEqFailure with ReprEq" $
-         vcat [ ppr ev, ppr ty1, ppr ty2, ppr xi1, ppr xi2 ]
-       ; new_ev <- rewriteEqEvidence ev NotSwapped xi1 xi2 co1 co2
+         vcat [ ppr ev, ppr redn1, ppr redn2 ]
+       ; new_ev <- rewriteEqEvidence ev NotSwapped redn1 redn2
        ; continueWith (mkIrredCt ReprEqReason new_ev) }
 
 -- | Call when canonicalizing an equality fails with utterly no hope.
@@ -1928,9 +1932,9 @@ canEqHardFailure :: CtEvidence
 -- See Note [Make sure that insolubles are fully rewritten]
 canEqHardFailure ev ty1 ty2
   = do { traceTcS "canEqHardFailure" (ppr ty1 $$ ppr ty2)
-       ; (s1, co1) <- rewrite ev ty1
-       ; (s2, co2) <- rewrite ev ty2
-       ; new_ev <- rewriteEqEvidence ev NotSwapped s1 s2 co1 co2
+       ; redn1 <- rewrite ev ty1
+       ; redn2 <- rewrite ev ty2
+       ; new_ev <- rewriteEqEvidence ev NotSwapped redn1 redn2
        ; continueWith (mkIrredCt ShapeMismatchReason new_ev) }
 
 {-
@@ -2067,7 +2071,7 @@ Ticket #12526 is another good example of this in action.
 -}
 
 ---------------------
-canEqCanLHS :: CtEvidence          -- ev :: lhs ~ rhs
+canEqCanLHS :: CtEvidence            -- ev :: lhs ~ rhs
             -> EqRel -> SwapFlag
             -> CanEqLHS              -- lhs (or, if swapped, rhs)
             -> TcType                -- lhs: pretty lhs, already rewritten
@@ -2097,16 +2101,15 @@ canEqCanLHSHetero ev eq_rel swapped lhs1 ps_xi1 ki1 xi2 ps_xi2 ki2
 
        ; let  -- kind_co :: (ki2 :: *) ~N (ki1 :: *)   (whether swapped or not)
               -- co1     :: kind(tv1) ~N ki1
-             rhs'    = xi2    `mkCastTy` kind_co   -- :: ki1
              ps_rhs' = ps_xi2 `mkCastTy` kind_co   -- :: ki1
-             rhs_co  = mkTcGReflLeftCo role xi2 kind_co
-               -- rhs_co :: (xi2 |> kind_co) ~ xi2
 
-             lhs_co = mkTcReflCo role xi1
+             lhs_redn = mkReflRedn role xi1
+             rhs_redn@(Reduction _ rhs')
+               = mkGReflRightRedn role xi2 kind_co
 
        ; traceTcS "Hetero equality gives rise to kind equality"
            (ppr kind_co <+> dcolon <+> sep [ ppr ki2, text "~#", ppr ki1 ])
-       ; type_ev <- rewriteEqEvidence ev swapped xi1 rhs' lhs_co rhs_co
+       ; type_ev <- rewriteEqEvidence ev swapped lhs_redn rhs_redn
 
           -- rewriteEqEvidence carries out the swap, so we're NotSwapped any more
        ; canEqCanLHSHomo type_ev eq_rel NotSwapped lhs1 ps_xi1 rhs' ps_rhs' }
@@ -2305,8 +2308,8 @@ canEqTyVarFunEq ev eq_rel swapped tv1 ps_xi1 fun_tc2 fun_args2 ps_xi2 mco
 -- want to rewrite the LHS to (as per e.g. swapOverTyVars)
 canEqCanLHSFinish :: CtEvidence
                   -> EqRel -> SwapFlag
-                  -> CanEqLHS              -- lhs (or, if swapped, rhs)
-                  -> TcType          -- rhs, pretty rhs
+                  -> CanEqLHS             -- lhs (or, if swapped, rhs)
+                  -> TcType               -- rhs (or, if swapped, lhs)
                   -> TcS (StopOrContinue Ct)
 canEqCanLHSFinish ev eq_rel swapped lhs rhs
 -- RHS is fully rewritten, but with type synonyms
@@ -2315,7 +2318,9 @@ canEqCanLHSFinish ev eq_rel swapped lhs rhs
 -- (TyEq:N) is checked in can_eq_nc', and (TyEq:TV) is handled in canEqCanLHS2
 
   = do { dflags <- getDynFlags
-       ; new_ev <- rewriteEqEvidence ev swapped lhs_ty rhs rewrite_co1 rewrite_co2
+       ; new_ev <- rewriteEqEvidence ev swapped
+                     (mkReflRedn role lhs_ty)
+                     (mkReflRedn role rhs)
 
      -- by now, (TyEq:K) is already satisfied
        ; massert (canEqLHSKind lhs `eqType` tcTypeKind rhs)
@@ -2356,7 +2361,7 @@ canEqCanLHSFinish ev eq_rel swapped lhs rhs
                          do { traceTcS "canEqCanLHSFinish can't make a canonical"
                                        (ppr lhs $$ ppr rhs)
                             ; continueWith (mkIrredCt reason new_ev) }
-                     ; Just (lhs_tv, co, new_rhs) ->
+                     ; Just (lhs_tv, rhs_redn@(Reduction _ new_rhs)) ->
               do { traceTcS "canEqCanLHSFinish breaking a cycle" $
                             ppr lhs $$ ppr rhs
                  ; traceTcS "new RHS:" (ppr new_rhs)
@@ -2370,8 +2375,8 @@ canEqCanLHSFinish ev eq_rel swapped lhs rhs
 
                    else do { -- See Detail (6) of Note [Type variable cycles]
                              new_new_ev <- rewriteEqEvidence new_ev NotSwapped
-                                             lhs_ty new_rhs
-                                             (mkTcNomReflCo lhs_ty) co
+                                             (mkReflRedn Nominal lhs_ty)
+                                             rhs_redn
 
                            ; continueWith (CEqCan { cc_ev = new_new_ev
                                                   , cc_lhs = lhs
@@ -2382,9 +2387,6 @@ canEqCanLHSFinish ev eq_rel swapped lhs rhs
 
     lhs_ty = canEqLHSType lhs
 
-    rewrite_co1  = mkTcReflCo role lhs_ty
-    rewrite_co2  = mkTcReflCo role rhs
-
     -- This is about (TyEq:N)
     bad_newtype | ReprEq <- eq_rel
                 , Just tc <- tyConAppTyCon_maybe rhs
@@ -2410,13 +2412,10 @@ rewriteCastedEquality :: CtEvidence     -- :: lhs ~ (rhs |> mco), or (rhs |> mco
                       -> TcS CtEvidence -- :: (lhs |> sym mco) ~ rhs
                                         -- result is independent of SwapFlag
 rewriteCastedEquality ev eq_rel swapped lhs rhs mco
-  = rewriteEqEvidence ev swapped new_lhs new_rhs lhs_co rhs_co
+  = rewriteEqEvidence ev swapped lhs_redn rhs_redn
   where
-    new_lhs = lhs `mkCastTyMCo` sym_mco
-    lhs_co  = mkTcGReflLeftMCo role lhs sym_mco
-
-    new_rhs = rhs
-    rhs_co  = mkTcGReflRightMCo role rhs mco
+    lhs_redn = mkGReflRightMRedn role lhs sym_mco
+    rhs_redn = mkGReflLeftMRedn  role rhs mco
 
     sym_mco = mkTcSymMCo mco
     role    = eqRelRole eq_rel
@@ -2945,9 +2944,8 @@ andWhenContinue tcs1 tcs2
            ContinueWith ct -> tcs2 ct }
 infixr 0 `andWhenContinue`    -- allow chaining with ($)
 
-rewriteEvidence :: CtEvidence   -- old evidence
-                -> TcPredType   -- new predicate
-                -> TcCoercion   -- Of type :: new predicate ~ <type of old evidence>
+rewriteEvidence :: CtEvidence   -- ^ old evidence
+                -> Reduction    -- ^ new predicate + coercion, of type <type of old evidence> ~ new predicate
                 -> TcS (StopOrContinue CtEvidence)
 -- Returns Just new_ev iff either (i)  'co' is reflexivity
 --                             or (ii) 'co' is not reflexivity, and 'new_pred' not cached
@@ -2983,7 +2981,7 @@ as well as in old_pred; that is important for good error messages.
  -}
 
 
-rewriteEvidence old_ev@(CtDerived {}) new_pred _co
+rewriteEvidence old_ev@(CtDerived {}) (Reduction _co new_pred)
   = -- If derived, don't even look at the coercion.
     -- This is very important, DO NOT re-order the equations for
     -- rewriteEvidence to put the isTcReflCo test first!
@@ -2993,30 +2991,28 @@ rewriteEvidence old_ev@(CtDerived {}) new_pred _co
     -- (Getting this wrong caused #7384.)
     continueWith (old_ev { ctev_pred = new_pred })
 
-rewriteEvidence old_ev new_pred co
+rewriteEvidence old_ev (Reduction co new_pred)
   | isTcReflCo co -- See Note [Rewriting with Refl]
   = continueWith (old_ev { ctev_pred = new_pred })
 
-rewriteEvidence ev@(CtGiven { ctev_evar = old_evar, ctev_loc = loc }) new_pred co
+rewriteEvidence ev@(CtGiven { ctev_evar = old_evar, ctev_loc = loc }) (Reduction co new_pred)
   = do { new_ev <- newGivenEvVar loc (new_pred, new_tm)
        ; continueWith new_ev }
   where
     -- mkEvCast optimises ReflCo
-    new_tm = mkEvCast (evId old_evar) (tcDowngradeRole Representational
-                                                       (ctEvRole ev)
-                                                       (mkTcSymCo co))
+    new_tm = mkEvCast (evId old_evar)
+                (tcDowngradeRole Representational (ctEvRole ev) co)
 
 rewriteEvidence ev@(CtWanted { ctev_dest = dest
                              , ctev_nosh = si
-                             , ctev_loc = loc }) new_pred co
+                             , ctev_loc = loc }) (Reduction co new_pred)
   = do { mb_new_ev <- newWanted_SI si loc new_pred
                -- The "_SI" variant ensures that we make a new Wanted
-               -- with the same shadow-info as the existing one
                -- with the same shadow-info as the existing one (#16735)
        ; massert (tcCoercionRole co == ctEvRole ev)
        ; setWantedEvTerm dest
             (mkEvCast (getEvExpr mb_new_ev)
-                      (tcDowngradeRole Representational (ctEvRole ev) co))
+                      (tcDowngradeRole Representational (ctEvRole ev) (mkSymCo co)))
        ; case mb_new_ev of
             Fresh  new_ev -> continueWith new_ev
             Cached _      -> stopWith ev "Cached wanted" }
@@ -3025,26 +3021,25 @@ rewriteEvidence ev@(CtWanted { ctev_dest = dest
 rewriteEqEvidence :: CtEvidence         -- Old evidence :: olhs ~ orhs (not swapped)
                                         --              or orhs ~ olhs (swapped)
                   -> SwapFlag
-                  -> TcType -> TcType   -- New predicate  nlhs ~ nrhs
-                  -> TcCoercion         -- lhs_co, of type :: nlhs ~ olhs
-                  -> TcCoercion         -- rhs_co, of type :: nrhs ~ orhs
+                  -> Reduction          -- lhs_co :: olhs ~ nlhs
+                  -> Reduction          -- rhs_co :: orhs ~ nrhs
                   -> TcS CtEvidence     -- Of type nlhs ~ nrhs
--- For (rewriteEqEvidence (Given g olhs orhs) False nlhs nrhs lhs_co rhs_co)
--- we generate
+-- With reductions (Reduction lhs_co nlhs) (Reduction rhs_co nrhs),
+-- rewriteEqEvidence yields, for a given equality (Given g olhs orhs):
 -- If not swapped
---      g1 : nlhs ~ nrhs = lhs_co ; g ; sym rhs_co
--- If 'swapped'
---      g1 : nlhs ~ nrhs = lhs_co ; Sym g ; sym rhs_co
+--      g1 : nlhs ~ nrhs = sym lhs_co ; g ; rhs_co
+-- If swapped
+--      g1 : nlhs ~ nrhs = sym lhs_co ; Sym g ; rhs_co
 --
--- For (Wanted w) we do the dual thing.
+-- For a wanted equality (Wanted w), we do the dual thing:
 -- New  w1 : nlhs ~ nrhs
 -- If not swapped
---      w : olhs ~ orhs = sym lhs_co ; w1 ; rhs_co
+--      w : olhs ~ orhs = lhs_co ; w1 ; sym rhs_co
 -- If swapped
---      w : orhs ~ olhs = sym rhs_co ; sym w1 ; lhs_co
+--      w : orhs ~ olhs = rhs_co ; sym w1 ; sym lhs_co
 --
--- It's all a form of rewwriteEvidence, specialised for equalities
-rewriteEqEvidence old_ev swapped nlhs nrhs lhs_co rhs_co
+-- It's all a form of rewriteEvidence, specialised for equalities
+rewriteEqEvidence old_ev swapped (Reduction lhs_co nlhs) (Reduction rhs_co nrhs)
   | CtDerived {} <- old_ev  -- Don't force the evidence for a Derived
   = return (old_ev { ctev_pred = new_pred })
 
@@ -3054,9 +3049,9 @@ rewriteEqEvidence old_ev swapped nlhs nrhs lhs_co rhs_co
   = return (old_ev { ctev_pred = new_pred })
 
   | CtGiven { ctev_evar = old_evar } <- old_ev
-  = do { let new_tm = evCoercion (lhs_co
+  = do { let new_tm = evCoercion ( mkTcSymCo lhs_co
                                   `mkTcTransCo` maybeTcSymCo swapped (mkTcCoVarCo old_evar)
-                                  `mkTcTransCo` mkTcSymCo rhs_co)
+                                  `mkTcTransCo` rhs_co)
        ; newGivenEvVar loc' (new_pred, new_tm) }
 
   | CtWanted { ctev_dest = dest, ctev_nosh = si } <- old_ev
@@ -3065,9 +3060,9 @@ rewriteEqEvidence old_ev swapped nlhs nrhs lhs_co rhs_co
                -- The "_SI" variant ensures that we make a new Wanted
                -- with the same shadow-info as the existing one (#16735)
        ; let co = maybeTcSymCo swapped $
-                  mkSymCo lhs_co
+                  lhs_co
                   `mkTransCo` hole_co
-                  `mkTransCo` rhs_co
+                  `mkTransCo` mkTcSymCo rhs_co
        ; setWantedEq dest co
        ; traceTcS "rewriteEqEvidence" (vcat [ppr old_ev, ppr nlhs, ppr nrhs, ppr co])
        ; return new_ev }
diff --git a/compiler/GHC/Tc/Solver/InertSet.hs b/compiler/GHC/Tc/Solver/InertSet.hs
index c5252fb09a..5f41ca4ffd 100644
--- a/compiler/GHC/Tc/Solver/InertSet.hs
+++ b/compiler/GHC/Tc/Solver/InertSet.hs
@@ -36,12 +36,12 @@ import GHC.Prelude
 import GHC.Tc.Solver.Types
 
 import GHC.Tc.Types.Constraint
-import GHC.Tc.Types.Evidence
 import GHC.Tc.Types.Origin
 import GHC.Tc.Utils.TcType
 import GHC.Types.Var
 import GHC.Types.Var.Env
 
+import GHC.Core.Reduction
 import GHC.Core.Predicate
 import GHC.Core.TyCo.FVs
 import qualified GHC.Core.TyCo.Rep as Rep
@@ -243,12 +243,12 @@ data InertSet
               -- used to undo the cycle-breaking needed to handle
               -- Note [Type variable cycles] in GHC.Tc.Solver.Canonical
 
-       , inert_famapp_cache :: FunEqMap (TcCoercion, TcType)
+       , inert_famapp_cache :: FunEqMap Reduction
               -- Just a hash-cons cache for use when reducing family applications
               -- only
               --
               -- If    F tys :-> (co, rhs, flav),
-              -- then  co :: rhs ~N F tys
+              -- then  co :: F tys ~N rhs
               -- all evidence is from instances or Givens; no coercion holes here
               -- (We have no way of "kicking out" from the cache, so putting
               --  wanteds here means we can end up solving a Wanted with itself. Bad)
diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs
index 4b0523b7f2..750b21f9c5 100644
--- a/compiler/GHC/Tc/Solver/Monad.hs
+++ b/compiler/GHC/Tc/Solver/Monad.hs
@@ -138,6 +138,7 @@ import GHC.Driver.Session
 import GHC.Core.Type
 import qualified GHC.Core.TyCo.Rep as Rep  -- this needs to be used only very locally
 import GHC.Core.Coercion
+import GHC.Core.Reduction
 
 import GHC.Tc.Solver.Types
 import GHC.Tc.Solver.InertSet
@@ -175,7 +176,6 @@ import Data.IORef
 import GHC.Exts (oneShot)
 import Data.List ( mapAccumL, partition )
 import Data.List.NonEmpty ( NonEmpty(..) )
-import Control.Arrow ( first )
 
 #if defined(DEBUG)
 import GHC.Data.Graph.Directed
@@ -1072,9 +1072,8 @@ removeInertCt is ct =
     CIrredCan {}     -> panic "removeInertCt: CIrredEvCan"
     CNonCanonical {} -> panic "removeInertCt: CNonCanonical"
 
--- | Looks up a family application in the inerts; returned coercion
--- is oriented input ~ output
-lookupFamAppInert :: TyCon -> [Type] -> TcS (Maybe (TcCoercion, TcType, CtFlavourRole))
+-- | Looks up a family application in the inerts.
+lookupFamAppInert :: TyCon -> [Type] -> TcS (Maybe (Reduction, CtFlavourRole))
 lookupFamAppInert fam_tc tys
   = do { IS { inert_cans = IC { inert_funeqs = inert_funeqs } } <- getTcSInerts
        ; return (lookup_inerts inert_funeqs) }
@@ -1082,7 +1081,8 @@ lookupFamAppInert fam_tc tys
     lookup_inerts inert_funeqs
       | Just (EqualCtList (CEqCan { cc_ev = ctev, cc_rhs = rhs } :| _))
           <- findFunEq inert_funeqs fam_tc tys
-      = Just (ctEvCoercion ctev, rhs, ctEvFlavourRole ctev)
+      = Just (mkReduction (ctEvCoercion ctev) rhs
+             ,ctEvFlavourRole ctev)
       | otherwise = Nothing
 
 lookupInInerts :: CtLoc -> TcPredType -> TcS (Maybe CtEvidence)
@@ -1111,20 +1111,19 @@ lookupSolvedDict (IS { inert_solved_dicts = solved }) loc cls tys
       _       -> Nothing
 
 ---------------------------
-lookupFamAppCache :: TyCon -> [Type] -> TcS (Maybe (TcCoercion, TcType))
+lookupFamAppCache :: TyCon -> [Type] -> TcS (Maybe Reduction)
 lookupFamAppCache fam_tc tys
   = do { IS { inert_famapp_cache = famapp_cache } <- getTcSInerts
        ; case findFunEq famapp_cache fam_tc tys of
-           result@(Just (co, ty)) ->
+           result@(Just redn) ->
              do { traceTcS "famapp_cache hit" (vcat [ ppr (mkTyConApp fam_tc tys)
-                                                    , ppr ty
-                                                    , ppr co ])
+                                                    , ppr redn ])
                 ; return result }
            Nothing -> return Nothing }
 
-extendFamAppCache :: TyCon -> [Type] -> (TcCoercion, TcType) -> TcS ()
+extendFamAppCache :: TyCon -> [Type] -> Reduction -> TcS ()
 -- NB: co :: rhs ~ F tys, to match expectations of rewriter
-extendFamAppCache tc xi_args stuff@(_, ty)
+extendFamAppCache tc xi_args stuff@(Reduction _ ty)
   = do { dflags <- getDynFlags
        ; when (gopt Opt_FamAppCache dflags) $
     do { traceTcS "extendFamAppCache" (vcat [ ppr tc <+> ppr xi_args
@@ -1141,8 +1140,9 @@ dropFromFamAppCache varset
        ; let filtered = filterTcAppMap check famapp_cache
        ; setTcSInerts $ inerts { inert_famapp_cache = filtered } }
   where
-    check :: (TcCoercion, TcType) -> Bool
-    check (co, _) = not (anyFreeVarsOfCo (`elemVarSet` varset) co)
+    check :: Reduction -> Bool
+    check redn
+      = not (anyFreeVarsOfCo (`elemVarSet` varset) $ reductionCoercion redn)
 
 {- *********************************************************************
 *                                                                      *
@@ -2190,11 +2190,10 @@ checkReductionDepth loc ty
          wrapErrTcS $
          solverDepthErrorTcS loc ty }
 
-matchFam :: TyCon -> [Type] -> TcS (Maybe (CoercionN, TcType))
--- Given (F tys) return (ty, co), where co :: ty ~N F tys
-matchFam tycon args = fmap (fmap (first mkTcSymCo)) $ wrapTcS $ matchFamTcM tycon args
+matchFam :: TyCon -> [Type] -> TcS (Maybe ReductionN)
+matchFam tycon args = wrapTcS $ matchFamTcM tycon args
 
-matchFamTcM :: TyCon -> [Type] -> TcM (Maybe (CoercionN, TcType))
+matchFamTcM :: TyCon -> [Type] -> TcM (Maybe ReductionN)
 -- Given (F tys) return (ty, co), where co :: F tys ~N ty
 matchFamTcM tycon args
   = do { fam_envs <- FamInst.tcGetFamInstEnvs
@@ -2205,10 +2204,11 @@ matchFamTcM tycon args
               , ppr_res match_fam_result ]
        ; return match_fam_result }
   where
-    ppr_res Nothing        = text "Match failed"
-    ppr_res (Just (co,ty)) = hang (text "Match succeeded:")
-                                2 (vcat [ text "Rewrites to:" <+> ppr ty
-                                        , text "Coercion:" <+> ppr co ])
+    ppr_res Nothing = text "Match failed"
+    ppr_res (Just (Reduction co ty))
+      = hang (text "Match succeeded:")
+          2 (vcat [ text "Rewrites to:" <+> ppr ty
+                  , text "Coercion:" <+> ppr co ])
 
 {-
 ************************************************************************
@@ -2227,9 +2227,8 @@ breakTyVarCycle_maybe :: CtEvidence
                       -> CheckTyEqResult   -- result of checkTypeEq
                       -> CanEqLHS
                       -> TcType     -- RHS
-                      -> TcS (Maybe (TcTyVar, CoercionN, TcType))
+                      -> TcS (Maybe (TcTyVar, ReductionN))
                          -- new RHS that doesn't have any type families
-                         -- co :: new type ~N old type
                          -- TcTyVar is the LHS tv; convenient for the caller
 breakTyVarCycle_maybe (ctLocOrigin . ctEvLoc -> CycleBreakerOrigin _) _ _ _
   -- see Detail (7) of Note
@@ -2243,8 +2242,8 @@ breakTyVarCycle_maybe ev cte_result (TyVarLHS lhs_tv) rhs
      -- See Detail (8) of the Note.
 
   = do { should_break <- final_check
-       ; if should_break then do { (co, new_rhs) <- go rhs
-                                 ; return (Just (lhs_tv, co, new_rhs)) }
+       ; if should_break then do { redn <- go rhs
+                                 ; return (Just (lhs_tv, redn)) }
                          else return Nothing }
   where
     flavour = ctEvFlavour ev
@@ -2262,7 +2261,7 @@ breakTyVarCycle_maybe ev cte_result (TyVarLHS lhs_tv) rhs
       = return False
 
     -- This could be considerably more efficient. See Detail (5) of Note.
-    go :: TcType -> TcS (CoercionN, TcType)
+    go :: TcType -> TcS ReductionN
     go ty | Just ty' <- rewriterView ty = go ty'
     go (Rep.TyConApp tc tys)
       | isTypeFamilyTyCon tc  -- worried about whether this type family is not actually
@@ -2270,41 +2269,32 @@ breakTyVarCycle_maybe ev cte_result (TyVarLHS lhs_tv) rhs
       = do { let (fun_args, extra_args) = splitAt (tyConArity tc) tys
                  fun_app                = mkTyConApp tc fun_args
                  fun_app_kind           = tcTypeKind fun_app
-           ; (co, new_ty) <- emit_work fun_app_kind fun_app
-           ; (extra_args_cos, extra_args') <- mapAndUnzipM go extra_args
-           ; return (mkAppCos co extra_args_cos, mkAppTys new_ty extra_args') }
+           ; fun_redn <- emit_work fun_app_kind fun_app
+           ; arg_redns <- unzipRedns <$> mapM go extra_args
+           ; return $ mkAppRedns fun_redn arg_redns }
               -- Worried that this substitution will change kinds?
               -- See Detail (3) of Note
 
       | otherwise
-      = do { (cos, tys) <- mapAndUnzipM go tys
-           ; return (mkTyConAppCo Nominal tc cos, mkTyConApp tc tys) }
+      = do { arg_redns <- unzipRedns <$> mapM go tys
+           ; return $ mkTyConAppRedn Nominal tc arg_redns }
 
     go (Rep.AppTy ty1 ty2)
-      = do { (co1, ty1') <- go ty1
-           ; (co2, ty2') <- go ty2
-           ; return (mkAppCo co1 co2, mkAppTy ty1' ty2') }
+      = mkAppRedn <$> go ty1 <*> go ty2
     go (Rep.FunTy vis w arg res)
-      = do { (co_w, w') <- go w
-           ; (co_arg, arg') <- go arg
-           ; (co_res, res') <- go res
-           ; return (mkFunCo Nominal co_w co_arg co_res, mkFunTy vis w' arg' res') }
+      = mkFunRedn Nominal vis <$> go w <*> go arg <*> go res
     go (Rep.CastTy ty cast_co)
-      = do { (co, ty') <- go ty
-             -- co :: ty' ~N ty
-             -- return_co :: (ty' |> cast_co) ~ (ty |> cast_co)
-           ; return (castCoercionKind1 co Nominal ty' ty cast_co, mkCastTy ty' cast_co) }
-
+      = mkCastRedn1 Nominal ty cast_co <$> go ty
     go ty@(Rep.TyVarTy {})    = skip ty
     go ty@(Rep.LitTy {})      = skip ty
     go ty@(Rep.ForAllTy {})   = skip ty  -- See Detail (1) of Note
     go ty@(Rep.CoercionTy {}) = skip ty  -- See Detail (2) of Note
 
-    skip ty = return (mkNomReflCo ty, ty)
+    skip ty = return $ mkReflRedn Nominal ty
 
-    emit_work :: TcKind                   -- of the function application
-              -> TcType                   -- original function application
-              -> TcS (CoercionN, TcType)  -- rewritten type (the fresh tyvar)
+    emit_work :: TcKind         -- of the function application
+              -> TcType         -- original function application
+              -> TcS ReductionN -- rewritten type (the fresh tyvar)
     emit_work fun_app_kind fun_app = case flavour of
       Given ->
         do { new_tv <- wrapTcS (TcM.newCycleBreakerTyVar fun_app_kind)
@@ -2318,14 +2308,14 @@ breakTyVarCycle_maybe ev cte_result (TyVarLHS lhs_tv) rhs
            ; updInertTcS $ \is ->
                is { inert_cycle_breakers = (new_tv, fun_app) :
                                            inert_cycle_breakers is }
-           ; return (mkNomReflCo new_ty, new_ty) }
+           ; return $ mkReflRedn Nominal new_ty }
                 -- Why reflexive? See Detail (4) of the Note
 
       _derived_or_wd ->
         do { new_tv <- wrapTcS (TcM.newFlexiTyVar fun_app_kind)
            ; let new_ty = mkTyVarTy new_tv
            ; co <- emitNewWantedEq new_loc Nominal new_ty fun_app
-           ; return (co, new_ty) }
+           ; return $ mkReduction (mkSymCo co) new_ty }
 
       -- See Detail (7) of the Note
     new_loc = updateCtLocOrigin (ctEvLoc ev) CycleBreakerOrigin
diff --git a/compiler/GHC/Tc/Solver/Rewrite.hs b/compiler/GHC/Tc/Solver/Rewrite.hs
index 13f6c4ce1b..cf95fd8b3a 100644
--- a/compiler/GHC/Tc/Solver/Rewrite.hs
+++ b/compiler/GHC/Tc/Solver/Rewrite.hs
@@ -20,6 +20,7 @@ import GHC.Tc.Types.Evidence
 import GHC.Core.TyCon
 import GHC.Core.TyCo.Rep   -- performs delicate algorithm on types
 import GHC.Core.Coercion
+import GHC.Core.Reduction
 import GHC.Types.Var
 import GHC.Types.Var.Set
 import GHC.Types.Var.Env
@@ -29,7 +30,6 @@ import GHC.Utils.Panic
 import GHC.Utils.Panic.Plain
 import GHC.Tc.Solver.Monad as TcS
 import GHC.Tc.Solver.Types
-
 import GHC.Utils.Misc
 import GHC.Data.Maybe
 import GHC.Exts (oneShot)
@@ -37,8 +37,6 @@ import Control.Monad
 import GHC.Utils.Monad ( zipWith3M )
 import Data.List.NonEmpty ( NonEmpty(..) )
 
-import Control.Arrow ( first )
-
 {-
 ************************************************************************
 *                                                                      *
@@ -221,28 +219,29 @@ changes the flavour from Derived just for this purpose.
 -- If (xi, co) <- rewrite mode ev ty, then co :: xi ~r ty
 -- where r is the role in @ev@.
 rewrite :: CtEvidence -> TcType
-        -> TcS (Xi, TcCoercion)
+        -> TcS Reduction
 rewrite ev ty
   = do { traceTcS "rewrite {" (ppr ty)
-       ; (ty', co) <- runRewriteCtEv ev (rewrite_one ty)
-       ; traceTcS "rewrite }" (ppr ty')
-       ; return (ty', co) }
+       ; redn <- runRewriteCtEv ev (rewrite_one ty)
+       ; traceTcS "rewrite }" (ppr $ reductionReducedType redn)
+       ; return redn }
 
 -- specialized to rewriting kinds: never Derived, always Nominal
 -- See Note [No derived kind equalities]
 -- See Note [Rewriting]
-rewriteKind :: CtLoc -> CtFlavour -> TcType -> TcS (Xi, TcCoercionN)
+rewriteKind :: CtLoc -> CtFlavour -> TcType -> TcS ReductionN
 rewriteKind loc flav ty
   = do { traceTcS "rewriteKind {" (ppr flav <+> ppr ty)
        ; let flav' = case flav of
                        Derived -> Wanted WDeriv  -- the WDeriv/WOnly choice matters not
                        _       -> flav
-       ; (ty', co) <- runRewrite loc flav' NomEq (rewrite_one ty)
-       ; traceTcS "rewriteKind }" (ppr ty' $$ ppr co) -- co is never a panic
-       ; return (ty', co) }
+       ; redn <- runRewrite loc flav' NomEq (rewrite_one ty)
+       ; traceTcS "rewriteKind }" (ppr redn) -- the coercion inside the reduction is never a panic
+       ; return redn }
 
 -- See Note [Rewriting]
-rewriteArgsNom :: CtEvidence -> TyCon -> [TcType] -> TcS ([Xi], [TcCoercion])
+rewriteArgsNom :: CtEvidence -> TyCon -> [TcType]
+               -> TcS Reductions
 -- Externally-callable, hence runRewrite
 -- Rewrite a vector of types all at once; in fact they are
 -- always the arguments of type family or class, so
@@ -255,11 +254,11 @@ rewriteArgsNom :: CtEvidence -> TyCon -> [TcType] -> TcS ([Xi], [TcCoercion])
 -- because rewriting may use a Derived equality ([D] a ~ ty)
 rewriteArgsNom ev tc tys
   = do { traceTcS "rewrite_args {" (vcat (map ppr tys))
-       ; (tys', cos, kind_co)
+       ; ArgsReductions redns@(Reductions _ tys') kind_co
            <- runRewriteCtEv ev (rewrite_args_tc tc Nothing tys)
        ; massert (isReflMCo kind_co)
        ; traceTcS "rewrite }" (vcat (map ppr tys'))
-       ; return (tys', cos) }
+       ; return redns }
 
 -- | Rewrite a type w.r.t. nominal equality. This is useful to rewrite
 -- a type w.r.t. any givens. It does not do type-family reduction. This
@@ -267,13 +266,13 @@ rewriteArgsNom ev tc tys
 -- only givens.
 rewriteType :: CtLoc -> TcType -> TcS TcType
 rewriteType loc ty
-  = do { (xi, _) <- runRewrite loc Given NomEq $
+  = do { redn <- runRewrite loc Given NomEq $
                     rewrite_one ty
                      -- use Given flavor so that it is rewritten
                      -- only w.r.t. Givens, never Wanteds/Deriveds
                      -- (Shouldn't matter, if only Givens are present
                      -- anyway)
-       ; return xi }
+       ; return $ reductionReducedType redn }
 
 {- *********************************************************************
 *                                                                      *
@@ -283,15 +282,15 @@ rewriteType loc ty
 
 {- Note [Rewriting]
 ~~~~~~~~~~~~~~~~~~~~
-  rewrite ty  ==>   (xi, co)
+  rewrite ty  ==>  Reduction co xi
     where
       xi has no reducible type functions
          has no skolems that are mapped in the inert set
          has no filled-in metavariables
-      co :: xi ~ ty
+      co :: ty ~ xi (coercions in reductions are always left-to-right)
 
 Key invariants:
-  (F0) co :: xi ~ zonk(ty')    where zonk(ty') ~ zonk(ty)
+  (F0) co :: zonk(ty') ~ xi   where zonk(ty') ~ zonk(ty)
   (F1) tcTypeKind(xi) succeeds and returns a fully zonked kind
   (F2) tcTypeKind(xi) `eqType` zonk(tcTypeKind(ty))
 
@@ -302,18 +301,17 @@ Rewriting also:
   * applies the substitution embodied in the inert set
 
 Because rewriting zonks and the returned coercion ("co" above) is also
-zonked, it's possible that (co :: xi ~ ty) isn't quite true. So, instead,
+zonked, it's possible that (co :: ty ~ xi) isn't quite true. So, instead,
 we can rely on this fact:
 
-  (F0) co :: xi ~ zonk(ty'), where zonk(ty') ~ zonk(ty)
+  (F0) co :: zonk(ty') ~ xi, where zonk(ty') ~ zonk(ty)
 
-Note that the left-hand type of co is *always* precisely xi. The right-hand
+Note that the right-hand type of co is *always* precisely xi. The left-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 zonk-equal to ty.
-It is for this reason that we
-occasionally have to explicitly zonk, when (co :: xi ~ ty) is important
-even before we zonk the whole program. For example, see the RTRNotFollowed
-case in rewriteTyVar.
+then the left-hand type of co will be the zonk-equal to ty.
+It is for this reason that we occasionally have to explicitly zonk,
+when (co :: ty ~ xi) is important even before we zonk the whole program.
+For example, see the RTRNotFollowed case in rewriteTyVar.
 
 Why have these invariants on rewriting? Because we sometimes use tcTypeKind
 during canonicalisation, and we want this kind to be zonked (e.g., see
@@ -322,7 +320,7 @@ GHC.Tc.Solver.Canonical.canEqCanLHS).
 Rewriting is always homogeneous. That is, the kind of the result of rewriting is
 always the same as the kind of the input, modulo zonking. More formally:
 
-  (F2) tcTypeKind(xi) `eqType` zonk(tcTypeKind(ty))
+  (F2) zonk(tcTypeKind(ty)) `eqType` tcTypeKind(xi)
 
 This invariant means that the kind of a rewritten type might not itself be rewritten.
 
@@ -388,17 +386,15 @@ rewrite_args_tc
   :: TyCon         -- T
   -> Maybe [Role]  -- Nothing: ambient role is Nominal; all args are Nominal
                    -- Otherwise: no assumptions; use roles provided
-  -> [Type]        -- Arg types [t1,..,tn]
-  -> RewriteM ( [Xi]  -- List of rewritten args [x1,..,xn]
-                   -- 1-1 corresp with [t1,..,tn]
-           , [Coercion]  -- List of arg coercions [co1,..,con]
-                         -- 1-1 corresp with [t1,..,tn]
-                         --    coi :: xi ~r ti
-           , MCoercionN) -- Result coercion, rco
-                         --    rco : (T t1..tn) ~N (T (x1 |> co1) .. (xn |> con))
+  -> [Type]
+  -> RewriteM ArgsReductions -- See the commentary on rewrite_args
 rewrite_args_tc tc = rewrite_args all_bndrs any_named_bndrs inner_ki emptyVarSet
   -- NB: TyCon kinds are always closed
   where
+  -- There are many bang patterns in here. It's been observed that they
+  -- greatly improve performance of an optimized build.
+  -- The T9872 test cases are good witnesses of this fact.
+
     (bndrs, named)
       = ty_con_binders_ty_binders' (tyConBinders tc)
     -- it's possible that the result kind has arrows (for, e.g., a type family)
@@ -414,13 +410,15 @@ rewrite_args :: [TyCoBinder] -> Bool -- Binders, and True iff any of them are
              -> Kind -> TcTyCoVarSet -- function kind; kind's free vars
              -> Maybe [Role] -> [Type]    -- these are in 1-to-1 correspondence
                                           -- Nothing: use all Nominal
-             -> RewriteM ([Xi], [Coercion], MCoercionN)
--- Coercions :: Xi ~ Type, at roles given
--- Third coercion :: tcTypeKind(fun xis) ~N tcTypeKind(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 rewriting
--- homoegeneous. The list of roles must be at least as long as the list of
+             -> RewriteM ArgsReductions
+-- This function returns ArgsReductions (Reductions cos xis) res_co
+--   coercions: co_i :: ty_i ~ xi_i, at roles given
+--   types:     xi_i
+--   coercion:  res_co :: tcTypeKind(fun tys) ~N tcTypeKind(fun xis)
+-- That is, the result coercion relates the kind of some function (whose kind is
+-- passed as the first parameter) instantiated at tys to the kind of that
+-- function instantiated at the xis. This is useful in keeping rewriting
+-- homogeneous. The list of roles must be at least as long as the list of
 -- types.
 rewrite_args orig_binders
              any_named_bndrs
@@ -436,33 +434,28 @@ rewrite_args orig_binders
 {-# INLINE rewrite_args_fast #-}
 -- | fast path rewrite_args, in which none of the binders are named and
 -- therefore we can avoid tracking a lifting context.
--- There are many bang patterns in here. It's been observed that they
--- greatly improve performance of an optimized build.
--- The T9872 test cases are good witnesses of this fact.
-rewrite_args_fast :: [Type]
-                  -> RewriteM ([Xi], [Coercion], MCoercionN)
+rewrite_args_fast :: [Type] -> RewriteM ArgsReductions
 rewrite_args_fast orig_tys
   = fmap finish (iterate orig_tys)
   where
 
-    iterate :: [Type]
-            -> RewriteM ([Xi], [Coercion])
-    iterate (ty:tys) = do
-      (xi, co)   <- rewrite_one ty
-      (xis, cos) <- iterate tys
-      pure (xi : xis, co : cos)
-    iterate [] = pure ([], [])
+    iterate :: [Type] -> RewriteM Reductions
+    iterate (ty : tys) = do
+      Reduction  co  xi  <- rewrite_one ty
+      Reductions cos xis <- iterate tys
+      pure $ Reductions (co : cos) (xi : xis)
+    iterate [] = pure $ Reductions [] []
 
     {-# INLINE finish #-}
-    finish :: ([Xi], [Coercion]) -> ([Xi], [Coercion], MCoercionN)
-    finish (xis, cos) = (xis, cos, MRefl)
+    finish :: Reductions -> ArgsReductions
+    finish redns = ArgsReductions redns MRefl
 
 {-# INLINE rewrite_args_slow #-}
 -- | Slow path, compared to rewrite_args_fast, because this one must track
 -- a lifting context.
 rewrite_args_slow :: [TyCoBinder] -> Kind -> TcTyCoVarSet
                   -> [Role] -> [Type]
-                  -> RewriteM ([Xi], [Coercion], MCoercionN)
+                  -> RewriteM ArgsReductions
 rewrite_args_slow binders inner_ki fvs roles tys
 -- Arguments used dependently must be rewritten with proper coercions, but
 -- we're not guaranteed to get a proper coercion when rewriting with the
@@ -476,17 +469,17 @@ rewrite_args_slow binders inner_ki fvs roles tys
 -- Note [No derived kind equalities]
   = do { rewritten_args <- zipWith3M fl (map isNamedBinder binders ++ repeat True)
                                         roles tys
-       ; return (simplifyArgsWorker binders inner_ki fvs roles rewritten_args) }
+       ; return $ simplifyArgsWorker binders inner_ki fvs roles rewritten_args }
   where
     {-# INLINE fl #-}
     fl :: Bool   -- must we ensure to produce a real coercion here?
-                  -- see comment at top of function
-       -> Role -> Type -> RewriteM (Xi, Coercion)
+                 -- see comment at top of function
+       -> Role -> Type -> RewriteM Reduction
     fl True  r ty = noBogusCoercions $ fl1 r ty
     fl False r ty =                    fl1 r ty
 
     {-# INLINE fl1 #-}
-    fl1 :: Role -> Type -> RewriteM (Xi, Coercion)
+    fl1 :: Role -> Type -> RewriteM Reduction
     fl1 Nominal ty
       = setEqRel NomEq $
         rewrite_one ty
@@ -498,16 +491,16 @@ rewrite_args_slow binders inner_ki fvs roles tys
     fl1 Phantom ty
     -- See Note [Phantoms in the rewriter]
       = do { ty <- liftTcS $ zonkTcType ty
-           ; return (ty, mkReflCo Phantom ty) }
+           ; return $ mkReflRedn Phantom ty }
 
 ------------------
-rewrite_one :: TcType -> RewriteM (Xi, Coercion)
+rewrite_one :: TcType -> RewriteM Reduction
 -- Rewrite a type to get rid of type function applications, returning
 -- the new type-function-free type, and a collection of new equality
 -- constraints.  See Note [Rewriting] for more detail.
 --
--- Postcondition: Coercion :: Xi ~ TcType
--- The role on the result coercion matches the EqRel in the RewriteEnv
+-- Postcondition:
+-- the role on the result coercion matches the EqRel in the RewriteEnv
 
 rewrite_one ty
   | Just ty' <- rewriterView ty  -- See Note [Rewriting synonyms]
@@ -515,7 +508,7 @@ rewrite_one ty
 
 rewrite_one xi@(LitTy {})
   = do { role <- getRole
-       ; return (xi, mkReflCo role xi) }
+       ; return $ mkReflRedn role xi }
 
 rewrite_one (TyVarTy tv)
   = rewriteTyVar tv
@@ -534,13 +527,12 @@ rewrite_one (TyConApp tc tys)
   | otherwise
   = rewrite_ty_con_app tc tys
 
-rewrite_one ty@(FunTy { ft_mult = mult, ft_arg = ty1, ft_res = ty2 })
-  = do { (xi1,co1) <- rewrite_one ty1
-       ; (xi2,co2) <- rewrite_one ty2
-       ; (xi3,co3) <- setEqRel NomEq $ rewrite_one mult
+rewrite_one (FunTy { ft_af = vis, ft_mult = mult, ft_arg = ty1, ft_res = ty2 })
+  = do { arg_redn <- rewrite_one ty1
+       ; res_redn <- rewrite_one ty2
+       ; w_redn <- setEqRel NomEq $ rewrite_one mult
        ; role <- getRole
-       ; return (ty { ft_mult = xi3, ft_arg = xi1, ft_res = xi2 }
-                , mkFunCo role co3 co1 co2) }
+       ; return $ mkFunRedn role vis w_redn arg_redn res_redn }
 
 rewrite_one ty@(ForAllTy {})
 -- TODO (RAE): This is inadequate, as it doesn't rewrite the kind of
@@ -550,126 +542,116 @@ rewrite_one ty@(ForAllTy {})
 -- We allow for-alls when, but only when, no type function
 -- applications inside the forall involve the bound type variables.
   = do { let (bndrs, rho) = tcSplitForAllTyVarBinders ty
-             tvs           = binderVars bndrs
-       ; (rho', co) <- rewrite_one rho
-       ; return (mkForAllTys bndrs rho', mkHomoForAllCos tvs co) }
+       ; redn <- rewrite_one rho
+       ; return $ mkHomoForAllRedn bndrs redn }
 
 rewrite_one (CastTy ty g)
-  = do { (xi, co) <- rewrite_one ty
-       ; (g', _)  <- rewrite_co g
+  = do { redn <- rewrite_one ty
+       ; g'   <- rewrite_co g
        ; role <- getRole
-       ; return (mkCastTy xi g', castCoercionKind1 co role xi ty g') }
-         -- It makes a /big/ difference to call castCoercionKind1 not
-         -- the more general castCoercionKind2.
-         -- See Note [castCoercionKind1] in GHC.Core.Coercion
-
-rewrite_one (CoercionTy co) = first mkCoercionTy <$> rewrite_co co
+       ; return $ mkCastRedn1 role ty g' redn }
+      -- This calls castCoercionKind1.
+      -- It makes a /big/ difference to call castCoercionKind1 not
+      -- the more general castCoercionKind2.
+      -- See Note [castCoercionKind1] in GHC.Core.Coercion
+
+rewrite_one (CoercionTy co)
+  = do { co' <- rewrite_co co
+       ; role <- getRole
+       ; return $ mkReflCoRedn role co' }
 
 -- | "Rewrite" a coercion. Really, just zonk it so we can uphold
 -- (F1) of Note [Rewriting]
-rewrite_co :: Coercion -> RewriteM (Coercion, Coercion)
-rewrite_co co
-  = do { co <- liftTcS $ zonkCo co
-       ; env_role <- getRole
-       ; let co' = mkTcReflCo env_role (mkCoercionTy co)
-       ; return (co, co') }
+rewrite_co :: Coercion -> RewriteM Coercion
+rewrite_co co = liftTcS $ zonkCo co
+
+-- | Rewrite a reduction, composing the resulting coercions.
+rewrite_reduction :: Reduction -> RewriteM Reduction
+rewrite_reduction (Reduction co xi)
+  = do { redn <- bumpDepth $ rewrite_one xi
+       ; return $ co `mkTransRedn` redn }
 
 -- rewrite (nested) AppTys
-rewrite_app_tys :: Type -> [Type] -> RewriteM (Xi, Coercion)
+rewrite_app_tys :: Type -> [Type] -> RewriteM Reduction
 -- 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
 rewrite_app_tys (AppTy ty1 ty2) tys = rewrite_app_tys ty1 (ty2:tys)
 rewrite_app_tys fun_ty arg_tys
-  = do { (fun_xi, fun_co) <- rewrite_one fun_ty
-       ; rewrite_app_ty_args fun_xi fun_co arg_tys }
+  = do { redn <- rewrite_one fun_ty
+       ; rewrite_app_ty_args redn arg_tys }
 
 -- Given a rewritten function (with the coercion produced by rewriting) and
 -- a bunch of unrewritten arguments, rewrite the arguments and apply.
 -- The coercion argument's role matches the role stored in the RewriteM monad.
 --
 -- The bang patterns used here were observed to improve performance. If you
--- wish to remove them, be sure to check for regeressions in allocations.
-rewrite_app_ty_args :: Xi -> Coercion -> [Type] -> RewriteM (Xi, Coercion)
-rewrite_app_ty_args fun_xi fun_co []
+-- wish to remove them, be sure to check for regressions in allocations.
+rewrite_app_ty_args :: Reduction -> [Type] -> RewriteM Reduction
+rewrite_app_ty_args redn []
   -- this will be a common case when called from rewrite_fam_app, so shortcut
-  = return (fun_xi, fun_co)
-rewrite_app_ty_args fun_xi fun_co arg_tys
-  = do { (xi, co, kind_co) <- case tcSplitTyConApp_maybe fun_xi of
+  = return redn
+rewrite_app_ty_args fun_redn@(Reduction fun_co fun_xi) arg_tys
+  = do { het_redn <- 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)
+                ; ArgsReductions (Reductions arg_cos arg_xis) kind_co
                     <- rewrite_vector (tcTypeKind 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
+                  -- We start with a reduction of the form
+                  --   fun_co :: ty ~ T xi_1 ... xi_n
+                  -- and further arguments a_1, ..., a_m.
+                  -- We rewrite these arguments, and obtain coercions:
+                  --   arg_co_i :: a_i ~ zeta_i
+                  -- Now, 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>
+                  -- fun_co <a_1> ... <a_m> ;; T <xi_1> .. <xi_n> arg_co_1 ... arg_co_m
                 ; 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)
+                        ReprEq -> mkAppCos fun_co (map mkNomReflCo arg_tys)
                                   `mkTcTransCo`
-                                  mkAppCos fun_co (map mkNomReflCo arg_tys)
-                ; return (app_xi, app_co, kind_co) }
+                                  mkTcTyConAppCo Representational tc
+                                    (zipWith mkReflCo tc_roles xis ++ arg_cos)
+
+                ; return $
+                    mkHetReduction
+                      (mkReduction app_co app_xi )
+                      kind_co }
            Nothing ->
-             do { (arg_xis, arg_cos, kind_co)
+             do { ArgsReductions redns kind_co
                     <- rewrite_vector (tcTypeKind fun_xi) (repeat Nominal) arg_tys
-                ; let arg_xi = mkAppTys fun_xi arg_xis
-                      arg_co = mkAppCos fun_co arg_cos
-                ; return (arg_xi, arg_co, kind_co) }
+                ; return $ mkHetReduction (mkAppRedns fun_redn redns) kind_co }
 
        ; role <- getRole
-       ; return (homogenise_result xi co role kind_co) }
+       ; return (homogeniseHetRedn role het_redn) }
 
-rewrite_ty_con_app :: TyCon -> [TcType] -> RewriteM (Xi, Coercion)
+rewrite_ty_con_app :: TyCon -> [TcType] -> RewriteM Reduction
 rewrite_ty_con_app tc tys
   = do { role <- getRole
        ; let m_roles | Nominal <- role = Nothing
                      | otherwise       = Just $ tyConRolesX role tc
-       ; (xis, cos, kind_co) <- rewrite_args_tc tc m_roles tys
-       ; let tyconapp_xi = mkTyConApp tc xis
-             tyconapp_co = mkTyConAppCo role tc cos
-       ; return (homogenise_result tyconapp_xi tyconapp_co role kind_co) }
-
--- Make the result of rewriting homogeneous (Note [Rewriting] (F2))
-homogenise_result :: Xi              -- a rewritten type
-                  -> Coercion        -- :: xi ~r original ty
-                  -> Role            -- r
-                  -> MCoercionN      -- kind_co :: tcTypeKind(xi) ~N tcTypeKind(ty)
-                  -> (Xi, Coercion)  -- (xi |> kind_co, (xi |> kind_co)
-                                     --   ~r original ty)
-homogenise_result xi co _ MRefl = (xi, co)
-homogenise_result xi co r mco@(MCo kind_co)
-  = (xi `mkCastTy` kind_co, (mkSymCo $ GRefl r xi mco) `mkTransCo` co)
-{-# INLINE homogenise_result #-}
+       ; ArgsReductions redns kind_co <- rewrite_args_tc tc m_roles tys
+       ; let tyconapp_redn
+                = mkHetReduction
+                    (mkTyConAppRedn role tc redns)
+                    kind_co
+       ; return $ homogeniseHetRedn role tyconapp_redn }
 
 -- Rewrite a vector (list of arguments).
 rewrite_vector :: Kind   -- of the function being applied to these arguments
-               -> [Role] -- If we're rewrite w.r.t. ReprEq, what roles do the
+               -> [Role] -- If we're rewriting w.r.t. ReprEq, what roles do the
                          -- args have?
                -> [Type] -- the args to rewrite
-               -> RewriteM ([Xi], [Coercion], MCoercionN)
+               -> RewriteM ArgsReductions
 rewrite_vector ki roles tys
   = do { eq_rel <- getEqRel
-       ; case eq_rel of
-           NomEq  -> rewrite_args bndrs
-                                  any_named_bndrs
-                                  inner_ki
-                                  fvs
-                                  Nothing
-                                  tys
-           ReprEq -> rewrite_args bndrs
-                                  any_named_bndrs
-                                  inner_ki
-                                  fvs
-                                  (Just roles)
-                                  tys
+       ; let mb_roles = case eq_rel of { NomEq -> Nothing; ReprEq -> Just roles }
+       ; rewrite_args bndrs any_named_bndrs inner_ki fvs mb_roles tys
        }
   where
     (bndrs, inner_ki, any_named_bndrs) = split_pi_tys' ki
@@ -764,7 +746,7 @@ is inlined in that case, and only FINISH 1 is performed.
 
 -}
 
-rewrite_fam_app :: TyCon -> [TcType] -> RewriteM (Xi, Coercion)
+rewrite_fam_app :: TyCon -> [TcType] -> RewriteM Reduction
   --   rewrite_fam_app            can be over-saturated
   --   rewrite_exact_fam_app      lifts out the application to top level
   -- Postcondition: Coercion :: Xi ~ F tys
@@ -777,14 +759,12 @@ rewrite_fam_app tc tys  -- Can 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) <- rewrite_exact_fam_app tc tys1
-               -- co1 :: xi1 ~ F tys1
-
-         ; rewrite_app_ty_args xi1 co1 tys_rest }
+         ; redn <- rewrite_exact_fam_app tc tys1
+         ; rewrite_app_ty_args redn tys_rest }
 
 -- the [TcType] exactly saturate the TyCon
 -- See Note [How to normalise a family application]
-rewrite_exact_fam_app :: TyCon -> [TcType] -> RewriteM (Xi, Coercion)
+rewrite_exact_fam_app :: TyCon -> [TcType] -> RewriteM Reduction
 rewrite_exact_fam_app tc tys
   = do { checkStackDepth (mkTyConApp tc tys)
 
@@ -793,68 +773,77 @@ rewrite_exact_fam_app tc tys
        ; case result1 of
              -- Don't use the cache;
              -- See Note [rewrite_exact_fam_app performance]
-         { Just (co, xi) -> finish False (xi, co)
+         { Just redn -> finish False redn
          ; Nothing ->
 
         -- That didn't work. So reduce the arguments, in STEP 3.
     do { eq_rel <- getEqRel
-           -- checking eq_rel == NomEq saves ~0.5% in T9872a
-       ; (xis, cos, kind_co) <- if eq_rel == NomEq
-                                then rewrite_args_tc tc Nothing tys
-                                else setEqRel NomEq $
-                                     rewrite_args_tc tc Nothing tys
-           -- kind_co :: tcTypeKind(F xis) ~N tcTypeKind(F tys)
-
-       ; let role    = eqRelRole eq_rel
-             args_co = mkTyConAppCo role tc cos
-           -- args_co :: F xis ~r F tys
-
-             homogenise :: TcType -> TcCoercion -> (TcType, TcCoercion)
-               -- in (xi', co') = homogenise xi co
-               --   assume co :: xi ~r F xis, co is homogeneous
-               --   then xi' :: tcTypeKind(F tys)
-               --   and co' :: xi' ~r F tys, which is homogeneous
-             homogenise xi co = homogenise_result xi (co `mkTcTransCo` args_co) role kind_co
+          -- checking eq_rel == NomEq saves ~0.5% in T9872a
+       ; ArgsReductions (Reductions cos xis) kind_co <-
+            if eq_rel == NomEq
+            then rewrite_args_tc tc Nothing tys
+            else setEqRel NomEq $
+                 rewrite_args_tc tc Nothing tys
+
+         -- If we manage to rewrite the type family application after
+         -- rewriting the arguments, we will need to compose these
+         -- reductions.
+         --
+         -- We have:
+         --
+         --   arg_co_i :: ty_i ~ xi_i
+         --   fam_co :: F xi_1 ... xi_n ~ zeta
+         --
+         -- The full reduction is obtained as a composite:
+         --
+         --   full_co :: F ty_1 ... ty_n ~ zeta
+         --   full_co = F co_1 ... co_n ;; fam_co
+       ; let
+           role    = eqRelRole eq_rel
+           args_co = mkTyConAppCo role tc cos
+       ;  let homogenise :: Reduction -> Reduction
+              homogenise redn
+                = homogeniseHetRedn role
+                $ mkHetReduction
+                    (args_co `mkTransRedn` redn)
+                    kind_co
 
          -- STEP 4: try the inerts
        ; result2 <- liftTcS $ lookupFamAppInert tc xis
        ; flavour <- getFlavour
        ; case result2 of
-         { Just (co, xi, fr@(_, inert_eq_rel))
-             -- co :: F xis ~ir xi
+         { Just (redn, fr@(_, inert_eq_rel))
 
              | fr `eqCanRewriteFR` (flavour, eq_rel) ->
                  do { traceRewriteM "rewrite family application with inert"
-                                (ppr tc <+> ppr xis $$ ppr xi)
-                    ; finish True (homogenise xi downgraded_co) }
+                                (ppr tc <+> ppr xis $$ ppr redn)
+                    ; finish True (homogenise downgraded_redn) }
                -- this will sometimes duplicate an inert in the cache,
                -- but avoiding doing so had no impact on performance, and
                -- it seems easier not to weed out that special case
              where
-               inert_role    = eqRelRole inert_eq_rel
-               role          = eqRelRole eq_rel
-               downgraded_co = tcDowngradeRole role inert_role (mkTcSymCo co)
-                 -- downgraded_co :: xi ~r F xis
+               inert_role      = eqRelRole inert_eq_rel
+               role            = eqRelRole eq_rel
+               downgraded_redn = downgradeRedn role inert_role redn
 
          ; _ ->
 
          -- inert didn't work. Try to reduce again, in STEP 5/6.
     do { result3 <- try_to_reduce tc xis
        ; case result3 of
-           Just (co, xi) -> finish True (homogenise xi co)
-           Nothing       -> -- we have made no progress at all: STEP 7.
-                            return (homogenise reduced (mkTcReflCo role reduced))
+           Just redn -> finish True (homogenise redn)
+           Nothing   -> -- we have made no progress at all: STEP 7.
+                        return (homogenise $ mkReflRedn role reduced)
              where
                reduced = mkTyConApp tc xis }}}}}
   where
       -- call this if the above attempts made progress.
       -- This recursively rewrites the result and then adds to the cache
     finish :: Bool  -- add to the cache?
-           -> (Xi, Coercion) -> RewriteM (Xi, Coercion)
-    finish use_cache (xi, co)
+           -> Reduction -> RewriteM Reduction
+    finish use_cache redn
       = do { -- rewrite the result: FINISH 1
-             (fully, fully_co) <- bumpDepth $ rewrite_one xi
-           ; let final_co = fully_co `mkTcTransCo` co
+             final_redn <- rewrite_reduction redn
            ; eq_rel <- getEqRel
            ; flavour <- getFlavour
 
@@ -863,13 +852,13 @@ rewrite_exact_fam_app tc tys
              -- the cache only wants Nominal eqs
              -- and Wanteds can rewrite Deriveds; the cache
              -- has only Givens
-             liftTcS $ extendFamAppCache tc tys (final_co, fully)
-           ; return (fully, final_co) }
+             liftTcS $ extendFamAppCache tc tys final_redn
+           ; return final_redn }
     {-# INLINE finish #-}
 
--- Returned coercion is output ~r input, where r is the role in the RewriteM monad
+-- Returned coercion is input ~r output, where r is the role in the RewriteM monad
 -- See Note [How to normalise a family application]
-try_to_reduce :: TyCon -> [TcType] -> RewriteM (Maybe (TcCoercion, TcType))
+try_to_reduce :: TyCon -> [TcType] -> RewriteM (Maybe Reduction)
 try_to_reduce tc tys
   = do { result <- liftTcS $ firstJustsM [ lookupFamAppCache tc tys  -- STEP 5
                                          , matchFam tc tys ]         -- STEP 6
@@ -877,19 +866,20 @@ try_to_reduce tc tys
   where
     -- The result above is always Nominal. We might want a Representational
     -- coercion; this downgrades (and prints, out of convenience).
-    downgrade :: Maybe (TcCoercionN, TcType) -> RewriteM (Maybe (TcCoercion, TcType))
+    downgrade :: Maybe Reduction -> RewriteM (Maybe Reduction)
     downgrade Nothing = return Nothing
-    downgrade result@(Just (co, xi))
+    downgrade result@(Just redn)
       = do { traceRewriteM "Eager T.F. reduction success" $
-             vcat [ ppr tc, ppr tys, ppr xi
-                  , ppr co <+> dcolon <+> ppr (coercionKind co)
+             vcat [ ppr tc
+                  , ppr tys
+                  , ppr redn
                   ]
            ; eq_rel <- getEqRel
               -- manually doing it this way avoids allocation in the vastly
               -- common NomEq case
            ; case eq_rel of
                NomEq  -> return result
-               ReprEq -> return (Just (mkSubCo co, xi)) }
+               ReprEq -> return $ Just (mkSubRedn redn) }
 
 {-
 ************************************************************************
@@ -903,31 +893,27 @@ data RewriteTvResult
   = RTRNotFollowed
       -- ^ The inert set doesn't make the tyvar equal to anything else
 
-  | RTRFollowed TcType Coercion
+  | RTRFollowed !Reduction
       -- ^ The tyvar rewrites to a not-necessarily rewritten other type.
-      -- co :: new type ~r old type, where the role is determined by
-      -- the RewriteEnv
+      -- The role is determined by the RewriteEnv.
       --
       -- With Quick Look, the returned TcType can be a polytype;
       -- that is, in the constraint solver, a unification variable
       -- can contain a polytype.  See GHC.Tc.Gen.App
       -- Note [Instantiation variables are short lived]
 
-rewriteTyVar :: TyVar -> RewriteM (Xi, Coercion)
+rewriteTyVar :: TyVar -> RewriteM Reduction
 rewriteTyVar tv
   = do { mb_yes <- rewrite_tyvar1 tv
        ; case mb_yes of
-           RTRFollowed ty1 co1  -- Recur
-             -> do { (ty2, co2) <- rewrite_one ty1
-                   -- ; traceRewriteM "rewriteTyVar2" (ppr tv $$ ppr ty2)
-                   ; return (ty2, co2 `mkTransCo` co1) }
+           RTRFollowed redn -> rewrite_reduction redn
 
            RTRNotFollowed   -- Done, but make sure the kind is zonked
                             -- Note [Rewriting] invariant (F0) and (F1)
              -> do { tv' <- liftTcS $ updateTyVarKindM zonkTcType tv
                    ; role <- getRole
                    ; let ty' = mkTyVarTy tv'
-                   ; return (ty', mkTcReflCo role ty') } }
+                   ; return $ mkReflRedn role ty' } }
 
 rewrite_tyvar1 :: TcTyVar -> RewriteM RewriteTvResult
 -- "Rewriting" a type variable means to apply the substitution to it
@@ -942,7 +928,8 @@ rewrite_tyvar1 tv
            Just ty -> do { traceRewriteM "Following filled tyvar"
                              (ppr tv <+> equals <+> ppr ty)
                          ; role <- getRole
-                         ; return (RTRFollowed ty (mkReflCo role ty)) } ;
+                         ; return $ RTRFollowed $
+                             mkReflRedn role ty }
            Nothing -> do { traceRewriteM "Unfilled tyvar" (pprTyVar tv)
                          ; fr <- getFlavourRole
                          ; rewrite_tyvar2 tv fr } }
@@ -966,16 +953,16 @@ rewrite_tyvar2 tv fr@(_, eq_rel)
                         (ppr tv <+>
                          equals <+>
                          ppr rhs_ty $$ ppr ctev)
-                    ; let rewrite_co1 = mkSymCo (ctEvCoercion ctev)
-                          rewrite_co  = case (ct_eq_rel, eq_rel) of
+                    ; let rewriting_co1 = ctEvCoercion ctev
+                          rewriting_co  = case (ct_eq_rel, eq_rel) of
                             (ReprEq, _rel)  -> assert (_rel == ReprEq )
                                     -- if this ASSERT fails, then
                                     -- eqCanRewriteFR answered incorrectly
-                                               rewrite_co1
-                            (NomEq, NomEq)  -> rewrite_co1
-                            (NomEq, ReprEq) -> mkSubCo rewrite_co1
+                                               rewriting_co1
+                            (NomEq, NomEq)  -> rewriting_co1
+                            (NomEq, ReprEq) -> mkSubCo rewriting_co1
 
-                    ; return (RTRFollowed rhs_ty rewrite_co) }
+                    ; return $ RTRFollowed $ mkReduction rewriting_co rhs_ty }
                     -- NB: ct is Derived then fmode must be also, hence
                     -- we are not going to touch the returned coercion
                     -- so ctEvCoercion is fine.
diff --git a/compiler/GHC/Types/Id/Make.hs b/compiler/GHC/Types/Id/Make.hs
index fe672f6143..cd91149007 100644
--- a/compiler/GHC/Types/Id/Make.hs
+++ b/compiler/GHC/Types/Id/Make.hs
@@ -48,6 +48,7 @@ import GHC.Core.Multiplicity
 import GHC.Core.TyCo.Rep
 import GHC.Core.FamInstEnv
 import GHC.Core.Coercion
+import GHC.Core.Reduction
 import GHC.Tc.Utils.TcType as TcType
 import GHC.Core.Make
 import GHC.Core.FVs     ( mkRuleInfo )
@@ -1031,7 +1032,9 @@ dataConSrcToImplBang dflags fam_envs arg_ty
           -- we use -fomit-iface-pragmas as the indication
   , let mb_co   = topNormaliseType_maybe fam_envs (scaledThing arg_ty)
                      -- Unwrap type families and newtypes
-        arg_ty' = case mb_co of { Just (_,ty) -> scaledSet arg_ty ty; Nothing -> arg_ty }
+        arg_ty' = case mb_co of
+                    { Just redn -> scaledSet arg_ty (reductionReducedType redn)
+                    ; Nothing   -> arg_ty }
   , isUnpackableType dflags fam_envs (scaledThing arg_ty')
   , (rep_tys, _) <- dataConArgUnpack arg_ty'
   , case unpk_prag of
@@ -1041,8 +1044,8 @@ dataConSrcToImplBang dflags fam_envs arg_ty
                 && rep_tys `lengthAtMost` 1) -- See Note [Unpack one-wide fields]
       srcUnpack -> isSrcUnpacked srcUnpack
   = case mb_co of
-      Nothing     -> HsUnpack Nothing
-      Just (co,_) -> HsUnpack (Just co)
+      Nothing   -> HsUnpack Nothing
+      Just redn -> HsUnpack (Just $ reductionCoercion redn)
 
   | otherwise -- Record the strict-but-no-unpack decision
   = HsStrict
diff --git a/compiler/ghc.cabal.in b/compiler/ghc.cabal.in
index e5376dc772..e9993e7776 100644
--- a/compiler/ghc.cabal.in
+++ b/compiler/ghc.cabal.in
@@ -335,6 +335,7 @@ Library
         GHC.Core.Ppr
         GHC.Types.TyThing.Ppr
         GHC.Core.Predicate
+        GHC.Core.Reduction
         GHC.Core.Rules
         GHC.Core.Seq
         GHC.Core.SimpleOpt
diff --git a/testsuite/tests/count-deps/CountDepsAst.stdout b/testsuite/tests/count-deps/CountDepsAst.stdout
index 184f20d7d0..bde8fc08da 100644
--- a/testsuite/tests/count-deps/CountDepsAst.stdout
+++ b/testsuite/tests/count-deps/CountDepsAst.stdout
@@ -1,4 +1,4 @@
-Found 274 Language.Haskell.Syntax module dependencies
+Found 275 Language.Haskell.Syntax module dependencies
 GHC.Builtin.Names
 GHC.Builtin.PrimOps
 GHC.Builtin.Types
@@ -42,6 +42,7 @@ GHC.Core.Opt.OccurAnal
 GHC.Core.PatSyn
 GHC.Core.Ppr
 GHC.Core.Predicate
+GHC.Core.Reduction
 GHC.Core.Rules
 GHC.Core.Seq
 GHC.Core.SimpleOpt
diff --git a/testsuite/tests/count-deps/CountDepsParser.stdout b/testsuite/tests/count-deps/CountDepsParser.stdout
index a2ef4064f5..48c1791fed 100644
--- a/testsuite/tests/count-deps/CountDepsParser.stdout
+++ b/testsuite/tests/count-deps/CountDepsParser.stdout
@@ -1,4 +1,4 @@
-Found 280 GHC.Parser module dependencies
+Found 281 GHC.Parser module dependencies
 GHC.Builtin.Names
 GHC.Builtin.PrimOps
 GHC.Builtin.Types
@@ -42,6 +42,7 @@ GHC.Core.Opt.OccurAnal
 GHC.Core.PatSyn
 GHC.Core.Ppr
 GHC.Core.Predicate
+GHC.Core.Reduction
 GHC.Core.Rules
 GHC.Core.Seq
 GHC.Core.SimpleOpt