{- (c) The University of Glasgow 2006 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998 \section{@Vars@: Variables} -} {-# LANGUAGE FlexibleContexts, MultiWayIf, FlexibleInstances, DeriveDataTypeable, PatternSynonyms, BangPatterns #-} {-# OPTIONS_GHC -Wno-incomplete-record-updates #-} -- | -- #name_types# -- GHC uses several kinds of name internally: -- -- * 'GHC.Types.Name.Occurrence.OccName': see "GHC.Types.Name.Occurrence#name_types" -- -- * 'GHC.Types.Name.Reader.RdrName': see "GHC.Types.Name.Reader#name_types" -- -- * 'GHC.Types.Name.Name': see "GHC.Types.Name#name_types" -- -- * 'GHC.Types.Id.Id': see "GHC.Types.Id#name_types" -- -- * 'GHC.Types.Var.Var' is a synonym for the 'GHC.Types.Id.Id' type but it may additionally -- potentially contain type variables, which have a 'GHC.Core.TyCo.Rep.Kind' -- rather than a 'GHC.Core.TyCo.Rep.Type' and only contain some extra -- details during typechecking. -- -- These 'Var' names may either be global or local, see "GHC.Types.Var#globalvslocal" -- -- #globalvslocal# -- Global 'Id's and 'Var's are those that are imported or correspond -- to a data constructor, primitive operation, or record selectors. -- Local 'Id's and 'Var's are those bound within an expression -- (e.g. by a lambda) or at the top level of the module being compiled. module GHC.Types.Var ( -- * The main data type and synonyms Var, CoVar, Id, NcId, DictId, DFunId, EvVar, EqVar, EvId, IpId, JoinId, TyVar, TcTyVar, TypeVar, KindVar, TKVar, TyCoVar, -- * In and Out variants InVar, InCoVar, InId, InTyVar, OutVar, OutCoVar, OutId, OutTyVar, -- ** Taking 'Var's apart varName, varUnique, varType, varMult, varMultMaybe, -- ** Modifying 'Var's setVarName, setVarUnique, setVarType, updateVarType, updateVarTypeM, -- ** Constructing, taking apart, modifying 'Id's mkGlobalVar, mkLocalVar, mkExportedLocalVar, mkCoVar, idInfo, idDetails, lazySetIdInfo, setIdDetails, globaliseId, setIdExported, setIdNotExported, setIdMult, updateIdTypeButNotMult, updateIdTypeAndMult, updateIdTypeAndMultM, -- ** Predicates isId, isTyVar, isTcTyVar, isLocalVar, isLocalId, isCoVar, isNonCoVarId, isTyCoVar, isGlobalId, isExportedId, mustHaveLocalBinding, -- * ForAllTyFlags ForAllTyFlag(Invisible,Required,Specified,Inferred), Specificity(..), isVisibleForAllTyFlag, isInvisibleForAllTyFlag, isInferredForAllTyFlag, -- * FunTyFlag FunTyFlag(..), isVisibleFunArg, isInvisibleFunArg, isFUNArg, mkFunTyFlag, visArg, invisArg, visArgTypeLike, visArgConstraintLike, invisArgTypeLike, invisArgConstraintLike, funTyFlagResultTypeOrConstraint, TypeOrConstraint(..), -- Re-export this: it's an argument of FunTyFlag -- * PiTyBinder PiTyBinder(..), PiTyVarBinder, isInvisiblePiTyBinder, isVisiblePiTyBinder, isTyBinder, isNamedPiTyBinder, isAnonPiTyBinder, namedPiTyBinder_maybe, anonPiTyBinderType_maybe, piTyBinderType, -- * TyVar's VarBndr(..), ForAllTyBinder, TyVarBinder, InvisTyBinder, InvisTVBinder, ReqTyBinder, ReqTVBinder, binderVar, binderVars, binderFlag, binderFlags, binderType, mkForAllTyBinder, mkForAllTyBinders, mkTyVarBinder, mkTyVarBinders, isTyVarBinder, tyVarSpecToBinder, tyVarSpecToBinders, tyVarReqToBinder, tyVarReqToBinders, mapVarBndr, mapVarBndrs, -- ** Constructing TyVar's mkTyVar, mkTcTyVar, -- ** Taking 'TyVar's apart tyVarName, tyVarKind, tcTyVarDetails, setTcTyVarDetails, -- ** Modifying 'TyVar's setTyVarName, setTyVarUnique, setTyVarKind, updateTyVarKind, updateTyVarKindM, nonDetCmpVar ) where import GHC.Prelude import {-# SOURCE #-} GHC.Core.TyCo.Rep( Type, Kind, Mult, Scaled, scaledThing ) import {-# SOURCE #-} GHC.Core.TyCo.Ppr( pprKind ) import {-# SOURCE #-} GHC.Tc.Utils.TcType( TcTyVarDetails, pprTcTyVarDetails, vanillaSkolemTvUnk ) import {-# SOURCE #-} GHC.Types.Id.Info( IdDetails, IdInfo, coVarDetails, isCoVarDetails, vanillaIdInfo, pprIdDetails ) import {-# SOURCE #-} GHC.Builtin.Types ( manyDataConTy ) import GHC.Types.Name hiding (varName) import GHC.Types.Unique ( Uniquable, Unique, getKey, getUnique , mkUniqueGrimily, nonDetCmpUnique ) import GHC.Types.Basic( TypeOrConstraint(..) ) import GHC.Utils.Misc import GHC.Utils.Binary import GHC.Utils.Outputable import GHC.Utils.Panic import GHC.Utils.Panic.Plain import Data.Data {- ************************************************************************ * * Synonyms * * ************************************************************************ -- These synonyms are here and not in Id because otherwise we need a very -- large number of SOURCE imports of "GHC.Types.Id" :-( -} -- | Identifier type Id = Var -- A term-level identifier -- predicate: isId -- | Coercion Variable type CoVar = Id -- See Note [Evidence: EvIds and CoVars] -- predicate: isCoVar -- | type NcId = Id -- A term-level (value) variable that is -- /not/ an (unlifted) coercion -- predicate: isNonCoVarId -- | Type or kind Variable type TyVar = Var -- Type *or* kind variable (historical) -- | Type or Kind Variable type TKVar = Var -- Type *or* kind variable (historical) -- | Type variable that might be a metavariable type TcTyVar = Var -- | Type Variable type TypeVar = Var -- Definitely a type variable -- | Kind Variable type KindVar = Var -- Definitely a kind variable -- See Note [Kind and type variables] -- See Note [Evidence: EvIds and CoVars] -- | Evidence Identifier type EvId = Id -- Term-level evidence: DictId, IpId, or EqVar -- | Evidence Variable type EvVar = EvId -- ...historical name for EvId -- | Dictionary Function Identifier type DFunId = Id -- A dictionary function -- | Dictionary Identifier type DictId = EvId -- A dictionary variable -- | Implicit parameter Identifier type IpId = EvId -- A term-level implicit parameter -- | Equality Variable type EqVar = EvId -- Boxed equality evidence type JoinId = Id -- A join variable -- | Type or Coercion Variable type TyCoVar = Id -- Type, *or* coercion variable -- predicate: isTyCoVar {- Many passes apply a substitution, and it's very handy to have type synonyms to remind us whether or not the substitution has been applied -} type InVar = Var type InTyVar = TyVar type InCoVar = CoVar type InId = Id type OutVar = Var type OutTyVar = TyVar type OutCoVar = CoVar type OutId = Id {- Note [Evidence: EvIds and CoVars] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ * An EvId (evidence Id) is a term-level evidence variable (dictionary, implicit parameter, or equality). Could be boxed or unboxed. * DictId, IpId, and EqVar are synonyms when we know what kind of evidence we are talking about. For example, an EqVar has type (t1 ~ t2). * A CoVar is always an un-lifted coercion, of type (t1 ~# t2) or (t1 ~R# t2) Note [Kind and type variables] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Before kind polymorphism, TyVar were used to mean type variables. Now they are used to mean kind *or* type variables. KindVar is used when we know for sure that it is a kind variable. In future, we might want to go over the whole compiler code to use: - TKVar to mean kind or type variables - TypeVar to mean type variables only - KindVar to mean kind variables ************************************************************************ * * \subsection{The main data type declarations} * * ************************************************************************ Every @Var@ has a @Unique@, to uniquify it and for fast comparison, a @Type@, and an @IdInfo@ (non-essential info about it, e.g., strictness). The essential info about different kinds of @Vars@ is in its @VarDetails@. -} -- | Variable -- -- Essentially a typed 'Name', that may also contain some additional information -- about the 'Var' and its use sites. data Var = TyVar { -- Type and kind variables -- see Note [Kind and type variables] varName :: !Name, realUnique :: {-# UNPACK #-} !Int, -- ^ Key for fast comparison -- Identical to the Unique in the name, -- cached here for speed varType :: Kind -- ^ The type or kind of the 'Var' in question } | TcTyVar { -- Used only during type inference -- Used for kind variables during -- inference, as well varName :: !Name, realUnique :: {-# UNPACK #-} !Int, varType :: Kind, tc_tv_details :: TcTyVarDetails } | Id { varName :: !Name, realUnique :: {-# UNPACK #-} !Int, varType :: Type, varMult :: Mult, -- See Note [Multiplicity of let binders] idScope :: IdScope, id_details :: IdDetails, -- Stable, doesn't change id_info :: IdInfo } -- Unstable, updated by simplifier -- | Identifier Scope data IdScope -- See Note [GlobalId/LocalId] = GlobalId | LocalId ExportFlag data ExportFlag -- See Note [ExportFlag on binders] = NotExported -- ^ Not exported: may be discarded as dead code. | Exported -- ^ Exported: kept alive {- Note [ExportFlag on binders] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ An ExportFlag of "Exported" on a top-level binder says "keep this binding alive; do not drop it as dead code". This transitively keeps alive all the other top-level bindings that this binding refers to. This property is persisted all the way down the pipeline, so that the binding will be compiled all the way to object code, and its symbols will appear in the linker symbol table. However, note that this use of "exported" is quite different to the export list on a Haskell module. Setting the ExportFlag on an Id does /not/ mean that if you import the module (in Haskell source code) you will see this Id. Of course, things that appear in the export list of the source Haskell module do indeed have their ExportFlag set. But many other things, such as dictionary functions, are kept alive by having their ExportFlag set, even though they are not exported in the source-code sense. We should probably use a different term for ExportFlag, like KeepAlive. Note [GlobalId/LocalId] ~~~~~~~~~~~~~~~~~~~~~~~ A GlobalId is * always a constant (top-level) * imported, or data constructor, or primop, or record selector * has a Unique that is globally unique across the whole GHC invocation (a single invocation may compile multiple modules) * never treated as a candidate by the free-variable finder; it's a constant! A LocalId is * bound within an expression (lambda, case, local let(rec)) * or defined at top level in the module being compiled * always treated as a candidate by the free-variable finder After CoreTidy, top-level LocalIds are turned into GlobalIds Note [Multiplicity of let binders] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ In Core, let-binders' multiplicity is always completely determined by syntax: a recursive let will always have multiplicity Many (it's a prerequisite for being recursive), and non-recursive let doesn't have a conventional multiplicity, instead they act, for the purpose of multiplicity, as an alias for their right-hand side. Therefore, the `varMult` field of identifier is only used by binders in lambda and case expressions. In a let expression the `varMult` field holds an arbitrary value which will (and must!) be ignored. -} instance Outputable Var where ppr var = sdocOption sdocSuppressVarKinds $ \supp_var_kinds -> getPprDebug $ \debug -> getPprStyle $ \sty -> let ppr_var = case var of (TyVar {}) | debug -> brackets (text "tv") (TcTyVar {tc_tv_details = d}) | dumpStyle sty || debug -> brackets (pprTcTyVarDetails d) (Id { idScope = s, id_details = d }) | debug -> brackets (ppr_id_scope s <> pprIdDetails d) _ -> empty in if | debug && (not supp_var_kinds) -> parens (ppr (varName var) <+> ppr (varMultMaybe var) <+> ppr_var <+> dcolon <+> pprKind (tyVarKind var)) | otherwise -> ppr (varName var) <> ppr_var ppr_id_scope :: IdScope -> SDoc ppr_id_scope GlobalId = text "gid" ppr_id_scope (LocalId Exported) = text "lidx" ppr_id_scope (LocalId NotExported) = text "lid" instance NamedThing Var where getName = varName instance Uniquable Var where getUnique = varUnique instance Eq Var where a == b = realUnique a == realUnique b instance Ord Var where a <= b = realUnique a <= realUnique b a < b = realUnique a < realUnique b a >= b = realUnique a >= realUnique b a > b = realUnique a > realUnique b a `compare` b = a `nonDetCmpVar` b -- | Compare Vars by their Uniques. -- This is what Ord Var does, provided here to make it explicit at the -- call-site that it can introduce non-determinism. -- See Note [Unique Determinism] nonDetCmpVar :: Var -> Var -> Ordering nonDetCmpVar a b = varUnique a `nonDetCmpUnique` varUnique b instance Data Var where -- don't traverse? toConstr _ = abstractConstr "Var" gunfold _ _ = error "gunfold" dataTypeOf _ = mkNoRepType "Var" instance HasOccName Var where occName = nameOccName . varName varUnique :: Var -> Unique varUnique var = mkUniqueGrimily (realUnique var) varMultMaybe :: Id -> Maybe Mult varMultMaybe (Id { varMult = mult }) = Just mult varMultMaybe _ = Nothing setVarUnique :: Var -> Unique -> Var setVarUnique var uniq = var { realUnique = getKey uniq, varName = setNameUnique (varName var) uniq } setVarName :: Var -> Name -> Var setVarName var new_name = var { realUnique = getKey (getUnique new_name), varName = new_name } setVarType :: Var -> Type -> Var setVarType id ty = id { varType = ty } -- | Update a 'Var's type. Does not update the /multiplicity/ -- stored in an 'Id', if any. Because of the possibility for -- abuse, ASSERTs that there is no multiplicity to update. updateVarType :: (Type -> Type) -> Var -> Var updateVarType upd var = case var of Id { id_details = details } -> assert (isCoVarDetails details) $ result _ -> result where result = var { varType = upd (varType var) } -- | Update a 'Var's type monadically. Does not update the /multiplicity/ -- stored in an 'Id', if any. Because of the possibility for -- abuse, ASSERTs that there is no multiplicity to update. updateVarTypeM :: Monad m => (Type -> m Type) -> Var -> m Var updateVarTypeM upd var = case var of Id { id_details = details } -> assert (isCoVarDetails details) $ result _ -> result where result = do { ty' <- upd (varType var) ; return (var { varType = ty' }) } {- ********************************************************************* * * * ForAllTyFlag * * ********************************************************************* -} -- | ForAllTyFlag -- -- Is something required to appear in source Haskell ('Required'), -- permitted by request ('Specified') (visible type application), or -- prohibited entirely from appearing in source Haskell ('Inferred')? -- See Note [VarBndrs, ForAllTyBinders, TyConBinders, and visibility] in "GHC.Core.TyCo.Rep" data ForAllTyFlag = Invisible Specificity | Required deriving (Eq, Ord, Data) -- (<) on ForAllTyFlag means "is less visible than" -- | Whether an 'Invisible' argument may appear in source Haskell. data Specificity = InferredSpec -- ^ the argument may not appear in source Haskell, it is -- only inferred. | SpecifiedSpec -- ^ the argument may appear in source Haskell, but isn't -- required. deriving (Eq, Ord, Data) pattern Inferred, Specified :: ForAllTyFlag pattern Inferred = Invisible InferredSpec pattern Specified = Invisible SpecifiedSpec {-# COMPLETE Required, Specified, Inferred #-} -- | Does this 'ForAllTyFlag' classify an argument that is written in Haskell? isVisibleForAllTyFlag :: ForAllTyFlag -> Bool isVisibleForAllTyFlag af = not (isInvisibleForAllTyFlag af) -- | Does this 'ForAllTyFlag' classify an argument that is not written in Haskell? isInvisibleForAllTyFlag :: ForAllTyFlag -> Bool isInvisibleForAllTyFlag (Invisible {}) = True isInvisibleForAllTyFlag Required = False isInferredForAllTyFlag :: ForAllTyFlag -> Bool -- More restrictive than isInvisibleForAllTyFlag isInferredForAllTyFlag (Invisible InferredSpec) = True isInferredForAllTyFlag _ = False instance Outputable ForAllTyFlag where ppr Required = text "[req]" ppr Specified = text "[spec]" ppr Inferred = text "[infrd]" instance Binary Specificity where put_ bh SpecifiedSpec = putByte bh 0 put_ bh InferredSpec = putByte bh 1 get bh = do h <- getByte bh case h of 0 -> return SpecifiedSpec _ -> return InferredSpec instance Binary ForAllTyFlag where put_ bh Required = putByte bh 0 put_ bh Specified = putByte bh 1 put_ bh Inferred = putByte bh 2 get bh = do h <- getByte bh case h of 0 -> return Required 1 -> return Specified _ -> return Inferred {- ********************************************************************* * * * FunTyFlag * * ********************************************************************* -} -- | The non-dependent version of 'ForAllTyFlag'. -- See Note [FunTyFlag] -- Appears here partly so that it's together with its friends ForAllTyFlag -- and ForallVisFlag, but also because it is used in IfaceType, rather -- early in the compilation chain data FunTyFlag = FTF_T_T -- (->) Type -> Type | FTF_T_C -- (-=>) Type -> Constraint | FTF_C_T -- (=>) Constraint -> Type | FTF_C_C -- (==>) Constraint -> Constraint deriving (Eq, Ord, Data) instance Outputable FunTyFlag where ppr FTF_T_T = text "[->]" ppr FTF_T_C = text "[-=>]" ppr FTF_C_T = text "[=>]" ppr FTF_C_C = text "[==>]" instance Binary FunTyFlag where put_ bh FTF_T_T = putByte bh 0 put_ bh FTF_T_C = putByte bh 1 put_ bh FTF_C_T = putByte bh 2 put_ bh FTF_C_C = putByte bh 3 get bh = do h <- getByte bh case h of 0 -> return FTF_T_T 1 -> return FTF_T_C 2 -> return FTF_C_T _ -> return FTF_C_C mkFunTyFlag :: TypeOrConstraint -> TypeOrConstraint -> FunTyFlag mkFunTyFlag TypeLike torc = visArg torc mkFunTyFlag ConstraintLike torc = invisArg torc visArg :: TypeOrConstraint -> FunTyFlag visArg TypeLike = FTF_T_T visArg ConstraintLike = FTF_T_C visArgTypeLike :: FunTyFlag visArgTypeLike = FTF_T_T visArgConstraintLike :: FunTyFlag visArgConstraintLike = FTF_T_C invisArg :: TypeOrConstraint -> FunTyFlag invisArg TypeLike = FTF_C_T invisArg ConstraintLike = FTF_C_C invisArgTypeLike :: FunTyFlag invisArgTypeLike = FTF_C_T invisArgConstraintLike :: FunTyFlag invisArgConstraintLike = FTF_C_C isInvisibleFunArg :: FunTyFlag -> Bool isInvisibleFunArg af = not (isVisibleFunArg af) isVisibleFunArg :: FunTyFlag -> Bool isVisibleFunArg FTF_T_T = True isVisibleFunArg FTF_T_C = True isVisibleFunArg _ = False isFUNArg :: FunTyFlag -> Bool -- This one, FUN, or (->), has an extra multiplicity argument isFUNArg FTF_T_T = True isFUNArg _ = False funTyFlagResultTypeOrConstraint :: FunTyFlag -> TypeOrConstraint -- Whether it /returns/ a type or a constraint funTyFlagResultTypeOrConstraint FTF_T_T = TypeLike funTyFlagResultTypeOrConstraint FTF_C_T = TypeLike funTyFlagResultTypeOrConstraint _ = ConstraintLike {- Note [FunTyFlag] ~~~~~~~~~~~~~~~~~~~~~ FunTyFlag is used principally in the FunTy constructor of Type. FunTy FTF_T_T t1 t2 means t1 -> t2 FunTy FTF_C_T t1 t2 means t1 => t2 FunTy FTF_T_C t1 t2 means t1 -=> t2 FunTy FTF_C_C t1 t2 means t1 ==> t2 However, the FunTyFlag in a FunTy is just redundant, cached information. In (FunTy { ft_af = af, ft_arg = t1, ft_res = t2 }) --------------------------------------------- (isPredTy t1) (isPredTy ty) FunTyFlag --------------------------------------------- False False FTF_T_T False True FTF_T_C True False FTF_C_T True True FTF_C_C where isPredTy is defined in GHC.Core.Type, and sees if t1's kind is Constraint. See GHC.Core.Type.chooseFunTyFlag, and GHC.Core.TyCo.Rep Note [Types for coercions, predicates, and evidence] The term (Lam b e) donesn't carry an FunTyFlag; instead it uses mkFunctionType when we want to get its types; see mkLamType. This is just an engineering choice; we could cache here too if we wanted. Why bother with all this? After all, we are in Core, where (=>) and (->) behave the same. We maintain this distinction throughout Core so that we can cheaply and conveniently determine * How to print a type * How to split up a type: tcSplitSigmaTy * How to specialise it (over type classes; GHC.Core.Opt.Specialise) For the specialisation point, consider (\ (d :: Ord a). blah). We want to give it type (Ord a => blah_ty) with a fat arrow; that is, using mkInvisFunTy, not mkVisFunTy. Why? Because the /specialiser/ treats dictionary arguments specially. Suppose we do w/w on 'foo', thus (#11272, #6056) foo :: Ord a => Int -> blah foo a d x = case x of I# x' -> $wfoo @a d x' $wfoo :: Ord a => Int# -> blah Now, at a call we see (foo @Int dOrdInt). The specialiser will specialise this to $sfoo, where $sfoo :: Int -> blah $sfoo x = case x of I# x' -> $wfoo @Int dOrdInt x' Now we /must/ also specialise $wfoo! But it wasn't user-written, and has a type built with mkLamTypes. Conclusion: the easiest thing is to make mkLamType build (c => ty) when the argument is a predicate type. See GHC.Core.TyCo.Rep Note [Types for coercions, predicates, and evidence] -} {- ********************************************************************* * * * VarBndr, ForAllTyBinder * * ********************************************************************* -} {- Note [The VarBndr type and its uses] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ VarBndr is polymorphic in both var and visibility fields. Currently there are nine different uses of 'VarBndr': * Var.ForAllTyBinder = VarBndr TyCoVar ForAllTyFlag Binder of a forall-type; see ForAllTy in GHC.Core.TyCo.Rep * Var.TyVarBinder = VarBndr TyVar ForAllTyFlag Subset of ForAllTyBinder when we are sure the binder is a TyVar * Var.InvisTVBinder = VarBndr TyVar Specificity Specialised form of TyVarBinder, when ForAllTyFlag = Invisible s See GHC.Core.Type.splitForAllInvisTVBinders * Var.ReqTVBinder = VarBndr TyVar () Specialised form of TyVarBinder, when ForAllTyFlag = Required See GHC.Core.Type.splitForAllReqTVBinders This one is barely used * TyCon.TyConBinder = VarBndr TyVar TyConBndrVis Binders of a TyCon; see TyCon in GHC.Core.TyCon * TyCon.TyConPiTyBinder = VarBndr TyCoVar TyConBndrVis Binders of a PromotedDataCon See Note [Promoted GADT data constructors] in GHC.Core.TyCon * IfaceType.IfaceForAllBndr = VarBndr IfaceBndr ForAllTyFlag * IfaceType.IfaceForAllSpecBndr = VarBndr IfaceBndr Specificity * IfaceType.IfaceTyConBinder = VarBndr IfaceBndr TyConBndrVis -} data VarBndr var argf = Bndr var argf -- See Note [The VarBndr type and its uses] deriving( Data ) -- | Variable Binder -- -- A 'ForAllTyBinder' is the binder of a ForAllTy -- It's convenient to define this synonym here rather its natural -- home in "GHC.Core.TyCo.Rep", because it's used in GHC.Core.DataCon.hs-boot -- -- A 'TyVarBinder' is a binder with only TyVar type ForAllTyBinder = VarBndr TyCoVar ForAllTyFlag type InvisTyBinder = VarBndr TyCoVar Specificity type ReqTyBinder = VarBndr TyCoVar () type TyVarBinder = VarBndr TyVar ForAllTyFlag type InvisTVBinder = VarBndr TyVar Specificity type ReqTVBinder = VarBndr TyVar () tyVarSpecToBinders :: [VarBndr a Specificity] -> [VarBndr a ForAllTyFlag] tyVarSpecToBinders = map tyVarSpecToBinder tyVarSpecToBinder :: VarBndr a Specificity -> VarBndr a ForAllTyFlag tyVarSpecToBinder (Bndr tv vis) = Bndr tv (Invisible vis) tyVarReqToBinders :: [VarBndr a ()] -> [VarBndr a ForAllTyFlag] tyVarReqToBinders = map tyVarReqToBinder tyVarReqToBinder :: VarBndr a () -> VarBndr a ForAllTyFlag tyVarReqToBinder (Bndr tv _) = Bndr tv Required binderVar :: VarBndr tv argf -> tv binderVar (Bndr v _) = v binderVars :: [VarBndr tv argf] -> [tv] binderVars tvbs = map binderVar tvbs binderFlag :: VarBndr tv argf -> argf binderFlag (Bndr _ argf) = argf binderFlags :: [VarBndr tv argf] -> [argf] binderFlags tvbs = map binderFlag tvbs binderType :: VarBndr TyCoVar argf -> Type binderType (Bndr tv _) = varType tv isTyVarBinder :: VarBndr TyCoVar vis -> Bool isTyVarBinder (Bndr tcv _) = isTyVar tcv -- | Make a named binder mkForAllTyBinder :: vis -> TyCoVar -> VarBndr TyCoVar vis mkForAllTyBinder vis var = Bndr var vis -- | Make a named binder -- 'var' should be a type variable mkTyVarBinder :: vis -> TyVar -> VarBndr TyVar vis mkTyVarBinder vis var = assert (isTyVar var) $ Bndr var vis -- | Make many named binders mkForAllTyBinders :: vis -> [TyCoVar] -> [VarBndr TyCoVar vis] mkForAllTyBinders vis = map (mkForAllTyBinder vis) -- | Make many named binders -- Input vars should be type variables mkTyVarBinders :: vis -> [TyVar] -> [VarBndr TyVar vis] mkTyVarBinders vis = map (mkTyVarBinder vis) mapVarBndr :: (var -> var') -> (VarBndr var flag) -> (VarBndr var' flag) mapVarBndr f (Bndr v fl) = Bndr (f v) fl mapVarBndrs :: (var -> var') -> [VarBndr var flag] -> [VarBndr var' flag] mapVarBndrs f = map (mapVarBndr f) instance Outputable tv => Outputable (VarBndr tv ForAllTyFlag) where ppr (Bndr v Required) = ppr v ppr (Bndr v Specified) = char '@' <> ppr v ppr (Bndr v Inferred) = braces (ppr v) instance Outputable tv => Outputable (VarBndr tv Specificity) where ppr = ppr . tyVarSpecToBinder instance (Binary tv, Binary vis) => Binary (VarBndr tv vis) where put_ bh (Bndr tv vis) = do { put_ bh tv; put_ bh vis } get bh = do { tv <- get bh; vis <- get bh; return (Bndr tv vis) } instance NamedThing tv => NamedThing (VarBndr tv flag) where getName (Bndr tv _) = getName tv {- ********************************************************************** * * PiTyBinder * * ********************************************************************** -} -- | A 'PiTyBinder' represents an argument to a function. PiTyBinders can be -- dependent ('Named') or nondependent ('Anon'). They may also be visible or -- not. See Note [PiTyBinders] data PiTyBinder = Named ForAllTyBinder -- A type-lambda binder, with a ForAllTyFlag | Anon (Scaled Type) FunTyFlag -- A term-lambda binder. Type here can be CoercionTy. -- The arrow is described by the FunTyFlag deriving Data instance Outputable PiTyBinder where ppr (Anon ty af) = 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) -- | 'PiTyVarBinder' is like 'PiTyBinder', but there can only be 'TyVar' -- in the 'Named' field. type PiTyVarBinder = PiTyBinder -- | Does this binder bind an invisible argument? isInvisiblePiTyBinder :: PiTyBinder -> Bool isInvisiblePiTyBinder (Named (Bndr _ vis)) = isInvisibleForAllTyFlag vis isInvisiblePiTyBinder (Anon _ af) = isInvisibleFunArg af -- | Does this binder bind a visible argument? isVisiblePiTyBinder :: PiTyBinder -> Bool isVisiblePiTyBinder = not . isInvisiblePiTyBinder isNamedPiTyBinder :: PiTyBinder -> Bool isNamedPiTyBinder (Named {}) = True isNamedPiTyBinder (Anon {}) = False namedPiTyBinder_maybe :: PiTyBinder -> Maybe TyCoVar namedPiTyBinder_maybe (Named tv) = Just $ binderVar tv namedPiTyBinder_maybe _ = Nothing -- | Does this binder bind a variable that is /not/ erased? Returns -- 'True' for anonymous binders. isAnonPiTyBinder :: PiTyBinder -> Bool isAnonPiTyBinder (Named {}) = False isAnonPiTyBinder (Anon {}) = True -- | Extract a relevant type, if there is one. anonPiTyBinderType_maybe :: PiTyBinder -> Maybe Type anonPiTyBinderType_maybe (Named {}) = Nothing anonPiTyBinderType_maybe (Anon ty _) = Just (scaledThing ty) -- | If its a named binder, is the binder a tyvar? -- Returns True for nondependent binder. -- This check that we're really returning a *Ty*Binder (as opposed to a -- coercion binder). That way, if/when we allow coercion quantification -- in more places, we'll know we missed updating some function. isTyBinder :: PiTyBinder -> Bool isTyBinder (Named bnd) = isTyVarBinder bnd isTyBinder _ = True piTyBinderType :: PiTyBinder -> Type piTyBinderType (Named (Bndr tv _)) = varType tv piTyBinderType (Anon ty _) = scaledThing ty {- Note [PiTyBinders] ~~~~~~~~~~~~~~~~~~~ But a type like forall a. Maybe a -> forall b. (a,b) -> b can be decomposed to a telescope of type [PiTyBinder], using splitPiTys. That function splits off all leading foralls and arrows, giving ([Named a, Anon (Maybe a), Named b, Anon (a,b)], b) A PiTyBinder represents the type of binders -- that is, the type of an argument to a Pi-type. GHC Core currently supports two different Pi-types: * Anon ty1 fun_flag: a non-dependent function type, written with ->, e.g. ty1 -> ty2 represented as FunTy ty1 ty2. These are lifted to Coercions with the corresponding FunCo. * Named (Var tv forall_flag) A dependent compile-time-only polytype, written with forall, e.g. forall (a:*). ty represented as ForAllTy (Bndr a v) ty Both forms of Pi-types classify terms/types that take an argument. In other words, if `x` is either a function or a polytype, `x arg` makes sense (for an appropriate `arg`). Wrinkles * The Anon constructor of PiTyBinder contains a FunTyFlag. Since the PiTyBinder really only describes the /argument/ it should perhaps only have a TypeOrConstraint rather than a full FunTyFlag. But it's very convenient to have the full FunTyFlag, say in mkPiTys, so that's what we do. Note [VarBndrs, ForAllTyBinders, TyConBinders, and visibility] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ * A ForAllTy (used for both types and kinds) contains a ForAllTyBinder. Each ForAllTyBinder Bndr a tvis is equipped with tvis::ForAllTyFlag, which says whether or not arguments for this binder should be visible (explicit) in source Haskell. * A TyCon contains a list of TyConBinders. Each TyConBinder Bndr a cvis is equipped with cvis::TyConBndrVis, which says whether or not type and kind arguments for this TyCon should be visible (explicit) in source Haskell. This table summarises the visibility rules: --------------------------------------------------------------------------------------- | Occurrences look like this | GHC displays type as in Haskell source code |-------------------------------------------------------------------------------------- | Bndr a tvis :: ForAllTyBinder, in the binder of ForAllTy for a term | tvis :: ForAllTyFlag | tvis = Inferred: f :: forall {a}. type Arg not allowed: f f :: forall {co}. type Arg not allowed: f | tvis = Specified: f :: forall a. type Arg optional: f or f @Int | tvis = Required: T :: forall k -> type Arg required: T * | This last form is illegal in terms: See Note [No Required PiTyBinder in terms] | | Bndr k cvis :: TyConBinder, in the TyConBinders of a TyCon | cvis :: TyConBndrVis | cvis = AnonTCB: T :: kind -> kind Required: T * | cvis = NamedTCB Inferred: T :: forall {k}. kind Arg not allowed: T | T :: forall {co}. kind Arg not allowed: T | cvis = NamedTCB Specified: T :: forall k. kind Arg not allowed[1]: T | cvis = NamedTCB Required: T :: forall k -> kind Required: T * --------------------------------------------------------------------------------------- [1] In types, in the Specified case, it would make sense to allow optional kind applications, thus (T @*), but we have not yet implemented that ---- In term declarations ---- * Inferred. Function defn, with no signature: f1 x = x We infer f1 :: forall {a}. a -> a, with 'a' Inferred It's Inferred because it doesn't appear in any user-written signature for f1 * Specified. Function defn, with signature (implicit forall): f2 :: a -> a; f2 x = x So f2 gets the type f2 :: forall a. a -> a, with 'a' Specified even though 'a' is not bound in the source code by an explicit forall * Specified. Function defn, with signature (explicit forall): f3 :: forall a. a -> a; f3 x = x So f3 gets the type f3 :: forall a. a -> a, with 'a' Specified * Inferred. Function defn, with signature (explicit forall), marked as inferred: f4 :: forall {a}. a -> a; f4 x = x So f4 gets the type f4 :: forall {a}. a -> a, with 'a' Inferred It's Inferred because the user marked it as such, even though it does appear in the user-written signature for f4 * Inferred/Specified. Function signature with inferred kind polymorphism. f5 :: a b -> Int So 'f5' gets the type f5 :: forall {k} (a:k->*) (b:k). a b -> Int Here 'k' is Inferred (it's not mentioned in the type), but 'a' and 'b' are Specified. * Specified. Function signature with explicit kind polymorphism f6 :: a (b :: k) -> Int This time 'k' is Specified, because it is mentioned explicitly, so we get f6 :: forall (k:*) (a:k->*) (b:k). a b -> Int * Similarly pattern synonyms: Inferred - from inferred types (e.g. no pattern type signature) - or from inferred kind polymorphism ---- In type declarations ---- * Inferred (k) data T1 a b = MkT1 (a b) Here T1's kind is T1 :: forall {k:*}. (k->*) -> k -> * The kind variable 'k' is Inferred, since it is not mentioned Note that 'a' and 'b' correspond to /Anon/ PiTyBinders in T1's kind, and Anon binders don't have a visibility flag. (Or you could think of Anon having an implicit Required flag.) * Specified (k) data T2 (a::k->*) b = MkT (a b) Here T's kind is T :: forall (k:*). (k->*) -> k -> * The kind variable 'k' is Specified, since it is mentioned in the signature. * Required (k) data T k (a::k->*) b = MkT (a b) Here T's kind is T :: forall k:* -> (k->*) -> k -> * The kind is Required, since it bound in a positional way in T's declaration Every use of T must be explicitly applied to a kind * Inferred (k1), Specified (k) data T a b (c :: k) = MkT (a b) (Proxy c) Here T's kind is T :: forall {k1:*} (k:*). (k1->*) -> k1 -> k -> * So 'k' is Specified, because it appears explicitly, but 'k1' is Inferred, because it does not Generally, in the list of TyConBinders for a TyCon, * Inferred arguments always come first * Specified, Anon and Required can be mixed e.g. data Foo (a :: Type) :: forall b. (a -> b -> Type) -> Type where ... Here Foo's TyConBinders are [Required 'a', Specified 'b', Anon] and its kind prints as Foo :: forall a -> forall b. (a -> b -> Type) -> Type See also Note [Required, Specified, and Inferred for types] in GHC.Tc.TyCl ---- Printing ----- We print forall types with enough syntax to tell you their visibility flag. But this is not source Haskell, and these types may not all be parsable. Specified: a list of Specified binders is written between `forall` and `.`: const :: forall a b. a -> b -> a Inferred: like Specified, but every binder is written in braces: f :: forall {k} (a:k). S k a -> Int Required: binders are put between `forall` and `->`: T :: forall k -> * ---- Other points ----- * In classic Haskell, all named binders (that is, the type variables in a polymorphic function type f :: forall a. a -> a) have been Inferred. * Inferred variables correspond to "generalized" variables from the Visible Type Applications paper (ESOP'16). Note [No Required PiTyBinder in terms] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We don't allow Required foralls for term variables, including pattern synonyms and data constructors. Why? Because then an application would need a /compulsory/ type argument (possibly without an "@"?), thus (f Int); and we don't have concrete syntax for that. We could change this decision, but Required, Named PiTyBinders are rare anyway. (Most are Anons.) However the type of a term can (just about) have a required quantifier; see Note [Required quantifiers in the type of a term] in GHC.Tc.Gen.Expr. -} {- ************************************************************************ * * * Type and kind variables * * * ************************************************************************ -} tyVarName :: TyVar -> Name tyVarName = varName tyVarKind :: TyVar -> Kind tyVarKind = varType setTyVarUnique :: TyVar -> Unique -> TyVar setTyVarUnique = setVarUnique setTyVarName :: TyVar -> Name -> TyVar setTyVarName = setVarName setTyVarKind :: TyVar -> Kind -> TyVar setTyVarKind tv k = tv {varType = k} updateTyVarKind :: (Kind -> Kind) -> TyVar -> TyVar updateTyVarKind update tv = tv {varType = update (tyVarKind tv)} updateTyVarKindM :: (Monad m) => (Kind -> m Kind) -> TyVar -> m TyVar updateTyVarKindM update tv = do { k' <- update (tyVarKind tv) ; return $ tv {varType = k'} } mkTyVar :: Name -> Kind -> TyVar mkTyVar name kind = TyVar { varName = name , realUnique = getKey (nameUnique name) , varType = kind } mkTcTyVar :: Name -> Kind -> TcTyVarDetails -> TyVar mkTcTyVar name kind details = -- NB: 'kind' may be a coercion kind; cf, 'GHC.Tc.Utils.TcMType.newMetaCoVar' TcTyVar { varName = name, realUnique = getKey (nameUnique name), varType = kind, tc_tv_details = details } tcTyVarDetails :: TyVar -> TcTyVarDetails -- See Note [TcTyVars and TyVars in the typechecker] in GHC.Tc.Utils.TcType tcTyVarDetails (TcTyVar { tc_tv_details = details }) = details -- MP: This should never happen, but it does. Future work is to turn this into a panic. tcTyVarDetails (TyVar {}) = vanillaSkolemTvUnk tcTyVarDetails var = pprPanic "tcTyVarDetails" (ppr var <+> dcolon <+> pprKind (tyVarKind var)) setTcTyVarDetails :: TyVar -> TcTyVarDetails -> TyVar setTcTyVarDetails tv details = tv { tc_tv_details = details } {- %************************************************************************ %* * \subsection{Ids} * * ************************************************************************ -} idInfo :: HasDebugCallStack => Id -> IdInfo idInfo (Id { id_info = info }) = info idInfo other = pprPanic "idInfo" (ppr other) idDetails :: Id -> IdDetails idDetails (Id { id_details = details }) = details idDetails other = pprPanic "idDetails" (ppr other) -- The next three have a 'Var' suffix even though they always build -- Ids, because "GHC.Types.Id" uses 'mkGlobalId' etc with different types mkGlobalVar :: IdDetails -> Name -> Type -> IdInfo -> Id mkGlobalVar details name ty info = mk_id name manyDataConTy ty GlobalId details info -- There is no support for linear global variables yet. They would require -- being checked at link-time, which can be useful, but is not a priority. mkLocalVar :: IdDetails -> Name -> Mult -> Type -> IdInfo -> Id mkLocalVar details name w ty info = mk_id name w ty (LocalId NotExported) details info mkCoVar :: Name -> Type -> CoVar -- Coercion variables have no IdInfo mkCoVar name ty = mk_id name manyDataConTy ty (LocalId NotExported) coVarDetails vanillaIdInfo -- | Exported 'Var's will not be removed as dead code mkExportedLocalVar :: IdDetails -> Name -> Type -> IdInfo -> Id mkExportedLocalVar details name ty info = mk_id name manyDataConTy ty (LocalId Exported) details info -- There is no support for exporting linear variables. See also [mkGlobalVar] mk_id :: Name -> Mult -> Type -> IdScope -> IdDetails -> IdInfo -> Id mk_id name !w ty scope details info = Id { varName = name, realUnique = getKey (nameUnique name), varMult = w, varType = ty, idScope = scope, id_details = details, id_info = info } ------------------- lazySetIdInfo :: Id -> IdInfo -> Var lazySetIdInfo id info = id { id_info = info } setIdDetails :: Id -> IdDetails -> Id setIdDetails id details = id { id_details = details } globaliseId :: Id -> Id -- ^ If it's a local, make it global globaliseId id = id { idScope = GlobalId } setIdExported :: Id -> Id -- ^ Exports the given local 'Id'. Can also be called on global 'Id's, such as data constructors -- and class operations, which are born as global 'Id's and automatically exported setIdExported id@(Id { idScope = LocalId {} }) = id { idScope = LocalId Exported } setIdExported id@(Id { idScope = GlobalId }) = id setIdExported tv = pprPanic "setIdExported" (ppr tv) setIdNotExported :: Id -> Id -- ^ We can only do this to LocalIds setIdNotExported id = assert (isLocalId id) $ id { idScope = LocalId NotExported } ----------------------- updateIdTypeButNotMult :: (Type -> Type) -> Id -> Id updateIdTypeButNotMult f id = id { varType = f (varType id) } updateIdTypeAndMult :: (Type -> Type) -> Id -> Id updateIdTypeAndMult f id@(Id { varType = ty , varMult = mult }) = id { varType = ty' , varMult = mult' } where !ty' = f ty !mult' = f mult updateIdTypeAndMult _ other = pprPanic "updateIdTypeAndMult" (ppr other) updateIdTypeAndMultM :: Monad m => (Type -> m Type) -> Id -> m Id updateIdTypeAndMultM f id@(Id { varType = ty , varMult = mult }) = do { !ty' <- f ty ; !mult' <- f mult ; return (id { varType = ty', varMult = mult' }) } updateIdTypeAndMultM _ other = pprPanic "updateIdTypeAndMultM" (ppr other) setIdMult :: Id -> Mult -> Id setIdMult id !r | isId id = id { varMult = r } | otherwise = pprPanic "setIdMult" (ppr id <+> ppr r) {- ************************************************************************ * * \subsection{Predicates over variables} * * ************************************************************************ -} -- | Is this a type-level (i.e., computationally irrelevant, thus erasable) -- variable? Satisfies @isTyVar = not . isId@. isTyVar :: Var -> Bool -- True of both TyVar and TcTyVar isTyVar (TyVar {}) = True isTyVar (TcTyVar {}) = True isTyVar _ = False isTcTyVar :: Var -> Bool -- True of TcTyVar only isTcTyVar (TcTyVar {}) = True isTcTyVar _ = False isTyCoVar :: Var -> Bool isTyCoVar v = isTyVar v || isCoVar v -- | Is this a value-level (i.e., computationally relevant) 'Id'entifier? -- Satisfies @isId = not . isTyVar@. isId :: Var -> Bool isId (Id {}) = True isId _ = False -- | Is this a coercion variable? -- Satisfies @'isId' v ==> 'isCoVar' v == not ('isNonCoVarId' v)@. isCoVar :: Var -> Bool isCoVar (Id { id_details = details }) = isCoVarDetails details isCoVar _ = False -- | Is this a term variable ('Id') that is /not/ a coercion variable? -- Satisfies @'isId' v ==> 'isCoVar' v == not ('isNonCoVarId' v)@. isNonCoVarId :: Var -> Bool isNonCoVarId (Id { id_details = details }) = not (isCoVarDetails details) isNonCoVarId _ = False isLocalId :: Var -> Bool isLocalId (Id { idScope = LocalId _ }) = True isLocalId _ = False -- | 'isLocalVar' returns @True@ for type variables as well as local 'Id's -- These are the variables that we need to pay attention to when finding free -- variables, or doing dependency analysis. isLocalVar :: Var -> Bool isLocalVar v = not (isGlobalId v) isGlobalId :: Var -> Bool isGlobalId (Id { idScope = GlobalId }) = True isGlobalId _ = False -- | 'mustHaveLocalBinding' returns @True@ of 'Id's and 'TyVar's -- that must have a binding in this module. The converse -- is not quite right: there are some global 'Id's that must have -- bindings, such as record selectors. But that doesn't matter, -- because it's only used for assertions mustHaveLocalBinding :: Var -> Bool mustHaveLocalBinding var = isLocalVar var -- | 'isExportedIdVar' means \"don't throw this away\" isExportedId :: Var -> Bool isExportedId (Id { idScope = GlobalId }) = True isExportedId (Id { idScope = LocalId Exported}) = True isExportedId _ = False