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

4 files changed, 83 insertions, 48 deletions

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)