[Git][ghc/ghc][wip/zap-coercions] Coercion zapping

Ben Gamari gitlab at gitlab.haskell.org
Tue Jun 11 19:28:01 UTC 2019



Ben Gamari pushed to branch wip/zap-coercions at Glasgow Haskell Compiler / GHC


Commits:
ea7f96de by Ben Gamari at 2019-06-11T19:27:48Z
Coercion zapping

- - - - -


20 changed files:

- compiler/basicTypes/VarSet.hs
- compiler/coreSyn/CoreFVs.hs
- compiler/coreSyn/CoreLint.hs
- compiler/coreSyn/CoreOpt.hs
- compiler/iface/IfaceEnv.hs
- compiler/iface/IfaceSyn.hs
- compiler/iface/IfaceType.hs
- compiler/iface/TcIface.hs
- compiler/iface/ToIface.hs
- compiler/main/DynFlags.hs
- compiler/typecheck/TcFlatten.hs
- compiler/typecheck/TcHsType.hs
- compiler/typecheck/TcTyDecls.hs
- compiler/typecheck/TcType.hs
- compiler/types/Coercion.hs
- compiler/types/Coercion.hs-boot
- compiler/types/FamInstEnv.hs
- compiler/types/OptCoercion.hs
- compiler/types/TyCoRep.hs
- compiler/types/Type.hs


Changes:

=====================================
compiler/basicTypes/VarSet.hs
=====================================
@@ -25,7 +25,7 @@ module VarSet (
         pluralVarSet, pprVarSet,
 
         -- * Deterministic Var set types
-        DVarSet, DIdSet, DTyVarSet, DTyCoVarSet,
+        DVarSet, DIdSet, DTyVarSet, DCoVarSet, DTyCoVarSet,
 
         -- ** Manipulating these sets
         emptyDVarSet, unitDVarSet, mkDVarSet,
@@ -225,6 +225,9 @@ type DIdSet      = UniqDSet Id
 -- | Deterministic Type Variable Set
 type DTyVarSet   = UniqDSet TyVar
 
+-- | Deterministic Coercion Variable Set
+type DCoVarSet   = UniqDSet CoVar
+
 -- | Deterministic Type or Coercion Variable Set
 type DTyCoVarSet = UniqDSet TyCoVar
 


=====================================
compiler/coreSyn/CoreFVs.hs
=====================================
@@ -396,6 +396,9 @@ orphNamesOfProv UnsafeCoerceProv    = emptyNameSet
 orphNamesOfProv (PhantomProv co)    = orphNamesOfCo co
 orphNamesOfProv (ProofIrrelProv co) = orphNamesOfCo co
 orphNamesOfProv (PluginProv _)      = emptyNameSet
+orphNamesOfProv (ZappedProv _)      = emptyNameSet
+    -- [ZappedCoDifference] Zapped coercions refer to no orphan names, even if the
+    -- original contained such names.
 
 orphNamesOfCos :: [Coercion] -> NameSet
 orphNamesOfCos = orphNamesOfThings orphNamesOfCo


=====================================
compiler/coreSyn/CoreLint.hs
=====================================
@@ -1788,6 +1788,7 @@ lintCoercion co@(UnivCo prov r ty1 ty2)
                                     ; check_kinds kco k1 k2 }
 
            PluginProv _     -> return ()  -- no extra checks
+           ZappedProv fvs   -> mapM_ lintTyCoVarInScope (dVarSetElems fvs)
 
        ; when (r /= Phantom && classifiesTypeWithValues k1
                             && classifiesTypeWithValues k2)
@@ -2014,7 +2015,6 @@ lintCoercion (HoleCo h)
   = do { addErrL $ text "Unfilled coercion hole:" <+> ppr h
        ; lintCoercion (CoVarCo (coHoleCoVar h)) }
 
-
 ----------
 lintUnliftedCoVar :: CoVar -> LintM ()
 lintUnliftedCoVar cv


=====================================
compiler/coreSyn/CoreOpt.hs
=====================================
@@ -1200,13 +1200,15 @@ pushCoTyArg co ty
        -- tyL = forall (a1 :: k1). ty1
        -- tyR = forall (a2 :: k2). ty2
 
-    co1 = mkSymCo (mkNthCo Nominal 0 co)
+    zap = zapCoercion unsafeGlobalDynFlags
+
+    co1 = zap $ mkSymCo (mkNthCo Nominal 0 co)
        -- co1 :: k2 ~N k1
        -- Note that NthCo can extract a Nominal equality between the
        -- kinds of the types related by a coercion between forall-types.
        -- See the NthCo case in CoreLint.
 
-    co2 = mkInstCo co (mkGReflLeftCo Nominal ty co1)
+    co2 = zap $ mkInstCo co (mkGReflLeftCo Nominal ty co1)
         -- co2 :: ty1[ (ty|>co1)/a1 ] ~ ty2[ ty/a2 ]
         -- Arg of mkInstCo is always nominal, hence mkNomReflCo
 


=====================================
compiler/iface/IfaceEnv.hs
=====================================
@@ -226,7 +226,7 @@ tcIfaceLclId occ
   = do  { lcl <- getLclEnv
         ; case (lookupFsEnv (if_id_env lcl) occ) of
             Just ty_var -> return ty_var
-            Nothing     -> failIfM (text "Iface id out of scope: " <+> ppr occ)
+            Nothing     -> failIfM (text "Iface id out of scope: " <+> ppr occ $$ ppr (if_id_env lcl))
         }
 
 extendIfaceIdEnv :: [Id] -> IfL a -> IfL a


=====================================
compiler/iface/IfaceSyn.hs
=====================================
@@ -1530,6 +1530,9 @@ freeNamesIfProv IfaceUnsafeCoerceProv    = emptyNameSet
 freeNamesIfProv (IfacePhantomProv co)    = freeNamesIfCoercion co
 freeNamesIfProv (IfaceProofIrrelProv co) = freeNamesIfCoercion co
 freeNamesIfProv (IfacePluginProv _)      = emptyNameSet
+freeNamesIfProv (IfaceZappedProv _ _)    = emptyNameSet
+  -- [ZappedCoDifference]: This won't report top-level names present in the
+  -- unzapped proof but not its kind.
 
 freeNamesIfVarBndr :: VarBndr IfaceBndr vis -> NameSet
 freeNamesIfVarBndr (Bndr bndr _) = freeNamesIfBndr bndr


=====================================
compiler/iface/IfaceType.hs
=====================================
@@ -335,6 +335,13 @@ data IfaceUnivCoProv
   | IfacePhantomProv IfaceCoercion
   | IfaceProofIrrelProv IfaceCoercion
   | IfacePluginProv String
+  | IfaceZappedProv [IfLclName] [CoVar]
+    -- ^ @local cvs, free cvs@
+    --
+    -- 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].
+    -- See Note [Zapping coercions] in TyCoRep.
 
 {- Note [Holes in IfaceCoercion]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -510,6 +517,9 @@ substIfaceType env ty
     go_prov (IfacePhantomProv co)    = IfacePhantomProv (go_co co)
     go_prov (IfaceProofIrrelProv co) = IfaceProofIrrelProv (go_co co)
     go_prov (IfacePluginProv str)    = IfacePluginProv str
+    go_prov (IfaceZappedProv cvs fCvs)
+                                     = IfaceZappedProv
+                                         cvs fCvs
 
 substIfaceAppArgs :: IfaceTySubst -> IfaceAppArgs -> IfaceAppArgs
 substIfaceAppArgs env args
@@ -1533,6 +1543,11 @@ pprIfaceUnivCoProv (IfaceProofIrrelProv co)
   = text "irrel" <+> pprParendIfaceCoercion co
 pprIfaceUnivCoProv (IfacePluginProv s)
   = text "plugin" <+> doubleQuotes (text s)
+pprIfaceUnivCoProv (IfaceZappedProv cvs fCvs)
+  = text "Zapped" <> brackets (whenPprDebug fvsDoc)
+  where
+    fvsDoc = text "free covars:" <+> ppr cvs
+          $$ text "open free covars:" <+> ppr fCvs
 
 -------------------
 instance Outputable IfaceTyCon where
@@ -1879,6 +1894,11 @@ instance Binary IfaceUnivCoProv where
   put_ bh (IfacePluginProv a) = do
           putByte bh 4
           put_ bh a
+  put_ bh (IfaceZappedProv coFvs _) = do
+          putByte bh 5
+          put_ bh coFvs
+          -- N.B. Free variables aren't serialised; see Note [Free tyvars in
+          -- IfaceType].
 
   get bh = do
       tag <- getByte bh
@@ -1890,6 +1910,10 @@ instance Binary IfaceUnivCoProv where
                    return $ IfaceProofIrrelProv a
            4 -> do a <- get bh
                    return $ IfacePluginProv a
+           5 -> do a <- get bh
+                   -- N.B. Free variables aren't serialised; see Note [Free
+                   -- tyvars in IfaceType].
+                   return $ IfaceZappedProv a []
            _ -> panic ("get IfaceUnivCoProv " ++ show tag)
 
 


=====================================
compiler/iface/TcIface.hs
=====================================
@@ -1209,7 +1209,12 @@ tcIfaceTyLit (IfaceStrTyLit n) = return (StrTyLit n)
 -}
 
 tcIfaceCo :: IfaceCoercion -> IfL Coercion
-tcIfaceCo = go
+tcIfaceCo = \co0 -> do
+    dflags <- getDynFlags
+    co <- go co0
+    if shouldBuildCoercions dflags
+      then return co
+      else return $ zapCoercion dflags co
   where
     go_mco IfaceMRefl    = pure MRefl
     go_mco (IfaceMCo co) = MCo <$> (go co)
@@ -1250,6 +1255,7 @@ tcIfaceUnivCoProv IfaceUnsafeCoerceProv     = return UnsafeCoerceProv
 tcIfaceUnivCoProv (IfacePhantomProv kco)    = PhantomProv <$> tcIfaceCo kco
 tcIfaceUnivCoProv (IfaceProofIrrelProv kco) = ProofIrrelProv <$> tcIfaceCo kco
 tcIfaceUnivCoProv (IfacePluginProv str)     = return $ PluginProv str
+tcIfaceUnivCoProv (IfaceZappedProv coFvs _) = ZappedProv . mkDVarSet <$> mapM tcIfaceLclId coFvs
 
 {-
 ************************************************************************


=====================================
compiler/iface/ToIface.hs
=====================================
@@ -275,6 +275,13 @@ toIfaceCoercionX fr co
     go_prov (PhantomProv co)    = IfacePhantomProv (go co)
     go_prov (ProofIrrelProv co) = IfaceProofIrrelProv (go co)
     go_prov (PluginProv str)    = IfacePluginProv str
+    go_prov (ZappedProv fvs)    = IfaceZappedProv cvs fCvs
+                          where
+                            (fCvs, cvs) = partitionWith f $ dVarSetElems fvs
+                            isFree = (`elemVarSet` fr)
+                            f v | ASSERT(isCoVar v)
+                                  isFree v  = Left v
+                                | otherwise = Right $ toIfaceCoVar v
 
 toIfaceTcArgs :: TyCon -> [Type] -> IfaceAppArgs
 toIfaceTcArgs = toIfaceTcArgsX emptyVarSet


=====================================
compiler/main/DynFlags.hs
=====================================
@@ -1,5 +1,6 @@
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
 
 -------------------------------------------------------------------------------
 --
@@ -45,6 +46,7 @@ module DynFlags (
         DynFlags(..),
         FlagSpec(..),
         HasDynFlags(..), ContainsDynFlags(..),
+        DynFlagsEnvM, runDynFlagsEnvM,
         RtsOptsEnabled(..),
         HscTarget(..), isObjectTarget, defaultObjectTarget,
         targetRetainsAllBindings,
@@ -63,6 +65,7 @@ module DynFlags (
         makeDynFlagsConsistent,
         shouldUseColor,
         shouldUseHexWordLiterals,
+        shouldBuildCoercions,
         positionIndependent,
         optimisationFlags,
 
@@ -501,6 +504,7 @@ data GeneralFlag
    | Opt_D_faststring_stats
    | Opt_D_dump_minimal_imports
    | Opt_DoCoreLinting
+   | Opt_DropCoercions
    | Opt_DoStgLinting
    | Opt_DoCmmLinting
    | Opt_DoAsmLinting
@@ -1358,6 +1362,17 @@ instance (Monad m, HasDynFlags m) => HasDynFlags (MaybeT m) where
 instance (Monad m, HasDynFlags m) => HasDynFlags (ExceptT e m) where
     getDynFlags = lift getDynFlags
 
+-- | A reader monad over 'DynFlags'.
+newtype DynFlagsEnvM a = DynFlagsEnvM (Reader DynFlags a)
+                       deriving (Functor, Applicative, Monad)
+
+instance HasDynFlags DynFlagsEnvM where
+    getDynFlags = DynFlagsEnvM ask
+
+runDynFlagsEnvM :: DynFlags -> DynFlagsEnvM a -> a
+runDynFlagsEnvM dflags (DynFlagsEnvM m) = runReader m dflags
+
+
 class ContainsDynFlags t where
     extractDynFlags :: t -> DynFlags
 
@@ -1687,6 +1702,14 @@ shouldUseHexWordLiterals :: DynFlags -> Bool
 shouldUseHexWordLiterals dflags =
   Opt_HexWordLiterals `EnumSet.member` generalFlags dflags
 
+-- | Should we generate coercions?
+--
+-- See Note [Zapping coercions] for details.
+shouldBuildCoercions :: DynFlags -> Bool
+shouldBuildCoercions dflags =
+    gopt Opt_DoCoreLinting dflags && not (gopt Opt_DropCoercions dflags)
+    -- TODO: Add flag to explicitly enable coercion generation without linting?
+
 -- | Are we building with @-fPIE@ or @-fPIC@ enabled?
 positionIndependent :: DynFlags -> Bool
 positionIndependent dflags = gopt Opt_PIC dflags || gopt Opt_PIE dflags
@@ -3463,6 +3486,8 @@ dynamic_flags_deps = [
         (setDumpFlag Opt_D_dump_rtti)
   , make_ord_flag defGhcFlag "dcore-lint"
         (NoArg (setGeneralFlag Opt_DoCoreLinting))
+  , make_ord_flag defGhcFlag "ddrop-coercions"
+        (NoArg (setGeneralFlag Opt_DropCoercions))
   , make_ord_flag defGhcFlag "dstg-lint"
         (NoArg (setGeneralFlag Opt_DoStgLinting))
   , make_ord_flag defGhcFlag "dcmm-lint"


=====================================
compiler/typecheck/TcFlatten.hs
=====================================
@@ -22,10 +22,12 @@ import Var
 import VarSet
 import VarEnv
 import Outputable
+import DynFlags
 import TcSMonad as TcS
 import BasicTypes( SwapFlag(..) )
 
 import Util
+import Pair
 import Bag
 import Control.Monad
 import MonadUtils    ( zipWith3M )
@@ -498,6 +500,9 @@ instance Applicative FlatM where
   pure x = FlatM $ const (pure x)
   (<*>) = ap
 
+instance HasDynFlags FlatM where
+  getDynFlags = liftTcS getDynFlags
+
 liftTcS :: TcS a -> FlatM a
 liftTcS thing_inside
   = FlatM $ const thing_inside
@@ -1330,7 +1335,7 @@ flatten_exact_fam_app_fully tc tys
   -- See Note [Reduce type family applications eagerly]
      -- the following tcTypeKind should never be evaluated, as it's just used in
      -- casting, and casts by refl are dropped
-  = do { mOut <- try_to_reduce_nocache tc tys
+  = do { mOut <- try_to_reduce_nocache tc tys emptyDVarSet
        ; case mOut of
            Just out -> pure out
            Nothing -> do
@@ -1374,6 +1379,7 @@ flatten_exact_fam_app_fully tc tys
                    _ -> do { mOut <- try_to_reduce tc
                                                    xis
                                                    kind_co
+                                                   (tyCoVarsOfCoDSet ret_co)
                                                    (`mkTransCo` ret_co)
                            ; case mOut of
                                Just out -> pure out
@@ -1419,11 +1425,18 @@ flatten_exact_fam_app_fully tc tys
                                -- where
                                -- orig_args is what was passed to the outer
                                -- function
+                  -> DTyCoVarSet  -- free variables of ret_co
                   -> (   Coercion     -- :: (xi |> kind_co) ~ F args
                       -> Coercion )   -- what to return from outer function
                   -> FlatM (Maybe (Xi, Coercion))
-    try_to_reduce tc tys kind_co update_co
-      = do { checkStackDepth (mkTyConApp tc tys)
+    try_to_reduce tc tys kind_co ret_co_fvs update_co
+      = do { let fvs = filterDVarSet isCoVar $ tyCoVarsOfTypesDSet tys
+                       `unionDVarSet` tyCoVarsOfCoDSet kind_co
+                       `unionDVarSet` ret_co_fvs
+                     -- See Note [Zapping coercions] in TyCoRep
+                 fam_ty = mkTyConApp tc tys
+           ; checkStackDepth (mkTyConApp tc tys)
+           ; dflags <- getDynFlags
            ; mb_match <- liftTcS $ matchFam tc tys
            ; case mb_match of
                  -- NB: norm_co will always be homogeneous. All type families
@@ -1443,18 +1456,25 @@ flatten_exact_fam_app_fully tc tys
                        ; when (eq_rel == NomEq) $
                          liftTcS $
                          extendFlatCache tc tys ( co, xi, flavour )
-                       ; let role = eqRelRole eq_rel
-                             xi' = xi `mkCastTy` kind_co
-                             co' = update_co $
-                                   mkTcCoherenceLeftCo role xi kind_co (mkSymCo co)
-                       ; return $ Just (xi', co') }
+                       ; let xi' = xi `mkCastTy` kind_co
+                             role = eqRelRole eq_rel
+                             -- See Note [Zapping coercions]
+                             co' = mkZappedCoercion dflags (mkSymCo co) (Pair xi' fam_ty) Nominal fvs
+                             co'' = update_co $ mkTcCoherenceLeftCo role xi kind_co co'
+                       ; return $ Just (xi', co'') }
                Nothing -> pure Nothing }
 
     try_to_reduce_nocache :: TyCon   -- F, family tycon
                           -> [Type]  -- args, not necessarily flattened
+                          -> DTyCoVarSet -- free variables of ret_co
                           -> FlatM (Maybe (Xi, Coercion))
-    try_to_reduce_nocache tc tys
-      = do { checkStackDepth (mkTyConApp tc tys)
+    try_to_reduce_nocache tc tys fvs_ret_co
+      = do { let fvs = filterDVarSet isCoVar $ tyCoVarsOfTypesDSet tys
+                       `unionDVarSet` fvs_ret_co
+                     -- See Note [Zapping coercions] in TyCoRep
+                 fam_ty = mkTyConApp tc tys
+           ; checkStackDepth fam_ty
+           ; dflags <- getDynFlags
            ; mb_match <- liftTcS $ matchFam tc tys
            ; case mb_match of
                  -- NB: norm_co will always be homogeneous. All type families
@@ -1464,7 +1484,8 @@ flatten_exact_fam_app_fully tc tys
                        ; eq_rel <- getEqRel
                        ; let co  = mkSymCo (maybeSubCo eq_rel norm_co
                                             `mkTransCo` mkSymCo final_co)
-                       ; return $ Just (xi, co) }
+                             co' = mkZappedCoercion dflags co (Pair xi fam_ty) Nominal fvs
+                       ; return $ Just (xi, co') }
                Nothing -> pure Nothing }
 
 {- Note [Reduce type family applications eagerly]


=====================================
compiler/typecheck/TcHsType.hs
=====================================
@@ -65,6 +65,7 @@ module TcHsType (
 
 import GhcPrelude
 
+import DynFlags
 import HsSyn
 import TcRnMonad
 import TcEvidence


=====================================
compiler/typecheck/TcTyDecls.hs
=====================================
@@ -138,6 +138,9 @@ synonymTyConsOfType ty
      go_prov (PhantomProv co)     = go_co co
      go_prov (ProofIrrelProv co)  = go_co co
      go_prov (PluginProv _)       = emptyNameEnv
+     go_prov (ZappedProv _)       = emptyNameEnv
+      -- [ZappedCoDifference]: This won't report type synonyms present in the
+      -- unzapped proof but not its kind.
 
      go_tc tc | isTypeSynonymTyCon tc = unitNameEnv (tyConName tc) tc
               | otherwise             = emptyNameEnv


=====================================
compiler/typecheck/TcType.hs
=====================================
@@ -1020,6 +1020,7 @@ exactTyCoVarsOfType ty
     goProv (PhantomProv kco)    = goCo kco
     goProv (ProofIrrelProv kco) = goCo kco
     goProv (PluginProv _)       = emptyVarSet
+    goProv (ZappedProv _)       = emptyVarSet -- TODO
 
     goVar v = unitVarSet v `unionVarSet` go (varType v)
 


=====================================
compiler/types/Coercion.hs
=====================================
@@ -97,6 +97,9 @@ module Coercion (
         -- ** Forcing evaluation of coercions
         seqCo,
 
+        -- ** Eliding coercions
+        zapCoercion,
+
         -- * Pretty-printing
         pprCo, pprParendCo,
         pprCoAxiom, pprCoAxBranch, pprCoAxBranchLHS,
@@ -970,6 +973,8 @@ mkSymCo :: Coercion -> Coercion
 mkSymCo co | isReflCo co          = co
 mkSymCo    (SymCo co)             = co
 mkSymCo    (SubCo (SymCo co))     = SubCo co
+mkSymCo (UnivCo (ZappedProv fvs) r t1 t2) = UnivCo (ZappedProv fvs) r t2 t1
+-- TODO: Handle other provenances
 mkSymCo co                        = SymCo co
 
 -- | Create a new 'Coercion' by composing the two given 'Coercion's transitively.
@@ -1114,6 +1119,10 @@ nthCoRole n co
     (Pair lty _, r) = coercionKindRole co
 
 mkLRCo :: LeftOrRight -> Coercion -> Coercion
+mkLRCo lr (UnivCo (ZappedProv fvs) r t1 t2)
+                       = UnivCo (ZappedProv fvs) r
+                                (pickLR lr (splitAppTy t1))
+                                (pickLR lr (splitAppTy t2))
 mkLRCo lr co
   | Just (ty, eq) <- isReflCo_maybe co
   = mkReflCo eq (pickLR lr (splitAppTy ty))
@@ -1170,6 +1179,7 @@ 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 (UnivCo (ZappedProv fvs) _ ty1 ty2) = mkUnivCo (ZappedProv fvs) Nominal (typeKind ty1) (typeKind ty2)
 mkKindCo co
   | Pair ty1 ty2 <- coercionKind co
        -- generally, calling coercionKind during coercion creation is a bad idea,
@@ -1193,6 +1203,7 @@ mkSubCo (FunCo Nominal arg res)
   = FunCo Representational
           (downgradeRole Representational Nominal arg)
           (downgradeRole Representational Nominal res)
+mkSubCo (UnivCo (ZappedProv fvs) Nominal t1 t2) = UnivCo (ZappedProv fvs) Representational t1 t2
 mkSubCo co = ASSERT2( coercionRole co == Nominal, ppr co <+> ppr (coercionRole co) )
              SubCo co
 
@@ -1293,6 +1304,7 @@ setNominalRole_maybe r co
                      PhantomProv _    -> False  -- should always be phantom
                      ProofIrrelProv _ -> True   -- it's always safe
                      PluginProv _     -> False  -- who knows? This choice is conservative.
+                     ZappedProv _     -> False  -- conservatively say no
       = Just $ UnivCo prov Nominal co1 co2
     setNominalRole_maybe_helper _ = Nothing
 
@@ -1400,6 +1412,7 @@ promoteCoercion co = case co of
     UnivCo (PhantomProv kco) _ _ _    -> kco
     UnivCo (ProofIrrelProv kco) _ _ _ -> kco
     UnivCo (PluginProv _) _ _ _       -> mkKindCo co
+    UnivCo (ZappedProv _) _ _ _       -> mkKindCo co
 
     SymCo g
       -> mkSymCo (promoteCoercion g)
@@ -2157,6 +2170,7 @@ seqProv UnsafeCoerceProv    = ()
 seqProv (PhantomProv co)    = seqCo co
 seqProv (ProofIrrelProv co) = seqCo co
 seqProv (PluginProv _)      = ()
+seqProv (ZappedProv fvs)    = seqDVarSet fvs
 
 seqCos :: [Coercion] -> ()
 seqCos []       = ()


=====================================
compiler/types/Coercion.hs-boot
=====================================
@@ -49,4 +49,5 @@ liftCoSubst :: HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion
 seqCo :: Coercion -> ()
 
 coercionKind :: Coercion -> Pair Type
+coercionKindRole :: Coercion -> (Pair Type, Role)
 coercionType :: Coercion -> Type


=====================================
compiler/types/FamInstEnv.hs
=====================================
@@ -1747,6 +1747,9 @@ allTyCoVarsInTy = go
     go_prov (PhantomProv co)    = go_co co
     go_prov (ProofIrrelProv co) = go_co co
     go_prov (PluginProv _)      = emptyVarSet
+    go_prov (ZappedProv _)      = emptyVarSet
+                                  -- We don't track free type variables, only
+                                  -- coercion variables.
 
 mkFlattenFreshTyName :: Uniquable a => a -> Name
 mkFlattenFreshTyName unq


=====================================
compiler/types/OptCoercion.hs
=====================================
@@ -108,8 +108,8 @@ optCoercion :: DynFlags -> TCvSubst -> Coercion -> NormalCo
 -- ^ optCoercion applies a substitution to a coercion,
 --   *and* optimises it to reduce its size
 optCoercion dflags env co
-  | hasNoOptCoercion dflags = substCo env co
-  | otherwise               = optCoercion' env co
+  | hasNoOptCoercion dflags           = substCo env co
+  | otherwise                         = optCoercion' env co
 
 optCoercion' :: TCvSubst -> Coercion -> NormalCo
 optCoercion' env co
@@ -497,6 +497,14 @@ opt_univ env sym (PhantomProv h) _r ty1 ty2
     ty1' = substTy (lcSubstLeft  env) ty1
     ty2' = substTy (lcSubstRight env) ty2
 
+opt_univ env sym (ZappedProv fvs) role ty1 ty2
+  | sym       = mkUnivCo (ZappedProv fvs') role ty2' ty1'
+  | otherwise = mkUnivCo (ZappedProv fvs') role ty1' ty2'
+  where
+    ty1' = substTy (lcSubstLeft env) ty1
+    ty2' = substTy (lcSubstRight env) ty2
+    fvs' = substFreeDVarSet (lcTCvSubst env) fvs
+
 opt_univ env sym prov role oty1 oty2
   | Just (tc1, tys1) <- splitTyConApp_maybe oty1
   , Just (tc2, tys2) <- splitTyConApp_maybe oty2
@@ -557,6 +565,7 @@ opt_univ env sym prov role oty1 oty2
       PhantomProv kco    -> PhantomProv $ opt_co4_wrap env sym False Nominal kco
       ProofIrrelProv kco -> ProofIrrelProv $ opt_co4_wrap env sym False Nominal kco
       PluginProv _       -> prov
+      ZappedProv fvs     -> ZappedProv $ substFreeDVarSet (lcTCvSubst env) fvs
 
 -------------
 opt_transList :: InScopeSet -> [NormalCo] -> [NormalCo] -> [NormalCo]
@@ -639,6 +648,8 @@ opt_trans_rule is in_co1@(UnivCo p1 r1 tyl1 _tyr1)
     opt_trans_prov (ProofIrrelProv kco1) (ProofIrrelProv kco2)
       = Just $ ProofIrrelProv $ opt_trans is kco1 kco2
     opt_trans_prov (PluginProv str1)     (PluginProv str2)     | str1 == str2 = Just p1
+    opt_trans_prov (ZappedProv fvs1)     (ZappedProv fvs2)
+      = Just $ ZappedProv $ fvs1 `unionDVarSet` fvs2
     opt_trans_prov _ _ = Nothing
 
 -- Push transitivity down through matching top-level constructors.


=====================================
compiler/types/TyCoRep.hs
=====================================
@@ -40,6 +40,7 @@ module TyCoRep (
         CoercionHole(..), coHoleCoVar, setCoHoleCoVar,
         CoercionN, CoercionR, CoercionP, KindCoercion,
         MCoercion(..), MCoercionR, MCoercionN,
+        mkZappedCoercion, zapCoercion,
 
         -- * Functions over types
         mkTyConTy, mkTyVarTy, mkTyVarTys,
@@ -132,6 +133,7 @@ module TyCoRep (
         substCoVarBndr,
         substTyVar, substTyVars, substTyCoVars,
         substForAllCoBndr,
+        substFreeDVarSet,
         substVarBndrUsing, substForAllCoBndrUsing,
         checkValidSubst, isValidTCvSubst,
 
@@ -162,7 +164,7 @@ import {-# SOURCE #-} Type( isCoercionTy, mkAppTy, mkCastTy
                           , tyCoVarsOfTypeWellScoped
                           , tyCoVarsOfTypesWellScoped
                           , scopedSort
-                          , coreView )
+                          , coreView, eqType )
    -- Transitively pulls in a LOT of stuff, better to break the loop
 
 import {-# SOURCE #-} Coercion
@@ -197,6 +199,7 @@ import UniqSet
 -- libraries
 import qualified Data.Data as Data hiding ( TyCon )
 import Data.List
+import Data.Maybe ( fromMaybe )
 import Data.IORef ( IORef )   -- for CoercionHole
 
 {-
@@ -1646,6 +1649,11 @@ data UnivCoProvenance
   | PluginProv String  -- ^ From a plugin, which asserts that this coercion
                        --   is sound. The string is for the use of the plugin.
 
+  | ZappedProv DVarSet
+    -- ^ See Note [Zapping coercions].
+    -- Free coercion variables must be tracked in 'DVarSet' since
+    -- they appear in interface files.
+
   deriving Data.Data
 
 instance Outputable UnivCoProvenance where
@@ -1653,6 +1661,7 @@ instance Outputable UnivCoProvenance where
   ppr (PhantomProv _)    = text "(phantom)"
   ppr (ProofIrrelProv _) = text "(proof irrel.)"
   ppr (PluginProv str)   = parens (text "plugin" <+> brackets (text str))
+  ppr (ZappedProv fvs)   = parens (text "zapped" <+> brackets (ppr fvs))
 
 -- | A coercion to be filled in by the type-checker. See Note [Coercion holes]
 data CoercionHole
@@ -1796,8 +1805,232 @@ Here,
   where
     co5 :: (a1 ~ Bool) ~ (a2 ~ Bool)
     co5 = TyConAppCo Nominal (~#) [<*>, <*>, co4, <Bool>]
+-}
+
+{-
+%************************************************************************
+%*                                                                      *
+                 Zapping coercions into oblivion
+%*                                                                      *
+%************************************************************************
+-}
+
+{- Note [Zapping coercions]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Coercions for even small programs can grow to be quite large (e.g. #8095),
+especially when type families are involved. For instance, the case of addition
+of inductive naturals can build coercions quadratic in size of the summands.
+For instance, consider the type-level addition operation defined on Peano naturals,
+
+    data Nat = Z | Succ Nat
+
+    type family (+) (a :: Nat) (b :: Nat)
+    type instance (+) Z        a   = a                -- CoAx1
+    type instance (+) (Succ a) b   = Succ (a + b)     -- CoAx2
+
+Now consider what is necessary to reduce (S (S (S Z)) + S Z). This
+reduction will produce two results: the reduced (i.e. flattened) type, and a
+coercion witnessing the reduction. The reduction will proceed as follows:
+
+       S (S (S Z)) + S Z       |>              Refl
+    ~> S (S (S Z) + S Z)       |>              CoAx2 Refl
+    ~> S (S (S Z + S Z))       |>              CoAx2 (CoAx2 Refl)
+    ~> S (S (S (Z + S Z)))     |>              CoAx2 (CoAx2 (CoAx2 Refl))
+    ~> S (S (S (S (S Z))))     |>              CoAx1 (CoAx2 (CoAx2 (CoAx2 Refl)))
+
+Note that when we are building coercions [TODO]
+
+Moreover, coercions are really only useful when validating core transformations
+(i.e. by the Core Linter). To avoid burdening users who aren't linting with the
+cost of maintaining these structures, we replace coercions with placeholders
+("zap" them) them unless -dcore-lint is enabled. These placeholders are
+represented by UnivCo with ZappedProv provenance. Concretely, a coercion
+
+    co :: t1 ~r t2
+
+is replaced by
+
+    UnivCo (ZappedProv fvs) r t1 t2
+
+To ensure that such coercions aren't floated out of the scope of proofs they
+require, the ZappedProv constructor includes the coercion's set of free coercion
+variables (as a DVarSet, since these sets are included in interface files).
+
+
+Zapping during type family reduction
+------------------------------------
+
+To avoid the quadratic blow-up in coercion size during type family reduction
+described above, we zap on every type family reduction step taken by
+TcFlatten.flatten_exact_fam_app_fully. When zapping we take care to avoid
+looking at the constructed coercion and instead build up a zapped coercion
+directly from type being reduced, its free variables, and the result of the
+reduction. This allows us to reduce recursive type families in time linear to
+the size of the type at the expense of Core Lint's ability to validate the
+reduction.
+
+Note that the free variable set of the zapped coercion is taken to be the free
+variable set of the unreduced family application, which is computed once at the
+beginning of reduction. This is an important optimisation as it allows us to
+avoid recomputing the free variable set (which requires linear work in the size
+of the coercion) with every reduction step. Moreover, this gives us the same
+result as naively computing the free variables of every reduction:
+
+  * The FV set of the unreduced type cannot be smaller than that of the reduced type
+    because there is nowhere for extra FVs to come from. Type family equations
+    are essentially function reduction, which can never introduce new fvs.
+
+  * The FV set of the unreducecd type cannot be larger than that of the reduced
+    type because the zapped coercion's kind must mention the types these fvs come
+    from, so the FVs of the zapped coercion must be at least those in the
+    starting types.
+
+Thus, the two sets are subsets of each other and are equal.
+
+
+Other places where we zap
+-------------------------
 
+Besides during type family reduction, we also zap coercions in a number of other
+places (again, only when DynFlags.shouldBuildCoercions is False). This zapping
+occurs in zapCoercion, which maps a coercion to its zapped form. However, there
+are a few optimisations which we implement:
 
+  * We don't zap coercions which are already zapping; this avoids an unnecessary
+    free variable computation.
+
+  * We don't zap Refl coercions. This is because Refls are actually far more
+    compact than zapped coercions: the coercion (Refl T) holds only one
+    reference to T, whereas its zapped equivalent would hold two. While this
+    makes little difference directly after construction due to sharing, this
+    sharing will be lost when we substitute or otherwise manipulate the zapped
+    coercion, resulting in a doubling of the coercions representation size.
+
+zapCoercion is called in a few places:
+
+  * CoreOpt.pushCoTyArg zaps the coercions it produces to avoid pile-up during
+    simplification [TODO]
+
+  * TcIface.tcIfaceCo
+
+  * Type.mapCoercion (which is used by zonking) can optionally zap coercions,
+    although this is currently disabled since it causes compiler allocations to
+    regress in a few cases.
+
+  * We considered zapping as well in optCoercion, although this too caused
+    significant allocation regressions.
+
+The importance of tracking free coercion variables
+--------------------------------------------------
+
+It is quite important that zapped coercions track their free coercion variables.
+To see why, consider this program:
+
+    data T a where
+      T1 :: Bool -> T Bool
+      T2 :: T Int
+
+    f :: T a -> a -> Bool
+    f = /\a (x:T a) (y:a).
+        case x of
+              T1 (c : a~Bool) (z : Bool) -> not (y |> c)
+              T2 -> True
+
+Now imagine that we zap the coercion `c`, replacing it with a generic UnivCo
+between `a` and Bool. If we didn't record the fact that this coercion was
+previously free in `c`, we may incorrectly float the expression `not (y |> c)`
+out of the case alternative which brings proof of `c` into scope. If this
+happened then `f T2 (I# 5)` would try to interpret `y` as a Bool, at
+which point we aren't far from a segmentation fault or much worse.
+
+Note that we don't need to track the coercion's free *type* variables. This
+means that we may float past type variables which the original proof had as free
+variables. While surprising, this doesn't jeopardise the validity of the
+coercion, which only depends upon the scoping relative to the free coercion
+variables.
+
+
+Differences between zapped and unzapped coercions
+-------------------------------------------------
+
+Alas, sometimes zapped coercions will behave slightly differently from their
+unzapped counterparts. Specifically, we are a bit lax in tracking external names
+that are present in the unzapped coercion but not its kind. This manifests in a
+few places (these are labelled in the source with the [ZappedCoDifference]
+keyword):
+
+ * Since we only track a zapped coercion's free *coercion* variables, the
+   simplifier may float such coercions farther than it would have if the proof
+   were present.
+
+ * IfaceSyn.freeNamesIfCoercion will fail to report top-level names present in
+   the unzapped proof but not its kind.
+
+ * TcTyDecls.synonymTyConsOfType will fail to report type synonyms present in
+   in the unzapped proof but not its kind.
+
+ * The result of TcValidity.fvCo will contain each free variable of a ZappedCo
+   only once, even if it would have reported multiple occurrences in the
+   unzapped coercion.
+
+ * Type.tyConsOfType does not report TyCons which appear only in the unzapped
+   proof and not its kind.
+
+ * Zapped coercions are represented in interface files as IfaceZappedProv. This
+   representation only includes local free variables, since these are sufficient
+   to avoid unsound floating. This means that the free variable lists of zapped
+   coercions loaded from interface files will lack top-level things (e.g. type
+   constructors) that appear only in the unzapped proof.
+
+-}
+
+-- | Make a zapped coercion if building of coercions is disabled, otherwise
+-- return the given un-zapped coercion.
+mkZappedCoercion :: HasDebugCallStack
+                 => DynFlags
+                 -> Coercion  -- ^ the un-zapped coercion
+                 -> Pair Type -- ^ the kind of the coercion
+                 -> Role      -- ^ the role of the coercion
+                 -> DCoVarSet -- ^ the free coercion variables of the coercion
+                 -> Coercion
+mkZappedCoercion dflags co (Pair ty1 ty2) role fCvs
+  | debugIsOn && not is_ok =
+    pprPanic "mkZappedCoercion" $ 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_fCvs
+    , text "given free co vars:" <+> ppr fCvs
+    ]
+  | shouldBuildCoercions dflags = co
+  | otherwise =
+    mkUnivCo (ZappedProv fCvs) role ty1 ty2
+  where
+    (Pair real_ty1 real_ty2, real_role) = coercionKindRole co
+    real_fCvs = filterVarSet isCoVar (coVarsOfCo co)
+    is_ok =
+           real_role == role
+        && (real_ty1 `eqType` ty1)
+        && (real_ty2 `eqType` ty2)
+        -- It's not generally possible to compute the actual free variable set
+        -- since we may encounter flattening skolems during reduction.
+        -- && dVarSetToVarSet fCvs == real_fCvs
+
+-- | Replace a coercion with a zapped coercion unless coercions are needed.
+zapCoercion :: DynFlags -> Coercion -> Coercion
+zapCoercion _ co@(UnivCo (ZappedProv _) _ _ _) = co  -- already zapped
+zapCoercion _ co@(Refl _) = co  -- Refl is smaller than zapped coercions
+zapCoercion dflags co =
+    mkZappedCoercion dflags co (Pair t1 t2) role fvs
+  where
+    (Pair t1 t2, role) = coercionKindRole co
+    fvs = filterDVarSet isCoVar $ tyCoVarsOfCoDSet co
+
+{-
 %************************************************************************
 %*                                                                      *
                  Free variables of types and coercions
@@ -1820,7 +2053,7 @@ instead do so at call sites, but it seems that we always want to do
 so, so it's easiest to do it here.
 
 It turns out that getting the free variables of types is performance critical,
-so we profiled several versions, exploring different implementation strategies.
+o we profiled several versions, exploring different implementation strategies.
 
 1. Baseline version: uses FV naively. Essentially:
 
@@ -2013,6 +2246,7 @@ ty_co_vars_of_prov (PhantomProv co)    is acc = ty_co_vars_of_co co is acc
 ty_co_vars_of_prov (ProofIrrelProv co) is acc = ty_co_vars_of_co co is acc
 ty_co_vars_of_prov UnsafeCoerceProv    _  acc = acc
 ty_co_vars_of_prov (PluginProv _)      _  acc = acc
+ty_co_vars_of_prov (ZappedProv fvs)    _  acc = dVarSetToVarSet fvs
 
 -- | Generates an in-scope set from the free variables in a list of types
 -- and a list of coercions
@@ -2160,6 +2394,7 @@ tyCoFVsOfProv UnsafeCoerceProv    fv_cand in_scope acc = emptyFV fv_cand in_scop
 tyCoFVsOfProv (PhantomProv co)    fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
 tyCoFVsOfProv (ProofIrrelProv co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
 tyCoFVsOfProv (PluginProv _)      fv_cand in_scope acc = emptyFV fv_cand in_scope acc
+tyCoFVsOfProv (ZappedProv fvs)    fv_cand in_scope acc = (mkFVs $ dVarSetElems fvs) fv_cand in_scope acc
 
 tyCoFVsOfCos :: [Coercion] -> FV
 tyCoFVsOfCos []       fv_cand in_scope acc = emptyFV fv_cand in_scope acc
@@ -2265,6 +2500,7 @@ almost_devoid_co_var_of_prov (ProofIrrelProv co) cv
   = almost_devoid_co_var_of_co co cv
 almost_devoid_co_var_of_prov UnsafeCoerceProv _ = True
 almost_devoid_co_var_of_prov (PluginProv _) _ = True
+almost_devoid_co_var_of_prov (ZappedProv fvs) cv = cv `elemDVarSet` fvs
 
 almost_devoid_co_var_of_type :: Type -> CoVar -> Bool
 almost_devoid_co_var_of_type (TyVarTy _) _ = True
@@ -2651,6 +2887,7 @@ noFreeVarsOfProv UnsafeCoerceProv    = True
 noFreeVarsOfProv (PhantomProv co)    = noFreeVarsOfCo co
 noFreeVarsOfProv (ProofIrrelProv co) = noFreeVarsOfCo co
 noFreeVarsOfProv (PluginProv {})     = True
+noFreeVarsOfProv (ZappedProv fvs)    = isEmptyDVarSet fvs
 
 {-
 %************************************************************************
@@ -3391,11 +3628,20 @@ subst_co subst co
     go_prov (PhantomProv kco)    = PhantomProv (go kco)
     go_prov (ProofIrrelProv kco) = ProofIrrelProv (go kco)
     go_prov p@(PluginProv _)     = p
+    go_prov (ZappedProv fvs)     = ZappedProv (filterDVarSet isCoVar $ substFreeDVarSet subst fvs)
 
     -- See Note [Substituting in a coercion hole]
     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
@@ -3475,14 +3721,15 @@ substForAllCoCoVarBndrUsing sym sco (TCvSubst in_scope tenv cenv)
 
 substCoVar :: TCvSubst -> CoVar -> Coercion
 substCoVar (TCvSubst _ _ cenv) cv
-  = case lookupVarEnv cenv cv of
+  = ASSERT( isCoVar cv )
+    case lookupVarEnv cenv cv of
       Just co -> co
       Nothing -> CoVarCo cv
 
 substCoVars :: TCvSubst -> [CoVar] -> [Coercion]
 substCoVars subst cvs = map (substCoVar subst) cvs
 
-lookupCoVar :: TCvSubst -> Var -> Maybe Coercion
+lookupCoVar :: TCvSubst -> CoVar  -> Maybe Coercion
 lookupCoVar (TCvSubst _ _ cenv) v = lookupVarEnv cenv v
 
 substTyVarBndr :: HasCallStack => TCvSubst -> TyVar -> (TCvSubst, TyVar)
@@ -4057,9 +4304,7 @@ tidyCo env@(_, subst) co
             -- the case above duplicates a bit of work in tidying h and the kind
             -- of tv. But the alternative is to use coercionKind, which seems worse.
     go (FunCo r co1 co2)     = (FunCo r $! go co1) $! go co2
-    go (CoVarCo cv)          = case lookupVarEnv subst cv of
-                                 Nothing  -> CoVarCo cv
-                                 Just cv' -> CoVarCo cv'
+    go (CoVarCo cv)          = CoVarCo $ substCoVar cv
     go (HoleCo h)            = HoleCo h
     go (AxiomInstCo con ind cos) = let args = map go cos
                                in  args `seqList` AxiomInstCo con ind args
@@ -4079,6 +4324,9 @@ tidyCo env@(_, subst) co
     go_prov (PhantomProv co)    = PhantomProv (go co)
     go_prov (ProofIrrelProv co) = ProofIrrelProv (go co)
     go_prov p@(PluginProv _)    = p
+    go_prov (ZappedProv fvs)    = ZappedProv $ mapUnionDVarSet (unitDVarSet . substCoVar) (dVarSetElems fvs)
+
+    substCoVar cv = fromMaybe cv $ lookupVarEnv subst cv
 
 tidyCos :: TidyEnv -> [Coercion] -> [Coercion]
 tidyCos env = map (tidyCo env)
@@ -4139,3 +4387,4 @@ provSize UnsafeCoerceProv    = 1
 provSize (PhantomProv co)    = 1 + coercionSize co
 provSize (ProofIrrelProv co) = 1 + coercionSize co
 provSize (PluginProv _)      = 1
+provSize (ZappedProv _)      = 1


=====================================
compiler/types/Type.hs
=====================================
@@ -267,7 +267,8 @@ import FV
 import Outputable
 import FastString
 import Pair
-import DynFlags  ( gopt_set, GeneralFlag(Opt_PrintExplicitRuntimeReps) )
+import DynFlags  ( HasDynFlags(..)
+                 , gopt_set, GeneralFlag(Opt_PrintExplicitRuntimeReps) )
 import ListSetOps
 import Unique ( nonDetCmpUnique )
 
@@ -479,6 +480,8 @@ expandTypeSynonyms ty
     go_prov subst (PhantomProv co)    = PhantomProv (go_co subst co)
     go_prov subst (ProofIrrelProv co) = ProofIrrelProv (go_co subst co)
     go_prov _     p@(PluginProv _)    = p
+    go_prov subst (ZappedProv fvs)
+      = ZappedProv $ substFreeDVarSet subst fvs
 
       -- the "False" and "const" are to accommodate the type of
       -- substForAllCoBndrUsing, which is general enough to
@@ -547,7 +550,8 @@ data TyCoMapper env m
       }
 
 {-# INLINABLE mapType #-}  -- See Note [Specialising mappers]
-mapType :: Monad m => TyCoMapper env m -> env -> Type -> m Type
+mapType :: (Monad m, HasDynFlags m)
+        => TyCoMapper env m -> env -> Type -> m Type
 mapType mapper@(TyCoMapper { tcm_tyvar = tyvar
                            , tcm_tycobinder = tycobinder
                            , tcm_tycon = tycon })
@@ -582,7 +586,7 @@ mapType mapper@(TyCoMapper { tcm_tyvar = tyvar
            ; return $ ForAllTy (Bndr tv' vis) inner' }
 
 {-# INLINABLE mapCoercion #-}  -- See Note [Specialising mappers]
-mapCoercion :: Monad m
+mapCoercion :: (Monad m, HasDynFlags m)
             => TyCoMapper env m -> env -> Coercion -> m Coercion
 mapCoercion mapper@(TyCoMapper { tcm_covar = covar
                                , tcm_hole = cohole
@@ -629,6 +633,11 @@ mapCoercion mapper@(TyCoMapper { tcm_covar = covar
     go_prov (PhantomProv co)    = PhantomProv <$> go co
     go_prov (ProofIrrelProv co) = ProofIrrelProv <$> go co
     go_prov p@(PluginProv _)    = return p
+    go_prov (ZappedProv fvs)
+      = let bndrFVs v =
+              ASSERT(isCoVar v)
+              tyCoVarsOfCoDSet <$> covar env v
+        in ZappedProv . unionDVarSets <$> mapM bndrFVs (dVarSetElems fvs)
 
 {-
 ************************************************************************
@@ -3012,7 +3021,7 @@ occCheckExpand vs_to_avoid ty
     go_prov cxt (PhantomProv co)    = PhantomProv <$> go_co cxt co
     go_prov cxt (ProofIrrelProv co) = ProofIrrelProv <$> go_co cxt co
     go_prov _   p@(PluginProv _)    = return p
-
+    go_prov _   p@(ZappedProv _)    = return p
 
 {-
 %************************************************************************
@@ -3068,6 +3077,10 @@ tyConsOfType ty
      go_prov (PluginProv _)      = emptyUniqSet
         -- this last case can happen from the tyConsOfType used from
         -- checkTauTvUpdate
+     go_prov (ZappedProv _)      = emptyUniqSet
+        -- [ZappedCoDifference] that this will not report TyCons present in the
+        -- unzapped proof but not its kind. See Note [Zapping coercions] in
+        -- TyCoRep.
 
      go_s tys     = foldr (unionUniqSets . go)     emptyUniqSet tys
      go_cos cos   = foldr (unionUniqSets . go_co)  emptyUniqSet cos



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/commit/ea7f96de6f492a82564b0633152a895b9408c15f

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/commit/ea7f96de6f492a82564b0633152a895b9408c15f
You're receiving this email because of your account on gitlab.haskell.org.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20190611/923af328/attachment-0001.html>


More information about the ghc-commits mailing list