diff options
29 files changed, 2658 insertions, 2522 deletions
diff --git a/compiler/basicTypes/Var.hs b/compiler/basicTypes/Var.hs index 5ba49fa66c..f5142caf3c 100644 --- a/compiler/basicTypes/Var.hs +++ b/compiler/basicTypes/Var.hs @@ -89,7 +89,8 @@ module Var ( import GhcPrelude -import {-# SOURCE #-} TyCoRep( Type, Kind, pprKind ) +import {-# SOURCE #-} TyCoRep( Type, Kind ) +import {-# SOURCE #-} TyCoPpr( pprKind ) import {-# SOURCE #-} TcType( TcTyVarDetails, pprTcTyVarDetails, vanillaSkolemTv ) import {-# SOURCE #-} IdInfo( IdDetails, IdInfo, coVarDetails, isCoVarDetails, vanillaIdInfo, pprIdDetails ) diff --git a/compiler/coreSyn/CoreFVs.hs b/compiler/coreSyn/CoreFVs.hs index 4674b21978..7f52054496 100644 --- a/compiler/coreSyn/CoreFVs.hs +++ b/compiler/coreSyn/CoreFVs.hs @@ -72,6 +72,7 @@ import VarSet import Var import Type import TyCoRep +import TyCoFVs import TyCon import CoAxiom import FamInstEnv diff --git a/compiler/coreSyn/CoreLint.hs b/compiler/coreSyn/CoreLint.hs index 9247498c74..86943e2ba7 100644 --- a/compiler/coreSyn/CoreLint.hs +++ b/compiler/coreSyn/CoreLint.hs @@ -49,6 +49,8 @@ import Kind import Type import RepType import TyCoRep -- checks validity of types/coercions +import TyCoSubst +import TyCoFVs import TyCon import CoAxiom import BasicTypes @@ -1051,7 +1053,7 @@ lintTyApp fun_ty arg_ty ; in_scope <- getInScope -- substTy needs the set of tyvars in scope to avoid generating -- uniques that are already in scope. - -- See Note [The substitution invariant] in TyCoRep + -- See Note [The substitution invariant] in TyCoSubst ; return (substTyWithInScope in_scope [tv] [arg_ty] body_ty) } | otherwise @@ -1495,7 +1497,7 @@ lint_app :: SDoc -> LintedKind -> [(LintedType,LintedKind)] -> LintM Kind lint_app doc kfn kas = do { in_scope <- getInScope -- We need the in_scope set to satisfy the invariant in - -- Note [The substitution invariant] in TyCoRep + -- Note [The substitution invariant] in TyCoSubst ; foldlM (go_app in_scope) kfn kas } where fail_msg extra = vcat [ hang (text "Kind application error in") 2 doc @@ -1717,7 +1719,7 @@ lintCoercion (ForAllCo tv1 kind_co co) -- scope. All the free vars of `t2` and `kind_co` should -- already be in `in_scope`, because they've been -- linted and `tv2` has the same unique as `tv1`. - -- See Note [The substitution invariant] + -- See Note [The substitution invariant] in TyCoSubst. unitVarEnv tv1 (TyVarTy tv2 `mkCastTy` mkSymCo kind_co) tyr = mkInvForAllTy tv2 $ substTy subst t2 @@ -1748,7 +1750,7 @@ lintCoercion (ForAllCo cv1 kind_co co) -- scope. All the free vars of `t2` and `kind_co` should -- already be in `in_scope`, because they've been -- linted and `cv2` has the same unique as `cv1`. - -- See Note [The substitution invariant] + -- See Note [The substitution invariant] in TyCoSubst. unitVarEnv cv1 (eta1 `mkTransCo` (mkCoVarCo cv2) `mkTransCo` (mkSymCo eta2)) tyr = mkTyCoInvForAllTy cv2 $ diff --git a/compiler/coreSyn/CoreSubst.hs b/compiler/coreSyn/CoreSubst.hs index 8ba2e68446..695c7a2f9d 100644 --- a/compiler/coreSyn/CoreSubst.hs +++ b/compiler/coreSyn/CoreSubst.hs @@ -79,9 +79,9 @@ import Data.List -- -- Some invariants apply to how you use the substitution: -- --- 1. Note [The substitution invariant] in TyCoRep +-- 1. Note [The substitution invariant] in TyCoSubst -- --- 2. Note [Substitutions apply only once] in TyCoRep +-- 2. Note [Substitutions apply only once] in TyCoSubst data Subst = Subst InScopeSet -- Variables in in scope (both Ids and TyVars) /after/ -- applying the substitution @@ -89,7 +89,7 @@ data Subst TvSubstEnv -- Substitution from TyVars to Types CvSubstEnv -- Substitution from CoVars to Coercions - -- INVARIANT 1: See TyCoRep Note [The substitution invariant] + -- INVARIANT 1: See TyCoSubst Note [The substitution invariant] -- This is what lets us deal with name capture properly -- It's a hard invariant to check... -- @@ -104,7 +104,7 @@ Note [Extending the Subst] For a core Subst, which binds Ids as well, we make a different choice for Ids than we do for TyVars. -For TyVars, see Note [Extending the TCvSubst] with Type.TvSubstEnv +For TyVars, see Note [Extending the TCvSubst] in TyCoSubst. For Ids, we have a different invariant The IdSubstEnv is extended *only* when the Unique on an Id changes @@ -171,7 +171,7 @@ mkEmptySubst in_scope = Subst in_scope emptyVarEnv emptyVarEnv emptyVarEnv mkSubst :: InScopeSet -> TvSubstEnv -> CvSubstEnv -> IdSubstEnv -> Subst mkSubst in_scope tvs cvs ids = Subst in_scope ids tvs cvs --- | Find the in-scope set: see TyCoRep Note [The substitution invariant] +-- | Find the in-scope set: see TyCoSubst Note [The substitution invariant] substInScope :: Subst -> InScopeSet substInScope (Subst in_scope _ _ _) = in_scope @@ -181,7 +181,7 @@ zapSubstEnv :: Subst -> Subst zapSubstEnv (Subst in_scope _ _ _) = Subst in_scope emptyVarEnv emptyVarEnv emptyVarEnv -- | Add a substitution for an 'Id' to the 'Subst': you must ensure that the in-scope set is --- such that TyCoRep Note [The substitution invariant] +-- such that TyCoSubst Note [The substitution invariant] -- holds after extending the substitution like this extendIdSubst :: Subst -> Id -> CoreExpr -> Subst -- ToDo: add an ASSERT that fvs(subst-result) is already in the in-scope set @@ -198,7 +198,7 @@ extendIdSubstList (Subst in_scope ids tvs cvs) prs -- | Add a substitution for a 'TyVar' to the 'Subst' -- The 'TyVar' *must* be a real TyVar, and not a CoVar -- You must ensure that the in-scope set is such that --- TyCoRep Note [The substitution invariant] holds +-- TyCoSubst Note [The substitution invariant] holds -- after extending the substitution like this. extendTvSubst :: Subst -> TyVar -> Type -> Subst extendTvSubst (Subst in_scope ids tvs cvs) tv ty @@ -214,7 +214,7 @@ extendTvSubstList subst vrs -- | Add a substitution from a 'CoVar' to a 'Coercion' to the 'Subst': -- you must ensure that the in-scope set satisfies --- TyCoRep Note [The substitution invariant] +-- TyCoSubst Note [The substitution invariant] -- after extending the substitution like this extendCvSubst :: Subst -> CoVar -> Coercion -> Subst extendCvSubst (Subst in_scope ids tvs cvs) v r @@ -339,7 +339,7 @@ instance Outputable Subst where -- | Apply a substitution to an entire 'CoreExpr'. Remember, you may only -- apply the substitution /once/: --- see Note [Substitutions apply only once] in TyCoRep +-- See Note [Substitutions apply only once] in TyCoSubst -- -- Do *not* attempt to short-cut in the case of an empty substitution! -- See Note [Extending the Subst] diff --git a/compiler/ghc.cabal.in b/compiler/ghc.cabal.in index 01013ca34b..479871c303 100644 --- a/compiler/ghc.cabal.in +++ b/compiler/ghc.cabal.in @@ -547,6 +547,10 @@ Library Kind Type TyCoRep + TyCoFVs + TyCoSubst + TyCoPpr + TyCoTidy Unify Bag Binary diff --git a/compiler/hsSyn/HsUtils.hs b/compiler/hsSyn/HsUtils.hs index 93e7cf5f81..c49ce8acf2 100644 --- a/compiler/hsSyn/HsUtils.hs +++ b/compiler/hsSyn/HsUtils.hs @@ -106,6 +106,7 @@ import TcEvidence import RdrName import Var import TyCoRep +import TyCoFVs ( tyConAppNeedsKindSig ) import Type ( appTyArgFlags, splitAppTys, tyConArgFlags ) import TysWiredIn ( unitTy ) import TcType diff --git a/compiler/iface/IfaceType.hs b/compiler/iface/IfaceType.hs index 298e14e463..9e7021bcc9 100644 --- a/compiler/iface/IfaceType.hs +++ b/compiler/iface/IfaceType.hs @@ -1075,7 +1075,7 @@ pprIfaceSigmaType show_forall ty pprUserIfaceForAll :: [IfaceForAllBndr] -> SDoc pprUserIfaceForAll tvs = sdocWithDynFlags $ \dflags -> - -- See Note [When to print foralls] + -- See Note [When to print foralls] in this module. ppWhen (any tv_has_kind_var tvs || any tv_is_required tvs || gopt Opt_PrintExplicitForalls dflags) $ diff --git a/compiler/iface/TcIface.hs b/compiler/iface/TcIface.hs index 5c3b64af0f..1e9fe4fbfa 100644 --- a/compiler/iface/TcIface.hs +++ b/compiler/iface/TcIface.hs @@ -35,6 +35,7 @@ import Type import Coercion import CoAxiom import TyCoRep -- needs to build types & coercions in a knot +import TyCoSubst ( substTyCoVars ) import HscTypes import Annotations import InstEnv diff --git a/compiler/iface/ToIface.hs b/compiler/iface/ToIface.hs index 535c1080f2..f20fed214a 100644 --- a/compiler/iface/ToIface.hs +++ b/compiler/iface/ToIface.hs @@ -68,6 +68,7 @@ import Var import VarEnv import VarSet import TyCoRep +import TyCoTidy ( tidyCo ) import Demand ( isTopSig ) import Data.Maybe ( catMaybes ) diff --git a/compiler/stgSyn/StgSubst.hs b/compiler/stgSyn/StgSubst.hs index 72fbe418d1..0616c6c529 100644 --- a/compiler/stgSyn/StgSubst.hs +++ b/compiler/stgSyn/StgSubst.hs @@ -72,7 +72,7 @@ extendInScope :: Id -> Subst -> Subst extendInScope id (Subst in_scope env) = Subst (in_scope `extendInScopeSet` id) env -- | Add a substitution for an 'Id' to the 'Subst': you must ensure that the --- in-scope set is such that TyCORep Note [The substitution invariant] +-- in-scope set is such that TyCoSubst Note [The substitution invariant] -- holds after extending the substitution like this. extendSubst :: Id -> Id -> Subst -> Subst extendSubst id new_id (Subst in_scope env) diff --git a/compiler/typecheck/TcExpr.hs b/compiler/typecheck/TcExpr.hs index e8d5ee6baa..df735d23d6 100644 --- a/compiler/typecheck/TcExpr.hs +++ b/compiler/typecheck/TcExpr.hs @@ -56,6 +56,7 @@ import NameSet import RdrName import TyCon import TyCoRep +import TyCoSubst (substTyWithInScope) import Type import TcEvidence import VarSet diff --git a/compiler/typecheck/TcPatSyn.hs b/compiler/typecheck/TcPatSyn.hs index 49f15e2849..b2b552725f 100644 --- a/compiler/typecheck/TcPatSyn.hs +++ b/compiler/typecheck/TcPatSyn.hs @@ -397,7 +397,7 @@ tcCheckPatSynDecl psb@PSB{ psb_id = lname@(dL->L _ name), psb_args = details -- satisfy the substitution invariant. There's no need to -- add 'ex_tvs' as they are already in the domain of the -- substitution. - -- See also Note [The substitution invariant] in TyCoRep. + -- See also Note [The substitution invariant] in TyCoSubst. ; prov_dicts <- mapM (emitWanted (ProvCtxtOrigin psb)) prov_theta' ; args' <- zipWithM (tc_arg subst) arg_names arg_tys ; return (ex_tvs', prov_dicts, args') } diff --git a/compiler/typecheck/TcSplice.hs b/compiler/typecheck/TcSplice.hs index 242028f578..47eaed3916 100644 --- a/compiler/typecheck/TcSplice.hs +++ b/compiler/typecheck/TcSplice.hs @@ -74,6 +74,7 @@ import TcMType import TcHsType import TcIface import TyCoRep +import TyCoFVs ( tyConAppNeedsKindSig ) import FamInst import FamInstEnv import InstEnv diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs index 55cb501139..c55d16ae9a 100644 --- a/compiler/typecheck/TcType.hs +++ b/compiler/typecheck/TcType.hs @@ -196,6 +196,9 @@ import GhcPrelude import Kind import TyCoRep +import TyCoSubst ( mkTvSubst, substTyWithCoVars ) +import TyCoFVs +import TyCoPpr ( pprParendTheta ) import Class import Var import ForeignCall diff --git a/compiler/types/Class.hs b/compiler/types/Class.hs index a50135bd7b..b5619142d1 100644 --- a/compiler/types/Class.hs +++ b/compiler/types/Class.hs @@ -26,7 +26,8 @@ module Class ( import GhcPrelude import {-# SOURCE #-} TyCon ( TyCon ) -import {-# SOURCE #-} TyCoRep ( Type, PredType, pprType ) +import {-# SOURCE #-} TyCoRep ( Type, PredType ) +import {-# SOURCE #-} TyCoPpr ( pprType ) import Var import Name import BasicTypes diff --git a/compiler/types/CoAxiom.hs b/compiler/types/CoAxiom.hs index a29659ab14..a814b6e021 100644 --- a/compiler/types/CoAxiom.hs +++ b/compiler/types/CoAxiom.hs @@ -31,7 +31,8 @@ module CoAxiom ( import GhcPrelude -import {-# SOURCE #-} TyCoRep ( Type, pprType ) +import {-# SOURCE #-} TyCoRep ( Type ) +import {-# SOURCE #-} TyCoPpr ( pprType ) import {-# SOURCE #-} TyCon ( TyCon ) import Outputable import FastString diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs index 81331e0b8e..d37887e9e7 100644 --- a/compiler/types/Coercion.hs +++ b/compiler/types/Coercion.hs @@ -120,6 +120,10 @@ import GhcPrelude import IfaceType import TyCoRep +import TyCoFVs +import TyCoPpr +import TyCoSubst +import TyCoTidy import Type import TyCon import CoAxiom diff --git a/compiler/types/OptCoercion.hs b/compiler/types/OptCoercion.hs index 67a61a3ded..936663a3d0 100644 --- a/compiler/types/OptCoercion.hs +++ b/compiler/types/OptCoercion.hs @@ -10,6 +10,7 @@ import GhcPrelude import DynFlags import TyCoRep +import TyCoSubst import Coercion import Type hiding( substTyVarBndr, substTy ) import TcType ( exactTyCoVarsOfType ) diff --git a/compiler/types/TyCoFVs.hs b/compiler/types/TyCoFVs.hs new file mode 100644 index 0000000000..09ef6c4618 --- /dev/null +++ b/compiler/types/TyCoFVs.hs @@ -0,0 +1,999 @@ +module TyCoFVs + ( + tyCoVarsOfType, tyCoVarsOfTypeDSet, tyCoVarsOfTypes, tyCoVarsOfTypesDSet, + tyCoFVsBndr, tyCoFVsVarBndr, tyCoFVsVarBndrs, + tyCoFVsOfType, tyCoVarsOfTypeList, + tyCoFVsOfTypes, tyCoVarsOfTypesList, + tyCoVarsOfTypesSet, tyCoVarsOfCosSet, + coVarsOfType, coVarsOfTypes, + coVarsOfCo, coVarsOfCos, + tyCoVarsOfCo, tyCoVarsOfCos, + tyCoVarsOfCoDSet, + tyCoFVsOfCo, tyCoFVsOfCos, + tyCoVarsOfCoList, tyCoVarsOfProv, + almostDevoidCoVarOfCo, + injectiveVarsOfType, tyConAppNeedsKindSig, + + noFreeVarsOfType, noFreeVarsOfTypes, noFreeVarsOfCo, + + mkTyCoInScopeSet, + + -- * Welll-scoped free variables + scopedSort, tyCoVarsOfTypeWellScoped, + tyCoVarsOfTypesWellScoped, + ) where + +import GhcPrelude + +import {-# SOURCE #-} Type (coreView) + +import TyCoRep +import TyCon +import Var +import FV + +import UniqFM +import VarSet +import VarEnv +import Util +import Panic + +{- +%************************************************************************ +%* * + Free variables of types and coercions +%* * +%************************************************************************ +-} + +{- Note [Free variables of types] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +The family of functions tyCoVarsOfType, tyCoVarsOfTypes etc, returns +a VarSet that is closed over the types of its variables. More precisely, + if S = tyCoVarsOfType( t ) + and (a:k) is in S + then tyCoVarsOftype( k ) is a subset of S + +Example: The tyCoVars of this ((a:* -> k) Int) is {a, k}. + +We could /not/ close over the kinds of the variable occurrences, and +instead do so at call sites, but it seems that we always want to do +so, so it's easiest to do it here. + +It turns out that getting the free variables of types is performance critical, +so we profiled several versions, exploring different implementation strategies. + +1. Baseline version: uses FV naively. Essentially: + + tyCoVarsOfType ty = fvVarSet $ tyCoFVsOfType ty + + This is not nice, because FV introduces some overhead to implement + determinism, and throught its "interesting var" function, neither of which + we need here, so they are a complete waste. + +2. UnionVarSet version: instead of reusing the FV-based code, we simply used + VarSets directly, trying to avoid the overhead of FV. E.g.: + + -- FV version: + tyCoFVsOfType (AppTy fun arg) a b c = (tyCoFVsOfType fun `unionFV` tyCoFVsOfType arg) a b c + + -- UnionVarSet version: + tyCoVarsOfType (AppTy fun arg) = (tyCoVarsOfType fun `unionVarSet` tyCoVarsOfType arg) + + This looks deceptively similar, but while FV internally builds a list- and + set-generating function, the VarSet functions manipulate sets directly, and + the latter peforms a lot worse than the naive FV version. + +3. Accumulator-style VarSet version: this is what we use now. We do use VarSet + as our data structure, but delegate the actual work to a new + ty_co_vars_of_... family of functions, which use accumulator style and the + "in-scope set" filter found in the internals of FV, but without the + determinism overhead. + +See #14880. + +Note [Closing over free variable kinds] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +tyCoVarsOfType and tyCoFVsOfType, while traversing a type, will also close over +free variable kinds. In previous GHC versions, this happened naively: whenever +we would encounter an occurrence of a free type variable, we would close over +its kind. This, however is wrong for two reasons (see #14880): + +1. Efficiency. If we have Proxy (a::k) -> Proxy (a::k) -> Proxy (a::k), then + we don't want to have to traverse k more than once. + +2. Correctness. Imagine we have forall k. b -> k, where b has + kind k, for some k bound in an outer scope. If we look at b's kind inside + the forall, we'll collect that k is free and then remove k from the set of + free variables. This is plain wrong. We must instead compute that b is free + and then conclude that b's kind is free. + +An obvious first approach is to move the closing-over-kinds from the +occurrences of a type variable to after finding the free vars - however, this +turns out to introduce performance regressions, and isn't even entirely +correct. + +In fact, it isn't even important *when* we close over kinds; what matters is +that we handle each type var exactly once, and that we do it in the right +context. + +So the next approach we tried was to use the "in-scope set" part of FV or the +equivalent argument in the accumulator-style `ty_co_vars_of_type` function, to +say "don't bother with variables we have already closed over". This should work +fine in theory, but the code is complicated and doesn't perform well. + +But there is a simpler way, which is implemented here. Consider the two points +above: + +1. Efficiency: we now have an accumulator, so the second time we encounter 'a', + we'll ignore it, certainly not looking at its kind - this is why + pre-checking set membership before inserting ends up not only being faster, + but also being correct. + +2. Correctness: we have an "in-scope set" (I think we should call it it a + "bound-var set"), specifying variables that are bound by a forall in the type + we are traversing; we simply ignore these variables, certainly not looking at + their kind. + +So now consider: + + forall k. b -> k + +where b :: k->Type is free; but of course, it's a different k! When looking at +b -> k we'll have k in the bound-var set. So we'll ignore the k. But suppose +this is our first encounter with b; we want the free vars of its kind. But we +want to behave as if we took the free vars of its kind at the end; that is, +with no bound vars in scope. + +So the solution is easy. The old code was this: + + 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) + +Now all we need to do is take the free vars of tyVarKind v *with an empty +bound-var set*, thus: + +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 (extendVarSet acc v) + ^^^^^^^^^^^ + +And that's it. + +-} + +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) + 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) + +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 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) + +-- | `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. +tyCoVarsOfTypeDSet :: Type -> DTyCoVarSet +-- See Note [Free variables of types] +tyCoVarsOfTypeDSet ty = fvDVarSet $ tyCoFVsOfType ty + +-- | `tyCoFVsOfType` that returns free variables of a type in deterministic +-- order. For explanation of why using `VarSet` is not deterministic see +-- Note [Deterministic FV] in FV. +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. +-- It's exported, so that it can be composed with +-- other functions that compute free variables. +-- See Note [FV naming conventions] in FV. +-- +-- Eta-expanded because that makes it run faster (apparently) +-- See Note [FV eta expansion] in FV for explanation. +tyCoFVsOfType :: Type -> FV +-- See Note [Free variables of types] +tyCoFVsOfType (TyVarTy v) f bound_vars (acc_list, acc_set) + | not (f v) = (acc_list, acc_set) + | v `elemVarSet` bound_vars = (acc_list, acc_set) + | v `elemVarSet` acc_set = (acc_list, acc_set) + | otherwise = tyCoFVsOfType (tyVarKind v) f + emptyVarSet -- See Note [Closing over free variable kinds] + (v:acc_list, extendVarSet acc_set v) +tyCoFVsOfType (TyConApp _ tys) f bound_vars acc = tyCoFVsOfTypes tys f bound_vars acc +tyCoFVsOfType (LitTy {}) f bound_vars acc = emptyFV f bound_vars acc +tyCoFVsOfType (AppTy fun arg) f bound_vars acc = (tyCoFVsOfType fun `unionFV` tyCoFVsOfType arg) f bound_vars acc +tyCoFVsOfType (FunTy _ arg res) f bound_vars acc = (tyCoFVsOfType arg `unionFV` tyCoFVsOfType res) f bound_vars acc +tyCoFVsOfType (ForAllTy bndr ty) f bound_vars acc = tyCoFVsBndr bndr (tyCoFVsOfType ty) f bound_vars acc +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 +-- Free vars of (forall b. <thing with fvs>) +tyCoFVsBndr (Bndr tv _) fvs = tyCoFVsVarBndr tv fvs + +tyCoFVsVarBndrs :: [Var] -> FV -> FV +tyCoFVsVarBndrs vars fvs = foldr tyCoFVsVarBndr fvs vars + +tyCoFVsVarBndr :: Var -> FV -> FV +tyCoFVsVarBndr var fvs + = tyCoFVsOfType (varType var) -- Free vars of its type/kind + `unionFV` delFV var fvs -- Delete it from the thing-inside + +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 + +-- | Get a deterministic set of the vars free in a coercion +tyCoVarsOfCoDSet :: Coercion -> DTyCoVarSet +-- See Note [Free variables of types] +tyCoVarsOfCoDSet co = fvDVarSet $ tyCoFVsOfCo co + +tyCoVarsOfCoList :: Coercion -> [TyCoVar] +-- See Note [Free variables of types] +tyCoVarsOfCoList co = fvVarList $ tyCoFVsOfCo co + +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] +tyCoFVsOfCo (Refl ty) fv_cand in_scope acc + = tyCoFVsOfType ty fv_cand in_scope acc +tyCoFVsOfCo (GRefl _ ty mco) fv_cand in_scope acc + = (tyCoFVsOfType ty `unionFV` tyCoFVsOfMCo mco) fv_cand in_scope acc +tyCoFVsOfCo (TyConAppCo _ _ cos) fv_cand in_scope acc = tyCoFVsOfCos cos fv_cand in_scope acc +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 _ co1 co2) fv_cand in_scope acc + = (tyCoFVsOfCo co1 `unionFV` tyCoFVsOfCo co2) fv_cand in_scope acc +tyCoFVsOfCo (CoVarCo v) fv_cand in_scope acc + = tyCoFVsOfCoVar v fv_cand in_scope acc +tyCoFVsOfCo (HoleCo h) fv_cand in_scope acc + = tyCoFVsOfCoVar (coHoleCoVar h) fv_cand in_scope acc + -- See Note [CoercionHoles and coercion free variables] +tyCoFVsOfCo (AxiomInstCo _ _ cos) fv_cand in_scope acc = tyCoFVsOfCos cos fv_cand in_scope acc +tyCoFVsOfCo (UnivCo p _ t1 t2) fv_cand in_scope acc + = (tyCoFVsOfProv p `unionFV` tyCoFVsOfType t1 + `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 (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 +tyCoFVsOfCo (SubCo co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc +tyCoFVsOfCo (AxiomRuleCo _ cs) fv_cand in_scope acc = tyCoFVsOfCos cs fv_cand in_scope acc + +tyCoFVsOfCoVar :: CoVar -> FV +tyCoFVsOfCoVar v fv_cand in_scope acc + = (unitFV v `unionFV` tyCoFVsOfType (varType v)) fv_cand in_scope acc + +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 + +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 ----------- + +{- + +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 +considerations outlined in Note [Free variables of types]. + +This is because FV includes the InterestingVarFun, which is useful here, +because we can cleverly use it to restrict our calculations to CoVars - this +is what getCoVarSet achieves. + +See #14880. + +-} + +getCoVarSet :: FV -> CoVarSet +getCoVarSet fv = snd (fv isCoVar emptyVarSet ([], emptyVarSet)) + +coVarsOfType :: Type -> CoVarSet +coVarsOfType ty = getCoVarSet (tyCoFVsOfType ty) + +coVarsOfTypes :: [Type] -> TyCoVarSet +coVarsOfTypes tys = getCoVarSet (tyCoFVsOfTypes tys) + +coVarsOfCo :: Coercion -> CoVarSet +coVarsOfCo co = getCoVarSet (tyCoFVsOfCo co) + +coVarsOfCos :: [Coercion] -> CoVarSet +coVarsOfCos cos = getCoVarSet (tyCoFVsOfCos cos) + +----- Whether a covar is /Almost Devoid/ in a type or coercion ---- + +-- | Given a covar and a coercion, returns True if covar is almost devoid in +-- the coercion. That is, covar can only appear in Refl and GRefl. +-- See last wrinkle in Note [Unused coercion variable in ForAllCo] in Coercion +almostDevoidCoVarOfCo :: CoVar -> Coercion -> Bool +almostDevoidCoVarOfCo cv co = + almost_devoid_co_var_of_co co cv + +almost_devoid_co_var_of_co :: Coercion -> CoVar -> Bool +almost_devoid_co_var_of_co (Refl {}) _ = True -- covar is allowed in Refl and +almost_devoid_co_var_of_co (GRefl {}) _ = True -- GRefl, so we don't look into + -- the coercions +almost_devoid_co_var_of_co (TyConAppCo _ _ cos) cv + = almost_devoid_co_var_of_cos cos cv +almost_devoid_co_var_of_co (AppCo co arg) cv + = almost_devoid_co_var_of_co co cv + && almost_devoid_co_var_of_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 _ 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 (CoVarCo v) cv = v /= cv +almost_devoid_co_var_of_co (HoleCo h) cv = (coHoleCoVar h) /= cv +almost_devoid_co_var_of_co (AxiomInstCo _ _ cos) cv + = almost_devoid_co_var_of_cos cos cv +almost_devoid_co_var_of_co (UnivCo p _ t1 t2) cv + = almost_devoid_co_var_of_prov p cv + && almost_devoid_co_var_of_type t1 cv + && almost_devoid_co_var_of_type t2 cv +almost_devoid_co_var_of_co (SymCo co) cv + = almost_devoid_co_var_of_co 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 co cv +almost_devoid_co_var_of_co (LRCo _ co) cv + = almost_devoid_co_var_of_co co cv +almost_devoid_co_var_of_co (InstCo co arg) cv + = almost_devoid_co_var_of_co co cv + && almost_devoid_co_var_of_co arg cv +almost_devoid_co_var_of_co (KindCo co) cv + = almost_devoid_co_var_of_co co cv +almost_devoid_co_var_of_co (SubCo co) cv + = almost_devoid_co_var_of_co co cv +almost_devoid_co_var_of_co (AxiomRuleCo _ cs) cv + = almost_devoid_co_var_of_cos cs cv + +almost_devoid_co_var_of_cos :: [Coercion] -> CoVar -> Bool +almost_devoid_co_var_of_cos [] _ = True +almost_devoid_co_var_of_cos (co:cos) cv + = almost_devoid_co_var_of_co co cv + && almost_devoid_co_var_of_cos cos cv + +almost_devoid_co_var_of_prov :: UnivCoProvenance -> CoVar -> Bool +almost_devoid_co_var_of_prov (PhantomProv co) cv + = almost_devoid_co_var_of_co co cv +almost_devoid_co_var_of_prov (ProofIrrelProv co) cv + = almost_devoid_co_var_of_co co cv +almost_devoid_co_var_of_prov UnsafeCoerceProv _ = True +almost_devoid_co_var_of_prov (PluginProv _) _ = True + +almost_devoid_co_var_of_type :: Type -> CoVar -> Bool +almost_devoid_co_var_of_type (TyVarTy _) _ = True +almost_devoid_co_var_of_type (TyConApp _ tys) cv + = almost_devoid_co_var_of_types tys cv +almost_devoid_co_var_of_type (LitTy {}) _ = True +almost_devoid_co_var_of_type (AppTy fun arg) cv + = almost_devoid_co_var_of_type fun cv + && almost_devoid_co_var_of_type arg cv +almost_devoid_co_var_of_type (FunTy _ arg res) cv + = almost_devoid_co_var_of_type arg cv + && almost_devoid_co_var_of_type res cv +almost_devoid_co_var_of_type (ForAllTy (Bndr v _) ty) cv + = almost_devoid_co_var_of_type (varType v) cv + && (v == cv || almost_devoid_co_var_of_type ty cv) +almost_devoid_co_var_of_type (CastTy ty co) cv + = almost_devoid_co_var_of_type ty cv + && almost_devoid_co_var_of_co co cv +almost_devoid_co_var_of_type (CoercionTy co) cv + = almost_devoid_co_var_of_co co cv + +almost_devoid_co_var_of_types :: [Type] -> CoVar -> Bool +almost_devoid_co_var_of_types [] _ = True +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 ----------------- + +-- | Returns the free variables of a 'Type' that are in injective positions. +-- For example, if @F@ is a non-injective type family, then: +-- +-- @ +-- injectiveTyVarsOf( Either c (Maybe (a, F b c)) ) = {a,c} +-- @ +-- +-- If @'injectiveVarsOfType' ty = itvs@, then knowing @ty@ fixes @itvs@. +-- More formally, if +-- @a@ is in @'injectiveVarsOfType' ty@ +-- and @S1(ty) ~ S2(ty)@, +-- then @S1(a) ~ S2(a)@, +-- where @S1@ and @S2@ are arbitrary substitutions. +-- +-- See @Note [When does a tycon application need an explicit kind signature?]@. +injectiveVarsOfType :: Type -> FV +injectiveVarsOfType = go + where + go ty | Just ty' <- coreView ty + = go ty' + go (TyVarTy v) = unitFV v `unionFV` go (tyVarKind v) + go (AppTy f a) = go f `unionFV` go a + go (FunTy _ ty1 ty2) = go ty1 `unionFV` go ty2 + go (TyConApp tc tys) = + case tyConInjectivityInfo tc of + NotInjective -> emptyFV + Injective inj -> mapUnionFV go $ + filterByList (inj ++ repeat True) tys + -- Oversaturated arguments to a tycon are + -- always injective, hence the repeat True + go (ForAllTy tvb ty) = tyCoFVsBndr tvb $ go ty + go LitTy{} = emptyFV + 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 +noFreeVarsOfType (TyVarTy _) = False +noFreeVarsOfType (AppTy t1 t2) = noFreeVarsOfType t1 && noFreeVarsOfType t2 +noFreeVarsOfType (TyConApp _ tys) = all noFreeVarsOfType tys +noFreeVarsOfType ty@(ForAllTy {}) = isEmptyVarSet (tyCoVarsOfType ty) +noFreeVarsOfType (FunTy _ t1 t2) = noFreeVarsOfType t1 && noFreeVarsOfType t2 +noFreeVarsOfType (LitTy _) = True +noFreeVarsOfType (CastTy ty co) = noFreeVarsOfType ty && noFreeVarsOfCo co +noFreeVarsOfType (CoercionTy co) = noFreeVarsOfCo co + +noFreeVarsOfMCo :: MCoercion -> Bool +noFreeVarsOfMCo MRefl = True +noFreeVarsOfMCo (MCo co) = noFreeVarsOfCo co + +noFreeVarsOfTypes :: [Type] -> Bool +noFreeVarsOfTypes = all noFreeVarsOfType + +-- | Returns True if this coercion has no free variables. Should be the same as +-- isEmptyVarSet . tyCoVarsOfCo, but faster in the non-forall case. +noFreeVarsOfCo :: Coercion -> Bool +noFreeVarsOfCo (Refl ty) = noFreeVarsOfType ty +noFreeVarsOfCo (GRefl _ ty co) = noFreeVarsOfType ty && noFreeVarsOfMCo co +noFreeVarsOfCo (TyConAppCo _ _ args) = all noFreeVarsOfCo args +noFreeVarsOfCo (AppCo c1 c2) = noFreeVarsOfCo c1 && noFreeVarsOfCo c2 +noFreeVarsOfCo co@(ForAllCo {}) = isEmptyVarSet (tyCoVarsOfCo co) +noFreeVarsOfCo (FunCo _ c1 c2) = noFreeVarsOfCo c1 && noFreeVarsOfCo c2 +noFreeVarsOfCo (CoVarCo _) = False +noFreeVarsOfCo (HoleCo {}) = True -- I'm unsure; probably never happens +noFreeVarsOfCo (AxiomInstCo _ _ args) = all noFreeVarsOfCo args +noFreeVarsOfCo (UnivCo p _ t1 t2) = noFreeVarsOfProv p && + noFreeVarsOfType t1 && + noFreeVarsOfType t2 +noFreeVarsOfCo (SymCo co) = noFreeVarsOfCo co +noFreeVarsOfCo (TransCo co1 co2) = noFreeVarsOfCo co1 && noFreeVarsOfCo co2 +noFreeVarsOfCo (NthCo _ _ co) = noFreeVarsOfCo co +noFreeVarsOfCo (LRCo _ co) = noFreeVarsOfCo co +noFreeVarsOfCo (InstCo co1 co2) = noFreeVarsOfCo co1 && noFreeVarsOfCo co2 +noFreeVarsOfCo (KindCo co) = noFreeVarsOfCo co +noFreeVarsOfCo (SubCo co) = noFreeVarsOfCo co +noFreeVarsOfCo (AxiomRuleCo _ cs) = all noFreeVarsOfCo cs + +-- | Returns True if this UnivCoProv has no free variables. Should be the same as +-- isEmptyVarSet . tyCoVarsOfProv, but faster in the non-forall case. +noFreeVarsOfProv :: UnivCoProvenance -> Bool +noFreeVarsOfProv UnsafeCoerceProv = True +noFreeVarsOfProv (PhantomProv co) = noFreeVarsOfCo co +noFreeVarsOfProv (ProofIrrelProv co) = noFreeVarsOfCo co +noFreeVarsOfProv (PluginProv {}) = True + + +-- | Does a 'TyCon' (that is applied to some number of arguments) need to be +-- ascribed with an explicit kind signature to resolve ambiguity if rendered as +-- a source-syntax type? +-- (See @Note [When does a tycon application need an explicit kind signature?]@ +-- for a full explanation of what this function checks for.) + +-- Morally, this function ought to belong in TyCon.hs, not TyCoRep.hs, but +-- accomplishing this requires a fair deal of futzing aruond with .hs-boot +-- files. +tyConAppNeedsKindSig + :: Bool -- ^ Should specified binders count towards injective positions in + -- the kind of the TyCon? (If you're using visible kind + -- applications, then you want True here. + -> TyCon + -> Int -- ^ The number of args the 'TyCon' is applied to. + -> Bool -- ^ Does @T t_1 ... t_n@ need a kind signature? (Where @n@ is the + -- number of arguments) +tyConAppNeedsKindSig spec_inj_pos tc n_args + | LT <- listLengthCmp tc_binders n_args + = False + | otherwise + = let (dropped_binders, remaining_binders) + = splitAt n_args tc_binders + result_kind = mkTyConKind remaining_binders tc_res_kind + result_vars = tyCoVarsOfType result_kind + dropped_vars = fvVarSet $ + mapUnionFV injective_vars_of_binder dropped_binders + + in not (subVarSet result_vars dropped_vars) + where + tc_binders = tyConBinders tc + tc_res_kind = tyConResKind tc + + -- Returns the variables that would be fixed by knowing a TyConBinder. See + -- Note [When does a tycon application need an explicit kind signature?] + -- for a more detailed explanation of what this function does. + injective_vars_of_binder :: TyConBinder -> FV + injective_vars_of_binder (Bndr tv vis) = + case vis of + AnonTCB VisArg -> injectiveVarsOfType (varType tv) + NamedTCB argf | source_of_injectivity argf + -> unitFV tv `unionFV` injectiveVarsOfType (varType tv) + _ -> emptyFV + + source_of_injectivity Required = True + source_of_injectivity Specified = spec_inj_pos + source_of_injectivity Inferred = False + +{- +Note [When does a tycon application need an explicit kind signature?] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +There are a couple of places in GHC where we convert Core Types into forms that +more closely resemble user-written syntax. These include: + +1. Template Haskell Type reification (see, for instance, TcSplice.reify_tc_app) +2. Converting Types to LHsTypes (in HsUtils.typeToLHsType, or in Haddock) + +This conversion presents a challenge: how do we ensure that the resulting type +has enough kind information so as not to be ambiguous? To better motivate this +question, consider the following Core type: + + -- Foo :: Type -> Type + type Foo = Proxy Type + +There is nothing ambiguous about the RHS of Foo in Core. But if we were to, +say, reify it into a TH Type, then it's tempting to just drop the invisible +Type argument and simply return `Proxy`. But now we've lost crucial kind +information: we don't know if we're dealing with `Proxy Type` or `Proxy Bool` +or `Proxy Int` or something else! We've inadvertently introduced ambiguity. + +Unlike in other situations in GHC, we can't just turn on +-fprint-explicit-kinds, as we need to produce something which has the same +structure as a source-syntax type. Moreover, we can't rely on visible kind +application, since the first kind argument to Proxy is inferred, not specified. +Our solution is to annotate certain tycons with their kinds whenever they +appear in applied form in order to resolve the ambiguity. For instance, we +would reify the RHS of Foo like so: + + type Foo = (Proxy :: Type -> Type) + +We need to devise an algorithm that determines precisely which tycons need +these explicit kind signatures. We certainly don't want to annotate _every_ +tycon with a kind signature, or else we might end up with horribly bloated +types like the following: + + (Either :: Type -> Type -> Type) (Int :: Type) (Char :: Type) + +We only want to annotate tycons that absolutely require kind signatures in +order to resolve some sort of ambiguity, and nothing more. + +Suppose we have a tycon application (T ty_1 ... ty_n). Why might this type +require a kind signature? It might require it when we need to fill in any of +T's omitted arguments. By "omitted argument", we mean one that is dropped when +reifying ty_1 ... ty_n. Sometimes, the omitted arguments are inferred and +specified arguments (e.g., TH reification in TcSplice), and sometimes the +omitted arguments are only the inferred ones (e.g., in HsUtils.typeToLHsType, +which reifies specified arguments through visible kind application). +Regardless, the key idea is that _some_ arguments are going to be omitted after +reification, and the only mechanism we have at our disposal for filling them in +is through explicit kind signatures. + +What do we mean by "fill in"? Let's consider this small example: + + T :: forall {k}. Type -> (k -> Type) -> k + +Moreover, we have this application of T: + + T @{j} Int aty + +When we reify this type, we omit the inferred argument @{j}. Is it fixed by the +other (non-inferred) arguments? Yes! If we know the kind of (aty :: blah), then +we'll generate an equality constraint (kappa -> Type) and, assuming we can +solve it, that will fix `kappa`. (Here, `kappa` is the unification variable +that we instantiate `k` with.) + +Therefore, for any application of a tycon T to some arguments, the Question We +Must Answer is: + +* Given the first n arguments of T, do the kinds of the non-omitted arguments + fill in the omitted arguments? + +(This is still a bit hand-wavey, but we'll refine this question incrementally +as we explain more of the machinery underlying this process.) + +Answering this question is precisely the role that the `injectiveVarsOfType` +and `injective_vars_of_binder` functions exist to serve. If an omitted argument +`a` appears in the set returned by `injectiveVarsOfType ty`, then knowing +`ty` determines (i.e., fills in) `a`. (More on `injective_vars_of_binder` in a +bit.) + +More formally, if +`a` is in `injectiveVarsOfType ty` +and S1(ty) ~ S2(ty), +then S1(a) ~ S2(a), +where S1 and S2 are arbitrary substitutions. + +For example, is `F` is a non-injective type family, then + + injectiveVarsOfType(Either c (Maybe (a, F b c))) = {a, c} + +Now that we know what this function does, here is a second attempt at the +Question We Must Answer: + +* Given the first n arguments of T (ty_1 ... ty_n), consider the binders + of T that are instantiated by non-omitted arguments. Do the injective + variables of these binders fill in the remainder of T's kind? + +Alright, we're getting closer. Next, we need to clarify what the injective +variables of a tycon binder are. This the role that the +`injective_vars_of_binder` function serves. Here is what this function does for +each form of tycon binder: + +* Anonymous binders are injective positions. For example, in the promoted data + constructor '(:): + + '(:) :: forall a. a -> [a] -> [a] + + The second and third tyvar binders (of kinds `a` and `[a]`) are both + anonymous, so if we had '(:) 'True '[], then the kinds of 'True and + '[] would contribute to the kind of '(:) 'True '[]. Therefore, + injective_vars_of_binder(_ :: a) = injectiveVarsOfType(a) = {a}. + (Similarly, injective_vars_of_binder(_ :: [a]) = {a}.) +* Named binders: + - Inferred binders are never injective positions. For example, in this data + type: + + data Proxy a + Proxy :: forall {k}. k -> Type + + If we had Proxy 'True, then the kind of 'True would not contribute to the + kind of Proxy 'True. Therefore, + injective_vars_of_binder(forall {k}. ...) = {}. + - Required binders are injective positions. For example, in this data type: + + data Wurble k (a :: k) :: k + Wurble :: forall k -> k -> k + + The first tyvar binder (of kind `forall k`) has required visibility, so if + we had Wurble (Maybe a) Nothing, then the kind of Maybe a would + contribute to the kind of Wurble (Maybe a) Nothing. Hence, + injective_vars_of_binder(forall a -> ...) = {a}. + - Specified binders /might/ be injective positions, depending on how you + approach things. Continuing the '(:) example: + + '(:) :: forall a. a -> [a] -> [a] + + Normally, the (forall a. ...) tyvar binder wouldn't contribute to the kind + of '(:) 'True '[], since it's not explicitly instantiated by the user. But + if visible kind application is enabled, then this is possible, since the + user can write '(:) @Bool 'True '[]. (In that case, + injective_vars_of_binder(forall a. ...) = {a}.) + + There are some situations where using visible kind application is appropriate + (e.g., HsUtils.typeToLHsType) and others where it is not (e.g., TH + reification), so the `injective_vars_of_binder` function is parametrized by + a Bool which decides if specified binders should be counted towards + injective positions or not. + +Now that we've defined injective_vars_of_binder, we can refine the Question We +Must Answer once more: + +* Given the first n arguments of T (ty_1 ... ty_n), consider the binders + of T that are instantiated by non-omitted arguments. For each such binder + b_i, take the union of all injective_vars_of_binder(b_i). Is this set a + superset of the free variables of the remainder of T's kind? + +If the answer to this question is "no", then (T ty_1 ... ty_n) needs an +explicit kind signature, since T's kind has kind variables leftover that +aren't fixed by the non-omitted arguments. + +One last sticking point: what does "the remainder of T's kind" mean? You might +be tempted to think that it corresponds to all of the arguments in the kind of +T that would normally be instantiated by omitted arguments. But this isn't +quite right, strictly speaking. Consider the following (silly) example: + + S :: forall {k}. Type -> Type + +And suppose we have this application of S: + + S Int Bool + +The Int argument would be omitted, and +injective_vars_of_binder(_ :: Type) = {}. This is not a superset of {k}, which +might suggest that (S Bool) needs an explicit kind signature. But +(S Bool :: Type) doesn't actually fix `k`! This is because the kind signature +only affects the /result/ of the application, not all of the individual +arguments. So adding a kind signature here won't make a difference. Therefore, +the fourth (and final) iteration of the Question We Must Answer is: + +* Given the first n arguments of T (ty_1 ... ty_n), consider the binders + of T that are instantiated by non-omitted arguments. For each such binder + b_i, take the union of all injective_vars_of_binder(b_i). Is this set a + superset of the free variables of the kind of (T ty_1 ... ty_n)? + +Phew, that was a lot of work! + +How can be sure that this is correct? That is, how can we be sure that in the +event that we leave off a kind annotation, that one could infer the kind of the +tycon application from its arguments? It's essentially a proof by induction: if +we can infer the kinds of every subtree of a type, then the whole tycon +application will have an inferrable kind--unless, of course, the remainder of +the tycon application's kind has uninstantiated kind variables. + +What happens if T is oversaturated? That is, if T's kind has fewer than n +arguments, in the case that the concrete application instantiates a result +kind variable with an arrow kind? If we run out of arguments, we do not attach +a kind annotation. This should be a rare case, indeed. Here is an example: + + data T1 :: k1 -> k2 -> * + data T2 :: k1 -> k2 -> * + + type family G (a :: k) :: k + type instance G T1 = T2 + + type instance F Char = (G T1 Bool :: (* -> *) -> *) -- F from above + +Here G's kind is (forall k. k -> k), and the desugared RHS of that last +instance of F is (G (* -> (* -> *) -> *) (T1 * (* -> *)) Bool). According to +the algorithm above, there are 3 arguments to G so we should peel off 3 +arguments in G's kind. But G's kind has only two arguments. This is the +rare special case, and we choose not to annotate the application of G with +a kind signature. After all, we needn't do this, since that instance would +be reified as: + + type instance F Char = G (T1 :: * -> (* -> *) -> *) Bool + +So the kind of G isn't ambiguous anymore due to the explicit kind annotation +on its argument. See #8953 and test th/T8953. +-} + + +{- +%************************************************************************ +%* * + Well-scoped tyvars +* * +************************************************************************ + +Note [ScopedSort] +~~~~~~~~~~~~~~~~~ +Consider + + foo :: Proxy a -> Proxy (b :: k) -> Proxy (a :: k2) -> () + +This function type is implicitly generalised over [a, b, k, k2]. These +variables will be Specified; that is, they will be available for visible +type application. This is because they are written in the type signature +by the user. + +However, we must ask: what order will they appear in? In cases without +dependency, this is easy: we just use the lexical left-to-right ordering +of first occurrence. With dependency, we cannot get off the hook so +easily. + +We thus state: + + * These variables appear in the order as given by ScopedSort, where + the input to ScopedSort is the left-to-right order of first occurrence. + +Note that this applies only to *implicit* quantification, without a +`forall`. If the user writes a `forall`, then we just use the order given. + +ScopedSort is defined thusly (as proposed in #15743): + * Work left-to-right through the input list, with a cursor. + * If variable v at the cursor is depended on by any earlier variable w, + move v immediately before the leftmost such w. + +INVARIANT: The prefix of variables before the cursor form a valid telescope. + +Note that ScopedSort makes sense only after type inference is done and all +types/kinds are fully settled and zonked. + +-} + +-- | Do a topological sort on a list of tyvars, +-- so that binders occur before occurrences +-- E.g. given [ a::k, k::*, b::k ] +-- it'll return a well-scoped list [ k::*, a::k, b::k ] +-- +-- This is a deterministic sorting operation +-- (that is, doesn't depend on Uniques). +-- +-- It is also meant to be stable: that is, variables should not +-- be reordered unnecessarily. This is specified in Note [ScopedSort] +-- See also Note [Ordering of implicit variables] in RnTypes + +scopedSort :: [TyCoVar] -> [TyCoVar] +scopedSort = go [] [] + where + go :: [TyCoVar] -- already sorted, in reverse order + -> [TyCoVarSet] -- each set contains all the variables which must be placed + -- before the tv corresponding to the set; they are accumulations + -- of the fvs in the sorted tvs' kinds + + -- This list is in 1-to-1 correspondence with the sorted tyvars + -- INVARIANT: + -- all (\tl -> all (`subVarSet` head tl) (tail tl)) (tails fv_list) + -- That is, each set in the list is a superset of all later sets. + + -> [TyCoVar] -- yet to be sorted + -> [TyCoVar] + go acc _fv_list [] = reverse acc + go acc fv_list (tv:tvs) + = go acc' fv_list' tvs + where + (acc', fv_list') = insert tv acc fv_list + + insert :: TyCoVar -- var to insert + -> [TyCoVar] -- sorted list, in reverse order + -> [TyCoVarSet] -- list of fvs, as above + -> ([TyCoVar], [TyCoVarSet]) -- augmented lists + insert tv [] [] = ([tv], [tyCoVarsOfType (tyVarKind tv)]) + insert tv (a:as) (fvs:fvss) + | tv `elemVarSet` fvs + , (as', fvss') <- insert tv as fvss + = (a:as', fvs `unionVarSet` fv_tv : fvss') + + | otherwise + = (tv:a:as, fvs `unionVarSet` fv_tv : fvs : fvss) + where + fv_tv = tyCoVarsOfType (tyVarKind tv) + + -- lists not in correspondence + insert _ _ _ = panic "scopedSort" + +-- | Get the free vars of a type in scoped order +tyCoVarsOfTypeWellScoped :: Type -> [TyVar] +tyCoVarsOfTypeWellScoped = scopedSort . tyCoVarsOfTypeList + +-- | Get the free vars of types in scoped order +tyCoVarsOfTypesWellScoped :: [Type] -> [TyVar] +tyCoVarsOfTypesWellScoped = scopedSort . tyCoVarsOfTypesList + diff --git a/compiler/types/TyCoPpr.hs b/compiler/types/TyCoPpr.hs new file mode 100644 index 0000000000..fe43ae43a3 --- /dev/null +++ b/compiler/types/TyCoPpr.hs @@ -0,0 +1,308 @@ +-- | Pretty-printing types and coercions. +module TyCoPpr + ( + -- * Pretty-printing + pprType, pprParendType, pprPrecType, pprPrecTypeX, + pprTypeApp, pprTCvBndr, pprTCvBndrs, + pprSigmaType, + pprTheta, pprParendTheta, pprForAll, pprUserForAll, + pprTyVar, pprTyVars, + pprThetaArrowTy, pprClassPred, + pprKind, pprParendKind, pprTyLit, + PprPrec(..), topPrec, sigPrec, opPrec, funPrec, appPrec, maybeParen, + pprDataCons, pprWithExplicitKindsWhen, + + pprCo, pprParendCo, + + debugPprType, + ) where + +import GhcPrelude + +import {-# SOURCE #-} ToIface( toIfaceTypeX, toIfaceTyLit, toIfaceForAllBndr + , toIfaceTyCon, toIfaceTcArgs, toIfaceCoercionX ) +import {-# SOURCE #-} DataCon( dataConFullSig + , dataConUserTyVarBinders + , DataCon ) + +import TyCon +import TyCoRep +import TyCoTidy +import TyCoFVs +import Class +import Var + +import IfaceType + +import VarSet +import VarEnv + +import DynFlags ( gopt_set, GeneralFlag(Opt_PrintExplicitKinds) ) +import Outputable +import BasicTypes ( PprPrec(..), topPrec, sigPrec, opPrec + , funPrec, appPrec, maybeParen ) + +{- +%************************************************************************ +%* * + Pretty-printing types + + Defined very early because of debug printing in assertions +%* * +%************************************************************************ + +@pprType@ is the standard @Type@ printer; the overloaded @ppr@ function is +defined to use this. @pprParendType@ is the same, except it puts +parens around the type, except for the atomic cases. @pprParendType@ +works just by setting the initial context precedence very high. + +Note that any function which pretty-prints a @Type@ first converts the @Type@ +to an @IfaceType@. See Note [IfaceType and pretty-printing] in IfaceType. + +See Note [Precedence in types] in BasicTypes. +-} + +-------------------------------------------------------- +-- When pretty-printing types, we convert to IfaceType, +-- and pretty-print that. +-- See Note [Pretty printing via IfaceSyn] in PprTyThing +-------------------------------------------------------- + +pprType, pprParendType :: Type -> SDoc +pprType = pprPrecType topPrec +pprParendType = pprPrecType appPrec + +pprPrecType :: PprPrec -> Type -> SDoc +pprPrecType = pprPrecTypeX emptyTidyEnv + +pprPrecTypeX :: TidyEnv -> PprPrec -> Type -> SDoc +pprPrecTypeX env prec ty + = getPprStyle $ \sty -> + if debugStyle sty -- Use debugPprType when in + then debug_ppr_ty prec ty -- when in debug-style + else pprPrecIfaceType prec (tidyToIfaceTypeStyX env ty sty) + -- NB: debug-style is used for -dppr-debug + -- dump-style is used for -ddump-tc-trace etc + +pprTyLit :: TyLit -> SDoc +pprTyLit = pprIfaceTyLit . toIfaceTyLit + +pprKind, pprParendKind :: Kind -> SDoc +pprKind = pprType +pprParendKind = pprParendType + +tidyToIfaceTypeStyX :: TidyEnv -> Type -> PprStyle -> IfaceType +tidyToIfaceTypeStyX env ty sty + | userStyle sty = tidyToIfaceTypeX env ty + | otherwise = toIfaceTypeX (tyCoVarsOfType ty) ty + -- in latter case, don't tidy, as we'll be printing uniques. + +tidyToIfaceType :: Type -> IfaceType +tidyToIfaceType = tidyToIfaceTypeX emptyTidyEnv + +tidyToIfaceTypeX :: TidyEnv -> Type -> IfaceType +-- It's vital to tidy before converting to an IfaceType +-- or nested binders will become indistinguishable! +-- +-- Also for the free type variables, tell toIfaceTypeX to +-- leave them as IfaceFreeTyVar. This is super-important +-- for debug printing. +tidyToIfaceTypeX env ty = toIfaceTypeX (mkVarSet free_tcvs) (tidyType env' ty) + where + env' = tidyFreeTyCoVars env free_tcvs + free_tcvs = tyCoVarsOfTypeWellScoped ty + +------------ +pprCo, pprParendCo :: Coercion -> SDoc +pprCo co = getPprStyle $ \ sty -> pprIfaceCoercion (tidyToIfaceCoSty co sty) +pprParendCo co = getPprStyle $ \ sty -> pprParendIfaceCoercion (tidyToIfaceCoSty co sty) + +tidyToIfaceCoSty :: Coercion -> PprStyle -> IfaceCoercion +tidyToIfaceCoSty co sty + | userStyle sty = tidyToIfaceCo co + | otherwise = toIfaceCoercionX (tyCoVarsOfCo co) co + -- in latter case, don't tidy, as we'll be printing uniques. + +tidyToIfaceCo :: Coercion -> IfaceCoercion +-- It's vital to tidy before converting to an IfaceType +-- or nested binders will become indistinguishable! +-- +-- Also for the free type variables, tell toIfaceCoercionX to +-- leave them as IfaceFreeCoVar. This is super-important +-- for debug printing. +tidyToIfaceCo co = toIfaceCoercionX (mkVarSet free_tcvs) (tidyCo env co) + where + env = tidyFreeTyCoVars emptyTidyEnv free_tcvs + free_tcvs = scopedSort $ tyCoVarsOfCoList co +------------ +pprClassPred :: Class -> [Type] -> SDoc +pprClassPred clas tys = pprTypeApp (classTyCon clas) tys + +------------ +pprTheta :: ThetaType -> SDoc +pprTheta = pprIfaceContext topPrec . map tidyToIfaceType + +pprParendTheta :: ThetaType -> SDoc +pprParendTheta = pprIfaceContext appPrec . map tidyToIfaceType + +pprThetaArrowTy :: ThetaType -> SDoc +pprThetaArrowTy = pprIfaceContextArr . map tidyToIfaceType + +------------------ +pprSigmaType :: Type -> SDoc +pprSigmaType = pprIfaceSigmaType ShowForAllWhen . tidyToIfaceType + +pprForAll :: [TyCoVarBinder] -> SDoc +pprForAll tvs = pprIfaceForAll (map toIfaceForAllBndr tvs) + +-- | Print a user-level forall; see Note [When to print foralls] in this module. +pprUserForAll :: [TyCoVarBinder] -> SDoc +pprUserForAll = pprUserIfaceForAll . map toIfaceForAllBndr + +pprTCvBndrs :: [TyCoVarBinder] -> SDoc +pprTCvBndrs tvs = sep (map pprTCvBndr tvs) + +pprTCvBndr :: TyCoVarBinder -> SDoc +pprTCvBndr = pprTyVar . binderVar + +pprTyVars :: [TyVar] -> SDoc +pprTyVars tvs = sep (map pprTyVar tvs) + +pprTyVar :: TyVar -> SDoc +-- Print a type variable binder with its kind (but not if *) +-- Here we do not go via IfaceType, because the duplication with +-- pprIfaceTvBndr is minimal, and the loss of uniques etc in +-- debug printing is disastrous +pprTyVar tv + | isLiftedTypeKind kind = ppr tv + | otherwise = parens (ppr tv <+> dcolon <+> ppr kind) + where + kind = tyVarKind tv + +----------------- +debugPprType :: Type -> SDoc +-- ^ debugPprType is a simple pretty printer that prints a type +-- without going through IfaceType. It does not format as prettily +-- as the normal route, but it's much more direct, and that can +-- be useful for debugging. E.g. with -dppr-debug it prints the +-- kind on type-variable /occurrences/ which the normal route +-- fundamentally cannot do. +debugPprType ty = debug_ppr_ty topPrec ty + +debug_ppr_ty :: PprPrec -> Type -> SDoc +debug_ppr_ty _ (LitTy l) + = ppr l + +debug_ppr_ty _ (TyVarTy tv) + = ppr tv -- With -dppr-debug we get (tv :: kind) + +debug_ppr_ty prec (FunTy { ft_af = af, ft_arg = arg, ft_res = res }) + = maybeParen prec funPrec $ + sep [debug_ppr_ty funPrec arg, arrow <+> debug_ppr_ty prec res] + where + arrow = case af of + VisArg -> text "->" + InvisArg -> text "=>" + +debug_ppr_ty prec (TyConApp tc tys) + | null tys = ppr tc + | otherwise = maybeParen prec appPrec $ + hang (ppr tc) 2 (sep (map (debug_ppr_ty appPrec) tys)) + +debug_ppr_ty _ (AppTy t1 t2) + = hang (debug_ppr_ty appPrec t1) -- Print parens so we see ((a b) c) + 2 (debug_ppr_ty appPrec t2) -- so that we can distinguish + -- TyConApp from AppTy + +debug_ppr_ty prec (CastTy ty co) + = maybeParen prec topPrec $ + hang (debug_ppr_ty topPrec ty) + 2 (text "|>" <+> ppr co) + +debug_ppr_ty _ (CoercionTy co) + = parens (text "CO" <+> ppr co) + +debug_ppr_ty prec ty@(ForAllTy {}) + | (tvs, body) <- split ty + = maybeParen prec funPrec $ + hang (text "forall" <+> fsep (map ppr tvs) <> dot) + -- The (map ppr tvs) will print kind-annotated + -- tvs, because we are (usually) in debug-style + 2 (ppr body) + where + split ty | ForAllTy tv ty' <- ty + , (tvs, body) <- split ty' + = (tv:tvs, body) + | otherwise + = ([], ty) + +{- +Note [When to print foralls] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Mostly we want to print top-level foralls when (and only when) the user specifies +-fprint-explicit-foralls. But when kind polymorphism is at work, that suppresses +too much information; see #9018. + +So I'm trying out this rule: print explicit foralls if + a) User specifies -fprint-explicit-foralls, or + b) Any of the quantified type variables has a kind + that mentions a kind variable + +This catches common situations, such as a type siguature + f :: m a +which means + f :: forall k. forall (m :: k->*) (a :: k). m a +We really want to see both the "forall k" and the kind signatures +on m and a. The latter comes from pprTCvBndr. + +Note [Infix type variables] +~~~~~~~~~~~~~~~~~~~~~~~~~~~ +With TypeOperators you can say + + f :: (a ~> b) -> b + +and the (~>) is considered a type variable. However, the type +pretty-printer in this module will just see (a ~> b) as + + App (App (TyVarTy "~>") (TyVarTy "a")) (TyVarTy "b") + +So it'll print the type in prefix form. To avoid confusion we must +remember to parenthesise the operator, thus + + (~>) a b -> b + +See #2766. +-} + +pprDataCons :: TyCon -> SDoc +pprDataCons = sepWithVBars . fmap pprDataConWithArgs . tyConDataCons + where + sepWithVBars [] = empty + sepWithVBars docs = sep (punctuate (space <> vbar) docs) + +pprDataConWithArgs :: DataCon -> SDoc +pprDataConWithArgs dc = sep [forAllDoc, thetaDoc, ppr dc <+> argsDoc] + where + (_univ_tvs, _ex_tvs, _eq_spec, theta, arg_tys, _res_ty) = dataConFullSig dc + user_bndrs = dataConUserTyVarBinders dc + forAllDoc = pprUserForAll user_bndrs + thetaDoc = pprThetaArrowTy theta + argsDoc = hsep (fmap pprParendType arg_tys) + + +pprTypeApp :: TyCon -> [Type] -> SDoc +pprTypeApp tc tys + = pprIfaceTypeApp topPrec (toIfaceTyCon tc) + (toIfaceTcArgs tc tys) + -- TODO: toIfaceTcArgs seems rather wasteful here + +------------------ +-- | Display all kind information (with @-fprint-explicit-kinds@) when the +-- provided 'Bool' argument is 'True'. +-- See @Note [Kind arguments in error messages]@ in "TcErrors". +pprWithExplicitKindsWhen :: Bool -> SDoc -> SDoc +pprWithExplicitKindsWhen b + = updSDocDynFlags $ \dflags -> + if b then gopt_set dflags Opt_PrintExplicitKinds + else dflags + diff --git a/compiler/types/TyCoPpr.hs-boot b/compiler/types/TyCoPpr.hs-boot new file mode 100644 index 0000000000..127dfb32d8 --- /dev/null +++ b/compiler/types/TyCoPpr.hs-boot @@ -0,0 +1,10 @@ +module TyCoPpr where + +import {-# SOURCE #-} TyCoRep (Type, Kind, Coercion, TyLit) +import Outputable + +pprType :: Type -> SDoc +pprKind :: Kind -> SDoc +pprCo :: Coercion -> SDoc +pprTyLit :: TyLit -> SDoc + diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs index 1f2f8c6724..51ad630372 100644 --- a/compiler/types/TyCoRep.hs +++ b/compiler/types/TyCoRep.hs @@ -9,6 +9,10 @@ Note [The Type-related module hierarchy] CoAxiom TyCon imports Class, CoAxiom TyCoRep imports Class, CoAxiom, TyCon + TyCoPpr imports TyCoRep + TyCoFVs imports TyCoRep + TyCoSubst imports TyCoRep, TyCoFVs, TyCoPpr + TyCoTidy imports TyCoRep, TyCoFVs TysPrim imports TyCoRep ( including mkTyConTy ) Kind imports TysPrim ( mainly for primitive kinds ) Type imports Kind @@ -65,88 +69,6 @@ module TyCoRep ( -- * Functions over coercions pickLR, - -- * Pretty-printing - pprType, pprParendType, pprPrecType, pprPrecTypeX, - pprTypeApp, pprTCvBndr, pprTCvBndrs, - pprSigmaType, - pprTheta, pprParendTheta, pprForAll, pprUserForAll, - pprTyVar, pprTyVars, - pprThetaArrowTy, pprClassPred, - pprKind, pprParendKind, pprTyLit, - PprPrec(..), topPrec, sigPrec, opPrec, funPrec, appPrec, maybeParen, - pprDataCons, pprWithExplicitKindsWhen, - - pprCo, pprParendCo, - - debugPprType, - - -- * Free variables - tyCoVarsOfType, tyCoVarsOfTypeDSet, tyCoVarsOfTypes, tyCoVarsOfTypesDSet, - tyCoFVsBndr, tyCoFVsVarBndr, tyCoFVsVarBndrs, - tyCoFVsOfType, tyCoVarsOfTypeList, - tyCoFVsOfTypes, tyCoVarsOfTypesList, - coVarsOfType, coVarsOfTypes, - coVarsOfCo, coVarsOfCos, - tyCoVarsOfCo, tyCoVarsOfCos, - tyCoVarsOfCoDSet, - tyCoFVsOfCo, tyCoFVsOfCos, - tyCoVarsOfCoList, tyCoVarsOfProv, - almostDevoidCoVarOfCo, - injectiveVarsOfType, tyConAppNeedsKindSig, - - noFreeVarsOfType, noFreeVarsOfCo, - - -- * Substitutions - TCvSubst(..), TvSubstEnv, CvSubstEnv, - emptyTvSubstEnv, emptyCvSubstEnv, composeTCvSubstEnv, composeTCvSubst, - emptyTCvSubst, mkEmptyTCvSubst, isEmptyTCvSubst, - mkTCvSubst, mkTvSubst, mkCvSubst, - getTvSubstEnv, - getCvSubstEnv, getTCvInScope, getTCvSubstRangeFVs, - isInScope, notElemTCvSubst, - setTvSubstEnv, setCvSubstEnv, zapTCvSubst, - extendTCvInScope, extendTCvInScopeList, extendTCvInScopeSet, - extendTCvSubst, extendTCvSubstWithClone, - extendCvSubst, extendCvSubstWithClone, - extendTvSubst, extendTvSubstBinderAndInScope, extendTvSubstWithClone, - extendTvSubstList, extendTvSubstAndInScope, - extendTCvSubstList, - unionTCvSubst, zipTyEnv, zipCoEnv, mkTyCoInScopeSet, - zipTvSubst, zipCvSubst, - zipTCvSubst, - mkTvSubstPrs, - - substTyWith, substTyWithCoVars, substTysWith, substTysWithCoVars, - substCoWith, - substTy, substTyAddInScope, - substTyUnchecked, substTysUnchecked, substThetaUnchecked, - substTyWithUnchecked, - substCoUnchecked, substCoWithUnchecked, - substTyWithInScope, - substTys, substTheta, - lookupTyVar, - substCo, substCos, substCoVar, substCoVars, lookupCoVar, - cloneTyVarBndr, cloneTyVarBndrs, - substVarBndr, substVarBndrs, - substTyVarBndr, substTyVarBndrs, - substCoVarBndr, - substTyVar, substTyVars, substTyCoVars, - substForAllCoBndr, - substVarBndrUsing, substForAllCoBndrUsing, - checkValidSubst, isValidTCvSubst, - - -- * Tidying type related things up for printing - tidyType, tidyTypes, - tidyOpenType, tidyOpenTypes, - tidyOpenKind, - tidyVarBndr, tidyVarBndrs, tidyFreeTyCoVars, avoidNameClashes, - tidyOpenTyCoVar, tidyOpenTyCoVars, - tidyTyCoVarOcc, - tidyTopType, - tidyKind, - tidyCo, tidyCos, - tidyTyCoVarBinder, tidyTyCoVarBinders, - -- * Sizes typeSize, coercionSize, provSize ) where @@ -155,48 +77,30 @@ module TyCoRep ( import GhcPrelude -import {-# SOURCE #-} DataCon( dataConFullSig - , dataConUserTyVarBinders - , DataCon ) -import {-# SOURCE #-} Type( isCoercionTy, mkAppTy, mkCastTy - , tyCoVarsOfTypeWellScoped - , tyCoVarsOfTypesWellScoped - , scopedSort - , coreView ) +import {-# SOURCE #-} Type( coreView ) +import {-# SOURCE #-} TyCoPpr ( pprType, pprCo, pprTyLit ) + -- Transitively pulls in a LOT of stuff, better to break the loop -import {-# SOURCE #-} Coercion import {-# SOURCE #-} ConLike ( ConLike(..), conLikeName ) -import {-# SOURCE #-} ToIface( toIfaceTypeX, toIfaceTyLit, toIfaceForAllBndr - , toIfaceTyCon, toIfaceTcArgs, toIfaceCoercionX ) -- friends: import IfaceType import Var -import VarEnv import VarSet import Name hiding ( varName ) import TyCon -import Class import CoAxiom -import FV -- others -import BasicTypes ( LeftOrRight(..), PprPrec(..), topPrec, sigPrec, opPrec - , funPrec, appPrec, maybeParen, pickLR ) +import BasicTypes ( LeftOrRight(..), pickLR ) import PrelNames import Outputable -import DynFlags import FastString -import Pair -import UniqSupply import Util -import UniqFM -import UniqSet -- libraries import qualified Data.Data as Data hiding ( TyCon ) -import Data.List import Data.IORef ( IORef ) -- for CoercionHole {- @@ -333,6 +237,9 @@ data Type deriving Data.Data +instance Outputable Type where + ppr = pprType + -- NOTE: Other parts of the code assume that type literals do not contain -- types or type variables. data TyLit @@ -340,6 +247,8 @@ data TyLit | StrTyLit FastString deriving (Eq, Ord, Data.Data) +instance Outputable TyLit where + ppr = pprTyLit {- Note [Function types] ~~~~~~~~~~~~~~~~~~~~~~~~ @@ -727,6 +636,13 @@ data TyCoBinder -- Visibility is determined by the AnonArgFlag deriving Data.Data +instance Outputable TyCoBinder where + ppr (Anon af ty) = ppr af <+> ppr ty + ppr (Named (Bndr v Required)) = ppr v + ppr (Named (Bndr v Specified)) = char '@' <> ppr v + ppr (Named (Bndr v Inferred)) = braces (ppr v) + + -- | 'TyBinder' is like 'TyCoBinder', but there can only be 'TyVarBinder' -- in the 'Named' field. type TyBinder = TyCoBinder @@ -1246,6 +1162,9 @@ type CoercionR = Coercion -- always representational type CoercionP = Coercion -- always phantom type KindCoercion = CoercionN -- always nominal +instance Outputable Coercion where + ppr = pprCo + -- | A semantically more meaningful type to represent what may or may not be a -- useful 'Coercion'. data MCoercion @@ -1798,2293 +1717,8 @@ Here, where co5 :: (a1 ~ Bool) ~ (a2 ~ Bool) co5 = TyConAppCo Nominal (~#) [<*>, <*>, co4, <Bool>] - - -%************************************************************************ -%* * - Free variables of types and coercions -%* * -%************************************************************************ --} - -{- Note [Free variables of types] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -The family of functions tyCoVarsOfType, tyCoVarsOfTypes etc, returns -a VarSet that is closed over the types of its variables. More precisely, - if S = tyCoVarsOfType( t ) - and (a:k) is in S - then tyCoVarsOftype( k ) is a subset of S - -Example: The tyCoVars of this ((a:* -> k) Int) is {a, k}. - -We could /not/ close over the kinds of the variable occurrences, and -instead do so at call sites, but it seems that we always want to do -so, so it's easiest to do it here. - -It turns out that getting the free variables of types is performance critical, -so we profiled several versions, exploring different implementation strategies. - -1. Baseline version: uses FV naively. Essentially: - - tyCoVarsOfType ty = fvVarSet $ tyCoFVsOfType ty - - This is not nice, because FV introduces some overhead to implement - determinism, and throught its "interesting var" function, neither of which - we need here, so they are a complete waste. - -2. UnionVarSet version: instead of reusing the FV-based code, we simply used - VarSets directly, trying to avoid the overhead of FV. E.g.: - - -- FV version: - tyCoFVsOfType (AppTy fun arg) a b c = (tyCoFVsOfType fun `unionFV` tyCoFVsOfType arg) a b c - - -- UnionVarSet version: - tyCoVarsOfType (AppTy fun arg) = (tyCoVarsOfType fun `unionVarSet` tyCoVarsOfType arg) - - This looks deceptively similar, but while FV internally builds a list- and - set-generating function, the VarSet functions manipulate sets directly, and - the latter peforms a lot worse than the naive FV version. - -3. Accumulator-style VarSet version: this is what we use now. We do use VarSet - as our data structure, but delegate the actual work to a new - ty_co_vars_of_... family of functions, which use accumulator style and the - "in-scope set" filter found in the internals of FV, but without the - determinism overhead. - -See #14880. - -Note [Closing over free variable kinds] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -tyCoVarsOfType and tyCoFVsOfType, while traversing a type, will also close over -free variable kinds. In previous GHC versions, this happened naively: whenever -we would encounter an occurrence of a free type variable, we would close over -its kind. This, however is wrong for two reasons (see #14880): - -1. Efficiency. If we have Proxy (a::k) -> Proxy (a::k) -> Proxy (a::k), then - we don't want to have to traverse k more than once. - -2. Correctness. Imagine we have forall k. b -> k, where b has - kind k, for some k bound in an outer scope. If we look at b's kind inside - the forall, we'll collect that k is free and then remove k from the set of - free variables. This is plain wrong. We must instead compute that b is free - and then conclude that b's kind is free. - -An obvious first approach is to move the closing-over-kinds from the -occurrences of a type variable to after finding the free vars - however, this -turns out to introduce performance regressions, and isn't even entirely -correct. - -In fact, it isn't even important *when* we close over kinds; what matters is -that we handle each type var exactly once, and that we do it in the right -context. - -So the next approach we tried was to use the "in-scope set" part of FV or the -equivalent argument in the accumulator-style `ty_co_vars_of_type` function, to -say "don't bother with variables we have already closed over". This should work -fine in theory, but the code is complicated and doesn't perform well. - -But there is a simpler way, which is implemented here. Consider the two points -above: - -1. Efficiency: we now have an accumulator, so the second time we encounter 'a', - we'll ignore it, certainly not looking at its kind - this is why - pre-checking set membership before inserting ends up not only being faster, - but also being correct. - -2. Correctness: we have an "in-scope set" (I think we should call it it a - "bound-var set"), specifying variables that are bound by a forall in the type - we are traversing; we simply ignore these variables, certainly not looking at - their kind. - -So now consider: - - forall k. b -> k - -where b :: k->Type is free; but of course, it's a different k! When looking at -b -> k we'll have k in the bound-var set. So we'll ignore the k. But suppose -this is our first encounter with b; we want the free vars of its kind. But we -want to behave as if we took the free vars of its kind at the end; that is, -with no bound vars in scope. - -So the solution is easy. The old code was this: - - 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) - -Now all we need to do is take the free vars of tyVarKind v *with an empty -bound-var set*, thus: - -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 (extendVarSet acc v) - ^^^^^^^^^^^ - -And that's it. - --} - -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) - 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) - -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 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) - --- | `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. -tyCoVarsOfTypeDSet :: Type -> DTyCoVarSet --- See Note [Free variables of types] -tyCoVarsOfTypeDSet ty = fvDVarSet $ tyCoFVsOfType ty - --- | `tyCoFVsOfType` that returns free variables of a type in deterministic --- order. For explanation of why using `VarSet` is not deterministic see --- Note [Deterministic FV] in FV. -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. --- It's exported, so that it can be composed with --- other functions that compute free variables. --- See Note [FV naming conventions] in FV. --- --- Eta-expanded because that makes it run faster (apparently) --- See Note [FV eta expansion] in FV for explanation. -tyCoFVsOfType :: Type -> FV --- See Note [Free variables of types] -tyCoFVsOfType (TyVarTy v) f bound_vars (acc_list, acc_set) - | not (f v) = (acc_list, acc_set) - | v `elemVarSet` bound_vars = (acc_list, acc_set) - | v `elemVarSet` acc_set = (acc_list, acc_set) - | otherwise = tyCoFVsOfType (tyVarKind v) f - emptyVarSet -- See Note [Closing over free variable kinds] - (v:acc_list, extendVarSet acc_set v) -tyCoFVsOfType (TyConApp _ tys) f bound_vars acc = tyCoFVsOfTypes tys f bound_vars acc -tyCoFVsOfType (LitTy {}) f bound_vars acc = emptyFV f bound_vars acc -tyCoFVsOfType (AppTy fun arg) f bound_vars acc = (tyCoFVsOfType fun `unionFV` tyCoFVsOfType arg) f bound_vars acc -tyCoFVsOfType (FunTy _ arg res) f bound_vars acc = (tyCoFVsOfType arg `unionFV` tyCoFVsOfType res) f bound_vars acc -tyCoFVsOfType (ForAllTy bndr ty) f bound_vars acc = tyCoFVsBndr bndr (tyCoFVsOfType ty) f bound_vars acc -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 --- Free vars of (forall b. <thing with fvs>) -tyCoFVsBndr (Bndr tv _) fvs = tyCoFVsVarBndr tv fvs - -tyCoFVsVarBndrs :: [Var] -> FV -> FV -tyCoFVsVarBndrs vars fvs = foldr tyCoFVsVarBndr fvs vars - -tyCoFVsVarBndr :: Var -> FV -> FV -tyCoFVsVarBndr var fvs - = tyCoFVsOfType (varType var) -- Free vars of its type/kind - `unionFV` delFV var fvs -- Delete it from the thing-inside - -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 - --- | Get a deterministic set of the vars free in a coercion -tyCoVarsOfCoDSet :: Coercion -> DTyCoVarSet --- See Note [Free variables of types] -tyCoVarsOfCoDSet co = fvDVarSet $ tyCoFVsOfCo co - -tyCoVarsOfCoList :: Coercion -> [TyCoVar] --- See Note [Free variables of types] -tyCoVarsOfCoList co = fvVarList $ tyCoFVsOfCo co - -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] -tyCoFVsOfCo (Refl ty) fv_cand in_scope acc - = tyCoFVsOfType ty fv_cand in_scope acc -tyCoFVsOfCo (GRefl _ ty mco) fv_cand in_scope acc - = (tyCoFVsOfType ty `unionFV` tyCoFVsOfMCo mco) fv_cand in_scope acc -tyCoFVsOfCo (TyConAppCo _ _ cos) fv_cand in_scope acc = tyCoFVsOfCos cos fv_cand in_scope acc -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 _ co1 co2) fv_cand in_scope acc - = (tyCoFVsOfCo co1 `unionFV` tyCoFVsOfCo co2) fv_cand in_scope acc -tyCoFVsOfCo (CoVarCo v) fv_cand in_scope acc - = tyCoFVsOfCoVar v fv_cand in_scope acc -tyCoFVsOfCo (HoleCo h) fv_cand in_scope acc - = tyCoFVsOfCoVar (coHoleCoVar h) fv_cand in_scope acc - -- See Note [CoercionHoles and coercion free variables] -tyCoFVsOfCo (AxiomInstCo _ _ cos) fv_cand in_scope acc = tyCoFVsOfCos cos fv_cand in_scope acc -tyCoFVsOfCo (UnivCo p _ t1 t2) fv_cand in_scope acc - = (tyCoFVsOfProv p `unionFV` tyCoFVsOfType t1 - `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 (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 -tyCoFVsOfCo (SubCo co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc -tyCoFVsOfCo (AxiomRuleCo _ cs) fv_cand in_scope acc = tyCoFVsOfCos cs fv_cand in_scope acc - -tyCoFVsOfCoVar :: CoVar -> FV -tyCoFVsOfCoVar v fv_cand in_scope acc - = (unitFV v `unionFV` tyCoFVsOfType (varType v)) fv_cand in_scope acc - -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 - -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 ----------- - -{- - -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 -considerations outlined in Note [Free variables of types]. - -This is because FV includes the InterestingVarFun, which is useful here, -because we can cleverly use it to restrict our calculations to CoVars - this -is what getCoVarSet achieves. - -See #14880. - --} - -getCoVarSet :: FV -> CoVarSet -getCoVarSet fv = snd (fv isCoVar emptyVarSet ([], emptyVarSet)) - -coVarsOfType :: Type -> CoVarSet -coVarsOfType ty = getCoVarSet (tyCoFVsOfType ty) - -coVarsOfTypes :: [Type] -> TyCoVarSet -coVarsOfTypes tys = getCoVarSet (tyCoFVsOfTypes tys) - -coVarsOfCo :: Coercion -> CoVarSet -coVarsOfCo co = getCoVarSet (tyCoFVsOfCo co) - -coVarsOfCos :: [Coercion] -> CoVarSet -coVarsOfCos cos = getCoVarSet (tyCoFVsOfCos cos) - ------ Whether a covar is /Almost Devoid/ in a type or coercion ---- - --- | Given a covar and a coercion, returns True if covar is almost devoid in --- the coercion. That is, covar can only appear in Refl and GRefl. --- See last wrinkle in Note [Unused coercion variable in ForAllCo] in Coercion -almostDevoidCoVarOfCo :: CoVar -> Coercion -> Bool -almostDevoidCoVarOfCo cv co = - almost_devoid_co_var_of_co co cv - -almost_devoid_co_var_of_co :: Coercion -> CoVar -> Bool -almost_devoid_co_var_of_co (Refl {}) _ = True -- covar is allowed in Refl and -almost_devoid_co_var_of_co (GRefl {}) _ = True -- GRefl, so we don't look into - -- the coercions -almost_devoid_co_var_of_co (TyConAppCo _ _ cos) cv - = almost_devoid_co_var_of_cos cos cv -almost_devoid_co_var_of_co (AppCo co arg) cv - = almost_devoid_co_var_of_co co cv - && almost_devoid_co_var_of_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 _ 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 (CoVarCo v) cv = v /= cv -almost_devoid_co_var_of_co (HoleCo h) cv = (coHoleCoVar h) /= cv -almost_devoid_co_var_of_co (AxiomInstCo _ _ cos) cv - = almost_devoid_co_var_of_cos cos cv -almost_devoid_co_var_of_co (UnivCo p _ t1 t2) cv - = almost_devoid_co_var_of_prov p cv - && almost_devoid_co_var_of_type t1 cv - && almost_devoid_co_var_of_type t2 cv -almost_devoid_co_var_of_co (SymCo co) cv - = almost_devoid_co_var_of_co 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 co cv -almost_devoid_co_var_of_co (LRCo _ co) cv - = almost_devoid_co_var_of_co co cv -almost_devoid_co_var_of_co (InstCo co arg) cv - = almost_devoid_co_var_of_co co cv - && almost_devoid_co_var_of_co arg cv -almost_devoid_co_var_of_co (KindCo co) cv - = almost_devoid_co_var_of_co co cv -almost_devoid_co_var_of_co (SubCo co) cv - = almost_devoid_co_var_of_co co cv -almost_devoid_co_var_of_co (AxiomRuleCo _ cs) cv - = almost_devoid_co_var_of_cos cs cv - -almost_devoid_co_var_of_cos :: [Coercion] -> CoVar -> Bool -almost_devoid_co_var_of_cos [] _ = True -almost_devoid_co_var_of_cos (co:cos) cv - = almost_devoid_co_var_of_co co cv - && almost_devoid_co_var_of_cos cos cv - -almost_devoid_co_var_of_prov :: UnivCoProvenance -> CoVar -> Bool -almost_devoid_co_var_of_prov (PhantomProv co) cv - = almost_devoid_co_var_of_co co cv -almost_devoid_co_var_of_prov (ProofIrrelProv co) cv - = almost_devoid_co_var_of_co co cv -almost_devoid_co_var_of_prov UnsafeCoerceProv _ = True -almost_devoid_co_var_of_prov (PluginProv _) _ = True - -almost_devoid_co_var_of_type :: Type -> CoVar -> Bool -almost_devoid_co_var_of_type (TyVarTy _) _ = True -almost_devoid_co_var_of_type (TyConApp _ tys) cv - = almost_devoid_co_var_of_types tys cv -almost_devoid_co_var_of_type (LitTy {}) _ = True -almost_devoid_co_var_of_type (AppTy fun arg) cv - = almost_devoid_co_var_of_type fun cv - && almost_devoid_co_var_of_type arg cv -almost_devoid_co_var_of_type (FunTy _ arg res) cv - = almost_devoid_co_var_of_type arg cv - && almost_devoid_co_var_of_type res cv -almost_devoid_co_var_of_type (ForAllTy (Bndr v _) ty) cv - = almost_devoid_co_var_of_type (varType v) cv - && (v == cv || almost_devoid_co_var_of_type ty cv) -almost_devoid_co_var_of_type (CastTy ty co) cv - = almost_devoid_co_var_of_type ty cv - && almost_devoid_co_var_of_co co cv -almost_devoid_co_var_of_type (CoercionTy co) cv - = almost_devoid_co_var_of_co co cv - -almost_devoid_co_var_of_types :: [Type] -> CoVar -> Bool -almost_devoid_co_var_of_types [] _ = True -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 ----------------- - --- | Returns the free variables of a 'Type' that are in injective positions. --- For example, if @F@ is a non-injective type family, then: --- --- @ --- injectiveTyVarsOf( Either c (Maybe (a, F b c)) ) = {a,c} --- @ --- --- If @'injectiveVarsOfType' ty = itvs@, then knowing @ty@ fixes @itvs@. --- More formally, if --- @a@ is in @'injectiveVarsOfType' ty@ --- and @S1(ty) ~ S2(ty)@, --- then @S1(a) ~ S2(a)@, --- where @S1@ and @S2@ are arbitrary substitutions. --- --- See @Note [When does a tycon application need an explicit kind signature?]@. -injectiveVarsOfType :: Type -> FV -injectiveVarsOfType = go - where - go ty | Just ty' <- coreView ty - = go ty' - go (TyVarTy v) = unitFV v `unionFV` go (tyVarKind v) - go (AppTy f a) = go f `unionFV` go a - go (FunTy _ ty1 ty2) = go ty1 `unionFV` go ty2 - go (TyConApp tc tys) = - case tyConInjectivityInfo tc of - NotInjective -> emptyFV - Injective inj -> mapUnionFV go $ - filterByList (inj ++ repeat True) tys - -- Oversaturated arguments to a tycon are - -- always injective, hence the repeat True - go (ForAllTy tvb ty) = tyCoFVsBndr tvb $ go ty - go LitTy{} = emptyFV - go (CastTy ty _) = go ty - go CoercionTy{} = emptyFV - --- | Does a 'TyCon' (that is applied to some number of arguments) need to be --- ascribed with an explicit kind signature to resolve ambiguity if rendered as --- a source-syntax type? --- (See @Note [When does a tycon application need an explicit kind signature?]@ --- for a full explanation of what this function checks for.) - --- Morally, this function ought to belong in TyCon.hs, not TyCoRep.hs, but --- accomplishing this requires a fair deal of futzing aruond with .hs-boot --- files. -tyConAppNeedsKindSig - :: Bool -- ^ Should specified binders count towards injective positions in - -- the kind of the TyCon? (If you're using visible kind - -- applications, then you want True here. - -> TyCon - -> Int -- ^ The number of args the 'TyCon' is applied to. - -> Bool -- ^ Does @T t_1 ... t_n@ need a kind signature? (Where @n@ is the - -- number of arguments) -tyConAppNeedsKindSig spec_inj_pos tc n_args - | LT <- listLengthCmp tc_binders n_args - = False - | otherwise - = let (dropped_binders, remaining_binders) - = splitAt n_args tc_binders - result_kind = mkTyConKind remaining_binders tc_res_kind - result_vars = tyCoVarsOfType result_kind - dropped_vars = fvVarSet $ - mapUnionFV injective_vars_of_binder dropped_binders - - in not (subVarSet result_vars dropped_vars) - where - tc_binders = tyConBinders tc - tc_res_kind = tyConResKind tc - - -- Returns the variables that would be fixed by knowing a TyConBinder. See - -- Note [When does a tycon application need an explicit kind signature?] - -- for a more detailed explanation of what this function does. - injective_vars_of_binder :: TyConBinder -> FV - injective_vars_of_binder (Bndr tv vis) = - case vis of - AnonTCB VisArg -> injectiveVarsOfType (varType tv) - NamedTCB argf | source_of_injectivity argf - -> unitFV tv `unionFV` injectiveVarsOfType (varType tv) - _ -> emptyFV - - source_of_injectivity Required = True - source_of_injectivity Specified = spec_inj_pos - source_of_injectivity Inferred = False - -{- -Note [When does a tycon application need an explicit kind signature?] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -There are a couple of places in GHC where we convert Core Types into forms that -more closely resemble user-written syntax. These include: - -1. Template Haskell Type reification (see, for instance, TcSplice.reify_tc_app) -2. Converting Types to LHsTypes (in HsUtils.typeToLHsType, or in Haddock) - -This conversion presents a challenge: how do we ensure that the resulting type -has enough kind information so as not to be ambiguous? To better motivate this -question, consider the following Core type: - - -- Foo :: Type -> Type - type Foo = Proxy Type - -There is nothing ambiguous about the RHS of Foo in Core. But if we were to, -say, reify it into a TH Type, then it's tempting to just drop the invisible -Type argument and simply return `Proxy`. But now we've lost crucial kind -information: we don't know if we're dealing with `Proxy Type` or `Proxy Bool` -or `Proxy Int` or something else! We've inadvertently introduced ambiguity. - -Unlike in other situations in GHC, we can't just turn on --fprint-explicit-kinds, as we need to produce something which has the same -structure as a source-syntax type. Moreover, we can't rely on visible kind -application, since the first kind argument to Proxy is inferred, not specified. -Our solution is to annotate certain tycons with their kinds whenever they -appear in applied form in order to resolve the ambiguity. For instance, we -would reify the RHS of Foo like so: - - type Foo = (Proxy :: Type -> Type) - -We need to devise an algorithm that determines precisely which tycons need -these explicit kind signatures. We certainly don't want to annotate _every_ -tycon with a kind signature, or else we might end up with horribly bloated -types like the following: - - (Either :: Type -> Type -> Type) (Int :: Type) (Char :: Type) - -We only want to annotate tycons that absolutely require kind signatures in -order to resolve some sort of ambiguity, and nothing more. - -Suppose we have a tycon application (T ty_1 ... ty_n). Why might this type -require a kind signature? It might require it when we need to fill in any of -T's omitted arguments. By "omitted argument", we mean one that is dropped when -reifying ty_1 ... ty_n. Sometimes, the omitted arguments are inferred and -specified arguments (e.g., TH reification in TcSplice), and sometimes the -omitted arguments are only the inferred ones (e.g., in HsUtils.typeToLHsType, -which reifies specified arguments through visible kind application). -Regardless, the key idea is that _some_ arguments are going to be omitted after -reification, and the only mechanism we have at our disposal for filling them in -is through explicit kind signatures. - -What do we mean by "fill in"? Let's consider this small example: - - T :: forall {k}. Type -> (k -> Type) -> k - -Moreover, we have this application of T: - - T @{j} Int aty - -When we reify this type, we omit the inferred argument @{j}. Is it fixed by the -other (non-inferred) arguments? Yes! If we know the kind of (aty :: blah), then -we'll generate an equality constraint (kappa -> Type) and, assuming we can -solve it, that will fix `kappa`. (Here, `kappa` is the unification variable -that we instantiate `k` with.) - -Therefore, for any application of a tycon T to some arguments, the Question We -Must Answer is: - -* Given the first n arguments of T, do the kinds of the non-omitted arguments - fill in the omitted arguments? - -(This is still a bit hand-wavey, but we'll refine this question incrementally -as we explain more of the machinery underlying this process.) - -Answering this question is precisely the role that the `injectiveVarsOfType` -and `injective_vars_of_binder` functions exist to serve. If an omitted argument -`a` appears in the set returned by `injectiveVarsOfType ty`, then knowing -`ty` determines (i.e., fills in) `a`. (More on `injective_vars_of_binder` in a -bit.) - -More formally, if -`a` is in `injectiveVarsOfType ty` -and S1(ty) ~ S2(ty), -then S1(a) ~ S2(a), -where S1 and S2 are arbitrary substitutions. - -For example, is `F` is a non-injective type family, then - - injectiveVarsOfType(Either c (Maybe (a, F b c))) = {a, c} - -Now that we know what this function does, here is a second attempt at the -Question We Must Answer: - -* Given the first n arguments of T (ty_1 ... ty_n), consider the binders - of T that are instantiated by non-omitted arguments. Do the injective - variables of these binders fill in the remainder of T's kind? - -Alright, we're getting closer. Next, we need to clarify what the injective -variables of a tycon binder are. This the role that the -`injective_vars_of_binder` function serves. Here is what this function does for -each form of tycon binder: - -* Anonymous binders are injective positions. For example, in the promoted data - constructor '(:): - - '(:) :: forall a. a -> [a] -> [a] - - The second and third tyvar binders (of kinds `a` and `[a]`) are both - anonymous, so if we had '(:) 'True '[], then the kinds of 'True and - '[] would contribute to the kind of '(:) 'True '[]. Therefore, - injective_vars_of_binder(_ :: a) = injectiveVarsOfType(a) = {a}. - (Similarly, injective_vars_of_binder(_ :: [a]) = {a}.) -* Named binders: - - Inferred binders are never injective positions. For example, in this data - type: - - data Proxy a - Proxy :: forall {k}. k -> Type - - If we had Proxy 'True, then the kind of 'True would not contribute to the - kind of Proxy 'True. Therefore, - injective_vars_of_binder(forall {k}. ...) = {}. - - Required binders are injective positions. For example, in this data type: - - data Wurble k (a :: k) :: k - Wurble :: forall k -> k -> k - - The first tyvar binder (of kind `forall k`) has required visibility, so if - we had Wurble (Maybe a) Nothing, then the kind of Maybe a would - contribute to the kind of Wurble (Maybe a) Nothing. Hence, - injective_vars_of_binder(forall a -> ...) = {a}. - - Specified binders /might/ be injective positions, depending on how you - approach things. Continuing the '(:) example: - - '(:) :: forall a. a -> [a] -> [a] - - Normally, the (forall a. ...) tyvar binder wouldn't contribute to the kind - of '(:) 'True '[], since it's not explicitly instantiated by the user. But - if visible kind application is enabled, then this is possible, since the - user can write '(:) @Bool 'True '[]. (In that case, - injective_vars_of_binder(forall a. ...) = {a}.) - - There are some situations where using visible kind application is appropriate - (e.g., HsUtils.typeToLHsType) and others where it is not (e.g., TH - reification), so the `injective_vars_of_binder` function is parametrized by - a Bool which decides if specified binders should be counted towards - injective positions or not. - -Now that we've defined injective_vars_of_binder, we can refine the Question We -Must Answer once more: - -* Given the first n arguments of T (ty_1 ... ty_n), consider the binders - of T that are instantiated by non-omitted arguments. For each such binder - b_i, take the union of all injective_vars_of_binder(b_i). Is this set a - superset of the free variables of the remainder of T's kind? - -If the answer to this question is "no", then (T ty_1 ... ty_n) needs an -explicit kind signature, since T's kind has kind variables leftover that -aren't fixed by the non-omitted arguments. - -One last sticking point: what does "the remainder of T's kind" mean? You might -be tempted to think that it corresponds to all of the arguments in the kind of -T that would normally be instantiated by omitted arguments. But this isn't -quite right, strictly speaking. Consider the following (silly) example: - - S :: forall {k}. Type -> Type - -And suppose we have this application of S: - - S Int Bool - -The Int argument would be omitted, and -injective_vars_of_binder(_ :: Type) = {}. This is not a superset of {k}, which -might suggest that (S Bool) needs an explicit kind signature. But -(S Bool :: Type) doesn't actually fix `k`! This is because the kind signature -only affects the /result/ of the application, not all of the individual -arguments. So adding a kind signature here won't make a difference. Therefore, -the fourth (and final) iteration of the Question We Must Answer is: - -* Given the first n arguments of T (ty_1 ... ty_n), consider the binders - of T that are instantiated by non-omitted arguments. For each such binder - b_i, take the union of all injective_vars_of_binder(b_i). Is this set a - superset of the free variables of the kind of (T ty_1 ... ty_n)? - -Phew, that was a lot of work! - -How can be sure that this is correct? That is, how can we be sure that in the -event that we leave off a kind annotation, that one could infer the kind of the -tycon application from its arguments? It's essentially a proof by induction: if -we can infer the kinds of every subtree of a type, then the whole tycon -application will have an inferrable kind--unless, of course, the remainder of -the tycon application's kind has uninstantiated kind variables. - -What happens if T is oversaturated? That is, if T's kind has fewer than n -arguments, in the case that the concrete application instantiates a result -kind variable with an arrow kind? If we run out of arguments, we do not attach -a kind annotation. This should be a rare case, indeed. Here is an example: - - data T1 :: k1 -> k2 -> * - data T2 :: k1 -> k2 -> * - - type family G (a :: k) :: k - type instance G T1 = T2 - - type instance F Char = (G T1 Bool :: (* -> *) -> *) -- F from above - -Here G's kind is (forall k. k -> k), and the desugared RHS of that last -instance of F is (G (* -> (* -> *) -> *) (T1 * (* -> *)) Bool). According to -the algorithm above, there are 3 arguments to G so we should peel off 3 -arguments in G's kind. But G's kind has only two arguments. This is the -rare special case, and we choose not to annotate the application of G with -a kind signature. After all, we needn't do this, since that instance would -be reified as: - - type instance F Char = G (T1 :: * -> (* -> *) -> *) Bool - -So the kind of G isn't ambiguous anymore due to the explicit kind annotation -on its argument. See #8953 and test th/T8953. --} - -------------- 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 -noFreeVarsOfType (TyVarTy _) = False -noFreeVarsOfType (AppTy t1 t2) = noFreeVarsOfType t1 && noFreeVarsOfType t2 -noFreeVarsOfType (TyConApp _ tys) = all noFreeVarsOfType tys -noFreeVarsOfType ty@(ForAllTy {}) = isEmptyVarSet (tyCoVarsOfType ty) -noFreeVarsOfType (FunTy _ t1 t2) = noFreeVarsOfType t1 && noFreeVarsOfType t2 -noFreeVarsOfType (LitTy _) = True -noFreeVarsOfType (CastTy ty co) = noFreeVarsOfType ty && noFreeVarsOfCo co -noFreeVarsOfType (CoercionTy co) = noFreeVarsOfCo co - -noFreeVarsOfMCo :: MCoercion -> Bool -noFreeVarsOfMCo MRefl = True -noFreeVarsOfMCo (MCo co) = noFreeVarsOfCo co - -noFreeVarsOfTypes :: [Type] -> Bool -noFreeVarsOfTypes = all noFreeVarsOfType - --- | Returns True if this coercion has no free variables. Should be the same as --- isEmptyVarSet . tyCoVarsOfCo, but faster in the non-forall case. -noFreeVarsOfCo :: Coercion -> Bool -noFreeVarsOfCo (Refl ty) = noFreeVarsOfType ty -noFreeVarsOfCo (GRefl _ ty co) = noFreeVarsOfType ty && noFreeVarsOfMCo co -noFreeVarsOfCo (TyConAppCo _ _ args) = all noFreeVarsOfCo args -noFreeVarsOfCo (AppCo c1 c2) = noFreeVarsOfCo c1 && noFreeVarsOfCo c2 -noFreeVarsOfCo co@(ForAllCo {}) = isEmptyVarSet (tyCoVarsOfCo co) -noFreeVarsOfCo (FunCo _ c1 c2) = noFreeVarsOfCo c1 && noFreeVarsOfCo c2 -noFreeVarsOfCo (CoVarCo _) = False -noFreeVarsOfCo (HoleCo {}) = True -- I'm unsure; probably never happens -noFreeVarsOfCo (AxiomInstCo _ _ args) = all noFreeVarsOfCo args -noFreeVarsOfCo (UnivCo p _ t1 t2) = noFreeVarsOfProv p && - noFreeVarsOfType t1 && - noFreeVarsOfType t2 -noFreeVarsOfCo (SymCo co) = noFreeVarsOfCo co -noFreeVarsOfCo (TransCo co1 co2) = noFreeVarsOfCo co1 && noFreeVarsOfCo co2 -noFreeVarsOfCo (NthCo _ _ co) = noFreeVarsOfCo co -noFreeVarsOfCo (LRCo _ co) = noFreeVarsOfCo co -noFreeVarsOfCo (InstCo co1 co2) = noFreeVarsOfCo co1 && noFreeVarsOfCo co2 -noFreeVarsOfCo (KindCo co) = noFreeVarsOfCo co -noFreeVarsOfCo (SubCo co) = noFreeVarsOfCo co -noFreeVarsOfCo (AxiomRuleCo _ cs) = all noFreeVarsOfCo cs - --- | Returns True if this UnivCoProv has no free variables. Should be the same as --- isEmptyVarSet . tyCoVarsOfProv, but faster in the non-forall case. -noFreeVarsOfProv :: UnivCoProvenance -> Bool -noFreeVarsOfProv UnsafeCoerceProv = True -noFreeVarsOfProv (PhantomProv co) = noFreeVarsOfCo co -noFreeVarsOfProv (ProofIrrelProv co) = noFreeVarsOfCo co -noFreeVarsOfProv (PluginProv {}) = True - -{- -%************************************************************************ -%* * - Substitutions - Data type defined here to avoid unnecessary mutual recursion -%* * -%************************************************************************ --} - --- | Type & coercion substitution --- --- #tcvsubst_invariant# --- The following invariants must hold of a 'TCvSubst': --- --- 1. The in-scope set is needed /only/ to --- guide the generation of fresh uniques --- --- 2. In particular, the /kind/ of the type variables in --- the in-scope set is not relevant --- --- 3. The substitution is only applied ONCE! This is because --- in general such application will not reach a fixed point. -data TCvSubst - = TCvSubst InScopeSet -- The in-scope type and kind variables - TvSubstEnv -- Substitutes both type and kind variables - CvSubstEnv -- Substitutes coercion variables - -- See Note [Substitutions apply only once] - -- and Note [Extending the TvSubstEnv] - -- and Note [Substituting types and coercions] - -- and Note [The substitution invariant] - --- | A substitution of 'Type's for 'TyVar's --- and 'Kind's for 'KindVar's -type TvSubstEnv = TyVarEnv Type - -- NB: A TvSubstEnv is used - -- both inside a TCvSubst (with the apply-once invariant - -- discussed in Note [Substitutions apply only once], - -- and also independently in the middle of matching, - -- and unification (see Types.Unify). - -- So you have to look at the context to know if it's idempotent or - -- apply-once or whatever - --- | A substitution of 'Coercion's for 'CoVar's -type CvSubstEnv = CoVarEnv Coercion - -{- Note [The substitution invariant] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -When calling (substTy subst ty) it should be the case that -the in-scope set in the substitution is a superset of both: - - (SIa) The free vars of the range of the substitution - (SIb) The free vars of ty minus the domain of the substitution - -The same rules apply to other substitutions (notably CoreSubst.Subst) - -* Reason for (SIa). Consider - substTy [a :-> Maybe b] (forall b. b->a) - we must rename the forall b, to get - forall b2. b2 -> Maybe b - Making 'b' part of the in-scope set forces this renaming to - take place. - -* Reason for (SIb). Consider - substTy [a :-> Maybe b] (forall b. (a,b,x)) - Then if we use the in-scope set {b}, satisfying (SIa), there is - a danger we will rename the forall'd variable to 'x' by mistake, - getting this: - forall x. (Maybe b, x, x) - Breaking (SIb) caused the bug from #11371. - -Note: if the free vars of the range of the substitution are freshly created, -then the problems of (SIa) can't happen, and so it would be sound to -ignore (SIa). - -Note [Substitutions apply only once] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We use TCvSubsts to instantiate things, and we might instantiate - forall a b. ty -with the types - [a, b], or [b, a]. -So the substitution might go [a->b, b->a]. A similar situation arises in Core -when we find a beta redex like - (/\ a /\ b -> e) b a -Then we also end up with a substitution that permutes type variables. Other -variations happen to; for example [a -> (a, b)]. - - ******************************************************** - *** So a substitution must be applied precisely once *** - ******************************************************** - -A TCvSubst is not idempotent, but, unlike the non-idempotent substitution -we use during unifications, it must not be repeatedly applied. - -Note [Extending the TvSubstEnv] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -See #tcvsubst_invariant# for the invariants that must hold. - -This invariant allows a short-cut when the subst envs are empty: -if the TvSubstEnv and CvSubstEnv are empty --- i.e. (isEmptyTCvSubst subst) -holds --- then (substTy subst ty) does nothing. - -For example, consider: - (/\a. /\b:(a~Int). ...b..) Int -We substitute Int for 'a'. The Unique of 'b' does not change, but -nevertheless we add 'b' to the TvSubstEnv, because b's kind does change - -This invariant has several crucial consequences: - -* In substVarBndr, we need extend the TvSubstEnv - - if the unique has changed - - or if the kind has changed - -* In substTyVar, we do not need to consult the in-scope set; - the TvSubstEnv is enough - -* In substTy, substTheta, we can short-circuit when the TvSubstEnv is empty - -Note [Substituting types and coercions] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Types and coercions are mutually recursive, and either may have variables -"belonging" to the other. Thus, every time we wish to substitute in a -type, we may also need to substitute in a coercion, and vice versa. -However, the constructor used to create type variables is distinct from -that of coercion variables, so we carry two VarEnvs in a TCvSubst. Note -that it would be possible to use the CoercionTy constructor to combine -these environments, but that seems like a false economy. - -Note that the TvSubstEnv should *never* map a CoVar (built with the Id -constructor) and the CvSubstEnv should *never* map a TyVar. Furthermore, -the range of the TvSubstEnv should *never* include a type headed with -CoercionTy. --} - -emptyTvSubstEnv :: TvSubstEnv -emptyTvSubstEnv = emptyVarEnv - -emptyCvSubstEnv :: CvSubstEnv -emptyCvSubstEnv = emptyVarEnv - -composeTCvSubstEnv :: InScopeSet - -> (TvSubstEnv, CvSubstEnv) - -> (TvSubstEnv, CvSubstEnv) - -> (TvSubstEnv, CvSubstEnv) --- ^ @(compose env1 env2)(x)@ is @env1(env2(x))@; i.e. apply @env2@ then @env1@. --- It assumes that both are idempotent. --- Typically, @env1@ is the refinement to a base substitution @env2@ -composeTCvSubstEnv in_scope (tenv1, cenv1) (tenv2, cenv2) - = ( tenv1 `plusVarEnv` mapVarEnv (substTy subst1) tenv2 - , cenv1 `plusVarEnv` mapVarEnv (substCo subst1) cenv2 ) - -- First apply env1 to the range of env2 - -- Then combine the two, making sure that env1 loses if - -- both bind the same variable; that's why env1 is the - -- *left* argument to plusVarEnv, because the right arg wins - where - subst1 = TCvSubst in_scope tenv1 cenv1 - --- | Composes two substitutions, applying the second one provided first, --- like in function composition. -composeTCvSubst :: TCvSubst -> TCvSubst -> TCvSubst -composeTCvSubst (TCvSubst is1 tenv1 cenv1) (TCvSubst is2 tenv2 cenv2) - = TCvSubst is3 tenv3 cenv3 - where - is3 = is1 `unionInScope` is2 - (tenv3, cenv3) = composeTCvSubstEnv is3 (tenv1, cenv1) (tenv2, cenv2) - -emptyTCvSubst :: TCvSubst -emptyTCvSubst = TCvSubst emptyInScopeSet emptyTvSubstEnv emptyCvSubstEnv - -mkEmptyTCvSubst :: InScopeSet -> TCvSubst -mkEmptyTCvSubst is = TCvSubst is emptyTvSubstEnv emptyCvSubstEnv - -isEmptyTCvSubst :: TCvSubst -> Bool - -- See Note [Extending the TvSubstEnv] -isEmptyTCvSubst (TCvSubst _ tenv cenv) = isEmptyVarEnv tenv && isEmptyVarEnv cenv - -mkTCvSubst :: InScopeSet -> (TvSubstEnv, CvSubstEnv) -> TCvSubst -mkTCvSubst in_scope (tenv, cenv) = TCvSubst in_scope tenv cenv - -mkTvSubst :: InScopeSet -> TvSubstEnv -> TCvSubst --- ^ Make a TCvSubst with specified tyvar subst and empty covar subst -mkTvSubst in_scope tenv = TCvSubst in_scope tenv emptyCvSubstEnv - -mkCvSubst :: InScopeSet -> CvSubstEnv -> TCvSubst --- ^ Make a TCvSubst with specified covar subst and empty tyvar subst -mkCvSubst in_scope cenv = TCvSubst in_scope emptyTvSubstEnv cenv - -getTvSubstEnv :: TCvSubst -> TvSubstEnv -getTvSubstEnv (TCvSubst _ env _) = env - -getCvSubstEnv :: TCvSubst -> CvSubstEnv -getCvSubstEnv (TCvSubst _ _ env) = env - -getTCvInScope :: TCvSubst -> InScopeSet -getTCvInScope (TCvSubst in_scope _ _) = in_scope - --- | Returns the free variables of the types in the range of a substitution as --- a non-deterministic set. -getTCvSubstRangeFVs :: TCvSubst -> VarSet -getTCvSubstRangeFVs (TCvSubst _ tenv cenv) - = unionVarSet tenvFVs cenvFVs - where - tenvFVs = tyCoVarsOfTypesSet tenv - cenvFVs = tyCoVarsOfCosSet cenv - -isInScope :: Var -> TCvSubst -> Bool -isInScope v (TCvSubst in_scope _ _) = v `elemInScopeSet` in_scope - -notElemTCvSubst :: Var -> TCvSubst -> Bool -notElemTCvSubst v (TCvSubst _ tenv cenv) - | isTyVar v - = not (v `elemVarEnv` tenv) - | otherwise - = not (v `elemVarEnv` cenv) - -setTvSubstEnv :: TCvSubst -> TvSubstEnv -> TCvSubst -setTvSubstEnv (TCvSubst in_scope _ cenv) tenv = TCvSubst in_scope tenv cenv - -setCvSubstEnv :: TCvSubst -> CvSubstEnv -> TCvSubst -setCvSubstEnv (TCvSubst in_scope tenv _) cenv = TCvSubst in_scope tenv cenv - -zapTCvSubst :: TCvSubst -> TCvSubst -zapTCvSubst (TCvSubst in_scope _ _) = TCvSubst in_scope emptyVarEnv emptyVarEnv - -extendTCvInScope :: TCvSubst -> Var -> TCvSubst -extendTCvInScope (TCvSubst in_scope tenv cenv) var - = TCvSubst (extendInScopeSet in_scope var) tenv cenv - -extendTCvInScopeList :: TCvSubst -> [Var] -> TCvSubst -extendTCvInScopeList (TCvSubst in_scope tenv cenv) vars - = TCvSubst (extendInScopeSetList in_scope vars) tenv cenv - -extendTCvInScopeSet :: TCvSubst -> VarSet -> TCvSubst -extendTCvInScopeSet (TCvSubst in_scope tenv cenv) vars - = TCvSubst (extendInScopeSetSet in_scope vars) tenv cenv - -extendTCvSubst :: TCvSubst -> TyCoVar -> Type -> TCvSubst -extendTCvSubst subst v ty - | isTyVar v - = extendTvSubst subst v ty - | CoercionTy co <- ty - = extendCvSubst subst v co - | otherwise - = pprPanic "extendTCvSubst" (ppr v <+> text "|->" <+> ppr ty) - -extendTCvSubstWithClone :: TCvSubst -> TyCoVar -> TyCoVar -> TCvSubst -extendTCvSubstWithClone subst tcv - | isTyVar tcv = extendTvSubstWithClone subst tcv - | otherwise = extendCvSubstWithClone subst tcv - -extendTvSubst :: TCvSubst -> TyVar -> Type -> TCvSubst -extendTvSubst (TCvSubst in_scope tenv cenv) tv ty - = TCvSubst in_scope (extendVarEnv tenv tv ty) cenv - -extendTvSubstBinderAndInScope :: TCvSubst -> TyCoBinder -> Type -> TCvSubst -extendTvSubstBinderAndInScope subst (Named (Bndr v _)) ty - = ASSERT( isTyVar v ) - extendTvSubstAndInScope subst v ty -extendTvSubstBinderAndInScope subst (Anon {}) _ - = subst - -extendTvSubstWithClone :: TCvSubst -> TyVar -> TyVar -> TCvSubst --- Adds a new tv -> tv mapping, /and/ extends the in-scope set -extendTvSubstWithClone (TCvSubst in_scope tenv cenv) tv tv' - = TCvSubst (extendInScopeSetSet in_scope new_in_scope) - (extendVarEnv tenv tv (mkTyVarTy tv')) - cenv - where - new_in_scope = tyCoVarsOfType (tyVarKind tv') `extendVarSet` tv' - -extendCvSubst :: TCvSubst -> CoVar -> Coercion -> TCvSubst -extendCvSubst (TCvSubst in_scope tenv cenv) v co - = TCvSubst in_scope tenv (extendVarEnv cenv v co) - -extendCvSubstWithClone :: TCvSubst -> CoVar -> CoVar -> TCvSubst -extendCvSubstWithClone (TCvSubst in_scope tenv cenv) cv cv' - = TCvSubst (extendInScopeSetSet in_scope new_in_scope) - tenv - (extendVarEnv cenv cv (mkCoVarCo cv')) - where - new_in_scope = tyCoVarsOfType (varType cv') `extendVarSet` cv' - -extendTvSubstAndInScope :: TCvSubst -> TyVar -> Type -> TCvSubst --- Also extends the in-scope set -extendTvSubstAndInScope (TCvSubst in_scope tenv cenv) tv ty - = TCvSubst (in_scope `extendInScopeSetSet` tyCoVarsOfType ty) - (extendVarEnv tenv tv ty) - cenv - -extendTvSubstList :: TCvSubst -> [Var] -> [Type] -> TCvSubst -extendTvSubstList subst tvs tys - = foldl2 extendTvSubst subst tvs tys - -extendTCvSubstList :: TCvSubst -> [Var] -> [Type] -> TCvSubst -extendTCvSubstList subst tvs tys - = foldl2 extendTCvSubst subst tvs tys - -unionTCvSubst :: TCvSubst -> TCvSubst -> TCvSubst --- Works when the ranges are disjoint -unionTCvSubst (TCvSubst in_scope1 tenv1 cenv1) (TCvSubst in_scope2 tenv2 cenv2) - = ASSERT( not (tenv1 `intersectsVarEnv` tenv2) - && not (cenv1 `intersectsVarEnv` cenv2) ) - TCvSubst (in_scope1 `unionInScope` in_scope2) - (tenv1 `plusVarEnv` tenv2) - (cenv1 `plusVarEnv` cenv2) - --- mkTvSubstPrs and zipTvSubst generate the in-scope set from --- the types given; but it's just a thunk so with a bit of luck --- it'll never be evaluated - --- | Generates the in-scope set for the 'TCvSubst' from the types in the incoming --- environment. No CoVars, please! -zipTvSubst :: HasDebugCallStack => [TyVar] -> [Type] -> TCvSubst -zipTvSubst tvs tys - = mkTvSubst (mkInScopeSet (tyCoVarsOfTypes tys)) tenv - where - tenv = zipTyEnv tvs tys - --- | Generates the in-scope set for the 'TCvSubst' from the types in the incoming --- environment. No TyVars, please! -zipCvSubst :: HasDebugCallStack => [CoVar] -> [Coercion] -> TCvSubst -zipCvSubst cvs cos - = TCvSubst (mkInScopeSet (tyCoVarsOfCos cos)) emptyTvSubstEnv cenv - where - cenv = zipCoEnv cvs cos - -zipTCvSubst :: HasDebugCallStack => [TyCoVar] -> [Type] -> TCvSubst -zipTCvSubst tcvs tys - = zip_tcvsubst tcvs tys (mkEmptyTCvSubst $ mkInScopeSet (tyCoVarsOfTypes tys)) - where zip_tcvsubst :: [TyCoVar] -> [Type] -> TCvSubst -> TCvSubst - zip_tcvsubst (tv:tvs) (ty:tys) subst - = zip_tcvsubst tvs tys (extendTCvSubst subst tv ty) - zip_tcvsubst [] [] subst = subst -- empty case - zip_tcvsubst _ _ _ = pprPanic "zipTCvSubst: length mismatch" - (ppr tcvs <+> ppr tys) - --- | Generates the in-scope set for the 'TCvSubst' from the types in the --- incoming environment. No CoVars, please! -mkTvSubstPrs :: [(TyVar, Type)] -> TCvSubst -mkTvSubstPrs prs = - ASSERT2( onlyTyVarsAndNoCoercionTy, text "prs" <+> ppr prs ) - mkTvSubst in_scope tenv - where tenv = mkVarEnv prs - in_scope = mkInScopeSet $ tyCoVarsOfTypes $ map snd prs - onlyTyVarsAndNoCoercionTy = - and [ isTyVar tv && not (isCoercionTy ty) - | (tv, ty) <- prs ] - -zipTyEnv :: HasDebugCallStack => [TyVar] -> [Type] -> TvSubstEnv -zipTyEnv tyvars tys - | debugIsOn - , not (all isTyVar tyvars) - = pprPanic "zipTyEnv" (ppr tyvars <+> ppr tys) - | otherwise - = ASSERT( all (not . isCoercionTy) tys ) - mkVarEnv (zipEqual "zipTyEnv" tyvars tys) - -- There used to be a special case for when - -- ty == TyVarTy tv - -- (a not-uncommon case) in which case the substitution was dropped. - -- But the type-tidier changes the print-name of a type variable without - -- changing the unique, and that led to a bug. Why? Pre-tidying, we had - -- a type {Foo t}, where Foo is a one-method class. So Foo is really a newtype. - -- And it happened that t was the type variable of the class. Post-tiding, - -- it got turned into {Foo t2}. The ext-core printer expanded this using - -- sourceTypeRep, but that said "Oh, t == t2" because they have the same unique, - -- and so generated a rep type mentioning t not t2. - -- - -- Simplest fix is to nuke the "optimisation" - -zipCoEnv :: HasDebugCallStack => [CoVar] -> [Coercion] -> CvSubstEnv -zipCoEnv cvs cos - | debugIsOn - , not (all isCoVar cvs) - = pprPanic "zipCoEnv" (ppr cvs <+> ppr cos) - | otherwise - = mkVarEnv (zipEqual "zipCoEnv" cvs cos) - -instance Outputable TCvSubst where - ppr (TCvSubst ins tenv cenv) - = brackets $ sep[ text "TCvSubst", - nest 2 (text "In scope:" <+> ppr ins), - nest 2 (text "Type env:" <+> ppr tenv), - nest 2 (text "Co env:" <+> ppr cenv) ] - -{- -%************************************************************************ -%* * - Performing type or kind substitutions -%* * -%************************************************************************ - -Note [Sym and ForAllCo] -~~~~~~~~~~~~~~~~~~~~~~~ -In OptCoercion, we try to push "sym" out to the leaves of a coercion. But, -how do we push sym into a ForAllCo? It's a little ugly. - -Here is the typing rule: - -h : k1 ~# k2 -(tv : k1) |- g : ty1 ~# ty2 ----------------------------- -ForAllCo tv h g : (ForAllTy (tv : k1) ty1) ~# - (ForAllTy (tv : k2) (ty2[tv |-> tv |> sym h])) - -Here is what we want: - -ForAllCo tv h' g' : (ForAllTy (tv : k2) (ty2[tv |-> tv |> sym h])) ~# - (ForAllTy (tv : k1) ty1) - - -Because the kinds of the type variables to the right of the colon are the kinds -coerced by h', we know (h' : k2 ~# k1). Thus, (h' = sym h). - -Now, we can rewrite ty1 to be (ty1[tv |-> tv |> sym h' |> h']). We thus want - -ForAllCo tv h' g' : - (ForAllTy (tv : k2) (ty2[tv |-> tv |> h'])) ~# - (ForAllTy (tv : k1) (ty1[tv |-> tv |> h'][tv |-> tv |> sym h'])) - -We thus see that we want - -g' : ty2[tv |-> tv |> h'] ~# ty1[tv |-> tv |> h'] - -and thus g' = sym (g[tv |-> tv |> h']). - -Putting it all together, we get this: - -sym (ForAllCo tv h g) -==> -ForAllCo tv (sym h) (sym g[tv |-> tv |> sym h]) - -Note [Substituting in a coercion hole] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -It seems highly suspicious to be substituting in a coercion that still -has coercion holes. Yet, this can happen in a situation like this: - - f :: forall k. k :~: Type -> () - f Refl = let x :: forall (a :: k). [a] -> ... - x = ... - -When we check x's type signature, we require that k ~ Type. We indeed -know this due to the Refl pattern match, but the eager unifier can't -make use of givens. So, when we're done looking at x's type, a coercion -hole will remain. Then, when we're checking x's definition, we skolemise -x's type (in order to, e.g., bring the scoped type variable `a` into scope). -This requires performing a substitution for the fresh skolem variables. - -This subsitution needs to affect the kind of the coercion hole, too -- -otherwise, the kind will have an out-of-scope variable in it. More problematically -in practice (we won't actually notice the out-of-scope variable ever), skolems -in the kind might have too high a level, triggering a failure to uphold the -invariant that no free variables in a type have a higher level than the -ambient level in the type checker. In the event of having free variables in the -hole's kind, I'm pretty sure we'll always have an erroneous program, so we -don't need to worry what will happen when the hole gets filled in. After all, -a hole relating a locally-bound type variable will be unable to be solved. This -is why it's OK not to look through the IORef of a coercion hole during -substitution. - --} - --- | Type substitution, see 'zipTvSubst' -substTyWith :: HasCallStack => [TyVar] -> [Type] -> Type -> Type --- Works only if the domain of the substitution is a --- superset of the type being substituted into -substTyWith tvs tys = {-#SCC "substTyWith" #-} - ASSERT( tvs `equalLength` tys ) - substTy (zipTvSubst tvs tys) - --- | Type substitution, see 'zipTvSubst'. Disables sanity checks. --- The problems that the sanity checks in substTy catch are described in --- Note [The substitution invariant]. --- The goal of #11371 is to migrate all the calls of substTyUnchecked to --- substTy and remove this function. Please don't use in new code. -substTyWithUnchecked :: [TyVar] -> [Type] -> Type -> Type -substTyWithUnchecked tvs tys - = ASSERT( tvs `equalLength` tys ) - substTyUnchecked (zipTvSubst tvs tys) - --- | Substitute tyvars within a type using a known 'InScopeSet'. --- Pre-condition: the 'in_scope' set should satisfy Note [The substitution --- invariant]; specifically it should include the free vars of 'tys', --- and of 'ty' minus the domain of the subst. -substTyWithInScope :: InScopeSet -> [TyVar] -> [Type] -> Type -> Type -substTyWithInScope in_scope tvs tys ty = - ASSERT( tvs `equalLength` tys ) - substTy (mkTvSubst in_scope tenv) ty - where tenv = zipTyEnv tvs tys - --- | Coercion substitution, see 'zipTvSubst' -substCoWith :: HasCallStack => [TyVar] -> [Type] -> Coercion -> Coercion -substCoWith tvs tys = ASSERT( tvs `equalLength` tys ) - substCo (zipTvSubst tvs tys) - --- | Coercion substitution, see 'zipTvSubst'. Disables sanity checks. --- The problems that the sanity checks in substCo catch are described in --- Note [The substitution invariant]. --- The goal of #11371 is to migrate all the calls of substCoUnchecked to --- substCo and remove this function. Please don't use in new code. -substCoWithUnchecked :: [TyVar] -> [Type] -> Coercion -> Coercion -substCoWithUnchecked tvs tys - = ASSERT( tvs `equalLength` tys ) - substCoUnchecked (zipTvSubst tvs tys) - - - --- | Substitute covars within a type -substTyWithCoVars :: [CoVar] -> [Coercion] -> Type -> Type -substTyWithCoVars cvs cos = substTy (zipCvSubst cvs cos) - --- | Type substitution, see 'zipTvSubst' -substTysWith :: [TyVar] -> [Type] -> [Type] -> [Type] -substTysWith tvs tys = ASSERT( tvs `equalLength` tys ) - substTys (zipTvSubst tvs tys) - --- | Type substitution, see 'zipTvSubst' -substTysWithCoVars :: [CoVar] -> [Coercion] -> [Type] -> [Type] -substTysWithCoVars cvs cos = ASSERT( cvs `equalLength` cos ) - substTys (zipCvSubst cvs cos) - --- | Substitute within a 'Type' after adding the free variables of the type --- to the in-scope set. This is useful for the case when the free variables --- aren't already in the in-scope set or easily available. --- See also Note [The substitution invariant]. -substTyAddInScope :: TCvSubst -> Type -> Type -substTyAddInScope subst ty = - substTy (extendTCvInScopeSet subst $ tyCoVarsOfType ty) ty - --- | When calling `substTy` it should be the case that the in-scope set in --- the substitution is a superset of the free vars of the range of the --- substitution. --- See also Note [The substitution invariant]. -isValidTCvSubst :: TCvSubst -> Bool -isValidTCvSubst (TCvSubst in_scope tenv cenv) = - (tenvFVs `varSetInScope` in_scope) && - (cenvFVs `varSetInScope` in_scope) - where - tenvFVs = tyCoVarsOfTypesSet tenv - cenvFVs = tyCoVarsOfCosSet cenv - --- | This checks if the substitution satisfies the invariant from --- Note [The substitution invariant]. -checkValidSubst :: HasCallStack => TCvSubst -> [Type] -> [Coercion] -> a -> a -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 "cenv" <+> ppr cenv $$ - text "cenvFVs" <+> ppr (tyCoVarsOfCosSet cenv) $$ - text "tys" <+> ppr tys $$ - text "cos" <+> ppr cos ) - ASSERT2( tysCosFVsInScope, - text "in_scope" <+> ppr in_scope $$ - text "tenv" <+> ppr tenv $$ - text "cenv" <+> ppr cenv $$ - text "tys" <+> ppr tys $$ - text "cos" <+> ppr cos $$ - text "needInScope" <+> ppr needInScope ) - a - where - 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 - tysCosFVsInScope = needInScope `varSetInScope` in_scope - - --- | Substitute within a 'Type' --- The substitution has to satisfy the invariants described in --- Note [The substitution invariant]. -substTy :: HasCallStack => TCvSubst -> Type -> Type -substTy subst ty - | isEmptyTCvSubst subst = ty - | otherwise = checkValidSubst subst [ty] [] $ - subst_ty subst ty - --- | Substitute within a 'Type' disabling the sanity checks. --- The problems that the sanity checks in substTy catch are described in --- Note [The substitution invariant]. --- The goal of #11371 is to migrate all the calls of substTyUnchecked to --- substTy and remove this function. Please don't use in new code. -substTyUnchecked :: TCvSubst -> Type -> Type -substTyUnchecked subst ty - | isEmptyTCvSubst subst = ty - | otherwise = subst_ty subst ty - --- | Substitute within several 'Type's --- The substitution has to satisfy the invariants described in --- Note [The substitution invariant]. -substTys :: HasCallStack => TCvSubst -> [Type] -> [Type] -substTys subst tys - | isEmptyTCvSubst subst = tys - | otherwise = checkValidSubst subst tys [] $ map (subst_ty subst) tys - --- | Substitute within several 'Type's disabling the sanity checks. --- The problems that the sanity checks in substTys catch are described in --- Note [The substitution invariant]. --- The goal of #11371 is to migrate all the calls of substTysUnchecked to --- substTys and remove this function. Please don't use in new code. -substTysUnchecked :: TCvSubst -> [Type] -> [Type] -substTysUnchecked subst tys - | isEmptyTCvSubst subst = tys - | otherwise = map (subst_ty subst) tys - --- | Substitute within a 'ThetaType' --- The substitution has to satisfy the invariants described in --- Note [The substitution invariant]. -substTheta :: HasCallStack => TCvSubst -> ThetaType -> ThetaType -substTheta = substTys - --- | Substitute within a 'ThetaType' disabling the sanity checks. --- The problems that the sanity checks in substTys catch are described in --- Note [The substitution invariant]. --- The goal of #11371 is to migrate all the calls of substThetaUnchecked to --- substTheta and remove this function. Please don't use in new code. -substThetaUnchecked :: TCvSubst -> ThetaType -> ThetaType -substThetaUnchecked = substTysUnchecked - - -subst_ty :: TCvSubst -> Type -> Type --- subst_ty is the main workhorse for type substitution --- --- Note that the in_scope set is poked only if we hit a forall --- so it may often never be fully computed -subst_ty subst ty - = go ty - where - go (TyVarTy tv) = substTyVar subst tv - go (AppTy fun arg) = mkAppTy (go fun) $! (go arg) - -- The mkAppTy smart constructor is important - -- we might be replacing (a Int), represented with App - -- by [Int], represented with TyConApp - go (TyConApp tc tys) = let args = map go tys - in args `seqList` TyConApp tc args - go ty@(FunTy { ft_arg = arg, ft_res = res }) - = let !arg' = go arg - !res' = go res - in ty { ft_arg = arg', ft_res = res' } - go (ForAllTy (Bndr tv vis) ty) - = case substVarBndrUnchecked subst tv of - (subst', tv') -> - (ForAllTy $! ((Bndr $! tv') vis)) $! - (subst_ty subst' ty) - go (LitTy n) = LitTy $! n - go (CastTy ty co) = (mkCastTy $! (go ty)) $! (subst_co subst co) - go (CoercionTy co) = CoercionTy $! (subst_co subst co) - -substTyVar :: TCvSubst -> TyVar -> Type -substTyVar (TCvSubst _ tenv _) tv - = ASSERT( isTyVar tv ) - case lookupVarEnv tenv tv of - Just ty -> ty - Nothing -> TyVarTy tv - -substTyVars :: TCvSubst -> [TyVar] -> [Type] -substTyVars subst = map $ substTyVar subst - -substTyCoVars :: TCvSubst -> [TyCoVar] -> [Type] -substTyCoVars subst = map $ substTyCoVar subst - -substTyCoVar :: TCvSubst -> TyCoVar -> Type -substTyCoVar subst tv - | isTyVar tv = substTyVar subst tv - | otherwise = CoercionTy $ substCoVar subst tv - -lookupTyVar :: TCvSubst -> TyVar -> Maybe Type - -- See Note [Extending the TCvSubst] -lookupTyVar (TCvSubst _ tenv _) tv - = ASSERT( isTyVar tv ) - lookupVarEnv tenv tv - --- | Substitute within a 'Coercion' --- The substitution has to satisfy the invariants described in --- Note [The substitution invariant]. -substCo :: HasCallStack => TCvSubst -> Coercion -> Coercion -substCo subst co - | isEmptyTCvSubst subst = co - | otherwise = checkValidSubst subst [] [co] $ subst_co subst co - --- | Substitute within a 'Coercion' disabling sanity checks. --- The problems that the sanity checks in substCo catch are described in --- Note [The substitution invariant]. --- The goal of #11371 is to migrate all the calls of substCoUnchecked to --- substCo and remove this function. Please don't use in new code. -substCoUnchecked :: TCvSubst -> Coercion -> Coercion -substCoUnchecked subst co - | isEmptyTCvSubst subst = co - | otherwise = subst_co subst co - --- | Substitute within several 'Coercion's --- The substitution has to satisfy the invariants described in --- Note [The substitution invariant]. -substCos :: HasCallStack => TCvSubst -> [Coercion] -> [Coercion] -substCos subst cos - | isEmptyTCvSubst subst = cos - | otherwise = checkValidSubst subst [] cos $ map (subst_co subst) cos - -subst_co :: TCvSubst -> Coercion -> Coercion -subst_co subst co - = go co - where - go_ty :: Type -> Type - go_ty = subst_ty subst - - go_mco :: MCoercion -> MCoercion - go_mco MRefl = MRefl - go_mco (MCo co) = MCo (go co) - - go :: Coercion -> Coercion - go (Refl ty) = mkNomReflCo $! (go_ty ty) - go (GRefl r ty mco) = (mkGReflCo r $! (go_ty ty)) $! (go_mco mco) - go (TyConAppCo r tc args)= let args' = map go args - in args' `seqList` mkTyConAppCo r tc args' - go (AppCo co arg) = (mkAppCo $! go co) $! go arg - go (ForAllCo tv kind_co co) - = case substForAllCoBndrUnchecked subst tv kind_co of - (subst', tv', kind_co') -> - ((mkForAllCo $! tv') $! kind_co') $! subst_co subst' co - go (FunCo r co1 co2) = (mkFunCo r $! go co1) $! go co2 - go (CoVarCo cv) = substCoVar subst cv - go (AxiomInstCo con ind cos) = mkAxiomInstCo con ind $! map go cos - go (UnivCo p r t1 t2) = (((mkUnivCo $! go_prov p) $! r) $! - (go_ty t1)) $! (go_ty t2) - go (SymCo co) = mkSymCo $! (go co) - go (TransCo co1 co2) = (mkTransCo $! (go co1)) $! (go co2) - go (NthCo r d co) = mkNthCo r d $! (go co) - go (LRCo lr co) = mkLRCo lr $! (go co) - go (InstCo co arg) = (mkInstCo $! (go co)) $! go arg - go (KindCo co) = mkKindCo $! (go co) - go (SubCo co) = mkSubCo $! (go co) - go (AxiomRuleCo c cs) = let cs1 = map go cs - in cs1 `seqList` AxiomRuleCo c cs1 - go (HoleCo h) = HoleCo $! go_hole h - - go_prov UnsafeCoerceProv = UnsafeCoerceProv - go_prov (PhantomProv kco) = PhantomProv (go kco) - go_prov (ProofIrrelProv kco) = ProofIrrelProv (go kco) - go_prov p@(PluginProv _) = p - - -- See Note [Substituting in a coercion hole] - go_hole h@(CoercionHole { ch_co_var = cv }) - = h { ch_co_var = updateVarType go_ty cv } - -substForAllCoBndr :: TCvSubst -> TyCoVar -> KindCoercion - -> (TCvSubst, TyCoVar, Coercion) -substForAllCoBndr subst - = substForAllCoBndrUsing False (substCo subst) subst - --- | Like 'substForAllCoBndr', but disables sanity checks. --- The problems that the sanity checks in substCo catch are described in --- Note [The substitution invariant]. --- The goal of #11371 is to migrate all the calls of substCoUnchecked to --- substCo and remove this function. Please don't use in new code. -substForAllCoBndrUnchecked :: TCvSubst -> TyCoVar -> KindCoercion - -> (TCvSubst, TyCoVar, Coercion) -substForAllCoBndrUnchecked subst - = substForAllCoBndrUsing False (substCoUnchecked subst) subst - --- See Note [Sym and ForAllCo] -substForAllCoBndrUsing :: Bool -- apply sym to binder? - -> (Coercion -> Coercion) -- transformation to kind co - -> TCvSubst -> TyCoVar -> KindCoercion - -> (TCvSubst, TyCoVar, KindCoercion) -substForAllCoBndrUsing sym sco subst old_var - | isTyVar old_var = substForAllCoTyVarBndrUsing sym sco subst old_var - | otherwise = substForAllCoCoVarBndrUsing sym sco subst old_var - -substForAllCoTyVarBndrUsing :: Bool -- apply sym to binder? - -> (Coercion -> Coercion) -- transformation to kind co - -> TCvSubst -> TyVar -> KindCoercion - -> (TCvSubst, TyVar, KindCoercion) -substForAllCoTyVarBndrUsing sym sco (TCvSubst in_scope tenv cenv) old_var old_kind_co - = ASSERT( isTyVar old_var ) - ( TCvSubst (in_scope `extendInScopeSet` new_var) new_env cenv - , new_var, new_kind_co ) - where - new_env | no_change && not sym = delVarEnv tenv old_var - | sym = extendVarEnv tenv old_var $ - TyVarTy new_var `CastTy` new_kind_co - | otherwise = extendVarEnv tenv old_var (TyVarTy new_var) - - no_kind_change = noFreeVarsOfCo old_kind_co - no_change = no_kind_change && (new_var == old_var) - - new_kind_co | no_kind_change = old_kind_co - | otherwise = sco old_kind_co - - Pair new_ki1 _ = coercionKind new_kind_co - -- We could do substitution to (tyVarKind old_var). We don't do so because - -- we already substituted new_kind_co, which contains the kind information - -- we want. We don't want to do substitution once more. Also, in most cases, - -- new_kind_co is a Refl, in which case coercionKind is really fast. - - new_var = uniqAway in_scope (setTyVarKind old_var new_ki1) - -substForAllCoCoVarBndrUsing :: Bool -- apply sym to binder? - -> (Coercion -> Coercion) -- transformation to kind co - -> TCvSubst -> CoVar -> KindCoercion - -> (TCvSubst, CoVar, KindCoercion) -substForAllCoCoVarBndrUsing sym sco (TCvSubst in_scope tenv cenv) - old_var old_kind_co - = ASSERT( isCoVar old_var ) - ( TCvSubst (in_scope `extendInScopeSet` new_var) tenv new_cenv - , new_var, new_kind_co ) - where - new_cenv | no_change && not sym = delVarEnv cenv old_var - | otherwise = extendVarEnv cenv old_var (mkCoVarCo new_var) - - no_kind_change = noFreeVarsOfCo old_kind_co - no_change = no_kind_change && (new_var == old_var) - - new_kind_co | no_kind_change = old_kind_co - | otherwise = sco old_kind_co - - Pair h1 h2 = coercionKind new_kind_co - - new_var = uniqAway in_scope $ mkCoVar (varName old_var) new_var_type - new_var_type | sym = h2 - | otherwise = h1 - -substCoVar :: TCvSubst -> CoVar -> Coercion -substCoVar (TCvSubst _ _ cenv) cv - = case lookupVarEnv cenv cv of - Just co -> co - Nothing -> CoVarCo cv - -substCoVars :: TCvSubst -> [CoVar] -> [Coercion] -substCoVars subst cvs = map (substCoVar subst) cvs - -lookupCoVar :: TCvSubst -> Var -> Maybe Coercion -lookupCoVar (TCvSubst _ _ cenv) v = lookupVarEnv cenv v - -substTyVarBndr :: HasCallStack => TCvSubst -> TyVar -> (TCvSubst, TyVar) -substTyVarBndr = substTyVarBndrUsing substTy - -substTyVarBndrs :: HasCallStack => TCvSubst -> [TyVar] -> (TCvSubst, [TyVar]) -substTyVarBndrs = mapAccumL substTyVarBndr - -substVarBndr :: HasCallStack => TCvSubst -> TyCoVar -> (TCvSubst, TyCoVar) -substVarBndr = substVarBndrUsing substTy - -substVarBndrs :: HasCallStack => TCvSubst -> [TyCoVar] -> (TCvSubst, [TyCoVar]) -substVarBndrs = mapAccumL substVarBndr - -substCoVarBndr :: HasCallStack => TCvSubst -> CoVar -> (TCvSubst, CoVar) -substCoVarBndr = substCoVarBndrUsing substTy - --- | Like 'substVarBndr', but disables sanity checks. --- The problems that the sanity checks in substTy catch are described in --- Note [The substitution invariant]. --- The goal of #11371 is to migrate all the calls of substTyUnchecked to --- substTy and remove this function. Please don't use in new code. -substVarBndrUnchecked :: TCvSubst -> TyCoVar -> (TCvSubst, TyCoVar) -substVarBndrUnchecked = substVarBndrUsing substTyUnchecked - -substVarBndrUsing :: (TCvSubst -> Type -> Type) - -> TCvSubst -> TyCoVar -> (TCvSubst, TyCoVar) -substVarBndrUsing subst_fn subst v - | isTyVar v = substTyVarBndrUsing subst_fn subst v - | otherwise = substCoVarBndrUsing subst_fn subst v - --- | Substitute a tyvar in a binding position, returning an --- extended subst and a new tyvar. --- Use the supplied function to substitute in the kind -substTyVarBndrUsing - :: (TCvSubst -> Type -> Type) -- ^ Use this to substitute in the kind - -> TCvSubst -> TyVar -> (TCvSubst, TyVar) -substTyVarBndrUsing subst_fn subst@(TCvSubst in_scope tenv cenv) old_var - = ASSERT2( _no_capture, pprTyVar old_var $$ pprTyVar new_var $$ ppr subst ) - ASSERT( isTyVar old_var ) - (TCvSubst (in_scope `extendInScopeSet` new_var) new_env cenv, new_var) - where - new_env | no_change = delVarEnv tenv old_var - | otherwise = extendVarEnv tenv old_var (TyVarTy new_var) - - _no_capture = not (new_var `elemVarSet` tyCoVarsOfTypesSet tenv) - -- Assertion check that we are not capturing something in the substitution - - old_ki = tyVarKind old_var - no_kind_change = noFreeVarsOfType old_ki -- verify that kind is closed - no_change = no_kind_change && (new_var == old_var) - -- no_change means that the new_var is identical in - -- all respects to the old_var (same unique, same kind) - -- See Note [Extending the TCvSubst] - -- - -- In that case we don't need to extend the substitution - -- to map old to new. But instead we must zap any - -- current substitution for the variable. For example: - -- (\x.e) with id_subst = [x |-> e'] - -- Here we must simply zap the substitution for x - - new_var | no_kind_change = uniqAway in_scope old_var - | otherwise = uniqAway in_scope $ - setTyVarKind old_var (subst_fn subst old_ki) - -- The uniqAway part makes sure the new variable is not already in scope - --- | Substitute a covar in a binding position, returning an --- extended subst and a new covar. --- Use the supplied function to substitute in the kind -substCoVarBndrUsing - :: (TCvSubst -> Type -> Type) - -> TCvSubst -> CoVar -> (TCvSubst, CoVar) -substCoVarBndrUsing subst_fn subst@(TCvSubst in_scope tenv cenv) old_var - = ASSERT( isCoVar old_var ) - (TCvSubst (in_scope `extendInScopeSet` new_var) tenv new_cenv, new_var) - where - new_co = mkCoVarCo new_var - no_kind_change = noFreeVarsOfTypes [t1, t2] - no_change = new_var == old_var && no_kind_change - - new_cenv | no_change = delVarEnv cenv old_var - | otherwise = extendVarEnv cenv old_var new_co - - new_var = uniqAway in_scope subst_old_var - subst_old_var = mkCoVar (varName old_var) new_var_type - - (_, _, t1, t2, role) = coVarKindsTypesRole old_var - t1' = subst_fn subst t1 - t2' = subst_fn subst t2 - new_var_type = mkCoercionType role t1' t2' - -- It's important to do the substitution for coercions, - -- because they can have free type variables - -cloneTyVarBndr :: TCvSubst -> TyVar -> Unique -> (TCvSubst, TyVar) -cloneTyVarBndr subst@(TCvSubst in_scope tv_env cv_env) tv uniq - = ASSERT2( isTyVar tv, ppr tv ) -- I think it's only called on TyVars - (TCvSubst (extendInScopeSet in_scope tv') - (extendVarEnv tv_env tv (mkTyVarTy tv')) cv_env, tv') - where - old_ki = tyVarKind tv - no_kind_change = noFreeVarsOfType old_ki -- verify that kind is closed - - tv1 | no_kind_change = tv - | otherwise = setTyVarKind tv (substTy subst old_ki) - - tv' = setVarUnique tv1 uniq - -cloneTyVarBndrs :: TCvSubst -> [TyVar] -> UniqSupply -> (TCvSubst, [TyVar]) -cloneTyVarBndrs subst [] _usupply = (subst, []) -cloneTyVarBndrs subst (t:ts) usupply = (subst'', tv:tvs) - where - (uniq, usupply') = takeUniqFromSupply usupply - (subst' , tv ) = cloneTyVarBndr subst t uniq - (subst'', tvs) = cloneTyVarBndrs subst' ts usupply' - -{- -%************************************************************************ -%* * - Pretty-printing types - - Defined very early because of debug printing in assertions -%* * -%************************************************************************ - -@pprType@ is the standard @Type@ printer; the overloaded @ppr@ function is -defined to use this. @pprParendType@ is the same, except it puts -parens around the type, except for the atomic cases. @pprParendType@ -works just by setting the initial context precedence very high. - -Note that any function which pretty-prints a @Type@ first converts the @Type@ -to an @IfaceType@. See Note [IfaceType and pretty-printing] in IfaceType. - -See Note [Precedence in types] in BasicTypes. --} - --------------------------------------------------------- --- When pretty-printing types, we convert to IfaceType, --- and pretty-print that. --- See Note [Pretty printing via IfaceSyn] in PprTyThing --------------------------------------------------------- - -pprType, pprParendType :: Type -> SDoc -pprType = pprPrecType topPrec -pprParendType = pprPrecType appPrec - -pprPrecType :: PprPrec -> Type -> SDoc -pprPrecType = pprPrecTypeX emptyTidyEnv - -pprPrecTypeX :: TidyEnv -> PprPrec -> Type -> SDoc -pprPrecTypeX env prec ty - = getPprStyle $ \sty -> - if debugStyle sty -- Use debugPprType when in - then debug_ppr_ty prec ty -- when in debug-style - else pprPrecIfaceType prec (tidyToIfaceTypeStyX env ty sty) - -- NB: debug-style is used for -dppr-debug - -- dump-style is used for -ddump-tc-trace etc - -pprTyLit :: TyLit -> SDoc -pprTyLit = pprIfaceTyLit . toIfaceTyLit - -pprKind, pprParendKind :: Kind -> SDoc -pprKind = pprType -pprParendKind = pprParendType - -tidyToIfaceTypeStyX :: TidyEnv -> Type -> PprStyle -> IfaceType -tidyToIfaceTypeStyX env ty sty - | userStyle sty = tidyToIfaceTypeX env ty - | otherwise = toIfaceTypeX (tyCoVarsOfType ty) ty - -- in latter case, don't tidy, as we'll be printing uniques. - -tidyToIfaceType :: Type -> IfaceType -tidyToIfaceType = tidyToIfaceTypeX emptyTidyEnv - -tidyToIfaceTypeX :: TidyEnv -> Type -> IfaceType --- It's vital to tidy before converting to an IfaceType --- or nested binders will become indistinguishable! --- --- Also for the free type variables, tell toIfaceTypeX to --- leave them as IfaceFreeTyVar. This is super-important --- for debug printing. -tidyToIfaceTypeX env ty = toIfaceTypeX (mkVarSet free_tcvs) (tidyType env' ty) - where - env' = tidyFreeTyCoVars env free_tcvs - free_tcvs = tyCoVarsOfTypeWellScoped ty - ------------- -pprCo, pprParendCo :: Coercion -> SDoc -pprCo co = getPprStyle $ \ sty -> pprIfaceCoercion (tidyToIfaceCoSty co sty) -pprParendCo co = getPprStyle $ \ sty -> pprParendIfaceCoercion (tidyToIfaceCoSty co sty) - -tidyToIfaceCoSty :: Coercion -> PprStyle -> IfaceCoercion -tidyToIfaceCoSty co sty - | userStyle sty = tidyToIfaceCo co - | otherwise = toIfaceCoercionX (tyCoVarsOfCo co) co - -- in latter case, don't tidy, as we'll be printing uniques. - -tidyToIfaceCo :: Coercion -> IfaceCoercion --- It's vital to tidy before converting to an IfaceType --- or nested binders will become indistinguishable! --- --- Also for the free type variables, tell toIfaceCoercionX to --- leave them as IfaceFreeCoVar. This is super-important --- for debug printing. -tidyToIfaceCo co = toIfaceCoercionX (mkVarSet free_tcvs) (tidyCo env co) - where - env = tidyFreeTyCoVars emptyTidyEnv free_tcvs - free_tcvs = scopedSort $ tyCoVarsOfCoList co ------------- -pprClassPred :: Class -> [Type] -> SDoc -pprClassPred clas tys = pprTypeApp (classTyCon clas) tys - ------------- -pprTheta :: ThetaType -> SDoc -pprTheta = pprIfaceContext topPrec . map tidyToIfaceType - -pprParendTheta :: ThetaType -> SDoc -pprParendTheta = pprIfaceContext appPrec . map tidyToIfaceType - -pprThetaArrowTy :: ThetaType -> SDoc -pprThetaArrowTy = pprIfaceContextArr . map tidyToIfaceType - ------------------- -instance Outputable Type where - ppr ty = pprType ty - -instance Outputable TyLit where - ppr = pprTyLit - ------------------- -pprSigmaType :: Type -> SDoc -pprSigmaType = pprIfaceSigmaType ShowForAllWhen . tidyToIfaceType - -pprForAll :: [TyCoVarBinder] -> SDoc -pprForAll tvs = pprIfaceForAll (map toIfaceForAllBndr tvs) - --- | Print a user-level forall; see Note [When to print foralls] -pprUserForAll :: [TyCoVarBinder] -> SDoc -pprUserForAll = pprUserIfaceForAll . map toIfaceForAllBndr - -pprTCvBndrs :: [TyCoVarBinder] -> SDoc -pprTCvBndrs tvs = sep (map pprTCvBndr tvs) - -pprTCvBndr :: TyCoVarBinder -> SDoc -pprTCvBndr = pprTyVar . binderVar - -pprTyVars :: [TyVar] -> SDoc -pprTyVars tvs = sep (map pprTyVar tvs) - -pprTyVar :: TyVar -> SDoc --- Print a type variable binder with its kind (but not if *) --- Here we do not go via IfaceType, because the duplication with --- pprIfaceTvBndr is minimal, and the loss of uniques etc in --- debug printing is disastrous -pprTyVar tv - | isLiftedTypeKind kind = ppr tv - | otherwise = parens (ppr tv <+> dcolon <+> ppr kind) - where - kind = tyVarKind tv - -instance Outputable TyCoBinder where - ppr (Anon af ty) = ppr af <+> ppr ty - ppr (Named (Bndr v Required)) = ppr v - ppr (Named (Bndr v Specified)) = char '@' <> ppr v - ppr (Named (Bndr v Inferred)) = braces (ppr v) - ------------------ -instance Outputable Coercion where -- defined here to avoid orphans - ppr = pprCo - -debugPprType :: Type -> SDoc --- ^ debugPprType is a simple pretty printer that prints a type --- without going through IfaceType. It does not format as prettily --- as the normal route, but it's much more direct, and that can --- be useful for debugging. E.g. with -dppr-debug it prints the --- kind on type-variable /occurrences/ which the normal route --- fundamentally cannot do. -debugPprType ty = debug_ppr_ty topPrec ty - -debug_ppr_ty :: PprPrec -> Type -> SDoc -debug_ppr_ty _ (LitTy l) - = ppr l - -debug_ppr_ty _ (TyVarTy tv) - = ppr tv -- With -dppr-debug we get (tv :: kind) - -debug_ppr_ty prec (FunTy { ft_af = af, ft_arg = arg, ft_res = res }) - = maybeParen prec funPrec $ - sep [debug_ppr_ty funPrec arg, arrow <+> debug_ppr_ty prec res] - where - arrow = case af of - VisArg -> text "->" - InvisArg -> text "=>" - -debug_ppr_ty prec (TyConApp tc tys) - | null tys = ppr tc - | otherwise = maybeParen prec appPrec $ - hang (ppr tc) 2 (sep (map (debug_ppr_ty appPrec) tys)) - -debug_ppr_ty _ (AppTy t1 t2) - = hang (debug_ppr_ty appPrec t1) -- Print parens so we see ((a b) c) - 2 (debug_ppr_ty appPrec t2) -- so that we can distinguish - -- TyConApp from AppTy - -debug_ppr_ty prec (CastTy ty co) - = maybeParen prec topPrec $ - hang (debug_ppr_ty topPrec ty) - 2 (text "|>" <+> ppr co) - -debug_ppr_ty _ (CoercionTy co) - = parens (text "CO" <+> ppr co) - -debug_ppr_ty prec ty@(ForAllTy {}) - | (tvs, body) <- split ty - = maybeParen prec funPrec $ - hang (text "forall" <+> fsep (map ppr tvs) <> dot) - -- The (map ppr tvs) will print kind-annotated - -- tvs, because we are (usually) in debug-style - 2 (ppr body) - where - split ty | ForAllTy tv ty' <- ty - , (tvs, body) <- split ty' - = (tv:tvs, body) - | otherwise - = ([], ty) - -{- -Note [When to print foralls] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Mostly we want to print top-level foralls when (and only when) the user specifies --fprint-explicit-foralls. But when kind polymorphism is at work, that suppresses -too much information; see #9018. - -So I'm trying out this rule: print explicit foralls if - a) User specifies -fprint-explicit-foralls, or - b) Any of the quantified type variables has a kind - that mentions a kind variable - -This catches common situations, such as a type siguature - f :: m a -which means - f :: forall k. forall (m :: k->*) (a :: k). m a -We really want to see both the "forall k" and the kind signatures -on m and a. The latter comes from pprTCvBndr. - -Note [Infix type variables] -~~~~~~~~~~~~~~~~~~~~~~~~~~~ -With TypeOperators you can say - - f :: (a ~> b) -> b - -and the (~>) is considered a type variable. However, the type -pretty-printer in this module will just see (a ~> b) as - - App (App (TyVarTy "~>") (TyVarTy "a")) (TyVarTy "b") - -So it'll print the type in prefix form. To avoid confusion we must -remember to parenthesise the operator, thus - - (~>) a b -> b - -See #2766. --} - -pprDataCons :: TyCon -> SDoc -pprDataCons = sepWithVBars . fmap pprDataConWithArgs . tyConDataCons - where - sepWithVBars [] = empty - sepWithVBars docs = sep (punctuate (space <> vbar) docs) - -pprDataConWithArgs :: DataCon -> SDoc -pprDataConWithArgs dc = sep [forAllDoc, thetaDoc, ppr dc <+> argsDoc] - where - (_univ_tvs, _ex_tvs, _eq_spec, theta, arg_tys, _res_ty) = dataConFullSig dc - user_bndrs = dataConUserTyVarBinders dc - forAllDoc = pprUserForAll user_bndrs - thetaDoc = pprThetaArrowTy theta - argsDoc = hsep (fmap pprParendType arg_tys) - - -pprTypeApp :: TyCon -> [Type] -> SDoc -pprTypeApp tc tys - = pprIfaceTypeApp topPrec (toIfaceTyCon tc) - (toIfaceTcArgs tc tys) - -- TODO: toIfaceTcArgs seems rather wasteful here - ------------------- --- | Display all kind information (with @-fprint-explicit-kinds@) when the --- provided 'Bool' argument is 'True'. --- See @Note [Kind arguments in error messages]@ in "TcErrors". -pprWithExplicitKindsWhen :: Bool -> SDoc -> SDoc -pprWithExplicitKindsWhen b - = updSDocDynFlags $ \dflags -> - if b then gopt_set dflags Opt_PrintExplicitKinds - else dflags - -{- -%************************************************************************ -%* * -\subsection{TidyType} -%* * -%************************************************************************ -} --- | This tidies up a type for printing in an error message, or in --- an interface file. --- --- It doesn't change the uniques at all, just the print names. -tidyVarBndrs :: TidyEnv -> [TyCoVar] -> (TidyEnv, [TyCoVar]) -tidyVarBndrs tidy_env tvs - = mapAccumL tidyVarBndr (avoidNameClashes tvs tidy_env) tvs - -tidyVarBndr :: TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar) -tidyVarBndr tidy_env@(occ_env, subst) var - = case tidyOccName occ_env (getHelpfulOccName var) of - (occ_env', occ') -> ((occ_env', subst'), var') - where - subst' = extendVarEnv subst var var' - var' = setVarType (setVarName var name') type' - type' = tidyType tidy_env (varType var) - name' = tidyNameOcc name occ' - name = varName var - -avoidNameClashes :: [TyCoVar] -> TidyEnv -> TidyEnv --- Seed the occ_env with clashes among the names, see --- Note [Tidying multiple names at once] in OccName -avoidNameClashes tvs (occ_env, subst) - = (avoidClashesOccEnv occ_env occs, subst) - where - occs = map getHelpfulOccName tvs - -getHelpfulOccName :: TyCoVar -> OccName --- A TcTyVar with a System Name is probably a --- unification variable; when we tidy them we give them a trailing --- "0" (or 1 etc) so that they don't take precedence for the --- un-modified name. Plus, indicating a unification variable in --- this way is a helpful clue for users -getHelpfulOccName tv - | isSystemName name, isTcTyVar tv - = mkTyVarOcc (occNameString occ ++ "0") - | otherwise - = occ - where - name = varName tv - occ = getOccName name - -tidyTyCoVarBinder :: TidyEnv -> VarBndr TyCoVar vis - -> (TidyEnv, VarBndr TyCoVar vis) -tidyTyCoVarBinder tidy_env (Bndr tv vis) - = (tidy_env', Bndr tv' vis) - where - (tidy_env', tv') = tidyVarBndr tidy_env tv - -tidyTyCoVarBinders :: TidyEnv -> [VarBndr TyCoVar vis] - -> (TidyEnv, [VarBndr TyCoVar vis]) -tidyTyCoVarBinders tidy_env tvbs - = mapAccumL tidyTyCoVarBinder - (avoidNameClashes (binderVars tvbs) tidy_env) tvbs - ---------------- -tidyFreeTyCoVars :: TidyEnv -> [TyCoVar] -> TidyEnv --- ^ Add the free 'TyVar's to the env in tidy form, --- so that we can tidy the type they are free in -tidyFreeTyCoVars (full_occ_env, var_env) tyvars - = fst (tidyOpenTyCoVars (full_occ_env, var_env) tyvars) - ---------------- -tidyOpenTyCoVars :: TidyEnv -> [TyCoVar] -> (TidyEnv, [TyCoVar]) -tidyOpenTyCoVars env tyvars = mapAccumL tidyOpenTyCoVar env tyvars - ---------------- -tidyOpenTyCoVar :: TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar) --- ^ Treat a new 'TyCoVar' as a binder, and give it a fresh tidy name --- using the environment if one has not already been allocated. See --- also 'tidyVarBndr' -tidyOpenTyCoVar env@(_, subst) tyvar - = case lookupVarEnv subst tyvar of - Just tyvar' -> (env, tyvar') -- Already substituted - Nothing -> - let env' = tidyFreeTyCoVars env (tyCoVarsOfTypeList (tyVarKind tyvar)) - in tidyVarBndr env' tyvar -- Treat it as a binder - ---------------- -tidyTyCoVarOcc :: TidyEnv -> TyCoVar -> TyCoVar -tidyTyCoVarOcc env@(_, subst) tv - = case lookupVarEnv subst tv of - Nothing -> updateVarType (tidyType env) tv - Just tv' -> tv' - ---------------- -tidyTypes :: TidyEnv -> [Type] -> [Type] -tidyTypes env tys = map (tidyType env) tys - ---------------- -tidyType :: TidyEnv -> Type -> Type -tidyType _ (LitTy n) = LitTy n -tidyType env (TyVarTy tv) = TyVarTy (tidyTyCoVarOcc env tv) -tidyType env (TyConApp tycon tys) = let args = tidyTypes env tys - in args `seqList` TyConApp tycon args -tidyType env (AppTy fun arg) = (AppTy $! (tidyType env fun)) $! (tidyType env arg) -tidyType env ty@(FunTy _ arg res) = let { !arg' = tidyType env arg - ; !res' = tidyType env res } - in ty { ft_arg = arg', ft_res = res' } -tidyType env (ty@(ForAllTy{})) = mkForAllTys' (zip tvs' vis) $! tidyType env' body_ty - where - (tvs, vis, body_ty) = splitForAllTys' ty - (env', tvs') = tidyVarBndrs env tvs -tidyType env (CastTy ty co) = (CastTy $! tidyType env ty) $! (tidyCo env co) -tidyType env (CoercionTy co) = CoercionTy $! (tidyCo env co) - - --- The following two functions differ from mkForAllTys and splitForAllTys in that --- they expect/preserve the ArgFlag argument. Thes belong to types/Type.hs, but --- how should they be named? -mkForAllTys' :: [(TyCoVar, ArgFlag)] -> Type -> Type -mkForAllTys' tvvs ty = foldr strictMkForAllTy ty tvvs - where - strictMkForAllTy (tv,vis) ty = (ForAllTy $! ((Bndr $! tv) $! vis)) $! ty - -splitForAllTys' :: Type -> ([TyCoVar], [ArgFlag], Type) -splitForAllTys' ty = go ty [] [] - where - go (ForAllTy (Bndr tv vis) ty) tvs viss = go ty (tv:tvs) (vis:viss) - go ty tvs viss = (reverse tvs, reverse viss, ty) - - ---------------- --- | Grabs the free type variables, tidies them --- and then uses 'tidyType' to work over the type itself -tidyOpenTypes :: TidyEnv -> [Type] -> (TidyEnv, [Type]) -tidyOpenTypes env tys - = (env', tidyTypes (trimmed_occ_env, var_env) tys) - where - (env'@(_, var_env), tvs') = tidyOpenTyCoVars env $ - tyCoVarsOfTypesWellScoped tys - trimmed_occ_env = initTidyOccEnv (map getOccName tvs') - -- The idea here was that we restrict the new TidyEnv to the - -- _free_ vars of the types, so that we don't gratuitously rename - -- the _bound_ variables of the types. - ---------------- -tidyOpenType :: TidyEnv -> Type -> (TidyEnv, Type) -tidyOpenType env ty = let (env', [ty']) = tidyOpenTypes env [ty] in - (env', ty') - ---------------- --- | Calls 'tidyType' on a top-level type (i.e. with an empty tidying environment) -tidyTopType :: Type -> Type -tidyTopType ty = tidyType emptyTidyEnv ty - ---------------- -tidyOpenKind :: TidyEnv -> Kind -> (TidyEnv, Kind) -tidyOpenKind = tidyOpenType - -tidyKind :: TidyEnv -> Kind -> Kind -tidyKind = tidyType - ----------------- -tidyCo :: TidyEnv -> Coercion -> Coercion -tidyCo env@(_, subst) co - = go co - where - go_mco MRefl = MRefl - go_mco (MCo co) = MCo (go co) - - go (Refl ty) = Refl (tidyType env ty) - go (GRefl r ty mco) = GRefl r (tidyType env ty) $! go_mco mco - go (TyConAppCo r tc cos) = let args = map go cos - in args `seqList` TyConAppCo r tc args - go (AppCo co1 co2) = (AppCo $! go co1) $! go co2 - go (ForAllCo tv h co) = ((ForAllCo $! tvp) $! (go h)) $! (tidyCo envp co) - where (envp, tvp) = tidyVarBndr env tv - -- the case above duplicates a bit of work in tidying h and the kind - -- of tv. But the alternative is to use coercionKind, which seems worse. - go (FunCo r co1 co2) = (FunCo r $! go co1) $! go co2 - go (CoVarCo cv) = case lookupVarEnv subst cv of - Nothing -> CoVarCo cv - Just cv' -> CoVarCo cv' - go (HoleCo h) = HoleCo h - go (AxiomInstCo con ind cos) = let args = map go cos - in args `seqList` AxiomInstCo con ind args - go (UnivCo p r t1 t2) = (((UnivCo $! (go_prov p)) $! r) $! - tidyType env t1) $! tidyType env t2 - go (SymCo co) = SymCo $! go co - go (TransCo co1 co2) = (TransCo $! go co1) $! go co2 - go (NthCo r d co) = NthCo r d $! go co - go (LRCo lr co) = LRCo lr $! go co - go (InstCo co ty) = (InstCo $! go co) $! go ty - go (KindCo co) = KindCo $! go co - go (SubCo co) = SubCo $! go co - go (AxiomRuleCo ax cos) = let cos1 = tidyCos env cos - in cos1 `seqList` AxiomRuleCo ax cos1 - - go_prov UnsafeCoerceProv = UnsafeCoerceProv - go_prov (PhantomProv co) = PhantomProv (go co) - go_prov (ProofIrrelProv co) = ProofIrrelProv (go co) - go_prov p@(PluginProv _) = p - -tidyCos :: TidyEnv -> [Coercion] -> [Coercion] -tidyCos env = map (tidyCo env) - {- ********************************************************************* * * diff --git a/compiler/types/TyCoRep.hs-boot b/compiler/types/TyCoRep.hs-boot index cdc4cd6d4c..8f1d0ad526 100644 --- a/compiler/types/TyCoRep.hs-boot +++ b/compiler/types/TyCoRep.hs-boot @@ -2,7 +2,6 @@ module TyCoRep where import GhcPrelude -import Outputable ( SDoc ) import Data.Data ( Data ) import {-# SOURCE #-} Var( Var, ArgFlag, AnonArgFlag ) @@ -10,7 +9,6 @@ data Type data TyThing data Coercion data UnivCoProvenance -data TCvSubst data TyLit data TyCoBinder data MCoercion @@ -21,8 +19,6 @@ type ThetaType = [PredType] type CoercionN = Coercion type MCoercionN = MCoercion -pprKind :: Kind -> SDoc -pprType :: Type -> SDoc mkFunTy :: AnonArgFlag -> Type -> Type -> Type mkForAllTy :: Var -> ArgFlag -> Type -> Type diff --git a/compiler/types/TyCoSubst.hs b/compiler/types/TyCoSubst.hs new file mode 100644 index 0000000000..5c557f595d --- /dev/null +++ b/compiler/types/TyCoSubst.hs @@ -0,0 +1,1029 @@ +{- +(c) The University of Glasgow 2006 +(c) The GRASP/AQUA Project, Glasgow University, 1998 +Type and Coercion - friends' interface +-} + +{-# LANGUAGE CPP #-} +{-# LANGUAGE BangPatterns #-} + +-- | Substitution into types and coercions. +module TyCoSubst + ( + -- * Substitutions + TCvSubst(..), TvSubstEnv, CvSubstEnv, + emptyTvSubstEnv, emptyCvSubstEnv, composeTCvSubstEnv, composeTCvSubst, + emptyTCvSubst, mkEmptyTCvSubst, isEmptyTCvSubst, + mkTCvSubst, mkTvSubst, mkCvSubst, + getTvSubstEnv, + getCvSubstEnv, getTCvInScope, getTCvSubstRangeFVs, + isInScope, notElemTCvSubst, + setTvSubstEnv, setCvSubstEnv, zapTCvSubst, + extendTCvInScope, extendTCvInScopeList, extendTCvInScopeSet, + extendTCvSubst, extendTCvSubstWithClone, + extendCvSubst, extendCvSubstWithClone, + extendTvSubst, extendTvSubstBinderAndInScope, extendTvSubstWithClone, + extendTvSubstList, extendTvSubstAndInScope, + extendTCvSubstList, + unionTCvSubst, zipTyEnv, zipCoEnv, mkTyCoInScopeSet, + zipTvSubst, zipCvSubst, + zipTCvSubst, + mkTvSubstPrs, + + substTyWith, substTyWithCoVars, substTysWith, substTysWithCoVars, + substCoWith, + substTy, substTyAddInScope, + substTyUnchecked, substTysUnchecked, substThetaUnchecked, + substTyWithUnchecked, + substCoUnchecked, substCoWithUnchecked, + substTyWithInScope, + substTys, substTheta, + lookupTyVar, + substCo, substCos, substCoVar, substCoVars, lookupCoVar, + cloneTyVarBndr, cloneTyVarBndrs, + substVarBndr, substVarBndrs, + substTyVarBndr, substTyVarBndrs, + substCoVarBndr, + substTyVar, substTyVars, substTyCoVars, + substForAllCoBndr, + substVarBndrUsing, substForAllCoBndrUsing, + checkValidSubst, isValidTCvSubst, + ) where + +#include "HsVersions.h" + +import GhcPrelude + +import {-# SOURCE #-} Type ( mkCastTy, mkAppTy, isCoercionTy ) +import {-# SOURCE #-} Coercion ( mkCoVarCo, mkKindCo, mkNthCo, mkTransCo + , mkNomReflCo, mkSubCo, mkSymCo + , mkFunCo, mkForAllCo, mkUnivCo + , mkAxiomInstCo, mkAppCo, mkGReflCo + , mkInstCo, mkLRCo, mkTyConAppCo + , mkCoercionType + , coercionKind, coVarKindsTypesRole ) + +import TyCoRep +import TyCoFVs +import TyCoPpr + +import Var +import VarSet +import VarEnv + +import Pair +import Util +import UniqSupply +import Unique +import UniqFM +import UniqSet +import Outputable + +import Data.List + +{- +%************************************************************************ +%* * + Substitutions + Data type defined here to avoid unnecessary mutual recursion +%* * +%************************************************************************ +-} + +-- | Type & coercion substitution +-- +-- #tcvsubst_invariant# +-- The following invariants must hold of a 'TCvSubst': +-- +-- 1. The in-scope set is needed /only/ to +-- guide the generation of fresh uniques +-- +-- 2. In particular, the /kind/ of the type variables in +-- the in-scope set is not relevant +-- +-- 3. The substitution is only applied ONCE! This is because +-- in general such application will not reach a fixed point. +data TCvSubst + = TCvSubst InScopeSet -- The in-scope type and kind variables + TvSubstEnv -- Substitutes both type and kind variables + CvSubstEnv -- Substitutes coercion variables + -- See Note [Substitutions apply only once] + -- and Note [Extending the TvSubstEnv] + -- and Note [Substituting types and coercions] + -- and Note [The substitution invariant] + +-- | A substitution of 'Type's for 'TyVar's +-- and 'Kind's for 'KindVar's +type TvSubstEnv = TyVarEnv Type + -- NB: A TvSubstEnv is used + -- both inside a TCvSubst (with the apply-once invariant + -- discussed in Note [Substitutions apply only once], + -- and also independently in the middle of matching, + -- and unification (see Types.Unify). + -- So you have to look at the context to know if it's idempotent or + -- apply-once or whatever + +-- | A substitution of 'Coercion's for 'CoVar's +type CvSubstEnv = CoVarEnv Coercion + +{- Note [The substitution invariant] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +When calling (substTy subst ty) it should be the case that +the in-scope set in the substitution is a superset of both: + + (SIa) The free vars of the range of the substitution + (SIb) The free vars of ty minus the domain of the substitution + +The same rules apply to other substitutions (notably CoreSubst.Subst) + +* Reason for (SIa). Consider + substTy [a :-> Maybe b] (forall b. b->a) + we must rename the forall b, to get + forall b2. b2 -> Maybe b + Making 'b' part of the in-scope set forces this renaming to + take place. + +* Reason for (SIb). Consider + substTy [a :-> Maybe b] (forall b. (a,b,x)) + Then if we use the in-scope set {b}, satisfying (SIa), there is + a danger we will rename the forall'd variable to 'x' by mistake, + getting this: + forall x. (Maybe b, x, x) + Breaking (SIb) caused the bug from #11371. + +Note: if the free vars of the range of the substitution are freshly created, +then the problems of (SIa) can't happen, and so it would be sound to +ignore (SIa). + +Note [Substitutions apply only once] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We use TCvSubsts to instantiate things, and we might instantiate + forall a b. ty +with the types + [a, b], or [b, a]. +So the substitution might go [a->b, b->a]. A similar situation arises in Core +when we find a beta redex like + (/\ a /\ b -> e) b a +Then we also end up with a substitution that permutes type variables. Other +variations happen to; for example [a -> (a, b)]. + + ******************************************************** + *** So a substitution must be applied precisely once *** + ******************************************************** + +A TCvSubst is not idempotent, but, unlike the non-idempotent substitution +we use during unifications, it must not be repeatedly applied. + +Note [Extending the TvSubstEnv] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +See #tcvsubst_invariant# for the invariants that must hold. + +This invariant allows a short-cut when the subst envs are empty: +if the TvSubstEnv and CvSubstEnv are empty --- i.e. (isEmptyTCvSubst subst) +holds --- then (substTy subst ty) does nothing. + +For example, consider: + (/\a. /\b:(a~Int). ...b..) Int +We substitute Int for 'a'. The Unique of 'b' does not change, but +nevertheless we add 'b' to the TvSubstEnv, because b's kind does change + +This invariant has several crucial consequences: + +* In substVarBndr, we need extend the TvSubstEnv + - if the unique has changed + - or if the kind has changed + +* In substTyVar, we do not need to consult the in-scope set; + the TvSubstEnv is enough + +* In substTy, substTheta, we can short-circuit when the TvSubstEnv is empty + +Note [Substituting types and coercions] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Types and coercions are mutually recursive, and either may have variables +"belonging" to the other. Thus, every time we wish to substitute in a +type, we may also need to substitute in a coercion, and vice versa. +However, the constructor used to create type variables is distinct from +that of coercion variables, so we carry two VarEnvs in a TCvSubst. Note +that it would be possible to use the CoercionTy constructor to combine +these environments, but that seems like a false economy. + +Note that the TvSubstEnv should *never* map a CoVar (built with the Id +constructor) and the CvSubstEnv should *never* map a TyVar. Furthermore, +the range of the TvSubstEnv should *never* include a type headed with +CoercionTy. +-} + +emptyTvSubstEnv :: TvSubstEnv +emptyTvSubstEnv = emptyVarEnv + +emptyCvSubstEnv :: CvSubstEnv +emptyCvSubstEnv = emptyVarEnv + +composeTCvSubstEnv :: InScopeSet + -> (TvSubstEnv, CvSubstEnv) + -> (TvSubstEnv, CvSubstEnv) + -> (TvSubstEnv, CvSubstEnv) +-- ^ @(compose env1 env2)(x)@ is @env1(env2(x))@; i.e. apply @env2@ then @env1@. +-- It assumes that both are idempotent. +-- Typically, @env1@ is the refinement to a base substitution @env2@ +composeTCvSubstEnv in_scope (tenv1, cenv1) (tenv2, cenv2) + = ( tenv1 `plusVarEnv` mapVarEnv (substTy subst1) tenv2 + , cenv1 `plusVarEnv` mapVarEnv (substCo subst1) cenv2 ) + -- First apply env1 to the range of env2 + -- Then combine the two, making sure that env1 loses if + -- both bind the same variable; that's why env1 is the + -- *left* argument to plusVarEnv, because the right arg wins + where + subst1 = TCvSubst in_scope tenv1 cenv1 + +-- | Composes two substitutions, applying the second one provided first, +-- like in function composition. +composeTCvSubst :: TCvSubst -> TCvSubst -> TCvSubst +composeTCvSubst (TCvSubst is1 tenv1 cenv1) (TCvSubst is2 tenv2 cenv2) + = TCvSubst is3 tenv3 cenv3 + where + is3 = is1 `unionInScope` is2 + (tenv3, cenv3) = composeTCvSubstEnv is3 (tenv1, cenv1) (tenv2, cenv2) + +emptyTCvSubst :: TCvSubst +emptyTCvSubst = TCvSubst emptyInScopeSet emptyTvSubstEnv emptyCvSubstEnv + +mkEmptyTCvSubst :: InScopeSet -> TCvSubst +mkEmptyTCvSubst is = TCvSubst is emptyTvSubstEnv emptyCvSubstEnv + +isEmptyTCvSubst :: TCvSubst -> Bool + -- See Note [Extending the TvSubstEnv] +isEmptyTCvSubst (TCvSubst _ tenv cenv) = isEmptyVarEnv tenv && isEmptyVarEnv cenv + +mkTCvSubst :: InScopeSet -> (TvSubstEnv, CvSubstEnv) -> TCvSubst +mkTCvSubst in_scope (tenv, cenv) = TCvSubst in_scope tenv cenv + +mkTvSubst :: InScopeSet -> TvSubstEnv -> TCvSubst +-- ^ Make a TCvSubst with specified tyvar subst and empty covar subst +mkTvSubst in_scope tenv = TCvSubst in_scope tenv emptyCvSubstEnv + +mkCvSubst :: InScopeSet -> CvSubstEnv -> TCvSubst +-- ^ Make a TCvSubst with specified covar subst and empty tyvar subst +mkCvSubst in_scope cenv = TCvSubst in_scope emptyTvSubstEnv cenv + +getTvSubstEnv :: TCvSubst -> TvSubstEnv +getTvSubstEnv (TCvSubst _ env _) = env + +getCvSubstEnv :: TCvSubst -> CvSubstEnv +getCvSubstEnv (TCvSubst _ _ env) = env + +getTCvInScope :: TCvSubst -> InScopeSet +getTCvInScope (TCvSubst in_scope _ _) = in_scope + +-- | Returns the free variables of the types in the range of a substitution as +-- a non-deterministic set. +getTCvSubstRangeFVs :: TCvSubst -> VarSet +getTCvSubstRangeFVs (TCvSubst _ tenv cenv) + = unionVarSet tenvFVs cenvFVs + where + tenvFVs = tyCoVarsOfTypesSet tenv + cenvFVs = tyCoVarsOfCosSet cenv + +isInScope :: Var -> TCvSubst -> Bool +isInScope v (TCvSubst in_scope _ _) = v `elemInScopeSet` in_scope + +notElemTCvSubst :: Var -> TCvSubst -> Bool +notElemTCvSubst v (TCvSubst _ tenv cenv) + | isTyVar v + = not (v `elemVarEnv` tenv) + | otherwise + = not (v `elemVarEnv` cenv) + +setTvSubstEnv :: TCvSubst -> TvSubstEnv -> TCvSubst +setTvSubstEnv (TCvSubst in_scope _ cenv) tenv = TCvSubst in_scope tenv cenv + +setCvSubstEnv :: TCvSubst -> CvSubstEnv -> TCvSubst +setCvSubstEnv (TCvSubst in_scope tenv _) cenv = TCvSubst in_scope tenv cenv + +zapTCvSubst :: TCvSubst -> TCvSubst +zapTCvSubst (TCvSubst in_scope _ _) = TCvSubst in_scope emptyVarEnv emptyVarEnv + +extendTCvInScope :: TCvSubst -> Var -> TCvSubst +extendTCvInScope (TCvSubst in_scope tenv cenv) var + = TCvSubst (extendInScopeSet in_scope var) tenv cenv + +extendTCvInScopeList :: TCvSubst -> [Var] -> TCvSubst +extendTCvInScopeList (TCvSubst in_scope tenv cenv) vars + = TCvSubst (extendInScopeSetList in_scope vars) tenv cenv + +extendTCvInScopeSet :: TCvSubst -> VarSet -> TCvSubst +extendTCvInScopeSet (TCvSubst in_scope tenv cenv) vars + = TCvSubst (extendInScopeSetSet in_scope vars) tenv cenv + +extendTCvSubst :: TCvSubst -> TyCoVar -> Type -> TCvSubst +extendTCvSubst subst v ty + | isTyVar v + = extendTvSubst subst v ty + | CoercionTy co <- ty + = extendCvSubst subst v co + | otherwise + = pprPanic "extendTCvSubst" (ppr v <+> text "|->" <+> ppr ty) + +extendTCvSubstWithClone :: TCvSubst -> TyCoVar -> TyCoVar -> TCvSubst +extendTCvSubstWithClone subst tcv + | isTyVar tcv = extendTvSubstWithClone subst tcv + | otherwise = extendCvSubstWithClone subst tcv + +extendTvSubst :: TCvSubst -> TyVar -> Type -> TCvSubst +extendTvSubst (TCvSubst in_scope tenv cenv) tv ty + = TCvSubst in_scope (extendVarEnv tenv tv ty) cenv + +extendTvSubstBinderAndInScope :: TCvSubst -> TyCoBinder -> Type -> TCvSubst +extendTvSubstBinderAndInScope subst (Named (Bndr v _)) ty + = ASSERT( isTyVar v ) + extendTvSubstAndInScope subst v ty +extendTvSubstBinderAndInScope subst (Anon {}) _ + = subst + +extendTvSubstWithClone :: TCvSubst -> TyVar -> TyVar -> TCvSubst +-- Adds a new tv -> tv mapping, /and/ extends the in-scope set +extendTvSubstWithClone (TCvSubst in_scope tenv cenv) tv tv' + = TCvSubst (extendInScopeSetSet in_scope new_in_scope) + (extendVarEnv tenv tv (mkTyVarTy tv')) + cenv + where + new_in_scope = tyCoVarsOfType (tyVarKind tv') `extendVarSet` tv' + +extendCvSubst :: TCvSubst -> CoVar -> Coercion -> TCvSubst +extendCvSubst (TCvSubst in_scope tenv cenv) v co + = TCvSubst in_scope tenv (extendVarEnv cenv v co) + +extendCvSubstWithClone :: TCvSubst -> CoVar -> CoVar -> TCvSubst +extendCvSubstWithClone (TCvSubst in_scope tenv cenv) cv cv' + = TCvSubst (extendInScopeSetSet in_scope new_in_scope) + tenv + (extendVarEnv cenv cv (mkCoVarCo cv')) + where + new_in_scope = tyCoVarsOfType (varType cv') `extendVarSet` cv' + +extendTvSubstAndInScope :: TCvSubst -> TyVar -> Type -> TCvSubst +-- Also extends the in-scope set +extendTvSubstAndInScope (TCvSubst in_scope tenv cenv) tv ty + = TCvSubst (in_scope `extendInScopeSetSet` tyCoVarsOfType ty) + (extendVarEnv tenv tv ty) + cenv + +extendTvSubstList :: TCvSubst -> [Var] -> [Type] -> TCvSubst +extendTvSubstList subst tvs tys + = foldl2 extendTvSubst subst tvs tys + +extendTCvSubstList :: TCvSubst -> [Var] -> [Type] -> TCvSubst +extendTCvSubstList subst tvs tys + = foldl2 extendTCvSubst subst tvs tys + +unionTCvSubst :: TCvSubst -> TCvSubst -> TCvSubst +-- Works when the ranges are disjoint +unionTCvSubst (TCvSubst in_scope1 tenv1 cenv1) (TCvSubst in_scope2 tenv2 cenv2) + = ASSERT( not (tenv1 `intersectsVarEnv` tenv2) + && not (cenv1 `intersectsVarEnv` cenv2) ) + TCvSubst (in_scope1 `unionInScope` in_scope2) + (tenv1 `plusVarEnv` tenv2) + (cenv1 `plusVarEnv` cenv2) + +-- mkTvSubstPrs and zipTvSubst generate the in-scope set from +-- the types given; but it's just a thunk so with a bit of luck +-- it'll never be evaluated + +-- | Generates the in-scope set for the 'TCvSubst' from the types in the incoming +-- environment. No CoVars, please! +zipTvSubst :: HasDebugCallStack => [TyVar] -> [Type] -> TCvSubst +zipTvSubst tvs tys + = mkTvSubst (mkInScopeSet (tyCoVarsOfTypes tys)) tenv + where + tenv = zipTyEnv tvs tys + +-- | Generates the in-scope set for the 'TCvSubst' from the types in the incoming +-- environment. No TyVars, please! +zipCvSubst :: HasDebugCallStack => [CoVar] -> [Coercion] -> TCvSubst +zipCvSubst cvs cos + = TCvSubst (mkInScopeSet (tyCoVarsOfCos cos)) emptyTvSubstEnv cenv + where + cenv = zipCoEnv cvs cos + +zipTCvSubst :: HasDebugCallStack => [TyCoVar] -> [Type] -> TCvSubst +zipTCvSubst tcvs tys + = zip_tcvsubst tcvs tys (mkEmptyTCvSubst $ mkInScopeSet (tyCoVarsOfTypes tys)) + where zip_tcvsubst :: [TyCoVar] -> [Type] -> TCvSubst -> TCvSubst + zip_tcvsubst (tv:tvs) (ty:tys) subst + = zip_tcvsubst tvs tys (extendTCvSubst subst tv ty) + zip_tcvsubst [] [] subst = subst -- empty case + zip_tcvsubst _ _ _ = pprPanic "zipTCvSubst: length mismatch" + (ppr tcvs <+> ppr tys) + +-- | Generates the in-scope set for the 'TCvSubst' from the types in the +-- incoming environment. No CoVars, please! +mkTvSubstPrs :: [(TyVar, Type)] -> TCvSubst +mkTvSubstPrs prs = + ASSERT2( onlyTyVarsAndNoCoercionTy, text "prs" <+> ppr prs ) + mkTvSubst in_scope tenv + where tenv = mkVarEnv prs + in_scope = mkInScopeSet $ tyCoVarsOfTypes $ map snd prs + onlyTyVarsAndNoCoercionTy = + and [ isTyVar tv && not (isCoercionTy ty) + | (tv, ty) <- prs ] + +zipTyEnv :: HasDebugCallStack => [TyVar] -> [Type] -> TvSubstEnv +zipTyEnv tyvars tys + | debugIsOn + , not (all isTyVar tyvars) + = pprPanic "zipTyEnv" (ppr tyvars <+> ppr tys) + | otherwise + = ASSERT( all (not . isCoercionTy) tys ) + mkVarEnv (zipEqual "zipTyEnv" tyvars tys) + -- There used to be a special case for when + -- ty == TyVarTy tv + -- (a not-uncommon case) in which case the substitution was dropped. + -- But the type-tidier changes the print-name of a type variable without + -- changing the unique, and that led to a bug. Why? Pre-tidying, we had + -- a type {Foo t}, where Foo is a one-method class. So Foo is really a newtype. + -- And it happened that t was the type variable of the class. Post-tiding, + -- it got turned into {Foo t2}. The ext-core printer expanded this using + -- sourceTypeRep, but that said "Oh, t == t2" because they have the same unique, + -- and so generated a rep type mentioning t not t2. + -- + -- Simplest fix is to nuke the "optimisation" + +zipCoEnv :: HasDebugCallStack => [CoVar] -> [Coercion] -> CvSubstEnv +zipCoEnv cvs cos + | debugIsOn + , not (all isCoVar cvs) + = pprPanic "zipCoEnv" (ppr cvs <+> ppr cos) + | otherwise + = mkVarEnv (zipEqual "zipCoEnv" cvs cos) + +instance Outputable TCvSubst where + ppr (TCvSubst ins tenv cenv) + = brackets $ sep[ text "TCvSubst", + nest 2 (text "In scope:" <+> ppr ins), + nest 2 (text "Type env:" <+> ppr tenv), + nest 2 (text "Co env:" <+> ppr cenv) ] + +{- +%************************************************************************ +%* * + Performing type or kind substitutions +%* * +%************************************************************************ + +Note [Sym and ForAllCo] +~~~~~~~~~~~~~~~~~~~~~~~ +In OptCoercion, we try to push "sym" out to the leaves of a coercion. But, +how do we push sym into a ForAllCo? It's a little ugly. + +Here is the typing rule: + +h : k1 ~# k2 +(tv : k1) |- g : ty1 ~# ty2 +---------------------------- +ForAllCo tv h g : (ForAllTy (tv : k1) ty1) ~# + (ForAllTy (tv : k2) (ty2[tv |-> tv |> sym h])) + +Here is what we want: + +ForAllCo tv h' g' : (ForAllTy (tv : k2) (ty2[tv |-> tv |> sym h])) ~# + (ForAllTy (tv : k1) ty1) + + +Because the kinds of the type variables to the right of the colon are the kinds +coerced by h', we know (h' : k2 ~# k1). Thus, (h' = sym h). + +Now, we can rewrite ty1 to be (ty1[tv |-> tv |> sym h' |> h']). We thus want + +ForAllCo tv h' g' : + (ForAllTy (tv : k2) (ty2[tv |-> tv |> h'])) ~# + (ForAllTy (tv : k1) (ty1[tv |-> tv |> h'][tv |-> tv |> sym h'])) + +We thus see that we want + +g' : ty2[tv |-> tv |> h'] ~# ty1[tv |-> tv |> h'] + +and thus g' = sym (g[tv |-> tv |> h']). + +Putting it all together, we get this: + +sym (ForAllCo tv h g) +==> +ForAllCo tv (sym h) (sym g[tv |-> tv |> sym h]) + +Note [Substituting in a coercion hole] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +It seems highly suspicious to be substituting in a coercion that still +has coercion holes. Yet, this can happen in a situation like this: + + f :: forall k. k :~: Type -> () + f Refl = let x :: forall (a :: k). [a] -> ... + x = ... + +When we check x's type signature, we require that k ~ Type. We indeed +know this due to the Refl pattern match, but the eager unifier can't +make use of givens. So, when we're done looking at x's type, a coercion +hole will remain. Then, when we're checking x's definition, we skolemise +x's type (in order to, e.g., bring the scoped type variable `a` into scope). +This requires performing a substitution for the fresh skolem variables. + +This subsitution needs to affect the kind of the coercion hole, too -- +otherwise, the kind will have an out-of-scope variable in it. More problematically +in practice (we won't actually notice the out-of-scope variable ever), skolems +in the kind might have too high a level, triggering a failure to uphold the +invariant that no free variables in a type have a higher level than the +ambient level in the type checker. In the event of having free variables in the +hole's kind, I'm pretty sure we'll always have an erroneous program, so we +don't need to worry what will happen when the hole gets filled in. After all, +a hole relating a locally-bound type variable will be unable to be solved. This +is why it's OK not to look through the IORef of a coercion hole during +substitution. + +-} + +-- | Type substitution, see 'zipTvSubst' +substTyWith :: HasCallStack => [TyVar] -> [Type] -> Type -> Type +-- Works only if the domain of the substitution is a +-- superset of the type being substituted into +substTyWith tvs tys = {-#SCC "substTyWith" #-} + ASSERT( tvs `equalLength` tys ) + substTy (zipTvSubst tvs tys) + +-- | Type substitution, see 'zipTvSubst'. Disables sanity checks. +-- The problems that the sanity checks in substTy catch are described in +-- Note [The substitution invariant]. +-- The goal of #11371 is to migrate all the calls of substTyUnchecked to +-- substTy and remove this function. Please don't use in new code. +substTyWithUnchecked :: [TyVar] -> [Type] -> Type -> Type +substTyWithUnchecked tvs tys + = ASSERT( tvs `equalLength` tys ) + substTyUnchecked (zipTvSubst tvs tys) + +-- | Substitute tyvars within a type using a known 'InScopeSet'. +-- Pre-condition: the 'in_scope' set should satisfy Note [The substitution +-- invariant]; specifically it should include the free vars of 'tys', +-- and of 'ty' minus the domain of the subst. +substTyWithInScope :: InScopeSet -> [TyVar] -> [Type] -> Type -> Type +substTyWithInScope in_scope tvs tys ty = + ASSERT( tvs `equalLength` tys ) + substTy (mkTvSubst in_scope tenv) ty + where tenv = zipTyEnv tvs tys + +-- | Coercion substitution, see 'zipTvSubst' +substCoWith :: HasCallStack => [TyVar] -> [Type] -> Coercion -> Coercion +substCoWith tvs tys = ASSERT( tvs `equalLength` tys ) + substCo (zipTvSubst tvs tys) + +-- | Coercion substitution, see 'zipTvSubst'. Disables sanity checks. +-- The problems that the sanity checks in substCo catch are described in +-- Note [The substitution invariant]. +-- The goal of #11371 is to migrate all the calls of substCoUnchecked to +-- substCo and remove this function. Please don't use in new code. +substCoWithUnchecked :: [TyVar] -> [Type] -> Coercion -> Coercion +substCoWithUnchecked tvs tys + = ASSERT( tvs `equalLength` tys ) + substCoUnchecked (zipTvSubst tvs tys) + + + +-- | Substitute covars within a type +substTyWithCoVars :: [CoVar] -> [Coercion] -> Type -> Type +substTyWithCoVars cvs cos = substTy (zipCvSubst cvs cos) + +-- | Type substitution, see 'zipTvSubst' +substTysWith :: [TyVar] -> [Type] -> [Type] -> [Type] +substTysWith tvs tys = ASSERT( tvs `equalLength` tys ) + substTys (zipTvSubst tvs tys) + +-- | Type substitution, see 'zipTvSubst' +substTysWithCoVars :: [CoVar] -> [Coercion] -> [Type] -> [Type] +substTysWithCoVars cvs cos = ASSERT( cvs `equalLength` cos ) + substTys (zipCvSubst cvs cos) + +-- | Substitute within a 'Type' after adding the free variables of the type +-- to the in-scope set. This is useful for the case when the free variables +-- aren't already in the in-scope set or easily available. +-- See also Note [The substitution invariant]. +substTyAddInScope :: TCvSubst -> Type -> Type +substTyAddInScope subst ty = + substTy (extendTCvInScopeSet subst $ tyCoVarsOfType ty) ty + +-- | When calling `substTy` it should be the case that the in-scope set in +-- the substitution is a superset of the free vars of the range of the +-- substitution. +-- See also Note [The substitution invariant]. +isValidTCvSubst :: TCvSubst -> Bool +isValidTCvSubst (TCvSubst in_scope tenv cenv) = + (tenvFVs `varSetInScope` in_scope) && + (cenvFVs `varSetInScope` in_scope) + where + tenvFVs = tyCoVarsOfTypesSet tenv + cenvFVs = tyCoVarsOfCosSet cenv + +-- | This checks if the substitution satisfies the invariant from +-- Note [The substitution invariant]. +checkValidSubst :: HasCallStack => TCvSubst -> [Type] -> [Coercion] -> a -> a +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 "cenv" <+> ppr cenv $$ + text "cenvFVs" <+> ppr (tyCoVarsOfCosSet cenv) $$ + text "tys" <+> ppr tys $$ + text "cos" <+> ppr cos ) + ASSERT2( tysCosFVsInScope, + text "in_scope" <+> ppr in_scope $$ + text "tenv" <+> ppr tenv $$ + text "cenv" <+> ppr cenv $$ + text "tys" <+> ppr tys $$ + text "cos" <+> ppr cos $$ + text "needInScope" <+> ppr needInScope ) + a + where + 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 + tysCosFVsInScope = needInScope `varSetInScope` in_scope + + +-- | Substitute within a 'Type' +-- The substitution has to satisfy the invariants described in +-- Note [The substitution invariant]. +substTy :: HasCallStack => TCvSubst -> Type -> Type +substTy subst ty + | isEmptyTCvSubst subst = ty + | otherwise = checkValidSubst subst [ty] [] $ + subst_ty subst ty + +-- | Substitute within a 'Type' disabling the sanity checks. +-- The problems that the sanity checks in substTy catch are described in +-- Note [The substitution invariant]. +-- The goal of #11371 is to migrate all the calls of substTyUnchecked to +-- substTy and remove this function. Please don't use in new code. +substTyUnchecked :: TCvSubst -> Type -> Type +substTyUnchecked subst ty + | isEmptyTCvSubst subst = ty + | otherwise = subst_ty subst ty + +-- | Substitute within several 'Type's +-- The substitution has to satisfy the invariants described in +-- Note [The substitution invariant]. +substTys :: HasCallStack => TCvSubst -> [Type] -> [Type] +substTys subst tys + | isEmptyTCvSubst subst = tys + | otherwise = checkValidSubst subst tys [] $ map (subst_ty subst) tys + +-- | Substitute within several 'Type's disabling the sanity checks. +-- The problems that the sanity checks in substTys catch are described in +-- Note [The substitution invariant]. +-- The goal of #11371 is to migrate all the calls of substTysUnchecked to +-- substTys and remove this function. Please don't use in new code. +substTysUnchecked :: TCvSubst -> [Type] -> [Type] +substTysUnchecked subst tys + | isEmptyTCvSubst subst = tys + | otherwise = map (subst_ty subst) tys + +-- | Substitute within a 'ThetaType' +-- The substitution has to satisfy the invariants described in +-- Note [The substitution invariant]. +substTheta :: HasCallStack => TCvSubst -> ThetaType -> ThetaType +substTheta = substTys + +-- | Substitute within a 'ThetaType' disabling the sanity checks. +-- The problems that the sanity checks in substTys catch are described in +-- Note [The substitution invariant]. +-- The goal of #11371 is to migrate all the calls of substThetaUnchecked to +-- substTheta and remove this function. Please don't use in new code. +substThetaUnchecked :: TCvSubst -> ThetaType -> ThetaType +substThetaUnchecked = substTysUnchecked + + +subst_ty :: TCvSubst -> Type -> Type +-- subst_ty is the main workhorse for type substitution +-- +-- Note that the in_scope set is poked only if we hit a forall +-- so it may often never be fully computed +subst_ty subst ty + = go ty + where + go (TyVarTy tv) = substTyVar subst tv + go (AppTy fun arg) = mkAppTy (go fun) $! (go arg) + -- The mkAppTy smart constructor is important + -- we might be replacing (a Int), represented with App + -- by [Int], represented with TyConApp + go (TyConApp tc tys) = let args = map go tys + in args `seqList` TyConApp tc args + go ty@(FunTy { ft_arg = arg, ft_res = res }) + = let !arg' = go arg + !res' = go res + in ty { ft_arg = arg', ft_res = res' } + go (ForAllTy (Bndr tv vis) ty) + = case substVarBndrUnchecked subst tv of + (subst', tv') -> + (ForAllTy $! ((Bndr $! tv') vis)) $! + (subst_ty subst' ty) + go (LitTy n) = LitTy $! n + go (CastTy ty co) = (mkCastTy $! (go ty)) $! (subst_co subst co) + go (CoercionTy co) = CoercionTy $! (subst_co subst co) + +substTyVar :: TCvSubst -> TyVar -> Type +substTyVar (TCvSubst _ tenv _) tv + = ASSERT( isTyVar tv ) + case lookupVarEnv tenv tv of + Just ty -> ty + Nothing -> TyVarTy tv + +substTyVars :: TCvSubst -> [TyVar] -> [Type] +substTyVars subst = map $ substTyVar subst + +substTyCoVars :: TCvSubst -> [TyCoVar] -> [Type] +substTyCoVars subst = map $ substTyCoVar subst + +substTyCoVar :: TCvSubst -> TyCoVar -> Type +substTyCoVar subst tv + | isTyVar tv = substTyVar subst tv + | otherwise = CoercionTy $ substCoVar subst tv + +lookupTyVar :: TCvSubst -> TyVar -> Maybe Type + -- See Note [Extending the TCvSubst] +lookupTyVar (TCvSubst _ tenv _) tv + = ASSERT( isTyVar tv ) + lookupVarEnv tenv tv + +-- | Substitute within a 'Coercion' +-- The substitution has to satisfy the invariants described in +-- Note [The substitution invariant]. +substCo :: HasCallStack => TCvSubst -> Coercion -> Coercion +substCo subst co + | isEmptyTCvSubst subst = co + | otherwise = checkValidSubst subst [] [co] $ subst_co subst co + +-- | Substitute within a 'Coercion' disabling sanity checks. +-- The problems that the sanity checks in substCo catch are described in +-- Note [The substitution invariant]. +-- The goal of #11371 is to migrate all the calls of substCoUnchecked to +-- substCo and remove this function. Please don't use in new code. +substCoUnchecked :: TCvSubst -> Coercion -> Coercion +substCoUnchecked subst co + | isEmptyTCvSubst subst = co + | otherwise = subst_co subst co + +-- | Substitute within several 'Coercion's +-- The substitution has to satisfy the invariants described in +-- Note [The substitution invariant]. +substCos :: HasCallStack => TCvSubst -> [Coercion] -> [Coercion] +substCos subst cos + | isEmptyTCvSubst subst = cos + | otherwise = checkValidSubst subst [] cos $ map (subst_co subst) cos + +subst_co :: TCvSubst -> Coercion -> Coercion +subst_co subst co + = go co + where + go_ty :: Type -> Type + go_ty = subst_ty subst + + go_mco :: MCoercion -> MCoercion + go_mco MRefl = MRefl + go_mco (MCo co) = MCo (go co) + + go :: Coercion -> Coercion + go (Refl ty) = mkNomReflCo $! (go_ty ty) + go (GRefl r ty mco) = (mkGReflCo r $! (go_ty ty)) $! (go_mco mco) + go (TyConAppCo r tc args)= let args' = map go args + in args' `seqList` mkTyConAppCo r tc args' + go (AppCo co arg) = (mkAppCo $! go co) $! go arg + go (ForAllCo tv kind_co co) + = case substForAllCoBndrUnchecked subst tv kind_co of + (subst', tv', kind_co') -> + ((mkForAllCo $! tv') $! kind_co') $! subst_co subst' co + go (FunCo r co1 co2) = (mkFunCo r $! go co1) $! go co2 + go (CoVarCo cv) = substCoVar subst cv + go (AxiomInstCo con ind cos) = mkAxiomInstCo con ind $! map go cos + go (UnivCo p r t1 t2) = (((mkUnivCo $! go_prov p) $! r) $! + (go_ty t1)) $! (go_ty t2) + go (SymCo co) = mkSymCo $! (go co) + go (TransCo co1 co2) = (mkTransCo $! (go co1)) $! (go co2) + go (NthCo r d co) = mkNthCo r d $! (go co) + go (LRCo lr co) = mkLRCo lr $! (go co) + go (InstCo co arg) = (mkInstCo $! (go co)) $! go arg + go (KindCo co) = mkKindCo $! (go co) + go (SubCo co) = mkSubCo $! (go co) + go (AxiomRuleCo c cs) = let cs1 = map go cs + in cs1 `seqList` AxiomRuleCo c cs1 + go (HoleCo h) = HoleCo $! go_hole h + + go_prov UnsafeCoerceProv = UnsafeCoerceProv + go_prov (PhantomProv kco) = PhantomProv (go kco) + go_prov (ProofIrrelProv kco) = ProofIrrelProv (go kco) + go_prov p@(PluginProv _) = p + + -- See Note [Substituting in a coercion hole] + go_hole h@(CoercionHole { ch_co_var = cv }) + = h { ch_co_var = updateVarType go_ty cv } + +substForAllCoBndr :: TCvSubst -> TyCoVar -> KindCoercion + -> (TCvSubst, TyCoVar, Coercion) +substForAllCoBndr subst + = substForAllCoBndrUsing False (substCo subst) subst + +-- | Like 'substForAllCoBndr', but disables sanity checks. +-- The problems that the sanity checks in substCo catch are described in +-- Note [The substitution invariant]. +-- The goal of #11371 is to migrate all the calls of substCoUnchecked to +-- substCo and remove this function. Please don't use in new code. +substForAllCoBndrUnchecked :: TCvSubst -> TyCoVar -> KindCoercion + -> (TCvSubst, TyCoVar, Coercion) +substForAllCoBndrUnchecked subst + = substForAllCoBndrUsing False (substCoUnchecked subst) subst + +-- See Note [Sym and ForAllCo] +substForAllCoBndrUsing :: Bool -- apply sym to binder? + -> (Coercion -> Coercion) -- transformation to kind co + -> TCvSubst -> TyCoVar -> KindCoercion + -> (TCvSubst, TyCoVar, KindCoercion) +substForAllCoBndrUsing sym sco subst old_var + | isTyVar old_var = substForAllCoTyVarBndrUsing sym sco subst old_var + | otherwise = substForAllCoCoVarBndrUsing sym sco subst old_var + +substForAllCoTyVarBndrUsing :: Bool -- apply sym to binder? + -> (Coercion -> Coercion) -- transformation to kind co + -> TCvSubst -> TyVar -> KindCoercion + -> (TCvSubst, TyVar, KindCoercion) +substForAllCoTyVarBndrUsing sym sco (TCvSubst in_scope tenv cenv) old_var old_kind_co + = ASSERT( isTyVar old_var ) + ( TCvSubst (in_scope `extendInScopeSet` new_var) new_env cenv + , new_var, new_kind_co ) + where + new_env | no_change && not sym = delVarEnv tenv old_var + | sym = extendVarEnv tenv old_var $ + TyVarTy new_var `CastTy` new_kind_co + | otherwise = extendVarEnv tenv old_var (TyVarTy new_var) + + no_kind_change = noFreeVarsOfCo old_kind_co + no_change = no_kind_change && (new_var == old_var) + + new_kind_co | no_kind_change = old_kind_co + | otherwise = sco old_kind_co + + Pair new_ki1 _ = coercionKind new_kind_co + -- We could do substitution to (tyVarKind old_var). We don't do so because + -- we already substituted new_kind_co, which contains the kind information + -- we want. We don't want to do substitution once more. Also, in most cases, + -- new_kind_co is a Refl, in which case coercionKind is really fast. + + new_var = uniqAway in_scope (setTyVarKind old_var new_ki1) + +substForAllCoCoVarBndrUsing :: Bool -- apply sym to binder? + -> (Coercion -> Coercion) -- transformation to kind co + -> TCvSubst -> CoVar -> KindCoercion + -> (TCvSubst, CoVar, KindCoercion) +substForAllCoCoVarBndrUsing sym sco (TCvSubst in_scope tenv cenv) + old_var old_kind_co + = ASSERT( isCoVar old_var ) + ( TCvSubst (in_scope `extendInScopeSet` new_var) tenv new_cenv + , new_var, new_kind_co ) + where + new_cenv | no_change && not sym = delVarEnv cenv old_var + | otherwise = extendVarEnv cenv old_var (mkCoVarCo new_var) + + no_kind_change = noFreeVarsOfCo old_kind_co + no_change = no_kind_change && (new_var == old_var) + + new_kind_co | no_kind_change = old_kind_co + | otherwise = sco old_kind_co + + Pair h1 h2 = coercionKind new_kind_co + + new_var = uniqAway in_scope $ mkCoVar (varName old_var) new_var_type + new_var_type | sym = h2 + | otherwise = h1 + +substCoVar :: TCvSubst -> CoVar -> Coercion +substCoVar (TCvSubst _ _ cenv) cv + = case lookupVarEnv cenv cv of + Just co -> co + Nothing -> CoVarCo cv + +substCoVars :: TCvSubst -> [CoVar] -> [Coercion] +substCoVars subst cvs = map (substCoVar subst) cvs + +lookupCoVar :: TCvSubst -> Var -> Maybe Coercion +lookupCoVar (TCvSubst _ _ cenv) v = lookupVarEnv cenv v + +substTyVarBndr :: HasCallStack => TCvSubst -> TyVar -> (TCvSubst, TyVar) +substTyVarBndr = substTyVarBndrUsing substTy + +substTyVarBndrs :: HasCallStack => TCvSubst -> [TyVar] -> (TCvSubst, [TyVar]) +substTyVarBndrs = mapAccumL substTyVarBndr + +substVarBndr :: HasCallStack => TCvSubst -> TyCoVar -> (TCvSubst, TyCoVar) +substVarBndr = substVarBndrUsing substTy + +substVarBndrs :: HasCallStack => TCvSubst -> [TyCoVar] -> (TCvSubst, [TyCoVar]) +substVarBndrs = mapAccumL substVarBndr + +substCoVarBndr :: HasCallStack => TCvSubst -> CoVar -> (TCvSubst, CoVar) +substCoVarBndr = substCoVarBndrUsing substTy + +-- | Like 'substVarBndr', but disables sanity checks. +-- The problems that the sanity checks in substTy catch are described in +-- Note [The substitution invariant]. +-- The goal of #11371 is to migrate all the calls of substTyUnchecked to +-- substTy and remove this function. Please don't use in new code. +substVarBndrUnchecked :: TCvSubst -> TyCoVar -> (TCvSubst, TyCoVar) +substVarBndrUnchecked = substVarBndrUsing substTyUnchecked + +substVarBndrUsing :: (TCvSubst -> Type -> Type) + -> TCvSubst -> TyCoVar -> (TCvSubst, TyCoVar) +substVarBndrUsing subst_fn subst v + | isTyVar v = substTyVarBndrUsing subst_fn subst v + | otherwise = substCoVarBndrUsing subst_fn subst v + +-- | Substitute a tyvar in a binding position, returning an +-- extended subst and a new tyvar. +-- Use the supplied function to substitute in the kind +substTyVarBndrUsing + :: (TCvSubst -> Type -> Type) -- ^ Use this to substitute in the kind + -> TCvSubst -> TyVar -> (TCvSubst, TyVar) +substTyVarBndrUsing subst_fn subst@(TCvSubst in_scope tenv cenv) old_var + = ASSERT2( _no_capture, pprTyVar old_var $$ pprTyVar new_var $$ ppr subst ) + ASSERT( isTyVar old_var ) + (TCvSubst (in_scope `extendInScopeSet` new_var) new_env cenv, new_var) + where + new_env | no_change = delVarEnv tenv old_var + | otherwise = extendVarEnv tenv old_var (TyVarTy new_var) + + _no_capture = not (new_var `elemVarSet` tyCoVarsOfTypesSet tenv) + -- Assertion check that we are not capturing something in the substitution + + old_ki = tyVarKind old_var + no_kind_change = noFreeVarsOfType old_ki -- verify that kind is closed + no_change = no_kind_change && (new_var == old_var) + -- no_change means that the new_var is identical in + -- all respects to the old_var (same unique, same kind) + -- See Note [Extending the TCvSubst] + -- + -- In that case we don't need to extend the substitution + -- to map old to new. But instead we must zap any + -- current substitution for the variable. For example: + -- (\x.e) with id_subst = [x |-> e'] + -- Here we must simply zap the substitution for x + + new_var | no_kind_change = uniqAway in_scope old_var + | otherwise = uniqAway in_scope $ + setTyVarKind old_var (subst_fn subst old_ki) + -- The uniqAway part makes sure the new variable is not already in scope + +-- | Substitute a covar in a binding position, returning an +-- extended subst and a new covar. +-- Use the supplied function to substitute in the kind +substCoVarBndrUsing + :: (TCvSubst -> Type -> Type) + -> TCvSubst -> CoVar -> (TCvSubst, CoVar) +substCoVarBndrUsing subst_fn subst@(TCvSubst in_scope tenv cenv) old_var + = ASSERT( isCoVar old_var ) + (TCvSubst (in_scope `extendInScopeSet` new_var) tenv new_cenv, new_var) + where + new_co = mkCoVarCo new_var + no_kind_change = noFreeVarsOfTypes [t1, t2] + no_change = new_var == old_var && no_kind_change + + new_cenv | no_change = delVarEnv cenv old_var + | otherwise = extendVarEnv cenv old_var new_co + + new_var = uniqAway in_scope subst_old_var + subst_old_var = mkCoVar (varName old_var) new_var_type + + (_, _, t1, t2, role) = coVarKindsTypesRole old_var + t1' = subst_fn subst t1 + t2' = subst_fn subst t2 + new_var_type = mkCoercionType role t1' t2' + -- It's important to do the substitution for coercions, + -- because they can have free type variables + +cloneTyVarBndr :: TCvSubst -> TyVar -> Unique -> (TCvSubst, TyVar) +cloneTyVarBndr subst@(TCvSubst in_scope tv_env cv_env) tv uniq + = ASSERT2( isTyVar tv, ppr tv ) -- I think it's only called on TyVars + (TCvSubst (extendInScopeSet in_scope tv') + (extendVarEnv tv_env tv (mkTyVarTy tv')) cv_env, tv') + where + old_ki = tyVarKind tv + no_kind_change = noFreeVarsOfType old_ki -- verify that kind is closed + + tv1 | no_kind_change = tv + | otherwise = setTyVarKind tv (substTy subst old_ki) + + tv' = setVarUnique tv1 uniq + +cloneTyVarBndrs :: TCvSubst -> [TyVar] -> UniqSupply -> (TCvSubst, [TyVar]) +cloneTyVarBndrs subst [] _usupply = (subst, []) +cloneTyVarBndrs subst (t:ts) usupply = (subst'', tv:tvs) + where + (uniq, usupply') = takeUniqFromSupply usupply + (subst' , tv ) = cloneTyVarBndr subst t uniq + (subst'', tvs) = cloneTyVarBndrs subst' ts usupply' + diff --git a/compiler/types/TyCoTidy.hs b/compiler/types/TyCoTidy.hs new file mode 100644 index 0000000000..5c0825a6fa --- /dev/null +++ b/compiler/types/TyCoTidy.hs @@ -0,0 +1,236 @@ +{-# LANGUAGE BangPatterns #-} + +-- | Tidying types and coercions for printing in error messages. +module TyCoTidy + ( + -- * Tidying type related things up for printing + tidyType, tidyTypes, + tidyOpenType, tidyOpenTypes, + tidyOpenKind, + tidyVarBndr, tidyVarBndrs, tidyFreeTyCoVars, avoidNameClashes, + tidyOpenTyCoVar, tidyOpenTyCoVars, + tidyTyCoVarOcc, + tidyTopType, + tidyKind, + tidyCo, tidyCos, + tidyTyCoVarBinder, tidyTyCoVarBinders + ) where + +import GhcPrelude + +import TyCoRep +import TyCoFVs (tyCoVarsOfTypesWellScoped, tyCoVarsOfTypeList) + +import Name hiding (varName) +import Var +import VarEnv +import Util (seqList) + +import Data.List + +{- +%************************************************************************ +%* * +\subsection{TidyType} +%* * +%************************************************************************ +-} + +-- | This tidies up a type for printing in an error message, or in +-- an interface file. +-- +-- It doesn't change the uniques at all, just the print names. +tidyVarBndrs :: TidyEnv -> [TyCoVar] -> (TidyEnv, [TyCoVar]) +tidyVarBndrs tidy_env tvs + = mapAccumL tidyVarBndr (avoidNameClashes tvs tidy_env) tvs + +tidyVarBndr :: TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar) +tidyVarBndr tidy_env@(occ_env, subst) var + = case tidyOccName occ_env (getHelpfulOccName var) of + (occ_env', occ') -> ((occ_env', subst'), var') + where + subst' = extendVarEnv subst var var' + var' = setVarType (setVarName var name') type' + type' = tidyType tidy_env (varType var) + name' = tidyNameOcc name occ' + name = varName var + +avoidNameClashes :: [TyCoVar] -> TidyEnv -> TidyEnv +-- Seed the occ_env with clashes among the names, see +-- Note [Tidying multiple names at once] in OccName +avoidNameClashes tvs (occ_env, subst) + = (avoidClashesOccEnv occ_env occs, subst) + where + occs = map getHelpfulOccName tvs + +getHelpfulOccName :: TyCoVar -> OccName +-- A TcTyVar with a System Name is probably a +-- unification variable; when we tidy them we give them a trailing +-- "0" (or 1 etc) so that they don't take precedence for the +-- un-modified name. Plus, indicating a unification variable in +-- this way is a helpful clue for users +getHelpfulOccName tv + | isSystemName name, isTcTyVar tv + = mkTyVarOcc (occNameString occ ++ "0") + | otherwise + = occ + where + name = varName tv + occ = getOccName name + +tidyTyCoVarBinder :: TidyEnv -> VarBndr TyCoVar vis + -> (TidyEnv, VarBndr TyCoVar vis) +tidyTyCoVarBinder tidy_env (Bndr tv vis) + = (tidy_env', Bndr tv' vis) + where + (tidy_env', tv') = tidyVarBndr tidy_env tv + +tidyTyCoVarBinders :: TidyEnv -> [VarBndr TyCoVar vis] + -> (TidyEnv, [VarBndr TyCoVar vis]) +tidyTyCoVarBinders tidy_env tvbs + = mapAccumL tidyTyCoVarBinder + (avoidNameClashes (binderVars tvbs) tidy_env) tvbs + +--------------- +tidyFreeTyCoVars :: TidyEnv -> [TyCoVar] -> TidyEnv +-- ^ Add the free 'TyVar's to the env in tidy form, +-- so that we can tidy the type they are free in +tidyFreeTyCoVars (full_occ_env, var_env) tyvars + = fst (tidyOpenTyCoVars (full_occ_env, var_env) tyvars) + +--------------- +tidyOpenTyCoVars :: TidyEnv -> [TyCoVar] -> (TidyEnv, [TyCoVar]) +tidyOpenTyCoVars env tyvars = mapAccumL tidyOpenTyCoVar env tyvars + +--------------- +tidyOpenTyCoVar :: TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar) +-- ^ Treat a new 'TyCoVar' as a binder, and give it a fresh tidy name +-- using the environment if one has not already been allocated. See +-- also 'tidyVarBndr' +tidyOpenTyCoVar env@(_, subst) tyvar + = case lookupVarEnv subst tyvar of + Just tyvar' -> (env, tyvar') -- Already substituted + Nothing -> + let env' = tidyFreeTyCoVars env (tyCoVarsOfTypeList (tyVarKind tyvar)) + in tidyVarBndr env' tyvar -- Treat it as a binder + +--------------- +tidyTyCoVarOcc :: TidyEnv -> TyCoVar -> TyCoVar +tidyTyCoVarOcc env@(_, subst) tv + = case lookupVarEnv subst tv of + Nothing -> updateVarType (tidyType env) tv + Just tv' -> tv' + +--------------- +tidyTypes :: TidyEnv -> [Type] -> [Type] +tidyTypes env tys = map (tidyType env) tys + +--------------- +tidyType :: TidyEnv -> Type -> Type +tidyType _ (LitTy n) = LitTy n +tidyType env (TyVarTy tv) = TyVarTy (tidyTyCoVarOcc env tv) +tidyType env (TyConApp tycon tys) = let args = tidyTypes env tys + in args `seqList` TyConApp tycon args +tidyType env (AppTy fun arg) = (AppTy $! (tidyType env fun)) $! (tidyType env arg) +tidyType env ty@(FunTy _ arg res) = let { !arg' = tidyType env arg + ; !res' = tidyType env res } + in ty { ft_arg = arg', ft_res = res' } +tidyType env (ty@(ForAllTy{})) = mkForAllTys' (zip tvs' vis) $! tidyType env' body_ty + where + (tvs, vis, body_ty) = splitForAllTys' ty + (env', tvs') = tidyVarBndrs env tvs +tidyType env (CastTy ty co) = (CastTy $! tidyType env ty) $! (tidyCo env co) +tidyType env (CoercionTy co) = CoercionTy $! (tidyCo env co) + + +-- The following two functions differ from mkForAllTys and splitForAllTys in that +-- they expect/preserve the ArgFlag argument. Thes belong to types/Type.hs, but +-- how should they be named? +mkForAllTys' :: [(TyCoVar, ArgFlag)] -> Type -> Type +mkForAllTys' tvvs ty = foldr strictMkForAllTy ty tvvs + where + strictMkForAllTy (tv,vis) ty = (ForAllTy $! ((Bndr $! tv) $! vis)) $! ty + +splitForAllTys' :: Type -> ([TyCoVar], [ArgFlag], Type) +splitForAllTys' ty = go ty [] [] + where + go (ForAllTy (Bndr tv vis) ty) tvs viss = go ty (tv:tvs) (vis:viss) + go ty tvs viss = (reverse tvs, reverse viss, ty) + + +--------------- +-- | Grabs the free type variables, tidies them +-- and then uses 'tidyType' to work over the type itself +tidyOpenTypes :: TidyEnv -> [Type] -> (TidyEnv, [Type]) +tidyOpenTypes env tys + = (env', tidyTypes (trimmed_occ_env, var_env) tys) + where + (env'@(_, var_env), tvs') = tidyOpenTyCoVars env $ + tyCoVarsOfTypesWellScoped tys + trimmed_occ_env = initTidyOccEnv (map getOccName tvs') + -- The idea here was that we restrict the new TidyEnv to the + -- _free_ vars of the types, so that we don't gratuitously rename + -- the _bound_ variables of the types. + +--------------- +tidyOpenType :: TidyEnv -> Type -> (TidyEnv, Type) +tidyOpenType env ty = let (env', [ty']) = tidyOpenTypes env [ty] in + (env', ty') + +--------------- +-- | Calls 'tidyType' on a top-level type (i.e. with an empty tidying environment) +tidyTopType :: Type -> Type +tidyTopType ty = tidyType emptyTidyEnv ty + +--------------- +tidyOpenKind :: TidyEnv -> Kind -> (TidyEnv, Kind) +tidyOpenKind = tidyOpenType + +tidyKind :: TidyEnv -> Kind -> Kind +tidyKind = tidyType + +---------------- +tidyCo :: TidyEnv -> Coercion -> Coercion +tidyCo env@(_, subst) co + = go co + where + go_mco MRefl = MRefl + go_mco (MCo co) = MCo (go co) + + go (Refl ty) = Refl (tidyType env ty) + go (GRefl r ty mco) = GRefl r (tidyType env ty) $! go_mco mco + go (TyConAppCo r tc cos) = let args = map go cos + in args `seqList` TyConAppCo r tc args + go (AppCo co1 co2) = (AppCo $! go co1) $! go co2 + go (ForAllCo tv h co) = ((ForAllCo $! tvp) $! (go h)) $! (tidyCo envp co) + where (envp, tvp) = tidyVarBndr env tv + -- the case above duplicates a bit of work in tidying h and the kind + -- of tv. But the alternative is to use coercionKind, which seems worse. + go (FunCo r co1 co2) = (FunCo r $! go co1) $! go co2 + go (CoVarCo cv) = case lookupVarEnv subst cv of + Nothing -> CoVarCo cv + Just cv' -> CoVarCo cv' + go (HoleCo h) = HoleCo h + go (AxiomInstCo con ind cos) = let args = map go cos + in args `seqList` AxiomInstCo con ind args + go (UnivCo p r t1 t2) = (((UnivCo $! (go_prov p)) $! r) $! + tidyType env t1) $! tidyType env t2 + go (SymCo co) = SymCo $! go co + go (TransCo co1 co2) = (TransCo $! go co1) $! go co2 + go (NthCo r d co) = NthCo r d $! go co + go (LRCo lr co) = LRCo lr $! go co + go (InstCo co ty) = (InstCo $! go co) $! go ty + go (KindCo co) = KindCo $! go co + go (SubCo co) = SubCo $! go co + go (AxiomRuleCo ax cos) = let cos1 = tidyCos env cos + in cos1 `seqList` AxiomRuleCo ax cos1 + + go_prov UnsafeCoerceProv = UnsafeCoerceProv + go_prov (PhantomProv co) = PhantomProv (go co) + go_prov (ProofIrrelProv co) = ProofIrrelProv (go co) + go_prov p@(PluginProv _) = p + +tidyCos :: TidyEnv -> [Coercion] -> [Coercion] +tidyCos env = map (tidyCo env) + + diff --git a/compiler/types/TyCon.hs b/compiler/types/TyCon.hs index 646399f484..d3977aaecb 100644 --- a/compiler/types/TyCon.hs +++ b/compiler/types/TyCon.hs @@ -132,7 +132,8 @@ module TyCon( import GhcPrelude -import {-# SOURCE #-} TyCoRep ( Kind, Type, PredType, pprType, mkForAllTy, mkFunTy ) +import {-# SOURCE #-} TyCoRep ( Kind, Type, PredType, mkForAllTy, mkFunTy ) +import {-# SOURCE #-} TyCoPpr ( pprType ) import {-# SOURCE #-} TysWiredIn ( runtimeRepTyCon, constraintKind , vecCountTyCon, vecElemTyCon, liftedTypeKind ) import {-# SOURCE #-} DataCon ( DataCon, dataConExTyCoVars, dataConFieldLabels diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs index 20a064b6b1..0400a31ae1 100644 --- a/compiler/types/Type.hs +++ b/compiler/types/Type.hs @@ -214,7 +214,7 @@ module Type ( pprTheta, pprThetaArrowTy, pprClassPred, pprKind, pprParendKind, pprSourceTyCon, PprPrec(..), topPrec, sigPrec, opPrec, funPrec, appPrec, maybeParen, - pprTyVar, pprTyVars, + pprTyVar, pprTyVars, debugPprType, pprWithTYPE, -- * Tidying type related things up for printing @@ -240,6 +240,10 @@ import BasicTypes import Kind import TyCoRep +import TyCoSubst +import TyCoTidy +import TyCoPpr +import TyCoFVs -- friends: import Var @@ -365,7 +369,7 @@ tcView (TyConApp tc tys) | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc tys = Just (mkAppTys (substTy (mkTvSubstPrs tenv) rhs) tys') -- The free vars of 'rhs' should all be bound by 'tenv', so it's -- ok to use 'substTy' here. - -- See also Note [The substitution invariant] in TyCoRep. + -- See also Note [The substitution invariant] in TyCoSubst. -- Its important to use mkAppTys, rather than (foldl AppTy), -- because the function part might well return a -- partially-applied type constructor; indeed, usually will! @@ -2105,108 +2109,6 @@ predTypeEqRel ty | otherwise = NomEq -{- -%************************************************************************ -%* * - Well-scoped tyvars -* * -************************************************************************ - -Note [ScopedSort] -~~~~~~~~~~~~~~~~~ -Consider - - foo :: Proxy a -> Proxy (b :: k) -> Proxy (a :: k2) -> () - -This function type is implicitly generalised over [a, b, k, k2]. These -variables will be Specified; that is, they will be available for visible -type application. This is because they are written in the type signature -by the user. - -However, we must ask: what order will they appear in? In cases without -dependency, this is easy: we just use the lexical left-to-right ordering -of first occurrence. With dependency, we cannot get off the hook so -easily. - -We thus state: - - * These variables appear in the order as given by ScopedSort, where - the input to ScopedSort is the left-to-right order of first occurrence. - -Note that this applies only to *implicit* quantification, without a -`forall`. If the user writes a `forall`, then we just use the order given. - -ScopedSort is defined thusly (as proposed in #15743): - * Work left-to-right through the input list, with a cursor. - * If variable v at the cursor is depended on by any earlier variable w, - move v immediately before the leftmost such w. - -INVARIANT: The prefix of variables before the cursor form a valid telescope. - -Note that ScopedSort makes sense only after type inference is done and all -types/kinds are fully settled and zonked. - --} - --- | Do a topological sort on a list of tyvars, --- so that binders occur before occurrences --- E.g. given [ a::k, k::*, b::k ] --- it'll return a well-scoped list [ k::*, a::k, b::k ] --- --- This is a deterministic sorting operation --- (that is, doesn't depend on Uniques). --- --- It is also meant to be stable: that is, variables should not --- be reordered unnecessarily. This is specified in Note [ScopedSort] --- See also Note [Ordering of implicit variables] in RnTypes - -scopedSort :: [TyCoVar] -> [TyCoVar] -scopedSort = go [] [] - where - go :: [TyCoVar] -- already sorted, in reverse order - -> [TyCoVarSet] -- each set contains all the variables which must be placed - -- before the tv corresponding to the set; they are accumulations - -- of the fvs in the sorted tvs' kinds - - -- This list is in 1-to-1 correspondence with the sorted tyvars - -- INVARIANT: - -- all (\tl -> all (`subVarSet` head tl) (tail tl)) (tails fv_list) - -- That is, each set in the list is a superset of all later sets. - - -> [TyCoVar] -- yet to be sorted - -> [TyCoVar] - go acc _fv_list [] = reverse acc - go acc fv_list (tv:tvs) - = go acc' fv_list' tvs - where - (acc', fv_list') = insert tv acc fv_list - - insert :: TyCoVar -- var to insert - -> [TyCoVar] -- sorted list, in reverse order - -> [TyCoVarSet] -- list of fvs, as above - -> ([TyCoVar], [TyCoVarSet]) -- augmented lists - insert tv [] [] = ([tv], [tyCoVarsOfType (tyVarKind tv)]) - insert tv (a:as) (fvs:fvss) - | tv `elemVarSet` fvs - , (as', fvss') <- insert tv as fvss - = (a:as', fvs `unionVarSet` fv_tv : fvss') - - | otherwise - = (tv:a:as, fvs `unionVarSet` fv_tv : fvs : fvss) - where - fv_tv = tyCoVarsOfType (tyVarKind tv) - - -- lists not in correspondence - insert _ _ _ = panic "scopedSort" - --- | Get the free vars of a type in scoped order -tyCoVarsOfTypeWellScoped :: Type -> [TyVar] -tyCoVarsOfTypeWellScoped = scopedSort . tyCoVarsOfTypeList - --- | Get the free vars of types in scoped order -tyCoVarsOfTypesWellScoped :: [Type] -> [TyVar] -tyCoVarsOfTypesWellScoped = scopedSort . tyCoVarsOfTypesList - ------------- Closing over kinds ----------------- -- | Add the kind variables free in the kinds of the tyvars in the given set. diff --git a/compiler/types/Type.hs-boot b/compiler/types/Type.hs-boot index d9ea519a08..4e2a498620 100644 --- a/compiler/types/Type.hs-boot +++ b/compiler/types/Type.hs-boot @@ -4,7 +4,6 @@ module Type where import GhcPrelude import TyCon -import Var ( TyCoVar ) import {-# SOURCE #-} TyCoRep( Type, Coercion ) import Util @@ -20,7 +19,4 @@ eqType :: Type -> Type -> Bool coreView :: Type -> Maybe Type tcView :: Type -> Maybe Type -tyCoVarsOfTypesWellScoped :: [Type] -> [TyCoVar] -tyCoVarsOfTypeWellScoped :: Type -> [TyCoVar] -scopedSort :: [TyCoVar] -> [TyCoVar] splitTyConApp_maybe :: HasDebugCallStack => Type -> Maybe (TyCon, [Type]) diff --git a/compiler/types/Unify.hs b/compiler/types/Unify.hs index b7ce569490..3b052f14d4 100644 --- a/compiler/types/Unify.hs +++ b/compiler/types/Unify.hs @@ -35,7 +35,9 @@ import Name( Name ) import Type hiding ( getTvSubstEnv ) import Coercion hiding ( getCvSubstEnv ) import TyCon -import TyCoRep hiding ( getTvSubstEnv, getCvSubstEnv ) +import TyCoRep +import TyCoFVs ( tyCoVarsOfCoList, tyCoFVsOfTypes ) +import TyCoSubst ( mkTvSubst ) import FV( FV, fvVarSet, fvVarList ) import Util import Pair |