Add kind equalities to GHC.

This implements the ideas originally put forward in
"System FC with Explicit Kind Equality" (ICFP'13).

There are several noteworthy changes with this patch:
 * We now have casts in types. These change the kind
   of a type. See new constructor `CastTy`.

 * All types and all constructors can be promoted.
   This includes GADT constructors. GADT pattern matches
   take place in type family equations. In Core,
   types can now be applied to coercions via the
   `CoercionTy` constructor.

 * Coercions can now be heterogeneous, relating types
   of different kinds. A coercion proving `t1 :: k1 ~ t2 :: k2`
   proves both that `t1` and `t2` are the same and also that
   `k1` and `k2` are the same.

 * The `Coercion` type has been significantly enhanced.
   The documentation in `docs/core-spec/core-spec.pdf` reflects
   the new reality.

 * The type of `*` is now `*`. No more `BOX`.

 * Users can write explicit kind variables in their code,
   anywhere they can write type variables. For backward compatibility,
   automatic inference of kind-variable binding is still permitted.

 * The new extension `TypeInType` turns on the new user-facing
   features.

 * Type families and synonyms are now promoted to kinds. This causes
   trouble with parsing `*`, leading to the somewhat awkward new
   `HsAppsTy` constructor for `HsType`. This is dispatched with in
   the renamer, where the kind `*` can be told apart from a
   type-level multiplication operator. Without `-XTypeInType` the
   old behavior persists. With `-XTypeInType`, you need to import
   `Data.Kind` to get `*`, also known as `Type`.

 * The kind-checking algorithms in TcHsType have been significantly
   rewritten to allow for enhanced kinds.

 * The new features are still quite experimental and may be in flux.

 * TODO: Several open tickets: #11195, #11196, #11197, #11198, #11203.

 * TODO: Update user manual.

Tickets addressed: #9017, #9173, #7961, #10524, #8566, #11142.
Updates Haddock submodule.

1 files changed, 124 insertions, 79 deletions

diff --git a/compiler/iface/IfaceSyn.hs b/compiler/iface/IfaceSyn.hs
index 307a448ec9..247566cebc 100644
--- a/compiler/iface/IfaceSyn.hs
+++ b/compiler/iface/IfaceSyn.hs
@@ -94,14 +94,14 @@ data IfaceDecl
               ifIdDetails :: IfaceIdDetails,
               ifIdInfo    :: IfaceIdInfo }
 
-  | IfaceData { ifName       :: IfaceTopBndr,        -- Type constructor
+  | IfaceData { ifName       :: IfaceTopBndr,   -- Type constructor
+                ifKind       :: IfaceType,      -- Kind of type constructor
                 ifCType      :: Maybe CType,    -- C type for CAPI FFI
                 ifTyVars     :: [IfaceTvBndr],  -- Type variables
                 ifRoles      :: [Role],         -- Roles
                 ifCtxt       :: IfaceContext,   -- The "stupid theta"
                 ifCons       :: IfaceConDecls,  -- Includes new/data/data family info
                 ifRec        :: RecFlag,        -- Recursive or not?
-                ifPromotable :: Bool,           -- Promotable to kind level?
                 ifGadtSyntax :: Bool,           -- True <=> declared using
                                                 -- GADT syntax
                 ifParent     :: IfaceTyConParent -- The axiom, for a newtype,
@@ -111,8 +111,7 @@ data IfaceDecl
   | IfaceSynonym { ifName    :: IfaceTopBndr,      -- Type constructor
                    ifTyVars  :: [IfaceTvBndr],     -- Type variables
                    ifRoles   :: [Role],            -- Roles
-                   ifSynKind :: IfaceKind,         -- Kind of the *rhs* (not of
-                                                   -- the tycon)
+                   ifSynKind :: IfaceKind,         -- Kind of the *tycon*
                    ifSynRhs  :: IfaceType }
 
   | IfaceFamily  { ifName    :: IfaceTopBndr,      -- Type constructor
@@ -120,8 +119,7 @@ data IfaceDecl
                    ifResVar  :: Maybe IfLclName,   -- Result variable name, used
                                                    -- only for pretty-printing
                                                    -- with --show-iface
-                   ifFamKind :: IfaceKind,         -- Kind of the *rhs* (not of
-                                                   -- the tycon)
+                   ifFamKind :: IfaceKind,         -- Kind of the *tycon*
                    ifFamFlav :: IfaceFamTyConFlav,
                    ifFamInj  :: Injectivity }      -- injectivity information
 
@@ -129,6 +127,7 @@ data IfaceDecl
                  ifName    :: IfaceTopBndr,             -- Name of the class TyCon
                  ifTyVars  :: [IfaceTvBndr],            -- Type variables
                  ifRoles   :: [Role],                   -- Roles
+                 ifKind    :: IfaceType,                -- Kind of TyCon
                  ifFDs     :: [FunDep FastString],      -- Functional dependencies
                  ifATs     :: [IfaceAT],                -- Associated type families
                  ifSigs    :: [IfaceClassOp],           -- Method signatures
@@ -187,11 +186,12 @@ data IfaceAT = IfaceAT  -- See Class.ClassATItem
 
 
 -- This is just like CoAxBranch
-data IfaceAxBranch = IfaceAxBranch { ifaxbTyVars  :: [IfaceTvBndr]
-                                   , ifaxbLHS     :: IfaceTcArgs
-                                   , ifaxbRoles   :: [Role]
-                                   , ifaxbRHS     :: IfaceType
-                                   , ifaxbIncomps :: [BranchIndex] }
+data IfaceAxBranch = IfaceAxBranch { ifaxbTyVars   :: [IfaceTvBndr]
+                                   , ifaxbCoVars   :: [IfaceIdBndr]
+                                   , ifaxbLHS      :: IfaceTcArgs
+                                   , ifaxbRoles    :: [Role]
+                                   , ifaxbRHS      :: IfaceType
+                                   , ifaxbIncomps  :: [BranchIndex] }
                                      -- See Note [Storing compatibility] in CoAxiom
 
 data IfaceConDecls
@@ -511,14 +511,20 @@ pprAxBranch :: SDoc -> IfaceAxBranch -> SDoc
 -- be a branch for an imported TyCon, so it would be an ExtName
 -- So it's easier to take an SDoc here
 pprAxBranch pp_tc (IfaceAxBranch { ifaxbTyVars = tvs
-                                  , ifaxbLHS = pat_tys
-                                  , ifaxbRHS = rhs
-                                  , ifaxbIncomps = incomps })
-  = hang (pprUserIfaceForAll tvs)
-       2 (hang pp_lhs 2 (equals <+> ppr rhs))
+                                 , ifaxbCoVars = cvs
+                                 , ifaxbLHS = pat_tys
+                                 , ifaxbRHS = rhs
+                                 , ifaxbIncomps = incomps })
+  = hang ppr_binders 2 (hang pp_lhs 2 (equals <+> ppr rhs))
     $+$
     nest 2 maybe_incomps
   where
+    ppr_binders
+      | null tvs && null cvs = empty
+      | null cvs             = brackets (pprWithCommas pprIfaceTvBndr tvs)
+      | otherwise
+      = brackets (pprWithCommas pprIfaceTvBndr tvs <> semi <+>
+                  pprWithCommas pprIfaceIdBndr cvs)
     pp_lhs = hang pp_tc 2 (pprParendIfaceTcArgs pat_tys)
     maybe_incomps = ppUnless (null incomps) $ parens $
                     ptext (sLit "incompatible indices:") <+> ppr incomps
@@ -617,7 +623,7 @@ pprIfaceDecl ss (IfaceData { ifName = tycon, ifCType = ctype,
                              ifRoles = roles, ifCons = condecls,
                              ifParent = parent, ifRec = isrec,
                              ifGadtSyntax = gadt,
-                             ifPromotable = is_prom })
+                             ifKind = kind })
 
   | gadt_style = vcat [ pp_roles
                       , pp_nd <+> pp_lhs <+> pp_where
@@ -635,13 +641,14 @@ pprIfaceDecl ss (IfaceData { ifName = tycon, ifCType = ctype,
     pp_cons    = ppr_trim (map show_con cons) :: [SDoc]
 
     pp_lhs = case parent of
-               IfNoParent -> pprIfaceDeclHead context ss tycon tc_tyvars
+               IfNoParent -> pprIfaceDeclHead context ss tycon kind tc_tyvars
                _          -> ptext (sLit "instance") <+> pprIfaceTyConParent parent
 
     pp_roles
-      | is_data_instance = Outputable.empty
-      | otherwise        = pprRoles (== Representational) (pprPrefixIfDeclBndr ss tycon)
-                                    tc_tyvars roles
+      | is_data_instance = empty
+      | otherwise        = pprRoles (== Representational)
+                                    (pprPrefixIfDeclBndr ss tycon)
+                                    tc_bndrs roles
             -- Don't display roles for data family instances (yet)
             -- See discussion on Trac #8672.
 
@@ -670,29 +677,31 @@ pprIfaceDecl ss (IfaceData { ifName = tycon, ifCType = ctype,
     ppr_tc_app gadt_subst dflags
        = pprPrefixIfDeclBndr ss tycon
          <+> sep [ pprParendIfaceType (substIfaceTyVar gadt_subst tv)
-                 | (tv,_kind) <- stripIfaceKindVars dflags tc_tyvars ]
+                 | (tv,_kind)
+                     <- suppressIfaceInvisibles dflags tc_bndrs tc_tyvars ]
+    (tc_bndrs, _, _) = splitIfaceSigmaTy kind
 
     pp_nd = case condecls of
               IfAbstractTyCon d -> ptext (sLit "abstract") <> ppShowIface ss (parens (ppr d))
               IfDataTyCon{}     -> ptext (sLit "data")
               IfNewTyCon{}      -> ptext (sLit "newtype")
 
-    pp_extra = vcat [pprCType ctype, pprRec isrec, pp_prom]
-
-    pp_prom | is_prom   = ptext (sLit "Promotable")
-            | otherwise = Outputable.empty
+    pp_extra = vcat [pprCType ctype, pprRec isrec, text "Kind:" <+> ppr kind]
 
 
 pprIfaceDecl ss (IfaceClass { ifATs = ats, ifSigs = sigs, ifRec = isrec
                             , ifCtxt   = context, ifName  = clas
                             , ifTyVars = tyvars,  ifRoles = roles
-                            , ifFDs    = fds, ifMinDef = minDef })
-  = vcat [ pprRoles (== Nominal) (pprPrefixIfDeclBndr ss clas) tyvars roles
-         , ptext (sLit "class") <+> pprIfaceDeclHead context ss clas tyvars
+                            , ifFDs    = fds, ifMinDef = minDef
+                            , ifKind   = kind })
+  = vcat [ pprRoles (== Nominal) (pprPrefixIfDeclBndr ss clas) bndrs roles
+         , ptext (sLit "class") <+> pprIfaceDeclHead context ss clas kind tyvars
                                 <+> pprFundeps fds <+> pp_where
          , nest 2 (vcat [ vcat asocs, vcat dsigs, pprec
                         , ppShowAllSubs ss (pprMinDef minDef)])]
     where
+      (bndrs, _, _) = splitIfaceSigmaTy kind
+
       pp_where = ppShowRhs ss $ ppUnless (null sigs && null ats) (ptext (sLit "where"))
 
       asocs = ppr_trim $ map maybeShowAssoc ats
@@ -716,10 +725,11 @@ pprIfaceDecl ss (IfaceClass { ifATs = ats, ifSigs = sigs, ifRec = isrec
           (\_ def -> cparen (isLexSym def) (ppr def)) 0 minDef <+>
         ptext (sLit "#-}")
 
-pprIfaceDecl ss (IfaceSynonym { ifName   = tc
-                              , ifTyVars = tv
-                              , ifSynRhs = mono_ty })
-  = hang (ptext (sLit "type") <+> pprIfaceDeclHead [] ss tc tv <+> equals)
+pprIfaceDecl ss (IfaceSynonym { ifName    = tc
+                              , ifTyVars  = tv
+                              , ifSynRhs  = mono_ty
+                              , ifSynKind = kind})
+  = hang (ptext (sLit "type") <+> pprIfaceDeclHead [] ss tc kind tv <+> equals)
        2 (sep [pprIfaceForAll tvs, pprIfaceContextArr theta, ppr tau])
   where
     (tvs, theta, tau) = splitIfaceSigmaTy mono_ty
@@ -728,19 +738,20 @@ pprIfaceDecl ss (IfaceFamily { ifName = tycon, ifTyVars = tyvars
                              , ifFamFlav = rhs, ifFamKind = kind
                              , ifResVar = res_var, ifFamInj = inj })
   | IfaceDataFamilyTyCon <- rhs
-  = ptext (sLit "data family") <+> pprIfaceDeclHead [] ss tycon tyvars
+  = ptext (sLit "data family") <+> pprIfaceDeclHead [] ss tycon kind tyvars
 
   | otherwise
-  = vcat [ hang (ptext (sLit "type family")
-                 <+> pprIfaceDeclHead [] ss tycon tyvars)
-              2 (pp_inj res_var inj <+> ppShowRhs ss (pp_rhs rhs))
-         , ppShowRhs ss (nest 2 (pp_branches rhs)) ]
+  = hang (text "type family" <+> pprIfaceDeclHead [] ss tycon kind tyvars)
+       2 (pp_inj res_var inj <+> ppShowRhs ss (pp_rhs rhs))
+    $$
+    nest 2 ( vcat [ text "Kind:" <+> ppr kind
+                  , ppShowRhs ss (pp_branches rhs) ] )
   where
-    pp_inj Nothing    _   = dcolon <+> ppr kind
+    pp_inj Nothing    _   = empty
     pp_inj (Just res) inj
-       | Injective injectivity <- inj = hsep [ equals, ppr res, dcolon, ppr kind
+       | Injective injectivity <- inj = hsep [ equals, ppr res
                                              , pp_inj_cond res injectivity]
-       | otherwise = hsep [ equals, ppr res, dcolon, ppr kind ]
+       | otherwise = hsep [ equals, ppr res ]
 
     pp_inj_cond res inj = case filterByList inj tyvars of
        []  -> empty
@@ -753,13 +764,14 @@ pprIfaceDecl ss (IfaceFamily { ifName = tycon, ifTyVars = tyvars
     pp_rhs IfaceAbstractClosedSynFamilyTyCon
       = ppShowIface ss (ptext (sLit "closed, abstract"))
     pp_rhs (IfaceClosedSynFamilyTyCon {})
-      = ptext (sLit "where")
+      = empty  -- see pp_branches
     pp_rhs IfaceBuiltInSynFamTyCon
       = ppShowIface ss (ptext (sLit "built-in"))
 
     pp_branches (IfaceClosedSynFamilyTyCon (Just (ax, brs)))
-      = vcat (map (pprAxBranch (pprPrefixIfDeclBndr ss tycon)) brs)
-        $$ ppShowIface ss (ptext (sLit "axiom") <+> ppr ax)
+      = hang (text "where")
+           2 (vcat (map (pprAxBranch (pprPrefixIfDeclBndr ss tycon)) brs)
+              $$ ppShowIface ss (ptext (sLit "axiom") <+> ppr ax))
     pp_branches _ = Outputable.empty
 
 pprIfaceDecl _ (IfacePatSyn { ifName = name, ifPatBuilder = builder,
@@ -768,7 +780,7 @@ pprIfaceDecl _ (IfacePatSyn { ifName = name, ifPatBuilder = builder,
                               ifPatArgs = arg_tys,
                               ifPatTy = pat_ty} )
   = pprPatSynSig name is_bidirectional
-                 (pprUserIfaceForAll tvs)
+                 (pprUserIfaceForAll (map tv_to_forall_bndr tvs))
                  (pprIfaceContextMaybe req_ctxt)
                  (pprIfaceContextMaybe prov_ctxt)
                  (pprIfaceType ty)
@@ -796,10 +808,11 @@ pprCType (Just cType) = ptext (sLit "C type:") <+> ppr cType
 
 -- if, for each role, suppress_if role is True, then suppress the role
 -- output
-pprRoles :: (Role -> Bool) -> SDoc -> [IfaceTvBndr] -> [Role] -> SDoc
-pprRoles suppress_if tyCon tyvars roles
+pprRoles :: (Role -> Bool) -> SDoc -> [IfaceForAllBndr]
+         -> [Role] -> SDoc
+pprRoles suppress_if tyCon bndrs roles
   = sdocWithDynFlags $ \dflags ->
-      let froles = suppressIfaceKinds dflags tyvars roles
+      let froles = suppressIfaceInvisibles dflags bndrs roles
       in ppUnless (all suppress_if roles || null froles) $
          ptext (sLit "type role") <+> tyCon <+> hsep (map ppr froles)
 
@@ -845,15 +858,19 @@ pprIfaceTyConParent IfNoParent
   = Outputable.empty
 pprIfaceTyConParent (IfDataInstance _ tc tys)
   = sdocWithDynFlags $ \dflags ->
-    let ftys = stripKindArgs dflags tys
+    let ftys = stripInvisArgs dflags tys
     in pprIfaceTypeApp tc ftys
 
-pprIfaceDeclHead :: IfaceContext -> ShowSub -> OccName -> [IfaceTvBndr] -> SDoc
-pprIfaceDeclHead context ss tc_occ tv_bndrs
+pprIfaceDeclHead :: IfaceContext -> ShowSub -> OccName
+                 -> IfaceType   -- of the tycon, for invisible-suppression
+                 -> [IfaceTvBndr] -> SDoc
+pprIfaceDeclHead context ss tc_occ kind tyvars
   = sdocWithDynFlags $ \ dflags ->
     sep [ pprIfaceContextArr context
         , pprPrefixIfDeclBndr ss tc_occ
-          <+> pprIfaceTvBndrs (stripIfaceKindVars dflags tv_bndrs) ]
+          <+> pprIfaceTvBndrs (suppressIfaceInvisibles dflags bndrs tyvars) ]
+  where
+    (bndrs, _, _) = splitIfaceSigmaTy kind
 
 isVanillaIfaceConDecl :: IfaceConDecl -> Bool
 isVanillaIfaceConDecl (IfCon { ifConExTvs  = ex_tvs
@@ -881,7 +898,8 @@ pprIfaceConDecl ss gadt_style mk_user_con_res_ty fls
     pp_prefix_con = pprPrefixIfDeclBndr ss name
 
     (univ_tvs, pp_res_ty) = mk_user_con_res_ty eq_spec
-    ppr_ty = pprIfaceForAllPart (univ_tvs ++ ex_tvs) ctxt pp_tau
+    ppr_ty = pprIfaceForAllPart (map tv_to_forall_bndr (univ_tvs ++ ex_tvs))
+                                ctxt pp_tau
 
         -- A bit gruesome this, but we can't form the full con_tau, and ppr it,
         -- because we don't have a Name for the tycon, only an OccName
@@ -944,6 +962,9 @@ ppr_rough :: Maybe IfaceTyCon -> SDoc
 ppr_rough Nothing   = dot
 ppr_rough (Just tc) = ppr tc
 
+tv_to_forall_bndr :: IfaceTvBndr -> IfaceForAllBndr
+tv_to_forall_bndr tv = IfaceTv tv Invisible
+
 {-
 Note [Result type of a data family GADT]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1128,6 +1149,7 @@ freeNamesIfDecl (IfaceId _s t d i) =
   freeNamesIfIdInfo i &&&
   freeNamesIfIdDetails d
 freeNamesIfDecl d@IfaceData{} =
+  freeNamesIfType (ifKind d) &&&
   freeNamesIfTvBndrs (ifTyVars d) &&&
   freeNamesIfaceTyConParent (ifParent d) &&&
   freeNamesIfContext (ifCtxt d) &&&
@@ -1135,16 +1157,15 @@ freeNamesIfDecl d@IfaceData{} =
 freeNamesIfDecl d@IfaceSynonym{} =
   freeNamesIfTvBndrs (ifTyVars d) &&&
   freeNamesIfType (ifSynRhs d) &&&
-  freeNamesIfKind (ifSynKind d) -- IA0_NOTE: because of promotion, we
-                                -- return names in the kind signature
+  freeNamesIfKind (ifSynKind d)
 freeNamesIfDecl d@IfaceFamily{} =
   freeNamesIfTvBndrs (ifTyVars d) &&&
   freeNamesIfFamFlav (ifFamFlav d) &&&
-  freeNamesIfKind (ifFamKind d) -- IA0_NOTE: because of promotion, we
-                                -- return names in the kind signature
+  freeNamesIfKind (ifFamKind d)
 freeNamesIfDecl d@IfaceClass{} =
   freeNamesIfTvBndrs (ifTyVars d) &&&
   freeNamesIfContext (ifCtxt d) &&&
+  freeNamesIfType (ifKind d) &&&
   fnList freeNamesIfAT     (ifATs d) &&&
   fnList freeNamesIfClsSig (ifSigs d)
 freeNamesIfDecl d@IfaceAxiom{} =
@@ -1162,10 +1183,12 @@ freeNamesIfDecl d@IfacePatSyn{} =
   mkNameSet (map flSelector (ifFieldLabels d))
 
 freeNamesIfAxBranch :: IfaceAxBranch -> NameSet
-freeNamesIfAxBranch (IfaceAxBranch { ifaxbTyVars = tyvars
-                                   , ifaxbLHS    = lhs
-                                   , ifaxbRHS    = rhs }) =
+freeNamesIfAxBranch (IfaceAxBranch { ifaxbTyVars   = tyvars
+                                   , ifaxbCoVars   = covars
+                                   , ifaxbLHS      = lhs
+                                   , ifaxbRHS      = rhs }) =
   freeNamesIfTvBndrs tyvars &&&
+  fnList freeNamesIfIdBndr covars &&&
   freeNamesIfTcArgs lhs &&&
   freeNamesIfType rhs
 
@@ -1217,9 +1240,9 @@ freeNamesIfKind :: IfaceType -> NameSet
 freeNamesIfKind = freeNamesIfType
 
 freeNamesIfTcArgs :: IfaceTcArgs -> NameSet
-freeNamesIfTcArgs (ITC_Type t ts) = freeNamesIfType t &&& freeNamesIfTcArgs ts
-freeNamesIfTcArgs (ITC_Kind k ks) = freeNamesIfKind k &&& freeNamesIfTcArgs ks
-freeNamesIfTcArgs ITC_Nil         = emptyNameSet
+freeNamesIfTcArgs (ITC_Vis   t ts) = freeNamesIfType t &&& freeNamesIfTcArgs ts
+freeNamesIfTcArgs (ITC_Invis k ks) = freeNamesIfKind k &&& freeNamesIfTcArgs ks
+freeNamesIfTcArgs ITC_Nil          = emptyNameSet
 
 freeNamesIfType :: IfaceType -> NameSet
 freeNamesIfType (IfaceTyVar _)        = emptyNameSet
@@ -1227,9 +1250,12 @@ freeNamesIfType (IfaceAppTy s t)      = freeNamesIfType s &&& freeNamesIfType t
 freeNamesIfType (IfaceTyConApp tc ts) = freeNamesIfTc tc &&& freeNamesIfTcArgs ts
 freeNamesIfType (IfaceTupleTy _ _ ts) = freeNamesIfTcArgs ts
 freeNamesIfType (IfaceLitTy _)        = emptyNameSet
-freeNamesIfType (IfaceForAllTy tv t)  = freeNamesIfTvBndr tv &&& freeNamesIfType t
+freeNamesIfType (IfaceForAllTy tv t)  =
+   freeNamesIfForAllBndr 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
+freeNamesIfType (IfaceCoercionTy c)   = freeNamesIfCoercion c
 
 freeNamesIfCoercion :: IfaceCoercion -> NameSet
 freeNamesIfCoercion (IfaceReflCo _ t) = freeNamesIfType t
@@ -1239,14 +1265,14 @@ freeNamesIfCoercion (IfaceTyConAppCo _ tc cos)
   = freeNamesIfTc tc &&& fnList freeNamesIfCoercion cos
 freeNamesIfCoercion (IfaceAppCo c1 c2)
   = freeNamesIfCoercion c1 &&& freeNamesIfCoercion c2
-freeNamesIfCoercion (IfaceForAllCo tv co)
-  = freeNamesIfTvBndr tv &&& freeNamesIfCoercion co
+freeNamesIfCoercion (IfaceForAllCo _ kind_co co)
+  = freeNamesIfCoercion kind_co &&& freeNamesIfCoercion co
 freeNamesIfCoercion (IfaceCoVarCo _)
   = emptyNameSet
 freeNamesIfCoercion (IfaceAxiomInstCo ax _ cos)
   = unitNameSet ax &&& fnList freeNamesIfCoercion cos
-freeNamesIfCoercion (IfaceUnivCo _ _ t1 t2)
-  = freeNamesIfType t1 &&& freeNamesIfType t2
+freeNamesIfCoercion (IfaceUnivCo p _ t1 t2)
+  = freeNamesIfProv p &&& freeNamesIfType t1 &&& freeNamesIfType t2
 freeNamesIfCoercion (IfaceSymCo c)
   = freeNamesIfCoercion c
 freeNamesIfCoercion (IfaceTransCo c1 c2)
@@ -1255,22 +1281,37 @@ freeNamesIfCoercion (IfaceNthCo _ co)
   = freeNamesIfCoercion co
 freeNamesIfCoercion (IfaceLRCo _ co)
   = freeNamesIfCoercion co
-freeNamesIfCoercion (IfaceInstCo co ty)
-  = freeNamesIfCoercion co &&& freeNamesIfType ty
+freeNamesIfCoercion (IfaceInstCo co co2)
+  = freeNamesIfCoercion co &&& freeNamesIfCoercion co2
+freeNamesIfCoercion (IfaceCoherenceCo c1 c2)
+  = freeNamesIfCoercion c1 &&& freeNamesIfCoercion c2
+freeNamesIfCoercion (IfaceKindCo c)
+  = freeNamesIfCoercion c
 freeNamesIfCoercion (IfaceSubCo co)
   = freeNamesIfCoercion co
-freeNamesIfCoercion (IfaceAxiomRuleCo _ax tys cos)
+freeNamesIfCoercion (IfaceAxiomRuleCo _ax cos)
   -- the axiom is just a string, so we don't count it as a name.
-  = fnList freeNamesIfType tys &&&
-    fnList freeNamesIfCoercion cos
+  = fnList freeNamesIfCoercion cos
+
+freeNamesIfProv :: IfaceUnivCoProv -> NameSet
+freeNamesIfProv IfaceUnsafeCoerceProv    = emptyNameSet
+freeNamesIfProv (IfacePhantomProv co)    = freeNamesIfCoercion co
+freeNamesIfProv (IfaceProofIrrelProv co) = freeNamesIfCoercion co
+freeNamesIfProv (IfacePluginProv _)      = emptyNameSet
 
 freeNamesIfTvBndrs :: [IfaceTvBndr] -> NameSet
 freeNamesIfTvBndrs = fnList freeNamesIfTvBndr
 
+freeNamesIfForAllBndr :: IfaceForAllBndr -> NameSet
+freeNamesIfForAllBndr (IfaceTv tv _) = freeNamesIfTvBndr tv
+
 freeNamesIfBndr :: IfaceBndr -> NameSet
 freeNamesIfBndr (IfaceIdBndr b) = freeNamesIfIdBndr b
 freeNamesIfBndr (IfaceTvBndr b) = freeNamesIfTvBndr b
 
+freeNamesIfBndrs :: [IfaceBndr] -> NameSet
+freeNamesIfBndrs = fnList freeNamesIfBndr
+
 freeNamesIfLetBndr :: IfaceLetBndr -> NameSet
 -- Remember IfaceLetBndr is used only for *nested* bindings
 -- The IdInfo can contain an unfolding (in the case of
@@ -1283,7 +1324,7 @@ freeNamesIfTvBndr (_fs,k) = freeNamesIfKind k
     -- kinds can have Names inside, because of promotion
 
 freeNamesIfIdBndr :: IfaceIdBndr -> NameSet
-freeNamesIfIdBndr = freeNamesIfTvBndr
+freeNamesIfIdBndr (_fs,k) = freeNamesIfKind k
 
 freeNamesIfIdInfo :: IfaceIdInfo -> NameSet
 freeNamesIfIdInfo NoInfo      = emptyNameSet
@@ -1297,7 +1338,7 @@ freeNamesIfUnfold :: IfaceUnfolding -> NameSet
 freeNamesIfUnfold (IfCoreUnfold _ e)     = freeNamesIfExpr e
 freeNamesIfUnfold (IfCompulsory e)       = freeNamesIfExpr e
 freeNamesIfUnfold (IfInlineRule _ _ _ e) = freeNamesIfExpr e
-freeNamesIfUnfold (IfDFunUnfold bs es)   = fnList freeNamesIfBndr bs &&& fnList freeNamesIfExpr es
+freeNamesIfUnfold (IfDFunUnfold bs es)   = freeNamesIfBndrs bs &&& fnList freeNamesIfExpr es
 
 freeNamesIfExpr :: IfaceExpr -> NameSet
 freeNamesIfExpr (IfaceExt v)          = unitNameSet v
@@ -1434,7 +1475,7 @@ instance Binary IfaceDecl where
         put_ bh a5
         put_ bh a6
 
-    put_ bh (IfaceClass a1 a2 a3 a4 a5 a6 a7 a8 a9) = do
+    put_ bh (IfaceClass a1 a2 a3 a4 a5 a6 a7 a8 a9 a10) = do
         putByte bh 5
         put_ bh a1
         put_ bh (occNameFS a2)
@@ -1445,6 +1486,7 @@ instance Binary IfaceDecl where
         put_ bh a7
         put_ bh a8
         put_ bh a9
+        put_ bh a10
 
     put_ bh (IfaceAxiom a1 a2 a3 a4) = do
         putByte bh 6
@@ -1513,8 +1555,9 @@ instance Binary IfaceDecl where
                     a7 <- get bh
                     a8 <- get bh
                     a9 <- get bh
+                    a10 <- get bh
                     occ <- return $! mkClsOccFS a2
-                    return (IfaceClass a1 occ a3 a4 a5 a6 a7 a8 a9)
+                    return (IfaceClass a1 occ a3 a4 a5 a6 a7 a8 a9 a10)
             6 -> do a1 <- get bh
                     a2 <- get bh
                     a3 <- get bh
@@ -1576,19 +1619,21 @@ instance Binary IfaceAT where
         return (IfaceAT dec defs)
 
 instance Binary IfaceAxBranch where
-    put_ bh (IfaceAxBranch a1 a2 a3 a4 a5) = do
+    put_ bh (IfaceAxBranch a1 a2 a3 a4 a5 a6) = do
         put_ bh a1
         put_ bh a2
         put_ bh a3
         put_ bh a4
         put_ bh a5
+        put_ bh a6
     get bh = do
         a1 <- get bh
         a2 <- get bh
         a3 <- get bh
         a4 <- get bh
         a5 <- get bh
-        return (IfaceAxBranch a1 a2 a3 a4 a5)
+        a6 <- get bh
+        return (IfaceAxBranch a1 a2 a3 a4 a5 a6)
 
 instance Binary IfaceConDecls where
     put_ bh (IfAbstractTyCon d)   = putByte bh 0 >> put_ bh d