Resotre nondeterministic tyCoVarsOfTypr

6 files changed, 197 insertions, 104 deletions

diff --git a/compiler/basicTypes/VarSet.hs b/compiler/basicTypes/VarSet.hs
index ac3c545b2a..dd54fd5475 100644
--- a/compiler/basicTypes/VarSet.hs
+++ b/compiler/basicTypes/VarSet.hs
@@ -13,12 +13,13 @@ module VarSet (
         emptyVarSet, unitVarSet, mkVarSet,
         extendVarSet, extendVarSetList,
         elemVarSet, subVarSet,
-        unionVarSet, unionVarSets, mapUnionVarSet,
+        unionVarSet, unionVarSets, mapUnionVarSet, mapUnionVarSetSet,
         intersectVarSet, intersectsVarSet, disjointVarSet,
         isEmptyVarSet, delVarSet, delVarSetList, delVarSetByKey,
         minusVarSet, filterVarSet, mapVarSet,
         anyVarSet, allVarSet,
         transCloVarSet, fixVarSet,
+        nonDetFoldVarSet,
         lookupVarSet_Directly, lookupVarSet, lookupVarSetByName,
         sizeVarSet, seqVarSet,
         elemVarSetByKey, partitionVarSet,
@@ -85,6 +86,9 @@ unionVarSets    :: [VarSet] -> VarSet
 mapUnionVarSet  :: (a -> VarSet) -> [a] -> VarSet
 -- ^ map the function over the list, and union the results
 
+mapUnionVarSetSet :: (Var -> VarSet) -> VarSet -> VarSet
+-- ^ map the function over the set, and union the results
+
 unitVarSet      :: Var -> VarSet
 extendVarSet    :: VarSet -> Var -> VarSet
 extendVarSetList:: VarSet -> [Var] -> VarSet
@@ -137,6 +141,8 @@ partitionVarSet = partitionUniqSet
 
 mapUnionVarSet get_set xs = foldr (unionVarSet . get_set) emptyVarSet xs
 
+mapUnionVarSetSet get_set xs = nonDetFoldUniqSet (unionVarSet . get_set) emptyVarSet xs
+
 -- See comments with type signatures
 intersectsVarSet s1 s2 = not (s1 `disjointVarSet` s2)
 disjointVarSet   s1 s2 = disjointUFM (getUniqSet s1) (getUniqSet s2)
@@ -187,6 +193,12 @@ transCloVarSet fn seeds
        where
          new_vs = fn candidates `minusVarSet` acc
 
+-- | Fold an operation over a VarSet. This is non-deterministic,
+-- and thus the operation must be commutative for determinstic
+-- behavior.
+nonDetFoldVarSet :: (Var -> a -> a) -> a -> VarSet -> a
+nonDetFoldVarSet = nonDetFoldUniqSet
+
 seqVarSet :: VarSet -> ()
 seqVarSet s = sizeVarSet s `seq` ()
 
diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs
index b1bc1d0b23..b283843b8a 100644
--- a/compiler/typecheck/TcMType.hs
+++ b/compiler/typecheck/TcMType.hs
@@ -70,7 +70,7 @@ module TcMType (
   skolemiseRuntimeUnk,
   zonkTcTyVar, zonkTcTyVars,
   zonkTcTyVarToTyVar, zonkSigTyVarPairs,
-  zonkTyCoVarsAndFV, zonkTcTypeAndFV,
+  zonkTyCoVarsAndFV,
   zonkTyCoVarsAndFVList,
   zonkTcTypeAndSplitDepVars, zonkTcTypesAndSplitDepVars,
   zonkQuantifiedTyVar, defaultTyVar,
@@ -1307,18 +1307,6 @@ tcGetGlobalTyCoVars
 zonkTcTypeInKnot :: TcType -> TcM TcType
 zonkTcTypeInKnot = mapType (zonkTcTypeMapper { tcm_smart = False }) ()
 
-zonkTcTypeAndFV :: TcType -> TcM DTyCoVarSet
--- Zonk a type and take its free variables
--- With kind polymorphism it can be essential to zonk *first*
--- so that we find the right set of free variables.  Eg
---    forall k1. forall (a:k2). a
--- where k2:=k1 is in the substitution.  We don't want
--- k2 to look free in this type!
--- NB: This might be called from within the knot, so don't use
--- smart constructors. See Note [Type-checking inside the knot] in TcHsType
-zonkTcTypeAndFV ty
-  = tyCoVarsOfTypeDSet <$> zonkTcTypeInKnot ty
-
 -- | Zonk a type and call 'candidateQTyVarsOfType' on it.
 -- Works within the knot.
 zonkTcTypeAndSplitDepVars :: TcType -> TcM CandidatesQTvs
diff --git a/compiler/typecheck/TcSplice.hs b/compiler/typecheck/TcSplice.hs
index 81cc474d32..44bb81e097 100644
--- a/compiler/typecheck/TcSplice.hs
+++ b/compiler/typecheck/TcSplice.hs
@@ -56,7 +56,6 @@ import GHCi
 import HscMain
         -- These imports are the reason that TcSplice
         -- is very high up the module hierarchy
-import FV
 import RnSplice( traceSplice, SpliceInfo(..) )
 import RdrName
 import HscTypes
@@ -1920,8 +1919,7 @@ reify_tc_app tc tys
               = splitAtList  tys tc_binders
             result_kind  = mkTyConKind remaining_binders tc_res_kind
             result_vars  = tyCoVarsOfType result_kind
-            dropped_vars = fvVarSet $
-                           mapUnionFV injectiveVarsOfBinder dropped_binders
+            dropped_vars = mapUnionVarSet injectiveVarsOfBinder dropped_binders
 
         in not (subVarSet result_vars dropped_vars)
 
diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index 9b1d07c79b..40ca0312ff 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -803,7 +803,8 @@ tcTyVarLevel tv
 tcTypeLevel :: TcType -> TcLevel
 -- Max level of any free var of the type
 tcTypeLevel ty
-  = foldDVarSet add topTcLevel (tyCoVarsOfTypeDSet ty)
+   -- OK to use non-determinism because maxTcLevel is commutative
+  = nonDetFoldVarSet add topTcLevel (tyCoVarsOfType ty)
   where
     add v lvl
       | isTcTyVar v = lvl `maxTcLevel` tcTyVarLevel v
diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs
index 5a2426487f..9d8c7a81a0 100644
--- a/compiler/types/TyCoRep.hs
+++ b/compiler/types/TyCoRep.hs
@@ -1499,7 +1499,83 @@ the variables. This is for two reasons:
 -- synonym.
 tyCoVarsOfType :: Type -> TyCoVarSet
 -- See Note [Free variables of types]
-tyCoVarsOfType ty = fvVarSet $ tyCoFVsOfType ty
+tyCoVarsOfType = closeOverKinds . tcvs_of_type
+
+-- | Returns free variables of types, including kind variables as
+-- a non-deterministic set. For type synonyms it does /not/ expand the
+-- synonym.
+tyCoVarsOfTypes :: [Type] -> TyCoVarSet
+-- See Note [Free variables of types]
+tyCoVarsOfTypes = closeOverKinds . tcvs_of_types
+
+tyCoVarsOfCo :: Coercion -> TyCoVarSet
+-- See Note [Free variables of types]
+tyCoVarsOfCo = closeOverKinds . tcvs_of_co
+
+tyCoVarsOfCos :: [Coercion] -> TyCoVarSet
+tyCoVarsOfCos = closeOverKinds . tcvs_of_cos
+
+tyCoVarsOfCosSet :: CoVarEnv Coercion -> TyCoVarSet
+tyCoVarsOfCosSet = tyCoVarsOfCos . nonDetEltsUFM
+  -- It's OK to use nonDetEltsUFM here because we immediately forget the
+  -- ordering by returning a set
+
+-- | Add the kind variables free in the kinds of the tyvars in the given set.
+-- Returns a non-deterministic set.
+closeOverKinds :: TyCoVarSetNotClosed -> TyCoVarSet
+closeOverKinds tcvs = mapUnionVarSetSet (tyCoVarsOfType . tyVarKind) tcvs `unionVarSet` tcvs
+
+-- Explicitly note that these sets are not closed over kinds
+type TyCoVarSetNotClosed = TyCoVarSet
+
+-- These functions produce a non-deterministic set. No point in going via FV (which maintains
+-- determinism info) and then drop the determinism. This is boring boiler plate code, but this
+-- is measurably faster than going via FV.
+tcvs_of_type :: Type -> TyCoVarSetNotClosed
+tcvs_of_type (TyVarTy v)                 = unitVarSet v
+tcvs_of_type (TyConApp _ tys)            = mapUnionVarSet tcvs_of_type tys
+tcvs_of_type (LitTy {})                  = emptyVarSet
+tcvs_of_type (AppTy fun arg)             = tcvs_of_type fun `unionVarSet` tcvs_of_type arg
+tcvs_of_type (FunTy arg res)             = tcvs_of_type arg `unionVarSet` tcvs_of_type res
+tcvs_of_type (ForAllTy (TvBndr tv _) ty) = tcvs_of_type ty `delVarSet` tv
+                                                           `unionVarSet` tcvs_of_type (tyVarKind tv)
+tcvs_of_type (CastTy ty co)              = tcvs_of_type ty `unionVarSet` tcvs_of_co co
+tcvs_of_type (CoercionTy co)             = tcvs_of_co co
+
+tcvs_of_types :: [Type] -> TyCoVarSetNotClosed
+tcvs_of_types = mapUnionVarSet tcvs_of_type
+
+tcvs_of_co :: Coercion -> TyCoVarSetNotClosed
+tcvs_of_co (Refl _ ty)              = tcvs_of_type ty
+tcvs_of_co (TyConAppCo _ _ cos)     = tcvs_of_cos cos
+tcvs_of_co (AppCo co arg)           = tcvs_of_co co `unionVarSet` tcvs_of_co arg
+tcvs_of_co (ForAllCo tv kind_co co) = tcvs_of_co co `delVarSet` tv
+                                                    `unionVarSet` tcvs_of_co kind_co
+tcvs_of_co (FunCo _ co1 co2)        = tcvs_of_co co1 `unionVarSet` tcvs_of_co co2
+tcvs_of_co (CoVarCo v)              = unitVarSet v
+tcvs_of_co (HoleCo h)               = unitVarSet (coHoleCoVar h)
+    -- See Note [CoercionHoles and coercion free variables]
+tcvs_of_co (AxiomInstCo _ _ cos)    = tcvs_of_cos cos
+tcvs_of_co (UnivCo p _ t1 t2)       = tcvs_of_prov p `unionVarSet` tcvs_of_type t1
+                                                     `unionVarSet` tcvs_of_type t2
+tcvs_of_co (SymCo co)          = tcvs_of_co co
+tcvs_of_co (TransCo co1 co2)   = tcvs_of_co co1 `unionVarSet` tcvs_of_co co2
+tcvs_of_co (NthCo _ _ co)      = tcvs_of_co co
+tcvs_of_co (LRCo _ co)         = tcvs_of_co co
+tcvs_of_co (InstCo co arg)     = tcvs_of_co co `unionVarSet` tcvs_of_co arg
+tcvs_of_co (CoherenceCo c1 c2) = tcvs_of_co c1 `unionVarSet` tcvs_of_co c2
+tcvs_of_co (KindCo co)         = tcvs_of_co co
+tcvs_of_co (SubCo co)          = tcvs_of_co co
+tcvs_of_co (AxiomRuleCo _ cs)  = tcvs_of_cos cs
+
+tcvs_of_cos :: [Coercion] -> TyCoVarSetNotClosed
+tcvs_of_cos = mapUnionVarSet tcvs_of_co
+
+tcvs_of_prov :: UnivCoProvenance -> TyCoVarSetNotClosed
+tcvs_of_prov UnsafeCoerceProv    = emptyVarSet
+tcvs_of_prov (PhantomProv co)    = tcvs_of_co co
+tcvs_of_prov (ProofIrrelProv co) = tcvs_of_co co
+tcvs_of_prov (PluginProv _)      = emptyVarSet
 
 -- | `tyCoFVsOfType` that returns free variables of a type in a deterministic
 -- set. For explanation of why using `VarSet` is not deterministic see
@@ -1553,12 +1629,42 @@ fvs_of_bndr :: TyVarBinder -> FVNotClosed -> FVNotClosed
 fvs_of_bndr (TvBndr tv _) fvs = (delFV tv fvs)
                                 `unionFV` fvs_of_type (tyVarKind tv)
 
--- | Returns free variables of types, including kind variables as
--- a non-deterministic set. For type synonyms it does /not/ expand the
--- synonym.
-tyCoVarsOfTypes :: [Type] -> TyCoVarSet
--- See Note [Free variables of types]
-tyCoVarsOfTypes tys = fvVarSet $ tyCoFVsOfTypes tys
+fvs_of_co :: Coercion -> FVNotClosed
+fvs_of_co (Refl _ ty)         fv_cand in_scope acc = fvs_of_type ty fv_cand in_scope acc
+fvs_of_co (TyConAppCo _ _ cos) fv_cand in_scope acc = fvs_of_cos cos fv_cand in_scope acc
+fvs_of_co (AppCo co arg) fv_cand in_scope acc
+  = (fvs_of_co co `unionFV` fvs_of_co arg) fv_cand in_scope acc
+fvs_of_co (ForAllCo tv kind_co co) fv_cand in_scope acc
+  = (delFV tv (fvs_of_co co) `unionFV` fvs_of_co kind_co) fv_cand in_scope acc
+fvs_of_co (FunCo _ co1 co2)    fv_cand in_scope acc
+  = (fvs_of_co co1 `unionFV` fvs_of_co co2) fv_cand in_scope acc
+fvs_of_co (CoVarCo v) fv_cand in_scope acc
+  = unitFV v fv_cand in_scope acc
+fvs_of_co (HoleCo h) fv_cand in_scope acc
+  = unitFV (coHoleCoVar h) fv_cand in_scope acc
+    -- See Note [CoercionHoles and coercion free variables]
+fvs_of_co (AxiomInstCo _ _ cos) fv_cand in_scope acc = fvs_of_cos cos fv_cand in_scope acc
+fvs_of_co (UnivCo p _ t1 t2) fv_cand in_scope acc
+  = (fvs_of_prov p `unionFV` fvs_of_type t1
+                     `unionFV` fvs_of_type t2) fv_cand in_scope acc
+fvs_of_co (SymCo co)          fv_cand in_scope acc = fvs_of_co co fv_cand in_scope acc
+fvs_of_co (TransCo co1 co2)   fv_cand in_scope acc = (fvs_of_co co1 `unionFV` fvs_of_co co2) fv_cand in_scope acc
+fvs_of_co (NthCo _ _ co)      fv_cand in_scope acc = fvs_of_co co fv_cand in_scope acc
+fvs_of_co (LRCo _ co)         fv_cand in_scope acc = fvs_of_co co fv_cand in_scope acc
+fvs_of_co (InstCo co arg)     fv_cand in_scope acc = (fvs_of_co co `unionFV` fvs_of_co arg) fv_cand in_scope acc
+fvs_of_co (CoherenceCo c1 c2) fv_cand in_scope acc = (fvs_of_co c1 `unionFV` fvs_of_co c2) fv_cand in_scope acc
+fvs_of_co (KindCo co)         fv_cand in_scope acc = fvs_of_co co fv_cand in_scope acc
+fvs_of_co (SubCo co)          fv_cand in_scope acc = fvs_of_co co fv_cand in_scope acc
+fvs_of_co (AxiomRuleCo _ cs)  fv_cand in_scope acc = fvs_of_cos cs fv_cand in_scope acc
+
+fvs_of_cos :: [Coercion] -> FVNotClosed
+fvs_of_cos = mapUnionFV fvs_of_co
+
+fvs_of_prov :: UnivCoProvenance -> FVNotClosed
+fvs_of_prov UnsafeCoerceProv    fv_cand in_scope acc = emptyFV fv_cand in_scope acc
+fvs_of_prov (PhantomProv co)    fv_cand in_scope acc = fvs_of_co co fv_cand in_scope acc
+fvs_of_prov (ProofIrrelProv co) fv_cand in_scope acc = fvs_of_co co fv_cand in_scope acc
+fvs_of_prov (PluginProv _)      fv_cand in_scope acc = emptyFV fv_cand in_scope acc
 
 -- | Returns free variables of types, including kind variables as
 -- a non-deterministic set. For type synonyms it does /not/ expand the
@@ -1588,10 +1694,6 @@ tyCoFVsOfTypes :: [Type] -> FV
 tyCoFVsOfTypes (ty:tys) fv_cand in_scope acc = (tyCoFVsOfType ty `unionFV` tyCoFVsOfTypes tys) fv_cand in_scope acc
 tyCoFVsOfTypes []       fv_cand in_scope acc = emptyFV fv_cand in_scope acc
 
-tyCoVarsOfCo :: Coercion -> TyCoVarSet
--- See Note [Free variables of types]
-tyCoVarsOfCo co = fvVarSet $ tyCoFVsOfCo co
-
 -- | Get a deterministic set of the vars free in a coercion
 tyCoVarsOfCoDSet :: Coercion -> DTyCoVarSet
 -- See Note [Free variables of types]
@@ -1607,71 +1709,63 @@ tyCoFVsOfCo :: Coercion -> FV
 tyCoFVsOfCo co = let unclosed = fvs_of_co co in
                  closeOverKindsFV unclosed
 
-fvs_of_co :: Coercion -> FVNotClosed
-fvs_of_co (Refl _ ty)         fv_cand in_scope acc = fvs_of_type ty fv_cand in_scope acc
-fvs_of_co (TyConAppCo _ _ cos) fv_cand in_scope acc = fvs_of_cos cos fv_cand in_scope acc
-fvs_of_co (AppCo co arg) fv_cand in_scope acc
-  = (fvs_of_co co `unionFV` fvs_of_co arg) fv_cand in_scope acc
-fvs_of_co (ForAllCo tv kind_co co) fv_cand in_scope acc
-  = (delFV tv (fvs_of_co co) `unionFV` fvs_of_co kind_co) fv_cand in_scope acc
-fvs_of_co (FunCo _ co1 co2)    fv_cand in_scope acc
-  = (fvs_of_co co1 `unionFV` fvs_of_co co2) fv_cand in_scope acc
-fvs_of_co (CoVarCo v) fv_cand in_scope acc
-  = unitFV v fv_cand in_scope acc
-fvs_of_co (HoleCo h) fv_cand in_scope acc
-  = unitFV (coHoleCoVar h) fv_cand in_scope acc
-    -- See Note [CoercionHoles and coercion free variables]
-fvs_of_co (AxiomInstCo _ _ cos) fv_cand in_scope acc = fvs_of_cos cos fv_cand in_scope acc
-fvs_of_co (UnivCo p _ t1 t2) fv_cand in_scope acc
-  = (fvs_of_prov p `unionFV` fvs_of_type t1
-                     `unionFV` fvs_of_type t2) fv_cand in_scope acc
-fvs_of_co (SymCo co)          fv_cand in_scope acc = fvs_of_co co fv_cand in_scope acc
-fvs_of_co (TransCo co1 co2)   fv_cand in_scope acc = (fvs_of_co co1 `unionFV` fvs_of_co co2) fv_cand in_scope acc
-fvs_of_co (NthCo _ _ co)      fv_cand in_scope acc = fvs_of_co co fv_cand in_scope acc
-fvs_of_co (LRCo _ co)         fv_cand in_scope acc = fvs_of_co co fv_cand in_scope acc
-fvs_of_co (InstCo co arg)     fv_cand in_scope acc = (fvs_of_co co `unionFV` fvs_of_co arg) fv_cand in_scope acc
-fvs_of_co (CoherenceCo c1 c2) fv_cand in_scope acc = (fvs_of_co c1 `unionFV` fvs_of_co c2) fv_cand in_scope acc
-fvs_of_co (KindCo co)         fv_cand in_scope acc = fvs_of_co co fv_cand in_scope acc
-fvs_of_co (SubCo co)          fv_cand in_scope acc = fvs_of_co co fv_cand in_scope acc
-fvs_of_co (AxiomRuleCo _ cs)  fv_cand in_scope acc = fvs_of_cos cs fv_cand in_scope acc
-
-fvs_of_cos :: [Coercion] -> FVNotClosed
-fvs_of_cos = mapUnionFV fvs_of_co
-
-fvs_of_prov :: UnivCoProvenance -> FVNotClosed
-fvs_of_prov UnsafeCoerceProv    fv_cand in_scope acc = emptyFV fv_cand in_scope acc
-fvs_of_prov (PhantomProv co)    fv_cand in_scope acc = fvs_of_co co fv_cand in_scope acc
-fvs_of_prov (ProofIrrelProv co) fv_cand in_scope acc = fvs_of_co co fv_cand in_scope acc
-fvs_of_prov (PluginProv _)      fv_cand in_scope acc = emptyFV fv_cand in_scope acc
-
-tyCoVarsOfCos :: [Coercion] -> TyCoVarSet
-tyCoVarsOfCos cos = fvVarSet $ tyCoFVsOfCos cos
-
-tyCoVarsOfCosSet :: CoVarEnv Coercion -> TyCoVarSet
-tyCoVarsOfCosSet cos = fvVarSet $ tyCoFVsOfCos $ nonDetEltsUFM cos
-  -- It's OK to use nonDetEltsUFM here because we immediately forget the
-  -- ordering by returning a set
-
 tyCoFVsOfCos :: [Coercion] -> FV
 tyCoFVsOfCos []       fv_cand in_scope acc = emptyFV fv_cand in_scope acc
 tyCoFVsOfCos (co:cos) fv_cand in_scope acc = (tyCoFVsOfCo co `unionFV` tyCoFVsOfCos cos) fv_cand in_scope acc
 
+-- NB: We can't just collect the covars and then closeOverKinds, because that
+-- would miss a covar mentioned only in the kind of a type variable. Also,
+-- this can't suffer from the problem in Note [Closiing over free variable kinds]
+-- because we can't bind coercion variables locally in a type.
 coVarsOfType :: Type -> CoVarSet
-coVarsOfType = filterVarSet isCoVar . tyCoVarsOfType
-
-coVarsOfTypes :: [Type] -> CoVarSet
-coVarsOfTypes = mapUnionVarSet coVarsOfType
+coVarsOfType (TyVarTy v)         = coVarsOfType (tyVarKind v)
+coVarsOfType (TyConApp _ tys)    = coVarsOfTypes tys
+coVarsOfType (LitTy {})          = emptyVarSet
+coVarsOfType (AppTy fun arg)     = coVarsOfType fun `unionVarSet` coVarsOfType arg
+coVarsOfType (FunTy arg res)     = coVarsOfType arg `unionVarSet` coVarsOfType res
+coVarsOfType (ForAllTy (TvBndr tv _) ty)
+  = (coVarsOfType ty `delVarSet` tv)
+    `unionVarSet` coVarsOfType (tyVarKind tv)
+coVarsOfType (CastTy ty co)      = coVarsOfType ty `unionVarSet` coVarsOfCo co
+coVarsOfType (CoercionTy co)     = coVarsOfCo co
+
+coVarsOfTypes :: [Type] -> TyCoVarSet
+coVarsOfTypes tys = mapUnionVarSet coVarsOfType tys
 
 coVarsOfCo :: Coercion -> CoVarSet
--- Extract *coercion* variables only.
-coVarsOfCo = filterVarSet isCoVar . tyCoVarsOfCo
-
--- | Add the kind variables free in the kinds of the tyvars in the given set.
--- Returns a non-deterministic set.
-closeOverKinds :: TyVarSet -> TyVarSet
-closeOverKinds = fvVarSet . closeOverKindsFV . mkFVs . nonDetEltsUniqSet
-  -- It's OK to use nonDetEltsUniqSet here because we immediately forget
-  -- about the ordering by returning a set.
+-- Extract *coercion* variables only.  Tiresome to repeat the code, but easy.
+coVarsOfCo (Refl _ ty)          = coVarsOfType ty
+coVarsOfCo (TyConAppCo _ _ args)= coVarsOfCos args
+coVarsOfCo (AppCo co arg)       = coVarsOfCo co `unionVarSet` coVarsOfCo arg
+coVarsOfCo (ForAllCo tv kind_co co)
+  = coVarsOfCo co `delVarSet` tv `unionVarSet` coVarsOfCo kind_co
+coVarsOfCo (FunCo _ co1 co2)    = coVarsOfCo co1 `unionVarSet` coVarsOfCo co2
+coVarsOfCo (CoVarCo v)          = coVarsOfCoVar v
+coVarsOfCo (HoleCo h)           = coVarsOfCoVar (coHoleCoVar h)
+                                  -- See Note [CoercionHoles and coercion free variables]
+coVarsOfCo (AxiomInstCo _ _ as) = coVarsOfCos as
+coVarsOfCo (UnivCo p _ t1 t2)   = coVarsOfProv p `unionVarSet` coVarsOfTypes [t1, t2]
+coVarsOfCo (SymCo co)           = coVarsOfCo co
+coVarsOfCo (TransCo co1 co2)    = coVarsOfCo co1 `unionVarSet` coVarsOfCo co2
+coVarsOfCo (NthCo _ _ co)       = coVarsOfCo co
+coVarsOfCo (LRCo _ co)          = coVarsOfCo co
+coVarsOfCo (InstCo co arg)      = coVarsOfCo co `unionVarSet` coVarsOfCo arg
+coVarsOfCo (CoherenceCo c1 c2)  = coVarsOfCos [c1, c2]
+coVarsOfCo (KindCo co)          = coVarsOfCo co
+coVarsOfCo (SubCo co)           = coVarsOfCo co
+coVarsOfCo (AxiomRuleCo _ cs)   = coVarsOfCos cs
+
+coVarsOfCoVar :: CoVar -> CoVarSet
+coVarsOfCoVar v = unitVarSet v `unionVarSet` coVarsOfType (varType v)
+
+coVarsOfProv :: UnivCoProvenance -> CoVarSet
+coVarsOfProv UnsafeCoerceProv    = emptyVarSet
+coVarsOfProv (PhantomProv co)    = coVarsOfCo co
+coVarsOfProv (ProofIrrelProv co) = coVarsOfCo co
+coVarsOfProv (PluginProv _)      = emptyVarSet
+
+coVarsOfCos :: [Coercion] -> CoVarSet
+coVarsOfCos cos = mapUnionVarSet coVarsOfCo cos
 
 -- | Given a list of tyvars returns a deterministic FV computation that
 -- returns the given tyvars with the kind variables free in the kinds of the
@@ -1693,38 +1787,38 @@ closeOverKindsDSet = fvDVarSet . closeOverKindsFV . mkFVs . dVarSetElems
 -- | Returns the free variables of a 'TyConBinder' that are in injective
 -- positions. (See @Note [Kind annotations on TyConApps]@ in "TcSplice" for an
 -- explanation of what an injective position is.)
-injectiveVarsOfBinder :: TyConBinder -> FV
+injectiveVarsOfBinder :: TyConBinder -> TyVarSet
 injectiveVarsOfBinder (TvBndr tv vis) =
   case vis of
     AnonTCB           -> injectiveVarsOfType (tyVarKind tv)
-    NamedTCB Required -> unitFV tv `unionFV`
+    NamedTCB Required -> unitVarSet tv `unionVarSet`
                          injectiveVarsOfType (tyVarKind tv)
-    NamedTCB _        -> emptyFV
+    NamedTCB _        -> emptyVarSet
 
 -- | Returns the free variables of a 'Type' that are in injective positions.
 -- (See @Note [Kind annotations on TyConApps]@ in "TcSplice" for an explanation
 -- of what an injective position is.)
-injectiveVarsOfType :: Type -> FV
-injectiveVarsOfType orig_ty = closeOverKindsFV (go orig_ty)
+injectiveVarsOfType :: Type -> TyVarSet
+injectiveVarsOfType orig_ty = closeOverKinds (go orig_ty)
   where
-    go :: Type -> FVNotClosed
+    go :: Type -> TyCoVarSetNotClosed
     go ty                | Just ty' <- coreView ty
                          = go ty'
-    go (TyVarTy v)       = unitFV v
-    go (AppTy f a)       = go f `unionFV` go a
-    go (FunTy ty1 ty2)   = go ty1 `unionFV` go ty2
+    go (TyVarTy v)       = unitVarSet v
+    go (AppTy f a)       = go f `unionVarSet` go a
+    go (FunTy ty1 ty2)   = go ty1 `unionVarSet` go ty2
     go (TyConApp tc tys) =
       case tyConInjectivityInfo tc of
-        NotInjective  -> emptyFV
-        Injective inj -> mapUnionFV go $
+        NotInjective  -> emptyVarSet
+        Injective inj -> mapUnionVarSet go $
                          filterByList (inj ++ repeat True) tys
                          -- Oversaturated arguments to a tycon are
                          -- always injective, hence the repeat True
-    go (ForAllTy tvb ty) = fvs_of_bndr tvb $ go (tyVarKind (binderVar tvb))
-                                             `unionFV` go ty
-    go LitTy{}           = emptyFV
+    go (ForAllTy (TvBndr tv _) ty) = go ty `delVarSet` tv
+                                           `unionVarSet` go (tyVarKind tv)
+    go LitTy{}           = emptyVarSet
     go (CastTy ty _)     = go ty
-    go CoercionTy{}      = emptyFV
+    go CoercionTy{}      = emptyVarSet
 
 -- | Returns True if this type has no free variables. Should be the same as
 -- isEmptyVarSet . tyCoVarsOfType, but faster in the non-forall case.
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index 967d2c6866..3c58b3fc98 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -2042,7 +2042,7 @@ isValidJoinPointType arity ty
   where
     valid_under tvs arity ty
       | arity == 0
-      = isEmptyVarSet (tvs `intersectVarSet` tyCoVarsOfType ty)
+      = tvs `intersectsVarSet` tyCoVarsOfType ty
       | Just (t, ty') <- splitForAllTy_maybe ty
       = valid_under (tvs `extendVarSet` t) (arity-1) ty'
       | Just (_, res_ty) <- splitFunTy_maybe ty
@@ -2184,7 +2184,7 @@ nonDetCmpType t1 t2
 nonDetCmpTypes :: [Type] -> [Type] -> Ordering
 nonDetCmpTypes ts1 ts2 = nonDetCmpTypesX rn_env ts1 ts2
   where
-    rn_env = mkRnEnv2 (mkInScopeSet (tyCoVarsOfTypes (ts1 ++ ts2)))
+    rn_env = mkRnEnv2 (mkInScopeSet (tyCoVarsOfTypes ts1 `unionVarSet` tyCoVarsOfTypes ts2))
 
 -- | An ordering relation between two 'Type's (known below as @t1 :: k1@
 -- and @t2 :: k2@)