diff options
author | Simon Peyton Jones <simonpj@microsoft.com> | 2019-12-19 00:04:15 +0000 |
---|---|---|
committer | Ben Gamari <ben@smart-cactus.org> | 2020-02-06 11:55:41 -0500 |
commit | ed2f0e5c38f1dfc9cf049ae63c56117cda99116e (patch) | |
tree | 09f89d7923ed378dbd7f664d8b3dd583ef5a0345 | |
parent | c4e6b35daef9336ea6b0922bab595cb02ac742b5 (diff) | |
download | haskell-ed2f0e5c38f1dfc9cf049ae63c56117cda99116e.tar.gz |
Reform the free variable finders for types
This patch delivers on (much of) #17509.
* Introduces the shallow vs deep free variable distinction
* Introduce TyCoRep.foldType,
foldType :: Monoid a => TyCoFolder env a
-> env -> Type -> a
and use it in the free variable finders.
* Substitution in TyCoSubst
* ASSERTs are on for checkValidSubst
* checkValidSubst uses shallowTyCoVarsOfTypes etc
Quite a few things still to do
* We could use foldType in lots of other places
* We could use mapType for substitution. (Check that we get
good code!)
* Some (but not yet all) clients of substitution can now
save time by using shallowTyCoVarsOfTypes
* All calls to tyCoVarsOfTypes should be inspected; most of
them should be shallow. Maybe.
* Currently shallowTyCoVarsOfTypes still returns
unification variables, but not CoVarHoles.
Reason: we need to return unification variables
in some of the calls in TcSimplify, eg when promoting.
* We should do the same thing for tyCoFVsOfTypes, which is
currently unchanged.
* tyCoFVsOfTypes returns CoVarHoles, because of the
use in TcSimplify.mkResidualConstraints. See
Note [Emitting the residual implication in simplifyInfer]
* #17509 talks about "relevant" variables too.
-rw-r--r-- | compiler/types/TyCoFVs.hs | 583 | ||||
-rw-r--r-- | compiler/types/TyCoRep.hs | 162 | ||||
-rw-r--r-- | compiler/types/TyCoSubst.hs | 30 | ||||
-rw-r--r-- | compiler/types/Type.hs | 7 |
4 files changed, 543 insertions, 239 deletions
diff --git a/compiler/types/TyCoFVs.hs b/compiler/types/TyCoFVs.hs index d4a0179f88..e1e3df94ed 100644 --- a/compiler/types/TyCoFVs.hs +++ b/compiler/types/TyCoFVs.hs @@ -1,24 +1,35 @@ +{-# LANGUAGE CPP #-} + module TyCoFVs - ( - tyCoVarsOfType, tyCoVarsOfTypeDSet, tyCoVarsOfTypes, tyCoVarsOfTypesDSet, - exactTyCoVarsOfType, exactTyCoVarsOfTypes, + ( shallowTyCoVarsOfType, shallowTyCoVarsOfTypes, + tyCoVarsOfType, tyCoVarsOfTypes, + tyCoVarsOfTypeDSet, tyCoVarsOfTypesDSet, + tyCoFVsBndr, tyCoFVsVarBndr, tyCoFVsVarBndrs, tyCoFVsOfType, tyCoVarsOfTypeList, tyCoFVsOfTypes, tyCoVarsOfTypesList, - tyCoVarsOfTypesSet, tyCoVarsOfCosSet, + + shallowTyCoVarsOfTyVarEnv, shallowTyCoVarsOfCoVarEnv, + + shallowTyCoVarsOfCo, shallowTyCoVarsOfCos, + tyCoVarsOfCo, tyCoVarsOfCos, coVarsOfType, coVarsOfTypes, coVarsOfCo, coVarsOfCos, - tyCoVarsOfCo, tyCoVarsOfCos, tyCoVarsOfCoDSet, tyCoFVsOfCo, tyCoFVsOfCos, - tyCoVarsOfCoList, tyCoVarsOfProv, + tyCoVarsOfCoList, + almostDevoidCoVarOfCo, + + -- Injective free vars injectiveVarsOfType, injectiveVarsOfTypes, invisibleVarsOfType, invisibleVarsOfTypes, - noFreeVarsOfType, noFreeVarsOfTypes, noFreeVarsOfCo, + -- Exact free vars + exactTyCoVarsOfType, exactTyCoVarsOfTypes, - mkTyCoInScopeSet, + -- No Free vars + noFreeVarsOfType, noFreeVarsOfTypes, noFreeVarsOfCo, -- * Well-scoped free variables scopedSort, tyCoVarsOfTypeWellScoped, @@ -30,17 +41,21 @@ module TyCoFVs ) where +#include "HsVersions.h" + import GhcPrelude -import {-# SOURCE #-} Type (coreView, tcView, partitionInvisibleTypes) +import {-# SOURCE #-} Type (coreView, tcView, partitionInvisibleTypes) +-- import Data.Monoid as DM ( Endo(..), All(..) ) +import Data.Monoid as DM ( Endo(..) ) import TyCoRep import TyCon import Var import FV import UniqFM -import UniqSet (nonDetEltsUniqSet) +import UniqSet( nonDetEltsUniqSet ) import VarSet import VarEnv import Util @@ -176,102 +191,233 @@ So if we're looking at a variable occurrence at all, then all variables in its kind are free. -} +{- ********************************************************************* +* * + Endo for free variables +* * +********************************************************************* -} + +{- Note [Acumulating parameter free variables] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We can use foldType to build an accumulating-parameter version of a +free-var finder, thus: + + fvs :: Type -> TyCoVarSet + fvs ty = appEndo (foldType folder ty) emptyVarSet + +Recall that + foldType :: TyCoFolder env a -> env -> Type -> a + + newtype Endo a = Endo (a -> a) -- In Data.Monoid + instance Monoid a => Monoid (Endo a) where + (Endo f) `mappend` (Endo g) = Endo (f.g) + + appEndo :: Endo a -> a -> a + appEndo (Endo f) x = f x + +So `mappend` for Endos is just function composition. + +It's very important that, after optimisation, we end up +with an arity-three function, something like this: + + fvs env (TyVarTy v) acc + | v `elemVarSet` env = acc + | v `elemVarSet` acc = acc + | otherwise = acc `extendVarSet` v + fvs env (AppTy t1 t2) = fvs env t1 (fvs env t2 acc) + ... + +The optimiser does do this, but not very robustly. It depends +critially on the basic arity-2 function not being exported, so that +all its calls are visibly to three arguments. This analysis is +done by the Call Arity pass. +-} + +runTyCoVars :: Endo TyCoVarSet -> TyCoVarSet +{-# INLINE runTyCoVars #-} +runTyCoVars f = appEndo f emptyVarSet + + +{- ********************************************************************* +* * + Deep free variables +* * +********************************************************************* -} + tyCoVarsOfType :: Type -> TyCoVarSet --- See Note [Free variables of types] -tyCoVarsOfType ty = ty_co_vars_of_type ty emptyVarSet emptyVarSet +tyCoVarsOfType ty = runTyCoVars (deep_ty ty) +-- Alternative: +-- tyCoVarsOfType ty = closeOverKinds (shallowTyCoVarsOfType ty) 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) - emptyVarSet -- See Note [Closing over free variable kinds] - (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 (Bndr tv _) ty) is acc = ty_co_vars_of_type (varType 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) +tyCoVarsOfTypes tys = runTyCoVars (deep_tys tys) +-- Alternative: +-- tyCoVarsOfTypes tys = closeOverKinds (shallowTyCoVarsOfTypes tys) tyCoVarsOfCo :: Coercion -> TyCoVarSet --- See Note [Free variables of types] -tyCoVarsOfCo co = ty_co_vars_of_co co emptyVarSet emptyVarSet +-- See Note [Free variables of Coercions] +tyCoVarsOfCo co = runTyCoVars (deep_co co) 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 mco) is acc = ty_co_vars_of_type ty is $ - ty_co_vars_of_mco mco 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` acc = acc - | otherwise = ty_co_vars_of_type (varType v) - emptyVarSet -- See Note [Closing over free variable kinds] - (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) +tyCoVarsOfCos cos = runTyCoVars (deep_cos cos) + +deep_ty :: Type -> Endo TyCoVarSet +deep_tys :: [Type] -> Endo TyCoVarSet +deep_co :: Coercion -> Endo TyCoVarSet +deep_cos :: [Coercion] -> Endo TyCoVarSet +(deep_ty, deep_tys, deep_co, deep_cos) = foldTyCo deepTcvFolder emptyVarSet + +deepTcvFolder :: TyCoFolder TyCoVarSet (Endo TyCoVarSet) +deepTcvFolder = TyCoFolder { tcf_tyvar = do_tcv, tcf_covar = do_tcv + , tcf_hole = do_hole, tcf_tycobinder = do_bndr } + where + do_tcv is v = Endo do_it + where + do_it acc | v `elemVarSet` is = acc + | v `elemVarSet` acc = acc + | otherwise = appEndo (deep_ty (varType v)) $ + acc `extendVarSet` v + + do_bndr is tcv _ = extendVarSet is tcv + do_hole is hole = do_tcv is (coHoleCoVar hole) + -- See Note [CoercionHoles and coercion free variables] + -- in TyCoRep + +{- ********************************************************************* +* * + Shallow free variables +* * +********************************************************************* -} + +shallowTyCoVarsOfType :: Type -> TyCoVarSet +-- See Note [Free variables of types] +shallowTyCoVarsOfType ty = runTyCoVars (shallow_ty ty) + +shallowTyCoVarsOfTypes :: [Type] -> TyCoVarSet +shallowTyCoVarsOfTypes tys = runTyCoVars (shallow_tys tys) + +shallowTyCoVarsOfCo :: Coercion -> TyCoVarSet +shallowTyCoVarsOfCo co = runTyCoVars (shallow_co co) + +shallowTyCoVarsOfCos :: [Coercion] -> TyCoVarSet +shallowTyCoVarsOfCos cos = runTyCoVars (shallow_cos cos) + +-- | Returns free variables of types, including kind variables as +-- a non-deterministic set. For type synonyms it does /not/ expand the +-- synonym. +shallowTyCoVarsOfTyVarEnv :: TyVarEnv Type -> TyCoVarSet +-- See Note [Free variables of types] +shallowTyCoVarsOfTyVarEnv tys = shallowTyCoVarsOfTypes (nonDetEltsUFM tys) + -- It's OK to use nonDetEltsUFM here because we immediately + -- forget the ordering by returning a set + +shallowTyCoVarsOfCoVarEnv :: CoVarEnv Coercion -> TyCoVarSet +shallowTyCoVarsOfCoVarEnv cos = shallowTyCoVarsOfCos (nonDetEltsUFM cos) + -- It's OK to use nonDetEltsUFM here because we immediately + -- forget the ordering by returning a set + +shallow_ty :: Type -> Endo TyCoVarSet +shallow_tys :: [Type] -> Endo TyCoVarSet +shallow_co :: Coercion -> Endo TyCoVarSet +shallow_cos :: [Coercion] -> Endo TyCoVarSet +(shallow_ty, shallow_tys, shallow_co, shallow_cos) = foldTyCo shallowTcvFolder emptyVarSet + +shallowTcvFolder :: TyCoFolder TyCoVarSet (Endo TyCoVarSet) +shallowTcvFolder = TyCoFolder { tcf_tyvar = do_tcv, tcf_covar = do_tcv + , tcf_hole = do_hole, tcf_tycobinder = do_bndr } + where + do_tcv 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 _ _ = mempty -- Ignore coercion holes + + +{- ********************************************************************* +* * + Closing over kinds +* * +********************************************************************* -} + +------------- Closing over kinds ----------------- + +closeOverKinds :: TyVarSet -> TyVarSet +closeOverKinds = fvVarSet . closeOverKindsFV . nonDetEltsUniqSet + +{- ---------------- Alternative version 1 (preferred) ------------- + +-- | Add the kind variables free in the kinds of the tyvars in the given set. +-- Returns a non-deterministic set. +closeOverKinds :: TyCoVarSet -> TyCoVarSet +closeOverKinds vs + = go vs vs + where + go :: VarSet -- Work list + -> VarSet -- Accumulator, always a superset of wl + -> VarSet + go wl acc + | isEmptyVarSet wl = acc + | otherwise = go wl_kvs (acc `unionVarSet` wl_kvs) + where + k v inner_acc = ty_co_vars_of_type (varType v) acc inner_acc + wl_kvs = nonDetFoldVarSet k emptyVarSet wl + -- wl_kvs = union of shallow free vars of the kinds of wl + -- but don't bother to collect vars in acc + +-} + +{- ---------------- Alternative version ------------- +-- | Add the kind variables free in the kinds of the tyvars in the given set. +-- Returns a non-deterministic set. +closeOverKinds :: TyVarSet -> TyVarSet +closeOverKinds vs = close_over_kinds vs emptyVarSet + + +close_over_kinds :: TyVarSet -- Work list + -> TyVarSet -- Accumulator + -> TyVarSet +-- Precondition: in any call (close_over_kinds wl acc) +-- for every tv in acc, the shallow kind-vars of tv +-- are either in the work list wl, or in acc +-- Postcondition: result is the deep free vars of (wl `union` acc) +close_over_kinds wl acc + = nonDetFoldVarSet do_one acc wl + where + do_one :: Var -> TyVarSet -> TyVarSet + -- (do_one v acc) adds v and its deep free-vars to acc + do_one v acc | v `elemVarSet` acc + = acc + | otherwise + = close_over_kinds (shallowTyCoVarsOfType (varType v)) $ + acc `extendVarSet` v +-} + + +{- ********************************************************************* +* * + The FV versions return deterministic results +* * +********************************************************************* -} + +-- | 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 +-- given tyvars. +closeOverKindsFV :: [TyVar] -> FV +closeOverKindsFV tvs = + mapUnionFV (tyCoFVsOfType . tyVarKind) tvs `unionFV` mkFVs tvs + +-- | Add the kind variables free in the kinds of the tyvars in the given set. +-- Returns a deterministically ordered list. +closeOverKindsList :: [TyVar] -> [TyVar] +closeOverKindsList tvs = fvVarList $ closeOverKindsFV tvs + +-- | Add the kind variables free in the kinds of the tyvars in the given set. +-- Returns a deterministic set. +closeOverKindsDSet :: DTyVarSet -> DTyVarSet +closeOverKindsDSet = fvDVarSet . closeOverKindsFV . dVarSetElems -- | `tyCoFVsOfType` that returns free variables of a type in a deterministic -- set. For explanation of why using `VarSet` is not deterministic see @@ -288,15 +434,6 @@ tyCoVarsOfTypeList :: Type -> [TyCoVar] 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 @@ -310,75 +447,6 @@ tyCoVarsOfTypesList :: [Type] -> [TyCoVar] -- See Note [Free variables of types] tyCoVarsOfTypesList tys = fvVarList $ tyCoFVsOfTypes tys -{- -************************************************************************ -* * - The "exact" free variables of a type -* * -************************************************************************ - -Note [Silly type synonym] -~~~~~~~~~~~~~~~~~~~~~~~~~ -Consider - type T a = Int -What are the free tyvars of (T x)? Empty, of course! - -exactTyCoVarsOfType is used by the type checker to figure out exactly -which type variables are mentioned in a type. It only matters -occasionally -- see the calls to exactTyCoVarsOfType. --} - -exactTyCoVarsOfType :: Type -> TyCoVarSet --- Find the free type variables (of any kind) --- but *expand* type synonyms. See Note [Silly type synonym] above. -exactTyCoVarsOfType ty - = go ty - where - go ty | Just ty' <- tcView ty = go ty' -- This is the key line - go (TyVarTy tv) = goVar tv - go (TyConApp _ tys) = exactTyCoVarsOfTypes tys - go (LitTy {}) = emptyVarSet - go (AppTy fun arg) = go fun `unionVarSet` go arg - go (FunTy _ arg res) = go arg `unionVarSet` go res - go (ForAllTy bndr ty) = delBinderVar (go ty) bndr `unionVarSet` go (binderType bndr) - go (CastTy ty co) = go ty `unionVarSet` goCo co - go (CoercionTy co) = goCo co - - goMCo MRefl = emptyVarSet - goMCo (MCo co) = goCo co - - goCo (Refl ty) = go ty - goCo (GRefl _ ty mco) = go ty `unionVarSet` goMCo mco - goCo (TyConAppCo _ _ args)= goCos args - goCo (AppCo co arg) = goCo co `unionVarSet` goCo arg - goCo (ForAllCo tv k_co co) - = goCo co `delVarSet` tv `unionVarSet` goCo k_co - goCo (FunCo _ co1 co2) = goCo co1 `unionVarSet` goCo co2 - goCo (CoVarCo v) = goVar v - goCo (HoleCo h) = goVar (coHoleCoVar h) - goCo (AxiomInstCo _ _ args) = goCos args - goCo (UnivCo p _ t1 t2) = goProv p `unionVarSet` go t1 `unionVarSet` go t2 - goCo (SymCo co) = goCo co - goCo (TransCo co1 co2) = goCo co1 `unionVarSet` goCo co2 - goCo (NthCo _ _ co) = goCo co - goCo (LRCo _ co) = goCo co - goCo (InstCo co arg) = goCo co `unionVarSet` goCo arg - goCo (KindCo co) = goCo co - goCo (SubCo co) = goCo co - goCo (AxiomRuleCo _ c) = goCos c - - goCos cos = foldr (unionVarSet . goCo) emptyVarSet cos - - goProv UnsafeCoerceProv = emptyVarSet - goProv (PhantomProv kco) = goCo kco - goProv (ProofIrrelProv kco) = goCo kco - goProv (PluginProv _) = emptyVarSet - - goVar v = unitVarSet v `unionVarSet` go (varType v) - -exactTyCoVarsOfTypes :: [Type] -> TyVarSet -exactTyCoVarsOfTypes tys = mapUnionVarSet exactTyCoVarsOfType tys - -- | The worker for `tyCoFVsOfType` and `tyCoFVsOfTypeList`. -- The previous implementation used `unionVarSet` which is O(n+m) and can -- make the function quadratic. @@ -435,11 +503,6 @@ 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] @@ -489,11 +552,8 @@ tyCoFVsOfCos (co:cos) fv_cand in_scope acc = (tyCoFVsOfCo co `unionFV` tyCoFVsOf ------------- Extracting the CoVars of a type or coercion ----------- -{- - -Note [CoVarsOfX and the InterestingVarFun] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - +{- Note [CoVarsOfX and the InterestingVarFun] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The coVarsOfType, coVarsOfTypes, coVarsOfCo, and coVarsOfCos functions are implemented in terms of the respective FV equivalents (tyCoFVsOf...), rather than the VarSet-based flavors (tyCoVarsOf...), despite the performance @@ -613,7 +673,82 @@ almost_devoid_co_var_of_types (ty:tys) cv = almost_devoid_co_var_of_type ty cv && almost_devoid_co_var_of_types tys cv -------------- Injective free vars ----------------- + + +{- ********************************************************************* +* * + The "exact" free variables of a type +* * +********************************************************************* -} + +{- Note [Silly type synonym] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider + type T a = Int +What are the free tyvars of (T x)? Empty, of course! + +exactTyCoVarsOfType is used by the type checker to figure out exactly +which type variables are mentioned in a type. It only matters +occasionally -- see the calls to exactTyCoVarsOfType. +-} + +exactTyCoVarsOfType :: Type -> TyCoVarSet +-- Find the free type variables (of any kind) +-- but *expand* type synonyms. See Note [Silly type synonym] above. +exactTyCoVarsOfType ty + = go ty + where + go ty | Just ty' <- tcView ty = go ty' -- This is the key line + go (TyVarTy tv) = goVar tv + go (TyConApp _ tys) = exactTyCoVarsOfTypes tys + go (LitTy {}) = emptyVarSet + go (AppTy fun arg) = go fun `unionVarSet` go arg + go (FunTy _ arg res) = go arg `unionVarSet` go res + go (ForAllTy bndr ty) = delBinderVar (go ty) bndr `unionVarSet` go (binderType bndr) + go (CastTy ty co) = go ty `unionVarSet` goCo co + go (CoercionTy co) = goCo co + + goMCo MRefl = emptyVarSet + goMCo (MCo co) = goCo co + + goCo (Refl ty) = go ty + goCo (GRefl _ ty mco) = go ty `unionVarSet` goMCo mco + goCo (TyConAppCo _ _ args)= goCos args + goCo (AppCo co arg) = goCo co `unionVarSet` goCo arg + goCo (ForAllCo tv k_co co) + = goCo co `delVarSet` tv `unionVarSet` goCo k_co + goCo (FunCo _ co1 co2) = goCo co1 `unionVarSet` goCo co2 + goCo (CoVarCo v) = goVar v + goCo (HoleCo h) = goVar (coHoleCoVar h) + goCo (AxiomInstCo _ _ args) = goCos args + goCo (UnivCo p _ t1 t2) = goProv p `unionVarSet` go t1 `unionVarSet` go t2 + goCo (SymCo co) = goCo co + goCo (TransCo co1 co2) = goCo co1 `unionVarSet` goCo co2 + goCo (NthCo _ _ co) = goCo co + goCo (LRCo _ co) = goCo co + goCo (InstCo co arg) = goCo co `unionVarSet` goCo arg + goCo (KindCo co) = goCo co + goCo (SubCo co) = goCo co + goCo (AxiomRuleCo _ c) = goCos c + + goCos cos = foldr (unionVarSet . goCo) emptyVarSet cos + + goProv UnsafeCoerceProv = emptyVarSet + goProv (PhantomProv kco) = goCo kco + goProv (ProofIrrelProv kco) = goCo kco + goProv (PluginProv _) = emptyVarSet + + goVar v = unitVarSet v `unionVarSet` go (varType v) + +exactTyCoVarsOfTypes :: [Type] -> TyVarSet +exactTyCoVarsOfTypes tys = mapUnionVarSet exactTyCoVarsOfType tys + + +{- ********************************************************************* +* * + Injective free vars +* * +********************************************************************* -} -- | Returns the free variables of a 'Type' that are in injective positions. -- Specifically, it finds the free variables while: @@ -681,7 +816,13 @@ injectiveVarsOfTypes :: Bool -- ^ look under injective type families? injectiveVarsOfTypes look_under_tfs = mapUnionFV (injectiveVarsOfType look_under_tfs) -------------- Invisible vars ----------------- +{- ********************************************************************* +* * + Invisible vars +* * +********************************************************************* -} + + -- | Returns the set of variables that are used invisibly anywhere within -- the given type. A variable will be included even if it is used both visibly -- and invisibly. An invisible use site includes: @@ -711,7 +852,31 @@ invisibleVarsOfTypes :: [Type] -> FV invisibleVarsOfTypes = mapUnionFV invisibleVarsOfType -------------- No free vars ----------------- +{- ********************************************************************* +* * + No free vars +* * +********************************************************************* -} + +{- Desired! + +nfvFolder :: TyCoFolder TyCoVarSet DM.All +nfvFolder = TyCoFolder { tcf_tyvar = do_tcv, tcf_covar = do_tcv + , tcf_hole = do_hole, tcf_tycobinder = do_bndr } + where + do_tcv is tv = All (tv `elemVarSet` is) + do_hole _ _ = All True -- I'm unsure; probably never happens + do_bndr is tv _ = is `extendVarSet` tv + +noFreeVarsOfType :: Type -> Bool +noFreeVarsOfType = DM.getAll . foldType nfvFolder emptyVarSet + +noFreeVarsOfTypes :: [Type] -> Bool +noFreeVarsOfTypes = DM.getAll . foldTypes nfvFolder emptyVarSet + +noFreeVarsOfCo :: Coercion -> Bool +noFreeVarsOfCo = getAll . foldCoercion nfvFolder emptyVarSet +-} -- | Returns True if this type has no free variables. Should be the same as -- isEmptyVarSet . tyCoVarsOfType, but faster in the non-forall case. @@ -764,15 +929,14 @@ noFreeVarsOfProv (PhantomProv co) = noFreeVarsOfCo co noFreeVarsOfProv (ProofIrrelProv co) = noFreeVarsOfCo co noFreeVarsOfProv (PluginProv {}) = True -{- -%************************************************************************ -%* * - Well-scoped tyvars +{- ********************************************************************* * * -************************************************************************ + scopedSort +* * +********************************************************************* -} -Note [ScopedSort] -~~~~~~~~~~~~~~~~~ +{- Note [ScopedSort] +~~~~~~~~~~~~~~~~~~~~ Consider foo :: Proxy a -> Proxy (b :: k) -> Proxy (a :: k2) -> () @@ -866,28 +1030,3 @@ tyCoVarsOfTypeWellScoped = scopedSort . tyCoVarsOfTypeList tyCoVarsOfTypesWellScoped :: [Type] -> [TyVar] tyCoVarsOfTypesWellScoped = scopedSort . tyCoVarsOfTypesList -------------- Closing over kinds ----------------- - --- | 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 . nonDetEltsUniqSet - -- It's OK to use nonDetEltsUniqSet here because we immediately forget - -- about the ordering by returning a set. - --- | 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 --- given tyvars. -closeOverKindsFV :: [TyVar] -> FV -closeOverKindsFV tvs = - mapUnionFV (tyCoFVsOfType . tyVarKind) tvs `unionFV` mkFVs tvs - --- | Add the kind variables free in the kinds of the tyvars in the given set. --- Returns a deterministically ordered list. -closeOverKindsList :: [TyVar] -> [TyVar] -closeOverKindsList tvs = fvVarList $ closeOverKindsFV tvs - --- | Add the kind variables free in the kinds of the tyvars in the given set. --- Returns a deterministic set. -closeOverKindsDSet :: DTyVarSet -> DTyVarSet -closeOverKindsDSet = fvDVarSet . closeOverKindsFV . dVarSetElems diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs index f55141d928..59ccc8f884 100644 --- a/compiler/types/TyCoRep.hs +++ b/compiler/types/TyCoRep.hs @@ -61,6 +61,9 @@ module TyCoRep ( -- * Functions over coercions pickLR, + -- ** Analyzing types + TyCoFolder(..), foldTyCo, + -- * Sizes typeSize, coercionSize, provSize ) where @@ -1635,6 +1638,165 @@ Here, {- ********************************************************************* * * + foldType and foldCoercion +* * +********************************************************************* -} + +{- Note [foldType] +~~~~~~~~~~~~~~~~~~ +foldType is a bit more powerful than perhaps it looks: + +* You can fold with an accumulating parameter, via + TyCoFolder env (Endo a) + Recall newtype Endo a = Endo (a->a) + +* You can fold monadically with a monad M, via + TyCoFolder env (M a) + provided you have + instance .. => Monoid (M a) + +Note [mapType vs foldType] +~~~~~~~~~~~~~~~~~~~~~~~~~~ +We define foldType here, but mapType in module Type. Why? + +* foldType is used in TyCoFVs for finding free variables. + It's a very simple function that analyses a type, + but does not construct one. + +* mapType constructs new types, and so it needs to call + the "smart constructors", mkAppTy, mkCastTy, and so on. + These are sophisticated functions, and can't be defined + here in TyCoRep. + +Note [Specialising foldType] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We inline foldType at every call site (there are not many), so that it +becomes specialised for the particular monoid *and* TyCoFolder at +that site. This is just for efficiency, but walking over types is +done a *lot* in GHC, so worth optimising. + +We were worried that + TyCoFolder env (Endo a) +might not eta-expand. Recall newtype Endo a = Endo (a->a). + +In particular, given + fvs :: Type -> TyCoVarSet + fvs ty = appEndo (foldType tcf emptyVarSet ty) emptyVarSet + + tcf :: TyCoFolder enf (Endo a) + tcf = TyCoFolder { tcf_tyvar = do_tv, ... } + where + do_tvs is tv = Endo do_it + where + do_it acc | tv `elemVarSet` is = acc + | tv `elemVarSet` acc = acc + | otherwise = acc `extendVarSet` tv + + +we want to end up with + fvs ty = go emptyVarSet ty emptyVarSet + where + go env (TyVarTy tv) acc = acc `extendVarSet` tv + ..etc.. + +And indeed this happens. + - Selections from 'tcf' are done at compile time + - 'go' is nicely eta-expanded. + +We were also worried about + deep_fvs :: Type -> TyCoVarSet + deep_fvs ty = appEndo (foldType deep_tcf emptyVarSet ty) emptyVarSet + + deep_tcf :: TyCoFolder enf (Endo a) + deep_tcf = TyCoFolder { tcf_tyvar = do_tv, ... } + where + do_tvs is tv = Endo do_it + where + do_it acc | tv `elemVarSet` is = acc + | tv `elemVarSet` acc = acc + | otherwise = deep_fvs (varType tv) + `unionVarSet` acc + `extendVarSet` tv + +Here deep_fvs and deep_tcf are mutually recursive, unlike fvs and tcf. +But, amazingly, we get good code here too. GHC is careful not to makr +TyCoFolder data constructor for deep_tcf as a loop breaker, so the +record selections still cancel. And eta expansion still happens too. +-} + +data TyCoFolder env a + = TyCoFolder + { tcf_tyvar :: env -> TyVar -> a + , tcf_covar :: env -> CoVar -> a + , tcf_hole :: env -> CoercionHole -> a + -- ^ What to do with coercion holes. + -- See Note [Coercion holes] in TyCoRep. + + , tcf_tycobinder :: env -> TyCoVar -> ArgFlag -> env + -- ^ The returned env is used in the extended scope + } + +{-# INLINE foldTyCo #-} -- See Note [Specialising foldType] +foldTyCo :: Monoid a => TyCoFolder env a -> env + -> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a) +foldTyCo (TyCoFolder { tcf_tyvar = tyvar + , tcf_tycobinder = tycobinder + , tcf_covar = covar + , tcf_hole = cohole }) env + = (go_ty env, go_tys env, go_co env, go_cos env) + where + go_ty env (TyVarTy tv) = tyvar env tv + go_ty env (AppTy t1 t2) = go_ty env t1 `mappend` go_ty env t2 + go_ty _ (LitTy {}) = mempty + go_ty env (CastTy ty co) = go_ty env ty `mappend` go_co env co + go_ty env (CoercionTy co) = go_co env co + go_ty env (FunTy _ arg res) = go_ty env arg `mappend` go_ty env res + go_ty env (TyConApp _ tys) = go_tys env tys + go_ty env (ForAllTy (Bndr tv vis) inner) + = let env' = tycobinder env tv vis + in go_ty env (varType tv) `mappend` go_ty env' inner + + -- Explicit recursion becuase using foldr builds a local + -- loop (with env free) and I'm not confident it'll be + -- lambda lifted in the end + go_tys _ [] = mempty + go_tys env (t:ts) = go_ty env t `mappend` go_tys env ts + + go_cos _ [] = mempty + go_cos env (c:cs) = go_co env c `mappend` go_cos env cs + + go_co env (Refl ty) = go_ty env ty + go_co env (GRefl _ ty MRefl) = go_ty env ty + go_co env (GRefl _ ty (MCo co)) = go_ty env ty `mappend` go_co env co + go_co env (TyConAppCo _ _ args) = go_cos env args + go_co env (AppCo c1 c2) = go_co env c1 `mappend` go_co env c2 + go_co env (FunCo _ c1 c2) = go_co env c1 `mappend` go_co env c2 + go_co env (CoVarCo cv) = covar env cv + go_co env (AxiomInstCo _ _ args) = go_cos env args + go_co env (HoleCo hole) = cohole env hole + go_co env (UnivCo p _ t1 t2) = go_prov env p `mappend` go_ty env t1 + `mappend` go_ty env t2 + go_co env (SymCo co) = go_co env co + go_co env (TransCo c1 c2) = go_co env c1 `mappend` go_co env c2 + go_co env (AxiomRuleCo _ cos) = go_cos env cos + go_co env (NthCo _ _ co) = go_co env co + go_co env (LRCo _ co) = go_co env co + 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 (ForAllCo tv kind_co co) + = go_co env kind_co `mappend` go_ty env (varType tv) + `mappend` go_co env' co + where + env' = tycobinder env tv Inferred + + go_prov env (PhantomProv co) = go_co env co + go_prov env (ProofIrrelProv co) = go_co env co + go_prov _ UnsafeCoerceProv = mempty + go_prov _ (PluginProv _) = mempty + +{- ********************************************************************* +* * typeSize, coercionSize * * ********************************************************************* -} diff --git a/compiler/types/TyCoSubst.hs b/compiler/types/TyCoSubst.hs index 27e2ab9f77..0d676ed5fa 100644 --- a/compiler/types/TyCoSubst.hs +++ b/compiler/types/TyCoSubst.hs @@ -26,7 +26,7 @@ module TyCoSubst extendTvSubst, extendTvSubstBinderAndInScope, extendTvSubstWithClone, extendTvSubstList, extendTvSubstAndInScope, extendTCvSubstList, - unionTCvSubst, zipTyEnv, zipCoEnv, mkTyCoInScopeSet, + unionTCvSubst, zipTyEnv, zipCoEnv, zipTvSubst, zipCvSubst, zipTCvSubst, mkTvSubstPrs, @@ -283,8 +283,8 @@ getTCvSubstRangeFVs :: TCvSubst -> VarSet getTCvSubstRangeFVs (TCvSubst _ tenv cenv) = unionVarSet tenvFVs cenvFVs where - tenvFVs = tyCoVarsOfTypesSet tenv - cenvFVs = tyCoVarsOfCosSet cenv + tenvFVs = shallowTyCoVarsOfTyVarEnv tenv + cenvFVs = shallowTyCoVarsOfCoVarEnv cenv isInScope :: Var -> TCvSubst -> Bool isInScope v (TCvSubst in_scope _ _) = v `elemInScopeSet` in_scope @@ -395,7 +395,7 @@ unionTCvSubst (TCvSubst in_scope1 tenv1 cenv1) (TCvSubst in_scope2 tenv2 cenv2) -- environment. No CoVars, please! zipTvSubst :: HasDebugCallStack => [TyVar] -> [Type] -> TCvSubst zipTvSubst tvs tys - = mkTvSubst (mkInScopeSet (tyCoVarsOfTypes tys)) tenv + = mkTvSubst (mkInScopeSet (shallowTyCoVarsOfTypes tys)) tenv where tenv = zipTyEnv tvs tys @@ -403,13 +403,14 @@ zipTvSubst tvs tys -- environment. No TyVars, please! zipCvSubst :: HasDebugCallStack => [CoVar] -> [Coercion] -> TCvSubst zipCvSubst cvs cos - = TCvSubst (mkInScopeSet (tyCoVarsOfCos cos)) emptyTvSubstEnv cenv + = TCvSubst (mkInScopeSet (shallowTyCoVarsOfCos cos)) emptyTvSubstEnv cenv where cenv = zipCoEnv cvs cos zipTCvSubst :: HasDebugCallStack => [TyCoVar] -> [Type] -> TCvSubst zipTCvSubst tcvs tys - = zip_tcvsubst tcvs tys (mkEmptyTCvSubst $ mkInScopeSet (tyCoVarsOfTypes tys)) + = zip_tcvsubst tcvs tys $ + mkEmptyTCvSubst $ mkInScopeSet $ shallowTyCoVarsOfTypes tys where zip_tcvsubst :: [TyCoVar] -> [Type] -> TCvSubst -> TCvSubst zip_tcvsubst (tv:tvs) (ty:tys) subst = zip_tcvsubst tvs tys (extendTCvSubst subst tv ty) @@ -424,7 +425,7 @@ mkTvSubstPrs prs = ASSERT2( onlyTyVarsAndNoCoercionTy, text "prs" <+> ppr prs ) mkTvSubst in_scope tenv where tenv = mkVarEnv prs - in_scope = mkInScopeSet $ tyCoVarsOfTypes $ map snd prs + in_scope = mkInScopeSet $ shallowTyCoVarsOfTypes $ map snd prs onlyTyVarsAndNoCoercionTy = and [ isTyVar tv && not (isCoercionTy ty) | (tv, ty) <- prs ] @@ -618,8 +619,8 @@ isValidTCvSubst (TCvSubst in_scope tenv cenv) = (tenvFVs `varSetInScope` in_scope) && (cenvFVs `varSetInScope` in_scope) where - tenvFVs = tyCoVarsOfTypesSet tenv - cenvFVs = tyCoVarsOfCosSet cenv + tenvFVs = shallowTyCoVarsOfTyVarEnv tenv + cenvFVs = shallowTyCoVarsOfCoVarEnv cenv -- | This checks if the substitution satisfies the invariant from -- Note [The substitution invariant]. @@ -628,9 +629,9 @@ checkValidSubst subst@(TCvSubst in_scope tenv cenv) tys cos a = ASSERT2( isValidTCvSubst subst, text "in_scope" <+> ppr in_scope $$ text "tenv" <+> ppr tenv $$ - text "tenvFVs" <+> ppr (tyCoVarsOfTypesSet tenv) $$ + text "tenvFVs" <+> ppr (shallowTyCoVarsOfTyVarEnv tenv) $$ text "cenv" <+> ppr cenv $$ - text "cenvFVs" <+> ppr (tyCoVarsOfCosSet cenv) $$ + text "cenvFVs" <+> ppr (shallowTyCoVarsOfCoVarEnv cenv) $$ text "tys" <+> ppr tys $$ text "cos" <+> ppr cos ) ASSERT2( tysCosFVsInScope, @@ -645,8 +646,9 @@ checkValidSubst subst@(TCvSubst in_scope tenv cenv) tys cos a substDomain = nonDetKeysUFM tenv ++ nonDetKeysUFM cenv -- It's OK to use nonDetKeysUFM here, because we only use this list to -- remove some elements from a set - needInScope = (tyCoVarsOfTypes tys `unionVarSet` tyCoVarsOfCos cos) - `delListFromUniqSet_Directly` substDomain + needInScope = (shallowTyCoVarsOfTypes tys `unionVarSet` + shallowTyCoVarsOfCos cos) + `delListFromUniqSet_Directly` substDomain tysCosFVsInScope = needInScope `varSetInScope` in_scope @@ -958,7 +960,7 @@ substTyVarBndrUsing subst_fn subst@(TCvSubst in_scope tenv cenv) old_var new_env | no_change = delVarEnv tenv old_var | otherwise = extendVarEnv tenv old_var (TyVarTy new_var) - _no_capture = not (new_var `elemVarSet` tyCoVarsOfTypesSet tenv) + _no_capture = not (new_var `elemVarSet` shallowTyCoVarsOfTyVarEnv tenv) -- Assertion check that we are not capturing something in the substitution old_ki = tyVarKind old_var diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs index e5859b2f4b..3d2b90c2ed 100644 --- a/compiler/types/Type.hs +++ b/compiler/types/Type.hs @@ -82,6 +82,7 @@ module Type ( -- ** Analyzing types TyCoMapper(..), mapType, mapCoercion, + TyCoFolder(..), foldTyCo, -- (Newtypes) newTyConInstRhs, @@ -552,10 +553,9 @@ isRuntimeRepVar :: TyVar -> Bool isRuntimeRepVar = isRuntimeRepTy . tyVarKind -{- -************************************************************************ +{- ********************************************************************* * * - Analyzing types + mapType * * ************************************************************************ @@ -696,6 +696,7 @@ mapCoercion mapper@(TyCoMapper { tcm_covar = covar go_prov (ProofIrrelProv co) = ProofIrrelProv <$> go co go_prov p@(PluginProv _) = return p + {- ************************************************************************ * * |