X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=ghc%2Fcompiler%2Ftypecheck%2FTcMonoType.lhs;h=90d5f8b95d787aa5aeb1d0992c7e7cd5e74d3eb3;hb=13878c136b4e6b676dbc859f378809676f4d679c;hp=c02e7125d1e035772420d1086a65a15aed4a8c17;hpb=9e93335020e64a811dbbb223e1727c76933a93ae;p=ghc-hetmet.git diff --git a/ghc/compiler/typecheck/TcMonoType.lhs b/ghc/compiler/typecheck/TcMonoType.lhs index c02e712..90d5f8b 100644 --- a/ghc/compiler/typecheck/TcMonoType.lhs +++ b/ghc/compiler/typecheck/TcMonoType.lhs @@ -4,64 +4,55 @@ \section[TcMonoType]{Typechecking user-specified @MonoTypes@} \begin{code} -module TcMonoType ( tcHsSigType, tcHsType, tcIfaceType, tcHsTheta, +module TcMonoType ( tcHsSigType, tcHsType, tcIfaceType, tcHsTheta, tcHsPred, UserTypeCtxt(..), -- Kind checking kcHsTyVar, kcHsTyVars, mkTyClTyVars, kcHsType, kcHsSigType, kcHsSigTypes, kcHsLiftedSigType, kcHsContext, - tcScopedTyVars, tcHsTyVars, mkImmutTyVars, + tcAddScopedTyVars, tcHsTyVars, mkImmutTyVars, - TcSigInfo(..), tcTySig, mkTcSig, maybeSig, - checkSigTyVars, sigCtxt, sigPatCtxt + TcSigInfo(..), tcTySig, mkTcSig, maybeSig, tcSigPolyId, tcSigMonoId ) where #include "HsVersions.h" import HsSyn ( HsType(..), HsTyVarBndr(..), Sig(..), HsPred(..), pprParendHsType, HsTupCon(..), hsTyVarNames ) -import RnHsSyn ( RenamedHsType, RenamedHsPred, RenamedContext, RenamedSig ) +import RnHsSyn ( RenamedHsType, RenamedHsPred, RenamedContext, RenamedSig, extractHsTyVars ) import TcHsSyn ( TcId ) import TcMonad import TcEnv ( tcExtendTyVarEnv, tcLookup, tcLookupGlobal, - tcGetGlobalTyVars, tcEnvTcIds, tcEnvTyVars, + tcInLocalScope, TyThing(..), TcTyThing(..), tcExtendKindEnv ) -import TcMType ( newKindVar, tcInstSigVars, - zonkKindEnv, zonkTcType, zonkTcTyVars, zonkTcTyVar, - unifyKind, unifyOpenTypeKind, +import TcMType ( newKindVar, zonkKindEnv, tcInstType, checkValidType, UserTypeCtxt(..), pprUserTypeCtxt ) -import TcType ( Type, Kind, SourceType(..), ThetaType, - mkTyVarTy, mkTyVarTys, mkFunTy, mkSynTy, - tcSplitForAllTys, tcSplitRhoTy, - hoistForAllTys, allDistinctTyVars, - zipFunTys, - mkSigmaTy, mkPredTy, mkTyConApp, - mkAppTys, mkRhoTy, +import TcUnify ( unifyKind, unifyOpenTypeKind ) +import TcType ( Type, Kind, SourceType(..), ThetaType, TyVarDetails(..), + TcTyVar, TcKind, TcThetaType, TcTauType, + mkTyVarTy, mkTyVarTys, mkFunTy, + hoistForAllTys, zipFunTys, + mkSigmaTy, mkPredTy, mkGenTyConApp, mkTyConApp, mkAppTys, liftedTypeKind, unliftedTypeKind, mkArrowKind, - mkArrowKinds, tcGetTyVar_maybe, tcGetTyVar, tcSplitFunTy_maybe, - tidyOpenType, tidyOpenTypes, tidyOpenTyVar, tidyOpenTyVars, - tyVarsOfType, mkForAllTys + mkArrowKinds, tcSplitFunTy_maybe ) import Inst ( Inst, InstOrigin(..), newMethodWithGivenTy, instToId ) -import PprType ( pprType ) -import Subst ( mkTopTyVarSubst, substTy ) -import CoreFVs ( idFreeTyVars ) + import Id ( mkLocalId, idName, idType ) -import Var ( Id, Var, TyVar, mkTyVar, tyVarKind ) -import VarEnv -import VarSet +import Var ( TyVar, mkTyVar, tyVarKind ) import ErrUtils ( Message ) -import TyCon ( TyCon, isSynTyCon, tyConArity, tyConKind ) +import TyCon ( TyCon, tyConKind ) import Class ( classTyCon ) import Name ( Name ) -import TysWiredIn ( mkListTy, mkTupleTy, genUnitTyCon ) +import NameSet +import TysWiredIn ( mkListTy, mkPArrTy, mkTupleTy, genUnitTyCon ) import BasicTypes ( Boxity(..) ) import SrcLoc ( SrcLoc ) -import Util ( isSingleton, lengthIs ) +import Util ( lengthIs ) import Outputable \end{code} @@ -194,21 +185,41 @@ tcHsTyVars tv_names kind_check thing_inside in tcExtendTyVarEnv tyvars (thing_inside tyvars) --- tcScopedTyVars is used for scoped type variables + + +tcAddScopedTyVars :: [RenamedHsType] -> TcM a -> TcM a +-- 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) -tcScopedTyVars :: [Name] - -> TcM a -- The kind checker - -> TcM b - -> TcM b -tcScopedTyVars [] kind_check thing_inside = thing_inside - -tcScopedTyVars tv_names kind_check thing_inside - = mapNF_Tc newNamedKindVar tv_names `thenTc` \ kind_env -> - tcExtendKindEnv kind_env kind_check `thenTc_` - zonkKindEnv kind_env `thenNF_Tc` \ tvs_w_kinds -> - listTc [tcNewMutTyVar name kind | (name, kind) <- tvs_w_kinds] `thenNF_Tc` \ tyvars -> + +-- Find the not-already-in-scope signature type variables, +-- kind-check them, and bring them into scope +-- +-- 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 +tcAddScopedTyVars [] thing_inside + = thing_inside -- Quick get-out for the empty case + +tcAddScopedTyVars sig_tys thing_inside + = tcGetEnv `thenNF_Tc` \ env -> + let + all_sig_tvs = foldr (unionNameSets . extractHsTyVars) emptyNameSet sig_tys + sig_tvs = filter not_in_scope (nameSetToList all_sig_tvs) + not_in_scope tv = not (tcInLocalScope env tv) + in + mapNF_Tc newNamedKindVar sig_tvs `thenTc` \ kind_env -> + tcExtendKindEnv kind_env (kcHsSigTypes sig_tys) `thenTc_` + zonkKindEnv kind_env `thenNF_Tc` \ tvs_w_kinds -> + listTc [ tcNewMutTyVar name kind PatSigTv + | (name, kind) <- tvs_w_kinds] `thenNF_Tc` \ tyvars -> tcExtendTyVarEnv tyvars thing_inside \end{code} @@ -252,10 +263,19 @@ kcHsLiftedSigType = kcLiftedType kcHsType :: RenamedHsType -> TcM TcKind kcHsType (HsTyVar name) = kcTyVar name +kcHsType (HsKindSig ty k) + = kcHsType ty `thenTc` \ k' -> + unifyKind k k' `thenTc_` + returnTc k + kcHsType (HsListTy ty) = kcLiftedType ty `thenTc` \ tau_ty -> returnTc liftedTypeKind +kcHsType (HsPArrTy ty) + = kcLiftedType ty `thenTc` \ tau_ty -> + returnTc liftedTypeKind + kcHsType (HsTupleTy (HsTupCon _ boxity _) tys) = mapTc kcTypeType tys `thenTc_` returnTc (case boxity of @@ -308,18 +328,27 @@ kcAppKind fun_kind arg_kind --------------------------- -kcHsContext ctxt = mapTc_ kcHsPred ctxt +kc_pred :: RenamedHsPred -> TcM TcKind -- Does *not* check for a saturated + -- application (reason: used from TcDeriv) +kc_pred pred@(HsIParam name ty) + = kcHsType ty + +kc_pred pred@(HsClassP cls tys) + = kcClass cls `thenTc` \ kind -> + mapTc kcHsType tys `thenTc` \ arg_kinds -> + newKindVar `thenNF_Tc` \ kv -> + unifyKind kind (mkArrowKinds arg_kinds kv) `thenTc_` + returnTc kv -kcHsPred :: RenamedHsPred -> TcM () -kcHsPred pred@(HsIParam name ty) - = tcAddErrCtxt (appKindCtxt (ppr pred)) $ - kcLiftedType ty +--------------------------- +kcHsContext ctxt = mapTc_ kcHsPred ctxt -kcHsPred pred@(HsClassP cls tys) +kcHsPred pred -- Checks that the result is of kind liftedType = tcAddErrCtxt (appKindCtxt (ppr pred)) $ - kcClass cls `thenTc` \ kind -> - mapTc kcHsType tys `thenTc` \ arg_kinds -> - unifyKind kind (mkArrowKinds arg_kinds liftedTypeKind) + kc_pred pred `thenTc` \ kind -> + unifyKind liftedTypeKind kind `thenTc_` + returnTc () + --------------------------- kcTyVar name -- Could be a tyvar or a tycon @@ -376,10 +405,17 @@ tc_type :: RenamedHsType -> TcM Type tc_type ty@(HsTyVar name) = tc_app ty [] +tc_type (HsKindSig ty k) + = tc_type ty -- Kind checking done already + tc_type (HsListTy ty) = tc_type ty `thenTc` \ tau_ty -> returnTc (mkListTy tau_ty) +tc_type (HsPArrTy ty) + = tc_type ty `thenTc` \ tau_ty -> + returnTc (mkPArrTy tau_ty) + tc_type (HsTupleTy (HsTupCon _ boxity arity) tys) = ASSERT( tys `lengthIs` arity ) tc_types tys `thenTc` \ tau_tys -> @@ -444,9 +480,7 @@ tc_fun_type name arg_tys case thing of ATyVar tv -> returnTc (mkAppTys (mkTyVarTy tv) arg_tys) - AGlobal (ATyCon tc) - | isSynTyCon tc -> returnTc (mkSynTy tc arg_tys) - | otherwise -> returnTc (mkTyConApp tc arg_tys) + AGlobal (ATyCon tc) -> returnTc (mkGenTyConApp tc arg_tys) other -> failWithTc (wrongThingErr "type constructor" thing name) \end{code} @@ -455,6 +489,10 @@ tc_fun_type name arg_tys Contexts ~~~~~~~~ \begin{code} +tcHsPred pred = kc_pred pred `thenTc_` tc_pred pred + -- Is happy with a partial application, e.g. (ST s) + -- Used from TcDeriv + tc_pred assn@(HsClassP class_name tys) = tcAddErrCtxt (appKindCtxt (ppr assn)) $ tc_types tys `thenTc` \ arg_tys -> @@ -509,8 +547,6 @@ been instantiated. \begin{code} data TcSigInfo = TySigInfo - Name -- N, the Name in corresponding binding - TcId -- *Polymorphic* binder for this value... -- Has name = N @@ -528,15 +564,21 @@ data TcSigInfo SrcLoc -- Of the signature instance Outputable TcSigInfo where - ppr (TySigInfo nm id tyvars theta tau _ inst loc) = - ppr nm <+> ptext SLIT("::") <+> ppr tyvars <+> ppr theta <+> ptext SLIT("=>") <+> ppr tau + 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_name _ _ _ _ _ _ _) : sigs) name - | name == sig_name = Just sig - | otherwise = maybeSig sigs name +maybeSig (sig@(TySigInfo sig_id _ _ _ _ _ _) : sigs) name + | name == idName sig_id = Just sig + | otherwise = maybeSig sigs name \end{code} @@ -558,280 +600,18 @@ mkTcSig poly_id src_loc -- 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 - let - (tyvars, rho) = tcSplitForAllTys (idType poly_id) - in - tcInstSigVars tyvars `thenNF_Tc` \ tyvars' -> - -- Make *signature* type variables - - let - tyvar_tys' = mkTyVarTys tyvars' - rho' = substTy (mkTopTyVarSubst tyvars tyvar_tys') rho - -- mkTopTyVarSubst because the tyvars' are fresh - - (theta', tau') = tcSplitRhoTy rho' - -- This splitRhoTy tries hard to make sure that tau' is a type synonym - -- wherever possible, which can improve interface files. - in + tcInstType SigTv (idType poly_id) `thenNF_Tc` \ (tyvars', theta', tau') -> + newMethodWithGivenTy SignatureOrigin - poly_id - tyvar_tys' - theta' tau' `thenNF_Tc` \ inst -> + poly_id + (mkTyVarTys tyvars') + theta' tau' `thenNF_Tc` \ inst -> -- We make a Method even if it's not overloaded; no harm - returnNF_Tc (TySigInfo name poly_id tyvars' theta' tau' (instToId inst) [inst] src_loc) - where - name = idName poly_id -\end{code} - - - -%************************************************************************ -%* * -\subsection{Checking signature type variables} -%* * -%************************************************************************ - -@checkSigTyVars@ is used after the type in a type signature has been unified with -the actual type found. It then checks that the type variables of the type signature -are - (a) Still all type variables - eg matching signature [a] against inferred type [(p,q)] - [then a will be unified to a non-type variable] - - (b) Still all distinct - eg matching signature [(a,b)] against inferred type [(p,p)] - [then a and b will be unified together] - - (c) Not mentioned in the environment - eg the signature for f in this: - - g x = ... where - f :: a->[a] - f y = [x,y] - - Here, f is forced to be monorphic by the free occurence of x. - - (d) Not (unified with another type variable that is) in scope. - eg f x :: (r->r) = (\y->y) :: forall a. a->r - when checking the expression type signature, we find that - even though there is nothing in scope whose type mentions r, - nevertheless the type signature for the expression isn't right. - - Another example is in a class or instance declaration: - class C a where - op :: forall b. a -> b - op x = x - Here, b gets unified with a - -Before doing this, the substitution is applied to the signature type variable. - -We used to have the notion of a "DontBind" type variable, which would -only be bound to itself or nothing. Then points (a) and (b) were -self-checking. But it gave rise to bogus consequential error messages. -For example: - - f = (*) -- Monomorphic - - g :: Num a => a -> a - g x = f x x - -Here, we get a complaint when checking the type signature for g, -that g isn't polymorphic enough; but then we get another one when -dealing with the (Num x) context arising from f's definition; -we try to unify x with Int (to default it), but find that x has already -been unified with the DontBind variable "a" from g's signature. -This is really a problem with side-effecting unification; we'd like to -undo g's effects when its type signature fails, but unification is done -by side effect, so we can't (easily). - -So we revert to ordinary type variables for signatures, and try to -give a helpful message in checkSigTyVars. - -\begin{code} -checkSigTyVars :: [TcTyVar] -- Universally-quantified type variables in the signature - -> TcTyVarSet -- Tyvars that are free in the type signature - -- Not necessarily zonked - -- These should *already* be in the free-in-env set, - -- and are used here only to improve the error message - -> TcM [TcTyVar] -- Zonked signature type variables - -checkSigTyVars [] free = returnTc [] -checkSigTyVars sig_tyvars free_tyvars - = zonkTcTyVars sig_tyvars `thenNF_Tc` \ sig_tys -> - tcGetGlobalTyVars `thenNF_Tc` \ globals -> - - checkTcM (allDistinctTyVars sig_tys globals) - (complain sig_tys globals) `thenTc_` - - returnTc (map (tcGetTyVar "checkSigTyVars") sig_tys) - - where - complain sig_tys globals - = -- For the in-scope ones, zonk them and construct a map - -- from the zonked tyvar to the in-scope one - -- If any of the in-scope tyvars zonk to a type, then ignore them; - -- that'll be caught later when we back up to their type sig - tcGetEnv `thenNF_Tc` \ env -> - let - in_scope_tvs = tcEnvTyVars env - in - zonkTcTyVars in_scope_tvs `thenNF_Tc` \ in_scope_tys -> - let - in_scope_assoc = [ (zonked_tv, in_scope_tv) - | (z_ty, in_scope_tv) <- in_scope_tys `zip` in_scope_tvs, - Just zonked_tv <- [tcGetTyVar_maybe z_ty] - ] - in_scope_env = mkVarEnv in_scope_assoc - in - - -- "check" checks each sig tyvar in turn - foldlNF_Tc check - (env2, in_scope_env, []) - (tidy_tvs `zip` tidy_tys) `thenNF_Tc` \ (env3, _, msgs) -> - - failWithTcM (env3, main_msg $$ nest 4 (vcat msgs)) - where - (env1, tidy_tvs) = tidyOpenTyVars emptyTidyEnv sig_tyvars - (env2, tidy_tys) = tidyOpenTypes env1 sig_tys - - main_msg = ptext SLIT("Inferred type is less polymorphic than expected") - - check (tidy_env, acc, msgs) (sig_tyvar,ty) - -- sig_tyvar is from the signature; - -- ty is what you get if you zonk sig_tyvar and then tidy it - -- - -- acc maps a zonked type variable back to a signature type variable - = case tcGetTyVar_maybe ty of { - Nothing -> -- Error (a)! - returnNF_Tc (tidy_env, acc, unify_msg sig_tyvar (quotes (ppr ty)) : msgs) ; - - Just tv -> - - case lookupVarEnv acc tv of { - Just sig_tyvar' -> -- Error (b) or (d)! - returnNF_Tc (tidy_env, acc, unify_msg sig_tyvar thing : msgs) - where - thing = ptext SLIT("another quantified type variable") <+> quotes (ppr sig_tyvar') - - ; Nothing -> - - if tv `elemVarSet` globals -- Error (c)! Type variable escapes - -- The least comprehensible, so put it last - -- Game plan: - -- a) get the local TcIds from the environment, - -- and pass them to find_globals (they might have tv free) - -- b) similarly, find any free_tyvars that mention tv - then tcGetEnv `thenNF_Tc` \ ve -> - find_globals tv tidy_env [] (tcEnvTcIds ve) `thenNF_Tc` \ (tidy_env1, globs) -> - find_frees tv tidy_env1 [] (varSetElems free_tyvars) `thenNF_Tc` \ (tidy_env2, frees) -> - returnNF_Tc (tidy_env2, acc, escape_msg sig_tyvar tv globs frees : msgs) - - else -- All OK - returnNF_Tc (tidy_env, extendVarEnv acc tv sig_tyvar, msgs) - }} - --- find_globals looks at the value environment and finds values --- whose types mention the offending type variable. It has to be --- careful to zonk the Id's type first, so it has to be in the monad. --- We must be careful to pass it a zonked type variable, too. - -find_globals :: Var - -> TidyEnv - -> [(Name,Type)] - -> [Id] - -> NF_TcM (TidyEnv,[(Name,Type)]) - -find_globals tv tidy_env acc [] - = returnNF_Tc (tidy_env, acc) - -find_globals tv tidy_env acc (id:ids) - | isEmptyVarSet (idFreeTyVars id) - = find_globals tv tidy_env acc ids - - | otherwise - = zonkTcType (idType id) `thenNF_Tc` \ id_ty -> - if tv `elemVarSet` tyVarsOfType id_ty then - let - (tidy_env', id_ty') = tidyOpenType tidy_env id_ty - acc' = (idName id, id_ty') : acc - in - find_globals tv tidy_env' acc' ids - else - find_globals tv tidy_env acc ids - -find_frees tv tidy_env acc [] - = returnNF_Tc (tidy_env, acc) -find_frees tv tidy_env acc (ftv:ftvs) - = zonkTcTyVar ftv `thenNF_Tc` \ ty -> - if tv `elemVarSet` tyVarsOfType ty then - let - (tidy_env', ftv') = tidyOpenTyVar tidy_env ftv - in - find_frees tv tidy_env' (ftv':acc) ftvs - else - find_frees tv tidy_env acc ftvs - - -escape_msg sig_tv tv globs frees - = mk_msg sig_tv <+> ptext SLIT("escapes") $$ - if not (null globs) then - vcat [pp_it <+> ptext SLIT("is mentioned in the environment"), - ptext SLIT("The following variables in the environment mention") <+> quotes (ppr tv), - nest 2 (vcat_first 10 [ppr name <+> dcolon <+> ppr ty | (name,ty) <- globs]) - ] - else if not (null frees) then - vcat [ptext SLIT("It is reachable from the type variable(s)") <+> pprQuotedList frees, - nest 2 (ptext SLIT("which") <+> is_are <+> ptext SLIT("free in the signature")) - ] - else - empty -- Sigh. It's really hard to give a good error message - -- all the time. One bad case is an existential pattern match - where - is_are | isSingleton frees = ptext SLIT("is") - | otherwise = ptext SLIT("are") - pp_it | sig_tv /= tv = ptext SLIT("It unifies with") <+> quotes (ppr tv) <> comma <+> ptext SLIT("which") - | otherwise = ptext SLIT("It") - - vcat_first :: Int -> [SDoc] -> SDoc - vcat_first n [] = empty - vcat_first 0 (x:xs) = text "...others omitted..." - vcat_first n (x:xs) = x $$ vcat_first (n-1) xs - -unify_msg tv thing = mk_msg tv <+> ptext SLIT("is unified with") <+> thing -mk_msg tv = ptext SLIT("Quantified type variable") <+> quotes (ppr tv) + returnNF_Tc (TySigInfo poly_id tyvars' theta' tau' + (instToId inst) [inst] src_loc) \end{code} -These two context are used with checkSigTyVars - -\begin{code} -sigCtxt :: Message -> [TcTyVar] -> TcThetaType -> TcTauType - -> TidyEnv -> NF_TcM (TidyEnv, Message) -sigCtxt when sig_tyvars sig_theta sig_tau tidy_env - = zonkTcType sig_tau `thenNF_Tc` \ actual_tau -> - let - (env1, tidy_sig_tyvars) = tidyOpenTyVars tidy_env sig_tyvars - (env2, tidy_sig_rho) = tidyOpenType env1 (mkRhoTy sig_theta sig_tau) - (env3, tidy_actual_tau) = tidyOpenType env2 actual_tau - msg = vcat [ptext SLIT("Signature type: ") <+> pprType (mkForAllTys tidy_sig_tyvars tidy_sig_rho), - ptext SLIT("Type to generalise:") <+> pprType tidy_actual_tau, - when - ] - in - returnNF_Tc (env3, msg) - -sigPatCtxt bound_tvs bound_ids tidy_env - = returnNF_Tc (env1, - sep [ptext SLIT("When checking a pattern that binds"), - nest 4 (vcat (zipWith ppr_id show_ids tidy_tys))]) - where - show_ids = filter is_interesting bound_ids - is_interesting id = any (`elemVarSet` idFreeTyVars id) bound_tvs - - (env1, tidy_tys) = tidyOpenTypes tidy_env (map idType show_ids) - ppr_id id ty = ppr id <+> dcolon <+> ppr ty - -- Don't zonk the types so we get the separate, un-unified versions -\end{code} %************************************************************************