diff options
Diffstat (limited to 'compiler/types/TyCoRep.hs')
-rw-r--r-- | compiler/types/TyCoRep.hs | 379 |
1 files changed, 283 insertions, 96 deletions
diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs index 81cd2b0f95..595799bbd7 100644 --- a/compiler/types/TyCoRep.hs +++ b/compiler/types/TyCoRep.hs @@ -1520,6 +1520,10 @@ so, so it's easiest to do it here. -} +{- +----------------------------------------------------------------- +--------------------- Baseline version (uses FV) ---------------- + -- | Returns free variables of a type, including kind variables as -- a non-deterministic set. For type synonyms it does /not/ expand the -- synonym. @@ -1527,6 +1531,209 @@ tyCoVarsOfType :: Type -> TyCoVarSet -- See Note [Free variables of types] tyCoVarsOfType ty = fvVarSet $ tyCoFVsOfType ty +-- | 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 + +tyCoVarsOfCo :: Coercion -> TyCoVarSet +-- See Note [Free variables of types] +tyCoVarsOfCo co = fvVarSet $ tyCoFVsOfCo co + +tyCoVarsOfCos :: [Coercion] -> TyCoVarSet +tyCoVarsOfCos cos = fvVarSet $ tyCoFVsOfCos cos + +tyCoVarsOfProv :: UnivCoProvenance -> TyCoVarSet +tyCoVarsOfProv prov = fvVarSet $ tyCoFVsOfProv prov + +-- | Generates an in-scope set from the free variables in a list of types +-- and a list of coercions +mkTyCoInScopeSet :: [Type] -> [Coercion] -> InScopeSet +mkTyCoInScopeSet tys cos + = mkInScopeSet (tyCoVarsOfTypes tys `unionVarSet` tyCoVarsOfCos cos) + +--------------------- End of Baseline version ---------------- +----------------------------------------------------------------- +-} + +{- +----------------------------------------------------------------- +--------------------- UnionVarSet version ---------------- +-- | 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 = mapUnionVarSet tyCoVarsOfType tys + +tyCoVarsOfType :: Type -> TyCoVarSet +-- See Note [Free variables of types] +tyCoVarsOfType (TyVarTy v) = extendVarSet (tyCoVarsOfType (tyVarKind v)) v +tyCoVarsOfType (TyConApp _ tys) = tyCoVarsOfTypes tys +tyCoVarsOfType (LitTy {}) = emptyVarSet +tyCoVarsOfType (AppTy fun arg) = (tyCoVarsOfType fun `unionVarSet` tyCoVarsOfType arg) +tyCoVarsOfType (FunTy arg res) = (tyCoVarsOfType arg `unionVarSet` tyCoVarsOfType res) +tyCoVarsOfType (ForAllTy bndr ty) = tyCoVarSetsBndr bndr (tyCoVarsOfType ty) +tyCoVarsOfType (CastTy ty co) = (tyCoVarsOfType ty `unionVarSet` tyCoVarsOfCo co) +tyCoVarsOfType (CoercionTy co) = tyCoVarsOfCo co + +tyCoVarSetsBndr :: TyVarBinder -> VarSet -> VarSet +-- Free vars of (forall b. <thing with fvs>) +tyCoVarSetsBndr (TvBndr tv _) fvs = (delVarSet fvs tv) + `unionVarSet` tyCoVarsOfType (tyVarKind tv) + +tyCoVarsOfCo :: Coercion -> TyCoVarSet +-- See Note [Free variables of types] +tyCoVarsOfCo (Refl _ ty) = tyCoVarsOfType ty +tyCoVarsOfCo (TyConAppCo _ _ cos) = tyCoVarsOfCos cos +tyCoVarsOfCo (AppCo co arg) + = (tyCoVarsOfCo co `unionVarSet` tyCoVarsOfCo arg) +tyCoVarsOfCo (ForAllCo tv kind_co co) + = (delVarSet (tyCoVarsOfCo co) tv `unionVarSet` tyCoVarsOfCo kind_co) +tyCoVarsOfCo (FunCo _ co1 co2) + = (tyCoVarsOfCo co1 `unionVarSet` tyCoVarsOfCo co2) +tyCoVarsOfCo (CoVarCo v) + = tyCoVarsOfCoVar v +tyCoVarsOfCo (HoleCo h) + = tyCoVarsOfCoVar (coHoleCoVar h) + -- See Note [CoercionHoles and coercion free variables] +tyCoVarsOfCo (AxiomInstCo _ _ cos) = tyCoVarsOfCos cos +tyCoVarsOfCo (UnivCo p _ t1 t2) + = (tyCoVarsOfProv p `unionVarSet` tyCoVarsOfType t1 + `unionVarSet` tyCoVarsOfType t2) +tyCoVarsOfCo (SymCo co) = tyCoVarsOfCo co +tyCoVarsOfCo (TransCo co1 co2) = (tyCoVarsOfCo co1 `unionVarSet` tyCoVarsOfCo co2) +tyCoVarsOfCo (NthCo _ _ co) = tyCoVarsOfCo co +tyCoVarsOfCo (LRCo _ co) = tyCoVarsOfCo co +tyCoVarsOfCo (InstCo co arg) = (tyCoVarsOfCo co `unionVarSet` tyCoVarsOfCo arg) +tyCoVarsOfCo (CoherenceCo c1 c2) = (tyCoVarsOfCo c1 `unionVarSet` tyCoVarsOfCo c2) +tyCoVarsOfCo (KindCo co) = tyCoVarsOfCo co +tyCoVarsOfCo (SubCo co) = tyCoVarsOfCo co +tyCoVarsOfCo (AxiomRuleCo _ cs) = tyCoVarsOfCos cs + +tyCoVarsOfCoVar :: CoVar -> VarSet +tyCoVarsOfCoVar v = (unitVarSet v `unionVarSet` tyCoVarsOfType (varType v)) + +tyCoVarsOfCos :: [Coercion] -> TyCoVarSet +-- tyCoVarsOfCos cos = fvVarSet $ tyCoFVsOfCos cos +tyCoVarsOfCos cos = mapUnionVarSet tyCoVarsOfCo cos + +tyCoVarsOfProv :: UnivCoProvenance -> TyCoVarSet +tyCoVarsOfProv prov = fvVarSet $ tyCoFVsOfProv pro +tyCoVarsOfProv (PhantomProv co) = tyTyCoVarsOfCo co +tyCoVarsOfProv (ProofIrrelProv co) = tyTyCoVarsOfCo co +tyCoVarsOfProv UnsafeCoerceProv = acc +tyCoVarsOfProv (PluginProv _) = acc + +-- | Generates an in-scope set from the free variables in a list of types +-- and a list of coercions +mkTyCoInScopeSet :: [Type] -> [Coercion] -> InScopeSet +mkTyCoInScopeSet tys cos + = mkInScopeSet (tyCoVarsOfTypes tys `unionVarSet` tyCoVarsOfCos cos) +--------------------- End of UnionVarSet version ---------------- +----------------------------------------------------------------- +-} + +----------------------------------------------------------------- +--------------------- Accumulator version ---------------- + +tyCoVarsOfType :: Type -> TyCoVarSet +-- See Note [Free variables of types] +tyCoVarsOfType ty = ty_co_vars_of_type ty emptyVarSet emptyVarSet + +tyCoVarsOfTypes :: [Type] -> TyCoVarSet +tyCoVarsOfTypes tys = ty_co_vars_of_types tys emptyVarSet emptyVarSet + +ty_co_vars_of_type :: Type -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet +ty_co_vars_of_type (TyVarTy v) is acc + | v `elemVarSet` is = acc + | v `elemVarSet` acc = acc + | otherwise = ty_co_vars_of_type (tyVarKind v) is (extendVarSet acc v) +ty_co_vars_of_type (TyConApp _ tys) is acc = ty_co_vars_of_types tys is acc +ty_co_vars_of_type (LitTy {}) _ acc = acc +ty_co_vars_of_type (AppTy fun arg) is acc = ty_co_vars_of_type fun is (ty_co_vars_of_type arg is acc) +ty_co_vars_of_type (FunTy arg res) is acc = ty_co_vars_of_type arg is (ty_co_vars_of_type res is acc) +ty_co_vars_of_type (ForAllTy (TvBndr tv _) ty) is acc = ty_co_vars_of_type (tyVarKind tv) is $ + ty_co_vars_of_type ty (extendVarSet is tv) acc +ty_co_vars_of_type (CastTy ty co) is acc = ty_co_vars_of_type ty is (ty_co_vars_of_co co is acc) +ty_co_vars_of_type (CoercionTy co) is acc = ty_co_vars_of_co co is acc + +ty_co_vars_of_types :: [Type] -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet +ty_co_vars_of_types [] _ acc = acc +ty_co_vars_of_types (ty:tys) is acc = ty_co_vars_of_type ty is (ty_co_vars_of_types tys is acc) + +tyCoVarsOfCo :: Coercion -> TyCoVarSet +-- See Note [Free variables of types] +tyCoVarsOfCo co = ty_co_vars_of_co co emptyVarSet emptyVarSet + +tyCoVarsOfCos :: [Coercion] -> TyCoVarSet +tyCoVarsOfCos cos = ty_co_vars_of_cos cos emptyVarSet emptyVarSet + + +ty_co_vars_of_co :: Coercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet +ty_co_vars_of_co (Refl ty) is acc = ty_co_vars_of_type ty is acc +ty_co_vars_of_co (GRefl _ ty mrefl) is acc = ty_co_vars_of_type ty is $ + ty_co_vars_of_mco mrefl is acc +ty_co_vars_of_co (TyConAppCo _ _ cos) is acc = ty_co_vars_of_cos cos is acc +ty_co_vars_of_co (AppCo co arg) is acc = ty_co_vars_of_co co is $ + ty_co_vars_of_co arg is acc +ty_co_vars_of_co (ForAllCo tv kind_co co) is acc = ty_co_vars_of_co kind_co is $ + ty_co_vars_of_co co (extendVarSet is tv) acc +ty_co_vars_of_co (FunCo _ co1 co2) is acc = ty_co_vars_of_co co1 is $ + ty_co_vars_of_co co2 is acc +ty_co_vars_of_co (CoVarCo v) is acc = ty_co_vars_of_co_var v is acc +ty_co_vars_of_co (HoleCo h) is acc = ty_co_vars_of_co_var (coHoleCoVar h) is acc + -- See Note [CoercionHoles and coercion free variables] +ty_co_vars_of_co (AxiomInstCo _ _ cos) is acc = ty_co_vars_of_cos cos is acc +ty_co_vars_of_co (UnivCo p _ t1 t2) is acc = ty_co_vars_of_prov p is $ + ty_co_vars_of_type t1 is $ + ty_co_vars_of_type t2 is acc +ty_co_vars_of_co (SymCo co) is acc = ty_co_vars_of_co co is acc +ty_co_vars_of_co (TransCo co1 co2) is acc = ty_co_vars_of_co co1 is $ + ty_co_vars_of_co co2 is acc +ty_co_vars_of_co (NthCo _ _ co) is acc = ty_co_vars_of_co co is acc +ty_co_vars_of_co (LRCo _ co) is acc = ty_co_vars_of_co co is acc +ty_co_vars_of_co (InstCo co arg) is acc = ty_co_vars_of_co co is $ + ty_co_vars_of_co arg is acc +ty_co_vars_of_co (KindCo co) is acc = ty_co_vars_of_co co is acc +ty_co_vars_of_co (SubCo co) is acc = ty_co_vars_of_co co is acc +ty_co_vars_of_co (AxiomRuleCo _ cs) is acc = ty_co_vars_of_cos cs is acc + +ty_co_vars_of_mco :: MCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet +ty_co_vars_of_mco MRefl _is acc = acc +ty_co_vars_of_mco (MCo co) is acc = ty_co_vars_of_co co is acc + +ty_co_vars_of_co_var :: CoVar -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet +ty_co_vars_of_co_var v is acc + | v `elemVarSet` is = acc + | v `elemVarSet` is = acc + | otherwise = ty_co_vars_of_type (varType v) is (extendVarSet acc v) + +ty_co_vars_of_cos :: [Coercion] -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet +ty_co_vars_of_cos [] _ acc = acc +ty_co_vars_of_cos (co:cos) is acc = ty_co_vars_of_co co is (ty_co_vars_of_cos cos is acc) + +tyCoVarsOfProv :: UnivCoProvenance -> TyCoVarSet +tyCoVarsOfProv prov = ty_co_vars_of_prov prov emptyVarSet emptyVarSet + +ty_co_vars_of_prov :: UnivCoProvenance -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet +ty_co_vars_of_prov (PhantomProv co) is acc = ty_co_vars_of_co co is acc +ty_co_vars_of_prov (ProofIrrelProv co) is acc = ty_co_vars_of_co co is acc +ty_co_vars_of_prov UnsafeCoerceProv _ acc = acc +ty_co_vars_of_prov (PluginProv _) _ acc = acc + +-- | Generates an in-scope set from the free variables in a list of types +-- and a list of coercions +mkTyCoInScopeSet :: [Type] -> [Coercion] -> InScopeSet +mkTyCoInScopeSet tys cos + = mkInScopeSet (ty_co_vars_of_types tys emptyVarSet $ + ty_co_vars_of_cos cos emptyVarSet emptyVarSet) + +--------------------- End of accumulator version ---------------- +----------------------------------------------------------------- + -- | `tyCoFVsOfType` that returns free variables of a type in a deterministic -- set. For explanation of why using `VarSet` is not deterministic see -- Note [Deterministic FV] in FV. @@ -1541,6 +1748,29 @@ tyCoVarsOfTypeList :: Type -> [TyCoVar] -- See Note [Free variables of types] tyCoVarsOfTypeList ty = fvVarList $ tyCoFVsOfType ty +-- | Returns free variables of types, including kind variables as +-- a non-deterministic set. For type synonyms it does /not/ expand the +-- synonym. +tyCoVarsOfTypesSet :: TyVarEnv Type -> TyCoVarSet +-- See Note [Free variables of types] +tyCoVarsOfTypesSet tys = tyCoVarsOfTypes $ nonDetEltsUFM tys + -- It's OK to use nonDetEltsUFM here because we immediately forget the + -- ordering by returning a set + +-- | Returns free variables of types, including kind variables as +-- a deterministic set. For type synonyms it does /not/ expand the +-- synonym. +tyCoVarsOfTypesDSet :: [Type] -> DTyCoVarSet +-- See Note [Free variables of types] +tyCoVarsOfTypesDSet tys = fvDVarSet $ tyCoFVsOfTypes tys + +-- | Returns free variables of types, including kind variables as +-- a deterministically ordered list. For type synonyms it does /not/ expand the +-- synonym. +tyCoVarsOfTypesList :: [Type] -> [TyCoVar] +-- See Note [Free variables of types] +tyCoVarsOfTypesList tys = fvVarList $ tyCoFVsOfTypes tys + -- | The worker for `tyCoFVsOfType` and `tyCoFVsOfTypeList`. -- The previous implementation used `unionVarSet` which is O(n+m) and can -- make the function quadratic. @@ -1566,45 +1796,11 @@ tyCoFVsBndr :: TyVarBinder -> FV -> FV tyCoFVsBndr (TvBndr tv _) fvs = (delFV tv fvs) `unionFV` tyCoFVsOfType (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 - --- | Returns free variables of types, including kind variables as --- a non-deterministic set. For type synonyms it does /not/ expand the --- synonym. -tyCoVarsOfTypesSet :: TyVarEnv Type -> TyCoVarSet --- See Note [Free variables of types] -tyCoVarsOfTypesSet tys = fvVarSet $ tyCoFVsOfTypes $ nonDetEltsUFM tys - -- It's OK to use nonDetEltsUFM here because we immediately forget the - -- ordering by returning a set - --- | Returns free variables of types, including kind variables as --- a deterministic set. For type synonyms it does /not/ expand the --- synonym. -tyCoVarsOfTypesDSet :: [Type] -> DTyCoVarSet --- See Note [Free variables of types] -tyCoVarsOfTypesDSet tys = fvDVarSet $ tyCoFVsOfTypes tys - --- | Returns free variables of types, including kind variables as --- a deterministically ordered list. For type synonyms it does /not/ expand the --- synonym. -tyCoVarsOfTypesList :: [Type] -> [TyCoVar] --- See Note [Free variables of types] -tyCoVarsOfTypesList tys = fvVarList $ tyCoFVsOfTypes tys - tyCoFVsOfTypes :: [Type] -> FV -- See Note [Free variables of types] 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] @@ -1618,6 +1814,11 @@ tyCoFVsOfMCo :: MCoercion -> FV tyCoFVsOfMCo MRefl = emptyFV tyCoFVsOfMCo (MCo co) = tyCoFVsOfCo co +tyCoVarsOfCosSet :: CoVarEnv Coercion -> TyCoVarSet +tyCoVarsOfCosSet cos = tyCoVarsOfCos $ nonDetEltsUFM cos + -- It's OK to use nonDetEltsUFM here because we immediately forget the + -- ordering by returning a set + tyCoFVsOfCo :: Coercion -> FV -- Extracts type and coercion variables from a coercion -- See Note [Free variables of types] @@ -1654,80 +1855,68 @@ tyCoFVsOfCoVar :: CoVar -> FV tyCoFVsOfCoVar v fv_cand in_scope acc = (unitFV v `unionFV` tyCoFVsOfType (varType v)) fv_cand in_scope acc -tyCoVarsOfProv :: UnivCoProvenance -> TyCoVarSet -tyCoVarsOfProv prov = fvVarSet $ tyCoFVsOfProv prov - tyCoFVsOfProv :: UnivCoProvenance -> FV tyCoFVsOfProv UnsafeCoerceProv fv_cand in_scope acc = emptyFV fv_cand in_scope acc tyCoFVsOfProv (PhantomProv co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc tyCoFVsOfProv (ProofIrrelProv co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc tyCoFVsOfProv (PluginProv _) fv_cand in_scope acc = emptyFV fv_cand in_scope acc -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 +------------- Extracting the CoVars of a type or coercion ----------- + +getCoVarSet :: FV -> CoVarSet +getCoVarSet fv = snd (fv isCoVar emptyVarSet ([], emptyVarSet)) + coVarsOfType :: Type -> CoVarSet -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 +coVarsOfType ty = getCoVarSet (tyCoFVsOfType ty) coVarsOfTypes :: [Type] -> TyCoVarSet -coVarsOfTypes tys = mapUnionVarSet coVarsOfType tys +coVarsOfTypes tys = getCoVarSet (tyCoFVsOfTypes tys) -coVarsOfMCo :: MCoercion -> CoVarSet -coVarsOfMCo MRefl = emptyVarSet -coVarsOfMCo (MCo co) = coVarsOfCo co +-- coVarsOfMCo :: MCoercion -> CoVarSet +-- coVarsOfMCo MRefl = emptyVarSet +-- coVarsOfMCo (MCo co) = coVarsOfCo co coVarsOfCo :: Coercion -> CoVarSet --- Extract *coercion* variables only. Tiresome to repeat the code, but easy. -coVarsOfCo (Refl ty) = coVarsOfType ty -coVarsOfCo (GRefl _ ty co) = coVarsOfType ty `unionVarSet` coVarsOfMCo co -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 (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 +coVarsOfCo co = getCoVarSet (tyCoFVsOfCo co) +-- -- Extract *coercion* variables only. Tiresome to repeat the code, but easy. +-- coVarsOfCo (Refl ty) = coVarsOfType ty +-- coVarsOfCo (GRefl _ ty co) = coVarsOfType ty `unionVarSet` coVarsOfMCo co +-- 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 (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 +coVarsOfCos cos = getCoVarSet (tyCoFVsOfCos cos) + +------------- Closing over kinds ----------------- -- | Add the kind variables free in the kinds of the tyvars in the given set. -- Returns a non-deterministic set. @@ -1753,6 +1942,8 @@ closeOverKindsList tvs = fvVarList $ closeOverKindsFV tvs closeOverKindsDSet :: DTyVarSet -> DTyVarSet closeOverKindsDSet = fvDVarSet . closeOverKindsFV . dVarSetElems +------------- Injective free vars ----------------- + -- | 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.) @@ -1788,6 +1979,8 @@ injectiveVarsOfType = go go (CastTy ty _) = go ty go CoercionTy{} = emptyFV +------------- No free vars ----------------- + -- | Returns True if this type has no free variables. Should be the same as -- isEmptyVarSet . tyCoVarsOfType, but faster in the non-forall case. noFreeVarsOfType :: Type -> Bool @@ -2131,12 +2324,6 @@ unionTCvSubst (TCvSubst in_scope1 tenv1 cenv1) (TCvSubst in_scope2 tenv2 cenv2) -- the types given; but it's just a thunk so with a bit of luck -- it'll never be evaluated --- | Generates an in-scope set from the free variables in a list of types --- and a list of coercions -mkTyCoInScopeSet :: [Type] -> [Coercion] -> InScopeSet -mkTyCoInScopeSet tys cos - = mkInScopeSet (tyCoVarsOfTypes tys `unionVarSet` tyCoVarsOfCos cos) - -- | Generates the in-scope set for the 'TCvSubst' from the types in the incoming -- environment. No CoVars, please! zipTvSubst :: [TyVar] -> [Type] -> TCvSubst |