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

8 files changed, 152 insertions, 124 deletions

diff --git a/compiler/iface/BuildTyCl.hs b/compiler/iface/BuildTyCl.hs
index 3ddd355a6d..693e2899c8 100644
--- a/compiler/iface/BuildTyCl.hs
+++ b/compiler/iface/BuildTyCl.hs
@@ -101,7 +101,7 @@ buildDataCon :: FamInstEnvs
                 -- See Note [Bangs on imported data constructors] in MkId
            -> [FieldLabel]             -- Field labels
            -> [TyVar]                  -- Universals
-           -> [TyVar]                  -- Existentials
+           -> [TyCoVar]                -- Existentials
            -> [TyVarBinder]            -- User-written 'TyVarBinder's
            -> [EqSpec]                 -- Equality spec
            -> KnotTied ThetaType       -- Does not include the "stupid theta"
diff --git a/compiler/iface/IfaceSyn.hs b/compiler/iface/IfaceSyn.hs
index 2784dda795..3266c5aec1 100644
--- a/compiler/iface/IfaceSyn.hs
+++ b/compiler/iface/IfaceSyn.hs
@@ -64,7 +64,7 @@ import SrcLoc
 import Fingerprint
 import Binary
 import BooleanFormula ( BooleanFormula, pprBooleanFormula, isTrue )
-import Var( TyVarBndr(..) )
+import Var( VarBndr(..) )
 import TyCon ( Role (..), Injectivity(..) )
 import Util( dropList, filterByList )
 import DataCon (SrcStrictness(..), SrcUnpackedness(..))
@@ -243,13 +243,13 @@ data IfaceConDecl
         -- but it's not so easy for the original TyCon/DataCon
         -- So this guarantee holds for IfaceConDecl, but *not* for DataCon
 
-        ifConExTvs   :: [IfaceTvBndr],  -- Existential tyvars
+        ifConExTCvs   :: [IfaceBndr],  -- Existential ty/covars
         ifConUserTvBinders :: [IfaceForAllBndr],
           -- The tyvars, in the order the user wrote them
           -- INVARIANT: the set of tyvars in ifConUserTvBinders is exactly the
-          --            set of ifConExTvs, unioned with the set of ifBinders
-          --            (from the parent IfaceDecl) whose tyvars do not appear
-          --            in ifConEqSpec
+          --            set of tyvars (*not* covars) of ifConExTCvs, unioned
+          --            with the set of ifBinders (from the parent IfaceDecl)
+          --            whose tyvars do not appear in ifConEqSpec
           -- See Note [DataCon user type variable binders] in DataCon
         ifConEqSpec  :: IfaceEqSpec,        -- Equality constraints
         ifConCtxt    :: IfaceContext,       -- Non-stupid context
@@ -1062,8 +1062,11 @@ pprIfaceConDecl ss gadt_style tycon tc_binders parent
     ppr_tc_app gadt_subst dflags
        = pprPrefixIfDeclBndr how_much (occName tycon)
          <+> sep [ pprParendIfaceType (substIfaceTyVar gadt_subst tv)
-                 | (tv,_kind)
-                     <- map ifTyConBinderTyVar $
+                 | IfaceTvBndr (tv,_kind)
+                   -- Coercions variables are invisible, see Note
+                   -- [VarBndrs, TyCoVarBinders, TyConBinders, and visibility]
+                   -- in TyCoRep
+                     <- map (ifTyConBinderVar) $
                         suppressIfaceInvisibles dflags tc_binders tc_binders ]
 
 instance Outputable IfaceRule where
@@ -1290,7 +1293,7 @@ freeNamesIfDecl (IfaceId { ifType = t, ifIdDetails = d, ifIdInfo = i})
 
 freeNamesIfDecl (IfaceData { ifBinders = bndrs, ifResKind = res_k
                            , ifParent = p, ifCtxt = ctxt, ifCons = cons })
-  = freeNamesIfTyVarBndrs bndrs &&&
+  = freeNamesIfVarBndrs bndrs &&&
     freeNamesIfType res_k &&&
     freeNamesIfaceTyConParent p &&&
     freeNamesIfContext ctxt &&&
@@ -1298,18 +1301,18 @@ freeNamesIfDecl (IfaceData { ifBinders = bndrs, ifResKind = res_k
 
 freeNamesIfDecl (IfaceSynonym { ifBinders = bndrs, ifResKind = res_k
                               , ifSynRhs = rhs })
-  = freeNamesIfTyVarBndrs bndrs &&&
+  = freeNamesIfVarBndrs bndrs &&&
     freeNamesIfKind res_k &&&
     freeNamesIfType rhs
 
 freeNamesIfDecl (IfaceFamily { ifBinders = bndrs, ifResKind = res_k
                              , ifFamFlav = flav })
-  = freeNamesIfTyVarBndrs bndrs &&&
+  = freeNamesIfVarBndrs bndrs &&&
     freeNamesIfKind res_k &&&
     freeNamesIfFamFlav flav
 
 freeNamesIfDecl (IfaceClass{ ifBinders = bndrs, ifBody = cls_body })
-  = freeNamesIfTyVarBndrs bndrs &&&
+  = freeNamesIfVarBndrs bndrs &&&
     freeNamesIfClassBody cls_body
 
 freeNamesIfDecl (IfaceAxiom { ifTyCon = tc, ifAxBranches = branches })
@@ -1327,8 +1330,8 @@ freeNamesIfDecl (IfacePatSyn { ifPatMatcher = (matcher, _)
                              , ifFieldLabels = lbls })
   = unitNameSet matcher &&&
     maybe emptyNameSet (unitNameSet . fst) mb_builder &&&
-    freeNamesIfTyVarBndrs univ_bndrs &&&
-    freeNamesIfTyVarBndrs ex_bndrs &&&
+    freeNamesIfVarBndrs univ_bndrs &&&
+    freeNamesIfVarBndrs ex_bndrs &&&
     freeNamesIfContext prov_ctxt &&&
     freeNamesIfContext req_ctxt &&&
     fnList freeNamesIfType args &&&
@@ -1391,12 +1394,12 @@ freeNamesIfConDecls (IfNewTyCon  c) = freeNamesIfConDecl c
 freeNamesIfConDecls _                   = emptyNameSet
 
 freeNamesIfConDecl :: IfaceConDecl -> NameSet
-freeNamesIfConDecl (IfCon { ifConExTvs   = ex_tvs, ifConCtxt = ctxt
+freeNamesIfConDecl (IfCon { ifConExTCvs  = ex_tvs, ifConCtxt = ctxt
                           , ifConArgTys  = arg_tys
                           , ifConFields  = flds
                           , ifConEqSpec  = eq_spec
                           , ifConStricts = bangs })
-  = fnList freeNamesIfTvBndr ex_tvs &&&
+  = fnList freeNamesIfBndr ex_tvs &&&
     freeNamesIfContext ctxt &&&
     fnList freeNamesIfType arg_tys &&&
     mkNameSet (map flSelector flds) &&&
@@ -1422,7 +1425,7 @@ freeNamesIfType (IfaceAppTy s t)      = freeNamesIfType s &&& freeNamesIfAppArgs
 freeNamesIfType (IfaceTyConApp tc ts) = freeNamesIfTc tc &&& freeNamesIfAppArgs ts
 freeNamesIfType (IfaceTupleTy _ _ ts) = freeNamesIfAppArgs ts
 freeNamesIfType (IfaceLitTy _)        = emptyNameSet
-freeNamesIfType (IfaceForAllTy tv t)  = freeNamesIfTyVarBndr tv &&& freeNamesIfType t
+freeNamesIfType (IfaceForAllTy tv t)  = freeNamesIfVarBndr tv &&& freeNamesIfType t
 freeNamesIfType (IfaceFunTy s t)      = freeNamesIfType s &&& freeNamesIfType t
 freeNamesIfType (IfaceDFunTy s t)     = freeNamesIfType s &&& freeNamesIfType t
 freeNamesIfType (IfaceCastTy t c)     = freeNamesIfType t &&& freeNamesIfCoercion c
@@ -1475,11 +1478,11 @@ freeNamesIfProv (IfacePhantomProv co)    = freeNamesIfCoercion co
 freeNamesIfProv (IfaceProofIrrelProv co) = freeNamesIfCoercion co
 freeNamesIfProv (IfacePluginProv _)      = emptyNameSet
 
-freeNamesIfTyVarBndr :: TyVarBndr IfaceTvBndr vis -> NameSet
-freeNamesIfTyVarBndr (TvBndr tv _) = freeNamesIfTvBndr tv
+freeNamesIfVarBndr :: VarBndr IfaceBndr vis -> NameSet
+freeNamesIfVarBndr (Bndr bndr _) = freeNamesIfBndr bndr
 
-freeNamesIfTyVarBndrs :: [TyVarBndr IfaceTvBndr vis] -> NameSet
-freeNamesIfTyVarBndrs = fnList freeNamesIfTyVarBndr
+freeNamesIfVarBndrs :: [VarBndr IfaceBndr vis] -> NameSet
+freeNamesIfVarBndrs = fnList freeNamesIfVarBndr
 
 freeNamesIfBndr :: IfaceBndr -> NameSet
 freeNamesIfBndr (IfaceIdBndr b) = freeNamesIfIdBndr b
diff --git a/compiler/iface/IfaceType.hs b/compiler/iface/IfaceType.hs
index 06ea8ff8db..23b09dab7a 100644
--- a/compiler/iface/IfaceType.hs
+++ b/compiler/iface/IfaceType.hs
@@ -22,8 +22,8 @@ module IfaceType (
         IfaceTvBndr, IfaceIdBndr, IfaceTyConBinder,
         IfaceForAllBndr, ArgFlag(..), ShowForAllFlag(..),
 
-        ifForAllBndrTyVar, ifForAllBndrName,
-        ifTyConBinderTyVar, ifTyConBinderName,
+        ifForAllBndrVar, ifForAllBndrName,
+        ifTyConBinderVar, ifTyConBinderName,
 
         -- Equality testing
         isIfaceLiftedTypeKind,
@@ -96,6 +96,13 @@ type IfaceTvBndr  = (IfLclName, IfaceKind)
 ifaceTvBndrName :: IfaceTvBndr -> IfLclName
 ifaceTvBndrName (n,_) = n
 
+ifaceIdBndrName :: IfaceIdBndr -> IfLclName
+ifaceIdBndrName (n,_) = n
+
+ifaceBndrName :: IfaceBndr -> IfLclName
+ifaceBndrName (IfaceTvBndr bndr) = ifaceTvBndrName bndr
+ifaceBndrName (IfaceIdBndr bndr) = ifaceIdBndrName bndr
+
 type IfaceLamBndr = (IfaceBndr, IfaceOneShot)
 
 data IfaceOneShot    -- See Note [Preserve OneShotInfo] in CoreTicy
@@ -148,8 +155,8 @@ data IfaceTyLit
   | IfaceStrTyLit FastString
   deriving (Eq)
 
-type IfaceTyConBinder = TyVarBndr IfaceTvBndr TyConBndrVis
-type IfaceForAllBndr  = TyVarBndr IfaceTvBndr ArgFlag
+type IfaceTyConBinder = VarBndr IfaceBndr TyConBndrVis
+type IfaceForAllBndr  = VarBndr IfaceBndr ArgFlag
 
 -- See Note [Suppressing invisible arguments]
 -- We use a new list type (rather than [(IfaceType,Bool)], because
@@ -297,7 +304,7 @@ data IfaceCoercion
   | IfaceFunCo        Role IfaceCoercion IfaceCoercion
   | IfaceTyConAppCo   Role IfaceTyCon [IfaceCoercion]
   | IfaceAppCo        IfaceCoercion IfaceCoercion
-  | IfaceForAllCo     IfaceTvBndr IfaceCoercion IfaceCoercion
+  | IfaceForAllCo     IfaceBndr IfaceCoercion IfaceCoercion
   | IfaceCoVarCo      IfLclName
   | IfaceAxiomInstCo  IfExtName BranchIndex [IfaceCoercion]
   | IfaceAxiomRuleCo  IfLclName [IfaceCoercion]
@@ -398,21 +405,21 @@ stripIfaceInvisVars dflags tyvars
   | gopt Opt_PrintExplicitKinds dflags = tyvars
   | otherwise = filterOut isInvisibleTyConBinder tyvars
 
--- | Extract an 'IfaceTvBndr' from an 'IfaceForAllBndr'.
-ifForAllBndrTyVar :: IfaceForAllBndr -> IfaceTvBndr
-ifForAllBndrTyVar = binderVar
+-- | Extract an 'IfaceBndr' from an 'IfaceForAllBndr'.
+ifForAllBndrVar :: IfaceForAllBndr -> IfaceBndr
+ifForAllBndrVar = binderVar
 
 -- | Extract the variable name from an 'IfaceForAllBndr'.
 ifForAllBndrName :: IfaceForAllBndr -> IfLclName
-ifForAllBndrName fab = ifaceTvBndrName (ifForAllBndrTyVar fab)
+ifForAllBndrName fab = ifaceBndrName (ifForAllBndrVar fab)
 
--- | Extract an 'IfaceTvBndr' from an 'IfaceTyConBinder'.
-ifTyConBinderTyVar :: IfaceTyConBinder -> IfaceTvBndr
-ifTyConBinderTyVar = binderVar
+-- | Extract an 'IfaceBndr' from an 'IfaceTyConBinder'.
+ifTyConBinderVar :: IfaceTyConBinder -> IfaceBndr
+ifTyConBinderVar = binderVar
 
 -- | Extract the variable name from an 'IfaceTyConBinder'.
 ifTyConBinderName :: IfaceTyConBinder -> IfLclName
-ifTyConBinderName tcb = ifaceTvBndrName (ifTyConBinderTyVar tcb)
+ifTyConBinderName tcb = ifaceBndrName (ifTyConBinderVar tcb)
 
 ifTypeIsVarFree :: IfaceType -> Bool
 -- Returns True if the type definitely has no variables at all
@@ -532,8 +539,8 @@ stripInvisArgs dflags tys
             IA_Vis   t ts -> IA_Vis t $ suppress_invis ts
               -- Keep recursing through the remainder of the arguments, as it's
               -- possible that there are remaining invisible ones.
-              -- See the "In type declarations" section of Note [TyVarBndrs,
-              -- TyVarBinders, TyConBinders, and visibility] in TyCoRep.
+              -- See the "In type declarations" section of Note [VarBndrs,
+              -- TyCoVarBinders, TyConBinders, and visibility] in TyCoRep.
 
 appArgsIfaceTypes :: IfaceAppArgs -> [IfaceType]
 appArgsIfaceTypes IA_Nil = []
@@ -660,9 +667,10 @@ pprIfaceTvBndr use_parens (tv, ki)
                  | otherwise  = id
 
 pprIfaceTyConBinders :: [IfaceTyConBinder] -> SDoc
-pprIfaceTyConBinders = sep . map go
+pprIfaceTyConBinders = sep . map (go . ifTyConBinderVar)
   where
-    go tcb = pprIfaceTvBndr True (ifTyConBinderTyVar tcb)
+    go (IfaceIdBndr bndr) = pprIfaceIdBndr bndr
+    go (IfaceTvBndr bndr) = pprIfaceTvBndr True bndr
 
 instance Binary IfaceBndr where
     put_ bh (IfaceIdBndr aa) = do
@@ -756,7 +764,7 @@ ppr_ty ctxt_prec (IfaceCoercionTy co)
       (ppr_co ctxt_prec co)
       (text "<>")
 
-ppr_ty ctxt_prec ty
+ppr_ty ctxt_prec ty -- IfaceForAllTy
   = maybeParen ctxt_prec funPrec (pprIfaceSigmaType ShowForAllMust ty)
 
 {-
@@ -804,18 +812,15 @@ defaultRuntimeRepVars :: PprStyle -> IfaceType -> IfaceType
 defaultRuntimeRepVars sty = go emptyFsEnv
   where
     go :: FastStringEnv () -> IfaceType -> IfaceType
-    go subs (IfaceForAllTy bndr ty)
+    go subs (IfaceForAllTy (Bndr (IfaceTvBndr (var, var_kind)) argf) ty)
       | isRuntimeRep var_kind
-      , isInvisibleArgFlag (binderArgFlag bndr) -- don't default *visible* quantification
-                                                -- or we get the mess in #13963
+      , isInvisibleArgFlag argf -- don't default *visible* quantification
+                                -- or we get the mess in #13963
       = let subs' = extendFsEnv subs var ()
         in go subs' ty
-      | otherwise
-      = IfaceForAllTy (TvBndr (var, go subs var_kind) (binderArgFlag bndr))
-                      (go subs ty)
-      where
-        var :: IfLclName
-        (var, var_kind) = binderVar bndr
+
+    go subs (IfaceForAllTy bndr ty)
+      = IfaceForAllTy (go_ifacebndr subs bndr) (go subs ty)
 
     go subs ty@(IfaceTyVar tv)
       | tv `elemFsEnv` subs
@@ -851,6 +856,12 @@ defaultRuntimeRepVars sty = go emptyFsEnv
     go _ ty@(IfaceLitTy {}) = ty
     go _ ty@(IfaceCoercionTy {}) = ty
 
+    go_ifacebndr :: FastStringEnv () -> IfaceForAllBndr -> IfaceForAllBndr
+    go_ifacebndr subs (Bndr (IfaceIdBndr (n, t)) argf)
+      = Bndr (IfaceIdBndr (n, go subs t)) argf
+    go_ifacebndr subs (Bndr (IfaceTvBndr (n, t)) argf)
+      = Bndr (IfaceTvBndr (n, go subs t)) argf
+
     go_args :: FastStringEnv () -> IfaceAppArgs -> IfaceAppArgs
     go_args _ IA_Nil = IA_Nil
     go_args subs (IA_Vis ty args)   = IA_Vis   (go subs ty) (go_args subs args)
@@ -917,7 +928,7 @@ ppr_iface_forall_part show_forall tvs ctxt sdoc
 -- | Render the "forall ... ." or "forall ... ->" bit of a type.
 pprIfaceForAll :: [IfaceForAllBndr] -> SDoc
 pprIfaceForAll [] = empty
-pprIfaceForAll bndrs@(TvBndr _ vis : _)
+pprIfaceForAll bndrs@(Bndr _ vis : _)
   = add_separator (forAllLit <+> doc) <+> pprIfaceForAll bndrs'
   where
     (bndrs', doc) = ppr_itv_bndrs bndrs vis
@@ -933,7 +944,7 @@ pprIfaceForAll bndrs@(TvBndr _ vis : _)
 ppr_itv_bndrs :: [IfaceForAllBndr]
              -> ArgFlag  -- ^ visibility of the first binder in the list
              -> ([IfaceForAllBndr], SDoc)
-ppr_itv_bndrs all_bndrs@(bndr@(TvBndr _ vis) : bndrs) vis1
+ppr_itv_bndrs all_bndrs@(bndr@(Bndr _ vis) : bndrs) vis1
   | vis `sameVis` vis1 = let (bndrs', doc) = ppr_itv_bndrs bndrs vis1 in
                          (bndrs', pprIfaceForAllBndr bndr <+> doc)
   | otherwise   = (all_bndrs, empty)
@@ -947,11 +958,13 @@ pprIfaceForAllCoBndrs :: [(IfLclName, IfaceCoercion)] -> SDoc
 pprIfaceForAllCoBndrs bndrs = hsep $ map pprIfaceForAllCoBndr bndrs
 
 pprIfaceForAllBndr :: IfaceForAllBndr -> SDoc
-pprIfaceForAllBndr (TvBndr tv Inferred) = sdocWithDynFlags $ \dflags ->
-                                           if gopt Opt_PrintExplicitForalls dflags
-                                           then braces $ pprIfaceTvBndr False tv
-                                           else pprIfaceTvBndr True tv
-pprIfaceForAllBndr (TvBndr tv _)        = pprIfaceTvBndr True tv
+pprIfaceForAllBndr (Bndr (IfaceTvBndr tv) Inferred)
+  = sdocWithDynFlags $ \dflags ->
+                          if gopt Opt_PrintExplicitForalls dflags
+                          then braces $ pprIfaceTvBndr False tv
+                          else pprIfaceTvBndr True tv
+pprIfaceForAllBndr (Bndr (IfaceTvBndr tv) _)  = pprIfaceTvBndr True tv
+pprIfaceForAllBndr (Bndr (IfaceIdBndr idv) _) = pprIfaceIdBndr idv
 
 pprIfaceForAllCoBndr :: (IfLclName, IfaceCoercion) -> SDoc
 pprIfaceForAllCoBndr (tv, kind_co)
@@ -981,7 +994,10 @@ pprUserIfaceForAll tvs
              || gopt Opt_PrintExplicitForalls dflags) $
      pprIfaceForAll tvs
    where
-     tv_has_kind_var (TvBndr (_,kind) _) = not (ifTypeIsVarFree kind)
+     tv_has_kind_var (Bndr (IfaceTvBndr (_,kind)) _)
+       = not (ifTypeIsVarFree kind)
+     tv_has_kind_var _ = False
+
      tv_is_required = isVisibleArgFlag . binderArgFlag
 
 {-
@@ -1012,8 +1028,10 @@ criteria are met:
    because omitting it and printing "T :: k -> Type" would be
    utterly misleading.
 
-   See Note [TyVarBndrs, TyVarBinders, TyConBinders, and visibility]
+   See Note [VarBndrs, TyCoVarBinders, TyConBinders, and visibility]
    in TyCoRep.
+
+N.B. Until now (Aug 2018) we didn't check anything for coercion variables.
 -}
 
 -------------------
@@ -1108,7 +1126,7 @@ pprTyTcApp' ctxt_prec tc tys dflags style
 -- of   eqTyCon          (~)
 --      eqPrimTyCon      (~#)
 --      eqReprPrimTyCon  (~R#)
---      hEqTyCon         (~~)
+--      heqTyCon         (~~)
 --
 -- See Note [Equality predicates in IfaceType]
 -- and Note [The equality types story] in TysPrim
@@ -1280,7 +1298,9 @@ ppr_co ctxt_prec co@(IfaceForAllCo {})
   where
     (tvs, inner_co) = split_co co
 
-    split_co (IfaceForAllCo (name, _) kind_co co')
+    split_co (IfaceForAllCo (IfaceTvBndr (name, _)) kind_co co')
+      = let (tvs, co'') = split_co co' in ((name,kind_co):tvs,co'')
+    split_co (IfaceForAllCo (IfaceIdBndr (name, _)) kind_co co')
       = let (tvs, co'') = split_co co' in ((name,kind_co):tvs,co'')
     split_co co' = ([], co')
 
diff --git a/compiler/iface/IfaceType.hs-boot b/compiler/iface/IfaceType.hs-boot
index 200e96c69d..44f1f3cfc2 100644
--- a/compiler/iface/IfaceType.hs-boot
+++ b/compiler/iface/IfaceType.hs-boot
@@ -3,16 +3,13 @@
 module IfaceType( IfaceType, IfaceTyCon, IfaceForAllBndr
                 , IfaceCoercion, IfaceTyLit, IfaceAppArgs ) where
 
-import Var (TyVarBndr, ArgFlag)
-import FastString (FastString)
+import Var (VarBndr, ArgFlag)
 
 data IfaceAppArgs
-type IfLclName = FastString
-type IfaceKind = IfaceType
 
 data IfaceType
 data IfaceTyCon
 data IfaceTyLit
 data IfaceCoercion
-type IfaceTvBndr      = (IfLclName, IfaceKind)
-type IfaceForAllBndr  = TyVarBndr IfaceTvBndr ArgFlag
+data IfaceBndr
+type IfaceForAllBndr  = VarBndr IfaceBndr ArgFlag
diff --git a/compiler/iface/MkIface.hs b/compiler/iface/MkIface.hs
index 59a396e381..4d2fa83f86 100644
--- a/compiler/iface/MkIface.hs
+++ b/compiler/iface/MkIface.hs
@@ -1646,7 +1646,7 @@ coAxBranchToIfaceBranch' tc (CoAxBranch { cab_tvs = tvs, cab_cvs = cvs
                   , ifaxbRHS     = tidyToIfaceType env1 rhs
                   , ifaxbIncomps = [] }
   where
-    (env1, tidy_tvs) = tidyTyCoVarBndrs emptyTidyEnv tvs
+    (env1, tidy_tvs) = tidyVarBndrs emptyTidyEnv tvs
     -- Don't re-bind in-scope tyvars
     -- See Note [CoAxBranch type variables] in CoAxiom
 
@@ -1710,7 +1710,7 @@ tyConToIfaceDecl env tycon
     -- an error.
     (tc_env1, tc_binders) = tidyTyConBinders env (tyConBinders tycon)
     tc_tyvars      = binderVars tc_binders
-    if_binders     = toIfaceTyVarBinders tc_binders
+    if_binders     = toIfaceTyCoVarBinders tc_binders
     if_res_kind    = tidyToIfaceType tc_env1 (tyConResKind tycon)
     if_syn_type ty = tidyToIfaceType tc_env1 ty
     if_res_var     = getOccFS `fmap` tyConFamilyResVar_maybe tycon
@@ -1751,7 +1751,7 @@ tyConToIfaceDecl env tycon
         = IfCon   { ifConName    = dataConName data_con,
                     ifConInfix   = dataConIsInfix data_con,
                     ifConWrapper = isJust (dataConWrapId_maybe data_con),
-                    ifConExTvs   = map toIfaceTvBndr ex_tvs',
+                    ifConExTCvs  = map toIfaceBndr ex_tvs',
                     ifConUserTvBinders = map toIfaceForAllBndr user_bndrs',
                     ifConEqSpec  = map (to_eq_spec . eqSpecPair) eq_spec,
                     ifConCtxt    = tidyToIfaceContext con_env2 theta,
@@ -1776,27 +1776,27 @@ tyConToIfaceDecl env tycon
           con_env1 = (fst tc_env1, mkVarEnv (zipEqual "ifaceConDecl" univ_tvs tc_tyvars))
                      -- A bit grimy, perhaps, but it's simple!
 
-          (con_env2, ex_tvs') = tidyTyCoVarBndrs con_env1 ex_tvs
-          user_bndrs' = map (tidyUserTyVarBinder con_env2) user_bndrs
+          (con_env2, ex_tvs') = tidyVarBndrs con_env1 ex_tvs
+          user_bndrs' = map (tidyUserTyCoVarBinder con_env2) user_bndrs
           to_eq_spec (tv,ty) = (tidyTyVar con_env2 tv, tidyToIfaceType con_env2 ty)
 
           -- By this point, we have tidied every universal and existential
-          -- tyvar. Because of the dcUserTyVarBinders invariant
+          -- tyvar. Because of the dcUserTyCoVarBinders invariant
           -- (see Note [DataCon user type variable binders]), *every*
           -- user-written tyvar must be contained in the substitution that
           -- tidying produced. Therefore, tidying the user-written tyvars is a
           -- simple matter of looking up each variable in the substitution,
-          -- which tidyTyVarOcc accomplishes.
-          tidyUserTyVarBinder :: TidyEnv -> TyVarBinder -> TyVarBinder
-          tidyUserTyVarBinder env (TvBndr tv vis) =
-            TvBndr (tidyTyVarOcc env tv) vis
+          -- which tidyTyCoVarOcc accomplishes.
+          tidyUserTyCoVarBinder :: TidyEnv -> TyCoVarBinder -> TyCoVarBinder
+          tidyUserTyCoVarBinder env (Bndr tv vis) =
+            Bndr (tidyTyCoVarOcc env tv) vis
 
 classToIfaceDecl :: TidyEnv -> Class -> (TidyEnv, IfaceDecl)
 classToIfaceDecl env clas
   = ( env1
     , IfaceClass { ifName   = getName tycon,
                    ifRoles  = tyConRoles (classTyCon clas),
-                   ifBinders = toIfaceTyVarBinders tc_binders,
+                   ifBinders = toIfaceTyCoVarBinders tc_binders,
                    ifBody   = body,
                    ifFDs    = map toIfaceFD clas_fds })
   where
@@ -1848,10 +1848,10 @@ tidyTyConBinder :: TidyEnv -> TyConBinder -> (TidyEnv, TyConBinder)
 -- If the type variable "binder" is in scope, don't re-bind it
 -- In a class decl, for example, the ATD binders mention
 -- (amd must mention) the class tyvars
-tidyTyConBinder env@(_, subst) tvb@(TvBndr tv vis)
+tidyTyConBinder env@(_, subst) tvb@(Bndr tv vis)
  = case lookupVarEnv subst tv of
-     Just tv' -> (env,  TvBndr tv' vis)
-     Nothing  -> tidyTyVarBinder env tvb
+     Just tv' -> (env,  Bndr tv' vis)
+     Nothing  -> tidyTyCoVarBinder env tvb
 
 tidyTyConBinders :: TidyEnv -> [TyConBinder] -> (TidyEnv, [TyConBinder])
 tidyTyConBinders = mapAccumL tidyTyConBinder
diff --git a/compiler/iface/TcIface.hs b/compiler/iface/TcIface.hs
index 0dc3fb5381..248f7d3c38 100644
--- a/compiler/iface/TcIface.hs
+++ b/compiler/iface/TcIface.hs
@@ -861,7 +861,7 @@ tc_ax_branch prev_branches
                             , ifaxbLHS = lhs, ifaxbRHS = rhs
                             , ifaxbRoles = roles, ifaxbIncomps = incomps })
   = bindIfaceTyConBinders_AT
-      (map (\b -> TvBndr b (NamedTCB Inferred)) tv_bndrs) $ \ tvs ->
+      (map (\b -> Bndr (IfaceTvBndr b) (NamedTCB Inferred)) tv_bndrs) $ \ tvs ->
          -- The _AT variant is needed here; see Note [CoAxBranch type variables] in CoAxiom
     bindIfaceIds cv_bndrs $ \ cvs -> do
     { tc_lhs <- tcIfaceAppArgs lhs
@@ -891,7 +891,7 @@ tcIfaceDataCons tycon_name tycon tc_tybinders if_cons
     tag_map = mkTyConTagMap tycon
 
     tc_con_decl (IfCon { ifConInfix = is_infix,
-                         ifConExTvs = ex_bndrs,
+                         ifConExTCvs = ex_bndrs,
                          ifConUserTvBinders = user_bndrs,
                          ifConName = dc_name,
                          ifConCtxt = ctxt, ifConEqSpec = spec,
@@ -900,7 +900,7 @@ tcIfaceDataCons tycon_name tycon tc_tybinders if_cons
                          ifConSrcStricts = if_src_stricts})
      = -- Universally-quantified tyvars are shared with
        -- parent TyCon, and are already in scope
-       bindIfaceTyVars ex_bndrs    $ \ ex_tvs -> do
+       bindIfaceBndrs ex_bndrs    $ \ ex_tvs -> do
         { traceIf (text "Start interface-file tc_con_decl" <+> ppr dc_name)
 
           -- By this point, we have bound every universal and existential
@@ -909,8 +909,12 @@ tcIfaceDataCons tycon_name tycon tc_tybinders if_cons
           -- ifConUserTvBinders has a matching counterpart somewhere in the
           -- bound universals/existentials. As a result, calling tcIfaceTyVar
           -- below is always guaranteed to succeed.
-        ; user_tv_bndrs <- mapM (\(TvBndr (name, _) vis) ->
-                                    TvBndr <$> tcIfaceTyVar name <*> pure vis)
+        ; user_tv_bndrs <- mapM (\(Bndr bd vis) ->
+                                   case bd of
+                                     IfaceIdBndr (name, _) ->
+                                       Bndr <$> tcIfaceLclId name <*> pure vis
+                                     IfaceTvBndr (name, _) ->
+                                       Bndr <$> tcIfaceTyVar name <*> pure vis)
                                 user_bndrs
 
         -- Read the context and argument types, but lazily for two reasons
@@ -936,7 +940,7 @@ tcIfaceDataCons tycon_name tycon tc_tybinders if_cons
 
         -- Remember, tycon is the representation tycon
         ; let orig_res_ty = mkFamilyTyConApp tycon
-                                (substTyVars (mkTvSubstPrs (map eqSpecPair eq_spec))
+                              (substTyCoVars (mkTvSubstPrs (map eqSpecPair eq_spec))
                                              (binderVars tc_tybinders))
 
         ; prom_rep_name <- newTyConRepName dc_name
@@ -1145,7 +1149,7 @@ tcIfaceType = go
            ; return (mkTyConApp tc' tks') }
     go (IfaceForAllTy bndr t)
       = bindIfaceForAllBndr bndr $ \ tv' vis ->
-        ForAllTy (TvBndr tv' vis) <$> go t
+        ForAllTy (Bndr tv' vis) <$> go t
     go (IfaceCastTy ty co)   = CastTy <$> go ty <*> tcIfaceCo co
     go (IfaceCoercionTy co)  = CoercionTy <$> tcIfaceCo co
 
@@ -1211,7 +1215,7 @@ tcIfaceCo = go
       = TyConAppCo r <$> tcIfaceTyCon tc <*> mapM go cs
     go (IfaceAppCo c1 c2)        = AppCo <$> go c1 <*> go c2
     go (IfaceForAllCo tv k c)  = do { k' <- go k
-                                      ; bindIfaceTyVar tv $ \ tv' ->
+                                      ; bindIfaceBndr tv $ \ tv' ->
                                         ForAllCo tv' k' <$> go c }
     go (IfaceCoVarCo n)          = CoVarCo <$> go_var n
     go (IfaceAxiomInstCo n i cs) = AxiomInstCo <$> tcIfaceCoAxiom n <*> pure i <*> mapM go cs
@@ -1745,23 +1749,18 @@ bindIfaceBndrs (b:bs) thing_inside
     thing_inside (b':bs')
 
 -----------------------
-bindIfaceForAllBndrs :: [IfaceForAllBndr] -> ([TyVarBinder] -> IfL a) -> IfL a
+bindIfaceForAllBndrs :: [IfaceForAllBndr] -> ([TyCoVarBinder] -> IfL a) -> IfL a
 bindIfaceForAllBndrs [] thing_inside = thing_inside []
 bindIfaceForAllBndrs (bndr:bndrs) thing_inside
   = bindIfaceForAllBndr bndr $ \tv vis ->
     bindIfaceForAllBndrs bndrs $ \bndrs' ->
-    thing_inside (mkTyVarBinder vis tv : bndrs')
+    thing_inside (mkTyCoVarBinder vis tv : bndrs')
 
-bindIfaceForAllBndr :: IfaceForAllBndr -> (TyVar -> ArgFlag -> IfL a) -> IfL a
-bindIfaceForAllBndr (TvBndr tv vis) thing_inside
+bindIfaceForAllBndr :: IfaceForAllBndr -> (TyCoVar -> ArgFlag -> IfL a) -> IfL a
+bindIfaceForAllBndr (Bndr (IfaceTvBndr tv) vis) thing_inside
   = bindIfaceTyVar tv $ \tv' -> thing_inside tv' vis
-
-bindIfaceTyVars :: [IfaceTvBndr] -> ([TyVar] -> IfL a) -> IfL a
-bindIfaceTyVars [] thing_inside = thing_inside []
-bindIfaceTyVars (tv:tvs) thing_inside
-  = bindIfaceTyVar tv   $ \tv' ->
-    bindIfaceTyVars tvs $ \tvs' ->
-    thing_inside (tv' : tvs')
+bindIfaceForAllBndr (Bndr (IfaceIdBndr tv) vis) thing_inside
+  = bindIfaceId tv $ \tv' -> thing_inside tv' vis
 
 bindIfaceTyVar :: IfaceTvBndr -> (TyVar -> IfL a) -> IfL a
 bindIfaceTyVar (occ,kind) thing_inside
@@ -1778,8 +1777,8 @@ bindIfaceTyConBinders :: [IfaceTyConBinder]
                       -> ([TyConBinder] -> IfL a) -> IfL a
 bindIfaceTyConBinders [] thing_inside = thing_inside []
 bindIfaceTyConBinders (b:bs) thing_inside
-  = bindIfaceTyConBinderX bindIfaceTyVar b $ \ b'  ->
-    bindIfaceTyConBinders bs               $ \ bs' ->
+  = bindIfaceTyConBinderX bindIfaceBndr b $ \ b'  ->
+    bindIfaceTyConBinders bs              $ \ bs' ->
     thing_inside (b':bs')
 
 bindIfaceTyConBinders_AT :: [IfaceTyConBinder]
@@ -1796,14 +1795,14 @@ bindIfaceTyConBinders_AT (b : bs) thing_inside
     thing_inside (b':bs')
   where
     bind_tv tv thing
-      = do { mb_tv <- lookupIfaceTyVar tv
+      = do { mb_tv <- lookupIfaceVar tv
            ; case mb_tv of
                Just b' -> thing b'
-               Nothing -> bindIfaceTyVar tv thing }
+               Nothing -> bindIfaceBndr tv thing }
 
-bindIfaceTyConBinderX :: (IfaceTvBndr -> (TyVar -> IfL a) -> IfL a)
+bindIfaceTyConBinderX :: (IfaceBndr -> (TyCoVar -> IfL a) -> IfL a)
                       -> IfaceTyConBinder
                       -> (TyConBinder -> IfL a) -> IfL a
-bindIfaceTyConBinderX bind_tv (TvBndr tv vis) thing_inside
+bindIfaceTyConBinderX bind_tv (Bndr tv vis) thing_inside
   = bind_tv tv $ \tv' ->
-    thing_inside (TvBndr tv' vis)
+    thing_inside (Bndr tv' vis)
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)
 
 {-
diff --git a/compiler/iface/ToIface.hs-boot b/compiler/iface/ToIface.hs-boot
index 46083f0414..e5f57ff9a3 100644
--- a/compiler/iface/ToIface.hs-boot
+++ b/compiler/iface/ToIface.hs-boot
@@ -3,14 +3,14 @@ module ToIface where
 import {-# SOURCE #-} TyCoRep
 import {-# SOURCE #-} IfaceType( IfaceType, IfaceTyCon, IfaceForAllBndr
                                , IfaceCoercion, IfaceTyLit, IfaceAppArgs )
-import Var ( TyVarBinder )
+import Var ( TyCoVarBinder )
 import TyCon ( TyCon )
 import VarSet( VarSet )
 
 -- For TyCoRep
 toIfaceTypeX :: VarSet -> Type -> IfaceType
 toIfaceTyLit :: TyLit -> IfaceTyLit
-toIfaceForAllBndr :: TyVarBinder -> IfaceForAllBndr
+toIfaceForAllBndr :: TyCoVarBinder -> IfaceForAllBndr
 toIfaceTyCon :: TyCon -> IfaceTyCon
 toIfaceTcArgs :: TyCon -> [Type] -> IfaceAppArgs
 toIfaceCoercionX :: VarSet -> Coercion -> IfaceCoercion