From: simonpj Date: Thu, 9 Oct 2003 12:00:18 +0000 (+0000) Subject: [project @ 2003-10-09 12:00:18 by simonpj] X-Git-Tag: Approx_11550_changesets_converted~385 X-Git-Url: http://git.megacz.com/?a=commitdiff_plain;h=34a2e4425231c0a5a26e7f96aae24006b92f55e9;p=ghc-hetmet.git [project @ 2003-10-09 12:00:18 by simonpj] Add these two files to the preceding mega-commit --- diff --git a/ghc/compiler/typecheck/TcHsType.lhs b/ghc/compiler/typecheck/TcHsType.lhs new file mode 100644 index 0000000..3be9d31 --- /dev/null +++ b/ghc/compiler/typecheck/TcHsType.lhs @@ -0,0 +1,821 @@ + +% (c) The GRASP/AQUA Project, Glasgow University, 1992-1998 +% +\section[TcMonoType]{Typechecking user-specified @MonoTypes@} + +\begin{code} +module TcHsType ( + tcHsSigType, tcHsPred, + UserTypeCtxt(..), + + -- Kind checking + kcHsTyVars, kcHsSigType, kcHsLiftedSigType, + kcCheckHsType, kcHsContext, + + -- Typechecking kinded types + tcHsKindedContext, tcHsKindedType, tcTyVarBndrs, dsHsType, + + tcAddScopedTyVars, + + TcSigInfo(..), tcTySig, mkTcSig, maybeSig, tcSigPolyId, tcSigMonoId + ) where + +#include "HsVersions.h" + +import HsSyn ( HsType(..), HsTyVarBndr(..), HsContext, Sig(..), HsPred(..) ) +import RnHsSyn ( RenamedHsType, RenamedContext, RenamedSig, extractHsTyVars ) +import TcHsSyn ( TcId ) + +import TcRnMonad +import TcEnv ( tcExtendTyVarEnv, tcExtendTyVarKindEnv, + tcLookup, tcLookupClass, tcLookupTyCon, + TyThing(..), TcTyThing(..), + getInLocalScope + ) +import TcMType ( newKindVar, tcInstType, newMutTyVar, + zonkTcType, zonkTcKindToKind, + checkValidType, UserTypeCtxt(..), pprUserTypeCtxt + ) +import TcUnify ( unifyKind, unifyFunKind, unifyTypeKind ) +import TcType ( Type, PredType(..), ThetaType, TyVarDetails(..), + TcTyVar, TcKind, TcThetaType, TcTauType, + mkTyVarTy, mkTyVarTys, mkFunTy, + mkForAllTys, mkFunTys, tcEqType, isPredTy, + mkSigmaTy, mkPredTy, mkGenTyConApp, mkTyConApp, mkAppTys, + liftedTypeKind, unliftedTypeKind, eqKind, + tcSplitFunTy_maybe, tcSplitForAllTys, tcSplitSigmaTy + ) +import PprType ( pprKind, pprThetaArrow ) +import qualified Type ( splitFunTys ) +import Inst ( Inst, InstOrigin(..), newMethod, instToId ) + +import Id ( mkLocalId, idName, idType ) +import Var ( TyVar, mkTyVar, tyVarKind ) +import ErrUtils ( Message ) +import TyCon ( TyCon, tyConKind ) +import Class ( classTyCon ) +import Name ( Name ) +import NameSet +import PrelNames ( genUnitTyConName ) +import Subst ( deShadowTy ) +import TysWiredIn ( mkListTy, mkPArrTy, mkTupleTy ) +import BasicTypes ( Boxity(..) ) +import SrcLoc ( SrcLoc ) +import Outputable +import List ( nubBy ) +\end{code} + + + ---------------------------- + General notes + ---------------------------- + +Generally speaking we now type-check types in three phases + + 1. kcHsType: kind check the HsType + *includes* performing any TH type splices; + so it returns a translated, and kind-annotated, type + + 2. dsHsType: convert from HsType to Type: + perform zonking + expand type synonyms [mkGenTyApps] + hoist the foralls [tcHsType] + + 3. checkValidType: check the validity of the resulting type + +Often these steps are done one after the other (tcHsSigType). +But in mutually recursive groups of type and class decls we do + 1 kind-check the whole group + 2 build TyCons/Classes in a knot-tied way + 3 check the validity of types in the now-unknotted TyCons/Classes + +For example, when we find + (forall a m. m a -> m a) +we bind a,m to kind varibles and kind-check (m a -> m a). This makes +a get kind *, and m get kind *->*. Now we typecheck (m a -> m a) in +an environment that binds a and m suitably. + +The kind checker passed to tcHsTyVars needs to look at enough to +establish the kind of the tyvar: + * For a group of type and class decls, it's just the group, not + the rest of the program + * For a tyvar bound in a pattern type signature, its the types + mentioned in the other type signatures in that bunch of patterns + * For a tyvar bound in a RULE, it's the type signatures on other + universally quantified variables in the rule + +Note that this may occasionally give surprising results. For example: + + data T a b = MkT (a b) + +Here we deduce a::*->*, b::* +But equally valid would be a::(*->*)-> *, b::*->* + + +Validity checking +~~~~~~~~~~~~~~~~~ +Some of the validity check could in principle be done by the kind checker, +but not all: + +- During desugaring, we normalise by expanding type synonyms. Only + after this step can we check things like type-synonym saturation + e.g. type T k = k Int + type S a = a + Then (T S) is ok, because T is saturated; (T S) expands to (S Int); + and then S is saturated. This is a GHC extension. + +- Similarly, also a GHC extension, we look through synonyms before complaining + about the form of a class or instance declaration + +- Ambiguity checks involve functional dependencies, and it's easier to wait + until knots have been resolved before poking into them + +Also, in a mutually recursive group of types, we can't look at the TyCon until we've +finished building the loop. So to keep things simple, we postpone most validity +checking until step (3). + +Knot tying +~~~~~~~~~~ +During step (1) we might fault in a TyCon defined in another module, and it might +(via a loop) refer back to a TyCon defined in this module. So when we tie a big +knot around type declarations with ARecThing, so that the fault-in code can get +the TyCon being defined. + + +%************************************************************************ +%* * +\subsection{Checking types} +%* * +%************************************************************************ + +\begin{code} +tcHsSigType :: UserTypeCtxt -> RenamedHsType -> TcM Type + -- Do kind checking, and hoist for-alls to the top +tcHsSigType ctxt hs_ty + = addErrCtxt (checkHsTypeCtxt ctxt hs_ty) $ + do { kinded_ty <- kcTypeType hs_ty + ; ty <- tcHsKindedType kinded_ty + ; checkValidType ctxt ty + ; returnM ty } + +-- tcHsPred is happy with a partial application, e.g. (ST s) +-- Used from TcDeriv +tcHsPred pred + = do { (kinded_pred,_) <- kc_pred pred -- kc_pred rather than kcHsPred + -- to avoid the partial application check + ; dsHsPred kinded_pred } + + +checkHsTypeCtxt ctxt hs_ty + = vcat [ptext SLIT("In the type signature:") <+> ppr hs_ty, + ptext SLIT("While checking") <+> pprUserTypeCtxt ctxt ] +\end{code} + + These functions are used during knot-tying in + type and class declarations, when we have to + separate kind-checking, desugaring, and validity checking + +\begin{code} +kcHsSigType, kcHsLiftedSigType :: HsType Name -> TcM (HsType Name) + -- Used for type signatures +kcHsSigType ty = kcTypeType ty +kcHsLiftedSigType ty = kcLiftedType ty + +tcHsKindedType :: RenamedHsType -> TcM Type + -- Don't do kind checking, nor validity checking, + -- but do hoist for-alls to the top + -- This is used in type and class decls, where kinding is + -- done in advance, and validity checking is done later + -- [Validity checking done later because of knot-tying issues.] +tcHsKindedType hs_ty + = do { ty <- dsHsType hs_ty + ; return (hoistForAllTys ty) } + +tcHsKindedContext :: RenamedContext -> TcM ThetaType +-- Used when we are expecting a ClassContext (i.e. no implicit params) +-- Does not do validity checking, like tcHsKindedType +tcHsKindedContext hs_theta = mappM dsHsPred hs_theta +\end{code} + + +%************************************************************************ +%* * + The main kind checker: kcHsType +%* * +%************************************************************************ + + First a couple of simple wrappers for kcHsType + +\begin{code} +--------------------------- +kcLiftedType :: HsType Name -> TcM (HsType Name) + -- The type ty must be a *lifted* *type* +kcLiftedType ty = kcCheckHsType ty liftedTypeKind + +--------------------------- +kcTypeType :: HsType Name -> TcM (HsType Name) + -- The type ty must be a *type*, but it can be lifted or unlifted +kcTypeType ty + = kcHsType ty `thenM` \ (ty', kind) -> + unifyTypeKind kind `thenM_` + returnM ty' + +--------------------------- +kcCheckHsType :: HsType Name -> TcKind -> TcM (HsType Name) +-- Check that the type has the specified kind +kcCheckHsType ty exp_kind + = kcHsType ty `thenM` \ (ty', act_kind) -> + checkExpectedKind (ppr ty) act_kind exp_kind `thenM_` + returnM ty' +\end{code} + + Here comes the main function + +\begin{code} +kcHsType :: HsType Name -> TcM (HsType Name, TcKind) +-- kcHsType *returns* the kind of the type, rather than taking an expected +-- kind as argument as tcExpr does. +-- Reasons: +-- (a) the kind of (->) is +-- forall bx1 bx2. Type bx1 -> Type bx2 -> Type Boxed +-- so we'd need to generate huge numbers of bx variables. +-- (b) kinds are so simple that the error messages are fine +-- +-- The translated type has explicitly-kinded type-variable binders + +kcHsType (HsParTy ty) + = kcHsType ty `thenM` \ (ty', kind) -> + returnM (HsParTy ty', kind) + +kcHsType (HsTyVar name) + = kcTyVar name `thenM` \ kind -> + returnM (HsTyVar name, kind) + +kcHsType (HsListTy ty) + = kcLiftedType ty `thenM` \ ty' -> + returnM (HsListTy ty', liftedTypeKind) + +kcHsType (HsPArrTy ty) + = kcLiftedType ty `thenM` \ ty' -> + returnM (HsPArrTy ty', liftedTypeKind) + +kcHsType (HsNumTy n) + = returnM (HsNumTy n, liftedTypeKind) + +kcHsType (HsKindSig ty k) + = kcCheckHsType ty k `thenM` \ ty' -> + returnM (HsKindSig ty' k, k) + +kcHsType (HsTupleTy Boxed tys) + = mappM kcLiftedType tys `thenM` \ tys' -> + returnM (HsTupleTy Boxed tys', liftedTypeKind) + +kcHsType (HsTupleTy Unboxed tys) + = mappM kcTypeType tys `thenM` \ tys' -> + returnM (HsTupleTy Unboxed tys', unliftedTypeKind) + +kcHsType (HsFunTy ty1 ty2) + = kcTypeType ty1 `thenM` \ ty1' -> + kcTypeType ty2 `thenM` \ ty2' -> + returnM (HsFunTy ty1' ty2', liftedTypeKind) + +kcHsType ty@(HsOpTy ty1 op ty2) + = kcTyVar op `thenM` \ op_kind -> + kcApps op_kind (ppr op) [ty1,ty2] `thenM` \ ([ty1',ty2'], res_kind) -> + returnM (HsOpTy ty1' op ty2', res_kind) + +kcHsType ty@(HsAppTy ty1 ty2) + = kcHsType fun_ty `thenM` \ (fun_ty', fun_kind) -> + kcApps fun_kind (ppr fun_ty) arg_tys `thenM` \ (arg_tys', res_kind) -> + returnM (foldl HsAppTy fun_ty' arg_tys', res_kind) + where + (fun_ty, arg_tys) = split ty1 [ty2] + split (HsAppTy f a) as = split f (a:as) + split f as = (f,as) + +kcHsType (HsPredTy pred) + = kcHsPred pred `thenM` \ pred' -> + returnM (HsPredTy pred', liftedTypeKind) + +kcHsType (HsForAllTy (Just tv_names) context ty) + = kcHsTyVars tv_names $ \ tv_names' -> + kcHsContext context `thenM` \ ctxt' -> + kcLiftedType ty `thenM` \ ty' -> + -- The body of a forall must be of kind * + -- In principle, I suppose, we could allow unlifted types, + -- but it seems simpler to stick to lifted types for now. + returnM (HsForAllTy (Just tv_names') ctxt' ty', liftedTypeKind) + +--------------------------- +kcApps :: TcKind -- Function kind + -> SDoc -- Function + -> [HsType Name] -- Arg types + -> TcM ([HsType Name], TcKind) -- Kind-checked args +kcApps fun_kind ppr_fun args + = split_fk fun_kind (length args) `thenM` \ (arg_kinds, res_kind) -> + mappM kc_arg (args `zip` arg_kinds) `thenM` \ args' -> + returnM (args', res_kind) + where + split_fk fk 0 = returnM ([], fk) + split_fk fk n = unifyFunKind fk `thenM` \ mb_fk -> + case mb_fk of + Nothing -> failWithTc too_many_args + Just (ak,fk') -> split_fk fk' (n-1) `thenM` \ (aks, rk) -> + returnM (ak:aks, rk) + + kc_arg (arg, arg_kind) = kcCheckHsType arg arg_kind + + too_many_args = ptext SLIT("Kind error:") <+> quotes ppr_fun <+> + ptext SLIT("is applied to too many type arguments") + +--------------------------- +kcHsContext :: HsContext Name -> TcM (HsContext Name) +kcHsContext ctxt = mappM kcHsPred ctxt + +kcHsPred pred -- Checks that the result is of kind liftedType + = kc_pred pred `thenM` \ (pred', kind) -> + checkExpectedKind (ppr pred) kind liftedTypeKind `thenM_` + returnM pred' + +--------------------------- +kc_pred :: HsPred Name -> TcM (HsPred Name, TcKind) + -- Does *not* check for a saturated + -- application (reason: used from TcDeriv) +kc_pred pred@(HsIParam name ty) + = kcHsType ty `thenM` \ (ty', kind) -> + returnM (HsIParam name ty', kind) + +kc_pred pred@(HsClassP cls tys) + = kcClass cls `thenM` \ kind -> + kcApps kind (ppr cls) tys `thenM` \ (tys', res_kind) -> + returnM (HsClassP cls tys', res_kind) + +--------------------------- +kcTyVar :: Name -> TcM TcKind +kcTyVar name -- Could be a tyvar or a tycon + = tcLookup name `thenM` \ thing -> + case thing of + ATyVar tv -> returnM (tyVarKind tv) + ARecTyCon kind -> returnM kind + AGlobal (ATyCon tc) -> returnM (tyConKind tc) + other -> failWithTc (wrongThingErr "type" thing name) + +kcClass :: Name -> TcM TcKind +kcClass cls -- Must be a class + = tcLookup cls `thenM` \ thing -> + case thing of + ARecClass kind -> returnM kind + AGlobal (AClass cls) -> returnM (tyConKind (classTyCon cls)) + other -> failWithTc (wrongThingErr "class" thing cls) +\end{code} + + Helper functions + + +\begin{code} +--------------------------- +-- We would like to get a decent error message from +-- (a) Under-applied type constructors +-- f :: (Maybe, Maybe) +-- (b) Over-applied type constructors +-- f :: Int x -> Int x +-- + + +checkExpectedKind :: SDoc -> TcKind -> TcKind -> TcM TcKind +-- A fancy wrapper for 'unifyKind', which tries to give +-- decent error messages. +-- Returns the same kind that it is passed, exp_kind +checkExpectedKind pp_ty act_kind exp_kind + | act_kind `eqKind` exp_kind -- Short cut for a very common case + = returnM exp_kind + | otherwise + = tryTc (unifyKind exp_kind act_kind) `thenM` \ (errs, mb_r) -> + case mb_r of { + Just _ -> returnM exp_kind ; -- Unification succeeded + Nothing -> + + -- So there's definitely an error + -- Now to find out what sort + zonkTcType exp_kind `thenM` \ exp_kind -> + zonkTcType act_kind `thenM` \ act_kind -> + + let (exp_as, _) = Type.splitFunTys exp_kind + (act_as, _) = Type.splitFunTys act_kind + -- Use the Type versions for kinds + n_exp_as = length exp_as + n_act_as = length act_as + + err | n_exp_as < n_act_as -- E.g. [Maybe] + = quotes pp_ty <+> ptext SLIT("is not applied to enough type arguments") + + -- Now n_exp_as >= n_act_as. In the next two cases, + -- n_exp_as == 0, and hence so is n_act_as + | exp_kind `eqKind` liftedTypeKind && act_kind `eqKind` unliftedTypeKind + = ptext SLIT("Expecting a lifted type, but") <+> quotes pp_ty + <+> ptext SLIT("is unlifted") + + | exp_kind `eqKind` unliftedTypeKind && act_kind `eqKind` liftedTypeKind + = ptext SLIT("Expecting an unlifted type, but") <+> quotes pp_ty + <+> ptext SLIT("is lifted") + + | otherwise -- E.g. Monad [Int] + = sep [ ptext SLIT("Expecting kind") <+> quotes (pprKind exp_kind) <> comma, + ptext SLIT("but") <+> quotes pp_ty <+> + ptext SLIT("has kind") <+> quotes (pprKind act_kind)] + in + failWithTc (ptext SLIT("Kind error:") <+> err) + } +\end{code} + +%************************************************************************ +%* * + Desugaring +%* * +%************************************************************************ + +The type desugarer + + * Transforms from HsType to Type + * Zonks any kinds + +It cannot fail, and does no validity checking + +\begin{code} +dsHsType :: HsType Name -- All HsTyVarBndrs are kind-annotated + -> TcM Type + +dsHsType ty@(HsTyVar name) + = ds_app ty [] + +dsHsType (HsParTy ty) -- Remove the parentheses markers + = dsHsType ty + +dsHsType (HsKindSig ty k) + = dsHsType ty -- Kind checking done already + +dsHsType (HsListTy ty) + = dsHsType ty `thenM` \ tau_ty -> + returnM (mkListTy tau_ty) + +dsHsType (HsPArrTy ty) + = dsHsType ty `thenM` \ tau_ty -> + returnM (mkPArrTy tau_ty) + +dsHsType (HsTupleTy boxity tys) + = dsHsTypes tys `thenM` \ tau_tys -> + returnM (mkTupleTy boxity (length tys) tau_tys) + +dsHsType (HsFunTy ty1 ty2) + = dsHsType ty1 `thenM` \ tau_ty1 -> + dsHsType ty2 `thenM` \ tau_ty2 -> + returnM (mkFunTy tau_ty1 tau_ty2) + +dsHsType (HsOpTy ty1 op ty2) + = dsHsType ty1 `thenM` \ tau_ty1 -> + dsHsType ty2 `thenM` \ tau_ty2 -> + ds_var_app op [tau_ty1,tau_ty2] + +dsHsType (HsNumTy n) + = ASSERT(n==1) + tcLookupTyCon genUnitTyConName `thenM` \ tc -> + returnM (mkTyConApp tc []) + +dsHsType ty@(HsAppTy ty1 ty2) + = ds_app ty1 [ty2] + +dsHsType (HsPredTy pred) + = dsHsPred pred `thenM` \ pred' -> + returnM (mkPredTy pred') + +dsHsType full_ty@(HsForAllTy (Just tv_names) ctxt ty) + = tcTyVarBndrs tv_names $ \ tyvars -> + mappM dsHsPred ctxt `thenM` \ theta -> + dsHsType ty `thenM` \ tau -> + returnM (mkSigmaTy tyvars theta tau) + +dsHsTypes arg_tys = mappM dsHsType arg_tys +\end{code} + +Help functions for type applications +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +\begin{code} +ds_app :: HsType Name -> [HsType Name] -> TcM Type +ds_app (HsAppTy ty1 ty2) tys + = ds_app ty1 (ty2:tys) + +ds_app ty tys + = dsHsTypes tys `thenM` \ arg_tys -> + case ty of + HsTyVar fun -> ds_var_app fun arg_tys + other -> dsHsType ty `thenM` \ fun_ty -> + returnM (mkAppTys fun_ty arg_tys) + +ds_var_app :: Name -> [Type] -> TcM Type +ds_var_app name arg_tys + = tcLookup name `thenM` \ thing -> + case thing of + ATyVar tv -> returnM (mkAppTys (mkTyVarTy tv) arg_tys) + AGlobal (ATyCon tc) -> returnM (mkGenTyConApp tc arg_tys) + ARecTyCon _ -> tcLookupTyCon name `thenM` \ tc -> + returnM (mkGenTyConApp tc arg_tys) + other -> pprPanic "ds_app_type" (ppr name <+> ppr arg_tys) +\end{code} + + +Contexts +~~~~~~~~ +\begin{code} +dsHsPred :: HsPred Name -> TcM PredType +dsHsPred pred@(HsClassP class_name tys) + = dsHsTypes tys `thenM` \ arg_tys -> + tcLookupClass class_name `thenM` \ clas -> + returnM (ClassP clas arg_tys) + +dsHsPred (HsIParam name ty) + = dsHsType ty `thenM` \ arg_ty -> + returnM (IParam name arg_ty) +\end{code} + + +%************************************************************************ +%* * + Type-variable binders +%* * +%************************************************************************ + + +\begin{code} +kcHsTyVars :: [HsTyVarBndr Name] + -> ([HsTyVarBndr Name] -> TcM r) -- These binders are kind-annotated + -- They scope over the thing inside + -> TcM r +kcHsTyVars tvs thing_inside + = mappM kcHsTyVar tvs `thenM` \ bndrs -> + tcExtendTyVarKindEnv bndrs $ + thing_inside bndrs + +kcHsTyVar :: HsTyVarBndr Name -> TcM (HsTyVarBndr Name) + -- Return a *kind-annotated* binder, and a tyvar with a mutable kind in it +kcHsTyVar (UserTyVar name) = newKindVar `thenM` \ kind -> + returnM (KindedTyVar name kind) +kcHsTyVar (KindedTyVar name kind) = returnM (KindedTyVar name kind) + +------------------ +tcTyVarBndrs :: [HsTyVarBndr Name] -- Kind-annotated binders, which need kind-zonking + -> ([TyVar] -> TcM r) + -> TcM r +-- Used when type-checking types/classes/type-decls +-- Brings into scope immutable TyVars, not mutable ones that require later zonking +tcTyVarBndrs bndrs thing_inside + = mapM zonk bndrs `thenM` \ tyvars -> + tcExtendTyVarEnv tyvars (thing_inside tyvars) + where + zonk (KindedTyVar name kind) = zonkTcKindToKind kind `thenM` \ kind' -> + returnM (mkTyVar name kind') + zonk (UserTyVar name) = pprTrace "BAD: Un-kinded tyvar" (ppr name) $ + returnM (mkTyVar name liftedTypeKind) +\end{code} + + +%************************************************************************ +%* * + Scoped type variables +%* * +%************************************************************************ + + +tcAddScopedTyVars is used for scoped type variables added by pattern +type signatures + e.g. \ ((x::a), (y::a)) -> x+y +They never have explicit kinds (because this is source-code only) +They are mutable (because they can get bound to a more specific type). + +Usually we kind-infer and expand type splices, and then +tupecheck/desugar the type. That doesn't work well for scoped type +variables, because they scope left-right in patterns. (e.g. in the +example above, the 'a' in (y::a) is bound by the 'a' in (x::a). + +The current not-very-good plan is to + * find all the types in the patterns + * find their free tyvars + * do kind inference + * bring the kinded type vars into scope + * BUT throw away the kind-checked type + (we'll kind-check it again when we type-check the pattern) + +This is bad because throwing away the kind checked type throws away +its splices. But too bad for now. [July 03] + +Historical note: + We no longer specify that these type variables must be univerally + quantified (lots of email on the subject). If you want to put that + back in, you need to + a) Do a checkSigTyVars after thing_inside + b) More insidiously, don't pass in expected_ty, else + we unify with it too early and checkSigTyVars barfs + Instead you have to pass in a fresh ty var, and unify + it with expected_ty afterwards + +\begin{code} +tcAddScopedTyVars :: [RenamedHsType] -> TcM a -> TcM a +tcAddScopedTyVars [] thing_inside + = thing_inside -- Quick get-out for the empty case + +tcAddScopedTyVars sig_tys thing_inside + = getInLocalScope `thenM` \ in_scope -> + let + sig_tvs = [ UserTyVar n | ty <- sig_tys, + n <- nameSetToList (extractHsTyVars ty), + not (in_scope n) ] + -- The tyvars we want are the free type variables of + -- the type that are not already in scope + in + -- Behave like kcHsType on a ForAll type + -- i.e. make kinded tyvars with mutable kinds, + -- and kind-check the enclosed types + kcHsTyVars sig_tvs (\ kinded_tvs -> do + { mappM kcTypeType sig_tys + ; return kinded_tvs }) `thenM` \ kinded_tvs -> + + -- Zonk the mutable kinds and bring the tyvars into scope + -- Rather like tcTyVarBndrs, except that it brings *mutable* + -- tyvars into scope, not immutable ones + mapM zonk kinded_tvs `thenM` \ tyvars -> + tcExtendTyVarEnv tyvars thing_inside + + where + zonk (KindedTyVar name kind) = zonkTcKindToKind kind `thenM` \ kind' -> + newMutTyVar name kind' VanillaTv + zonk (UserTyVar name) = pprTrace "BAD: Un-kinded tyvar" (ppr name) $ + returnM (mkTyVar name liftedTypeKind) +\end{code} + + +%************************************************************************ +%* * +\subsection{Signatures} +%* * +%************************************************************************ + +@tcSigs@ checks the signatures for validity, and returns a list of +{\em freshly-instantiated} signatures. That is, the types are already +split up, and have fresh type variables installed. All non-type-signature +"RenamedSigs" are ignored. + +The @TcSigInfo@ contains @TcTypes@ because they are unified with +the variable's type, and after that checked to see whether they've +been instantiated. + +\begin{code} +data TcSigInfo + = TySigInfo + TcId -- *Polymorphic* binder for this value... + -- Has name = N + + [TcTyVar] -- tyvars + TcThetaType -- theta + TcTauType -- tau + + TcId -- *Monomorphic* binder for this value + -- Does *not* have name = N + -- Has type tau + + [Inst] -- Empty if theta is null, or + -- (method mono_id) otherwise + + SrcLoc -- Of the signature + +instance Outputable TcSigInfo where + ppr (TySigInfo id tyvars theta tau _ inst loc) = + ppr id <+> ptext SLIT("::") <+> ppr tyvars <+> ppr theta <+> ptext SLIT("=>") <+> ppr tau + +tcSigPolyId :: TcSigInfo -> TcId +tcSigPolyId (TySigInfo id _ _ _ _ _ _) = id + +tcSigMonoId :: TcSigInfo -> TcId +tcSigMonoId (TySigInfo _ _ _ _ id _ _) = id + +maybeSig :: [TcSigInfo] -> Name -> Maybe (TcSigInfo) + -- Search for a particular signature +maybeSig [] name = Nothing +maybeSig (sig@(TySigInfo sig_id _ _ _ _ _ _) : sigs) name + | name == idName sig_id = Just sig + | otherwise = maybeSig sigs name +\end{code} + + +\begin{code} +tcTySig :: RenamedSig -> TcM TcSigInfo + +tcTySig (Sig v ty src_loc) + = addSrcLoc src_loc $ + tcHsSigType (FunSigCtxt v) ty `thenM` \ sigma_tc_ty -> + mkTcSig (mkLocalId v sigma_tc_ty) `thenM` \ sig -> + returnM sig + +mkTcSig :: TcId -> TcM TcSigInfo +mkTcSig poly_id + = -- Instantiate this type + -- It's important to do this even though in the error-free case + -- we could just split the sigma_tc_ty (since the tyvars don't + -- unified with anything). But in the case of an error, when + -- the tyvars *do* get unified with something, we want to carry on + -- typechecking the rest of the program with the function bound + -- to a pristine type, namely sigma_tc_ty + tcInstType SigTv (idType poly_id) `thenM` \ (tyvars', theta', tau') -> + + getInstLoc SignatureOrigin `thenM` \ inst_loc -> + newMethod inst_loc poly_id + (mkTyVarTys tyvars') + theta' tau' `thenM` \ inst -> + -- We make a Method even if it's not overloaded; no harm + -- But do not extend the LIE! We're just making an Id. + + getSrcLocM `thenM` \ src_loc -> + returnM (TySigInfo poly_id tyvars' theta' tau' + (instToId inst) [inst] src_loc) +\end{code} + + +%************************************************************************ +%* * +\subsection{Errors and contexts} +%* * +%************************************************************************ + + +\begin{code} +hoistForAllTys :: Type -> Type +-- Used for user-written type signatures only +-- Move all the foralls and constraints to the top +-- e.g. T -> forall a. a ==> forall a. T -> a +-- T -> (?x::Int) -> Int ==> (?x::Int) -> T -> Int +-- +-- Also: eliminate duplicate constraints. These can show up +-- when hoisting constraints, notably implicit parameters. +-- +-- We want to 'look through' type synonyms when doing this +-- so it's better done on the Type than the HsType + +hoistForAllTys ty + = let + no_shadow_ty = deShadowTy ty + -- Running over ty with an empty substitution gives it the + -- no-shadowing property. This is important. For example: + -- type Foo r = forall a. a -> r + -- foo :: Foo (Foo ()) + -- Here the hoisting should give + -- foo :: forall a a1. a -> a1 -> () + -- + -- What about type vars that are lexically in scope in the envt? + -- We simply rely on them having a different unique to any + -- binder in 'ty'. Otherwise we'd have to slurp the in-scope-tyvars + -- out of the envt, which is boring and (I think) not necessary. + in + case hoist no_shadow_ty of + (tvs, theta, body) -> mkForAllTys tvs (mkFunTys (nubBy tcEqType theta) body) + -- The 'nubBy' eliminates duplicate constraints, + -- notably implicit parameters + where + hoist ty + | (tvs1, body_ty) <- tcSplitForAllTys ty, + not (null tvs1) + = case hoist body_ty of + (tvs2,theta,tau) -> (tvs1 ++ tvs2, theta, tau) + + | Just (arg, res) <- tcSplitFunTy_maybe ty + = let + arg' = hoistForAllTys arg -- Don't forget to apply hoist recursively + in -- to the argument type + if (isPredTy arg') then + case hoist res of + (tvs,theta,tau) -> (tvs, arg':theta, tau) + else + case hoist res of + (tvs,theta,tau) -> (tvs, theta, mkFunTy arg' tau) + + | otherwise = ([], [], ty) +\end{code} + + +%************************************************************************ +%* * +\subsection{Errors and contexts} +%* * +%************************************************************************ + +\begin{code} +wrongThingErr expected thing name + = pp_thing thing <+> quotes (ppr name) <+> ptext SLIT("used as a") <+> text expected + where + pp_thing (AGlobal (ATyCon _)) = ptext SLIT("Type constructor") + pp_thing (AGlobal (AClass _)) = ptext SLIT("Class") + pp_thing (AGlobal (AnId _)) = ptext SLIT("Identifier") + pp_thing (AGlobal (ADataCon _)) = ptext SLIT("Data constructor") + pp_thing (ATyVar _) = ptext SLIT("Type variable") + pp_thing (ATcId _ _ _) = ptext SLIT("Local identifier") + pp_thing (ARecTyCon _) = ptext SLIT("Rec tycon") + pp_thing (ARecClass _) = ptext SLIT("Rec class") +\end{code} diff --git a/ghc/compiler/utils/IOEnv.hs b/ghc/compiler/utils/IOEnv.hs new file mode 100644 index 0000000..3b4f983 --- /dev/null +++ b/ghc/compiler/utils/IOEnv.hs @@ -0,0 +1,185 @@ +-- (c) The University of Glasgow 2002 +-- +-- The IO Monad with an environment +-- + +module IOEnv ( + IOEnv, -- Instance of Monad + + -- Standard combinators, specialised + returnM, thenM, thenM_, failM, + mappM, mappM_, sequenceM, foldlM, + mapAndUnzipM, mapAndUnzip3M, + checkM, ifM, + + -- Getting at the environment + getEnv, setEnv, updEnv, + + runIOEnv, unsafeInterleaveM, + tryM, fixM, + + -- I/O operations + ioToIOEnv, + IORef, newMutVar, readMutVar, writeMutVar, updMutVar + ) where +#include "HsVersions.h" + +import Panic ( tryJust ) +import DATA_IOREF ( IORef, newIORef, readIORef, writeIORef ) +import UNSAFE_IO ( unsafeInterleaveIO ) +import FIX_IO ( fixIO ) +import EXCEPTION ( Exception(..) ) +import IO ( isUserError ) + + +---------------------------------------------------------------------- +-- Defining the monad type +---------------------------------------------------------------------- + + +newtype IOEnv env a = IOEnv (env -> IO a) +unIOEnv (IOEnv m) = m + +instance Monad (IOEnv m) where + (>>=) = thenM + (>>) = thenM_ + return = returnM + fail s = failM -- Ignore the string + +returnM :: a -> IOEnv env a +returnM a = IOEnv (\ env -> return a) + +thenM :: IOEnv env a -> (a -> IOEnv env b) -> IOEnv env b +thenM (IOEnv m) f = IOEnv (\ env -> do { r <- m env ; + unIOEnv (f r) env }) + +thenM_ :: IOEnv env a -> IOEnv env b -> IOEnv env b +thenM_ (IOEnv m) f = IOEnv (\ env -> do { m env ; unIOEnv f env }) + +failM :: IOEnv env a +failM = IOEnv (\ env -> ioError (userError "IOEnv failure")) + + + +---------------------------------------------------------------------- +-- Fundmantal combinators specific to the monad +---------------------------------------------------------------------- + + +--------------------------- +runIOEnv :: env -> IOEnv env a -> IO a +runIOEnv env (IOEnv m) = m env + + +--------------------------- +{-# NOINLINE fixM #-} + -- Aargh! Not inlining fixTc alleviates a space leak problem. + -- Normally fixTc is used with a lazy tuple match: if the optimiser is + -- shown the definition of fixTc, it occasionally transforms the code + -- in such a way that the code generator doesn't spot the selector + -- thunks. Sigh. + +fixM :: (a -> IOEnv env a) -> IOEnv env a +fixM f = IOEnv (\ env -> fixIO (\ r -> unIOEnv (f r) env)) + + +--------------------------- +tryM :: IOEnv env r -> IOEnv env (Either Exception r) +-- Reflect exception into IOEnv envonad +tryM (IOEnv thing) = IOEnv (\ env -> tryJust tc_errors (thing env)) + where +#if __GLASGOW_HASKELL__ > 504 || __GLASGOW_HASKELL__ < 500 + tc_errors e@(IOException ioe) | isUserError ioe = Just e +#elif __GLASGOW_HASKELL__ == 502 + tc_errors e@(UserError _) = Just e +#else + tc_errors e@(IOException ioe) | isUserError e = Just e +#endif + tc_errors _other = Nothing + -- type checker failures show up as UserErrors only + + +--------------------------- +unsafeInterleaveM :: IOEnv env a -> IOEnv env a +unsafeInterleaveM (IOEnv m) = IOEnv (\ env -> unsafeInterleaveIO (m env)) + + +---------------------------------------------------------------------- +-- Accessing input/output +---------------------------------------------------------------------- + +ioToIOEnv :: IO a -> IOEnv env a +ioToIOEnv io = IOEnv (\ env -> io) + +newMutVar :: a -> IOEnv env (IORef a) +newMutVar val = IOEnv (\ env -> newIORef val) + +writeMutVar :: IORef a -> a -> IOEnv env () +writeMutVar var val = IOEnv (\ env -> writeIORef var val) + +readMutVar :: IORef a -> IOEnv env a +readMutVar var = IOEnv (\ env -> readIORef var) + +updMutVar :: IORef a -> (a->a) -> IOEnv env () +updMutVar var upd_fn = IOEnv (\ env -> do { v <- readIORef var; writeIORef var (upd_fn v) }) + + +---------------------------------------------------------------------- +-- Accessing the environment +---------------------------------------------------------------------- + +getEnv :: IOEnv env env +{-# INLINE getEnv #-} +getEnv = IOEnv (\ env -> return env) + +setEnv :: env' -> IOEnv env' a -> IOEnv env a +{-# INLINE setEnv #-} +setEnv new_env (IOEnv m) = IOEnv (\ env -> m new_env) + +updEnv :: (env -> env') -> IOEnv env' a -> IOEnv env a +{-# INLINE updEnv #-} +updEnv upd (IOEnv m) = IOEnv (\ env -> m (upd env)) + + +---------------------------------------------------------------------- +-- Standard combinators, but specialised for this monad +-- (for efficiency) +---------------------------------------------------------------------- + +mappM :: (a -> IOEnv env b) -> [a] -> IOEnv env [b] +mappM_ :: (a -> IOEnv env b) -> [a] -> IOEnv env () + -- Funny names to avoid clash with Prelude +sequenceM :: [IOEnv env a] -> IOEnv env [a] +foldlM :: (a -> b -> IOEnv env a) -> a -> [b] -> IOEnv env a +mapAndUnzipM :: (a -> IOEnv env (b,c)) -> [a] -> IOEnv env ([b],[c]) +mapAndUnzip3M :: (a -> IOEnv env (b,c,d)) -> [a] -> IOEnv env ([b],[c],[d]) +checkM :: Bool -> IOEnv env () -> IOEnv env () -- Perform arg if bool is False +ifM :: Bool -> IOEnv env () -> IOEnv env () -- Perform arg if bool is True + +mappM f [] = return [] +mappM f (x:xs) = do { r <- f x; rs <- mappM f xs; return (r:rs) } + +mappM_ f [] = return () +mappM_ f (x:xs) = f x >> mappM_ f xs + +sequenceM [] = return [] +sequenceM (x:xs) = do { r <- x; rs <- sequenceM xs; return (r:rs) } + +foldlM k z [] = return z +foldlM k z (x:xs) = do { r <- k z x; foldlM k r xs } + +mapAndUnzipM f [] = return ([],[]) +mapAndUnzipM f (x:xs) = do { (r,s) <- f x; + (rs,ss) <- mapAndUnzipM f xs; + return (r:rs, s:ss) } + +mapAndUnzip3M f [] = return ([],[], []) +mapAndUnzip3M f (x:xs) = do { (r,s,t) <- f x; + (rs,ss,ts) <- mapAndUnzip3M f xs; + return (r:rs, s:ss, t:ts) } + +checkM True err = return () +checkM False err = err + +ifM True do_it = do_it +ifM False do_it = return ()