Coercion Quantification

This patch corresponds to #15497.

According to https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase2,
 we would like to have coercion quantifications back. This will
allow us to migrate (~#) to be homogeneous, instead of its current
heterogeneous definition. This patch is (lots of) plumbing only. There
should be no user-visible effects.

An overview of changes:

- Both `ForAllTy` and `ForAllCo` can quantify over coercion variables,
but only in *Core*. All relevant functions are updated accordingly.
- Small changes that should be irrelevant to the main task:
    1. removed dead code `mkTransAppCo` in Coercion
    2. removed out-dated Note Computing a coercion kind and
       roles in Coercion
    3. Added `Eq4` in Note Respecting definitional equality in
       TyCoRep, and updated `mkCastTy` accordingly.
    4. Various updates and corrections of notes and typos.
- Haddock submodule needs to be changed too.

Acknowledgments:
This work was completed mostly during Ningning Xie's Google Summer
of Code, sponsored by Google. It was advised by Richard Eisenberg,
supported by NSF grant 1704041.

Test Plan: ./validate

Reviewers: goldfire, simonpj, bgamari, hvr, erikd, simonmar

Subscribers: RyanGlScott, monoidal, rwbarton, carter

GHC Trac Issues: #15497

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

1 files changed, 26 insertions, 17 deletions

diff --git a/compiler/iface/ToIface.hs b/compiler/iface/ToIface.hs
index 0b0782d6e8..653b7407da 100644
--- a/compiler/iface/ToIface.hs
+++ b/compiler/iface/ToIface.hs
@@ -8,7 +8,7 @@ module ToIface
     , toIfaceIdBndr
     , toIfaceBndr
     , toIfaceForAllBndr
-    , toIfaceTyVarBinders
+    , toIfaceTyCoVarBinders
     , toIfaceTyVar
       -- * Types
     , toIfaceType, toIfaceTypeX
@@ -81,23 +81,32 @@ toIfaceTvBndrX fr tyvar = ( occNameFS (getOccName tyvar)
                           , toIfaceTypeX fr (tyVarKind tyvar)
                           )
 
-
-toIfaceIdBndr :: Id -> (IfLclName, IfaceType)
-toIfaceIdBndr id      = (occNameFS (getOccName id),    toIfaceType (idType id))
-
 toIfaceTvBndrs :: [TyVar] -> [IfaceTvBndr]
 toIfaceTvBndrs = map toIfaceTvBndr
 
+toIfaceIdBndr :: Id -> IfaceIdBndr
+toIfaceIdBndr = toIfaceIdBndrX emptyVarSet
+
+toIfaceIdBndrX :: VarSet -> CoVar -> IfaceIdBndr
+toIfaceIdBndrX fr covar = ( occNameFS (getOccName covar)
+                          , toIfaceTypeX fr (varType covar)
+                          )
+
 toIfaceBndr :: Var -> IfaceBndr
 toIfaceBndr var
   | isId var  = IfaceIdBndr (toIfaceIdBndr var)
   | otherwise = IfaceTvBndr (toIfaceTvBndr var)
 
-toIfaceTyVarBinder :: TyVarBndr TyVar vis -> TyVarBndr IfaceTvBndr vis
-toIfaceTyVarBinder (TvBndr tv vis) = TvBndr (toIfaceTvBndr tv) vis
+toIfaceBndrX :: VarSet -> Var -> IfaceBndr
+toIfaceBndrX fr var
+  | isId var  = IfaceIdBndr (toIfaceIdBndrX fr var)
+  | otherwise = IfaceTvBndr (toIfaceTvBndrX fr var)
+
+toIfaceTyCoVarBinder :: VarBndr Var vis -> VarBndr IfaceBndr vis
+toIfaceTyCoVarBinder (Bndr tv vis) = Bndr (toIfaceBndr tv) vis
 
-toIfaceTyVarBinders :: [TyVarBndr TyVar vis] -> [TyVarBndr IfaceTvBndr vis]
-toIfaceTyVarBinders = map toIfaceTyVarBinder
+toIfaceTyCoVarBinders :: [VarBndr Var vis] -> [VarBndr IfaceBndr vis]
+toIfaceTyCoVarBinders = map toIfaceTyCoVarBinder
 
 {-
 ************************************************************************
@@ -168,11 +177,11 @@ toIfaceTyVar = occNameFS . getOccName
 toIfaceCoVar :: CoVar -> FastString
 toIfaceCoVar = occNameFS . getOccName
 
-toIfaceForAllBndr :: TyVarBinder -> IfaceForAllBndr
+toIfaceForAllBndr :: TyCoVarBinder -> IfaceForAllBndr
 toIfaceForAllBndr = toIfaceForAllBndrX emptyVarSet
 
-toIfaceForAllBndrX :: VarSet -> TyVarBinder -> IfaceForAllBndr
-toIfaceForAllBndrX fr (TvBndr v vis) = TvBndr (toIfaceTvBndrX fr v) vis
+toIfaceForAllBndrX :: VarSet -> TyCoVarBinder -> IfaceForAllBndr
+toIfaceForAllBndrX fr (Bndr v vis) = Bndr (toIfaceBndrX fr v) vis
 
 ----------------
 toIfaceTyCon :: TyCon -> IfaceTyCon
@@ -256,7 +265,7 @@ toIfaceCoercionX fr co
       | otherwise                = IfaceTyConAppCo r (toIfaceTyCon tc) (map go cos)
     go (FunCo r co1 co2)   = IfaceFunCo r (go co1) (go co2)
 
-    go (ForAllCo tv k co) = IfaceForAllCo (toIfaceTvBndr tv)
+    go (ForAllCo tv k co) = IfaceForAllCo (toIfaceBndr tv)
                                           (toIfaceCoercionX fr' k)
                                           (toIfaceCoercionX fr' co)
                           where
@@ -295,12 +304,12 @@ toIfaceAppArgsX fr kind ty_args
     go env ty                  ts
       | Just ty' <- coreView ty
       = go env ty' ts
-    go env (ForAllTy (TvBndr tv vis) res) (t:ts)
+    go env (ForAllTy (Bndr tv vis) res) (t:ts)
       | isVisibleArgFlag vis = IA_Vis   t' ts'
       | otherwise            = IA_Invis t' ts'
       where
         t'  = toIfaceTypeX fr t
-        ts' = go (extendTvSubst env tv t) res ts
+        ts' = go (extendTCvSubst env tv t) res ts
 
     go env (FunTy _ res) (t:ts) -- No type-class args in tycon apps
       = IA_Vis (toIfaceTypeX fr t) (go env res ts)
@@ -354,8 +363,8 @@ patSynToIfaceDecl ps
     (_univ_tvs, req_theta, _ex_tvs, prov_theta, args, rhs_ty) = patSynSig ps
     univ_bndrs = patSynUnivTyVarBinders ps
     ex_bndrs   = patSynExTyVarBinders ps
-    (env1, univ_bndrs') = tidyTyVarBinders emptyTidyEnv univ_bndrs
-    (env2, ex_bndrs')   = tidyTyVarBinders env1 ex_bndrs
+    (env1, univ_bndrs') = tidyTyCoVarBinders emptyTidyEnv univ_bndrs
+    (env2, ex_bndrs')   = tidyTyCoVarBinders env1 ex_bndrs
     to_if_pr (id, needs_dummy) = (idName id, needs_dummy)
 
 {-