Zonk coercion holes correctly; a few other fixes.wip/zapzapzap

Non-perf tests pass. Now let's see the real results!

18 files changed, 223 insertions, 73 deletions

diff --git a/compiler/GHC/Core/Coercion.hs b/compiler/GHC/Core/Coercion.hs
index 4e13e02bc7..861a0002a7 100644
--- a/compiler/GHC/Core/Coercion.hs
+++ b/compiler/GHC/Core/Coercion.hs
@@ -126,7 +126,13 @@ module GHC.Core.Coercion (
 
         hasCoercionHoleTy, hasCoercionHoleCo, hasThisCoercionHoleTy,
 
-        setCoHoleType
+        setCoHoleType,
+
+        FreeCoVarsHoles,
+        mkFreeCoVarsHoles, updateFreeCoVars, updateFreeCoVarsM,
+        sizeFreeCoVarsHoles,
+        freeCoVars, freeCoHoles,
+
        ) where
 
 import {-# SOURCE #-} GHC.CoreToIface (toIfaceTyCon, tidyToIfaceTcArgs)
@@ -1337,7 +1343,7 @@ mkProofIrrelCo r kco        g1 g2 = mkUnivCo (ProofIrrelProv kco) r
                                              (mkCoercionTy g1) (mkCoercionTy g2)
 
 -- | TODO (RAE): Comment
-mkZappedCo :: Role -> Type -> Type -> DCoVarSet -> Coercion
+mkZappedCo :: Role -> Type -> Type -> FreeCoVarsHoles -> Coercion
 mkZappedCo = ZappedCo
 
 {-
@@ -2347,7 +2353,7 @@ seqCo (InstCo co arg)           = seqCo co `seq` seqCo arg
 seqCo (KindCo co)               = seqCo co
 seqCo (SubCo co)                = seqCo co
 seqCo (AxiomRuleCo _ cs)        = seqCos cs
-seqCo (ZappedCo r t1 t2 cvs)    = r `seq` seqType t1 `seq` seqType t2 `seq` seqDVarSet cvs
+seqCo (ZappedCo r t1 t2 _vs)   = r `seq` seqType t1 `seq` seqType t2
 
 seqProv :: UnivCoProvenance -> ()
 seqProv (PhantomProv co)    = seqCo co
@@ -2776,4 +2782,4 @@ hasThisCoercionHoleTy ty hole = Monoid.getAny (f ty)
 
 -- | Set the type of a 'CoercionHole'
 setCoHoleType :: CoercionHole -> Type -> CoercionHole
-setCoHoleType h t = setCoHoleCoVar h (setVarType (coHoleCoVar h) t)
+setCoHoleType h t = setCoHoleCoVar h (setVarType (coHoleCoVar h) t)
\ No newline at end of file
diff --git a/compiler/GHC/Core/Coercion.hs-boot b/compiler/GHC/Core/Coercion.hs-boot
index 2d90b8e210..0c1f81b7cb 100644
--- a/compiler/GHC/Core/Coercion.hs-boot
+++ b/compiler/GHC/Core/Coercion.hs-boot
@@ -10,7 +10,6 @@ import {-# SOURCE #-} GHC.Core.TyCon
 import GHC.Types.Basic ( LeftOrRight )
 import GHC.Core.Coercion.Axiom
 import GHC.Types.Var
-import GHC.Types.Var.Set
 import GHC.Data.Pair
 import GHC.Utils.Misc
 
@@ -34,7 +33,7 @@ mkKindCo :: Coercion -> Coercion
 mkSubCo :: HasDebugCallStack => Coercion -> Coercion
 mkProofIrrelCo :: Role -> Coercion -> Coercion -> Coercion -> Coercion
 mkAxiomRuleCo :: CoAxiomRule -> [Coercion] -> Coercion
-mkZappedCo :: Role -> Type -> Type -> DCoVarSet -> Coercion
+mkZappedCo :: Role -> Type -> Type -> FreeCoVarsHoles -> Coercion
 
 isGReflCo :: Coercion -> Bool
 isReflCo :: Coercion -> Bool
diff --git a/compiler/GHC/Core/Coercion/Opt.hs b/compiler/GHC/Core/Coercion/Opt.hs
index 3c81d3f349..4ebe2379c3 100644
--- a/compiler/GHC/Core/Coercion/Opt.hs
+++ b/compiler/GHC/Core/Coercion/Opt.hs
@@ -36,6 +36,7 @@ import GHC.Utils.Trace
 
 import Control.Monad   ( zipWithM )
 import GHC.Core.TyCo.FVs
+import GHC.Types.Unique.DSet
 
 {-
 %************************************************************************
@@ -471,22 +472,23 @@ opt_co4 env sym rep r (AxiomRuleCo co cs)
     wrapSym sym $
     AxiomRuleCo co (zipWith (opt_co2 env False) (coaxrAsmpRoles co) cs)
 
-opt_co4 env sym rep r (ZappedCo _r t1 t2 cvs)
+opt_co4 env sym rep r (ZappedCo _r t1 t2 vs)
   | assert (r == _r) $
+    assert (isEmptyUniqDSet (freeCoHoles vs)) $
     t1' `eqType` t2'
   = mkReflCo (chooseRole rep r) t1'
 
   | sym
-  = ZappedCo (chooseRole rep r) t2' t1' cvs'
+  = ZappedCo (chooseRole rep r) t2' t1' vs'
 
   | otherwise
-  = ZappedCo (chooseRole rep r) t1' t2' cvs'
+  = ZappedCo (chooseRole rep r) t1' t2' vs'
 
   where
     t1' = substTy (lcSubstLeft env) t1
     t2' = substTy (lcSubstRight env) t2
 
-    cvs' = coVarsOfCosDSet $ map opt (dVarSetElems cvs)
+    vs' = updateFreeCoVars vs (coVarsOfCosDSet . map opt . dVarSetElems)
     opt cv = opt_covar env False False (coVarRole cv) cv
 
 
@@ -702,10 +704,10 @@ opt_trans_rule is in_co1@(LRCo d1 co1) in_co2@(LRCo d2 co2)
   = fireTransRule "PushLR" in_co1 in_co2 $
     mkLRCo d1 (opt_trans is co1 co2)
 
-opt_trans_rule _is in_co1@(ZappedCo r1 t1 _ cvs1) in_co2@(ZappedCo r2 _ t2 cvs2)
+opt_trans_rule _is in_co1@(ZappedCo r1 t1 _ vs1) in_co2@(ZappedCo r2 _ t2 vs2)
   = assert (r1 == r2) $
     fireTransRule "PushZapped" in_co1 in_co2 $
-    mkZappedCo r1 t1 t2 (cvs1 `unionDVarSet` cvs2)
+    mkZappedCo r1 t1 t2 (vs1 `mappend` vs2)
 
 -- Push transitivity inside instantiation
 opt_trans_rule is in_co1@(InstCo co1 ty1) in_co2@(InstCo co2 ty2)
diff --git a/compiler/GHC/Core/Lint.hs b/compiler/GHC/Core/Lint.hs
index eda7407dbe..b9b3d5ca1d 100644
--- a/compiler/GHC/Core/Lint.hs
+++ b/compiler/GHC/Core/Lint.hs
@@ -96,6 +96,7 @@ import Data.List          ( partition )
 import Data.Maybe
 import GHC.Data.Pair
 import qualified GHC.LanguageExtensions as LangExt
+import GHC.Types.Unique.DSet
 
 {-
 Note [Core Lint guarantee]
@@ -2409,14 +2410,17 @@ lintCoercion (HoleCo h)
   = do { addErrL $ text "Unfilled coercion hole:" <+> ppr h
        ; lintCoercion (CoVarCo (coHoleCoVar h)) }
 
-lintCoercion (ZappedCo r t1 t2 cvs)
+lintCoercion co@(ZappedCo r t1 t2 vs)
   = do { t1' <- lintType t1
        ; t2' <- lintType t2
 
-       ; substed_cvs <- mapM lintCoVar (dVarSetElems cvs)
-       ; let cvs' = coVarsOfCosDSet substed_cvs
+       ; vs' <- updateFreeCoVarsM vs $ \cvs ->
+                  coVarsOfCosDSet <$> mapM lintCoVar (dVarSetElems cvs)
 
-       ; return (ZappedCo r t1' t2' cvs') }
+       ; checkL (isEmptyUniqDSet (freeCoHoles vs)) $
+         text "Unzonked coercion hole in ZappedCo:" <+> ppr co
+
+       ; return (ZappedCo r t1' t2' vs') }
 
 lintCoVar :: CoVar -> LintM LintedCoercion
 lintCoVar cv
diff --git a/compiler/GHC/Core/TyCo/FVs.hs b/compiler/GHC/Core/TyCo/FVs.hs
index 9d9cd6b169..c2921ec057 100644
--- a/compiler/GHC/Core/TyCo/FVs.hs
+++ b/compiler/GHC/Core/TyCo/FVs.hs
@@ -16,11 +16,13 @@ module GHC.Core.TyCo.FVs
         tyCoVarsOfCo, tyCoVarsOfCos, tyCoVarsOfMCo,
         coVarsOfType, coVarsOfTypes,
         coVarsOfCo, coVarsOfCos,
-        coVarsOfCoDSet, coVarsOfCosDSet,
+        coVarsOfCosDSet,
         tyCoVarsOfCoDSet, tyCoVarsOfCosDSet,
         tyCoFVsOfCo, tyCoFVsOfCos,
         tyCoVarsOfCoList,
 
+        coVarsHolesOfCo, coVarsHolesOfCos,
+
         almostDevoidCoVarOfCo,
 
         -- Injective free vars
@@ -52,7 +54,7 @@ import GHC.Core.TyCo.Rep
 import GHC.Core.TyCon
 import GHC.Types.Var
 import GHC.Utils.FV
-
+import GHC.Types.Unique.DSet
 import GHC.Types.Unique.FM
 import GHC.Types.Var.Set
 import GHC.Types.Var.Env
@@ -431,9 +433,6 @@ deepCoVarFolder = TyCoFolder { tcf_view = noView
                        -- See Note [CoercionHoles and coercion free variables]
                        -- in GHC.Core.TyCo.Rep
 
-coVarsOfCoDSet :: Coercion -> DCoVarSet
-coVarsOfCoDSet = fvDVarSet . filterFV isCoVar . tyCoFVsOfCo
-
 coVarsOfCosDSet :: [Coercion] -> DCoVarSet
 coVarsOfCosDSet = fvDVarSet . filterFV isCoVar . tyCoFVsOfCos
 
@@ -648,7 +647,11 @@ tyCoFVsOfCo (KindCo co)         fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in
 tyCoFVsOfCo (SubCo co)          fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
 tyCoFVsOfCo (AxiomRuleCo _ cs)  fv_cand in_scope acc = tyCoFVsOfCos cs fv_cand in_scope acc
 tyCoFVsOfCo (ZappedCo _ a b vs) fv_cand in_scope acc
-  = (tyCoFVsOfType a `unionFV` tyCoFVsOfType b `unionFV` mkFVs (dVarSetElems vs))
+  = (tyCoFVsOfType a `unionFV`
+     tyCoFVsOfType b `unionFV`
+     mapUnionFV tyCoFVsOfCoVar (dVarSetElems (freeCoVars vs)) `unionFV`
+     mapUnionFV (tyCoFVsOfCoVar . coHoleCoVar) (uniqDSetToList (freeCoHoles vs)))
+       -- See Note [CoercionHoles and coercion free variables]
     fv_cand in_scope acc
 
 tyCoFVsOfCoVar :: CoVar -> FV
@@ -717,10 +720,12 @@ almost_devoid_co_var_of_co (SubCo co) cv
   = almost_devoid_co_var_of_co co cv
 almost_devoid_co_var_of_co (AxiomRuleCo _ cs) cv
   = almost_devoid_co_var_of_cos cs cv
-almost_devoid_co_var_of_co (ZappedCo _ t1 t2 cvs) cv
+almost_devoid_co_var_of_co (ZappedCo _ t1 t2 vs) cv
   = almost_devoid_co_var_of_type t1 cv
   && almost_devoid_co_var_of_type t2 cv
-  && not (cv `elemDVarSet` cvs)
+  && not (cv `elemDVarSet` freeCoVars vs)
+  && not (cv `elemDVarSet` mapUniqDSet coHoleCoVar (freeCoHoles vs))
+                            -- there should be no holes here, anyway
 
 almost_devoid_co_var_of_cos :: [Coercion] -> CoVar -> Bool
 almost_devoid_co_var_of_cos [] _ = True
@@ -1014,3 +1019,21 @@ tyCoVarsOfTypeWellScoped = scopedSort . tyCoVarsOfTypeList
 -- | Get the free vars of types in scoped order
 tyCoVarsOfTypesWellScoped :: [Type] -> [TyVar]
 tyCoVarsOfTypesWellScoped = scopedSort . tyCoVarsOfTypesList
+
+{- *********************************************************************
+*                                                                      *
+      Free coercion holes
+*                                                                      *
+********************************************************************* -}
+
+coVarsHolesOfCo :: Coercion -> FreeCoVarsHoles
+coVarsHolesOfCos :: [Coercion] -> FreeCoVarsHoles
+(coVarsHolesOfCo, coVarsHolesOfCos) = (go_co, go_cos)
+  where
+    (go_ty, _, go_co, go_cos) = foldTyCo folder ()
+    folder = TyCoFolder { tcf_view = noView
+                        , tcf_tyvar = \ _ tv -> go_ty (varType tv)
+                        , tcf_covar = \ _ cv -> mkFreeCoVarsHoles (unitDVarSet cv) mempty `mappend`
+                                                go_ty (varType cv)
+                        , tcf_hole = \ _ h -> mkFreeCoVarsHoles mempty (unitUniqDSet h)
+                        , tcf_tycobinder = const2 }
diff --git a/compiler/GHC/Core/TyCo/Rep.hs b/compiler/GHC/Core/TyCo/Rep.hs
index 79dea31396..ee9712281e 100644
--- a/compiler/GHC/Core/TyCo/Rep.hs
+++ b/compiler/GHC/Core/TyCo/Rep.hs
@@ -41,6 +41,12 @@ module GHC.Core.TyCo.Rep (
         CoercionN, CoercionR, CoercionP, KindCoercion,
         MCoercion(..), MCoercionR, MCoercionN,
 
+        FreeCoVarsHoles,
+        mkFreeCoVarsHoles, updateFreeCoVars, updateFreeCoVarsM,
+        sizeFreeCoVarsHoles,
+        freeCoVars, freeCoHoles,
+
+
         -- * Functions over types
         mkNakedTyConTy, mkTyVarTy, mkTyVarTys,
         mkTyCoVarTy, mkTyCoVarTys,
@@ -98,6 +104,10 @@ import GHC.Utils.Panic
 -- libraries
 import qualified Data.Data as Data hiding ( TyCon )
 import Data.IORef ( IORef )   -- for CoercionHole
+import GHC.Types.Unique.DSet
+import qualified Data.Semigroup   -- for (<>) in a Semigroup instance only
+import GHC.Utils.Panic.Plain
+
 
 {- **********************************************************************
 *                                                                       *
@@ -1209,7 +1219,7 @@ data Coercion
   | HoleCo CoercionHole              -- ^ See Note [Coercion holes]
                                      -- Only present during typechecking
 
-  | ZappedCo Role Type Type DCoVarSet      -- TODO (RAE): Comment
+  | ZappedCo Role Type Type !FreeCoVarsHoles     -- TODO (RAE): Comment
   deriving Data.Data
 
 type CoercionN = Coercion       -- always nominal
@@ -1661,6 +1671,55 @@ instance Outputable CoercionHole where
 instance Uniquable CoercionHole where
   getUnique (CoercionHole { ch_co_var = cv }) = getUnique cv
 
+-- | Stores the free covars and coercion holes from a type or coercion;
+-- these are often needed together
+data FreeCoVarsHoles = FCVH_Empty  -- avoid allocating a new FCVH node at every <>
+                     | FCVH !DCoVarSet !(UniqDSet CoercionHole)
+  deriving Data.Data
+
+mkFreeCoVarsHoles :: DCoVarSet -> UniqDSet CoercionHole -> FreeCoVarsHoles
+mkFreeCoVarsHoles = FCVH
+
+-- this one preserves FCVH_Empty
+-- Pre-condition: f empty == empty
+updateFreeCoVars :: FreeCoVarsHoles -> (DCoVarSet -> DCoVarSet) -> FreeCoVarsHoles
+updateFreeCoVars FCVH_Empty f    = assert (isEmptyDVarSet (f emptyDVarSet))
+                                   FCVH_Empty
+updateFreeCoVars (FCVH cvs hs) f = FCVH (f cvs) hs
+
+-- this one preserves FCVH_Empty
+-- Pre-condition: f empty == empty (and has no side effects)
+updateFreeCoVarsM :: Applicative m => FreeCoVarsHoles -> (DCoVarSet -> m DCoVarSet)
+                  -> m FreeCoVarsHoles
+updateFreeCoVarsM FCVH_Empty _    = pure FCVH_Empty
+updateFreeCoVarsM (FCVH cvs hs) f = FCVH <$> f cvs <*> pure hs
+
+freeCoVars :: FreeCoVarsHoles -> DCoVarSet
+freeCoVars FCVH_Empty   = emptyDVarSet
+freeCoVars (FCVH cvs _) = cvs
+
+freeCoHoles :: FreeCoVarsHoles -> UniqDSet CoercionHole
+freeCoHoles FCVH_Empty  = emptyUniqDSet
+freeCoHoles (FCVH _ hs) = hs
+
+sizeFreeCoVarsHoles :: FreeCoVarsHoles -> Int
+sizeFreeCoVarsHoles FCVH_Empty    = 0
+sizeFreeCoVarsHoles (FCVH cvs hs) = sizeDVarSet cvs + sizeUniqDSet hs
+
+instance Outputable FreeCoVarsHoles where
+  ppr FCVH_Empty   = braces empty
+  ppr (FCVH vs hs) = braces (fcat (punctuate comma (map ppr (dVarSetElems vs))) <> vbar <>
+                             fcat (punctuate comma (map ppr (uniqDSetToList hs))))
+
+instance Semigroup FreeCoVarsHoles where
+  FCVH_Empty   <> FCVH_Empty   = FCVH_Empty
+  FCVH_Empty   <> other        = other
+  other        <> FCVH_Empty   = other
+  FCVH vs1 hs1 <> FCVH vs2 hs2 = FCVH (vs1 `mappend` vs2) (hs1 `mappend` hs2)
+
+instance Monoid FreeCoVarsHoles where
+  mempty = FCVH_Empty
+
 {- Note [Phantom coercions]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider
@@ -1936,9 +1995,10 @@ foldTyCo (TyCoFolder { tcf_view       = view
     go_co env (InstCo co arg)         = go_co env co `mappend` go_co env arg
     go_co env (KindCo co)             = go_co env co
     go_co env (SubCo co)              = go_co env co
-    go_co env (ZappedCo _ t1 t2 cvs)  = go_ty env t1 `mappend`
+    go_co env (ZappedCo _ t1 t2 vs)   = go_ty env t1 `mappend`
                                         go_ty env t2 `mappend`
-                                        foldMap (covar env) cvs
+                                        foldMap (covar env) (freeCoVars vs) `mappend`
+                                        foldMap (cohole env) (freeCoHoles vs)
     go_co env (ForAllCo tv kind_co co)
       = go_co env kind_co `mappend` go_ty env (varType tv)
                           `mappend` go_co env' co
@@ -2004,7 +2064,7 @@ coercionSize (InstCo co arg)     = 1 + coercionSize co + coercionSize arg
 coercionSize (KindCo co)         = 1 + coercionSize co
 coercionSize (SubCo co)          = 1 + coercionSize co
 coercionSize (AxiomRuleCo _ cs)  = 1 + sum (map coercionSize cs)
-coercionSize (ZappedCo _ a b vs) = 1 + typeSize a + typeSize b + sizeDVarSet vs
+coercionSize (ZappedCo _ a b vs) = 1 + typeSize a + typeSize b + sizeFreeCoVarsHoles vs
 
 provSize :: UnivCoProvenance -> Int
 provSize (PhantomProv co)    = 1 + coercionSize co
diff --git a/compiler/GHC/Core/TyCo/Rep.hs-boot b/compiler/GHC/Core/TyCo/Rep.hs-boot
index f2e59d534f..89138ebf3a 100644
--- a/compiler/GHC/Core/TyCo/Rep.hs-boot
+++ b/compiler/GHC/Core/TyCo/Rep.hs-boot
@@ -8,6 +8,7 @@ import {-# SOURCE #-} GHC.Core.TyCon ( TyCon )
 
 data Type
 data Coercion
+data FreeCoVarsHoles
 data UnivCoProvenance
 data TyLit
 data TyCoBinder
diff --git a/compiler/GHC/Core/TyCo/Subst.hs b/compiler/GHC/Core/TyCo/Subst.hs
index defdad591c..e9a16d60e8 100644
--- a/compiler/GHC/Core/TyCo/Subst.hs
+++ b/compiler/GHC/Core/TyCo/Subst.hs
@@ -85,6 +85,7 @@ import GHC.Utils.Panic
 import GHC.Utils.Panic.Plain
 
 import Data.List (mapAccumL)
+import GHC.Types.Unique.DSet
 
 {-
 %************************************************************************
@@ -859,8 +860,11 @@ subst_co subst co
     go (AxiomRuleCo c cs)    = let cs1 = map go cs
                                 in cs1 `seqList` AxiomRuleCo c cs1
     go (HoleCo h)            = HoleCo $! go_hole h
-    go (ZappedCo r t1 t2 vs) = ((mkZappedCo r $! go_ty t1) $! go_ty t2) $!
-                                 coVarsOfCosDSet (map (substCoVar subst) (dVarSetElems vs))
+    go (ZappedCo r t1 t2 vs) = ((mkZappedCo r $! go_ty t1) $! go_ty t2) $! new_vs
+      where
+        cos_from_vs = map (substCoVar subst) (dVarSetElems (freeCoVars vs))
+        new_vs      = coVarsHolesOfCos cos_from_vs `mappend`
+                      mkFreeCoVarsHoles mempty (mapUniqDSet go_hole (freeCoHoles vs))
 
     go_prov (PhantomProv kco)    = PhantomProv (go kco)
     go_prov (ProofIrrelProv kco) = ProofIrrelProv (go kco)
diff --git a/compiler/GHC/Core/TyCo/Tidy.hs b/compiler/GHC/Core/TyCo/Tidy.hs
index 28f4a1f504..880dc3c725 100644
--- a/compiler/GHC/Core/TyCo/Tidy.hs
+++ b/compiler/GHC/Core/TyCo/Tidy.hs
@@ -248,7 +248,7 @@ tidyCo env@(_, subst) co
     go (SubCo co)            = SubCo $! go co
     go (AxiomRuleCo ax cos)  = AxiomRuleCo ax $ strictMap go cos
     go (ZappedCo r t1 t2 vs) = ((ZappedCo r $! tidyType env t1) $! tidyType env t2) $!
-                                 mapDVarSet go_covar vs
+                                updateFreeCoVars vs (mapDVarSet go_covar)
 
     go_covar cv
       | Just cv' <- lookupVarEnv subst cv = cv'
diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs
index 01e26e0d73..1c84383e50 100644
--- a/compiler/GHC/Core/Type.hs
+++ b/compiler/GHC/Core/Type.hs
@@ -296,6 +296,7 @@ import GHC.Types.Unique ( nonDetCmpUnique )
 import GHC.Data.Maybe   ( orElse, expectJust )
 import Data.Maybe       ( isJust )
 import Control.Monad    ( guard )
+import GHC.Types.Unique.DSet
 -- import GHC.Utils.Trace
 
 -- $type_classification
@@ -622,9 +623,10 @@ expandTypeSynonyms ty
       = AxiomRuleCo ax (map (go_co subst) cs)
     go_co _ (HoleCo h)
       = pprPanic "expandTypeSynonyms hit a hole" (ppr h)
-    go_co subst (ZappedCo r t1 t2 cvs)
-      = mkZappedCo r (go subst t1) (go subst t2)
-                   (coVarsOfCosDSet (map (substCoVar subst) (dVarSetElems cvs)))
+    go_co subst (ZappedCo r t1 t2 vs)
+      = assert (isEmptyUniqDSet (freeCoHoles vs)) $
+        mkZappedCo r (go subst t1) (go subst t2)
+                   (updateFreeCoVars vs (coVarsOfCosDSet . map (substCoVar subst) . dVarSetElems))
 
     go_prov subst (PhantomProv co)    = PhantomProv (go_co subst co)
     go_prov subst (ProofIrrelProv co) = ProofIrrelProv (go_co subst co)
@@ -976,9 +978,16 @@ mapTyCoX (TyCoMapper { tcm_tyvar = tyvar
            ; co' <- go_co env' co
            ; return $ mkForAllCo tv' kind_co' co' }
         -- See Note [Efficiency for ForAllCo case of mapTyCoX]
-    go_co env (ZappedCo r t1 t2 cvs)
-      = ZappedCo r <$> go_ty env t1 <*> go_ty env t2 <*>
-                 (coVarsOfCosDSet <$> mapM (covar env) (dVarSetElems cvs))
+    go_co env (ZappedCo r t1 t2 vs)
+      = do { t1' <- go_ty env t1
+           ; t2' <- go_ty env t2
+           ; let cvs = freeCoVars vs
+                 hs  = freeCoHoles vs
+           ; cos_from_cvs <- mapM (covar env) (dVarSetElems cvs)
+           ; cos_from_hs  <- mapM (cohole env) (uniqDSetToList hs)
+           ; let new_vs = coVarsHolesOfCos cos_from_cvs `mappend` coVarsHolesOfCos cos_from_hs
+           ; return $ mkZappedCo r t1' t2' new_vs }
+
 
     go_prov env (PhantomProv co)    = PhantomProv <$> go_co env co
     go_prov env (ProofIrrelProv co) = ProofIrrelProv <$> go_co env co
@@ -2532,7 +2541,7 @@ getRuntimeRep_maybe :: HasDebugCallStack
 getRuntimeRep_maybe = kindRep_maybe . typeKind
 
 -- | Extract the RuntimeRep classifier of a type. For instance,
--- @getRuntimeRep_maybe Int = LiftedRep@. Panics if this is not possible.
+-- @getRuntimeRep Int = LiftedRep@. Panics if this is not possible.
 getRuntimeRep :: HasDebugCallStack => Type -> Type
 getRuntimeRep ty
   = case getRuntimeRep_maybe ty of
@@ -3372,11 +3381,11 @@ occCheckExpand vs_to_avoid ty
                                              ; co2' <- go_co cxt co2
                                              ; w' <- go_co cxt w
                                              ; return (mkFunCo r w' co1' co2') }
-    go_co env (CoVarCo cv)              = do { cv' <- go_covar env cv
+    go_co cxt (CoVarCo cv)              = do { cv' <- go_covar cxt cv
                                              ; return (mkCoVarCo cv') }
-    go_co (as,_) co@(HoleCo h)
-      | bad_var_occ as (ch_co_var h)    = Nothing
-      | otherwise                       = return co
+    go_co cxt co@(HoleCo h)
+      | ok_hole cxt h = return co
+      | otherwise     = Nothing
 
     go_co cxt (AxiomInstCo ax ind args) = do { args' <- mapM (go_co cxt) args
                                              ; return (mkAxiomInstCo ax ind args') }
@@ -3402,16 +3411,20 @@ occCheckExpand vs_to_avoid ty
                                              ; return (mkSubCo co') }
     go_co cxt (AxiomRuleCo ax cs)       = do { cs' <- mapM (go_co cxt) cs
                                              ; return (mkAxiomRuleCo ax cs') }
-    go_co cxt (ZappedCo r t1 t2 cvs)    = do { t1' <- go cxt t1
-                                             ; t2' <- go cxt t2
-                                             ; cvs' <- mapM (go_covar cxt) (dVarSetElems cvs)
-                                             ; return (mkZappedCo r t1' t2' (mkDVarSet cvs')) }
+    go_co cxt (ZappedCo r t1 t2 vs)
+      = do { t1' <- go cxt t1
+           ; t2' <- go cxt t2
+           ; vs' <- updateFreeCoVarsM vs $ \cvs ->
+                      mkDVarSet <$> mapM (go_covar cxt) (dVarSetElems cvs)
+           ; guard (all (ok_hole cxt) (uniqDSetToList (freeCoHoles vs)))
+           ; return (mkZappedCo r t1' t2' vs') }
 
     go_covar (as,env) cv
       | Just cv' <- lookupVarEnv env cv = return cv'
       | bad_var_occ as cv               = Nothing
       | otherwise                       = return cv
 
+    ok_hole (as,_) h = not (bad_var_occ as (ch_co_var h))
     ------------------
     go_prov cxt (PhantomProv co)    = PhantomProv <$> go_co cxt co
     go_prov cxt (ProofIrrelProv co) = ProofIrrelProv <$> go_co cxt co
diff --git a/compiler/GHC/CoreToIface.hs b/compiler/GHC/CoreToIface.hs
index 24bf2f656a..b40750c8a1 100644
--- a/compiler/GHC/CoreToIface.hs
+++ b/compiler/GHC/CoreToIface.hs
@@ -84,6 +84,7 @@ import GHC.Utils.Misc
 import GHC.Utils.Trace
 
 import Data.Maybe ( catMaybes )
+import GHC.Types.Unique.DSet
 
 {- Note [Avoiding space leaks in toIface*]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -296,9 +297,14 @@ toIfaceCoercionX fr co
     go (KindCo c)           = IfaceKindCo (go c)
     go (SubCo co)           = IfaceSubCo (go co)
     go (ZappedCo r t1 t2 vs)= IfaceZappedCo r (toIfaceTypeX fr t1) (toIfaceTypeX fr t2)
-                                            free_cvs (map toIfaceCoVar (dVarSetElems bound_cvs))
+                                              (free_cvs1 `unionDVarSet` free_cvs2)
+                                              (map toIfaceCoVar (dVarSetElems bound_cvs))
       where
-        (free_cvs, bound_cvs) = partitionDVarSet (`elemVarSet` fr) vs
+        cvs                    = freeCoVars vs
+        hs                     = freeCoHoles vs
+        (free_cvs1, bound_cvs) = partitionDVarSet (`elemVarSet` fr) cvs
+        free_cvs2              = mkDVarSet (map coHoleCoVar (uniqDSetToList hs))
+
     go (AxiomRuleCo co cs)  = IfaceAxiomRuleCo (coaxrName co) (map go cs)
     go (AxiomInstCo c i cs) = IfaceAxiomInstCo (coAxiomName c) i (map go cs)
     go (UnivCo p r t1 t2)   = IfaceUnivCo (go_prov p) r
diff --git a/compiler/GHC/IfaceToCore.hs b/compiler/GHC/IfaceToCore.hs
index df1bf0eb65..6999077a10 100644
--- a/compiler/GHC/IfaceToCore.hs
+++ b/compiler/GHC/IfaceToCore.hs
@@ -1429,7 +1429,8 @@ tcIfaceCo = go
     go (IfaceHoleCo c)           = pprPanic "tcIfaceCo:IfaceHoleCo"    (ppr c)
     go (IfaceZappedCo r t1 t2 free_cvs bound_cvs)
       = assert (isEmptyDVarSet free_cvs) $
-        ZappedCo r <$> tcIfaceType t1 <*> tcIfaceType t2 <*> (mkDVarSet <$> mapM go_var bound_cvs)
+        ZappedCo r <$> tcIfaceType t1 <*> tcIfaceType t2 <*>
+                 (mkFreeCoVarsHoles <$> (mkDVarSet <$> mapM go_var bound_cvs) <*> pure mempty)
 
     go_var :: FastString -> IfL CoVar
     go_var = tcIfaceLclId
diff --git a/compiler/GHC/Tc/Solver/Rewrite.hs b/compiler/GHC/Tc/Solver/Rewrite.hs
index 43436347b8..baedbef2ef 100644
--- a/compiler/GHC/Tc/Solver/Rewrite.hs
+++ b/compiler/GHC/Tc/Solver/Rewrite.hs
@@ -1127,22 +1127,23 @@ mk_maybe_roles ReprEq roles = Just roles
 data UsedCoVars
   = JustZonked    -- ^ we only zonked; nothing else interesting happened
                   -- consequence: a coercion between the output and the input is just Refl
-  | UsedCoVars DCoVarSet   -- ^ something interesting happened, with the given set
+  | UsedCoVars !FreeCoVarsHoles
+                           -- ^ something interesting happened, with the given sets
                            -- of free covars. NB: UsedCoVars <empty> is *not* the same
                            -- as JustZonked!
 
 instance Semigroup UsedCoVars where
-  JustZonked      <> JustZonked      = JustZonked
-  UsedCoVars cvs  <> JustZonked      = UsedCoVars cvs
-  JustZonked      <> UsedCoVars cvs  = UsedCoVars cvs
-  UsedCoVars cvs1 <> UsedCoVars cvs2 = UsedCoVars (cvs1 `unionDVarSet` cvs2)
+  JustZonked     <> JustZonked     = JustZonked
+  other          <> JustZonked     = other
+  JustZonked     <> other          = other
+  UsedCoVars vs1 <> UsedCoVars vs2 = UsedCoVars (vs1 `mappend` vs2)
 
 instance Monoid UsedCoVars where
   mempty = JustZonked
 
 coercionUsedCoVars :: Coercion -> UsedCoVars
 coercionUsedCoVars co | isReflCo co = JustZonked
-                      | otherwise   = UsedCoVars (coVarsOfCoDSet co)
+                      | otherwise   = UsedCoVars (coVarsHolesOfCo co)
 
 
 rewrite_zapped :: Type -> RewriteM (Xi, UsedCoVars)
@@ -1173,7 +1174,7 @@ rewrite_zapped (TyVarTy tv)
                  ; when wrw $ recordRewriter ctev
 
                  ; (xi, ucv) <- bumpDepth $ rewrite_zapped rhs_ty
-                 ; return (xi, ucv `mappend` UsedCoVars (coVarsOfCoDSet (ctEvCoercion ctev))) }
+                 ; return (xi, ucv `mappend` coercionUsedCoVars (ctEvCoercion ctev)) }
 
        ; _ -> do { tv' <- liftTcS $ updateTyVarKindM zonkTcType tv
                  ; return (mkTyVarTy tv', JustZonked) }}}}}
@@ -1201,8 +1202,15 @@ rewrite_zapped (FunTy { ft_af = vis, ft_mult = mult, ft_arg = ty1, ft_res = ty2
            <- setEqRel NomEq $ liftA3 (,,) (rewrite_zapped mult)
                                            (rewrite_zapped arg_rep)
                                            (rewrite_zapped res_rep)
-       ; let arg_ki_co = build_zapped_mco arg_rep arg_rep_xi ucv4
-             res_ki_co = build_zapped_mco res_rep res_rep_xi ucv5
+       ; let arg_rr_mco = build_zapped_mco arg_rep arg_rep_xi ucv4
+             res_rr_mco = build_zapped_mco res_rep res_rep_xi ucv5
+
+             mk_TYPE_mco MRefl = MRefl
+             mk_TYPE_mco (MCo rr_co) = MCo (mkTyConAppCo Nominal tYPETyCon [rr_co])
+
+             arg_ki_co = mk_TYPE_mco arg_rr_mco
+             res_ki_co = mk_TYPE_mco res_rr_mco
+
        ; return ( mkFunTy vis mult_xi (xi1 `mkCastTyMCo` arg_ki_co) (xi2 `mkCastTyMCo` res_ki_co)
                 , mconcat [ucv1, ucv2, ucv3, ucv4, ucv5] ) }
 
@@ -1431,7 +1439,7 @@ rewrite_args_slow_zapped orig_binders orig_inner_ki fvs orig_roles orig_tys
 build_zapped_mco :: Kind -> Kind -> UsedCoVars -> MCoercionN
 build_zapped_mco _ki1 _ki2 JustZonked = MRefl
 build_zapped_mco ki1 ki2 _ | ki1 `eqType` ki2 = MRefl
-build_zapped_mco ki1 ki2 (UsedCoVars cvs) = MCo $ mkZappedCo Nominal ki1 ki2 cvs
+build_zapped_mco ki1 ki2 (UsedCoVars vs) = MCo $ mkZappedCo Nominal ki1 ki2 vs
 
 build_zapped_co :: Role -> Type -> Type -> UsedCoVars -> Coercion
 build_zapped_co r t1 t2 ucv
@@ -1439,4 +1447,6 @@ build_zapped_co r t1 t2 ucv
   | otherwise                                = mkReflCo r t2  -- t2 is more zonked, generally
 
 -- TODO (RAE): Make mode where both rewriters run, comparing the results
--- TODO (RAE): Fix rw in HEAD
\ No newline at end of file
+-- TODO (RAE): Fix rw in HEAD
+-- TODO (RAE): Make reduction strict in HEAD
+-- TODO (RAE): Make reduction use MCo in HEAD
\ No newline at end of file
diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs
index 4f69413a86..038fc5027b 100644
--- a/compiler/GHC/Tc/Utils/TcMType.hs
+++ b/compiler/GHC/Tc/Utils/TcMType.hs
@@ -1581,15 +1581,11 @@ collect_cand_qtvs_co orig_ty bound = go_co
     go_co dv (InstCo co1 co2)      = foldlM go_co dv [co1, co2]
     go_co dv (KindCo co)           = go_co dv co
     go_co dv (SubCo co)            = go_co dv co
+    go_co dv (HoleCo hole)         = go_hole dv hole
     go_co dv (ZappedCo _ t1 t2 vs) = do dv1 <- collect_cand_qtvs orig_ty True bound dv  t1
                                         dv2 <- collect_cand_qtvs orig_ty True bound dv1 t2
-                                        foldlM go_cv dv2 vs
-
-    go_co dv (HoleCo hole)
-      = do m_co <- unpackCoercionHole_maybe hole
-           case m_co of
-             Just co -> go_co dv co
-             Nothing -> go_cv dv (coHoleCoVar hole)
+                                        dv3 <- foldlM go_cv dv2 (freeCoVars vs)
+                                        foldlM go_hole dv3 (freeCoHoles vs)
 
     go_co dv (CoVarCo cv) = go_cv dv cv
 
@@ -1615,6 +1611,13 @@ collect_cand_qtvs_co orig_ty bound = go_co
                                     (dv { dv_cvs = cvs `extendVarSet` cv })
                                     (idType cv)
 
+    go_hole :: CandidatesQTvs -> CoercionHole -> TcM CandidatesQTvs
+    go_hole dv hole = do
+      m_co <- unpackCoercionHole_maybe hole
+      case m_co of
+        Just co -> go_co dv co
+        Nothing -> go_cv dv (coHoleCoVar hole)
+
     is_bound tv = tv `elemVarSet` bound
 
 {- Note [Order of accumulation]
diff --git a/compiler/GHC/Tc/Utils/Zonk.hs b/compiler/GHC/Tc/Utils/Zonk.hs
index b0af88d813..6a0380469b 100644
--- a/compiler/GHC/Tc/Utils/Zonk.hs
+++ b/compiler/GHC/Tc/Utils/Zonk.hs
@@ -1911,10 +1911,15 @@ zonkScaledTcTypeToTypeX env (Scaled m ty) = Scaled <$> zonkTcTypeToTypeX env m
 
 zonkTcTypeToTypeX   :: ZonkEnv -> TcType   -> TcM Type
 zonkTcTypesToTypesX :: ZonkEnv -> [TcType] -> TcM [Type]
-zonkCoToCo          :: ZonkEnv -> Coercion -> TcM Coercion
-(zonkTcTypeToTypeX, zonkTcTypesToTypesX, zonkCoToCo, _)
+zonkCoToCo_, zonkCoToCo         :: ZonkEnv -> Coercion -> TcM Coercion  -- "RAE"
+(zonkTcTypeToTypeX, zonkTcTypesToTypesX, zonkCoToCo_, _)
   = mapTyCoX zonk_tycomapper
 
+zonkCoToCo env co = do { traceTc "RAE1" (ppr co)
+                       ; co' <- zonkCoToCo_ env co
+                       ; traceTc "RAE2" (ppr co')
+                       ; return co' }
+
 zonkScaledTcTypesToTypesX :: ZonkEnv -> [Scaled TcType] -> TcM [Scaled Type]
 zonkScaledTcTypesToTypesX env scaled_tys =
    mapM (zonkScaledTcTypeToTypeX env) scaled_tys
diff --git a/compiler/GHC/Types/Unique/DSet.hs b/compiler/GHC/Types/Unique/DSet.hs
index d1602e2c6e..c67a183e3c 100644
--- a/compiler/GHC/Types/Unique/DSet.hs
+++ b/compiler/GHC/Types/Unique/DSet.hs
@@ -33,7 +33,8 @@ module GHC.Types.Unique.DSet (
         lookupUniqDSet,
         uniqDSetToList,
         partitionUniqDSet,
-        mapUniqDSet
+        mapUniqDSet,
+        seqUniqDSet,
     ) where
 
 import GHC.Prelude
@@ -45,6 +46,7 @@ import GHC.Types.Unique
 
 import Data.Coerce
 import Data.Data
+import qualified Data.Semigroup
 
 -- See Note [UniqSet invariant] in GHC.Types.Unique.Set for why we want a newtype here.
 -- Beyond preserving invariants, we may also want to 'override' typeclass
@@ -53,6 +55,12 @@ import Data.Data
 newtype UniqDSet a = UniqDSet {getUniqDSet' :: UniqDFM a a}
                    deriving (Data)
 
+instance Semigroup (UniqDSet a) where
+  (<>) = unionUniqDSets
+
+instance Monoid (UniqDSet a) where
+  mempty = emptyUniqDSet
+
 instance Foldable UniqDSet where
   foldr f z = foldr f z . uniqDSetToList
 
@@ -143,3 +151,6 @@ instance Outputable a => Outputable (UniqDSet a) where
 
 pprUniqDSet :: (a -> SDoc) -> UniqDSet a -> SDoc
 pprUniqDSet f = braces . pprWithCommas f . uniqDSetToList
+
+seqUniqDSet :: UniqDSet a -> ()
+seqUniqDSet set = sizeUniqDSet set `seq` ()
\ No newline at end of file
diff --git a/testsuite/tests/dependent/should_compile/T14729.stderr b/testsuite/tests/dependent/should_compile/T14729.stderr
index ac0108be7c..3155500ff7 100644
--- a/testsuite/tests/dependent/should_compile/T14729.stderr
+++ b/testsuite/tests/dependent/should_compile/T14729.stderr
@@ -1,5 +1,7 @@
 TYPE SIGNATURES
-  x :: forall (x :: Bool). P (F Int) (x |> Sym (T14729.D:R:FInt[0]))
+  x ::
+    forall (x :: Bool).
+    P (F Int) (x |> Sym (Zapped nominal (F Int) Bool {} []))
   y :: forall {x :: Bool}. P Bool x
 TYPE CONSTRUCTORS
   type family F{1} :: * -> *
diff --git a/testsuite/tests/rep-poly/T20363_show_co.stderr b/testsuite/tests/rep-poly/T20363_show_co.stderr
index 6b18496208..b213307622 100644
--- a/testsuite/tests/rep-poly/T20363_show_co.stderr
+++ b/testsuite/tests/rep-poly/T20363_show_co.stderr
@@ -3,8 +3,8 @@ T20363_show_co.hs:23:10: error:
     • The newtype constructor pattern
       does not have a fixed runtime representation.
       Its type is:
-        ((# #) |> (TYPE (Sym (T20363_show_co.D:R:NilRep[0])))_N) :: TYPE
-                                                                      NilRep
+        ((# #) |> (TYPE
+                     (Sym (Zapped nominal NilRep ZeroBitRep {} [])))_N) :: TYPE NilRep
       NB: GHC does not (yet) support rewriting in runtime representations.
       Please comment on GHC ticket #13105 if this is causing you trouble.
       <https://gitlab.haskell.org/ghc/ghc/-/issues/13105>