Experiment: zapwip/zap-dcoercions

23 files changed, 303 insertions, 37 deletions

diff --git a/compiler/GHC/Core/Coercion.hs b/compiler/GHC/Core/Coercion.hs
index 2d8db7f768..5a211d9f94 100644
--- a/compiler/GHC/Core/Coercion.hs
+++ b/compiler/GHC/Core/Coercion.hs
@@ -1390,6 +1390,8 @@ expandProv _ _ (PluginProv str)
   = PluginProv str
 expandProv _ _ (CorePrepProv homo)
   = CorePrepProv homo
+expandProv _ _ (ZappedProv cvs)
+  = ZappedProv cvs
 
 mkDehydrateCo :: Coercion -> DCoercion
 mkDehydrateCo co | isReflCo co       = ReflDCo
@@ -2085,6 +2087,7 @@ setNominalRole_maybe_prov prov = case prov of
   ProofIrrelProv _ -> Just prov -- it's always safe
   PluginProv _     -> Nothing   -- who knows? This choice is conservative.
   CorePrepProv _   -> Just prov
+  ZappedProv   _   -> Just prov
 
 -- | Make a phantom coercion between two types. The coercion passed
 -- in must be a nominal coercion between the kinds of the
@@ -2201,6 +2204,7 @@ promoteCoercion co = case co of
     UnivCo (ProofIrrelProv kco) _ _ _ -> kco
     UnivCo (PluginProv _)       _ _ _ -> mkKindCo co
     UnivCo (CorePrepProv _)     _ _ _ -> mkKindCo co
+    UnivCo (ZappedProv _)       _ _ _ -> mkKindCo co
 
     HydrateDCo {} -> mkKindCo co
 
@@ -3099,6 +3103,7 @@ seqProv seq_co (PhantomProv co)    = seq_co co
 seqProv seq_co (ProofIrrelProv co) = seq_co co
 seqProv _      (PluginProv _)      = ()
 seqProv _      (CorePrepProv _)    = ()
+seqProv _      (ZappedProv cvs)    = seqVarSet cvs
 
 seqCos :: [Coercion] -> ()
 seqCos []       = ()
diff --git a/compiler/GHC/Core/Coercion/Opt.hs b/compiler/GHC/Core/Coercion/Opt.hs
index 85de59d716..96e6a846bd 100644
--- a/compiler/GHC/Core/Coercion/Opt.hs
+++ b/compiler/GHC/Core/Coercion/Opt.hs
@@ -4,7 +4,6 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE StandaloneKindSignatures #-}
 {-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE ViewPatterns #-}
 
 module GHC.Core.Coercion.Opt
    ( optCoercion
@@ -18,6 +17,7 @@ import GHC.Prelude
 
 import GHC.Tc.Utils.TcType   ( exactTyCoVarsOfType )
 
+import GHC.Core.TyCo.FVs ( shallowCoVarsOfType, shallowCoVarsOfCo, shallowCoVarsOfDCo )
 import GHC.Core.TyCo.Rep
 import GHC.Core.TyCo.Subst
 import GHC.Core.Coercion
@@ -42,7 +42,7 @@ import GHC.Utils.Trace
 
 import Control.Monad   ( zipWithM )
 import qualified Data.Kind ( Type )
-
+import Data.List ( zipWith4 )
 {-
 %************************************************************************
 %*                                                                      *
@@ -143,15 +143,18 @@ newtype OptCoercionOpts = OptCoercionOpts
 
 data OptDCoMethod
   = HydrateDCos
-      -- ^ Turn directed coercions back into full-fledge coercions in the
-      -- coerction optimiser, so that they can be fully optimised.
+      -- ^ Turn directed coercions back into fully-fledged coercions in the
+      -- coercion optimiser, so that they can be fully optimised.
   | OptDCos
       -- ^ Optimise directed coercions with the (currently limited)
-      -- forms of optimisation avaiable for directed coercions.
+      -- forms of optimisation available for directed coercions.
       { skipDCoOpt :: !Bool
         -- ^ Whether to skip optimisation of directed coercions entirely
-        -- when possible.
-        }
+        -- (when possible).
+      }
+  | ZapDCos
+      -- ^ Zap directed coercions, storing only the RHS type
+      -- and the free variables of the coercion.
 
 data OptCoParams =
   OptCoParams { optDCoMethod :: !OptDCoMethod }
@@ -191,6 +194,97 @@ optCoercion' opts env co
   where
     lc = mkSubstLiftingContext env
 
+zapCoercion :: Coercion -> Coercion
+zapCoercion co = case co of
+  _
+    | isReflexiveCo co
+    -> mkReflCo r l_ty
+  GRefl r ty (MCo co) ->
+    GRefl r ty (MCo $ zapCoercion co)
+  FunCo r w arg res ->
+    mkFunCo r
+      (zapCoercion w)
+      (zapCoercion arg)
+      (zapCoercion res)
+  TyConAppCo r tc arg_cos ->
+    mkTyConAppCo r tc (map zapCoercion arg_cos)
+  AppCo lco rco ->
+    mkAppCo (zapCoercion lco) (zapCoercion rco)
+  ForAllCo tv kco bco ->
+    mkForAllCo tv (zapCoercion kco) (zapCoercion bco)
+  SymCo co ->
+    mkSymCo $ zapCoercion co
+  SubCo co ->
+    mkSubCo $ zapCoercion co
+  CoVarCo {} ->
+    co
+  AxiomInstCo ax br cos ->
+    AxiomInstCo ax br (map zapCoercion cos)
+  AxiomRuleCo ax cos ->
+    AxiomRuleCo ax (map zapCoercion cos)
+  UnivCo {} ->
+    co
+  HydrateDCo r l_ty dco r_ty ->
+    mkHydrateDCo r l_ty (zapDCoercion r l_ty dco r_ty) (Just r_ty)
+  _ -> zapped_co
+    --if coercionSize zapped_co < coercionSize co
+    --then zapped_co
+    --else co
+  where
+    (Pair l_ty r_ty, r) = {-# SCC "zapCo_coercionKindRole" #-} coercionKindRole co
+    zapped_co = UnivCo (ZappedProv cvs) r l_ty r_ty
+    cvs = {-# SCC "zapCo_shallowCoVars" #-} shallowCoVarsOfCo co
+
+zapDCoercion :: Role -> Type -> DCoercion -> Type -> DCoercion
+zapDCoercion r l_ty dco r_ty = case dco of
+  _
+    | isReflexiveDCo r l_ty dco r_ty
+    -> mkReflDCo
+  GReflRightDCo co ->
+    GReflRightDCo (zapCoercion co)
+  GReflLeftDCo co ->
+    GReflLeftDCo (zapCoercion co)
+  TyConAppDCo dcos
+    | TyConApp tc  l_args <- l_ty
+    , TyConApp tc' r_args <- r_ty
+    , tc == tc'
+    -> mkTyConAppDCo $
+        zipWith4 zapDCoercion
+          (tyConRolesX r tc) l_args dcos r_args
+  AppDCo dco1 dco2
+    | AppTy lty1 lty2 <- l_ty
+    , AppTy rty1 rty2 <- r_ty
+    -> mkAppDCo
+        (zapDCoercion r       lty1 dco1 rty1)
+        (zapDCoercion Nominal lty2 dco2 rty2)
+  ForAllDCo tv kco bco
+    | ForAllTy (Bndr l_tv _) l_body <- l_ty
+    , ForAllTy (Bndr r_tv _) r_body <- r_ty
+    -> mkForAllDCo tv
+         (zapDCoercion Nominal (tyVarKind l_tv) kco (tyVarKind r_tv))
+         (zapDCoercion r       l_body           bco r_body)
+  SubDCo dco ->
+    mkSubDCo l_ty (zapDCoercion Nominal l_ty dco r_ty) r_ty
+  CoVarDCo {} ->
+    dco
+  AxiomInstDCo {} ->
+    dco
+  StepsDCo {} ->
+    dco
+  UnivDCo {} ->
+    dco
+  DehydrateCo co ->
+    DehydrateCo (zapCoercion co)
+  _ -> zapped_dco
+    --if dcoercionSize zapped_dco < dcoercionSize dco
+    --then zapped_dco
+    --else dco
+  where
+    cvs = {-# SCC "zapDCo_shallowCoVars" #-}
+           shallowCoVarsOfType l_ty
+           `unionVarSet`
+           shallowCoVarsOfDCo dco
+    zapped_dco = UnivDCo (ZappedProv cvs) r_ty
 
 type NormalCo    = Coercion
   -- Invariants:
@@ -376,19 +470,27 @@ opt_co4 opts env sym rep r (AxiomInstCo con ind cos)
 opt_co4 opts env@(LC _ _lift_co_env) sym rep r (HydrateDCo _r lhs_ty dco rhs_ty)
   = case optDCoMethod opts of
       HydrateDCos ->
-        opt_co4 opts env sym rep r (hydrateOneLayerDCo r lhs_ty dco)
+        {-# SCC "opt_co4_hydrate" #-}
+          opt_co4 opts env sym rep r $
+          hydrateOneLayerDCo r lhs_ty dco
+      ZapDCos ->
+        {-# SCC "opt_co4_zap" #-}
+        opt_co4 (opts { optDCoMethod = HydrateDCos }) env sym rep r $
+        HydrateDCo r lhs_ty (zapDCoercion r lhs_ty dco rhs_ty) rhs_ty
       OptDCos { skipDCoOpt = do_skip }
         | do_skip && isEmptyVarEnv _lift_co_env
         -> let res = substCo (lcTCvSubst env) (HydrateDCo r lhs_ty dco rhs_ty)
-        in assert (r == _r) $
+        in {-# SCC "opt_co4_skip" #-}
+           assert (r == _r) $
            wrapSym sym $
            wrapRole rep r $
            res
         | otherwise
-        -> assert (r == _r) $
-             wrapSym sym $
-             (\ (lhs', dco') -> mkHydrateDCo r' lhs' dco' (Just rhs')) $
-             opt_dco4_wrap "HydrateDCo" opts env rep r lhs_ty dco
+        -> {-# SCC "opt_co4_dco" #-}
+           assert (r == _r) $
+           wrapSym sym $
+           (\ (lhs', dco') -> mkHydrateDCo r' lhs' dco' (Just rhs')) $
+           opt_dco4_wrap "HydrateDCo" opts env rep r lhs_ty dco
   where
     rhs' = substTyUnchecked (lcSubstRight env) rhs_ty
     r'   = chooseRole rep r
@@ -744,6 +846,13 @@ opt_univ co_or_dco opts env sym prov role oty1 oty2
                               opts env sym False Nominal kco
       PluginProv str     -> PluginProv str
       CorePrepProv homo  -> CorePrepProv homo
+      ZappedProv cvs     -> ZappedProv $ nonDetStrictFoldVarSet subst_gather emptyVarSet cvs
+        where
+          subst_gather cv acc
+            | Just co <- lookupCoVar (lcTCvSubst env) cv
+            = acc `unionVarSet` shallowCoVarsOfCo co -- SLD TODO: De-duplicate with subst_co_dco
+            | otherwise
+            = acc `extendVarSet` cv
 
 -------------
 opt_transList :: HasDebugCallStack => OptCoParams -> InScopeSet -> [NormalCo] -> [NormalCo] -> [NormalCo]
diff --git a/compiler/GHC/Core/FVs.hs b/compiler/GHC/Core/FVs.hs
index 843c874265..64304906f0 100644
--- a/compiler/GHC/Core/FVs.hs
+++ b/compiler/GHC/Core/FVs.hs
@@ -418,6 +418,7 @@ orphNamesOfProv orph_names (PhantomProv co)    = orph_names co
 orphNamesOfProv orph_names (ProofIrrelProv co) = orph_names co
 orphNamesOfProv _          (PluginProv _)      = emptyNameSet
 orphNamesOfProv _          (CorePrepProv _)    = emptyNameSet
+orphNamesOfProv _          (ZappedProv _)      = emptyNameSet
 
 orphNamesOfCos :: [Coercion] -> NameSet
 orphNamesOfCos = orphNamesOfThings orphNamesOfCo
diff --git a/compiler/GHC/Core/FamInstEnv.hs b/compiler/GHC/Core/FamInstEnv.hs
index 98ac2edc2c..87807dcefc 100644
--- a/compiler/GHC/Core/FamInstEnv.hs
+++ b/compiler/GHC/Core/FamInstEnv.hs
@@ -1502,8 +1502,7 @@ normalise_var_bndr tcvar
   = do { lc1 <- getLC
        ; env <- getEnv
        ; let
-           do_normalise ki = do { redn <- normalise_type ki; return redn }
-           callback lc ki  = runNormM (do_normalise ki) env lc Nominal
+           callback lc ki = runNormM (normalise_type ki) env lc Nominal
        ; return $ liftCoSubstVarBndrUsing (mkHydrateReductionDCoercion Nominal)
                     callback lc1 tcvar }
 
diff --git a/compiler/GHC/Core/Lint.hs b/compiler/GHC/Core/Lint.hs
index 4225f5a000..afa123de2b 100644
--- a/compiler/GHC/Core/Lint.hs
+++ b/compiler/GHC/Core/Lint.hs
@@ -2257,7 +2257,6 @@ lintCoercion (UnivCo prov r ty1 ty2)
                 _          -> return ()
             }
 
-
 lintCoercion (SymCo co)
   = do { co' <- lintCoercion co
        ; return (SymCo co') }
@@ -2577,6 +2576,15 @@ lintProv co_or_dco r ty1 ty2 prov = case prov of
   CorePrepProv homo ->
     return $ CorePrepProv homo
 
+  ZappedProv cvs ->
+    do { subst <- getTCvSubst
+       ; mapM_
+           (checkTyCoVarInScope "coercion" subst)
+           (nonDetEltsUniqSet cvs)
+         -- Don't bother to return substituted cvs;
+         -- they don't matter to Lint
+       ; return (ZappedProv cvs) }
+
   where
     k1, k2 :: LintedKind
     k1 = typeKind ty1
diff --git a/compiler/GHC/Core/TyCo/FVs.hs b/compiler/GHC/Core/TyCo/FVs.hs
index f504148f65..18287a3918 100644
--- a/compiler/GHC/Core/TyCo/FVs.hs
+++ b/compiler/GHC/Core/TyCo/FVs.hs
@@ -23,6 +23,10 @@ module GHC.Core.TyCo.FVs
         tyCoVarsOfCoList,
         tyCoVarsOfDCoList,
 
+        shallowCoVarsOfType, shallowCoVarsOfTypes,
+        shallowCoVarsOfCo, shallowCoVarsOfCos,
+        shallowCoVarsOfDCo, shallowCoVarsOfDCos,
+
         almostDevoidCoVarOfCo,
         almostDevoidCoVarOfDCo,
 
@@ -59,6 +63,7 @@ import GHC.Types.Var
 import GHC.Utils.FV
 
 import GHC.Types.Unique.FM
+import GHC.Types.Unique.Set ( nonDetEltsUniqSet )
 import GHC.Types.Var.Set
 import GHC.Types.Var.Env
 import GHC.Utils.Misc
@@ -373,7 +378,8 @@ shallow_co  :: Coercion   -> Endo TyCoVarSet
 shallow_cos :: [Coercion] -> Endo TyCoVarSet
 shallow_dco  :: DCoercion   -> Endo TyCoVarSet
 shallow_dcos :: [DCoercion] -> Endo TyCoVarSet
-(shallow_ty, shallow_tys, shallow_co, shallow_cos, shallow_dco, shallow_dcos) = foldTyCo shallowTcvFolder emptyVarSet
+(shallow_ty, shallow_tys, shallow_co, shallow_cos, shallow_dco, shallow_dcos)
+  = foldTyCo shallowTcvFolder emptyVarSet
 
 shallowTcvFolder :: TyCoFolder TyCoVarSet (Endo TyCoVarSet)
 shallowTcvFolder = TyCoFolder { tcf_view = noView
@@ -389,6 +395,48 @@ shallowTcvFolder = TyCoFolder { tcf_view = noView
     do_bndr is tcv _ = extendVarSet is tcv
     do_hole _ _  = mempty   -- Ignore coercion holes
 
+shallowCoVarsOfType :: Type -> CoVarSet
+-- See Note [Free variables of types]
+shallowCoVarsOfType ty = runTyCoVars (shallow_cv_ty ty)
+
+shallowCoVarsOfTypes :: [Type] -> CoVarSet
+shallowCoVarsOfTypes tys = runTyCoVars (shallow_cv_tys tys)
+
+shallowCoVarsOfCo :: Coercion -> CoVarSet
+shallowCoVarsOfCo co = runTyCoVars (shallow_cv_co co)
+
+shallowCoVarsOfCos :: [Coercion] -> CoVarSet
+shallowCoVarsOfCos cos = runTyCoVars (shallow_cv_cos cos)
+
+shallowCoVarsOfDCo :: DCoercion -> CoVarSet
+shallowCoVarsOfDCo dco = runTyCoVars (shallow_cv_dco dco)
+
+shallowCoVarsOfDCos :: [DCoercion] -> CoVarSet
+shallowCoVarsOfDCos dcos = runTyCoVars (shallow_cv_dcos dcos)
+
+shallow_cv_ty  :: Type       -> Endo CoVarSet
+shallow_cv_tys :: [Type]     -> Endo CoVarSet
+shallow_cv_co  :: Coercion   -> Endo CoVarSet
+shallow_cv_cos :: [Coercion] -> Endo CoVarSet
+shallow_cv_dco  :: DCoercion   -> Endo CoVarSet
+shallow_cv_dcos :: [DCoercion] -> Endo CoVarSet
+(shallow_cv_ty, shallow_cv_tys, shallow_cv_co, shallow_cv_cos, shallow_cv_dco, shallow_cv_dcos)
+  = foldTyCo shallowCvFolder emptyVarSet
+
+shallowCvFolder :: TyCoFolder CoVarSet (Endo CoVarSet)
+shallowCvFolder = TyCoFolder { tcf_view = noView
+                             , tcf_tyvar = do_tv, tcf_covar = do_cv
+                             , tcf_hole  = do_hole, tcf_tycobinder = do_bndr }
+  where
+    do_tv _ _  = mempty
+    do_cv is v = Endo do_it
+      where
+        do_it acc | v `elemVarSet` is  = acc
+                  | v `elemVarSet` acc = acc
+                  | otherwise          = acc `extendVarSet` v
+
+    do_bndr is tcv _ = extendVarSet is tcv
+    do_hole is hole = do_cv is (coHoleCoVar hole)
 
 {- *********************************************************************
 *                                                                      *
@@ -670,6 +718,7 @@ tyCoFVsOfProv tyCoFVs_of_co (PhantomProv co)    fv_cand in_scope acc = tyCoFVs_o
 tyCoFVsOfProv tyCoFVs_of_co (ProofIrrelProv co) fv_cand in_scope acc = tyCoFVs_of_co co fv_cand in_scope acc
 tyCoFVsOfProv _             (PluginProv _)      fv_cand in_scope acc = emptyFV fv_cand in_scope acc
 tyCoFVsOfProv _             (CorePrepProv _)    fv_cand in_scope acc = emptyFV fv_cand in_scope acc
+tyCoFVsOfProv _             (ZappedProv cvs)    fv_cand in_scope acc = mkFVs (nonDetEltsUniqSet cvs) fv_cand in_scope acc
 
 tyCoFVsOfCos :: [Coercion] -> FV
 tyCoFVsOfCos []       fv_cand in_scope acc = emptyFV fv_cand in_scope acc
@@ -800,6 +849,7 @@ almost_devoid_co_var_of_prov almost_devoid_co (ProofIrrelProv co) cv
   = almost_devoid_co co cv
 almost_devoid_co_var_of_prov _ (PluginProv _)   _ = True
 almost_devoid_co_var_of_prov _ (CorePrepProv _) _ = True
+almost_devoid_co_var_of_prov _ (ZappedProv cvs) cv = not (cv `elemVarSet` cvs)
 
 almost_devoid_co_var_of_type :: Type -> CoVar -> Bool
 almost_devoid_co_var_of_type (TyVarTy _) _ = True
diff --git a/compiler/GHC/Core/TyCo/Rep.hs b/compiler/GHC/Core/TyCo/Rep.hs
index 70731396cf..312e458fef 100644
--- a/compiler/GHC/Core/TyCo/Rep.hs
+++ b/compiler/GHC/Core/TyCo/Rep.hs
@@ -95,6 +95,7 @@ import GHC.Core.Coercion.Axiom
 import {-# SOURCE #-} GHC.Builtin.Types ( manyDataConTy )
 import GHC.Types.Basic ( LeftOrRight(..), pickLR )
 import GHC.Types.Unique ( Uniquable(..) )
+import GHC.Types.Unique.Set ( nonDetEltsUniqSet )
 import GHC.Utils.Outputable
 import GHC.Data.FastString
 import GHC.Utils.Misc
@@ -1852,6 +1853,9 @@ data UnivCoProvenance kco
       Bool   -- True  <=> the UnivCo must be homogeneously kinded
              -- False <=> allow hetero-kinded, e.g. Int ~ Int#
 
+  | ZappedProv
+      CoVarSet
+
   deriving Data.Data
 
 instance Outputable (UnivCoProvenance kco) where
@@ -1859,6 +1863,7 @@ instance Outputable (UnivCoProvenance kco) where
   ppr (ProofIrrelProv _) = text "(proof irrel.)"
   ppr (PluginProv str)   = parens (text "plugin" <+> brackets (text str))
   ppr (CorePrepProv _)   = text "(CorePrep)"
+  ppr (ZappedProv _)     = text "(zapped)"
 
 -- | A coercion to be filled in by the type-checker. See Note [Coercion holes]
 data CoercionHole
@@ -2193,11 +2198,18 @@ foldTyCo (TyCoFolder { tcf_view       = view
         env' = tycobinder env tv Inferred
     go_dco env (UnivDCo prov t2)       = go_prov go_dco env prov `mappend` go_ty env t2
 
-    go_prov :: (env ->co -> a) -> env -> UnivCoProvenance co -> a
+    {-# INLINE go_prov #-}
+    go_prov :: (env -> co -> a) -> env -> UnivCoProvenance co -> a
     go_prov do_fold env (PhantomProv co)    = do_fold env co
     go_prov do_fold env (ProofIrrelProv co) = do_fold env co
     go_prov _       _   (PluginProv _)      = mempty
     go_prov _       _   (CorePrepProv _)    = mempty
+    go_prov _       env (ZappedProv cvs)    = go_cvs env (nonDetEltsUniqSet cvs)
+
+    go_cvs _   []       = mempty
+    go_cvs env (cv:cvs) = covar env cv `mappend` go_cvs env cvs
+      -- NB. Explicit recursion here is much better than nonDetStrictFoldVarSet.
+      -- Test case T9198 is very sensitive to this difference.
 
 -- | A view function that looks through nothing.
 noView :: Type -> Maybe Type
@@ -2275,6 +2287,7 @@ provSize co_size (PhantomProv co)    = 1 + co_size co
 provSize co_size (ProofIrrelProv co) = 1 + co_size co
 provSize _       (PluginProv _)      = 1
 provSize _       (CorePrepProv _)    = 1
+provSize _       (ZappedProv cvs)    = 1 + sizeVarSet cvs
 
 {-
 ************************************************************************
diff --git a/compiler/GHC/Core/TyCo/Subst.hs b/compiler/GHC/Core/TyCo/Subst.hs
index fde5648cd0..fd885696e4 100644
--- a/compiler/GHC/Core/TyCo/Subst.hs
+++ b/compiler/GHC/Core/TyCo/Subst.hs
@@ -911,6 +911,10 @@ subst_co_dco subst = (go, go_dco)
     go_prov do_subst (ProofIrrelProv kco) = ProofIrrelProv $! do_subst kco
     go_prov _        p@(PluginProv _)     = p
     go_prov _        p@(CorePrepProv _)   = p
+    go_prov _        (ZappedProv cvs)     = ZappedProv $! nonDetStrictFoldVarSet subst_gather emptyVarSet cvs
+        where
+          subst_gather cv acc
+            = acc `unionVarSet` shallowCoVarsOfCo (substCoVar subst cv)
 
     -- See Note [Substituting in a coercion hole]
     go_hole h@(CoercionHole { ch_co_var = cv })
diff --git a/compiler/GHC/Core/TyCo/Tidy.hs b/compiler/GHC/Core/TyCo/Tidy.hs
index 598f58379d..940f41d1ae 100644
--- a/compiler/GHC/Core/TyCo/Tidy.hs
+++ b/compiler/GHC/Core/TyCo/Tidy.hs
@@ -24,6 +24,7 @@ import GHC.Core.TyCo.Rep
 import GHC.Core.TyCo.FVs (tyCoVarsOfTypesWellScoped, tyCoVarsOfTypeList)
 
 import GHC.Types.Name hiding (varName)
+import GHC.Types.Unique.Set (mapUniqSet)
 import GHC.Types.Var
 import GHC.Types.Var.Env
 import GHC.Utils.Misc (strictMap)
@@ -277,6 +278,7 @@ tidyCoDCo env@(_, subst) = (go, go_dco)
     go_prov do_tidy (ProofIrrelProv co) = ProofIrrelProv $! do_tidy co
     go_prov _       p@(PluginProv _)    = p
     go_prov _       p@(CorePrepProv _)  = p
+    go_prov _       (ZappedProv cvs)    = ZappedProv $! mapUniqSet go_cv cvs
 
     go_cv cv = lookupVarEnv subst cv `orElse` cv
 
diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs
index 049118351a..5f1c5d9397 100644
--- a/compiler/GHC/Core/Type.hs
+++ b/compiler/GHC/Core/Type.hs
@@ -667,6 +667,7 @@ expandTypeSynonyms ty
     go_prov do_subst (ProofIrrelProv co) = ProofIrrelProv $ do_subst co
     go_prov _        p@(PluginProv _)    = p
     go_prov _        p@(CorePrepProv _)  = p
+    go_prov _        p@(ZappedProv _)    = p
 
       -- the "False" and "const" are to accommodate the type of
       -- substForAllCoBndrUsing, which is general enough to
@@ -932,7 +933,7 @@ mapTyCo mapper
         -> (go_ty (), go_tys (), go_co (), go_cos ())
 
 {-# INLINE mapTyCoX #-}  -- See Note [Specialising mappers]
-mapTyCoX :: Monad m => TyCoMapper env m
+mapTyCoX :: forall m env. Monad m => TyCoMapper env m
          -> ( env -> Type       -> m Type
             , env -> [Type]     -> m [Type]
             , env -> Coercion   -> m Coercion
@@ -987,7 +988,7 @@ mapTyCoX (TyCoMapper { tcm_tyvar = tyvar
     go_co env (CoVarCo cv)        = covar env cv
     go_co env (HoleCo hole)       = cohole env hole
     go_co env (HydrateDCo r t1 dco t2) = mkHydrateDCo r <$> go_ty env t1 <*> go_dco env dco <*> (Just <$> go_ty env t2)
-    go_co env (UnivCo p r t1 t2)  = mkUnivCo <$> go_prov (go_co env) p <*> pure r
+    go_co env (UnivCo p r t1 t2)  = mkUnivCo <$> go_prov go_co env p <*> pure r
                                     <*> go_ty env t1 <*> go_ty env t2
     go_co env (SymCo co)          = mkSymCo <$> go_co env co
     go_co env (TransCo c1 c2)     = mkTransCo <$> go_co env c1 <*> go_co env c2
@@ -1041,13 +1042,22 @@ mapTyCoX (TyCoMapper { tcm_tyvar = tyvar
            ; co' <- go_dco env' co
            ; return $ mkForAllDCo tv' kind_dco' co' }
         -- See Note [Efficiency for ForAllCo case of mapTyCoX]
-    go_dco env (UnivDCo p rhs)     = mkUnivDCo <$> go_prov (go_dco env) p <*> go_ty env rhs
+    go_dco env (UnivDCo p rhs)     = mkUnivDCo <$> go_prov go_dco env p <*> go_ty env rhs
     go_dco env (SubDCo dco)        = SubDCo <$> go_dco env dco
 
-    go_prov go (PhantomProv co)    = PhantomProv    <$> go co
-    go_prov go (ProofIrrelProv co) = ProofIrrelProv <$> go co
-    go_prov _  p@(PluginProv _)    = return p
-    go_prov _  p@(CorePrepProv _)  = return p
+    go_prov :: (env -> co -> m co) -> env -> UnivCoProvenance co -> m (UnivCoProvenance co)
+    go_prov go env (PhantomProv co)    = PhantomProv    <$> go env co
+    go_prov go env (ProofIrrelProv co) = ProofIrrelProv <$> go env co
+    go_prov _  _   p@(PluginProv _)    = return p
+    go_prov _  _   p@(CorePrepProv _)  = return p
+    go_prov _  env (ZappedProv cvs)
+      = ZappedProv <$>
+         nonDetStrictFoldVarSet (go_cv env) (return emptyVarSet) cvs
+
+    go_cv env v mcvs = do { cvs <- mcvs
+                          ; co  <- covar env v
+                          ; return (tyCoVarsOfCo co `unionVarSet` cvs) }
+
 
 
 {-
@@ -3511,6 +3521,7 @@ occCheckExpand vs_to_avoid ty
     go_prov prov_go (ProofIrrelProv co) = ProofIrrelProv <$> prov_go co
     go_prov _       p@(PluginProv _)    = return p
     go_prov _       p@(CorePrepProv _)  = return p
+    go_prov _       p@(ZappedProv _)    = return p
 
 
 {-
@@ -3580,6 +3591,7 @@ tyConsOfType ty
      go_prov get_tycons (PhantomProv co)    = get_tycons co
      go_prov get_tycons (ProofIrrelProv co) = get_tycons co
      go_prov _          (PluginProv _)      = emptyUniqSet
+     go_prov _          (ZappedProv _)      = emptyUniqSet
      go_prov _          (CorePrepProv _)    = emptyUniqSet
         -- this last case can happen from the tyConsOfType used from
         -- checkTauTvUpdate
diff --git a/compiler/GHC/CoreToIface.hs b/compiler/GHC/CoreToIface.hs
index 1d1b2dc86c..e5d2cfcca1 100644
--- a/compiler/GHC/CoreToIface.hs
+++ b/compiler/GHC/CoreToIface.hs
@@ -78,6 +78,7 @@ import GHC.Types.Var.Set
 import GHC.Types.Tickish
 import GHC.Types.Demand ( isTopSig )
 import GHC.Types.Cpr ( topCprSig )
+import GHC.Types.Unique.Set (nonDetEltsUniqSet)
 
 import GHC.Utils.Outputable
 import GHC.Utils.Panic
@@ -347,6 +348,13 @@ toIfaceCoercionDCoercion fr = (go, go_dco)
     go_prov to_iface (ProofIrrelProv co) = IfaceProofIrrelProv (to_iface co)
     go_prov _        (PluginProv str)    = IfacePluginProv str
     go_prov _        (CorePrepProv b)    = IfaceCorePrepProv b
+    go_prov _        (ZappedProv cvs)    = IfaceZappedProv
+                                              (map toIfaceCoVar $ nonDetEltsUniqSet bound_cvs)
+                                              (nonDetEltsUniqSet free_cvs)
+                                            -- We only care about the sets (e.g. to check membership),
+                                            -- so order (and hence non-determinism) doesn't matter here.
+      where
+        (free_cvs, bound_cvs) = partitionVarSet (`elemVarSet` fr) cvs
 
 toIfaceTcArgs :: TyCon -> [Type] -> IfaceAppArgs
 toIfaceTcArgs = toIfaceTcArgsX emptyVarSet
diff --git a/compiler/GHC/Driver/Config.hs b/compiler/GHC/Driver/Config.hs
index 1ea2562c29..99d3cfe63a 100644
--- a/compiler/GHC/Driver/Config.hs
+++ b/compiler/GHC/Driver/Config.hs
@@ -25,10 +25,13 @@ initOptCoercionOpts dflags = OptCoercionOpts
        = if hasNoOptCoercion dflags
          then Nothing
          else
-            let dco_method =
-                 if hasKeepDCoercions dflags
-                 then OptDCos { skipDCoOpt = True }
-                 else HydrateDCos
+            let dco_method
+                  | hasZapDCoercions dflags
+                  = ZapDCos
+                  | hasKeepDCoercions dflags
+                  = OptDCos { skipDCoOpt = True }
+                  | otherwise
+                  = HydrateDCos
             in Just dco_method
    }
 
diff --git a/compiler/GHC/Driver/Flags.hs b/compiler/GHC/Driver/Flags.hs
index 09aa170abf..7607aec91e 100644
--- a/compiler/GHC/Driver/Flags.hs
+++ b/compiler/GHC/Driver/Flags.hs
@@ -394,6 +394,7 @@ data GeneralFlag
    | Opt_G_NoStateHack
    | Opt_G_NoOptCoercion
    | Opt_G_KeepDCoercions
+   | Opt_G_ZapDCoercions
    deriving (Eq, Show, Enum)
 
 -- Check whether a flag should be considered an "optimisation flag"
diff --git a/compiler/GHC/Driver/Session.hs b/compiler/GHC/Driver/Session.hs
index 27b404bb22..3d4527acaf 100644
--- a/compiler/GHC/Driver/Session.hs
+++ b/compiler/GHC/Driver/Session.hs
@@ -29,7 +29,7 @@ module GHC.Driver.Session (
         ProfAuto(..),
         glasgowExtsFlags,
         hasPprDebug, hasNoDebugOutput, hasNoStateHack,
-        hasNoOptCoercion, hasKeepDCoercions,
+        hasNoOptCoercion, hasKeepDCoercions, hasZapDCoercions,
         dopt, dopt_set, dopt_unset,
         gopt, gopt_set, gopt_unset, setGeneralFlag', unSetGeneralFlag',
         wopt, wopt_set, wopt_unset,
@@ -1439,6 +1439,9 @@ hasNoOptCoercion = gopt Opt_G_NoOptCoercion
 hasKeepDCoercions :: DynFlags -> Bool
 hasKeepDCoercions = gopt Opt_G_KeepDCoercions
 
+hasZapDCoercions :: DynFlags -> Bool
+hasZapDCoercions = gopt Opt_G_ZapDCoercions
+
 -- | Test whether a 'DumpFlag' is set
 dopt :: DumpFlag -> DynFlags -> Bool
 dopt f dflags = (f `EnumSet.member` dumpFlags dflags)
@@ -2305,6 +2308,12 @@ dynamic_flags_deps = [
         (NoArg (setGeneralFlag Opt_G_NoOptCoercion))
   , make_ord_flag defGhcFlag "fkeep-dcoercions"
         (NoArg (setGeneralFlag Opt_G_KeepDCoercions))
+  , make_ord_flag defGhcFlag "fzap-dcoercions"
+        (NoArg (setGeneralFlag Opt_G_ZapDCoercions))
+  , make_ord_flag defGhcFlag "fno-keep-dcoercions"
+        (NoArg (unSetGeneralFlag Opt_G_KeepDCoercions))
+  , make_ord_flag defGhcFlag "fno-zap-dcoercions"
+        (NoArg (unSetGeneralFlag Opt_G_ZapDCoercions))
   , make_ord_flag defGhcFlag "with-rtsopts"
         (HasArg setRtsOpts)
   , make_ord_flag defGhcFlag "rtsopts"
@@ -3825,6 +3834,7 @@ impliedGFlags = [(Opt_DeferTypeErrors, turnOn, Opt_DeferTypedHoles)
                 ,(Opt_DeferTypeErrors, turnOn, Opt_DeferOutOfScopeVariables)
                 ,(Opt_DoLinearCoreLinting, turnOn, Opt_DoCoreLinting)
                 ,(Opt_Strictness, turnOn, Opt_WorkerWrapper)
+                ,(Opt_DoCoreLinting, turnOff, Opt_G_ZapDCoercions)
                 ] ++ validHoleFitsImpliedGFlags
 
 -- General flags that are switched on/off when other general flags are switched
@@ -3934,7 +3944,8 @@ optLevelFlags -- see Note [Documenting optimisation flags]
 
     , ([0],     Opt_IgnoreInterfacePragmas)
     , ([0],     Opt_OmitInterfacePragmas)
-    , ([0],     Opt_G_KeepDCoercions)
+ -- , ([0],     Opt_G_KeepDCoercions)
+    , ([0,1,2], Opt_G_ZapDCoercions)
 
     , ([1,2],   Opt_CoreConstantFolding)
 
@@ -3993,6 +4004,7 @@ disableUnusedBinds = mapM_ unSetWarningFlag unusedBindsFlags
 enableDLint :: DynP ()
 enableDLint = do
     mapM_ setGeneralFlag dLintFlags
+    unSetGeneralFlag Opt_G_ZapDCoercions
     addWayDynP WayDebug
   where
     dLintFlags :: [GeneralFlag]
diff --git a/compiler/GHC/Iface/Rename.hs b/compiler/GHC/Iface/Rename.hs
index 6a3cae6e94..47b7a61822 100644
--- a/compiler/GHC/Iface/Rename.hs
+++ b/compiler/GHC/Iface/Rename.hs
@@ -741,6 +741,12 @@ rnIfaceProv rn_thing (IfacePhantomProv    iface_co) = IfacePhantomProv    <$> rn
 rnIfaceProv rn_thing (IfaceProofIrrelProv iface_co) = IfaceProofIrrelProv <$> rn_thing iface_co
 rnIfaceProv _        (IfacePluginProv str)          = return (IfacePluginProv str)
 rnIfaceProv _        (IfaceCorePrepProv homo)       = return (IfaceCorePrepProv homo)
+rnIfaceProv _        (IfaceZappedProv cvs fcvs) =
+  assertPpr (null fcvs)
+    (vcat [ text "rnIfaceProv (ZappedProv): fcvs is not empty"
+          , text "fcvs:" <+> ppr fcvs
+          , text "cvs:" <+> ppr cvs ]) $
+  return (IfaceZappedProv cvs fcvs)
 
 rnIfaceTyCon :: Rename IfaceTyCon
 rnIfaceTyCon (IfaceTyCon n info)
diff --git a/compiler/GHC/Iface/Syntax.hs b/compiler/GHC/Iface/Syntax.hs
index 892cdc7cb7..e88216d522 100644
--- a/compiler/GHC/Iface/Syntax.hs
+++ b/compiler/GHC/Iface/Syntax.hs
@@ -1728,6 +1728,7 @@ freeNamesIfProv free_names (IfacePhantomProv co)    = free_names co
 freeNamesIfProv free_names (IfaceProofIrrelProv co) = free_names co
 freeNamesIfProv _          (IfacePluginProv _)      = emptyNameSet
 freeNamesIfProv _          (IfaceCorePrepProv _)    = emptyNameSet
+freeNamesIfProv _          (IfaceZappedProv {})     = emptyNameSet
 
 freeNamesIfVarBndr :: VarBndr IfaceBndr vis -> NameSet
 freeNamesIfVarBndr (Bndr bndr _) = freeNamesIfBndr bndr
diff --git a/compiler/GHC/Iface/Type.hs b/compiler/GHC/Iface/Type.hs
index d8248ae2c7..bdb9a1f4a7 100644
--- a/compiler/GHC/Iface/Type.hs
+++ b/compiler/GHC/Iface/Type.hs
@@ -416,6 +416,7 @@ data IfaceUnivCoProv iface_co
   | IfaceProofIrrelProv iface_co
   | IfacePluginProv String
   | IfaceCorePrepProv Bool            -- See defn of CorePrepProv
+  | IfaceZappedProv [IfLclName] [Var] -- See Note [Free tyvars in IfaceType]
 
 {- Note [Holes in IfaceCoercion]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -634,6 +635,7 @@ substIfaceType env ty
     go_prov do_subst (IfaceProofIrrelProv co) = IfaceProofIrrelProv (do_subst co)
     go_prov _        co@(IfacePluginProv _)   = co
     go_prov _        co@(IfaceCorePrepProv _) = co
+    go_prov _        co@(IfaceZappedProv {})  = co
 
 substIfaceAppArgs :: IfaceTySubst -> IfaceAppArgs -> IfaceAppArgs
 substIfaceAppArgs env args
@@ -1898,6 +1900,8 @@ pprIfaceUnivCoProv _ (IfacePluginProv s)
   = text "plugin" <+> doubleQuotes (text s)
 pprIfaceUnivCoProv _ (IfaceCorePrepProv _)
   = text "CorePrep"
+pprIfaceUnivCoProv _ (IfaceZappedProv cvs fcvs)
+  = hang (text "zap") 2 (sep [ppr cvs, ppr fcvs])
 
 -------------------
 instance Outputable IfaceTyCon where
@@ -2350,6 +2354,13 @@ instance Binary iface_co => Binary (IfaceUnivCoProv iface_co) where
   put_ bh (IfaceCorePrepProv a) = do
           putByte bh 4
           put_ bh a
+  put_ bh (IfaceZappedProv cvs fcvs) = do
+          massertPpr (null fcvs) $
+            vcat [ text "put IfaceZappedProv: fcvs is not empty"
+                 , text "fcvs:" <+> ppr fcvs
+                 , text "cvs:" <+> ppr cvs ]
+          putByte bh 5
+          put_ bh cvs
 
   get bh = do
       tag <- getByte bh
@@ -2362,6 +2373,8 @@ instance Binary iface_co => Binary (IfaceUnivCoProv iface_co) where
                    return $ IfacePluginProv a
            4 -> do a <- get bh
                    return (IfaceCorePrepProv a)
+           5 -> do a <- get bh
+                   return (IfaceZappedProv a [])
            _ -> panic ("get IfaceUnivCoProv " ++ show tag)
 
 
diff --git a/compiler/GHC/IfaceToCore.hs b/compiler/GHC/IfaceToCore.hs
index 2697da5843..3eda7902a4 100644
--- a/compiler/GHC/IfaceToCore.hs
+++ b/compiler/GHC/IfaceToCore.hs
@@ -1460,6 +1460,13 @@ tcIfaceUnivCoProv tc_co (IfacePhantomProv kco)    = PhantomProv <$> tc_co kco
 tcIfaceUnivCoProv tc_co (IfaceProofIrrelProv kco) = ProofIrrelProv <$> tc_co kco
 tcIfaceUnivCoProv _     (IfacePluginProv str)     = return $ PluginProv str
 tcIfaceUnivCoProv _     (IfaceCorePrepProv b)     = return $ CorePrepProv b
+tcIfaceUnivCoProv _     (IfaceZappedProv cvs fcvs)=
+  do { massertPpr (null fcvs) $
+         vcat [ text "tcIfaceUnivCoProv (ZappedProv): fcvs is not empty"
+              , text "fcvs:" <+> ppr fcvs
+              , text "cvs:" <+> ppr cvs ]
+     ; cvs <- mkVarSet <$> mapM tcIfaceLclId cvs
+     ; return (ZappedProv cvs) }
 
 {-
 ************************************************************************
diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs
index fed45019d7..1252e54802 100644
--- a/compiler/GHC/Tc/Solver/Monad.hs
+++ b/compiler/GHC/Tc/Solver/Monad.hs
@@ -1,7 +1,5 @@
 {-# LANGUAGE CPP #-}
-{-# LANGUAGE DeriveFunctor #-}
 {-# LANGUAGE DerivingStrategies #-}
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE MultiWayIf #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
diff --git a/compiler/GHC/Tc/TyCl/Utils.hs b/compiler/GHC/Tc/TyCl/Utils.hs
index 2c5b486219..aec4f14f7c 100644
--- a/compiler/GHC/Tc/TyCl/Utils.hs
+++ b/compiler/GHC/Tc/TyCl/Utils.hs
@@ -170,6 +170,7 @@ synonymTyConsOfType ty
      go_prov syns (ProofIrrelProv co)  = syns co
      go_prov _    (PluginProv _)       = emptyNameEnv
      go_prov _    (CorePrepProv _)     = emptyNameEnv
+     go_prov _    (ZappedProv _)       = emptyNameEnv
 
      go_tc tc | isTypeSynonymTyCon tc = unitNameEnv (tyConName tc) tc
               | otherwise             = emptyNameEnv
diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs
index 88cfcb606e..2d24cdbe2a 100644
--- a/compiler/GHC/Tc/Utils/TcMType.hs
+++ b/compiler/GHC/Tc/Utils/TcMType.hs
@@ -1637,6 +1637,10 @@ collect_cand_qtvs_co_dco orig_ty bound dv = (go_co dv, go_dco dv)
     go_prov collect dv (ProofIrrelProv co) = collect dv co
     go_prov _       dv (PluginProv _)      = return dv
     go_prov _       dv (CorePrepProv _)    = return dv
+    go_prov _       dv (ZappedProv cvs)    = nonDetStrictFoldVarSet zt_cv (return dv) cvs
+
+    zt_cv :: CoVar -> TcM CandidatesQTvs -> TcM CandidatesQTvs
+    zt_cv cv mdvs = do { dvs <- mdvs; go_cv dvs cv }
 
     go_cv :: CandidatesQTvs -> CoVar -> TcM CandidatesQTvs
     go_cv dv@(DV { dv_cvs = cvs }) cv
diff --git a/docs/users_guide/using-optimisation.rst b/docs/users_guide/using-optimisation.rst
index f68b5966d9..7aa9cd27ad 100644
--- a/docs/users_guide/using-optimisation.rst
+++ b/docs/users_guide/using-optimisation.rst
@@ -768,7 +768,7 @@ by saying ``-fno-wombat``.
     :type: dynamic
     :category:
 
-    :default: Keep with :ghc-flag:`-O0`, don't keep otherwise.
+    :default: Don't keep directed coercions.
 
     Keep directed coercions in the coercion optimiser, instead of turning
     them into coercions. Only applies when coercion optimisation is enabled.
@@ -778,6 +778,15 @@ by saying ``-fno-wombat``.
     (i.e. enabling :ghc-flag:`-fno-opt-coercion` causes a significant regression in compile-time),
     then you might want to NOT enable this flag.
 
+.. ghc-flag:: -fzap-dcoercions
+    :shortdesc: Zap directed coercions in the coercion optimiser
+    :type: dynamic
+    :category:
+
+    :default: Zap directed coercions.
+
+    Zap directed coercions in the coercion optimiser. Takes precedence over :ghc-flag:`-fkeep-dcoercions`.
+
 .. ghc-flag:: -fno-pre-inlining
     :shortdesc: Turn off pre-inlining
     :type: dynamic
diff --git a/testsuite/tests/perf/compiler/all.T b/testsuite/tests/perf/compiler/all.T
index 3bd97d06cf..e424639e7a 100644
--- a/testsuite/tests/perf/compiler/all.T
+++ b/testsuite/tests/perf/compiler/all.T
@@ -169,7 +169,7 @@ test ('T8095',
       [ only_ways(['normal']),
         collect_compiler_stats('bytes allocated',2) ],
       compile,
-      ['-v0 -O -fkeep-dcoercions'])
+      ['-v0 -O'])
 test ('T13386',
       [ only_ways(['normal']),
         collect_compiler_stats('bytes allocated',1) ],
@@ -206,7 +206,7 @@ test ('LargeRecord',
       , extra_files(['SuperRecord.hs'])
       ],
       multimod_compile,
-      ['LargeRecord', '-v0 -O -fkeep-dcoercions'])
+      ['LargeRecord', '-v0 -O'])
 
 test('T9961',
      [ only_ways(['normal']),
@@ -244,7 +244,7 @@ test('T12227',
      ],
      compile,
      # Use `-M1G` to prevent memory thrashing with ghc-8.0.1.
-     ['-O2 -fkeep-dcoercions -ddump-hi -ddump-to-file +RTS -M1G'])
+     ['-O2 -ddump-hi -ddump-to-file +RTS -M1G'])
 
 test('T12425',
      [ only_ways(['optasm']),