things seem to now all fit! (may need to add some extra wiring)

21 files changed, 275 insertions, 85 deletions

diff --git a/compiler/backpack/RnModIface.hs b/compiler/backpack/RnModIface.hs
index 3da30de..2693b97 100644
--- a/compiler/backpack/RnModIface.hs
+++ b/compiler/backpack/RnModIface.hs
@@ -702,8 +702,8 @@ rnIfaceCo (IfaceSubCo c) = IfaceSubCo <$> rnIfaceCo c
 rnIfaceCo (IfaceAxiomRuleCo ax cos)
     = IfaceAxiomRuleCo ax <$> mapM rnIfaceCo cos
 rnIfaceCo (IfaceKindCo c) = IfaceKindCo <$> rnIfaceCo c
-rnIfaceCo (IfaceErased role lty rty)
-    = IfaceErased role <$>  rnIfaceType lty <*> rnIfaceType rty
+rnIfaceCo (IfaceErased as bs cs  role lty rty)
+    = IfaceErased as bs cs role <$>  rnIfaceType lty <*> rnIfaceType rty
 
 rnIfaceTyCon :: Rename IfaceTyCon
 rnIfaceTyCon (IfaceTyCon n info)
diff --git a/compiler/basicTypes/IdInfo.hs b/compiler/basicTypes/IdInfo.hs
index dea309d..aee8a8b 100644
--- a/compiler/basicTypes/IdInfo.hs
+++ b/compiler/basicTypes/IdInfo.hs
@@ -14,7 +14,7 @@ Haskell. [WDP 94/11])
 module IdInfo (
         -- * The IdDetails type
         IdDetails(..), pprIdDetails, coVarDetails, isCoVarDetails,
-        JoinArity, isJoinIdDetails_maybe,
+        JoinArity, isJoinIdDetails_maybe, isCoercionHoleDetails,
         RecSelParent(..),
 
         -- * The IdInfo type
@@ -159,6 +159,11 @@ data IdDetails
   | CoVarId    -- ^ A coercion variable
                -- This only covers /un-lifted/ coercions, of type
                -- (t1 ~# t2) or (t1 ~R# t2), not their lifted variants
+  | CoercionHoleId  -- ^ A variable introduced for tracking the scoping of
+                    -- a coercion hole during typechecking. See
+                    -- Note [Coercion holes] in TyCoRep.
+                    -- cribbed from bgamari wip/zap-coercions
+
   | JoinId JoinArity           -- ^ An 'Id' for a join point taking n arguments
        -- Note [Join points] in CoreSyn
 
@@ -184,6 +189,11 @@ isCoVarDetails :: IdDetails -> Bool
 isCoVarDetails CoVarId = True
 isCoVarDetails _       = False
 
+-- | Check if an 'IdDetails' says 'CoercionHoleId'.
+isCoercionHoleDetails :: IdDetails -> Bool
+isCoercionHoleDetails CoercionHoleId = True
+isCoercionHoleDetails _              = False
+
 isJoinIdDetails_maybe :: IdDetails -> Maybe JoinArity
 isJoinIdDetails_maybe (JoinId join_arity) = Just join_arity
 isJoinIdDetails_maybe _                   = Nothing
diff --git a/compiler/basicTypes/IdInfo.hs-boot b/compiler/basicTypes/IdInfo.hs-boot
index cacfe6a..533baff 100644
--- a/compiler/basicTypes/IdInfo.hs-boot
+++ b/compiler/basicTypes/IdInfo.hs-boot
@@ -8,4 +8,4 @@ vanillaIdInfo :: IdInfo
 coVarDetails :: IdDetails
 isCoVarDetails :: IdDetails -> Bool
 pprIdDetails :: IdDetails -> SDoc
-
+isCoercionHoleDetails :: IdDetails -> Bool
diff --git a/compiler/basicTypes/Var.hs b/compiler/basicTypes/Var.hs
index f5142ca..745aadc 100644
--- a/compiler/basicTypes/Var.hs
+++ b/compiler/basicTypes/Var.hs
@@ -58,7 +58,7 @@ module Var (
         isId, isTyVar, isTcTyVar,
         isLocalVar, isLocalId, isCoVar, isNonCoVarId, isTyCoVar,
         isGlobalId, isExportedId,
-        mustHaveLocalBinding,
+        mustHaveLocalBinding, isCoercionHole,
 
         -- * ArgFlags
         ArgFlag(..), isVisibleArgFlag, isInvisibleArgFlag, sameVis,
@@ -93,7 +93,7 @@ import {-# SOURCE #-}   TyCoRep( Type, Kind )
 import {-# SOURCE #-}   TyCoPpr( pprKind )
 import {-# SOURCE #-}   TcType( TcTyVarDetails, pprTcTyVarDetails, vanillaSkolemTv )
 import {-# SOURCE #-}   IdInfo( IdDetails, IdInfo, coVarDetails, isCoVarDetails,
-                                vanillaIdInfo, pprIdDetails )
+                                vanillaIdInfo, pprIdDetails,isCoercionHoleDetails )
 
 import Name hiding (varName)
 import Unique ( Uniquable, Unique, getKey, getUnique
@@ -760,3 +760,10 @@ isExportedId :: Var -> Bool
 isExportedId (Id { idScope = GlobalId })        = True
 isExportedId (Id { idScope = LocalId Exported}) = True
 isExportedId _ = False
+
+
+-- | Is this a CoercionHoleId? See Note [Coercion holes] in TyCoRep.
+--- copied from wip/zap-coercions
+isCoercionHole :: Var -> Bool
+isCoercionHole (Id { id_details = details }) = isCoercionHoleDetails details
+isCoercionHole _                             = False
diff --git a/compiler/coreSyn/CoreFVs.hs b/compiler/coreSyn/CoreFVs.hs
index 36fcfef..d2fc160 100644
--- a/compiler/coreSyn/CoreFVs.hs
+++ b/compiler/coreSyn/CoreFVs.hs
@@ -372,8 +372,8 @@ orphNamesOfMCo MRefl    = emptyNameSet
 orphNamesOfMCo (MCo co) = orphNamesOfCo co
 
 orphNamesOfCo :: Coercion -> NameSet
-orphNamesOfCo (ErasedCoercion _r lty rty )
-                                     = orphNamesOfType lty `unionNameSet`  orphNamesOfType rty
+orphNamesOfCo (ErasedCoercion vs  _r lty rty )
+                                    = orphNamesOfType lty `unionNameSet`  orphNamesOfType rty
 orphNamesOfCo (Refl ty)             = orphNamesOfType ty
 orphNamesOfCo (GRefl _ ty mco)      = orphNamesOfType ty `unionNameSet` orphNamesOfMCo mco
 orphNamesOfCo (TyConAppCo _ tc cos) = unitNameSet (getName tc) `unionNameSet` orphNamesOfCos cos
diff --git a/compiler/coreSyn/CoreLint.hs b/compiler/coreSyn/CoreLint.hs
index 7458003..8d1eb68 100644
--- a/compiler/coreSyn/CoreLint.hs
+++ b/compiler/coreSyn/CoreLint.hs
@@ -1689,9 +1689,10 @@ lintCoercion :: OutCoercion -> LintM (LintedKind, LintedKind, LintedType, Linted
 
 -- If you edit this function, you may need to update the GHC formalism
 -- See Note [GHC Formalism]
-lintCoercion (ErasedCoercion role lty rty)
+lintCoercion (ErasedCoercion fvs role lty rty)
   = do { kl <- lintType lty ;
          kr <- lintType rty ;
+         mapM_ lintTyCoVarInScope (dVarSetElems fvs);
          return (kl,kr,lty,rty,role)
        }
 lintCoercion (Refl ty)
diff --git a/compiler/iface/IfaceSyn.hs b/compiler/iface/IfaceSyn.hs
index 0859ef5..575174b 100644
--- a/compiler/iface/IfaceSyn.hs
+++ b/compiler/iface/IfaceSyn.hs
@@ -1578,7 +1578,7 @@ freeNamesIfMCoercion IfaceMRefl    = emptyNameSet
 freeNamesIfMCoercion (IfaceMCo co) = freeNamesIfCoercion co
 
 freeNamesIfCoercion :: IfaceCoercion -> NameSet
-freeNamesIfCoercion (IfaceErased _role ltyp rtyp)
+freeNamesIfCoercion (IfaceErased _ _ _ _role ltyp rtyp)
   = freeNamesIfType ltyp &&& freeNamesIfType rtyp
 freeNamesIfCoercion (IfaceReflCo t) = freeNamesIfType t
 freeNamesIfCoercion (IfaceGReflCo _ t mco)
diff --git a/compiler/iface/IfaceType.hs b/compiler/iface/IfaceType.hs
index 78aa479..15400b1 100644
--- a/compiler/iface/IfaceType.hs
+++ b/compiler/iface/IfaceType.hs
@@ -348,7 +348,14 @@ data IfaceCoercion
   | IfaceSubCo        IfaceCoercion
   | IfaceFreeCoVar    CoVar    -- See Note [Free tyvars in IfaceType]
   | IfaceHoleCo       CoVar    -- ^ See Note [Holes in IfaceCoercion]
-  | IfaceErased       Role IfaceType IfaceType --- coercions are erased
+  | IfaceErased     [IfLclName] [IfLclName] [Var]  Role IfaceType IfaceType
+
+    -- ^ @local tyvars, local covars, open free variables@
+    --
+    -- Local variables are those bound in the current IfaceType; free variables
+    -- are used only when printing open types and are not serialised; see Note
+    -- [Free tyvars in IfaceType].
+    --
 
 data IfaceUnivCoProv
   = IfaceUnsafeCoerceProv
@@ -523,7 +530,7 @@ substIfaceType env ty
     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)
-    go_co (IfaceErased role lty rty) = IfaceErased role (go lty)  (go rty)
+    go_co (IfaceErased as bs cs role lty rty) = IfaceErased as bs cs  role (go lty)  (go rty)
     go_cos = map go_co
 
     go_prov IfaceUnsafeCoerceProv    = IfaceUnsafeCoerceProv
@@ -1596,9 +1603,9 @@ ppr_co ctxt_prec (IfaceSubCo co)
   = ppr_special_co ctxt_prec (text "Sub") [co]
 ppr_co ctxt_prec (IfaceKindCo co)
   = ppr_special_co ctxt_prec (text "Kind") [co]
-ppr_co ctxt_prec (IfaceErased role lty rty)
+ppr_co ctxt_prec (IfaceErased as bs cs  role lty rty)
   = maybeParen ctxt_prec appPrec $
-    text "ErasedCoercion" <+> ppr role <+>
+    text "ErasedCoercion" <+> ppr (as,bs,cs) <+> ppr role <+>
     pprParendIfaceType lty <+> pprParendIfaceType rty
 ppr_special_co :: PprPrec -> SDoc -> [IfaceCoercion] -> SDoc
 ppr_special_co ctxt_prec doc cos
@@ -1893,8 +1900,12 @@ instance Binary IfaceCoercion where
           putByte bh 17
           put_ bh a
           put_ bh b
-  put_ bh (IfaceErased r lty rty) = do
+  put_ bh (IfaceErased as bs _nocs r lty rty) = do
            putByte bh 18
+           put_ bh as
+           put_ bh bs
+           -- no cs because ... we dont?
+           -- would
            put_ bh r
            put_ bh lty
            put_ bh rty
@@ -1961,10 +1972,12 @@ instance Binary IfaceCoercion where
                    b <- get bh
                    return $ IfaceAxiomRuleCo a b
            18 -> do
+                  as  <- get bh
+                  bs <- get bh
                   role <- get bh
                   lty  <- get bh
                   rty  <- get bh
-                  return $ IfaceErased role lty rty
+                  return $ IfaceErased as bs [] role lty rty
            _ -> panic ("get IfaceCoercion " ++ show tag)
 
 instance Binary IfaceUnivCoProv where
@@ -2040,7 +2053,8 @@ instance NFData IfaceCoercion where
     IfaceSubCo f1 -> rnf f1
     IfaceFreeCoVar f1 -> f1 `seq` ()
     IfaceHoleCo f1 -> f1 `seq` ()
-    IfaceErased rl lty rty-> rl `seq`  rnf lty `seq` rnf rty
+    IfaceErased as bs cs  rl lty rty->  liftRnf rwhnf as `seq` liftRnf rwhnf bs `seq` liftRnf rwhnf cs
+                  `seq` rl `seq`  rnf lty `seq` rnf rty
 
 instance NFData IfaceUnivCoProv where
   rnf x = seq x ()
diff --git a/compiler/iface/TcIface.hs b/compiler/iface/TcIface.hs
index 18d62f5..afaede3 100644
--- a/compiler/iface/TcIface.hs
+++ b/compiler/iface/TcIface.hs
@@ -1215,8 +1215,10 @@ tcIfaceCo = go
     go_mco IfaceMRefl    = pure MRefl
     go_mco (IfaceMCo co) = MCo <$> (go co)
 
-    go (IfaceErased r ltyi rtyi)
-                                 = ErasedCoercion r  <$>(tcIfaceType ltyi)
+    go (IfaceErased tvs cvs _ r ltyi rtyi)
+                                 = do cvs' <- mapM tcIfaceLclId cvs
+                                      tvs' <- mapM tcIfaceTyVar tvs
+                                      ErasedCoercion ( mkDVarSet $! cvs' ++  tvs') r  <$>(tcIfaceType ltyi)
                                                      <*>(tcIfaceType rtyi)
     go (IfaceReflCo t)           = Refl <$> tcIfaceType t
     go (IfaceGReflCo r t mco)    = GRefl r <$> tcIfaceType t <*> go_mco mco
diff --git a/compiler/iface/ToIface.hs b/compiler/iface/ToIface.hs
index c23985d..8aabfc0 100644
--- a/compiler/iface/ToIface.hs
+++ b/compiler/iface/ToIface.hs
@@ -265,7 +265,17 @@ toIfaceCoercionX fr co
     go_mco MRefl     = IfaceMRefl
     go_mco (MCo co)  = IfaceMCo $ go co
 
-    go (ErasedCoercion r lty rty)     = IfaceErased r (toIfaceType lty) (toIfaceType rty)
+    go (ErasedCoercion fvs r lty rty)     = IfaceErased tvs cvs openVars r (toIfaceTypeX fr lty) (toIfaceTypeX fr rty)
+
+                          where
+                            (tvs, cvs, openVars) = foldl' f ([], [], []) (dVarSetElems fvs)
+                            isOpen = (`elemVarSet` fr)
+                            f (a,b,c) v
+                              | isOpen v  = (a, b, v:c)
+                              | isCoVar v = (a, toIfaceCoVar v:b, c)
+                              | isTyVar v = (toIfaceTyVar v:a, b, c)
+                              | otherwise = panic "ToIface.toIfaceCoercionX(go_prov): Bad free variable in ZappedProv"
+
     go (Refl ty)            = IfaceReflCo (toIfaceTypeX fr ty)
     go (GRefl r ty mco)     = IfaceGReflCo r (toIfaceTypeX fr ty) (go_mco mco)
     go (CoVarCo cv)
diff --git a/compiler/main/DynFlags.hs b/compiler/main/DynFlags.hs
index 94cee4a..178d503 100644
--- a/compiler/main/DynFlags.hs
+++ b/compiler/main/DynFlags.hs
@@ -66,6 +66,7 @@ module DynFlags (
         positionIndependent,
         optimisationFlags,
         setFlagsFromEnvFile,
+        shouldEraseCoercions,
 
         Way(..), mkBuildTag, wayRTSOnly, addWay', updateWays,
         wayGeneralFlags, wayUnsetGeneralFlags,
@@ -506,6 +507,7 @@ data GeneralFlag
    = Opt_DumpToFile                     -- ^ Append dump output to files instead of stdout.
    | Opt_D_faststring_stats
    | Opt_D_dump_minimal_imports
+   | Opt_EraseCoercions
    | Opt_DoCoreLinting
    | Opt_DoStgLinting
    | Opt_DoCmmLinting
@@ -1698,6 +1700,10 @@ shouldUseHexWordLiterals :: DynFlags -> Bool
 shouldUseHexWordLiterals dflags =
   Opt_HexWordLiterals `EnumSet.member` generalFlags dflags
 
+shouldEraseCoercions :: DynFlags -> Bool
+shouldEraseCoercions dflags =
+  not  (gopt Opt_DoCoreLinting dflags) ||  not (gopt Opt_EraseCoercions dflags)
+
 -- | Are we building with @-fPIE@ or @-fPIC@ enabled?
 positionIndependent :: DynFlags -> Bool
 positionIndependent dflags = gopt Opt_PIC dflags || gopt Opt_PIE dflags
@@ -3313,7 +3319,8 @@ dynamic_flags_deps = [
         ------ Debugging ----------------------------------------------------
   , make_ord_flag defGhcFlag "dstg-stats"
         (NoArg (setGeneralFlag Opt_StgStats))
-
+  , make_ord_flag defGhcFlag "derase-coercions"
+        (NoArg (setGeneralFlag Opt_EraseCoercions))
   , make_ord_flag defGhcFlag "ddump-cmm"
         (setDumpFlag Opt_D_dump_cmm)
   , make_ord_flag defGhcFlag "ddump-cmm-from-stg"
diff --git a/compiler/simplCore/CoreEraseCoercionProofs.hs b/compiler/simplCore/CoreEraseCoercionProofs.hs
index 0801807..1b053ec 100644
--- a/compiler/simplCore/CoreEraseCoercionProofs.hs
+++ b/compiler/simplCore/CoreEraseCoercionProofs.hs
@@ -38,18 +38,10 @@ coreExprEraseProof (Case  scrut v ty alts  )=
     Case (coreExprEraseProof scrut) v ty (map eraseAltPfs alts)
     --- TODO : add mrefl and refl cases,
     --- that should suffice to prevent regresions vs current ghc
-coreExprEraseProof (Cast  e co ) = case co of
-      (Refl _t) -> Cast e  co
-      (GRefl _r _t MRefl) -> Cast e co
-      (_) ->  Cast (coreExprEraseProof e) (ErasedCoercion role lty rty )
-  where
-    (Pair lty rty,role) = coercionKindRole co
+coreExprEraseProof (Cast  e co ) =    Cast (coreExprEraseProof e) (forcedEraseCoercion co )
 coreExprEraseProof (Tick  tick e)= Tick tick (coreExprEraseProof e)
 coreExprEraseProof (Type  t) = Type t
-coreExprEraseProof (Coercion co )= case co of
-      (Refl t) -> Coercion co
-      (GRefl r t MRefl) -> Coercion co
-      (_) ->  Coercion (ErasedCoercion role lty rty )
+coreExprEraseProof (Coercion co )=  Coercion $! forcedEraseCoercion co
   where
     (Pair lty rty,role) = coercionKindRole co
 eraseAltPfs :: CoreAlt -> CoreAlt
diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs
index 4cf5db3..72a0815 100644
--- a/compiler/typecheck/TcMType.hs
+++ b/compiler/typecheck/TcMType.hs
@@ -1357,9 +1357,10 @@ collect_cand_qtvs_co :: VarSet -- bound variables
 collect_cand_qtvs_co bound = go_co
   where
 
-    go_co dv (ErasedCoercion _role lty rty ) = do
+    go_co dv (ErasedCoercion fvs  _role lty rty ) = do
                                     dv1 <-collect_cand_qtvs True bound dv lty
-                                    collect_cand_qtvs True bound dv1 rty
+                                    dv2 <- collect_cand_qtvs True bound dv1 rty
+                                    foldlM go_cv dv2 (dVarSetElems fvs)
     go_co dv (Refl ty)             = collect_cand_qtvs True bound dv ty
     go_co dv (GRefl _ ty mco)      = do dv1 <- collect_cand_qtvs True bound dv ty
                                         go_mco dv1 mco
diff --git a/compiler/typecheck/TcTyDecls.hs b/compiler/typecheck/TcTyDecls.hs
index a09140d..0fe209a 100644
--- a/compiler/typecheck/TcTyDecls.hs
+++ b/compiler/typecheck/TcTyDecls.hs
@@ -117,7 +117,7 @@ synonymTyConsOfType ty
      go_mco MRefl    = emptyNameEnv
      go_mco (MCo co) = go_co co
 
-     go_co (ErasedCoercion r lty rty ) = go lty `plusNameEnv` go rty
+     go_co (ErasedCoercion _fvs _r lty rty ) = go lty `plusNameEnv` go rty
      go_co (Refl ty)              = go ty
      go_co (GRefl _ ty mco)       = go ty `plusNameEnv` go_mco mco
      go_co (TyConAppCo _ tc cs)   = go_tc tc `plusNameEnv` go_co_s cs
diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs
index 49e9fe2..f2eb296 100644
--- a/compiler/types/Coercion.hs
+++ b/compiler/types/Coercion.hs
@@ -111,7 +111,14 @@ module Coercion (
         -- * Other
         promoteCoercion, buildCoercion,
 
-        simplifyArgsWorker
+        simplifyArgsWorker,
+
+        --- * coercion erasure
+        forcedEraseCoercion,
+        eraseCoercion,
+        mkErasedCoercion,
+        alwaysMkErasedCoercion
+
        ) where
 
 #include "HsVersions.h"
@@ -144,6 +151,7 @@ import TysPrim
 import ListSetOps
 import Maybes
 import UniqFM
+import DynFlags         ( DynFlags, shouldEraseCoercions)
 
 import Control.Monad (foldM, zipWithM)
 import Data.Function ( on )
@@ -709,12 +717,6 @@ mkFunCo r co1 co2
 mkAppCo :: Coercion     -- ^ :: t1 ~r t2
         -> Coercion     -- ^ :: s1 ~N s2, where s1 :: k1, s2 :: k2
         -> Coercion     -- ^ :: t1 s1 ~r t2 s2
-mkAppCo co1 co2
-  | r2 == Nominal  || (r1 == Phantom && (r2 == Nominal || r2 == Phantom))
-  = ErasedCoercion r1 (mkAppTy lt1 lt2) (mkAppTy rt1 rt2)
-  where
-    (Pair lt1 rt1,r1) = coercionKindRole co1
-    (Pair lt2 rt2,r2) = coercionKindRole co2
 mkAppCo co arg
   | Just (ty1, r) <- isReflCo_maybe co
   , Just (ty2, _) <- isReflCo_maybe arg
@@ -974,7 +976,7 @@ mkSymCo :: Coercion -> Coercion
 mkSymCo co | isReflCo co          = co
 mkSymCo    (SymCo co)             = co
 mkSymCo    (SubCo (SymCo co))     = SubCo co
-mkSymCo (ErasedCoercion r lt rt)  = ErasedCoercion r rt lt
+mkSymCo (ErasedCoercion fv r lt rt)  = ErasedCoercion fv r rt lt
 mkSymCo co                        = SymCo co
 
 -- | Create a new 'Coercion' by composing the two given 'Coercion's transitively.
@@ -984,21 +986,122 @@ mkTransCo co1 co2 | isReflCo co1 = co2
                   | isReflCo co2 = co1
 mkTransCo (GRefl r t1 (MCo co1)) (GRefl _ _ (MCo co2))
   = GRefl r t1 (MCo $ mkTransCo co1 co2)
-mkTransCo co1 co2
-    | isErasedCoercion co1 || isErasedCoercion co2
-     =   ErasedCoercion r1 lt1 rt2
-    |  otherwise            = TransCo co1 co2
-  where
-    (Pair lt1 _rt1,r1) = coercionKindRole co1
-    (Pair _lt2 rt2,_r2) = coercionKindRole co2
-isErasedCoercion_maybe :: Coercion -> Maybe (Role,Type,Type)
-isErasedCoercion_maybe (ErasedCoercion r lt rt) = Just (r,lt,rt)
+mkTransCo (ErasedCoercion  fvs1 r t1a _t1b) (ErasedCoercion fvs2 _ _t2a t2b)
+  = ErasedCoercion  (fvs1 `unionDVarSet` fvs2) r t1a t2b
+mkTransCo (ErasedCoercion  fvs r t1a _t1b) co2
+  = ErasedCoercion (fvs `unionDVarSet` tyCoVarsOfCoDSet co2) r t1a t2b
+  where Pair _t2a t2b = coercionKind co2
+mkTransCo co1 (ErasedCoercion  fvs r _t2a t2b)
+  = ErasedCoercion  (fvs `unionDVarSet` tyCoVarsOfCoDSet co1) r t1a t2b
+  where Pair t1a _t1b = coercionKind co1
+mkTransCo co1 co2                 = TransCo co1 co2
+
+
+isErasedCoercion_maybe :: Coercion -> Maybe (DVarSet,Role,Type,Type)
+isErasedCoercion_maybe (ErasedCoercion fv  r lt rt) = Just (fv,r,lt,rt)
 isErasedCoercion_maybe _ = Nothing
 
 isErasedCoercion :: Coercion -> Bool
 isErasedCoercion c = case isErasedCoercion_maybe c of
                       Just _ -> True ; Nothing -> False
 
+-- shamelessly copied from Ben Gamari's version of this code
+-- | Make a Erased coercion if building of coercions is disabled, otherwise
+-- return the given un-erased coercion.
+mkErasedCoercion :: HasDebugCallStack
+                 => DynFlags
+                 -> Coercion  -- ^ the un-Erased coercion
+                 -> Pair Type -- ^ the kind of the coercion
+                 -> Role      -- ^ the role of the coercion
+                 -> DTyCoVarSet -- ^ the free variables of the coercion
+                 -> Coercion
+mkErasedCoercion dflags co (Pair ty1 ty2) role fvs
+  | debugIsOn && real_role /= role =
+    pprPanic "mkErasedCoercion(roles mismatch)" panic_doc
+  | debugIsOn && not co_kind_ok =
+    pprPanic "mkErasedCoercion(kind mismatch)" panic_doc
+  | not $ shouldEraseCoercions dflags = co
+  | otherwise =
+    ErasedCoercion fvs   role ty1 ty2
+  where
+    (Pair real_ty1 real_ty2, real_role) = coercionKindRole co
+    real_fvs = tyCoVarsOfCoDSet co
+        -- We must unify here (at the loss of some precision in the assertion)
+        -- since we may encounter flattening skolems.
+    --co_kind_ok = isJust $ tcUnifyTys (const BindMe) [real_ty1, real_ty2] [ty1, ty2]
+    co_kind_ok = True
+        -- N.B. It's not generally possible to check fCvs against the actual
+        -- free variable set since we may encounter flattening skolems during
+        -- reduction.
+    panic_doc = vcat
+        [ text "real role:" <+> ppr real_role
+        , text "given role:" <+> ppr role
+        , text "real ty1:" <+> ppr real_ty1
+        , text "given ty1:" <+> ppr ty1
+        , text "real ty2:" <+> ppr real_ty2
+        , text "given ty2:" <+> ppr ty2
+        , text "real free co vars:" <+> ppr real_fvs
+        , text "given free co vars:" <+> ppr fvs
+        , text "coercion:" <+> ppr co
+        ]
+
+-- | Replace a coercion with a erased coercion unless coercions are needed.
+eraseCoercion :: DynFlags -> Coercion -> Coercion
+eraseCoercion _ co@(ErasedCoercion _ _ _ _ ) = co  -- already zapped
+eraseCoercion _ co@(Refl _) = co  -- Refl is smaller than zapped coercions
+eraseCoercion _ co@(GRefl _r _ty MRefl ) = co
+eraseCoercion dflags co =
+    mkErasedCoercion dflags co (Pair t1 t2) role fvs
+  where
+    (Pair t1 t2, role) = coercionKindRole co
+    fvs = filterDVarSet (not . isCoercionHole) $ tyCoVarsOfCoDSet co
+
+alwaysMkErasedCoercion :: HasDebugCallStack
+                 => Coercion  -- ^ the un-Erased coercion
+                 -> Pair Type -- ^ the kind of the coercion
+                 -> Role      -- ^ the role of the coercion
+                 -> DTyCoVarSet -- ^ the free variables of the coercion
+                 -> Coercion
+alwaysMkErasedCoercion co (Pair ty1 ty2) role fvs
+  | debugIsOn && real_role /= role =
+    pprPanic "mkErasedCoercion(roles mismatch)" panic_doc
+  | debugIsOn && not co_kind_ok =
+    pprPanic "mkErasedCoercion(kind mismatch)" panic_doc
+  | otherwise =
+    ErasedCoercion fvs   role ty1 ty2
+  where
+    (Pair real_ty1 real_ty2, real_role) = coercionKindRole co
+    real_fvs = tyCoVarsOfCoDSet co
+        -- We must unify here (at the loss of some precision in the assertion)
+        -- since we may encounter flattening skolems.
+    --co_kind_ok = isJust $ tcUnifyTys (const BindMe) [real_ty1, real_ty2] [ty1, ty2]
+    co_kind_ok = True
+        -- N.B. It's not generally possible to check fCvs against the actual
+        -- free variable set since we may encounter flattening skolems during
+        -- reduction.
+    panic_doc = vcat
+        [ text "real role:" <+> ppr real_role
+        , text "given role:" <+> ppr role
+        , text "real ty1:" <+> ppr real_ty1
+        , text "given ty1:" <+> ppr ty1
+        , text "real ty2:" <+> ppr real_ty2
+        , text "given ty2:" <+> ppr ty2
+        , text "real free co vars:" <+> ppr real_fvs
+        , text "given free co vars:" <+> ppr fvs
+        , text "coercion:" <+> ppr co
+        ]
+
+
+forcedEraseCoercion ::  HasDebugCallStack => Coercion -> Coercion
+forcedEraseCoercion co@(ErasedCoercion _ _ _ _ ) = co  -- already zapped
+forcedEraseCoercion co@(Refl _) = co  -- Refl is smaller than zapped coercions
+forcedEraseCoercion co@(GRefl _r _ty MRefl ) = co
+forcedEraseCoercion co =
+    alwaysMkErasedCoercion  co (Pair t1 t2) role fvs
+  where
+    (Pair t1 t2, role) = coercionKindRole co
+    fvs = filterDVarSet (not . isCoercionHole) $ tyCoVarsOfCoDSet co
+
 -- | Compose two MCoercions via transitivity
 mkTransMCo :: MCoercion -> MCoercion -> MCoercion
 mkTransMCo MRefl     co2       = co2
@@ -1024,13 +1127,13 @@ mkNthCo r n co
         ASSERT( r == Nominal )
         mkNomReflCo (varType tv)
 
-    go r 0 (ErasedCoercion _ lt rt)
+    go r 0 (ErasedCoercion fvs _ lt rt)
       | Just(ltv,_) <- splitForAllTy_maybe lt
       , Just(rtv,_) <- splitForAllTy_maybe rt
 
       = -- ErasedCoercion proofs are quite strange!
         ASSERT(r == Nominal)
-        ErasedCoercion Nominal (varType ltv) (varType rtv )
+        ErasedCoercion fvs Nominal (varType ltv) (varType rtv )
 
 
     go r n co
@@ -1048,7 +1151,7 @@ mkNthCo r n co
               | otherwise
               = False
 
-    go r n (ErasedCoercion r0 lt rt )
+    go r n (ErasedCoercion fv r0 lt rt )
       | Just (ltycon,lts) <- splitTyConApp_maybe lt
       , Just (rtycon,rts) <- splitTyConApp_maybe rt
       ,let ltc = tyConAppTyCon lt  --- not sure why i'm copying this debugging stuff
@@ -1057,7 +1160,7 @@ mkNthCo r n co
         ASSERT2( ok_tc_app rt n, ppr n $$ ppr rt )
         ASSERT( nthRole r0 ltc n == r )
         ASSERT( nthRole r0 rtc n == r )
-        ErasedCoercion r (tyConAppArgN n lt) (tyConAppArgN n rt)
+        ErasedCoercion fv r (tyConAppArgN n lt) (tyConAppArgN n rt)
       where ok_tc_app :: Type -> Int -> Bool
             ok_tc_app ty n
               | Just (_, tys) <- splitTyConApp_maybe ty
@@ -1219,6 +1322,8 @@ mkKindCo co | Just (ty, _) <- isReflCo_maybe co = Refl (typeKind ty)
 mkKindCo (GRefl _ _ (MCo co)) = co
 mkKindCo (UnivCo (PhantomProv h) _ _ _)    = h
 mkKindCo (UnivCo (ProofIrrelProv h) _ _ _) = h
+mkKindCo (ErasedCoercion fvs r lt rt )
+        = (ErasedCoercion fvs Nominal (typeKind lt) (typeKind rt))
 mkKindCo co
   | Pair ty1 ty2 <- coercionKind co
        -- generally, calling coercionKind during coercion creation is a bad idea,
@@ -1234,7 +1339,7 @@ mkKindCo co
 mkSubCo :: Coercion -> Coercion
 -- Input coercion is Nominal, result is Representational
 -- see also Note [Role twiddling functions]
-mkSubCo (ErasedCoercion Nominal lt rt) = ErasedCoercion Representational lt rt
+mkSubCo (ErasedCoercion fvs Nominal lt rt) = ErasedCoercion fvs  Representational lt rt
 mkSubCo (Refl ty) = GRefl Representational ty MRefl
 mkSubCo (GRefl Nominal ty co) = GRefl Representational ty co
 mkSubCo (TyConAppCo Nominal tc cos)
@@ -1306,7 +1411,7 @@ setNominalRole_maybe r co
   | r == Nominal = Just co
   | otherwise = setNominalRole_maybe_helper co
   where
-    setNominalRole_maybe_helper (ErasedCoercion _ lt rt) = Just (ErasedCoercion Nominal lt rt)
+    setNominalRole_maybe_helper (ErasedCoercion fvs  _ lt rt) = Just (ErasedCoercion fvs Nominal lt rt)
     setNominalRole_maybe_helper (SubCo co)  = Just co
     setNominalRole_maybe_helper co@(Refl _) = Just co
     setNominalRole_maybe_helper (GRefl _ ty co) = Just $ GRefl Nominal ty co
@@ -1349,7 +1454,7 @@ mkPhantomCo h t1 t2
 
 -- takes any coercion and turns it into a Phantom coercion
 toPhantomCo :: Coercion -> Coercion
-toPhantomCo (ErasedCoercion _ lt rt) = ErasedCoercion Phantom lt rt
+toPhantomCo (ErasedCoercion fvs _ lt rt) = ErasedCoercion fvs Phantom lt rt
 toPhantomCo co  = mkPhantomCo (mkKindCo co) ty1 ty2
     where Pair ty1 ty2 = coercionKind co
 
@@ -1488,7 +1593,7 @@ promoteCoercion co = case co of
     SubCo g
       -> promoteCoercion g
 
-    ErasedCoercion r _lty _rty -> ErasedCoercion r ty1 ty2
+    ErasedCoercion fvs r _lty _rty -> ErasedCoercion fvs r ty1 ty2
   where
     Pair ty1 ty2 = coercionKind co
     ki1 = typeKind ty1
@@ -2176,7 +2281,7 @@ seqMCo MRefl    = ()
 seqMCo (MCo co) = seqCo co
 
 seqCo :: Coercion -> ()
-seqCo (ErasedCoercion r lt rt) = r `seq` seqType lt `seq` seqType rt
+seqCo (ErasedCoercion fvs r lt rt) = seqDVarSet fvs `seq`r `seq` seqType lt `seq` seqType rt
 seqCo (Refl ty)                 = seqType ty
 seqCo (GRefl r ty mco)          = r `seq` seqType ty `seq` seqMCo mco
 seqCo (TyConAppCo r tc cos)     = r `seq` tc `seq` seqCos cos
@@ -2242,7 +2347,7 @@ coercionLKind :: Coercion -> Type
 coercionLKind co
   = go co
   where
-    go (ErasedCoercion _role ltyp _rtyp)   = ltyp
+    go (ErasedCoercion _fvs _role ltyp _rtyp)   = ltyp
     go (Refl ty)                = ty
     go (GRefl _ ty _)           = ty
     go (TyConAppCo _ tc cos)    = mkTyConApp tc (map go cos)
@@ -2298,7 +2403,7 @@ coercionRKind :: Coercion -> Type
 coercionRKind co
   = go co
   where
-    go (ErasedCoercion _role _ltyp rtype)   = rtype
+    go (ErasedCoercion _fvs _role _ltyp rtype)   = rtype
     go (Refl ty)                = ty
     go (GRefl _ ty MRefl)       = ty
     go (GRefl _ ty (MCo co1))   = mkCastTy ty co1
@@ -2404,7 +2509,7 @@ change reduces /total/ compile time by a factor of more than ten.
 coercionRole :: Coercion -> Role
 coercionRole = go
   where
-    go (ErasedCoercion r _ _) = r
+    go (ErasedCoercion _ r  _ _ ) = r
     go (Refl _) = Nominal
     go (GRefl r _ _) = r
     go (TyConAppCo r _ _) = r
diff --git a/compiler/types/OptCoercion.hs b/compiler/types/OptCoercion.hs
index 46a4196..b7a512c 100644
--- a/compiler/types/OptCoercion.hs
+++ b/compiler/types/OptCoercion.hs
@@ -191,7 +191,7 @@ opt_co4_wrap env sym rep r co
     pprTrace "opt_co4_wrap }" (ppr co $$ text "---" $$ ppr result) $
     result
 -}
-opt_co4 _lc _sym _rp _role e@(ErasedCoercion _ _ _) = e
+opt_co4 _lc _sym _rp _role e@(ErasedCoercion _ _ _ _) = e
 opt_co4 env _   rep r (Refl ty)
   = ASSERT2( r == Nominal, text "Expected role:" <+> ppr r    $$
                            text "Found role:" <+> ppr Nominal $$
diff --git a/compiler/types/TyCoFVs.hs b/compiler/types/TyCoFVs.hs
index 58068c0..56d430e 100644
--- a/compiler/types/TyCoFVs.hs
+++ b/compiler/types/TyCoFVs.hs
@@ -207,8 +207,10 @@ tyCoVarsOfCos cos = ty_co_vars_of_cos cos emptyVarSet emptyVarSet
 
 
 ty_co_vars_of_co :: Coercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
-ty_co_vars_of_co (ErasedCoercion _r lty rty) is acc =  ty_co_vars_of_type rty is $
-                                                       ty_co_vars_of_type lty is acc
+ty_co_vars_of_co (ErasedCoercion fvs  _r lty rty) is acc
+                                             =  ty_co_vars_of_type rty is $
+                                                ty_co_vars_of_type lty is $
+                                                    dVarSetToVarSet fvs `unionVarSet` acc
 ty_co_vars_of_co (Refl ty)            is acc = ty_co_vars_of_type ty is acc
 ty_co_vars_of_co (GRefl _ ty mco)     is acc = ty_co_vars_of_type ty is $
                                                ty_co_vars_of_mco mco is acc
@@ -343,7 +345,8 @@ exactTyCoVarsOfType ty
     goMCo MRefl    = emptyVarSet
     goMCo (MCo co) = goCo co
 
-    goCo (ErasedCoercion _ lty rty ) = go lty `unionVarSet` go rty
+    goCo (ErasedCoercion fvs _ lty rty )
+     =  go lty `unionVarSet` go rty `unionVarSet` dVarSetToVarSet fvs
     goCo (Refl ty)            = go ty
     goCo (GRefl _ ty mco)     = go ty `unionVarSet` goMCo mco
     goCo (TyConAppCo _ _ args)= goCos args
@@ -440,8 +443,9 @@ tyCoVarsOfCosSet cos = tyCoVarsOfCos $ nonDetEltsUFM cos
 tyCoFVsOfCo :: Coercion -> FV
 -- Extracts type and coercion variables from a coercion
 -- See Note [Free variables of types]
-tyCoFVsOfCo (ErasedCoercion _ lty rty) fv_cand in_scope acc
-  = (tyCoFVsOfType lty `unionFV` tyCoFVsOfType rty) fv_cand in_scope acc
+tyCoFVsOfCo (ErasedCoercion fvs  _ lty rty) fv_cand in_scope acc
+  = (tyCoFVsOfType lty `unionFV` tyCoFVsOfType rty
+                       `unionFV` (mkFVs $ dVarSetElems fvs)) fv_cand in_scope acc
 tyCoFVsOfCo (Refl ty) fv_cand in_scope acc
   = tyCoFVsOfType ty fv_cand in_scope acc
 tyCoFVsOfCo (GRefl _ ty mco) fv_cand in_scope acc
@@ -531,7 +535,7 @@ almostDevoidCoVarOfCo cv co =
   almost_devoid_co_var_of_co co cv
 
 almost_devoid_co_var_of_co :: Coercion -> CoVar -> Bool
-almost_devoid_co_var_of_co (ErasedCoercion _ _ _)  _ =  True
+almost_devoid_co_var_of_co (ErasedCoercion fvs _ _  _)  cv =  cv `elemDVarSet` fvs
 almost_devoid_co_var_of_co (Refl {}) _ = True   -- covar is allowed in Refl and
 almost_devoid_co_var_of_co (GRefl {}) _ = True  -- GRefl, so we don't look into
                                                 -- the coercions
@@ -735,8 +739,8 @@ noFreeVarsOfTypes = all noFreeVarsOfType
 -- | Returns True if this coercion has no free variables. Should be the same as
 -- isEmptyVarSet . tyCoVarsOfCo, but faster in the non-forall case.
 noFreeVarsOfCo :: Coercion -> Bool
-noFreeVarsOfCo (ErasedCoercion r lty rty)=  noFreeVarsOfType lty &&
-                                            noFreeVarsOfType rty
+noFreeVarsOfCo (ErasedCoercion fvs r lty rty)=  noFreeVarsOfType lty &&
+                                            noFreeVarsOfType rty && isEmptyDVarSet fvs
 noFreeVarsOfCo (Refl ty)              = noFreeVarsOfType ty
 noFreeVarsOfCo (GRefl _ ty co)        = noFreeVarsOfType ty && noFreeVarsOfMCo co
 noFreeVarsOfCo (TyConAppCo _ _ args)  = all noFreeVarsOfCo args
diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs
index 484e776..db3df51 100644
--- a/compiler/types/TyCoRep.hs
+++ b/compiler/types/TyCoRep.hs
@@ -88,7 +88,7 @@ import BasicTypes ( LeftOrRight(..), pickLR )
 import Outputable
 import FastString
 import Util
-
+import  UniqDSet
 -- libraries
 import qualified Data.Data as Data hiding ( TyCon )
 import Data.IORef ( IORef )   -- for CoercionHole
@@ -1068,8 +1068,11 @@ data Coercion
 
   | HoleCo CoercionHole              -- ^ See Note [Coercion holes]
                                      -- Only present during typechecking
-  | ErasedCoercion Role Type Type-- ^ optimization hack because cast terms blowup fusion heavy
-                   -- code, implied whenever corelint isn't enabled
+  | ErasedCoercion DTyCoVarSet Role Type Type
+     --  ^ optimization hack because cast terms blowup fusion heavy
+                   -- code, implied whenever corelint isn't enabled.
+                   -- we track coercion free variables for interface files,
+                   -- even though
   deriving Data.Data
 
 type CoercionN = Coercion       -- always nominal
@@ -1674,7 +1677,9 @@ coercionSize (ForAllCo _ h co)   = 1 + coercionSize co + coercionSize h
 coercionSize (FunCo _ co1 co2)   = 1 + coercionSize co1 + coercionSize co2
 coercionSize (CoVarCo _)         = 1
 coercionSize (HoleCo _)          = 1
-coercionSize (ErasedCoercion _ lty rty  )=   1 + typeSize lty + typeSize rty
+coercionSize (ErasedCoercion cofvs _ lty rty  )
+                                 =   1 + typeSize lty + typeSize rty
+                                       + sizeUniqDSet cofvs
 coercionSize (AxiomInstCo _ _ args) = 1 + sum (map coercionSize args)
 coercionSize (UnivCo p _ t1 t2)  = 1 + provSize p + typeSize t1 + typeSize t2
 coercionSize (SymCo co)          = 1 + coercionSize co
diff --git a/compiler/types/TyCoSubst.hs b/compiler/types/TyCoSubst.hs
index 3b65350..19cace7 100644
--- a/compiler/types/TyCoSubst.hs
+++ b/compiler/types/TyCoSubst.hs
@@ -14,6 +14,7 @@ module TyCoSubst
         TCvSubst(..), TvSubstEnv, CvSubstEnv,
         emptyTvSubstEnv, emptyCvSubstEnv, composeTCvSubstEnv, composeTCvSubst,
         emptyTCvSubst, mkEmptyTCvSubst, isEmptyTCvSubst,
+        substFreeDVarSet,
         mkTCvSubst, mkTvSubst, mkCvSubst,
         getTvSubstEnv,
         getCvSubstEnv, getTCvInScope, getTCvSubstRangeFVs,
@@ -791,7 +792,12 @@ subst_co subst co
     go_mco (MCo co) = MCo (go co)
 
     go :: Coercion -> Coercion
-    go (ErasedCoercion r lty rty ) = (ErasedCoercion  r   $! (go_ty lty)) $! (go_ty rty)
+    go (ErasedCoercion fvs r lty rty )
+      = (((ErasedCoercion
+          $! (substFreeDVarSet subst fvs))
+          $! r)
+          $! (go_ty lty))
+          $! (go_ty rty)
     go (Refl ty)             = mkNomReflCo $! (go_ty ty)
     go (GRefl r ty mco)      = (mkGReflCo r $! (go_ty ty)) $! (go_mco mco)
     go (TyConAppCo r tc args)= let args' = map go args
@@ -826,6 +832,15 @@ subst_co subst co
     go_hole h@(CoercionHole { ch_co_var = cv })
       = h { ch_co_var = updateVarType go_ty cv }
 
+
+-- | Perform a substitution within a 'DVarSet' of free variables.
+substFreeDVarSet :: TCvSubst -> DVarSet -> DVarSet
+substFreeDVarSet subst =
+    let f v
+          | isTyVar v = tyCoVarsOfTypeDSet $ substTyVar subst v
+          | otherwise = tyCoVarsOfCoDSet $ substCoVar subst v
+    in mapUnionDVarSet f . dVarSetElems
+
 substForAllCoBndr :: TCvSubst -> TyCoVar -> KindCoercion
                   -> (TCvSubst, TyCoVar, Coercion)
 substForAllCoBndr subst
diff --git a/compiler/types/TyCoTidy.hs b/compiler/types/TyCoTidy.hs
index 4b6ab59..2f7ce8e 100644
--- a/compiler/types/TyCoTidy.hs
+++ b/compiler/types/TyCoTidy.hs
@@ -24,8 +24,10 @@ import TyCoFVs (tyCoVarsOfTypesWellScoped, tyCoVarsOfTypeList)
 import Name hiding (varName)
 import Var
 import VarEnv
+import VarSet
 import Util (seqList)
 
+import Data.Maybe ( fromMaybe )
 import Data.List
 
 {-
@@ -197,7 +199,10 @@ tidyCo env@(_, subst) co
     go_mco MRefl    = MRefl
     go_mco (MCo co) = MCo (go co)
 
-    go (ErasedCoercion r lty rty ) = ErasedCoercion r (tidyType env lty) (tidyType env rty)
+    -- this is seemingly missing in
+    go (ErasedCoercion fvs  r lty rty )
+      = ErasedCoercion (mapUnionDVarSet (unitDVarSet . substCoVar) (dVarSetElems fvs))
+                       r (tidyType env lty) (tidyType env rty)
     go (Refl ty)             = Refl (tidyType env ty)
     go (GRefl r ty mco)      = GRefl r (tidyType env ty) $! go_mco mco
     go (TyConAppCo r tc cos) = let args = map go cos
@@ -226,6 +231,8 @@ tidyCo env@(_, subst) co
     go (AxiomRuleCo ax cos)  = let cos1 = tidyCos env cos
                                in cos1 `seqList` AxiomRuleCo ax cos1
 
+    substCoVar cv = fromMaybe cv $ lookupVarEnv subst cv
+
     go_prov UnsafeCoerceProv    = UnsafeCoerceProv
     go_prov (PhantomProv co)    = PhantomProv (go co)
     go_prov (ProofIrrelProv co) = ProofIrrelProv (go co)
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index 22100d1..564f5ea 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -424,8 +424,8 @@ expandTypeSynonyms ty
     go_mco _     MRefl    = MRefl
     go_mco subst (MCo co) = MCo (go_co subst co)
 
-    go_co subst (ErasedCoercion r lty rty)
-      = ErasedCoercion r (go subst lty) (go subst rty)
+    go_co subst (ErasedCoercion  fvs r lty rty)
+      = ErasedCoercion (substFreeDVarSet subst fvs) r (go subst lty) (go subst rty)
     go_co subst (Refl ty)
       = mkNomReflCo (go subst ty)
     go_co subst (GRefl r ty mco)
@@ -651,6 +651,7 @@ mapCoercion :: Monad m
             => TyCoMapper env m -> env -> Coercion -> m Coercion
 mapCoercion mapper@(TyCoMapper { tcm_covar = covar
                                , tcm_hole = cohole
+                               , tcm_tyvar = tyvar
                                , tcm_tycobinder = tycobinder
                                , tcm_tycon = tycon })
             env co
@@ -659,8 +660,16 @@ mapCoercion mapper@(TyCoMapper { tcm_covar = covar
     go_mco MRefl    = return MRefl
     go_mco (MCo co) = MCo <$> (go co)
 
-    go (ErasedCoercion r lty rty )
-      = ErasedCoercion r <$> mapType mapper env lty <*>  mapType mapper env rty
+    go (ErasedCoercion fvs  r lty rty )
+      =
+        let bndrFVs v | isCoVar v = tyCoVarsOfCoDSet <$> covar env v
+              | isTyVar v = tyCoVarsOfTypeDSet <$> tyvar env v
+              | isCoercionHole v = return emptyDVarSet
+              | otherwise = pprPanic "mapCoercion(coercion): Bad free variable" (ppr v)
+         in
+            do fvs' <- unionDVarSets <$> mapM bndrFVs (dVarSetElems fvs)
+               (ErasedCoercion fvs' r <$>  mapType mapper env lty <*> mapType mapper env rty)
+
     go (Refl ty) = Refl <$> mapType mapper env ty
     go (GRefl r ty mco) = mkGReflCo r <$> mapType mapper env ty <*> (go_mco mco)
     go (TyConAppCo r tc args)
@@ -2685,9 +2694,10 @@ occCheckExpand vs_to_avoid ty
     go_mco ctx (MCo co) = MCo <$> go_co ctx co
 
     ------------------
-    go_co ctx  (ErasedCoercion r lty rty ) = do { lty' <- go ctx lty
+    go_co ctx  (ErasedCoercion fvs r lty rty )
+                                        = do { lty' <- go ctx lty
                                               ; rty' <- go ctx rty
-                                              ; return $ ErasedCoercion  r lty' rty' }
+                                              ; return $ ErasedCoercion fvs  r lty' rty' }
     go_co cxt (Refl ty)                 = do { ty' <- go cxt ty
                                              ; return (mkNomReflCo ty') }
     go_co cxt (GRefl r ty mco)          = do { mco' <- go_mco cxt mco
@@ -2775,7 +2785,7 @@ tyConsOfType ty
      go (CastTy ty co)              = go ty `unionUniqSets` go_co co
      go (CoercionTy co)             = go_co co
 
-     go_co (ErasedCoercion r lty rty ) =  go lty `unionUniqSets` go rty
+     go_co (ErasedCoercion _fv _r lty rty ) =  go lty `unionUniqSets` go rty
      go_co (Refl ty)               = go ty
      go_co (GRefl _ ty mco)        = go ty `unionUniqSets` go_mco mco
      go_co (TyConAppCo _ tc args)  = go_tc tc `unionUniqSets` go_cos args