diff options
Diffstat (limited to 'compiler/GHC/Core/TyCo/FVs.hs')
| -rw-r--r-- | compiler/GHC/Core/TyCo/FVs.hs | 341 |
1 files changed, 332 insertions, 9 deletions
diff --git a/compiler/GHC/Core/TyCo/FVs.hs b/compiler/GHC/Core/TyCo/FVs.hs index 366f3b8efe..3685876fa4 100644 --- a/compiler/GHC/Core/TyCo/FVs.hs +++ b/compiler/GHC/Core/TyCo/FVs.hs @@ -30,6 +30,15 @@ module GHC.Core.TyCo.FVs anyFreeVarsOfType, anyFreeVarsOfTypes, anyFreeVarsOfCo, noFreeVarsOfType, noFreeVarsOfTypes, noFreeVarsOfCo, + -- * Free type constructors + tyConsOfType, + + -- * Free vars with visible/invisible separate + visVarsOfTypes, visVarsOfType, + + -- * Occurrence-check expansion + occCheckExpand, + -- * Well-scoped free variables scopedSort, tyCoVarsOfTypeWellScoped, tyCoVarsOfTypesWellScoped, @@ -44,19 +53,26 @@ module GHC.Core.TyCo.FVs import GHC.Prelude -import {-# SOURCE #-} GHC.Core.Type (coreView, partitionInvisibleTypes) +import {-# SOURCE #-} GHC.Core.Type( partitionInvisibleTypes, coreView ) +import {-# SOURCE #-} GHC.Core.Coercion( coercionLKind ) + +import GHC.Builtin.Types.Prim( funTyFlagTyCon ) import Data.Monoid as DM ( Endo(..), Any(..) ) import GHC.Core.TyCo.Rep import GHC.Core.TyCon -import GHC.Types.Var +import GHC.Core.Coercion.Axiom( coAxiomTyCon ) import GHC.Utils.FV +import GHC.Types.Var import GHC.Types.Unique.FM +import GHC.Types.Unique.Set + import GHC.Types.Var.Set import GHC.Types.Var.Env import GHC.Utils.Misc import GHC.Utils.Panic +import GHC.Data.Pair {- %************************************************************************ @@ -575,7 +591,7 @@ tyCoFVsOfType (ForAllTy bndr ty) f bound_vars acc = tyCoFVsBndr bndr (tyCoFVsOfT tyCoFVsOfType (CastTy ty co) f bound_vars acc = (tyCoFVsOfType ty `unionFV` tyCoFVsOfCo co) f bound_vars acc tyCoFVsOfType (CoercionTy co) f bound_vars acc = tyCoFVsOfCo co f bound_vars acc -tyCoFVsBndr :: TyCoVarBinder -> FV -> FV +tyCoFVsBndr :: ForAllTyBinder -> FV -> FV -- Free vars of (forall b. <thing with fvs>) tyCoFVsBndr (Bndr tv _) fvs = tyCoFVsVarBndr tv fvs @@ -617,7 +633,7 @@ tyCoFVsOfCo (AppCo co arg) fv_cand in_scope acc = (tyCoFVsOfCo co `unionFV` tyCoFVsOfCo arg) fv_cand in_scope acc tyCoFVsOfCo (ForAllCo tv kind_co co) fv_cand in_scope acc = (tyCoFVsVarBndr tv (tyCoFVsOfCo co) `unionFV` tyCoFVsOfCo kind_co) fv_cand in_scope acc -tyCoFVsOfCo (FunCo _ w co1 co2) fv_cand in_scope acc +tyCoFVsOfCo (FunCo { fco_mult = w, fco_arg = co1, fco_res = co2 }) fv_cand in_scope acc = (tyCoFVsOfCo co1 `unionFV` tyCoFVsOfCo co2 `unionFV` tyCoFVsOfCo w) fv_cand in_scope acc tyCoFVsOfCo (CoVarCo v) fv_cand in_scope acc = tyCoFVsOfCoVar v fv_cand in_scope acc @@ -630,7 +646,7 @@ tyCoFVsOfCo (UnivCo p _ t1 t2) fv_cand in_scope acc `unionFV` tyCoFVsOfType t2) fv_cand in_scope acc tyCoFVsOfCo (SymCo co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc tyCoFVsOfCo (TransCo co1 co2) fv_cand in_scope acc = (tyCoFVsOfCo co1 `unionFV` tyCoFVsOfCo co2) fv_cand in_scope acc -tyCoFVsOfCo (NthCo _ _ co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc +tyCoFVsOfCo (SelCo _ co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc tyCoFVsOfCo (LRCo _ co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc tyCoFVsOfCo (InstCo co arg) fv_cand in_scope acc = (tyCoFVsOfCo co `unionFV` tyCoFVsOfCo arg) fv_cand in_scope acc tyCoFVsOfCo (KindCo co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc @@ -673,8 +689,8 @@ almost_devoid_co_var_of_co (AppCo co arg) cv almost_devoid_co_var_of_co (ForAllCo v kind_co co) cv = almost_devoid_co_var_of_co kind_co cv && (v == cv || almost_devoid_co_var_of_co co cv) -almost_devoid_co_var_of_co (FunCo _ w co1 co2) cv - = almost_devoid_co_var_of_co w cv +almost_devoid_co_var_of_co (FunCo { fco_mult = w, fco_arg = co1, fco_res = co2 }) cv + = almost_devoid_co_var_of_co w cv && almost_devoid_co_var_of_co co1 cv && almost_devoid_co_var_of_co co2 cv almost_devoid_co_var_of_co (CoVarCo v) cv = v /= cv @@ -690,7 +706,7 @@ almost_devoid_co_var_of_co (SymCo co) cv almost_devoid_co_var_of_co (TransCo co1 co2) cv = almost_devoid_co_var_of_co co1 cv && almost_devoid_co_var_of_co co2 cv -almost_devoid_co_var_of_co (NthCo _ _ co) cv +almost_devoid_co_var_of_co (SelCo _ co) cv = almost_devoid_co_var_of_co co cv almost_devoid_co_var_of_co (LRCo _ co) cv = almost_devoid_co_var_of_co co cv @@ -747,6 +763,43 @@ almost_devoid_co_var_of_types (ty:tys) cv +{- +%************************************************************************ +%* * + Free tyvars, but with visible/invisible info +%* * +%************************************************************************ + +-} +-- | Retrieve the free variables in this type, splitting them based +-- on whether they are used visibly or invisibly. Invisible ones come +-- first. +visVarsOfType :: Type -> Pair TyCoVarSet +visVarsOfType orig_ty = Pair invis_vars vis_vars + where + Pair invis_vars1 vis_vars = go orig_ty + invis_vars = invis_vars1 `minusVarSet` vis_vars + + go (TyVarTy tv) = Pair (tyCoVarsOfType $ tyVarKind tv) (unitVarSet tv) + go (AppTy t1 t2) = go t1 `mappend` go t2 + go (TyConApp tc tys) = go_tc tc tys + go (FunTy _ w t1 t2) = go w `mappend` go t1 `mappend` go t2 + go (ForAllTy (Bndr tv _) ty) + = ((`delVarSet` tv) <$> go ty) `mappend` + (invisible (tyCoVarsOfType $ varType tv)) + go (LitTy {}) = mempty + go (CastTy ty co) = go ty `mappend` invisible (tyCoVarsOfCo co) + go (CoercionTy co) = invisible $ tyCoVarsOfCo co + + invisible vs = Pair vs emptyVarSet + + go_tc tc tys = let (invis, vis) = partitionInvisibleTypes tc tys in + invisible (tyCoVarsOfTypes invis) `mappend` foldMap go vis + +visVarsOfTypes :: [Type] -> Pair TyCoVarSet +visVarsOfTypes = foldMap visVarsOfType + + {- ********************************************************************* * * Injective free vars @@ -833,7 +886,7 @@ injectiveVarsOfTypes look_under_tfs = mapUnionFV (injectiveVarsOfType look_under -- * In the kind of a bound variable in a forall -- * In a coercion -- * In a Specified or Inferred argument to a function --- See Note [VarBndrs, TyCoVarBinders, TyConBinders, and visibility] in "GHC.Core.TyCo.Rep" +-- See Note [VarBndrs, ForAllTyBinders, TyConBinders, and visibility] in "GHC.Core.TyCo.Rep" invisibleVarsOfType :: Type -> FV invisibleVarsOfType = go where @@ -996,3 +1049,273 @@ tyCoVarsOfTypeWellScoped = scopedSort . tyCoVarsOfTypeList -- | Get the free vars of types in scoped order tyCoVarsOfTypesWellScoped :: [Type] -> [TyVar] tyCoVarsOfTypesWellScoped = scopedSort . tyCoVarsOfTypesList + +{- +************************************************************************ +* * + Free type constructors +* * +************************************************************************ +-} + +-- | All type constructors occurring in the type; looking through type +-- synonyms, but not newtypes. +-- When it finds a Class, it returns the class TyCon. +tyConsOfType :: Type -> UniqSet TyCon +tyConsOfType ty + = go ty + where + go :: Type -> UniqSet TyCon -- The UniqSet does duplicate elim + go ty | Just ty' <- coreView ty = go ty' + go (TyVarTy {}) = emptyUniqSet + go (LitTy {}) = emptyUniqSet + go (TyConApp tc tys) = go_tc tc `unionUniqSets` go_s tys + go (AppTy a b) = go a `unionUniqSets` go b + go (FunTy af w a b) = go w `unionUniqSets` + go a `unionUniqSets` go b + `unionUniqSets` go_tc (funTyFlagTyCon af) + go (ForAllTy (Bndr tv _) ty) = go ty `unionUniqSets` go (varType tv) + go (CastTy ty co) = go ty `unionUniqSets` go_co co + go (CoercionTy co) = go_co co + + go_co (Refl ty) = go ty + go_co (GRefl _ ty mco) = go ty `unionUniqSets` go_mco mco + go_co (TyConAppCo _ tc args) = go_tc tc `unionUniqSets` go_cos args + go_co (AppCo co arg) = go_co co `unionUniqSets` go_co arg + go_co (ForAllCo _ kind_co co) = go_co kind_co `unionUniqSets` go_co co + go_co (FunCo { fco_mult = m, fco_arg = a, fco_res = r }) + = go_co m `unionUniqSets` go_co a `unionUniqSets` go_co r + go_co (AxiomInstCo ax _ args) = go_ax ax `unionUniqSets` go_cos args + go_co (UnivCo p _ t1 t2) = go_prov p `unionUniqSets` go t1 `unionUniqSets` go t2 + go_co (CoVarCo {}) = emptyUniqSet + go_co (HoleCo {}) = emptyUniqSet + go_co (SymCo co) = go_co co + go_co (TransCo co1 co2) = go_co co1 `unionUniqSets` go_co co2 + go_co (SelCo _ co) = go_co co + go_co (LRCo _ co) = go_co co + go_co (InstCo co arg) = go_co co `unionUniqSets` go_co arg + go_co (KindCo co) = go_co co + go_co (SubCo co) = go_co co + go_co (AxiomRuleCo _ cs) = go_cos cs + + go_mco MRefl = emptyUniqSet + go_mco (MCo co) = go_co co + + go_prov (PhantomProv co) = go_co co + go_prov (ProofIrrelProv co) = go_co co + go_prov (PluginProv _) = emptyUniqSet + go_prov (CorePrepProv _) = emptyUniqSet + -- this last case can happen from the tyConsOfType used from + -- checkTauTvUpdate + + go_s tys = foldr (unionUniqSets . go) emptyUniqSet tys + go_cos cos = foldr (unionUniqSets . go_co) emptyUniqSet cos + + go_tc tc = unitUniqSet tc + go_ax ax = go_tc $ coAxiomTyCon ax + + +{- ********************************************************************** +* * + Occurs check expansion +%* * +%********************************************************************* -} + +{- Note [Occurs check expansion] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +(occurCheckExpand tv xi) expands synonyms in xi just enough to get rid +of occurrences of tv outside type function arguments, if that is +possible; otherwise, it returns Nothing. + +For example, suppose we have + type F a b = [a] +Then + occCheckExpand b (F Int b) = Just [Int] +but + occCheckExpand a (F a Int) = Nothing + +We don't promise to do the absolute minimum amount of expanding +necessary, but we try not to do expansions we don't need to. We +prefer doing inner expansions first. For example, + type F a b = (a, Int, a, [a]) + type G b = Char +We have + occCheckExpand b (F (G b)) = Just (F Char) +even though we could also expand F to get rid of b. + +Note [Occurrence checking: look inside kinds] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Suppose we are considering unifying + (alpha :: *) ~ Int -> (beta :: alpha -> alpha) +This may be an error (what is that alpha doing inside beta's kind?), +but we must not make the mistake of actually unifying or we'll +build an infinite data structure. So when looking for occurrences +of alpha in the rhs, we must look in the kinds of type variables +that occur there. + +occCheckExpand tries to expand type synonyms to remove +unnecessary occurrences of a variable, and thereby get past an +occurs-check failure. This is good; but + we can't do it in the /kind/ of a variable /occurrence/ + +For example #18451 built an infinite type: + type Const a b = a + data SameKind :: k -> k -> Type + type T (k :: Const Type a) = forall (b :: k). SameKind a b + +We have + b :: k + k :: Const Type a + a :: k (must be same as b) + +So if we aren't careful, a's kind mentions a, which is bad. +And expanding an /occurrence/ of 'a' doesn't help, because the +/binding site/ is the master copy and all the occurrences should +match it. + +Here's a related example: + f :: forall a b (c :: Const Type b). Proxy '[a, c] + +The list means that 'a' gets the same kind as 'c'; but that +kind mentions 'b', so the binders are out of order. + +Bottom line: in occCheckExpand, do not expand inside the kinds +of occurrences. See bad_var_occ in occCheckExpand. And +see #18451 for more debate. +-} + +occCheckExpand :: [Var] -> Type -> Maybe Type +-- See Note [Occurs check expansion] +-- We may have needed to do some type synonym unfolding in order to +-- get rid of the variable (or forall), so we also return the unfolded +-- version of the type, which is guaranteed to be syntactically free +-- of the given type variable. If the type is already syntactically +-- free of the variable, then the same type is returned. +occCheckExpand vs_to_avoid ty + | null vs_to_avoid -- Efficient shortcut + = Just ty -- Can happen, eg. GHC.Core.Utils.mkSingleAltCase + + | otherwise + = go (mkVarSet vs_to_avoid, emptyVarEnv) ty + where + go :: (VarSet, VarEnv TyCoVar) -> Type -> Maybe Type + -- The VarSet is the set of variables we are trying to avoid + -- The VarEnv carries mappings necessary + -- because of kind expansion + go (as, env) ty@(TyVarTy tv) + | Just tv' <- lookupVarEnv env tv = return (mkTyVarTy tv') + | bad_var_occ as tv = Nothing + | otherwise = return ty + + go _ ty@(LitTy {}) = return ty + go cxt (AppTy ty1 ty2) = do { ty1' <- go cxt ty1 + ; ty2' <- go cxt ty2 + ; return (AppTy ty1' ty2') } + go cxt ty@(FunTy _ w ty1 ty2) + = do { w' <- go cxt w + ; ty1' <- go cxt ty1 + ; ty2' <- go cxt ty2 + ; return (ty { ft_mult = w', ft_arg = ty1', ft_res = ty2' }) } + go cxt@(as, env) (ForAllTy (Bndr tv vis) body_ty) + = do { ki' <- go cxt (varType tv) + ; let tv' = setVarType tv ki' + env' = extendVarEnv env tv tv' + as' = as `delVarSet` tv + ; body' <- go (as', env') body_ty + ; return (ForAllTy (Bndr tv' vis) body') } + + -- For a type constructor application, first try expanding away the + -- offending variable from the arguments. If that doesn't work, next + -- see if the type constructor is a type synonym, and if so, expand + -- it and try again. + go cxt ty@(TyConApp tc tys) + = case mapM (go cxt) tys of + Just tys' -> return (TyConApp tc tys') + Nothing | Just ty' <- coreView ty -> go cxt ty' + | otherwise -> Nothing + -- Failing that, try to expand a synonym + + go cxt (CastTy ty co) = do { ty' <- go cxt ty + ; co' <- go_co cxt co + ; return (CastTy ty' co') } + go cxt (CoercionTy co) = do { co' <- go_co cxt co + ; return (CoercionTy co') } + + ------------------ + bad_var_occ :: VarSet -> Var -> Bool + -- Works for TyVar and CoVar + -- See Note [Occurrence checking: look inside kinds] + bad_var_occ vs_to_avoid v + = v `elemVarSet` vs_to_avoid + || tyCoVarsOfType (varType v) `intersectsVarSet` vs_to_avoid + + ------------------ + go_mco _ MRefl = return MRefl + go_mco ctx (MCo co) = MCo <$> go_co ctx co + + ------------------ + go_co cxt (Refl ty) = do { ty' <- go cxt ty + ; return (Refl ty') } + go_co cxt (GRefl r ty mco) = do { mco' <- go_mco cxt mco + ; ty' <- go cxt ty + ; return (GRefl r ty' mco') } + -- Note: Coercions do not contain type synonyms + go_co cxt (TyConAppCo r tc args) = do { args' <- mapM (go_co cxt) args + ; return (TyConAppCo r tc args') } + go_co cxt (AppCo co arg) = do { co' <- go_co cxt co + ; arg' <- go_co cxt arg + ; return (AppCo co' arg') } + go_co cxt@(as, env) (ForAllCo tv kind_co body_co) + = do { kind_co' <- go_co cxt kind_co + ; let tv' = setVarType tv $ + coercionLKind kind_co' + env' = extendVarEnv env tv tv' + as' = as `delVarSet` tv + ; body' <- go_co (as', env') body_co + ; return (ForAllCo tv' kind_co' body') } + go_co cxt co@(FunCo { fco_mult = w, fco_arg = co1 ,fco_res = co2 }) + = do { co1' <- go_co cxt co1 + ; co2' <- go_co cxt co2 + ; w' <- go_co cxt w + ; return (co { fco_mult = w', fco_arg = co1', fco_res = co2' })} + + go_co (as,env) co@(CoVarCo c) + | Just c' <- lookupVarEnv env c = return (CoVarCo c') + | bad_var_occ as c = Nothing + | otherwise = return co + + go_co (as,_) co@(HoleCo h) + | bad_var_occ as (ch_co_var h) = Nothing + | otherwise = return co + + go_co cxt (AxiomInstCo ax ind args) = do { args' <- mapM (go_co cxt) args + ; return (AxiomInstCo ax ind args') } + go_co cxt (UnivCo p r ty1 ty2) = do { p' <- go_prov cxt p + ; ty1' <- go cxt ty1 + ; ty2' <- go cxt ty2 + ; return (UnivCo p' r ty1' ty2') } + go_co cxt (SymCo co) = do { co' <- go_co cxt co + ; return (SymCo co') } + go_co cxt (TransCo co1 co2) = do { co1' <- go_co cxt co1 + ; co2' <- go_co cxt co2 + ; return (TransCo co1' co2') } + go_co cxt (SelCo n co) = do { co' <- go_co cxt co + ; return (SelCo n co') } + go_co cxt (LRCo lr co) = do { co' <- go_co cxt co + ; return (LRCo lr co') } + go_co cxt (InstCo co arg) = do { co' <- go_co cxt co + ; arg' <- go_co cxt arg + ; return (InstCo co' arg') } + go_co cxt (KindCo co) = do { co' <- go_co cxt co + ; return (KindCo co') } + go_co cxt (SubCo co) = do { co' <- go_co cxt co + ; return (SubCo co') } + go_co cxt (AxiomRuleCo ax cs) = do { cs' <- mapM (go_co cxt) cs + ; return (AxiomRuleCo ax cs') } + + ------------------ + go_prov cxt (PhantomProv co) = PhantomProv <$> go_co cxt co + go_prov cxt (ProofIrrelProv co) = ProofIrrelProv <$> go_co cxt co + go_prov _ p@(PluginProv _) = return p + go_prov _ p@(CorePrepProv _) = return p + |