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, 5 insertions, 5 deletions

diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index df54dc2a94..dab9f2c308 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -50,7 +50,7 @@ import Name
 import VarEnv
 import VarSet
 import Id          ( idType, idName )
-import Var         ( TyVarBndr(..), mkTyVar )
+import Var         ( VarBndr(..), mkTyVar )
 import ErrUtils
 import DynFlags
 import Util
@@ -481,11 +481,11 @@ check_type env ctxt rank ty
                    (forAllEscapeErr env' ty tau_kind)
         }
   where
-    (tvbs, phi)  = tcSplitForAllTyVarBndrs ty
+    (tvbs, phi)  = tcSplitForAllVarBndrs ty
     (theta, tau) = tcSplitPhiTy phi
 
     tvs          = binderVars tvbs
-    (env', _)    = tidyTyCoVarBndrs env tvs
+    (env', _)    = tidyVarBndrs env tvs
 
     tau_kind              = typeKind tau
     phi_kind | null theta = tau_kind
@@ -2079,7 +2079,7 @@ checkValidTelescope :: [TyConBinder]   -- explicit vars (zonked)
 checkValidTelescope tvbs user_tyvars extra
   = do { let tvs      = binderVars tvbs
 
-             (_, sorted_tidied_tvs) = tidyTyCoVarBndrs emptyTidyEnv $
+             (_, sorted_tidied_tvs) = tidyVarBndrs emptyTidyEnv $
                                       toposortTyVars tvs
        ; unless (go [] emptyVarSet (binderVars tvbs)) $
          addErr $
@@ -2118,7 +2118,7 @@ fvType (TyConApp _ tys)      = fvTypes tys
 fvType (LitTy {})            = []
 fvType (AppTy fun arg)       = fvType fun ++ fvType arg
 fvType (FunTy arg res)       = fvType arg ++ fvType res
-fvType (ForAllTy (TvBndr tv _) ty)
+fvType (ForAllTy (Bndr tv _) ty)
   = fvType (tyVarKind tv) ++
     filter (/= tv) (fvType ty)
 fvType (CastTy ty _)         = fvType ty