Refactor coercion rule

Summary:
The patch is an attempt on #15192.

It defines a new coercion rule

```
 | GRefl Role Type MCoercion
```

which correspondes to the typing rule

```
     t1 : k1
  ------------------------------------
  GRefl r t1 MRefl: t1 ~r t1

     t1 : k1       co :: k1 ~ k2
  ------------------------------------
  GRefl r t1 (MCo co) : t1 ~r t1 |> co
```

MCoercion wraps a coercion, which might be reflexive (MRefl)
or not (MCo co). To know more about MCoercion see #14975.

We keep Refl ty as a special case for nominal reflexive coercions,
naemly, Refl ty :: ty ~n ty.

This commit is meant to be a general performance improvement,
but there are a few regressions. See #15192, comment:13 for
more information.

Test Plan: ./validate

Reviewers: bgamari, goldfire, simonpj

Subscribers: rwbarton, thomie, carter

GHC Trac Issues: #15192

Differential Revision: https://phabricator.haskell.org/D4747

23 files changed, 635 insertions, 375 deletions

diff --git a/compiler/backpack/RnModIface.hs b/compiler/backpack/RnModIface.hs
index f807b39ce8..6b958df760 100644
--- a/compiler/backpack/RnModIface.hs
+++ b/compiler/backpack/RnModIface.hs
@@ -641,8 +641,14 @@ rnIfaceLetBndr (IfLetBndr fs ty info jpi)
 rnIfaceLamBndr :: Rename IfaceLamBndr
 rnIfaceLamBndr (bndr, oneshot) = (,) <$> rnIfaceBndr bndr <*> pure oneshot
 
+rnIfaceMCo :: Rename IfaceMCoercion
+rnIfaceMCo IfaceMRefl    = pure IfaceMRefl
+rnIfaceMCo (IfaceMCo co) = IfaceMCo <$> rnIfaceCo co
+
 rnIfaceCo :: Rename IfaceCoercion
-rnIfaceCo (IfaceReflCo role ty) = IfaceReflCo role <$> rnIfaceType ty
+rnIfaceCo (IfaceReflCo ty) = IfaceReflCo <$> rnIfaceType ty
+rnIfaceCo (IfaceGReflCo role ty mco)
+  = IfaceGReflCo role <$> rnIfaceType ty <*> rnIfaceMCo mco
 rnIfaceCo (IfaceFunCo role co1 co2)
     = IfaceFunCo role <$> rnIfaceCo co1 <*> rnIfaceCo co2
 rnIfaceCo (IfaceTyConAppCo role tc cos)
@@ -670,7 +676,6 @@ rnIfaceCo (IfaceSubCo c) = IfaceSubCo <$> rnIfaceCo c
 rnIfaceCo (IfaceAxiomRuleCo ax cos)
     = IfaceAxiomRuleCo ax <$> mapM rnIfaceCo cos
 rnIfaceCo (IfaceKindCo c) = IfaceKindCo <$> rnIfaceCo c
-rnIfaceCo (IfaceCoherenceCo c1 c2) = IfaceCoherenceCo <$> rnIfaceCo c1 <*> rnIfaceCo c2
 
 rnIfaceTyCon :: Rename IfaceTyCon
 rnIfaceTyCon (IfaceTyCon n info)
diff --git a/compiler/coreSyn/CoreFVs.hs b/compiler/coreSyn/CoreFVs.hs
index a7a96e2fcd..607fb73bbe 100644
--- a/compiler/coreSyn/CoreFVs.hs
+++ b/compiler/coreSyn/CoreFVs.hs
@@ -366,8 +366,13 @@ orphNamesOfThings f = foldr (unionNameSet . f) emptyNameSet
 orphNamesOfTypes :: [Type] -> NameSet
 orphNamesOfTypes = orphNamesOfThings orphNamesOfType
 
+orphNamesOfMCo :: MCoercion -> NameSet
+orphNamesOfMCo MRefl    = emptyNameSet
+orphNamesOfMCo (MCo co) = orphNamesOfCo co
+
 orphNamesOfCo :: Coercion -> NameSet
-orphNamesOfCo (Refl _ ty)           = orphNamesOfType ty
+orphNamesOfCo (Refl ty)             = orphNamesOfType ty
+orphNamesOfCo (GRefl _ ty mco)      = orphNamesOfType ty `unionNameSet` orphNamesOfMCo mco
 orphNamesOfCo (TyConAppCo _ tc cos) = unitNameSet (getName tc) `unionNameSet` orphNamesOfCos cos
 orphNamesOfCo (AppCo co1 co2)       = orphNamesOfCo co1 `unionNameSet` orphNamesOfCo co2
 orphNamesOfCo (ForAllCo _ kind_co co)
@@ -381,7 +386,6 @@ orphNamesOfCo (TransCo co1 co2)     = orphNamesOfCo co1 `unionNameSet` orphNames
 orphNamesOfCo (NthCo _ _ co)        = orphNamesOfCo co
 orphNamesOfCo (LRCo  _ co)          = orphNamesOfCo co
 orphNamesOfCo (InstCo co arg)       = orphNamesOfCo co `unionNameSet` orphNamesOfCo arg
-orphNamesOfCo (CoherenceCo co1 co2) = orphNamesOfCo co1 `unionNameSet` orphNamesOfCo co2
 orphNamesOfCo (KindCo co)           = orphNamesOfCo co
 orphNamesOfCo (SubCo co)            = orphNamesOfCo co
 orphNamesOfCo (AxiomRuleCo _ cs)    = orphNamesOfCos cs
diff --git a/compiler/coreSyn/CoreLint.hs b/compiler/coreSyn/CoreLint.hs
index 93826f5862..6dee383cd9 100644
--- a/compiler/coreSyn/CoreLint.hs
+++ b/compiler/coreSyn/CoreLint.hs
@@ -1617,15 +1617,28 @@ lintCoercion :: OutCoercion -> LintM (LintedKind, LintedKind, LintedType, Linted
 --
 -- If   lintCoercion co = (k1, k2, s1, s2, r)
 -- then co :: s1 ~r s2
---      s1 :: k2
+--      s1 :: k1
 --      s2 :: k2
 
 -- If you edit this function, you may need to update the GHC formalism
 -- See Note [GHC Formalism]
-lintCoercion (Refl r ty)
+lintCoercion (Refl ty)
+  = do { k <- lintType ty
+       ; return (k, k, ty, ty, Nominal) }
+
+lintCoercion (GRefl r ty MRefl)
   = do { k <- lintType ty
        ; return (k, k, ty, ty, r) }
 
+lintCoercion (GRefl r ty (MCo co))
+  = do { k <- lintType ty
+       ; (_, _, k1, k2, r') <- lintCoercion co
+       ; ensureEqTys k k1
+               (hang (text "GRefl coercion kind mis-match:" <+> ppr co)
+                   2 (vcat [ppr ty, ppr k, ppr k1]))
+       ; lintRole co Nominal r'
+       ; return (k1, k2, ty, mkCastTy ty co, r) }
+
 lintCoercion co@(TyConAppCo r tc cos)
   | tc `hasKey` funTyConKey
   , [_rep1,_rep2,_co1,_co2] <- cos
@@ -1646,7 +1659,7 @@ lintCoercion co@(TyConAppCo r tc cos)
 lintCoercion co@(AppCo co1 co2)
   | TyConAppCo {} <- co1
   = failWithL (text "TyConAppCo to the left of AppCo:" <+> ppr co)
-  | Refl _ (TyConApp {}) <- co1
+  | Just (TyConApp {}, _) <- isReflCo_maybe co1
   = failWithL (text "Refl (TyConApp ...) to the left of AppCo:" <+> ppr co)
   | otherwise
   = do { (k1,  k2,  s1, s2, r1) <- lintCoercion co1
@@ -1884,12 +1897,6 @@ lintCoercion co@(AxiomInstCo con ind cos)
            ; return (extendTCvSubst subst_l ktv s',
                      extendTCvSubst subst_r ktv t') }
 
-lintCoercion (CoherenceCo co1 co2)
-  = do { (_, k2, t1, t2, r) <- lintCoercion co1
-       ; let lhsty = mkCastTy t1 co2
-       ; k1' <- lintType lhsty
-       ; return (k1', k2, lhsty, t2, r) }
-
 lintCoercion (KindCo co)
   = do { (k1, k2, _, _, _) <- lintCoercion co
        ; return (liftedTypeKind, liftedTypeKind, k1, k2, Nominal) }
diff --git a/compiler/coreSyn/CoreOpt.hs b/compiler/coreSyn/CoreOpt.hs
index 0353ab6a75..8684c84515 100644
--- a/compiler/coreSyn/CoreOpt.hs
+++ b/compiler/coreSyn/CoreOpt.hs
@@ -995,7 +995,7 @@ pushCoTyArg co ty
        -- kinds of the types related by a coercion between forall-types.
        -- See the NthCo case in CoreLint.
 
-    co2 = mkInstCo co (mkCoherenceLeftCo (mkNomReflCo ty) co1)
+    co2 = mkInstCo co (mkGReflLeftCo Nominal ty co1)
         -- co2 :: ty1[ (ty|>co1)/a1 ] ~ ty2[ ty/a2 ]
         -- Arg of mkInstCo is always nominal, hence mkNomReflCo
 
diff --git a/compiler/iface/IfaceSyn.hs b/compiler/iface/IfaceSyn.hs
index 778e8d637d..4a2d228bef 100644
--- a/compiler/iface/IfaceSyn.hs
+++ b/compiler/iface/IfaceSyn.hs
@@ -1425,8 +1425,14 @@ freeNamesIfType (IfaceDFunTy s t)     = freeNamesIfType s &&& freeNamesIfType t
 freeNamesIfType (IfaceCastTy t c)     = freeNamesIfType t &&& freeNamesIfCoercion c
 freeNamesIfType (IfaceCoercionTy c)   = freeNamesIfCoercion c
 
+freeNamesIfMCoercion :: IfaceMCoercion -> NameSet
+freeNamesIfMCoercion IfaceMRefl    = emptyNameSet
+freeNamesIfMCoercion (IfaceMCo co) = freeNamesIfCoercion co
+
 freeNamesIfCoercion :: IfaceCoercion -> NameSet
-freeNamesIfCoercion (IfaceReflCo _ t) = freeNamesIfType t
+freeNamesIfCoercion (IfaceReflCo t) = freeNamesIfType t
+freeNamesIfCoercion (IfaceGReflCo _ t mco)
+  = freeNamesIfType t &&& freeNamesIfMCoercion mco
 freeNamesIfCoercion (IfaceFunCo _ c1 c2)
   = freeNamesIfCoercion c1 &&& freeNamesIfCoercion c2
 freeNamesIfCoercion (IfaceTyConAppCo _ tc cos)
@@ -1452,8 +1458,6 @@ freeNamesIfCoercion (IfaceLRCo _ co)
   = freeNamesIfCoercion co
 freeNamesIfCoercion (IfaceInstCo co co2)
   = freeNamesIfCoercion co &&& freeNamesIfCoercion co2
-freeNamesIfCoercion (IfaceCoherenceCo c1 c2)
-  = freeNamesIfCoercion c1 &&& freeNamesIfCoercion c2
 freeNamesIfCoercion (IfaceKindCo c)
   = freeNamesIfCoercion c
 freeNamesIfCoercion (IfaceSubCo co)
diff --git a/compiler/iface/IfaceType.hs b/compiler/iface/IfaceType.hs
index 5a7f761d32..e3866f5e6d 100644
--- a/compiler/iface/IfaceType.hs
+++ b/compiler/iface/IfaceType.hs
@@ -14,6 +14,7 @@ module IfaceType (
         IfExtName, IfLclName,
 
         IfaceType(..), IfacePredType, IfaceKind, IfaceCoercion(..),
+        IfaceMCoercion(..),
         IfaceUnivCoProv(..),
         IfaceTyCon(..), IfaceTyConInfo(..), IfaceTyConSort(..), IsPromoted(..),
         IfaceTyLit(..), IfaceTcArgs(..),
@@ -280,8 +281,13 @@ data IfaceTyConInfo   -- Used to guide pretty-printing
                    , ifaceTyConSort       :: IfaceTyConSort }
     deriving (Eq)
 
+data IfaceMCoercion
+  = IfaceMRefl
+  | IfaceMCo IfaceCoercion
+
 data IfaceCoercion
-  = IfaceReflCo       Role IfaceType
+  = IfaceReflCo       IfaceType
+  | IfaceGReflCo      Role IfaceType (IfaceMCoercion)
   | IfaceFunCo        Role IfaceCoercion IfaceCoercion
   | IfaceTyConAppCo   Role IfaceTyCon [IfaceCoercion]
   | IfaceAppCo        IfaceCoercion IfaceCoercion
@@ -298,7 +304,6 @@ data IfaceCoercion
   | IfaceNthCo        Int IfaceCoercion
   | IfaceLRCo         LeftOrRight IfaceCoercion
   | IfaceInstCo       IfaceCoercion IfaceCoercion
-  | IfaceCoherenceCo  IfaceCoercion IfaceCoercion
   | IfaceKindCo       IfaceCoercion
   | IfaceSubCo        IfaceCoercion
   | IfaceFreeCoVar    CoVar    -- See Note [Free tyvars in IfaceType]
@@ -457,8 +462,12 @@ substIfaceType env ty
     go (IfaceCastTy ty co)    = IfaceCastTy (go ty) (go_co co)
     go (IfaceCoercionTy co)   = IfaceCoercionTy (go_co co)
 
-    go_co (IfaceReflCo r ty)     = IfaceReflCo r (go ty)
-    go_co (IfaceFunCo r c1 c2)   = IfaceFunCo r (go_co c1) (go_co c2)
+    go_mco IfaceMRefl    = IfaceMRefl
+    go_mco (IfaceMCo co) = IfaceMCo $ go_co co
+
+    go_co (IfaceReflCo ty)           = IfaceReflCo (go ty)
+    go_co (IfaceGReflCo r ty mco)    = IfaceGReflCo r (go ty) (go_mco mco)
+    go_co (IfaceFunCo r c1 c2)       = IfaceFunCo r (go_co c1) (go_co c2)
     go_co (IfaceTyConAppCo r tc cos) = IfaceTyConAppCo r tc (go_cos cos)
     go_co (IfaceAppCo c1 c2)         = IfaceAppCo (go_co c1) (go_co c2)
     go_co (IfaceForAllCo {})         = pprPanic "substIfaceCoercion" (ppr ty)
@@ -472,7 +481,6 @@ substIfaceType env ty
     go_co (IfaceNthCo n co)          = IfaceNthCo n (go_co co)
     go_co (IfaceLRCo lr co)          = IfaceLRCo lr (go_co co)
     go_co (IfaceInstCo c1 c2)        = IfaceInstCo (go_co c1) (go_co c2)
-    go_co (IfaceCoherenceCo c1 c2)   = IfaceCoherenceCo (go_co c1) (go_co c2)
     go_co (IfaceKindCo co)           = IfaceKindCo (go_co co)
     go_co (IfaceSubCo co)            = IfaceSubCo (go_co co)
     go_co (IfaceAxiomRuleCo n cos)   = IfaceAxiomRuleCo n (go_cos cos)
@@ -1197,7 +1205,12 @@ pprIfaceCoercion = ppr_co topPrec
 pprParendIfaceCoercion = ppr_co appPrec
 
 ppr_co :: PprPrec -> IfaceCoercion -> SDoc
-ppr_co _         (IfaceReflCo r ty) = angleBrackets (ppr ty) <> ppr_role r
+ppr_co _         (IfaceReflCo ty) = angleBrackets (ppr ty) <> ppr_role Nominal
+ppr_co _         (IfaceGReflCo r ty IfaceMRefl)
+  = angleBrackets (ppr ty) <> ppr_role r
+ppr_co ctxt_prec (IfaceGReflCo r ty (IfaceMCo co))
+  = ppr_special_co ctxt_prec
+    (text "GRefl" <+> ppr r <+> pprParendIfaceType ty) [co]
 ppr_co ctxt_prec (IfaceFunCo r co1 co2)
   = maybeParen ctxt_prec funPrec $
     sep (ppr_co funPrec co1 : ppr_fun_tail co2)
@@ -1258,8 +1271,6 @@ ppr_co ctxt_prec (IfaceLRCo lr co)
   = ppr_special_co ctxt_prec (ppr lr) [co]
 ppr_co ctxt_prec (IfaceSubCo co)
   = ppr_special_co ctxt_prec (text "Sub") [co]
-ppr_co ctxt_prec (IfaceCoherenceCo co1 co2)
-  = ppr_special_co ctxt_prec (text "Coh") [co1,co2]
 ppr_co ctxt_prec (IfaceKindCo co)
   = ppr_special_co ctxt_prec (text "Kind") [co]
 
@@ -1490,64 +1501,79 @@ instance Binary IfaceType where
               _  -> do n <- get bh
                        return (IfaceLitTy n)
 
+instance Binary IfaceMCoercion where
+  put_ bh IfaceMRefl = do
+          putByte bh 1
+  put_ bh (IfaceMCo co) = do
+          putByte bh 2
+          put_ bh co
+
+  get bh = do
+    tag <- getByte bh
+    case tag of
+         1 -> return IfaceMRefl
+         2 -> do a <- get bh
+                 return $ IfaceMCo a
+         _ -> panic ("get IfaceMCoercion " ++ show tag)
+
 instance Binary IfaceCoercion where
-  put_ bh (IfaceReflCo a b) = do
+  put_ bh (IfaceReflCo a) = do
           putByte bh 1
           put_ bh a
+  put_ bh (IfaceGReflCo a b c) = do
+          putByte bh 2
+          put_ bh a
           put_ bh b
+          put_ bh c
   put_ bh (IfaceFunCo a b c) = do
-          putByte bh 2
+          putByte bh 3
           put_ bh a
           put_ bh b
           put_ bh c
   put_ bh (IfaceTyConAppCo a b c) = do
-          putByte bh 3
+          putByte bh 4
           put_ bh a
           put_ bh b
           put_ bh c
   put_ bh (IfaceAppCo a b) = do
-          putByte bh 4
+          putByte bh 5
           put_ bh a
           put_ bh b
   put_ bh (IfaceForAllCo a b c) = do
-          putByte bh 5
+          putByte bh 6
           put_ bh a
           put_ bh b
           put_ bh c
   put_ bh (IfaceCoVarCo a) = do
-          putByte bh 6
+          putByte bh 7
           put_ bh a
   put_ bh (IfaceAxiomInstCo a b c) = do
-          putByte bh 7
+          putByte bh 8
           put_ bh a
           put_ bh b
           put_ bh c
   put_ bh (IfaceUnivCo a b c d) = do
-          putByte bh 8
+          putByte bh 9
           put_ bh a
           put_ bh b
           put_ bh c
           put_ bh d
   put_ bh (IfaceSymCo a) = do
-          putByte bh 9
-          put_ bh a
-  put_ bh (IfaceTransCo a b) = do
           putByte bh 10
           put_ bh a
-          put_ bh b
-  put_ bh (IfaceNthCo a b) = do
+  put_ bh (IfaceTransCo a b) = do
           putByte bh 11
           put_ bh a
           put_ bh b
-  put_ bh (IfaceLRCo a b) = do
+  put_ bh (IfaceNthCo a b) = do
           putByte bh 12
           put_ bh a
           put_ bh b
-  put_ bh (IfaceInstCo a b) = do
+  put_ bh (IfaceLRCo a b) = do
           putByte bh 13
           put_ bh a
           put_ bh b
-  put_ bh (IfaceCoherenceCo a b) = do
+  put_ bh (IfaceInstCo a b) = do
           putByte bh 14
           put_ bh a
           put_ bh b
@@ -1571,51 +1597,51 @@ instance Binary IfaceCoercion where
       tag <- getByte bh
       case tag of
            1 -> do a <- get bh
-                   b <- get bh
-                   return $ IfaceReflCo a b
+                   return $ IfaceReflCo a
            2 -> do a <- get bh
                    b <- get bh
                    c <- get bh
-                   return $ IfaceFunCo a b c
+                   return $ IfaceGReflCo a b c
            3 -> do a <- get bh
                    b <- get bh
                    c <- get bh
-                   return $ IfaceTyConAppCo a b c
+                   return $ IfaceFunCo a b c
            4 -> do a <- get bh
                    b <- get bh
-                   return $ IfaceAppCo a b
+                   c <- get bh
+                   return $ IfaceTyConAppCo a b c
            5 -> do a <- get bh
                    b <- get bh
+                   return $ IfaceAppCo a b
+           6 -> do a <- get bh
+                   b <- get bh
                    c <- get bh
                    return $ IfaceForAllCo a b c
-           6 -> do a <- get bh
-                   return $ IfaceCoVarCo a
            7 -> do a <- get bh
+                   return $ IfaceCoVarCo a
+           8 -> do a <- get bh
                    b <- get bh
                    c <- get bh
                    return $ IfaceAxiomInstCo a b c
-           8 -> do a <- get bh
+           9 -> do a <- get bh
                    b <- get bh
                    c <- get bh
                    d <- get bh
                    return $ IfaceUnivCo a b c d
-           9 -> do a <- get bh
-                   return $ IfaceSymCo a
            10-> do a <- get bh
-                   b <- get bh
-                   return $ IfaceTransCo a b
+                   return $ IfaceSymCo a
            11-> do a <- get bh
                    b <- get bh
-                   return $ IfaceNthCo a b
+                   return $ IfaceTransCo a b
            12-> do a <- get bh
                    b <- get bh
-                   return $ IfaceLRCo a b
+                   return $ IfaceNthCo a b
            13-> do a <- get bh
                    b <- get bh
-                   return $ IfaceInstCo a b
+                   return $ IfaceLRCo a b
            14-> do a <- get bh
                    b <- get bh
-                   return $ IfaceCoherenceCo a b
+                   return $ IfaceInstCo a b
            15-> do a <- get bh
                    return $ IfaceKindCo a
            16-> do a <- get bh
diff --git a/compiler/iface/TcIface.hs b/compiler/iface/TcIface.hs
index bffda71f0a..58bcd8c281 100644
--- a/compiler/iface/TcIface.hs
+++ b/compiler/iface/TcIface.hs
@@ -1199,7 +1199,11 @@ tcIfaceTyLit (IfaceStrTyLit n) = return (StrTyLit n)
 tcIfaceCo :: IfaceCoercion -> IfL Coercion
 tcIfaceCo = go
   where
-    go (IfaceReflCo r t)         = Refl r <$> tcIfaceType t
+    go_mco IfaceMRefl    = pure MRefl
+    go_mco (IfaceMCo co) = MCo <$> (go co)
+
+    go (IfaceReflCo t)           = Refl <$> tcIfaceType t
+    go (IfaceGReflCo r t mco)    = GRefl r <$> tcIfaceType t <*> go_mco mco
     go (IfaceFunCo r c1 c2)      = mkFunCo r <$> go c1 <*> go c2
     go (IfaceTyConAppCo r tc cs)
       = TyConAppCo r <$> tcIfaceTyCon tc <*> mapM go cs
@@ -1219,8 +1223,6 @@ tcIfaceCo = go
     go (IfaceNthCo d c)          = do { c' <- go c
                                       ; return $ mkNthCo (nthCoRole d c') d c' }
     go (IfaceLRCo lr c)          = LRCo lr  <$> go c
-    go (IfaceCoherenceCo c1 c2)  = CoherenceCo <$> go c1
-                                               <*> go c2
     go (IfaceKindCo c)           = KindCo   <$> go c
     go (IfaceSubCo c)            = SubCo    <$> go c
     go (IfaceAxiomRuleCo ax cos) = AxiomRuleCo <$> tcIfaceCoAxiomRule ax
diff --git a/compiler/iface/ToIface.hs b/compiler/iface/ToIface.hs
index 4b810fa687..291aea36a7 100644
--- a/compiler/iface/ToIface.hs
+++ b/compiler/iface/ToIface.hs
@@ -221,7 +221,11 @@ toIfaceCoercionX :: VarSet -> Coercion -> IfaceCoercion
 toIfaceCoercionX fr co
   = go co
   where
-    go (Refl r ty)          = IfaceReflCo r (toIfaceTypeX fr ty)
+    go_mco MRefl     = IfaceMRefl
+    go_mco (MCo co)  = IfaceMCo $ go co
+
+    go (Refl ty)            = IfaceReflCo (toIfaceTypeX fr ty)
+    go (GRefl r ty mco)     = IfaceGReflCo r (toIfaceTypeX fr ty) (go_mco mco)
     go (CoVarCo cv)
       -- See [TcTyVars in IfaceType] in IfaceType
       | cv `elemVarSet` fr  = IfaceFreeCoVar cv
@@ -234,7 +238,6 @@ toIfaceCoercionX fr co
     go (NthCo _r d co)      = IfaceNthCo d (go co)
     go (LRCo lr co)         = IfaceLRCo lr (go co)
     go (InstCo co arg)      = IfaceInstCo (go co) (go arg)
-    go (CoherenceCo c1 c2)  = IfaceCoherenceCo (go c1) (go c2)
     go (KindCo c)           = IfaceKindCo (go c)
     go (SubCo co)           = IfaceSubCo (go co)
     go (AxiomRuleCo co cs)  = IfaceAxiomRuleCo (coaxrName co) (map go cs)
diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index a8fff6b767..42f28c7c2b 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -1291,7 +1291,7 @@ canEqCast flat ev eq_rel swapped ty1 co1 ty2 ps_ty2
                                            , ppr ty1 <+> text "|>" <+> ppr co1
                                            , ppr ps_ty2 ])
        ; new_ev <- rewriteEqEvidence ev swapped ty1 ps_ty2
-                                     (mkTcReflCo role ty1 `mkTcCoherenceRightCo` co1)
+                                     (mkTcGReflRightCo role ty1 co1)
                                      (mkTcReflCo role ps_ty2)
        ; can_eq_nc flat new_ev eq_rel ty1 ty1 ty2 ps_ty2 }
   where
@@ -1737,7 +1737,10 @@ canCFunEqCan ev fn tys fsk
                                -- new_co     :: F tys' ~ new_fsk
                                -- co         :: F tys ~ (new_fsk |> kind_co)
                             co = mkTcSymCo lhs_co `mkTcTransCo`
-                                 (new_co `mkTcCoherenceRightCo` kind_co)
+                                 mkTcCoherenceRightCo Nominal
+                                                      (mkTyVarTy new_fsk)
+                                                      kind_co
+                                                      new_co
 
                       ; traceTcS "Discharging fmv/fsk due to hetero flattening" (ppr ev)
                       ; dischargeFunEq ev fsk co xi
@@ -1788,7 +1791,7 @@ canEqTyVar ev eq_rel swapped tv1 ps_ty1 xi2 ps_xi2
 
                        new_rhs     = xi2 `mkCastTy` rhs_kind_co
                        ps_rhs      = ps_xi2 `mkCastTy` rhs_kind_co
-                       rhs_co      = mkTcReflCo role xi2 `mkTcCoherenceLeftCo` rhs_kind_co
+                       rhs_co      = mkTcGReflLeftCo role xi2 rhs_kind_co
 
                  ; new_ev <- rewriteEqEvidence ev swapped xi1 new_rhs
                                                (mkTcReflCo role xi1) rhs_co
@@ -1803,8 +1806,8 @@ canEqTyVar ev eq_rel swapped tv1 ps_ty1 xi2 ps_xi2
              new_rhs = xi2 `mkCastTy` sym_k2_co  -- :: flat_k2
              ps_rhs  = ps_xi2 `mkCastTy` sym_k2_co
 
-             lhs_co = mkReflCo role xi1 `mkTcCoherenceLeftCo` sym_k1_co
-             rhs_co = mkReflCo role xi2 `mkTcCoherenceLeftCo` sym_k2_co
+             lhs_co = mkTcGReflLeftCo role xi1 sym_k1_co
+             rhs_co = mkTcGReflLeftCo role xi2 sym_k2_co
                -- lhs_co :: (xi1 |> sym k1_co) ~ xi1
                -- rhs_co :: (xi2 |> sym k2_co) ~ xi2
 
@@ -1841,11 +1844,11 @@ canEqTyVarHetero ev eq_rel tv1 co1 ki1 ps_tv1 xi2 ki2 ps_xi2
              homo_co = mkTcSymCo (ctEvCoercion kind_ev) `mkTcTransCo` mkTcSymCo co1
              rhs'    = mkCastTy xi2 homo_co     -- :: kind(tv1)
              ps_rhs' = mkCastTy ps_xi2 homo_co  -- :: kind(tv1)
-             rhs_co  = mkReflCo role xi2 `mkTcCoherenceLeftCo` homo_co
+             rhs_co  = mkTcGReflLeftCo role xi2 homo_co
                -- rhs_co :: (xi2 |> homo_co :: kind(tv1)) ~ xi2
 
              lhs'   = mkTyVarTy tv1       -- :: kind(tv1)
-             lhs_co = mkReflCo role lhs' `mkTcCoherenceRightCo` co1
+             lhs_co = mkTcGReflRightCo role lhs' co1
                -- lhs_co :: (tv1 :: kind(tv1)) ~ (tv1 |> co1 :: ki1)
 
        ; traceTcS "Hetero equality gives rise to given kind equality"
@@ -1895,10 +1898,10 @@ canEqTyVarHomo ev eq_rel swapped tv1 ps_ty1 ty2 _
              sym_co2 = mkTcSymCo co2
              ty1     = mkTyVarTy tv1
              new_lhs = ty1 `mkCastTy` sym_co2
-             lhs_co  = mkReflCo role ty1 `mkTcCoherenceLeftCo` sym_co2
+             lhs_co  = mkTcGReflLeftCo role ty1 sym_co2
 
              new_rhs = mkTyVarTy tv2
-             rhs_co  = mkReflCo role new_rhs `mkTcCoherenceRightCo` co2
+             rhs_co  = mkTcGReflRightCo role new_rhs co2
 
        ; new_ev <- rewriteEqEvidence ev swapped new_lhs new_rhs lhs_co rhs_co
 
diff --git a/compiler/typecheck/TcEvidence.hs b/compiler/typecheck/TcEvidence.hs
index 66fcb7a589..50c49bc65a 100644
--- a/compiler/typecheck/TcEvidence.hs
+++ b/compiler/typecheck/TcEvidence.hs
@@ -35,7 +35,9 @@ module TcEvidence (
   mkTcAxInstCo, mkTcUnbranchedAxInstCo, mkTcForAllCo, mkTcForAllCos,
   mkTcSymCo, mkTcTransCo, mkTcNthCo, mkTcLRCo, mkTcSubCo, maybeTcSubCo,
   tcDowngradeRole,
-  mkTcAxiomRuleCo, mkTcCoherenceLeftCo, mkTcCoherenceRightCo, mkTcPhantomCo,
+  mkTcAxiomRuleCo, mkTcGReflRightCo, mkTcGReflLeftCo, mkTcPhantomCo,
+  mkTcCoherenceLeftCo,
+  mkTcCoherenceRightCo,
   mkTcKindCo,
   tcCoercionKind, coVarsOfTcCo,
   mkTcCoVarCo,
@@ -115,8 +117,12 @@ mkTcSubCo              :: TcCoercionN -> TcCoercionR
 maybeTcSubCo           :: EqRel -> TcCoercion -> TcCoercion
 tcDowngradeRole        :: Role -> Role -> TcCoercion -> TcCoercion
 mkTcAxiomRuleCo        :: CoAxiomRule -> [TcCoercion] -> TcCoercionR
-mkTcCoherenceLeftCo    :: TcCoercion -> TcCoercionN -> TcCoercion
-mkTcCoherenceRightCo   :: TcCoercion -> TcCoercionN -> TcCoercion
+mkTcGReflRightCo       :: Role -> TcType -> TcCoercionN -> TcCoercion
+mkTcGReflLeftCo        :: Role -> TcType -> TcCoercionN -> TcCoercion
+mkTcCoherenceLeftCo    :: Role -> TcType -> TcCoercionN
+                       -> TcCoercion -> TcCoercion
+mkTcCoherenceRightCo   :: Role -> TcType -> TcCoercionN
+                       -> TcCoercion -> TcCoercion
 mkTcPhantomCo          :: TcCoercionN -> TcType -> TcType -> TcCoercionP
 mkTcKindCo             :: TcCoercion -> TcCoercionN
 mkTcCoVarCo            :: CoVar -> TcCoercion
@@ -148,6 +154,8 @@ mkTcSubCo              = mkSubCo
 maybeTcSubCo           = maybeSubCo
 tcDowngradeRole        = downgradeRole
 mkTcAxiomRuleCo        = mkAxiomRuleCo
+mkTcGReflRightCo       = mkGReflRightCo
+mkTcGReflLeftCo        = mkGReflLeftCo
 mkTcCoherenceLeftCo    = mkCoherenceLeftCo
 mkTcCoherenceRightCo   = mkCoherenceRightCo
 mkTcPhantomCo          = mkPhantomCo
diff --git a/compiler/typecheck/TcFlatten.hs b/compiler/typecheck/TcFlatten.hs
index f6a1adf45e..ee13091681 100644
--- a/compiler/typecheck/TcFlatten.hs
+++ b/compiler/typecheck/TcFlatten.hs
@@ -1115,6 +1115,17 @@ as desired. (Why do we want Star? Because we started with something of kind Star
 
 Whew.
 
+Note [flatten_exact_fam_app_fully performance]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+The refactor of GRefl seems to cause performance trouble for T9872x: the allocation of flatten_exact_fam_app_fully_performance increased. See note [Generalized reflexive coercion] in TyCoRep for more information about GRefl and Trac #15192 for the current state.
+
+The explicit pattern match in homogenise_result helps with T9872a, b, c.
+
+Still, it increases the expected allocation of T9872d by ~2%.
+
+TODO: a step-by-step replay of the refactor to analyze the performance.
+
 -}
 
 {-# INLINE flatten_args_tc #-}
@@ -1208,12 +1219,12 @@ flatten_args_fast orig_binders orig_inner_ki orig_roles orig_tys
           --
           --   let kind_co = mkTcSymCo $ mkReflCo Nominal (tyBinderType binder)
           --       casted_xi = xi `mkCastTy` kind_co
-          --       casted_co = co `mkTcCoherenceLeftCo` kind_co
+          --       casted_co = xi |> kind_co ~r xi ; co
           --
           -- but this isn't necessary:
           --   mkTcSymCo (Refl a b) = Refl a b,
           --   mkCastTy x (Refl _ _) = x
-          --   mkTcCoherenceLeftCo x (Refl _ _) = x
+          --   mkTcGReflLeftCo _ ty (Refl _ _) `mkTransCo` co = co
           --
           -- Also, no need to check isAnonTyBinder or isNamedTyBinder, since
           -- we've already established that they're all anonymous.
@@ -1229,7 +1240,7 @@ flatten_args_fast orig_binders orig_inner_ki orig_roles orig_tys
     finish (xis, cos, binders) = (xis, cos, kind_co)
       where
         final_kind = mkPiTys binders orig_inner_ki
-        kind_co    = mkReflCo Nominal final_kind
+        kind_co    = mkNomReflCo final_kind
 
 {-# INLINE flatten_args_slow #-}
 -- | Slow path, compared to flatten_args_fast, because this one must track
@@ -1283,7 +1294,7 @@ flatten_args_slow orig_binders orig_inner_ki orig_fvs orig_roles orig_tys
            ; let kind_co = mkTcSymCo $
                    liftCoSubst Nominal lc (tyBinderType binder)
                  !casted_xi = xi `mkCastTy` kind_co
-                 casted_co = co `mkTcCoherenceLeftCo` kind_co
+                 casted_co =  mkTcCoherenceLeftCo role xi kind_co co
 
              -- now, extend the lifting context with the new binding
                  !new_lc | Just tv <- tyBinderVar_maybe binder
@@ -1314,13 +1325,13 @@ flatten_args_slow orig_binders orig_inner_ki orig_fvs orig_roles orig_tys
                <- go acc_xis acc_cos zapped_lc bndrs new_inner roles casted_tys
            -- cos_out :: xis_out ~ casted_tys
            -- we need to return cos :: xis_out ~ tys
-           --
-           -- zipWith has the map first because it will fuse.
-           ; let cos = zipWith (flip mkTcCoherenceRightCo)
-                               (map mkTcSymCo arg_cos)
-                               cos_out
+           ; let cos = zipWith3 mkTcGReflRightCo
+                                roles
+                                casted_tys
+                                (map mkTcSymCo arg_cos)
+                 cos' = zipWith mkTransCo cos_out cos
 
-           ; return (xis_out, cos, res_co_out `mkTcTransCo` res_co) }
+           ; return (xis_out, cos', res_co_out `mkTcTransCo` res_co) }
 
     go _ _ _ _ _ _ _ = pprPanic
         "flatten_args wandered into deeper water than usual" (vcat [])
@@ -1408,7 +1419,8 @@ flatten_one (CastTy ty g)
   = do { (xi, co) <- flatten_one ty
        ; (g', _)   <- flatten_co g
 
-       ; return (mkCastTy xi g', castCoercionKind co g' g) }
+       ; role <- getRole
+       ; return (mkCastTy xi g', castCoercionKind co role xi ty g' g) }
 
 flatten_one (CoercionTy co) = first mkCoercionTy <$> flatten_co co
 
@@ -1471,7 +1483,8 @@ flatten_app_ty_args fun_xi fun_co arg_tys
                       arg_co = mkAppCos fun_co arg_cos
                 ; return (arg_xi, arg_co, kind_co) }
 
-       ; return (homogenise_result xi co kind_co) }
+       ; role <- getRole
+       ; return (homogenise_result xi co role kind_co) }
 
 flatten_ty_con_app :: TyCon -> [TcType] -> FlatM (Xi, Coercion)
 flatten_ty_con_app tc tys
@@ -1479,18 +1492,21 @@ flatten_ty_con_app tc tys
        ; (xis, cos, kind_co) <- flatten_args_tc tc (tyConRolesX role tc) tys
        ; let tyconapp_xi = mkTyConApp tc xis
              tyconapp_co = mkTyConAppCo role tc cos
-       ; return (homogenise_result tyconapp_xi tyconapp_co kind_co) }
+       ; return (homogenise_result tyconapp_xi tyconapp_co role kind_co) }
 
 -- Make the result of flattening homogeneous (Note [Flattening] (F2))
 homogenise_result :: Xi              -- a flattened type
-                  -> Coercion        -- :: xi ~ original ty
+                  -> Coercion        -- :: xi ~r original ty
+                  -> Role            -- r
                   -> CoercionN       -- kind_co :: typeKind(xi) ~N typeKind(ty)
                   -> (Xi, Coercion)  -- (xi |> kind_co, (xi |> kind_co)
-                                     --   ~ original ty)
-homogenise_result xi co kind_co
-  = let xi' = xi `mkCastTy` kind_co
-        co' = co `mkTcCoherenceLeftCo` kind_co
-    in  (xi', co')
+                                     --   ~r original ty)
+homogenise_result xi co r kind_co
+  -- the explicit pattern match here improves the performance of T9872a, b, c by
+  -- ~2%
+  | isGReflCo kind_co = (xi `mkCastTy` kind_co, co)
+  | otherwise         = (xi `mkCastTy` kind_co
+                        , (mkSymCo $ GRefl r xi (MCo kind_co)) `mkTransCo` co)
 {-# INLINE homogenise_result #-}
 
 -- Flatten a vector (list of arguments).
@@ -1588,6 +1604,7 @@ flatten_fam_app tc tys  -- Can be over-saturated
          ; flatten_app_ty_args xi1 co1 tys_rest } } }
 
 -- the [TcType] exactly saturate the TyCon
+-- See note [flatten_exact_fam_app_fully performance]
 flatten_exact_fam_app_fully :: TyCon -> [TcType] -> FlatM (Xi, Coercion)
 flatten_exact_fam_app_fully tc tys
   -- See Note [Reduce type family applications eagerly]
@@ -1625,10 +1642,10 @@ flatten_exact_fam_app_fully tc tys
                                   -- flatten it
                                   -- fsk_co :: fsk_xi ~ fsk
                            ; let xi  = fsk_xi `mkCastTy` kind_co
-                                 co' = (fsk_co `mkTcCoherenceLeftCo` kind_co)
-                                        `mkTransCo`
-                                        maybeSubCo eq_rel (mkSymCo co)
-                                        `mkTransCo` ret_co
+                                 co' = mkTcCoherenceLeftCo role fsk_xi kind_co fsk_co
+                                       `mkTransCo`
+                                       maybeSubCo eq_rel (mkSymCo co)
+                                       `mkTransCo` ret_co
                            ; return (xi, co')
                            }
                                             -- :: fsk_xi ~ F xis
@@ -1658,12 +1675,12 @@ flatten_exact_fam_app_fully tc tys
                                  ; traceFlat "flatten/flat-cache miss" $
                                      (ppr tc <+> ppr xis $$ ppr fsk $$ ppr ev)
 
-                                 -- NB: fsk's kind is already flattend because
+                                 -- NB: fsk's kind is already flattened because
                                  --     the xis are flattened
-                                 ; let xi = mkTyVarTy fsk `mkCastTy` kind_co
-                                       co' = (maybeSubCo eq_rel (mkSymCo co)
-                                               `mkTcCoherenceLeftCo` kind_co)
-                                              `mkTransCo` ret_co
+                                 ; let fsk_ty = mkTyVarTy fsk
+                                       xi = fsk_ty `mkCastTy` kind_co
+                                       co' = mkTcCoherenceLeftCo role fsk_ty kind_co (maybeSubCo eq_rel (mkSymCo co))
+                                             `mkTransCo` ret_co
                                  ; return (xi, co')
                                  }
                            }
@@ -1707,9 +1724,10 @@ flatten_exact_fam_app_fully tc tys
                        ; when (eq_rel == NomEq) $
                          liftTcS $
                          extendFlatCache tc tys ( co, xi, flavour )
-                       ; let xi' = xi `mkCastTy` kind_co
-                             co' = update_co $ mkSymCo co
-                                                `mkTcCoherenceLeftCo` kind_co
+                       ; let role = eqRelRole eq_rel
+                             xi' = xi `mkCastTy` kind_co
+                             co' = update_co $
+                                   mkTcCoherenceLeftCo role xi kind_co (mkSymCo co)
                        ; return $ Just (xi', co') }
                Nothing -> pure Nothing }
 
@@ -1735,9 +1753,10 @@ flatten_exact_fam_app_fully tc tys
                        ; eq_rel <- getEqRel
                        ; let co  = maybeSubCo eq_rel norm_co
                                     `mkTransCo` mkSymCo final_co
+                             role = eqRelRole eq_rel
                              xi' = xi `mkCastTy` kind_co
-                             co' = update_co $ mkSymCo co
-                                                `mkTcCoherenceLeftCo` kind_co
+                             co' = update_co $
+                                   mkTcCoherenceLeftCo role xi kind_co (mkSymCo co)
                        ; return $ Just (xi', co') }
                Nothing -> pure Nothing }
 
diff --git a/compiler/typecheck/TcTyDecls.hs b/compiler/typecheck/TcTyDecls.hs
index cce0f02a0b..f64b9f3e73 100644
--- a/compiler/typecheck/TcTyDecls.hs
+++ b/compiler/typecheck/TcTyDecls.hs
@@ -32,7 +32,7 @@ import GhcPrelude
 import TcRnMonad
 import TcEnv
 import TcBinds( tcValBinds, addTypecheckedBinds )
-import TyCoRep( Type(..), Coercion(..), UnivCoProvenance(..) )
+import TyCoRep( Type(..), Coercion(..), MCoercion(..), UnivCoProvenance(..) )
 import TcType
 import TysWiredIn( unitTy )
 import MkCore( rEC_SEL_ERROR_ID )
@@ -111,7 +111,11 @@ synonymTyConsOfType ty
      -- in the same recursive group.  Possibly this restriction will be
      -- lifted in the future but for now, this code is "just for completeness
      -- sake".
-     go_co (Refl _ ty)            = go ty
+     go_mco MRefl    = emptyNameEnv
+     go_mco (MCo co) = go_co co
+
+     go_co (Refl ty)              = go ty
+     go_co (GRefl _ ty mco)       = go ty `plusNameEnv` go_mco mco
      go_co (TyConAppCo _ tc cs)   = go_tc tc `plusNameEnv` go_co_s cs
      go_co (AppCo co co')         = go_co co `plusNameEnv` go_co co'
      go_co (ForAllCo _ co co')    = go_co co `plusNameEnv` go_co co'
@@ -125,7 +129,6 @@ synonymTyConsOfType ty
      go_co (NthCo _ _ co)         = go_co co
      go_co (LRCo _ co)            = go_co co
      go_co (InstCo co co')        = go_co co `plusNameEnv` go_co co'
-     go_co (CoherenceCo co co')   = go_co co `plusNameEnv` go_co co'
      go_co (KindCo co)            = go_co co
      go_co (SubCo co)             = go_co co
      go_co (AxiomRuleCo _ cs)     = go_co_s cs
diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index 092c5a1923..00bae72117 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -936,7 +936,11 @@ exactTyCoVarsOfType ty
     go (CastTy ty co)       = go ty `unionVarSet` goCo co
     go (CoercionTy co)      = goCo co
 
-    goCo (Refl _ ty)        = go ty
+    goMCo MRefl    = emptyVarSet
+    goMCo (MCo co) = goCo co
+
+    goCo (Refl ty)            = go ty
+    goCo (GRefl _ ty mco)     = go ty `unionVarSet` goMCo mco
     goCo (TyConAppCo _ _ args)= goCos args
     goCo (AppCo co arg)     = goCo co `unionVarSet` goCo arg
     goCo (ForAllCo tv k_co co)
@@ -951,7 +955,6 @@ exactTyCoVarsOfType ty
     goCo (NthCo _ _ co)      = goCo co
     goCo (LRCo _ co)         = goCo co
     goCo (InstCo co arg)     = goCo co `unionVarSet` goCo arg
-    goCo (CoherenceCo c1 c2) = goCo c1 `unionVarSet` goCo c2
     goCo (KindCo co)         = goCo co
     goCo (SubCo co)          = goCo co
     goCo (AxiomRuleCo _ c)   = goCos c
diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs
index eb44bc385f..08a5c59879 100644
--- a/compiler/typecheck/TcUnify.hs
+++ b/compiler/typecheck/TcUnify.hs
@@ -971,7 +971,7 @@ promoteTcType dest_lvl ty
                                           , uo_thing    = Nothing
                                           , uo_visible  = False }
            ; ki_co <- uType KindLevel kind_orig (typeKind ty) res_kind
-           ; let co = mkTcNomReflCo ty `mkTcCoherenceRightCo` ki_co
+           ; let co = mkTcGReflRightCo Nominal ty ki_co
            ; return (co, ty `mkCastTy` ki_co) }
 
 {- Note [Promoting a type]
@@ -1265,7 +1265,7 @@ uType, uType_defer
   -> CtOrigin
   -> TcType    -- ty1 is the *actual* type
   -> TcType    -- ty2 is the *expected* type
-  -> TcM Coercion
+  -> TcM CoercionN
 
 --------------
 -- It is always safe to defer unification to the main constraint solver
@@ -1300,7 +1300,7 @@ uType t_or_k origin orig_ty1 orig_ty2
             else traceTc "u_tys yields coercion:" (ppr co)
        ; return co }
   where
-    go :: TcType -> TcType -> TcM Coercion
+    go :: TcType -> TcType -> TcM CoercionN
         -- The arguments to 'go' are always semantically identical
         -- to orig_ty{1,2} except for looking through type synonyms
 
@@ -1324,15 +1324,15 @@ uType t_or_k origin orig_ty1 orig_ty2
       -- See Note [Expanding synonyms during unification]
     go ty1@(TyConApp tc1 []) (TyConApp tc2 [])
       | tc1 == tc2
-      = return $ mkReflCo Nominal ty1
+      = return $ mkNomReflCo ty1
 
     go (CastTy t1 co1) t2
       = do { co_tys <- go t1 t2
-           ; return (mkCoherenceLeftCo co_tys co1) }
+           ; return (mkCoherenceLeftCo Nominal t1 co1 co_tys) }
 
     go t1 (CastTy t2 co2)
       = do { co_tys <- go t1 t2
-           ; return (mkCoherenceRightCo co_tys co2) }
+           ; return ( mkCoherenceRightCo Nominal t2 co2 co_tys) }
 
         -- See Note [Expanding synonyms during unification]
         --
diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index 60fb2618c3..d51fa9d4b6 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -2030,8 +2030,13 @@ fvType (CoercionTy co)       = fvCo co
 fvTypes :: [Type] -> [TyVar]
 fvTypes tys                = concat (map fvType tys)
 
+fvMCo :: MCoercion -> [TyCoVar]
+fvMCo MRefl    = []
+fvMCo (MCo co) = fvCo co
+
 fvCo :: Coercion -> [TyCoVar]
-fvCo (Refl _ ty)            = fvType ty
+fvCo (Refl ty)              = fvType ty
+fvCo (GRefl _ ty mco)       = fvType ty ++ fvMCo mco
 fvCo (TyConAppCo _ _ args)  = concatMap fvCo args
 fvCo (AppCo co arg)         = fvCo co ++ fvCo arg
 fvCo (ForAllCo tv h co)     = filter (/= tv) (fvCo co) ++ fvCo h
@@ -2044,7 +2049,6 @@ fvCo (TransCo co1 co2)      = fvCo co1 ++ fvCo co2
 fvCo (NthCo _ _ co)         = fvCo co
 fvCo (LRCo _ co)            = fvCo co
 fvCo (InstCo co arg)        = fvCo co ++ fvCo arg
-fvCo (CoherenceCo co1 co2)  = fvCo co1 ++ fvCo co2
 fvCo (KindCo co)            = fvCo co
 fvCo (SubCo co)             = fvCo co
 fvCo (AxiomRuleCo _ cs)     = concatMap fvCo cs
diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs
index 346190c7a7..8493a4ae82 100644
--- a/compiler/types/Coercion.hs
+++ b/compiler/types/Coercion.hs
@@ -23,7 +23,7 @@ module Coercion (
         coercionRole, coercionKindRole,
 
         -- ** Constructing coercions
-        mkReflCo, mkRepReflCo, mkNomReflCo,
+        mkGReflCo, mkReflCo, mkRepReflCo, mkNomReflCo,
         mkCoVarCo, mkCoVarCos,
         mkAxInstCo, mkUnbranchedAxInstCo,
         mkAxInstRHS, mkUnbranchedAxInstRHS,
@@ -37,8 +37,8 @@ module Coercion (
         mkUnsafeCo, mkHoleCo, mkUnivCo, mkSubCo,
         mkAxiomInstCo, mkProofIrrelCo,
         downgradeRole, maybeSubCo, mkAxiomRuleCo,
-        mkCoherenceCo, mkCoherenceRightCo, mkCoherenceLeftCo,
-        mkKindCo, castCoercionKind,
+        mkGReflRightCo, mkGReflLeftCo, mkCoherenceLeftCo, mkCoherenceRightCo,
+        mkKindCo, castCoercionKind, castCoercionKindI,
 
         mkHeteroCoercionType,
 
@@ -59,7 +59,7 @@ module Coercion (
 
         pickLR,
 
-        isReflCo, isReflCo_maybe, isReflexiveCo, isReflexiveCo_maybe,
+        isGReflCo, isReflCo, isReflCo_maybe, isGReflCo_maybe, isReflexiveCo, isReflexiveCo_maybe,
         isReflCoVar_maybe,
 
         -- ** Coercion variables
@@ -295,13 +295,14 @@ decomposePiCos orig_kind orig_args orig_co = go [] orig_subst orig_kind orig_arg
        -> ([CoercionN], Coercion)
     go acc_arg_cos subst  ki  (ty:tys) co
       | Just (kv, inner_ki) <- splitForAllTy_maybe ki
-        -- know     co :: (forall a:s1.t1) ~ (forall b:s2.t2)
-        --    function :: forall a:s1.t1   (the function is not passed to decomposePiCos)
-        --          ty :: s2
-        -- need arg_co :: s2 ~ s1
-        --      res_co :: t1[ty |> arg_co / a] ~ t2[ty / b]
+        -- know       co :: (forall a:s1.t1) ~ (forall b:s2.t2)
+        --      function :: forall a:s1.t1
+        --                  (the function is not passed to decomposePiCos)
+        --            ty :: s2
+        -- need   arg_co :: s2 ~ s1
+        --        res_co :: t1[ty |> arg_co / a] ~ t2[ty / b]
       = let arg_co = mkNthCo Nominal 0 (mkSymCo co)
-            res_co = mkInstCo co (mkNomReflCo ty `mkCoherenceLeftCo` arg_co)
+            res_co = mkInstCo co (mkGReflLeftCo Nominal ty arg_co)
             subst' = extendTCvSubst subst kv ty
         in
         go (arg_co : acc_arg_cos) subst' inner_ki tys res_co
@@ -337,7 +338,8 @@ getCoVar_maybe _            = Nothing
 -- | Attempts to tease a coercion apart into a type constructor and the application
 -- of a number of coercion arguments to that constructor
 splitTyConAppCo_maybe :: Coercion -> Maybe (TyCon, [Coercion])
-splitTyConAppCo_maybe (Refl r ty)
+splitTyConAppCo_maybe co
+  | Just (ty, r) <- isReflCo_maybe co
   = do { (tc, tys) <- splitTyConApp_maybe ty
        ; let args = zipWith mkReflCo (tyConRolesX r tc) tys
        ; return (tc, args) }
@@ -363,8 +365,9 @@ splitAppCo_maybe (TyConAppCo r tc args)
        -- Use mkTyConAppCo to preserve the invariant
        --  that identity coercions are always represented by Refl
 
-splitAppCo_maybe (Refl r ty)
-  | Just (ty1, ty2) <- splitAppTy_maybe ty
+splitAppCo_maybe co
+  | Just (ty, r) <- isReflCo_maybe co
+  , Just (ty1, ty2) <- splitAppTy_maybe ty
   = Just (mkReflCo r ty1, mkNomReflCo ty2)
 splitAppCo_maybe _ = Nothing
 
@@ -446,23 +449,46 @@ isReflCoVar_maybe cv
   | isCoVar cv
   , Pair ty1 ty2 <- coVarTypes cv
   , ty1 `eqType` ty2
-  = Just (Refl (coVarRole cv) ty1)
+  = Just (mkReflCo (coVarRole cv) ty1)
   | otherwise
   = Nothing
 
+-- | Tests if this coercion is obviously a generalized reflexive coercion.
+-- Guaranteed to work very quickly.
+isGReflCo :: Coercion -> Bool
+isGReflCo (GRefl{}) = True
+isGReflCo (Refl{})  = True -- Refl ty == GRefl N ty MRefl
+isGReflCo _         = False
+
+-- | Tests if this MCoercion is obviously generalized reflexive
+-- Guaranteed to work very quickly.
+isGReflMCo :: MCoercion -> Bool
+isGReflMCo MRefl = True
+isGReflMCo (MCo co) | isGReflCo co = True
+isGReflMCo _ = False
+
 -- | Tests if this coercion is obviously reflexive. Guaranteed to work
 -- very quickly. Sometimes a coercion can be reflexive, but not obviously
 -- so. c.f. 'isReflexiveCo'
 isReflCo :: Coercion -> Bool
-isReflCo (Refl {}) = True
-isReflCo _         = False
+isReflCo (Refl{}) = True
+isReflCo (GRefl _ _ mco) | isGReflMCo mco = True
+isReflCo _ = False
+
+-- | Returns the type coerced if this coercion is a generalized reflexive
+-- coercion. Guaranteed to work very quickly.
+isGReflCo_maybe :: Coercion -> Maybe (Type, Role)
+isGReflCo_maybe (GRefl r ty _) = Just (ty, r)
+isGReflCo_maybe (Refl ty)      = Just (ty, Nominal)
+isGReflCo_maybe _ = Nothing
 
 -- | Returns the type coerced if this coercion is reflexive. Guaranteed
 -- to work very quickly. Sometimes a coercion can be reflexive, but not
 -- obviously so. c.f. 'isReflexiveCo_maybe'
 isReflCo_maybe :: Coercion -> Maybe (Type, Role)
-isReflCo_maybe (Refl r ty) = Just (ty, r)
-isReflCo_maybe _           = Nothing
+isReflCo_maybe (Refl ty) = Just (ty, Nominal)
+isReflCo_maybe (GRefl r ty mco) | isGReflMCo mco = Just (ty, r)
+isReflCo_maybe _ = Nothing
 
 -- | Slowly checks if the coercion is reflexive. Don't call this in a loop,
 -- as it walks over the entire coercion.
@@ -472,7 +498,8 @@ isReflexiveCo = isJust . isReflexiveCo_maybe
 -- | Extracts the coerced type from a reflexive coercion. This potentially
 -- walks over the entire coercion, so avoid doing this in a loop.
 isReflexiveCo_maybe :: Coercion -> Maybe (Type, Role)
-isReflexiveCo_maybe (Refl r ty) = Just (ty, r)
+isReflexiveCo_maybe (Refl ty) = Just (ty, Nominal)
+isReflexiveCo_maybe (GRefl r ty mco) | isGReflMCo mco = Just (ty, r)
 isReflexiveCo_maybe co
   | ty1 `eqType` ty2
   = Just (ty1, r)
@@ -542,17 +569,25 @@ role is bizarre and a caller should have to ask for this behavior explicitly.
 
 -}
 
+-- | Make a generalized reflexive coercion
+mkGReflCo :: Role -> Type -> MCoercionN -> Coercion
+mkGReflCo r ty mco
+  | isGReflMCo mco = if r == Nominal then Refl ty
+                     else GRefl r ty MRefl
+  | otherwise    = GRefl r ty mco
+
+-- | Make a reflexive coercion
 mkReflCo :: Role -> Type -> Coercion
-mkReflCo r ty
-  = Refl r ty
+mkReflCo Nominal ty = Refl ty
+mkReflCo r       ty = GRefl r ty MRefl
 
 -- | Make a representational reflexive coercion
 mkRepReflCo :: Type -> Coercion
-mkRepReflCo = mkReflCo Representational
+mkRepReflCo ty = GRefl Representational ty MRefl
 
 -- | Make a nominal reflexive coercion
 mkNomReflCo :: Type -> Coercion
-mkNomReflCo = mkReflCo Nominal
+mkNomReflCo = Refl
 
 -- | Apply a type constructor to a list of coercions. It is the
 -- caller's responsibility to get the roles correct on argument coercions.
@@ -570,7 +605,8 @@ mkTyConAppCo r tc cos
   = mkAppCos (liftCoSubst r (mkLiftingContext tv_co_prs) rhs_ty) leftover_cos
 
   | Just tys_roles <- traverse isReflCo_maybe cos
-  = Refl r (mkTyConApp tc (map fst tys_roles))    -- See Note [Refl invariant]
+  = mkReflCo r (mkTyConApp tc (map fst tys_roles))
+  -- See Note [Refl invariant]
 
   | otherwise = TyConAppCo r tc cos
 
@@ -581,7 +617,7 @@ mkFunCo r co1 co2
     -- See Note [Refl invariant]
   | Just (ty1, _) <- isReflCo_maybe co1
   , Just (ty2, _) <- isReflCo_maybe co2
-  = Refl r (mkFunTy ty1 ty2)
+  = mkReflCo r (mkFunTy ty1 ty2)
   | otherwise = FunCo r co1 co2
 
 -- | Apply a 'Coercion' to another 'Coercion'.
@@ -590,11 +626,13 @@ mkFunCo r co1 co2
 mkAppCo :: Coercion     -- ^ :: t1 ~r t2
         -> Coercion     -- ^ :: s1 ~N s2, where s1 :: k1, s2 :: k2
         -> Coercion     -- ^ :: t1 s1 ~r t2 s2
-mkAppCo (Refl r ty1) arg
-  | Just (ty2, _) <- isReflCo_maybe arg
-  = Refl r (mkAppTy ty1 ty2)
+mkAppCo co arg
+  | Just (ty1, r) <- isReflCo_maybe co
+  , Just (ty2, _) <- isReflCo_maybe arg
+  = mkReflCo r (mkAppTy ty1 ty2)
 
-  | Just (tc, tys) <- splitTyConApp_maybe ty1
+  | Just (ty1, r) <- isReflCo_maybe co
+  , Just (tc, tys) <- splitTyConApp_maybe ty1
     -- Expand type synonyms; a TyConAppCo can't have a type synonym (Trac #9102)
   = mkTyConAppCo r tc (zip_roles (tyConRolesX r tc) tys)
   where
@@ -687,27 +725,31 @@ mkTransAppCo r1 co1 ty1a ty1b r2 co2 ty2a ty2b r3
 -- The kind of the tyvar should be the left-hand kind of the kind coercion.
 mkForAllCo :: TyVar -> Coercion -> Coercion -> Coercion
 mkForAllCo tv kind_co co
-  | Refl r ty <- co
-  , Refl {} <- kind_co
-  = Refl r (mkInvForAllTy tv ty)
+  | Just (ty, r) <- isReflCo_maybe co
+  , isGReflCo kind_co
+  = mkReflCo r (mkInvForAllTy tv ty)
   | otherwise
   = ForAllCo tv kind_co co
 
 -- | Make nested ForAllCos
 mkForAllCos :: [(TyVar, Coercion)] -> Coercion -> Coercion
-mkForAllCos bndrs (Refl r ty)
+mkForAllCos bndrs co
+  | Just (ty, r ) <- isReflCo_maybe co
   = let (refls_rev'd, non_refls_rev'd) = span (isReflCo . snd) (reverse bndrs) in
     foldl (flip $ uncurry ForAllCo)
-          (Refl r $ mkInvForAllTys (reverse (map fst refls_rev'd)) ty)
+          (mkReflCo r (mkInvForAllTys (reverse (map fst refls_rev'd)) ty))
           non_refls_rev'd
-mkForAllCos bndrs co = foldr (uncurry ForAllCo) co bndrs
+  | otherwise
+  = foldr (uncurry ForAllCo) co bndrs
 
 -- | Make a Coercion quantified over a type variable;
 -- the variable has the same type in both sides of the coercion
 mkHomoForAllCos :: [TyVar] -> Coercion -> Coercion
-mkHomoForAllCos tvs (Refl r ty)
-  = Refl r (mkInvForAllTys tvs ty)
-mkHomoForAllCos tvs ty = mkHomoForAllCos_NoRefl tvs ty
+mkHomoForAllCos tvs co
+  | Just (ty, r) <- isReflCo_maybe co
+  = mkReflCo r (mkInvForAllTys tvs ty)
+  | otherwise
+  = mkHomoForAllCos_NoRefl tvs co
 
 -- | Like 'mkHomoForAllCos', but doesn't check if the inner coercion
 -- is reflexive.
@@ -834,7 +876,7 @@ mkUnivCo :: UnivCoProvenance
          -> Type       -- ^ t2 :: k2
          -> Coercion   -- ^ :: t1 ~r t2
 mkUnivCo prov role ty1 ty2
-  | ty1 `eqType` ty2 = Refl role ty1
+  | ty1 `eqType` ty2 = mkReflCo role ty1
   | otherwise        = UnivCo prov role ty1 ty2
 
 -- | Create a symmetric version of the given 'Coercion' that asserts
@@ -844,7 +886,7 @@ mkSymCo :: Coercion -> Coercion
 
 -- Do a few simple optimizations, but don't bother pushing occurrences
 -- of symmetry to the leaves; the optimizer will take care of that.
-mkSymCo co@(Refl {})              = co
+mkSymCo co | isReflCo co          = co
 mkSymCo    (SymCo co)             = co
 mkSymCo    (SubCo (SymCo co))     = SubCo co
 mkSymCo co                        = SymCo co
@@ -852,9 +894,11 @@ mkSymCo co                        = SymCo co
 -- | Create a new 'Coercion' by composing the two given 'Coercion's transitively.
 --   (co1 ; co2)
 mkTransCo :: Coercion -> Coercion -> Coercion
-mkTransCo co1 (Refl {}) = co1
-mkTransCo (Refl {}) co2 = co2
-mkTransCo co1 co2       = TransCo co1 co2
+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
 
 mkNthCo :: HasDebugCallStack
         => Role  -- the role of the coercion you're creating
@@ -867,17 +911,19 @@ mkNthCo r n co
   where
     Pair ty1 ty2 = coercionKind co
 
-    go r 0 (Refl _ ty)
-      | Just (tv, _) <- splitForAllTy_maybe ty
+    go r 0 co
+      | Just (ty, _) <- isReflCo_maybe co
+      , Just (tv, _) <- splitForAllTy_maybe ty
       = ASSERT( r == Nominal )
-        Refl r (tyVarKind tv)
-    go r n (Refl r0 ty)
+        mkReflCo r (tyVarKind tv)
+
+    go r n co
+      | Just (ty, r0) <- isReflCo_maybe co
+      , let tc = tyConAppTyCon ty
       = ASSERT2( ok_tc_app ty n, ppr n $$ ppr ty )
         ASSERT( nthRole r0 tc n == r )
         mkReflCo r (tyConAppArgN n ty)
-      where tc = tyConAppTyCon ty
-
-            ok_tc_app :: Type -> Int -> Bool
+      where ok_tc_app :: Type -> Int -> Bool
             ok_tc_app ty n
               | Just (_, tys) <- splitTyConApp_maybe ty
               = tys `lengthExceeds` n
@@ -978,43 +1024,59 @@ nthCoRole n co
     (Pair lty _, r) = coercionKindRole co
 
 mkLRCo :: LeftOrRight -> Coercion -> Coercion
-mkLRCo lr (Refl eq ty) = Refl eq (pickLR lr (splitAppTy ty))
-mkLRCo lr co           = LRCo lr co
+mkLRCo lr co
+  | Just (ty, eq) <- isReflCo_maybe co
+  = mkReflCo eq (pickLR lr (splitAppTy ty))
+  | otherwise
+  = LRCo lr co
 
 -- | Instantiates a 'Coercion'.
 mkInstCo :: Coercion -> Coercion -> Coercion
-mkInstCo (ForAllCo tv _kind_co body_co) (Refl _ arg)
+mkInstCo (ForAllCo tv _kind_co body_co) co
+  | Just (arg, _) <- isReflCo_maybe co
   = substCoWithUnchecked [tv] [arg] body_co
 mkInstCo co arg = InstCo co arg
 
--- This could work harder to produce Refl coercions, but that would be
--- quite inefficient. Seems better not to try.
-mkCoherenceCo :: Coercion -> Coercion -> Coercion
-mkCoherenceCo co1 (Refl {}) = co1
-mkCoherenceCo (CoherenceCo co1 co2) co3
-  = CoherenceCo co1 (co2 `mkTransCo` co3)
-mkCoherenceCo co1 co2     = CoherenceCo co1 co2
-
--- | A CoherenceCo c1 c2 applies the coercion c2 to the left-hand type
--- in the kind of c1. This function uses sym to get the coercion on the
--- right-hand type of c1. Thus, if c1 :: s ~ t, then mkCoherenceRightCo c1 c2
--- has the kind (s ~ (t |> c2)) down through type constructors.
--- The second coercion must be representational.
-mkCoherenceRightCo :: Coercion -> Coercion -> Coercion
-mkCoherenceRightCo c1 c2 = mkSymCo (mkCoherenceCo (mkSymCo c1) c2)
-
--- | An explicitly directed synonym of mkCoherenceCo. The second
--- coercion must be representational.
-mkCoherenceLeftCo :: Coercion -> Coercion -> Coercion
-mkCoherenceLeftCo = mkCoherenceCo
-
-infixl 5 `mkCoherenceCo`
-infixl 5 `mkCoherenceRightCo`
-infixl 5 `mkCoherenceLeftCo`
+-- | Given @ty :: k1@, @co :: k1 ~ k2@,
+-- produces @co' :: ty ~r (ty |> co)@
+mkGReflRightCo :: Role -> Type -> CoercionN -> Coercion
+mkGReflRightCo r ty co
+  | isGReflCo co = mkReflCo r ty
+    -- the kinds of @k1@ and @k2@ are the same, thus @isGReflCo@
+    -- instead of @isReflCo@
+  | otherwise = GRefl r ty (MCo co)
+
+-- | Given @ty :: k1@, @co :: k1 ~ k2@,
+-- produces @co' :: (ty |> co) ~r ty@
+mkGReflLeftCo :: Role -> Type -> CoercionN -> Coercion
+mkGReflLeftCo r ty co
+  | isGReflCo co = mkReflCo r ty
+    -- the kinds of @k1@ and @k2@ are the same, thus @isGReflCo@
+    -- instead of @isReflCo@
+  | otherwise    = mkSymCo $ GRefl r ty (MCo co)
+
+-- | Given @ty :: k2@, @co :: k1 ~ k2@, @co2:: ty ~ ty'@,
+-- produces @co' :: (ty |> co) ~r ty'
+-- It is not only a utility function, but it saves allocation when co
+-- is a GRefl coercion.
+mkCoherenceLeftCo :: Role -> Type -> CoercionN -> Coercion -> Coercion
+mkCoherenceLeftCo r ty co co2
+  | isGReflCo co = co2
+  | otherwise = (mkSymCo $ GRefl r ty (MCo co)) `mkTransCo` co2
+
+-- | Given @ty :: k2@, @co :: k1 ~ k2@, @co2:: ty' ~ ty@,
+-- produces @co' :: ty' ~r (ty |> co)
+-- It is not only a utility function, but it saves allocation when co
+-- is a GRefl coercion.
+mkCoherenceRightCo :: Role -> Type -> CoercionN -> Coercion -> Coercion
+mkCoherenceRightCo r ty co co2
+  | isGReflCo co = co2
+  | otherwise = co2 `mkTransCo` GRefl r ty (MCo co)
 
 -- | Given @co :: (a :: k) ~ (b :: k')@ produce @co' :: k ~ k'@.
 mkKindCo :: Coercion -> Coercion
-mkKindCo (Refl _ ty) = Refl Nominal (typeKind ty)
+mkKindCo co | Just (ty, _) <- isReflCo_maybe co = Refl (typeKind ty)
+mkKindCo (GRefl _ _ (MCo co)) = co
 mkKindCo (UnivCo (PhantomProv h) _ _ _)    = h
 mkKindCo (UnivCo (ProofIrrelProv h) _ _ _) = h
 mkKindCo co
@@ -1025,14 +1087,15 @@ mkKindCo co
   , let tk1 = typeKind ty1
         tk2 = typeKind ty2
   , tk1 `eqType` tk2
-  = Refl Nominal tk1
+  = Refl tk1
   | otherwise
   = KindCo co
 
 mkSubCo :: Coercion -> Coercion
 -- Input coercion is Nominal, result is Representational
 -- see also Note [Role twiddling functions]
-mkSubCo (Refl Nominal ty) = Refl Representational ty
+mkSubCo (Refl ty) = GRefl Representational ty MRefl
+mkSubCo (GRefl Nominal ty co) = GRefl Representational ty co
 mkSubCo (TyConAppCo Nominal tc cos)
   = TyConAppCo Representational tc (applyRoles tc cos)
 mkSubCo (FunCo Nominal arg res)
@@ -1088,9 +1151,10 @@ mkProofIrrelCo :: Role       -- ^ role of the created coercion, "r"
 
 -- if the two coercion prove the same fact, I just don't care what
 -- the individual coercions are.
-mkProofIrrelCo r (Refl {}) g  _  = Refl r (CoercionTy g)
-mkProofIrrelCo r kco       g1 g2 = mkUnivCo (ProofIrrelProv kco) r
-                                     (mkCoercionTy g1) (mkCoercionTy g2)
+mkProofIrrelCo r co g  _ | isGReflCo co  = mkReflCo r (mkCoercionTy g)
+  -- kco is a kind coercion, thus @isGReflCo@ rather than @isReflCo@
+mkProofIrrelCo r kco        g1 g2 = mkUnivCo (ProofIrrelProv kco) r
+                                             (mkCoercionTy g1) (mkCoercionTy g2)
 
 {-
 %************************************************************************
@@ -1109,7 +1173,8 @@ setNominalRole_maybe r co
   | otherwise = setNominalRole_maybe_helper co
   where
     setNominalRole_maybe_helper (SubCo co)  = Just co
-    setNominalRole_maybe_helper (Refl _ ty) = Just $ Refl Nominal ty
+    setNominalRole_maybe_helper co@(Refl _) = Just co
+    setNominalRole_maybe_helper (GRefl _ ty co) = Just $ GRefl Nominal ty co
     setNominalRole_maybe_helper (TyConAppCo Representational tc cos)
       = do { cos' <- zipWithM setNominalRole_maybe (tyConRolesX Representational tc) cos
            ; return $ TyConAppCo Nominal tc cos' }
@@ -1132,8 +1197,6 @@ setNominalRole_maybe r co
       = NthCo Nominal n <$> setNominalRole_maybe (coercionRole co) co
     setNominalRole_maybe_helper (InstCo co arg)
       = InstCo <$> setNominalRole_maybe_helper co <*> pure arg
-    setNominalRole_maybe_helper (CoherenceCo co1 co2)
-      = CoherenceCo <$> setNominalRole_maybe_helper co1 <*> pure co2
     setNominalRole_maybe_helper (UnivCo prov _ co1 co2)
       | case prov of UnsafeCoerceProv -> True   -- it's always unsafe
                      PhantomProv _    -> False  -- should always be phantom
@@ -1200,8 +1263,13 @@ promoteCoercion co = case co of
      --    The ASSERT( False )s throughout
      -- are these cases explicitly, but they should never fire.
 
-    Refl _ ty -> ASSERT( False )
-                 mkNomReflCo (typeKind ty)
+    Refl _ -> ASSERT( False )
+              mkNomReflCo ki1
+
+    GRefl _ _ MRefl -> ASSERT( False )
+                       mkNomReflCo ki1
+
+    GRefl _ _ (MCo co) -> co
 
     TyConAppCo _ tc args
       | Just co' <- instCoercions (mkNomReflCo (tyConKind tc)) args
@@ -1262,9 +1330,6 @@ promoteCoercion co = case co of
     InstCo g _
       -> promoteCoercion g
 
-    CoherenceCo g h
-      -> mkSymCo h `mkTransCo` promoteCoercion g
-
     KindCo _
       -> ASSERT( False )
          mkNomReflCo liftedTypeKind
@@ -1308,11 +1373,24 @@ instCoercions g ws
            ; return (piResultTy <$> g_tys <*> w_tys, g') }
 
 -- | Creates a new coercion with both of its types casted by different casts
--- castCoercionKind g h1 h2, where g :: t1 ~ t2, has type (t1 |> h1) ~ (t2 |> h2)
--- The second and third coercions must be nominal.
-castCoercionKind :: Coercion -> Coercion -> Coercion -> Coercion
-castCoercionKind g h1 h2
-  = g `mkCoherenceLeftCo` h1 `mkCoherenceRightCo` h2
+-- @castCoercionKind g r t1 t2 h1 h2@, where @g :: t1 ~r t2@,
+-- has type @(t1 |> h1) ~r (t2 |> h2)@.
+-- @h1@ and @h2@ must be nominal.
+castCoercionKind :: Coercion -> Role -> Type -> Type
+                 -> CoercionN -> CoercionN -> Coercion
+castCoercionKind g r t1 t2 h1 h2
+  = mkCoherenceRightCo r t2 h2 (mkCoherenceLeftCo r t1 h1 g)
+
+-- | Creates a new coercion with both of its types casted by different casts
+-- @castCoercionKind g h1 h2@, where @g :: t1 ~r t2@,
+-- has type @(t1 |> h1) ~r (t2 |> h2)@.
+-- @h1@ and @h2@ must be nominal.
+-- It calls @coercionKindRole@, so it's quite inefficient (which 'I' stands for)
+-- Use @castCoercionKind@ instead if @t1@, @t2@, and @r@ are known beforehand.
+castCoercionKindI :: Coercion -> CoercionN -> CoercionN -> Coercion
+castCoercionKindI g h1 h2
+  = mkCoherenceRightCo r t2 h2 (mkCoherenceLeftCo r t1 h1 g)
+  where (Pair t1 t2, r) = coercionKindRole g
 
 -- See note [Newtype coercions] in TyCon
 
@@ -1499,8 +1577,8 @@ eqCoercionX env = eqTypeX env `on` coercionType
 Note [Lifting coercions over types: liftCoSubst]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 The KPUSH rule deals with this situation
-   data T a = MkK (a -> Maybe a)
-   g :: T t1 ~ K t2
+   data T a = K (a -> Maybe a)
+   g :: T t1 ~ T t2
    x :: t1 -> Maybe t1
 
    case (K @t1 x) |> g of
@@ -1563,7 +1641,7 @@ liftCoSubstWith r tvs cos ty
 -- types of the mapped coercions in @lc@, and similar for @lc_right@.
 liftCoSubst :: HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion
 liftCoSubst r lc@(LC subst env) ty
-  | isEmptyVarEnv env = Refl r (substTy subst ty)
+  | isEmptyVarEnv env = mkReflCo r (substTy subst ty)
   | otherwise         = ty_co_subst lc r ty
 
 emptyLiftingContext :: InScopeSet -> LiftingContext
@@ -1583,8 +1661,10 @@ extendLiftingContext :: LiftingContext  -- ^ original LC
                      -> Coercion        -- ^ ...to this lifted version
                      -> LiftingContext
     -- mappings to reflexive coercions are just substitutions
-extendLiftingContext (LC subst env) tv (Refl _ ty) = LC (extendTvSubst subst tv ty) env
 extendLiftingContext (LC subst env) tv arg
+  | Just (ty, _) <- isReflCo_maybe arg
+  = LC (extendTvSubst subst tv ty) env
+  | otherwise
   = ASSERT( isTyVar tv )
     LC subst (extendVarEnv env tv arg)
 
@@ -1611,9 +1691,10 @@ extendLiftingContextEx lc@(LC subst env) ((v,ty):rest)
 -- works with existentially bound variables, which are considered to have
 -- nominal roles.
   = let lc' = LC (subst `extendTCvInScopeSet` tyCoVarsOfType ty)
-                 (extendVarEnv env v (mkSymCo $ mkCoherenceCo
-                                         (mkNomReflCo ty)
-                                         (ty_co_subst lc Nominal (tyVarKind v))))
+                 (extendVarEnv env v $
+                  mkGReflRightCo Nominal
+                                 ty
+                                 (ty_co_subst lc Nominal (tyVarKind v)))
     in extendLiftingContextEx lc' rest
 
 -- | Erase the environments in a lifting context
@@ -1651,9 +1732,9 @@ ty_co_subst lc role ty
                            = let (lc', v', h) = liftCoSubstVarBndr lc v in
                              mkForAllCo v' h $! ty_co_subst lc' r ty
     go r ty@(LitTy {})     = ASSERT( r == Nominal )
-                             mkReflCo r ty
-    go r (CastTy ty co)    = castCoercionKind (go r ty) (substLeftCo lc co)
-                                                        (substRightCo lc co)
+                             mkNomReflCo ty
+    go r (CastTy ty co)    = castCoercionKindI (go r ty) (substLeftCo lc co)
+                                                         (substRightCo lc co)
     go r (CoercionTy co)   = mkProofIrrelCo r kco (substLeftCo lc co)
                                                   (substRightCo lc co)
       where kco = go Nominal (coercionType co)
@@ -1682,7 +1763,7 @@ liftCoSubstTyVar (LC subst env) r v
   = downgradeRole_maybe r (coercionRole co_arg) co_arg
 
   | otherwise
-  = Just $ Refl r (substTyVar subst v)
+  = Just $ mkReflCo r (substTyVar subst v)
 
 liftCoSubstVarBndr :: LiftingContext -> TyVar
                    -> (LiftingContext, TyVar, Coercion)
@@ -1705,7 +1786,7 @@ liftCoSubstVarBndrUsing fun lc@(LC subst cenv) old_var
     Pair k1 _    = coercionKind eta
     new_var      = uniqAway (getTCvInScope subst) (setVarType old_var k1)
 
-    lifted   = Refl Nominal (TyVarTy new_var)
+    lifted   = Refl (TyVarTy new_var)
     new_cenv = extendVarEnv cenv old_var lifted
 
 -- | Is a var in the domain of a lifting context?
@@ -1776,8 +1857,13 @@ lcInScopeSet (LC subst _) = getTCvInScope subst
 %************************************************************************
 -}
 
+seqMCo :: MCoercion -> ()
+seqMCo MRefl    = ()
+seqMCo (MCo co) = seqCo co
+
 seqCo :: Coercion -> ()
-seqCo (Refl r ty)               = r `seq` seqType ty
+seqCo (Refl ty)                 = seqType ty
+seqCo (GRefl r ty mco)          = r `seq` seqType ty `seq` seqMCo mco
 seqCo (TyConAppCo r tc cos)     = r `seq` tc `seq` seqCos cos
 seqCo (AppCo co1 co2)           = seqCo co1 `seq` seqCo co2
 seqCo (ForAllCo tv k co)        = seqType (tyVarKind tv) `seq` seqCo k
@@ -1793,7 +1879,6 @@ seqCo (TransCo co1 co2)         = seqCo co1 `seq` seqCo co2
 seqCo (NthCo r n co)            = r `seq` n `seq` seqCo co
 seqCo (LRCo lr co)              = lr `seq` seqCo co
 seqCo (InstCo co arg)           = seqCo co `seq` seqCo arg
-seqCo (CoherenceCo co1 co2)     = seqCo co1 `seq` seqCo co2
 seqCo (KindCo co)               = seqCo co
 seqCo (SubCo co)                = seqCo co
 seqCo (AxiomRuleCo _ cs)        = seqCos cs
@@ -1844,11 +1929,14 @@ coercionKind :: Coercion -> Pair Type
 coercionKind co =
   go co
   where
-    go (Refl _ ty)          = Pair ty ty
+    go (Refl ty) = Pair ty ty
+    go (GRefl _ ty MRefl) = Pair ty ty
+    go (GRefl _ ty (MCo co1)) = Pair ty (mkCastTy ty co1)
     go (TyConAppCo _ tc cos)= mkTyConApp tc <$> (sequenceA $ map go cos)
     go (AppCo co1 co2)      = mkAppTy <$> go co1 <*> go co2
     go co@(ForAllCo tv1 k_co co1)
-       | isReflCo k_co            = mkInvForAllTy tv1 <$> go co1
+       | isGReflCo k_co           = mkInvForAllTy tv1 <$> go co1
+         -- kind_co always has kind @Type@, thus @isGReflCo@
        | otherwise                = go_forall empty_subst co
        where
          empty_subst = mkEmptyTCvSubst (mkInScopeSet $ tyCoVarsOfCo co)
@@ -1889,9 +1977,6 @@ coercionKind co =
         tys = go co
     go (LRCo lr co)         = (pickLR lr . splitAppTy) <$> go co
     go (InstCo aco arg)     = go_app aco [arg]
-    go (CoherenceCo g h)
-      = let Pair ty1 ty2 = go g in
-        Pair (mkCastTy ty1 h) ty2
     go (KindCo co)          = typeKind <$> go co
     go (SubCo co)           = go co
     go (AxiomRuleCo ax cos) = expectJust "coercionKind" $
@@ -1909,9 +1994,10 @@ coercionKind co =
       where
         Pair _ k2 = go k_co
         tv2       = setTyVarKind tv1 (substTy subst k2)
-        subst' | isReflCo k_co = extendTCvInScope subst tv1
-               | otherwise     = extendTvSubst (extendTCvInScope subst tv2) tv1 $
-                                 TyVarTy tv2 `mkCastTy` mkSymCo k_co
+        subst' | isGReflCo k_co = extendTCvInScope subst tv1
+                 -- kind_co always has kind @Type@, thus @isGReflCo@
+               | otherwise      = extendTvSubst (extendTCvInScope subst tv2) tv1 $
+                                  TyVarTy tv2 `mkCastTy` mkSymCo k_co
     go_forall subst other_co
       = substTy subst `pLiftSnd` go other_co
 
@@ -1945,7 +2031,8 @@ coercionKindRole co = (coercionKind co, coercionRole co)
 coercionRole :: Coercion -> Role
 coercionRole = go
   where
-    go (Refl r _) = r
+    go (Refl _) = Nominal
+    go (GRefl r _ _) = r
     go (TyConAppCo r _ _) = r
     go (AppCo co1 _) = go co1
     go (ForAllCo _ _ co) = go co
@@ -1959,7 +2046,6 @@ coercionRole = go
     go (NthCo r _d _co) = r
     go (LRCo {}) = Nominal
     go (InstCo co _) = go co
-    go (CoherenceCo co1 _) = go co1
     go (KindCo {}) = Nominal
     go (SubCo _) = Representational
     go (AxiomRuleCo ax _) = coaxrRole ax
@@ -1992,10 +2078,14 @@ buildCoercion orig_ty1 orig_ty2 = go orig_ty1 orig_ty2
                | Just ty2' <- coreView ty2 = go ty1 ty2'
 
     go (CastTy ty1 co) ty2
-      = go ty1 ty2 `mkCoherenceLeftCo` co
+      = let co' = go ty1 ty2
+            r = coercionRole co'
+        in  mkCoherenceLeftCo r ty1 co co'
 
     go ty1 (CastTy ty2 co)
-      = go ty1 ty2 `mkCoherenceRightCo` co
+      = let co' = go ty1 ty2
+            r = coercionRole co'
+        in  mkCoherenceRightCo r ty2 co co'
 
     go ty1@(TyVarTy tv1) _tyvarty
       = ASSERT( case _tyvarty of
diff --git a/compiler/types/Coercion.hs-boot b/compiler/types/Coercion.hs-boot
index df4a24e5b2..6e6acd752a 100644
--- a/compiler/types/Coercion.hs-boot
+++ b/compiler/types/Coercion.hs-boot
@@ -28,12 +28,14 @@ mkTransCo :: Coercion -> Coercion -> Coercion
 mkNthCo :: HasDebugCallStack => Role -> Int -> Coercion -> Coercion
 mkLRCo :: LeftOrRight -> Coercion -> Coercion
 mkInstCo :: Coercion -> Coercion -> Coercion
-mkCoherenceCo :: Coercion -> Coercion -> Coercion
+mkGReflCo :: Role -> Type -> MCoercionN -> Coercion
+mkNomReflCo :: Type -> Coercion
 mkKindCo :: Coercion -> Coercion
 mkSubCo :: Coercion -> Coercion
 mkProofIrrelCo :: Role -> Coercion -> Coercion -> Coercion -> Coercion
 mkAxiomRuleCo :: CoAxiomRule -> [Coercion] -> Coercion
 
+isGReflCo :: Coercion -> Bool
 isReflCo :: Coercion -> Bool
 isReflexiveCo :: Coercion -> Bool
 decomposePiCos :: Kind -> [Type] -> Coercion -> ([Coercion], Coercion)
diff --git a/compiler/types/FamInstEnv.hs b/compiler/types/FamInstEnv.hs
index 306e1b1034..046edfaa42 100644
--- a/compiler/types/FamInstEnv.hs
+++ b/compiler/types/FamInstEnv.hs
@@ -1341,15 +1341,15 @@ 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
+               -> NormM (Coercion, Type)   -- (coercion, new type), where
+                                           -- co :: old-type ~ new_type
 -- 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
 -- Does nothing to newtypes
 -- The returned coercion *must* be *homogeneous*
 -- See Note [Normalising types]
--- Try to not to disturb type synonyms if possible
+-- Try not to disturb type synonyms if possible
 
 normalise_type ty
   = go ty
@@ -1376,7 +1376,8 @@ normalise_type ty
       = do { (nco, nty) <- go ty
            ; lc <- getLC
            ; let co' = substRightCo lc co
-           ; return (castCoercionKind nco co co', mkCastTy nty co') }
+           ; return (castCoercionKind nco Nominal ty nty co co'
+                    , mkCastTy nty co') }
     go (CoercionTy co)
       = do { lc <- getLC
            ; r <- getRole
@@ -1623,7 +1624,11 @@ allTyVarsInTy = go
     go (CastTy ty co)    = go ty `unionVarSet` go_co co
     go (CoercionTy co)   = go_co co
 
-    go_co (Refl _ ty)           = go ty
+    go_mco MRefl    = emptyVarSet
+    go_mco (MCo co) = go_co co
+
+    go_co (Refl ty)             = go ty
+    go_co (GRefl _ ty mco)      = go ty `unionVarSet` go_mco mco
     go_co (TyConAppCo _ _ args) = go_cos args
     go_co (AppCo co arg)        = go_co co `unionVarSet` go_co arg
     go_co (ForAllCo tv h co)
@@ -1638,7 +1643,6 @@ allTyVarsInTy = go
     go_co (NthCo _ _ co)        = go_co co
     go_co (LRCo _ co)           = go_co co
     go_co (InstCo co arg)       = go_co co `unionVarSet` go_co arg
-    go_co (CoherenceCo c1 c2)   = go_co c1 `unionVarSet` go_co c2
     go_co (KindCo co)           = go_co co
     go_co (SubCo co)            = go_co co
     go_co (AxiomRuleCo _ cs)    = go_cos cs
diff --git a/compiler/types/OptCoercion.hs b/compiler/types/OptCoercion.hs
index db4bc8c668..70ae469795 100644
--- a/compiler/types/OptCoercion.hs
+++ b/compiler/types/OptCoercion.hs
@@ -74,7 +74,7 @@ We thus want some coercion proving this:
   (t1[tv |-> s1]) ~ (t2[tv |-> s2 |> sym h])
 
 If we substitute the *type* tv for the *coercion*
-(g2 `mkCoherenceRightCo` sym h) in g, we'll get this result exactly.
+(g2 ; t2 ~ t2 |> sym h) in g, we'll get this result exactly.
 This is bizarre,
 though, because we're substituting a type variable with a coercion. However,
 this operation already exists: it's called *lifting*, and defined in Coercion.
@@ -170,12 +170,30 @@ opt_co4_wrap env sym rep r co
     result
 -}
 
-opt_co4 env _   rep r (Refl _r ty)
+opt_co4 env _   rep r (Refl ty)
+  = ASSERT2( r == Nominal, text "Expected role:" <+> ppr r    $$
+                           text "Found role:" <+> ppr Nominal $$
+                           text "Type:" <+> ppr ty )
+    liftCoSubst (chooseRole rep r) env ty
+
+opt_co4 env _   rep r (GRefl _r ty MRefl)
   = ASSERT2( r == _r, text "Expected role:" <+> ppr r $$
                       text "Found role:" <+> ppr _r   $$
                       text "Type:" <+> ppr ty )
     liftCoSubst (chooseRole rep r) env ty
 
+opt_co4 env sym  rep r (GRefl _r ty (MCo co))
+  = ASSERT2( r == _r, text "Expected role:" <+> ppr r $$
+                      text "Found role:" <+> ppr _r   $$
+                      text "Type:" <+> ppr ty )
+    if isGReflCo co || isGReflCo co'
+    then liftCoSubst r' env ty
+    else wrapSym sym $ mkCoherenceRightCo r' ty' co' (liftCoSubst r' env ty)
+  where
+    r'  = chooseRole rep r
+    ty' = substTy (lcSubstLeft env) ty
+    co' = opt_co4 env False False Nominal co
+
 opt_co4 env sym rep r (SymCo co)  = opt_co4_wrap env (not sym) rep r co
   -- surprisingly, we don't have to do anything to the env here. This is
   -- because any "lifting" substitutions in the env are tied to ForAllCos,
@@ -225,7 +243,7 @@ opt_co4 env sym rep r (CoVarCo cv)
   = opt_co4_wrap (zapLiftingContext env) sym rep r co
 
   | ty1 `eqType` ty2   -- See Note [Optimise CoVarCo to Refl]
-  = Refl (chooseRole rep r) ty1
+  = mkReflCo (chooseRole rep r) ty1
 
   | otherwise
   = ASSERT( isCoVar cv1 )
@@ -273,11 +291,13 @@ opt_co4 env sym rep r (TransCo co1 co2)
     co2' = opt_co4_wrap env sym rep r co2
     in_scope = lcInScopeSet env
 
-opt_co4 env _sym rep r (NthCo _r n (Refl _r2 ty))
-  | Just (_tc, args) <- ASSERT( r == _r )
+opt_co4 env _sym rep r (NthCo _r n co)
+  | Just (ty, _) <- isReflCo_maybe co
+  , Just (_tc, args) <- ASSERT( r == _r )
                         splitTyConApp_maybe ty
   = liftCoSubst (chooseRole rep r) env (args `getNth` n)
-  | n == 0
+  | Just (ty, _) <- isReflCo_maybe co
+  , n == 0
   , Just (tv, _) <- splitForAllTy_maybe ty
   = liftCoSubst (chooseRole rep r) env (tyVarKind tv)
 
@@ -330,7 +350,7 @@ opt_co4 env sym rep r (InstCo co1 arg)
     -- forall over type...
   | Just (tv, kind_co, co_body) <- splitForAllCo_maybe co1
   = opt_co4_wrap (extendLiftingContext env tv
-                    (arg' `mkCoherenceRightCo` mkSymCo kind_co))
+                    (mkCoherenceRightCo Nominal t2 (mkSymCo kind_co) arg'))
                  sym rep r co_body
 
     -- See if it is a forall after optimization
@@ -339,7 +359,7 @@ opt_co4 env sym rep r (InstCo co1 arg)
     -- forall over type...
   | Just (tv', kind_co', co_body') <- splitForAllCo_maybe co1'
   = opt_co4_wrap (extendLiftingContext (zapLiftingContext env) tv'
-                    (arg' `mkCoherenceRightCo` mkSymCo kind_co'))
+                    (mkCoherenceRightCo Nominal t2 (mkSymCo kind_co') arg'))
             False False r' co_body'
 
   | otherwise = InstCo co1' arg'
@@ -347,22 +367,7 @@ opt_co4 env sym rep r (InstCo co1 arg)
     co1' = opt_co4_wrap env sym rep r co1
     r'   = chooseRole rep r
     arg' = opt_co4_wrap env sym False Nominal arg
-
-opt_co4 env sym rep r (CoherenceCo co1 co2)
-  | TransCo col1 cor1 <- co1
-  = opt_co4_wrap env sym rep r (mkTransCo (mkCoherenceCo col1 co2) cor1)
-
-  | TransCo col1' cor1' <- co1'
-  = if sym then opt_trans in_scope col1'
-                  (optCoercion' (zapTCvSubst (lcTCvSubst env))
-                               (mkCoherenceRightCo cor1' co2'))
-           else opt_trans in_scope (mkCoherenceCo col1' co2') cor1'
-
-  | otherwise
-  = wrapSym sym $ mkCoherenceCo (opt_co4_wrap env False rep r co1) co2'
-  where co1' = opt_co4_wrap env sym   rep   r       co1
-        co2' = opt_co4_wrap env False False Nominal co2
-        in_scope = lcInScopeSet env
+    Pair _ t2 = coercionKind arg'
 
 opt_co4 env sym _rep r (KindCo co)
   = ASSERT( r == Nominal )
@@ -476,12 +481,14 @@ opt_transList is = zipWith (opt_trans is)
 opt_trans :: InScopeSet -> NormalCo -> NormalCo -> NormalCo
 opt_trans is co1 co2
   | isReflCo co1 = co2
+    -- optimize when co1 is a Refl Co
   | otherwise    = opt_trans1 is co1 co2
 
 opt_trans1 :: InScopeSet -> NormalNonIdCo -> NormalCo -> NormalCo
 -- First arg is not the identity
 opt_trans1 is co1 co2
   | isReflCo co2 = co1
+    -- optimize when co2 is a Refl Co
   | otherwise    = opt_trans2 is co1 co2
 
 opt_trans2 :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> NormalCo
@@ -507,6 +514,11 @@ opt_trans2 _ co1 co2
 -- Optimize coercions with a top-level use of transitivity.
 opt_trans_rule :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> Maybe NormalCo
 
+opt_trans_rule is in_co1@(GRefl r1 t1 (MCo co1)) in_co2@(GRefl r2 _ (MCo co2))
+  = ASSERT( r1 == r2 )
+    fireTransRule "GRefl" in_co1 in_co2 $
+    mkGReflRightCo r1 t1 (opt_trans is co1 co2)
+
 -- Push transitivity through matching destructors
 opt_trans_rule is in_co1@(NthCo r1 d1 co1) in_co2@(NthCo r2 d2 co2)
   | d1 == d2
@@ -659,18 +671,12 @@ opt_trans_rule is co1 co2
     co2_is_axiom_maybe = isAxiom_maybe co2
     role = coercionRole co1 -- should be the same as coercionRole co2!
 
-opt_trans_rule is co1 co2
-  | Just (lco, lh) <- isCohRight_maybe co1
-  , Just (rco, rh) <- isCohLeft_maybe co2
-  , (coercionType lh) `eqType` (coercionType rh)
-  = opt_trans_rule is lco rco
-
 opt_trans_rule _ co1 co2        -- Identity rule
   | (Pair ty1 _, r) <- coercionKindRole co1
   , Pair _ ty2 <- coercionKind co2
   , ty1 `eqType` ty2
   = fireTransRule "RedTypeDirRefl" co1 co2 $
-    Refl r ty2
+    mkReflCo r ty2
 
 opt_trans_rule _ _ _ = Nothing
 
@@ -696,19 +702,21 @@ opt_trans_rule_app is orig_co1 orig_co2 co1a co1bs co2a co2bs
   = ASSERT( co1bs `equalLength` co2bs )
     fireTransRule ("EtaApps:" ++ show (length co1bs)) orig_co1 orig_co2 $
     let Pair _ rt1a = coercionKind co1a
-        Pair lt2a _ = coercionKind co2a
+        (Pair lt2a _, rt2a) = coercionKindRole co2a
 
         Pair _ rt1bs = traverse coercionKind co1bs
         Pair lt2bs _ = traverse coercionKind co2bs
+        rt2bs = map coercionRole co2bs
 
         kcoa = mkKindCo $ buildCoercion lt2a rt1a
         kcobs = map mkKindCo $ zipWith buildCoercion lt2bs rt1bs
 
-        co2a' = mkCoherenceLeftCo co2a kcoa
-        co2bs' = zipWith mkCoherenceLeftCo co2bs kcobs
+        co2a'   = mkCoherenceLeftCo rt2a lt2a kcoa co2a
+        co2bs'  = zipWith3 mkGReflLeftCo rt2bs lt2bs kcobs
+        co2bs'' = zipWith mkTransCo co2bs' co2bs
     in
     mkAppCos (opt_trans is co1a co2a')
-             (zipWith (opt_trans is) co1bs co2bs')
+             (zipWith (opt_trans is) co1bs co2bs'')
 
 fireTransRule :: String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
 fireTransRule _rule _co1 _co2 res
@@ -820,8 +828,7 @@ This can be done with mkKindCo and buildCoercion. The latter assumes two
 types are identical modulo casts and builds a coercion between them.
 
 Then, we build (co1a ; co2a |> sym ak) and (co1b ; co2b |> sym bk) as the
-output coercions. These are well-kinded. (We cast the right-hand coercion
-because mkCoherenceLeftCo is smaller than mkCoherenceRightCo.)
+output coercions. These are well-kinded.
 
 Also, note that all of this is done after accumulated any nested AppCo
 parameters. This step is to avoid quadratic behavior in calling coercionKind.
@@ -910,18 +917,6 @@ matchAxiom sym ax@(CoAxiom { co_ax_tc = tc }) ind co
   = Nothing
 
 -------------
--- destruct a CoherenceCo
-isCohLeft_maybe :: Coercion -> Maybe (Coercion, Coercion)
-isCohLeft_maybe (CoherenceCo co1 co2) = Just (co1, co2)
-isCohLeft_maybe _                     = Nothing
-
--- destruct a (sym (co1 |> co2)).
--- if isCohRight_maybe co = Just (co1, co2), then (sym co1) `mkCohRightCo` co2 = co
-isCohRight_maybe :: Coercion -> Maybe (Coercion, Coercion)
-isCohRight_maybe (SymCo (CoherenceCo co1 co2)) = Just (mkSymCo co1, co2)
-isCohRight_maybe _                             = Nothing
-
--------------
 compatible_co :: Coercion -> Coercion -> Bool
 -- Check whether (co1 . co2) will be well-kinded
 compatible_co co1 co2
@@ -940,15 +935,15 @@ Suppose we have
 
 but g is *not* a ForAllCo. We want to eta-expand it. So, we do this:
 
-  g' = all a1:(ForAllKindCo g).(InstCo g (a1 `mkCoherenceRightCo` ForAllKindCo g))
+  g' = all a1:(ForAllKindCo g).(InstCo g (a1 ~ a1 |> ForAllKindCo g))
 
 Call the kind coercion h1 and the body coercion h2. We can see that
 
-  h2 : t1 ~ t2[a2 |-> (a1 |> h2)]
+  h2 : t1 ~ t2[a2 |-> (a1 |> h1)]
 
 According to the typing rule for ForAllCo, we get that
 
-  g' : all a1:k1.t1  ~  all a1:k2.(t2[a2 |-> (a1 |> h2)][a1 |-> a1 |> sym h2])
+  g' : all a1:k1.t1  ~  all a1:k2.(t2[a2 |-> (a1 |> h1)][a1 |-> a1 |> sym h1])
 
 or
 
@@ -967,7 +962,7 @@ etaForAllCo_maybe co
   , isForAllTy ty2
   , let kind_co = mkNthCo Nominal 0 co
   = Just ( tv1, kind_co
-         , mkInstCo co (mkNomReflCo (TyVarTy tv1) `mkCoherenceRightCo` kind_co) )
+         , mkInstCo co (mkGReflRightCo Nominal (TyVarTy tv1) kind_co))
 
   | otherwise
   = Nothing
diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs
index 0ec5888cef..6427917fe5 100644
--- a/compiler/types/TyCoRep.hs
+++ b/compiler/types/TyCoRep.hs
@@ -34,7 +34,7 @@ module TyCoRep (
         UnivCoProvenance(..),
         CoercionHole(..), coHoleCoVar, setCoHoleCoVar,
         CoercionN, CoercionR, CoercionP, KindCoercion,
-        MCoercion(..), MCoercionR,
+        MCoercion(..), MCoercionR, MCoercionN,
 
         -- * Functions over types
         mkTyConTy, mkTyVarTy, mkTyVarTys,
@@ -861,8 +861,8 @@ data Coercion
   --    -   _ stands for a parameter that is not a Role or Coercion.
 
   -- These ones mirror the shape of types
-  = -- Refl :: "e" -> _ -> e
-    Refl Role Type  -- See Note [Refl invariant]
+  = -- Refl :: _ -> N
+    Refl Type  -- See Note [Refl invariant]
           -- Invariant: applications of (Refl T) to a bunch of identity coercions
           --            always show up as Refl.
           -- For example  (Refl T) (Refl a) (Refl b) shows up as (Refl (T a b)).
@@ -873,7 +873,13 @@ data Coercion
           -- ConAppCo coercions (like all coercions other than Refl)
           -- are NEVER the identity.
 
-          -- Use (Refl Representational _), not (SubCo (Refl Nominal _))
+          -- Use (GRefl Representational ty MRefl), not (SubCo (Refl ty))
+
+  -- GRefl :: "e" -> _ -> Maybe N -> e
+  -- See Note [Generalized reflexive coercion]
+  | GRefl Role Type MCoercionN  -- See Note [Refl invariant]
+          -- Use (Refl ty), not (GRefl Nominal ty MRefl)
+          -- Use (GRefl Representational _ _), not (SubCo (GRefl Nominal _ _))
 
   -- These ones simply lift the correspondingly-named
   -- Type constructors into Coercions
@@ -933,11 +939,6 @@ data Coercion
     -- :: e -> N -> e
     -- See Note [InstCo roles]
 
-  -- Coherence applies a coercion to the left-hand type of another coercion
-  -- See Note [Coherence]
-  | CoherenceCo Coercion KindCoercion
-     -- :: e -> N -> e
-
   -- Extract a kind coercion from a (heterogeneous) type coercion
   -- NB: all kind coercions are Nominal
   | KindCo Coercion
@@ -962,7 +963,9 @@ data MCoercion
     -- A trivial Reflexivity coercion
   | MCo Coercion
     -- Other coercions
+  deriving Data.Data
 type MCoercionR = MCoercion
+type MCoercionN = MCoercion
 
 instance Outputable MCoercion where
   ppr MRefl    = text "MRefl"
@@ -974,7 +977,7 @@ Note [Refl invariant]
 Invariant 1:
 
 Coercions have the following invariant
-     Refl is always lifted as far as possible.
+     Refl (similar for GRefl r ty MRefl) is always lifted as far as possible.
 
 You might think that a consequencs is:
      Every identity coercions has Refl at the root
@@ -985,6 +988,42 @@ But that's not quite true because of coercion variables.  Consider
 etc.  So the consequence is only true of coercions that
 have no coercion variables.
 
+Note [Generalized reflexive coercion]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+GRefl is a generalized reflexive coercion (see Trac #15192). It wraps a kind
+coercion, which might be reflexive (MRefl) or any coercion (MCo co). The typing
+rules for GRefl:
+
+  ty : k1
+  ------------------------------------
+  GRefl r ty MRefl: ty ~r ty
+
+  ty : k1       co :: k1 ~ k2
+  ------------------------------------
+  GRefl r ty (MCo co) : ty ~r ty |> co
+
+Consider we have
+
+   g1 :: s ~r t
+   s  :: k1
+   g2 :: k1 ~ k2
+
+and we want to construct a coercions co which has type
+
+   (s |> g2) ~r t
+
+We can define
+
+   co = Sym (GRefl r s g2) ; g1
+
+It is easy to see that
+
+   Refl == GRefl Nominal ty MRefl :: ty ~n ty
+
+A nominal reflexive coercion is quite common, so we keep the special form Refl to
+save allocation.
+
 Note [Coercion axioms applied to coercions]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 The reason coercion axioms can be applied to coercions and not just
@@ -1076,19 +1115,6 @@ add Names to, e.g., VarSets, and there generally is just an impedance mismatch
 in a bunch of places. So we use tv1. When we need tv2, we can use
 setTyVarKind.
 
-Note [Coherence]
-~~~~~~~~~~~~~~~~
-The Coherence typing rule is thus:
-
-  g1 : s ~ t    s : k1    g2 : k1 ~ k2
-  ------------------------------------
-  CoherenceCo g1 g2 : (s |> g2) ~ t
-
-While this looks (and is) unsymmetric, a combination of other coercion
-combinators can make the symmetric version.
-
-For role information, see Note [Roles and kind coercions].
-
 Note [Predicate coercions]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 Suppose we have
@@ -1600,10 +1626,17 @@ tyCoVarsOfCoList :: Coercion -> [TyCoVar]
 -- See Note [Free variables of types]
 tyCoVarsOfCoList co = fvVarList $ tyCoFVsOfCo co
 
+tyCoFVsOfMCo :: MCoercion -> FV
+tyCoFVsOfMCo MRefl    = emptyFV
+tyCoFVsOfMCo (MCo co) = tyCoFVsOfCo co
+
 tyCoFVsOfCo :: Coercion -> FV
 -- Extracts type and coercion variables from a coercion
 -- See Note [Free variables of types]
-tyCoFVsOfCo (Refl _ ty)         fv_cand in_scope acc = tyCoFVsOfType ty fv_cand in_scope acc
+tyCoFVsOfCo (Refl ty) fv_cand in_scope acc
+  = tyCoFVsOfType ty fv_cand in_scope acc
+tyCoFVsOfCo (GRefl _ ty mco) fv_cand in_scope acc
+  = (tyCoFVsOfType ty `unionFV` tyCoFVsOfMCo mco) fv_cand in_scope acc
 tyCoFVsOfCo (TyConAppCo _ _ cos) fv_cand in_scope acc = tyCoFVsOfCos cos fv_cand in_scope acc
 tyCoFVsOfCo (AppCo co arg) fv_cand in_scope acc
   = (tyCoFVsOfCo co `unionFV` tyCoFVsOfCo arg) fv_cand in_scope acc
@@ -1625,7 +1658,6 @@ tyCoFVsOfCo (TransCo co1 co2)   fv_cand in_scope acc = (tyCoFVsOfCo co1 `unionFV
 tyCoFVsOfCo (NthCo _ _ co)      fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
 tyCoFVsOfCo (LRCo _ co)         fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
 tyCoFVsOfCo (InstCo co arg)     fv_cand in_scope acc = (tyCoFVsOfCo co `unionFV` tyCoFVsOfCo arg) fv_cand in_scope acc
-tyCoFVsOfCo (CoherenceCo c1 c2) fv_cand in_scope acc = (tyCoFVsOfCo c1 `unionFV` tyCoFVsOfCo c2) fv_cand in_scope acc
 tyCoFVsOfCo (KindCo co)         fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
 tyCoFVsOfCo (SubCo co)          fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
 tyCoFVsOfCo (AxiomRuleCo _ cs)  fv_cand in_scope acc = tyCoFVsOfCos cs fv_cand in_scope acc
@@ -1670,9 +1702,14 @@ coVarsOfType (CoercionTy co)     = coVarsOfCo co
 coVarsOfTypes :: [Type] -> TyCoVarSet
 coVarsOfTypes tys = mapUnionVarSet coVarsOfType tys
 
+coVarsOfMCo :: MCoercion -> CoVarSet
+coVarsOfMCo MRefl    = emptyVarSet
+coVarsOfMCo (MCo co) = coVarsOfCo co
+
 coVarsOfCo :: Coercion -> CoVarSet
 -- Extract *coercion* variables only.  Tiresome to repeat the code, but easy.
-coVarsOfCo (Refl _ ty)         = coVarsOfType ty
+coVarsOfCo (Refl ty)             = coVarsOfType ty
+coVarsOfCo (GRefl _ ty co)       = coVarsOfType ty `unionVarSet` coVarsOfMCo co
 coVarsOfCo (TyConAppCo _ _ args) = coVarsOfCos args
 coVarsOfCo (AppCo co arg)      = coVarsOfCo co `unionVarSet` coVarsOfCo arg
 coVarsOfCo (ForAllCo tv kind_co co)
@@ -1688,7 +1725,6 @@ coVarsOfCo (TransCo co1 co2)    = coVarsOfCo co1 `unionVarSet` coVarsOfCo co2
 coVarsOfCo (NthCo _ _ co)       = coVarsOfCo co
 coVarsOfCo (LRCo _ co)          = coVarsOfCo co
 coVarsOfCo (InstCo co arg)      = coVarsOfCo co `unionVarSet` coVarsOfCo arg
-coVarsOfCo (CoherenceCo c1 c2)  = coVarsOfCos [c1, c2]
 coVarsOfCo (KindCo co)          = coVarsOfCo co
 coVarsOfCo (SubCo co)           = coVarsOfCo co
 coVarsOfCo (AxiomRuleCo _ cs)   = coVarsOfCos cs
@@ -1776,10 +1812,15 @@ noFreeVarsOfType (LitTy _)        = True
 noFreeVarsOfType (CastTy ty co)   = noFreeVarsOfType ty && noFreeVarsOfCo co
 noFreeVarsOfType (CoercionTy co)  = noFreeVarsOfCo co
 
+noFreeVarsOfMCo :: MCoercion -> Bool
+noFreeVarsOfMCo MRefl    = True
+noFreeVarsOfMCo (MCo co) = noFreeVarsOfCo co
+
 -- | Returns True if this coercion has no free variables. Should be the same as
 -- isEmptyVarSet . tyCoVarsOfCo, but faster in the non-forall case.
 noFreeVarsOfCo :: Coercion -> Bool
-noFreeVarsOfCo (Refl _ ty)            = noFreeVarsOfType ty
+noFreeVarsOfCo (Refl ty)              = noFreeVarsOfType ty
+noFreeVarsOfCo (GRefl _ ty co)        = noFreeVarsOfType ty && noFreeVarsOfMCo co
 noFreeVarsOfCo (TyConAppCo _ _ args)  = all noFreeVarsOfCo args
 noFreeVarsOfCo (AppCo c1 c2)          = noFreeVarsOfCo c1 && noFreeVarsOfCo c2
 noFreeVarsOfCo co@(ForAllCo {})       = isEmptyVarSet (tyCoVarsOfCo co)
@@ -1795,7 +1836,6 @@ noFreeVarsOfCo (TransCo co1 co2)      = noFreeVarsOfCo co1 && noFreeVarsOfCo co2
 noFreeVarsOfCo (NthCo _ _ co)         = noFreeVarsOfCo co
 noFreeVarsOfCo (LRCo _ co)            = noFreeVarsOfCo co
 noFreeVarsOfCo (InstCo co1 co2)       = noFreeVarsOfCo co1 && noFreeVarsOfCo co2
-noFreeVarsOfCo (CoherenceCo co1 co2)  = noFreeVarsOfCo co1 && noFreeVarsOfCo co2
 noFreeVarsOfCo (KindCo co)            = noFreeVarsOfCo co
 noFreeVarsOfCo (SubCo co)             = noFreeVarsOfCo co
 noFreeVarsOfCo (AxiomRuleCo _ cs)     = all noFreeVarsOfCo cs
@@ -2456,8 +2496,13 @@ subst_co subst co
     go_ty :: Type -> Type
     go_ty = subst_ty subst
 
+    go_mco :: MCoercion -> MCoercion
+    go_mco MRefl    = MRefl
+    go_mco (MCo co) = MCo (go co)
+
     go :: Coercion -> Coercion
-    go (Refl r ty)           = mkReflCo r $! go_ty ty
+    go (Refl ty)             = mkNomReflCo $! (go_ty ty)
+    go (GRefl r ty mco)      = (mkGReflCo r $! (go_ty ty)) $! (go_mco mco)
     go (TyConAppCo r tc args)= let args' = map go args
                                in  args' `seqList` mkTyConAppCo r tc args'
     go (AppCo co arg)        = (mkAppCo $! go co) $! go arg
@@ -2474,7 +2519,6 @@ subst_co subst co
     go (NthCo r d co)        = mkNthCo r d $! (go co)
     go (LRCo lr co)          = mkLRCo lr $! (go co)
     go (InstCo co arg)       = (mkInstCo $! (go co)) $! go arg
-    go (CoherenceCo co1 co2) = (mkCoherenceCo $! (go co1)) $! (go co2)
     go (KindCo co)           = mkKindCo $! (go co)
     go (SubCo co)            = mkSubCo $! (go co)
     go (AxiomRuleCo c cs)    = let cs1 = map go cs
@@ -3057,7 +3101,11 @@ tidyCo :: TidyEnv -> Coercion -> Coercion
 tidyCo env@(_, subst) co
   = go co
   where
-    go (Refl r ty)           = Refl r (tidyType env ty)
+    go_mco MRefl    = MRefl
+    go_mco (MCo co) = MCo (go co)
+
+    go (Refl ty)             = Refl (tidyType env ty)
+    go (GRefl r ty mco)      = GRefl r (tidyType env ty) $! go_mco mco
     go (TyConAppCo r tc cos) = let args = map go cos
                                in args `seqList` TyConAppCo r tc args
     go (AppCo co1 co2)       = (AppCo $! go co1) $! go co2
@@ -3079,7 +3127,6 @@ tidyCo env@(_, subst) co
     go (NthCo r d co)        = NthCo r d $! go co
     go (LRCo lr co)          = LRCo lr $! go co
     go (InstCo co ty)        = (InstCo $! go co) $! go ty
-    go (CoherenceCo co1 co2) = (CoherenceCo $! go co1) $! go co2
     go (KindCo co)           = KindCo $! go co
     go (SubCo co)            = SubCo $! go co
     go (AxiomRuleCo ax cos)  = let cos1 = tidyCos env cos
@@ -3124,7 +3171,9 @@ typeSize (CastTy ty co)             = typeSize ty + coercionSize co
 typeSize (CoercionTy co)            = coercionSize co
 
 coercionSize :: Coercion -> Int
-coercionSize (Refl _ ty)         = typeSize ty
+coercionSize (Refl ty)             = typeSize ty
+coercionSize (GRefl _ ty MRefl)    = typeSize ty
+coercionSize (GRefl _ ty (MCo co)) = 1 + typeSize ty + coercionSize co
 coercionSize (TyConAppCo _ _ args) = 1 + sum (map coercionSize args)
 coercionSize (AppCo co arg)      = coercionSize co + coercionSize arg
 coercionSize (ForAllCo _ h co)   = 1 + coercionSize co + coercionSize h
@@ -3138,7 +3187,6 @@ coercionSize (TransCo co1 co2)   = 1 + coercionSize co1 + coercionSize co2
 coercionSize (NthCo _ _ co)      = 1 + coercionSize co
 coercionSize (LRCo  _ co)        = 1 + coercionSize co
 coercionSize (InstCo co arg)     = 1 + coercionSize co + coercionSize arg
-coercionSize (CoherenceCo c1 c2) = 1 + coercionSize c1 + coercionSize c2
 coercionSize (KindCo co)         = 1 + coercionSize co
 coercionSize (SubCo co)          = 1 + coercionSize co
 coercionSize (AxiomRuleCo _ cs)  = 1 + sum (map coercionSize cs)
diff --git a/compiler/types/TyCoRep.hs-boot b/compiler/types/TyCoRep.hs-boot
index 3753e70b84..9f886dc458 100644
--- a/compiler/types/TyCoRep.hs-boot
+++ b/compiler/types/TyCoRep.hs-boot
@@ -12,10 +12,13 @@ data UnivCoProvenance
 data TCvSubst
 data TyLit
 data TyBinder
+data MCoercion
 
 type PredType = Type
 type Kind = Type
 type ThetaType = [PredType]
+type CoercionN = Coercion
+type MCoercionN = MCoercion
 
 pprKind :: Kind -> SDoc
 pprType :: Type -> SDoc
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index f501930cc7..45b1b74382 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -403,8 +403,13 @@ expandTypeSynonyms ty
     go subst (CastTy ty co)  = mkCastTy (go subst ty) (go_co subst co)
     go subst (CoercionTy co) = mkCoercionTy (go_co subst co)
 
-    go_co subst (Refl r ty)
-      = mkReflCo r (go subst ty)
+    go_mco _     MRefl    = MRefl
+    go_mco subst (MCo co) = MCo (go_co subst co)
+
+    go_co subst (Refl ty)
+      = mkNomReflCo (go subst ty)
+    go_co subst (GRefl r ty mco)
+      = mkGReflCo r (go subst ty) (go_mco subst mco)
        -- NB: coercions are always expanded upon creation
     go_co subst (TyConAppCo r tc args)
       = mkTyConAppCo r tc (map (go_co subst) args)
@@ -431,8 +436,6 @@ expandTypeSynonyms ty
       = mkLRCo lr (go_co subst co)
     go_co subst (InstCo co arg)
       = mkInstCo (go_co subst co) (go_co subst arg)
-    go_co subst (CoherenceCo co1 co2)
-      = mkCoherenceCo (go_co subst co1) (go_co subst co2)
     go_co subst (KindCo co)
       = mkKindCo (go_co subst co)
     go_co subst (SubCo co)
@@ -541,7 +544,11 @@ mapCoercion mapper@(TyCoMapper { tcm_smart = smart, tcm_covar = covar
             env co
   = go co
   where
-    go (Refl r ty) = Refl r <$> mapType mapper env ty
+    go_mco MRefl    = return MRefl
+    go_mco (MCo co) = MCo <$> (go co)
+
+    go (Refl ty) = Refl <$> mapType mapper env ty
+    go (GRefl r ty mco) = mkgreflco r <$> mapType mapper env ty <*> (go_mco mco)
     go (TyConAppCo r tc args)
       = mktyconappco r tc <$> mapM go args
     go (AppCo c1 c2) = mkappco <$> go c1 <*> go c2
@@ -565,7 +572,6 @@ mapCoercion mapper@(TyCoMapper { tcm_smart = smart, tcm_covar = covar
     go (NthCo r i co)      = mknthco r i <$> go co
     go (LRCo lr co)        = mklrco lr <$> go co
     go (InstCo co arg)     = mkinstco <$> go co <*> go arg
-    go (CoherenceCo c1 c2) = mkcoherenceco <$> go c1 <*> go c2
     go (KindCo co)         = mkkindco <$> go co
     go (SubCo co)          = mksubco <$> go co
 
@@ -575,16 +581,16 @@ mapCoercion mapper@(TyCoMapper { tcm_smart = smart, tcm_covar = covar
     go_prov p@(PluginProv _)    = return p
 
     ( mktyconappco, mkappco, mkaxiominstco, mkunivco
-      , mksymco, mktransco, mknthco, mklrco, mkinstco, mkcoherenceco
-      , mkkindco, mksubco, mkforallco)
+      , mksymco, mktransco, mknthco, mklrco, mkinstco
+      , mkkindco, mksubco, mkforallco, mkgreflco)
       | smart
       = ( mkTyConAppCo, mkAppCo, mkAxiomInstCo, mkUnivCo
-        , mkSymCo, mkTransCo, mkNthCo, mkLRCo, mkInstCo, mkCoherenceCo
-        , mkKindCo, mkSubCo, mkForAllCo )
+        , mkSymCo, mkTransCo, mkNthCo, mkLRCo, mkInstCo
+        , mkKindCo, mkSubCo, mkForAllCo, mkGReflCo )
       | otherwise
       = ( TyConAppCo, AppCo, AxiomInstCo, UnivCo
-        , SymCo, TransCo, NthCo, LRCo, InstCo, CoherenceCo
-        , KindCo, SubCo, ForAllCo )
+        , SymCo, TransCo, NthCo, LRCo, InstCo
+        , KindCo, SubCo, ForAllCo, GRefl )
 
 {-
 ************************************************************************
@@ -2293,7 +2299,8 @@ nonDetCmpTypeX env orig_t1 orig_t2 =
 nonDetCmpTypesX :: RnEnv2 -> [Type] -> [Type] -> Ordering
 nonDetCmpTypesX _   []        []        = EQ
 nonDetCmpTypesX env (t1:tys1) (t2:tys2) = nonDetCmpTypeX env t1 t2
-                                      `thenCmp` nonDetCmpTypesX env tys1 tys2
+                                          `thenCmp`
+                                          nonDetCmpTypesX env tys1 tys2
 nonDetCmpTypesX _   []        _         = LT
 nonDetCmpTypesX _   _         []        = GT
 
@@ -2463,8 +2470,15 @@ occCheckExpand vs_to_avoid ty
            -- See Note [Occurrence checking: look inside kinds]
 
     ------------------
-    go_co cxt (Refl r ty)               = do { ty' <- go cxt ty
-                                             ; return (mkReflCo r ty') }
+    go_mco _   MRefl = return MRefl
+    go_mco ctx (MCo co) = MCo <$> go_co ctx co
+
+    ------------------
+    go_co cxt (Refl ty)                 = do { ty' <- go cxt ty
+                                             ; return (mkNomReflCo ty') }
+    go_co cxt (GRefl r ty mco)          = do { mco' <- go_mco cxt mco
+                                             ; ty' <- go cxt ty
+                                             ; return (mkGReflCo r ty' mco') }
       -- Note: Coercions do not contain type synonyms
     go_co cxt (TyConAppCo r tc args)    = do { args' <- mapM (go_co cxt) args
                                              ; return (mkTyConAppCo r tc args') }
@@ -2504,9 +2518,6 @@ occCheckExpand vs_to_avoid ty
     go_co cxt (InstCo co arg)           = do { co' <- go_co cxt co
                                              ; arg' <- go_co cxt arg
                                              ; return (mkInstCo co' arg') }
-    go_co cxt (CoherenceCo co1 co2)     = do { co1' <- go_co cxt co1
-                                             ; co2' <- go_co cxt co2
-                                             ; return (mkCoherenceCo co1' co2') }
     go_co cxt (KindCo co)               = do { co' <- go_co cxt co
                                              ; return (mkKindCo co') }
     go_co cxt (SubCo co)                = do { co' <- go_co cxt co
@@ -2547,7 +2558,8 @@ tyConsOfType ty
      go (CastTy ty co)              = go ty `unionUniqSets` go_co co
      go (CoercionTy co)             = go_co co
 
-     go_co (Refl _ ty)             = go ty
+     go_co (Refl ty)               = go ty
+     go_co (GRefl _ ty mco)        = go ty `unionUniqSets` go_mco mco
      go_co (TyConAppCo _ tc args)  = go_tc tc `unionUniqSets` go_cos args
      go_co (AppCo co arg)          = go_co co `unionUniqSets` go_co arg
      go_co (ForAllCo _ kind_co co) = go_co kind_co `unionUniqSets` go_co co
@@ -2561,11 +2573,13 @@ tyConsOfType ty
      go_co (NthCo _ _ co)          = go_co co
      go_co (LRCo _ co)             = go_co co
      go_co (InstCo co arg)         = go_co co `unionUniqSets` go_co arg
-     go_co (CoherenceCo co1 co2)   = go_co co1 `unionUniqSets` go_co co2
      go_co (KindCo co)             = go_co co
      go_co (SubCo co)              = go_co co
      go_co (AxiomRuleCo _ cs)      = go_cos cs
 
+     go_mco MRefl    = emptyUniqSet
+     go_mco (MCo co) = go_co co
+
      go_prov UnsafeCoerceProv    = emptyUniqSet
      go_prov (PhantomProv co)    = go_co co
      go_prov (ProofIrrelProv co) = go_co co
diff --git a/compiler/types/Unify.hs b/compiler/types/Unify.hs
index edd82ba6fa..a8474524ab 100644
--- a/compiler/types/Unify.hs
+++ b/compiler/types/Unify.hs
@@ -1319,7 +1319,7 @@ data MatchEnv = ME { me_tmpls :: TyVarSet
                    , me_env   :: RnEnv2 }
 
 -- | 'liftCoMatch' is sort of inverse to 'liftCoSubst'.  In particular, if
---   @liftCoMatch vars ty co == Just s@, then @listCoSubst s ty == co@,
+--   @liftCoMatch vars ty co == Just s@, then @liftCoSubst s ty == co@,
 --   where @==@ there means that the result of 'liftCoSubst' has the same
 --   type as the original co; but may be different under the hood.
 --   That is, it matches a type against a coercion of the same
@@ -1392,9 +1392,6 @@ ty_co_match menv subst ty co lkco rkco
     ty_co_match menv subst ty' co (substed_co_l `mkTransCo` lkco)
                                   (substed_co_r `mkTransCo` rkco)
 
-  | CoherenceCo co1 co2 <- co
-  = ty_co_match menv subst ty co1 (lkco `mkTransCo` mkSymCo co2) rkco
-
   | SymCo co' <- co
   = swapLiftCoEnv <$> ty_co_match menv (swapLiftCoEnv subst) ty co' rkco lkco
 
@@ -1409,7 +1406,7 @@ ty_co_match menv subst (TyVarTy tv1) co lkco rkco
   = if any (inRnEnvR rn_env) (tyCoVarsOfCoList co)
     then Nothing      -- occurs check failed
     else Just $ extendVarEnv subst tv1' $
-                castCoercionKind co (mkSymCo lkco) (mkSymCo rkco)
+                castCoercionKindI co (mkSymCo lkco) (mkSymCo rkco)
 
   | otherwise
   = Nothing
@@ -1457,6 +1454,21 @@ ty_co_match menv subst (ForAllTy (TvBndr tv1 _) ty1)
 ty_co_match _ subst (CoercionTy {}) _ _ _
   = Just subst -- don't inspect coercions
 
+ty_co_match menv subst ty (GRefl r t (MCo co)) lkco rkco
+  =  ty_co_match menv subst ty (GRefl r t MRefl) lkco (rkco `mkTransCo` mkSymCo co)
+
+ty_co_match menv subst ty co1 lkco rkco
+  | Just (CastTy t co, r) <- isReflCo_maybe co1
+  -- In @pushRefl@, pushing reflexive coercion inside CastTy will give us
+  -- t |> co ~ t ; <t> ; t ~ t |> co
+  -- But transitive coercions are not helpful. Therefore we deal
+  -- with it here: we do recursion on the smaller reflexive coercion,
+  -- while propagating the correct kind coercions.
+  = let kco' = mkSymCo co
+    in ty_co_match menv subst ty (mkReflCo r t) (lkco `mkTransCo` kco')
+                                                (rkco `mkTransCo` kco')
+
+
 ty_co_match menv subst ty co lkco rkco
   | Just co' <- pushRefl co = ty_co_match menv subst ty co' lkco rkco
   | otherwise               = Nothing
@@ -1501,17 +1513,18 @@ ty_co_match_args menv subst (ty:tys) (arg:args) (lkco:lkcos) (rkco:rkcos)
 ty_co_match_args _    _     _        _          _ _ = Nothing
 
 pushRefl :: Coercion -> Maybe Coercion
-pushRefl (Refl Nominal (AppTy ty1 ty2))
-  = Just (AppCo (Refl Nominal ty1) (mkNomReflCo ty2))
-pushRefl (Refl r (FunTy ty1 ty2))
-  | Just rep1 <- getRuntimeRep_maybe ty1
-  , Just rep2 <- getRuntimeRep_maybe ty2
-  = Just (TyConAppCo r funTyCon [ mkReflCo r rep1, mkReflCo r rep2
-                                , mkReflCo r ty1,  mkReflCo r ty2 ])
-pushRefl (Refl r (TyConApp tc tys))
-  = Just (TyConAppCo r tc (zipWith mkReflCo (tyConRolesX r tc) tys))
-pushRefl (Refl r (ForAllTy (TvBndr tv _) ty))
-  = Just (mkHomoForAllCos_NoRefl [tv] (Refl r ty))
+pushRefl co =
+  case (isReflCo_maybe co) of
+    Just (AppTy ty1 ty2, Nominal)
+      -> Just (AppCo (mkReflCo Nominal ty1) (mkNomReflCo ty2))
+    Just (FunTy ty1 ty2, r)
+      | Just rep1 <- getRuntimeRep_maybe ty1
+      , Just rep2 <- getRuntimeRep_maybe ty2
+      ->  Just (TyConAppCo r funTyCon [ mkReflCo r rep1, mkReflCo r rep2
+                                       , mkReflCo r ty1,  mkReflCo r ty2 ])
+    Just (TyConApp tc tys, r)
+      -> Just (TyConAppCo r tc (zipWith mkReflCo (tyConRolesX r tc) tys))
+    Just (ForAllTy (TvBndr tv _) ty, r)
+      -> Just (mkHomoForAllCos_NoRefl [tv] (mkReflCo r ty))
     -- NB: NoRefl variant. Otherwise, we get a loop!
-pushRefl (Refl r (CastTy ty co))  = Just (castCoercionKind (Refl r ty) co co)
-pushRefl _                        = Nothing
+    _ -> Nothing