X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=ghc%2Fcompiler%2Ftypecheck%2FTcBinds.lhs;h=c4e1b92f6c981640dce050094c6cfaeafa1b4d51;hb=ff818166a0a06e77becad9e28ed116f3b7f5cc8b;hp=9db0b3a69e1bfceac650c90d1e1b71f64ca07b24;hpb=759739c69f9cd540f03c3c69aa1990d5d58a5dd6;p=ghc-hetmet.git diff --git a/ghc/compiler/typecheck/TcBinds.lhs b/ghc/compiler/typecheck/TcBinds.lhs index 9db0b3a..c4e1b92 100644 --- a/ghc/compiler/typecheck/TcBinds.lhs +++ b/ghc/compiler/typecheck/TcBinds.lhs @@ -4,7 +4,7 @@ \section[TcBinds]{TcBinds} \begin{code} -module TcBinds ( tcBindsAndThen, tcTopBinds, tcMonoBinds, tcSpecSigs ) where +module TcBinds ( tcBindsAndThen, tcTopBinds, tcHsBootSigs, tcMonoBinds, tcSpecSigs ) where #include "HsVersions.h" @@ -13,7 +13,8 @@ import {-# SOURCE #-} TcExpr ( tcCheckSigma, tcCheckRho ) import CmdLineOpts ( DynFlag(Opt_MonomorphismRestriction) ) import HsSyn ( HsExpr(..), HsBind(..), LHsBinds, Sig(..), - LSig, Match(..), HsBindGroup(..), IPBind(..), + LSig, Match(..), HsBindGroup(..), IPBind(..), + HsType(..), hsLTyVarNames, isVanillaLSig, LPat, GRHSs, MatchGroup(..), emptyLHsBinds, isEmptyLHsBinds, collectHsBindBinders, collectPatBinders, pprPatBind ) @@ -21,31 +22,32 @@ import TcHsSyn ( TcId, TcDictBinds, zonkId, mkHsLet ) import TcRnMonad import Inst ( InstOrigin(..), newDictsAtLoc, newIPDict, instToId ) -import TcEnv ( tcExtendIdEnv, tcExtendIdEnv2, newLocalName, tcLookupLocalIds ) -import TcUnify ( Expected(..), tcInfer, checkSigTyVars, sigCtxt ) +import TcEnv ( tcExtendIdEnv, tcExtendIdEnv2, tcExtendTyVarEnv2, + newLocalName, tcLookupLocalIds, pprBinders, + tcGetGlobalTyVars ) +import TcUnify ( Expected(..), tcInfer, unifyTheta, + bleatEscapedTvs, sigCtxt ) import TcSimplify ( tcSimplifyInfer, tcSimplifyInferCheck, tcSimplifyRestricted, tcSimplifyToDicts, tcSimplifyIPs ) import TcHsType ( tcHsSigType, UserTypeCtxt(..), tcAddLetBoundTyVars, - TcSigInfo(..), TcSigFun, mkTcSig, lookupSig + TcSigInfo(..), TcSigFun, lookupSig ) import TcPat ( tcPat, PatCtxt(..) ) import TcSimplify ( bindInstsOfLocalFuns ) -import TcMType ( newTyFlexiVarTy, tcSkolType, zonkQuantifiedTyVar, zonkTcTypes ) +import TcMType ( newTyFlexiVarTy, zonkQuantifiedTyVar, + tcInstSigType, zonkTcTypes, zonkTcTyVar ) import TcType ( TcTyVar, SkolemInfo(SigSkol), TcTauType, TcSigmaType, - TvSubstEnv, mkTvSubst, substTheta, substTy, mkTyVarTy, mkForAllTys, mkFunTys, tyVarsOfType, - mkForAllTy, isUnLiftedType, tcGetTyVar_maybe, - mkTyVarTys ) -import Unify ( tcMatchPreds ) -import Kind ( argTypeKind, isUnliftedTypeKind ) -import VarEnv ( lookupVarEnv ) + mkForAllTy, isUnLiftedType, tcGetTyVar, + mkTyVarTys, tidyOpenTyVar, tidyOpenType ) +import Kind ( argTypeKind ) +import VarEnv ( TyVarEnv, emptyVarEnv, lookupVarEnv, extendVarEnv, emptyTidyEnv ) import TysPrim ( alphaTyVar ) import Id ( mkLocalId, mkSpecPragmaId, setInlinePragma ) import Var ( idType, idName ) import Name ( Name ) import NameSet -import Var ( tyVarKind ) import VarSet import SrcLoc ( Located(..), unLoc, noLoc, getLoc ) import Bag @@ -94,15 +96,28 @@ tcTopBinds :: [HsBindGroup Name] -> TcM (LHsBinds TcId, TcLclEnv) -- want. The bit we care about is the local bindings -- and the free type variables thereof tcTopBinds binds - = tc_binds_and_then TopLevel glue binds $ - getLclEnv `thenM` \ env -> - returnM (emptyLHsBinds, env) + = tc_binds_and_then TopLevel glue binds $ + do { env <- getLclEnv + ; return (emptyLHsBinds, env) } where -- The top level bindings are flattened into a giant -- implicitly-mutually-recursive MonoBinds glue (HsBindGroup binds1 _ _) (binds2, env) = (binds1 `unionBags` binds2, env) + glue (HsIPBinds _) _ = panic "Top-level HsIpBinds" -- Can't have a HsIPBinds at top level +tcHsBootSigs :: [HsBindGroup Name] -> TcM (LHsBinds TcId, TcLclEnv) +-- A hs-boot file has only one BindGroup, and it only has type +-- signatures in it. The renamer checked all this +tcHsBootSigs [HsBindGroup _ sigs _] + = do { ids <- mapM (addLocM tc_sig) (filter isVanillaLSig sigs) + ; tcExtendIdEnv ids $ do + { env <- getLclEnv + ; return (emptyLHsBinds, env) }} + where + tc_sig (Sig (L _ name) ty) + = do { sigma_ty <- tcHsSigType (FunSigCtxt name) ty + ; return (mkLocalId name sigma_ty) } tcBindsAndThen :: (HsBindGroup TcId -> thing -> thing) -- Combinator @@ -242,7 +257,7 @@ tcBindWithSigs :: TopLevelFlag tcBindWithSigs top_lvl mbind sigs is_rec = do { -- TYPECHECK THE SIGNATURES tc_ty_sigs <- recoverM (returnM []) $ - tcTySigs [sig | sig@(L _(Sig name _)) <- sigs] + tcTySigs (filter isVanillaLSig sigs) ; let lookup_sig = lookupSig tc_ty_sigs -- SET UP THE MAIN RECOVERY; take advantage of any type sigs @@ -277,7 +292,7 @@ tcBindWithSigs top_lvl mbind sigs is_rec = do -- TODO: location a bit awkward, but the mbinds have been -- dependency analysed and may no longer be adjacent addErrCtxt (genCtxt (bndrNames mono_bind_infos)) $ - generalise is_unres mono_bind_infos tc_ty_sigs lie_req + generalise top_lvl is_unres mono_bind_infos tc_ty_sigs lie_req -- FINALISE THE QUANTIFIED TYPE VARIABLES -- The quantified type variables often include meta type variables @@ -434,22 +449,27 @@ tcMonoBinds :: LHsBinds Name -> TcSigFun -> RecFlag -> TcM (LHsBinds TcId, [MonoBindInfo]) -type MonoBindInfo = (Name, Maybe TcSigInfo, TcId) - -- Type signature (if any), and - -- the monomorphic bound things - -bndrNames :: [MonoBindInfo] -> [Name] -bndrNames mbi = [n | (n,_,_) <- mbi] - -getMonoType :: MonoBindInfo -> TcTauType -getMonoType (_,_,mono_id) = idType mono_id - tcMonoBinds binds lookup_sig is_rec = do { tc_binds <- mapBagM (wrapLocM (tcLhs lookup_sig)) binds - ; let mono_info = getMonoBindInfo tc_binds - ; binds' <- tcExtendIdEnv2 (rhsEnvExtension mono_info) $ + + -- Bring (a) the scoped type variables, and (b) the Ids, into scope for the RHSs + -- For (a) it's ok to bring them all into scope at once, even + -- though each type sig should scope only over its own RHS, + -- because the renamer has sorted all that out. + ; let mono_info = getMonoBindInfo tc_binds + rhs_tvs = [ (name, mkTyVarTy tv) + | (_, Just sig, _) <- mono_info, + (name, tv) <- sig_scoped sig `zip` sig_tvs sig ] + rhs_id_env = map mk mono_info -- A binding for each term variable + + ; binds' <- tcExtendTyVarEnv2 rhs_tvs $ + tcExtendIdEnv2 rhs_id_env $ + traceTc (text "tcMonoBinds" <+> vcat [ppr n <+> ppr id <+> ppr (idType id) | (n,id) <- rhs_id_env]) `thenM_` mapBagM (wrapLocM tcRhs) tc_binds ; return (binds', mono_info) } + where + mk (name, Just sig, _) = (name, sig_id sig) -- Use the type sig if there is one + mk (name, Nothing, mono_id) = (name, mono_id) -- otherwise use a monomorphic version ------------------------ -- tcLhs typechecks the LHS of the bindings, to construct the environment in which @@ -471,6 +491,16 @@ data TcMonoBind -- Half completed; LHS done, RHS not done = TcFunBind MonoBindInfo (Located TcId) Bool (MatchGroup Name) | TcPatBind [MonoBindInfo] (LPat TcId) (GRHSs Name) TcSigmaType +type MonoBindInfo = (Name, Maybe TcSigInfo, TcId) + -- Type signature (if any), and + -- the monomorphic bound things + +bndrNames :: [MonoBindInfo] -> [Name] +bndrNames mbi = [n | (n,_,_) <- mbi] + +getMonoType :: MonoBindInfo -> TcTauType +getMonoType (_,_,mono_id) = idType mono_id + tcLhs :: TcSigFun -> HsBind Name -> TcM TcMonoBind tcLhs lookup_sig (FunBind (L nm_loc name) inf matches) = do { let mb_sig = lookup_sig name @@ -504,7 +534,7 @@ tcLhs lookup_sig bind@(PatBind pat grhss _) ------------------- tcRhs :: TcMonoBind -> TcM (HsBind TcId) -tcRhs (TcFunBind _ fun'@(L _ mono_id) inf matches) +tcRhs (TcFunBind info fun'@(L _ mono_id) inf matches) = do { matches' <- tcMatchesFun (idName mono_id) matches (Check (idType mono_id)) ; return (FunBind fun' inf matches') } @@ -522,15 +552,6 @@ getMonoBindInfo tc_binds where get_info (TcFunBind info _ _ _) rest = info : rest get_info (TcPatBind infos _ _ _) rest = infos ++ rest - ---------------------- -rhsEnvExtension :: [MonoBindInfo] -> [(Name, TcId)] --- Environment for RHS of definitions: use type sig if there is one -rhsEnvExtension mono_info - = map mk mono_info - where - mk (name, Just sig, _) = (name, sig_id sig) - mk (name, Nothing, mono_id) = (name, mono_id) \end{code} @@ -540,6 +561,8 @@ rhsEnvExtension mono_info %* * %************************************************************************ +Type signatures are tricky. See Note [Signature skolems] in TcType + \begin{code} tcTySigs :: [LSig Name] -> TcM [TcSigInfo] -- The trick here is that all the signatures should have the same @@ -547,67 +570,50 @@ tcTySigs :: [LSig Name] -> TcM [TcSigInfo] -- all the right hand sides agree a common vocabulary for their type -- constraints tcTySigs [] = return [] -tcTySigs (L span (Sig (L _ name) ty) : sigs) - = do { -- Typecheck the first signature - ; sigma1 <- setSrcSpan span $ - tcHsSigType (FunSigCtxt name) ty - ; let id1 = mkLocalId name sigma1 - ; tc_sig1 <- mkTcSig id1 - - ; tc_sigs <- mapM (tcTySig tc_sig1) sigs - ; return (tc_sig1 : tc_sigs) } -tcTySig sig1 (L span (Sig (L _ name) ty)) +tcTySigs sigs + = do { (tc_sig1 : tc_sigs) <- mappM tcTySig sigs + ; mapM (check_ctxt tc_sig1) tc_sigs + ; return (tc_sig1 : tc_sigs) } + where + -- Check tha all the signature contexts are the same + -- The type signatures on a mutually-recursive group of definitions + -- must all have the same context (or none). + -- + -- We unify them because, with polymorphic recursion, their types + -- might not otherwise be related. This is a rather subtle issue. + check_ctxt :: TcSigInfo -> TcSigInfo -> TcM () + check_ctxt sig1@(TcSigInfo { sig_theta = theta1 }) sig@(TcSigInfo { sig_theta = theta }) + = setSrcSpan (instLocSrcSpan (sig_loc sig)) $ + addErrCtxt (sigContextsCtxt sig1 sig) $ + unifyTheta theta1 theta + + +tcTySig :: LSig Name -> TcM TcSigInfo +tcTySig (L span (Sig (L _ name) ty)) = setSrcSpan span $ do { sigma_ty <- tcHsSigType (FunSigCtxt name) ty - ; (tvs, theta, tau) <- tcSkolType rigid_info sigma_ty - ; let poly_id = mkLocalId name sigma_ty - bale_out = failWithTc $ - sigContextsErr (sig_id sig1) name sigma_ty - - -- Try to match the context of this signature with - -- that of the first signature - ; case tcMatchPreds tvs (sig_theta sig1) theta of { - Nothing -> bale_out - ; Just tenv -> do - ; case check_tvs tenv tvs of - Nothing -> bale_out - Just tvs' -> do { - - let subst = mkTvSubst tenv - theta' = substTheta subst theta - tau' = substTy subst tau - ; loc <- getInstLoc (SigOrigin rigid_info) - ; return (TcSigInfo { sig_id = poly_id, sig_tvs = tvs', - sig_theta = theta', sig_tau = tau', - sig_loc = loc }) }}} - where - rigid_info = SigSkol name - - -- Rather tedious check that the type variables - -- have been matched only with another type variable, - -- and that two type variables have not been matched - -- with the same one - -- A return of Nothing indicates that one of the bad - -- things has happened - check_tvs :: TvSubstEnv -> [TcTyVar] -> Maybe [TcTyVar] - check_tvs tenv [] = Just [] - check_tvs tenv (tv:tvs) - | Just ty <- lookupVarEnv tenv tv - = do { tv' <- tcGetTyVar_maybe ty - ; tvs' <- check_tvs tenv tvs - ; if tv' `elem` tvs' - then Nothing - else Just (tv':tvs') } - | otherwise - = do { tvs' <- check_tvs tenv tvs - ; Just (tv:tvs') } + ; (tvs, theta, tau) <- tcInstSigType name sigma_ty + ; loc <- getInstLoc (SigOrigin (SigSkol name)) + + ; let poly_id = mkLocalId name sigma_ty + + -- The scoped names are the ones explicitly mentioned + -- in the HsForAll. (There may be more in sigma_ty, because + -- of nested type synonyms. See Note [Scoped] with TcSigInfo.) + scoped_names = case ty of + L _ (HsForAllTy _ tvs _ _) -> hsLTyVarNames tvs + other -> [] + + ; return (TcSigInfo { sig_id = poly_id, sig_scoped = scoped_names, + sig_tvs = tvs, sig_theta = theta, sig_tau = tau, + sig_loc = loc }) } \end{code} \begin{code} -generalise :: Bool -> [MonoBindInfo] -> [TcSigInfo] -> [Inst] +generalise :: TopLevelFlag -> Bool -> [MonoBindInfo] -> [TcSigInfo] -> [Inst] -> TcM ([TcTyVar], TcDictBinds, [TcId]) -generalise is_unrestricted mono_infos sigs lie_req +generalise top_lvl is_unrestricted mono_infos sigs lie_req | not is_unrestricted -- RESTRICTED CASE = -- Check signature contexts are empty do { checkTc (all is_mono_sig sigs) @@ -615,7 +621,8 @@ generalise is_unrestricted mono_infos sigs lie_req -- Now simplify with exactly that set of tyvars -- We have to squash those Methods - ; (qtvs, binds) <- tcSimplifyRestricted doc tau_tvs lie_req + ; (qtvs, binds) <- tcSimplifyRestricted doc top_lvl bndr_names + tau_tvs lie_req -- Check that signature type variables are OK ; final_qtvs <- checkSigsTyVars qtvs sigs @@ -649,34 +656,74 @@ generalise is_unrestricted mono_infos sigs lie_req is_mono_sig sig = null (sig_theta sig) doc = ptext SLIT("type signature(s) for") <+> pprBinders bndr_names -mkMethInst (TcSigInfo { sig_id = poly_id, sig_tvs = tvs, - sig_theta = theta, sig_tau = tau, sig_loc = loc }) mono_id - = Method mono_id poly_id (mkTyVarTys tvs) theta tau loc + mkMethInst (TcSigInfo { sig_id = poly_id, sig_tvs = tvs, + sig_theta = theta, sig_tau = tau, sig_loc = loc }) mono_id + = Method mono_id poly_id (mkTyVarTys tvs) theta tau loc checkSigsTyVars :: [TcTyVar] -> [TcSigInfo] -> TcM [TcTyVar] checkSigsTyVars qtvs sigs - = mappM check_one sigs `thenM` \ sig_tvs_s -> - let - -- Sigh. Make sure that all the tyvars in the type sigs - -- appear in the returned ty var list, which is what we are - -- going to generalise over. Reason: we occasionally get - -- silly types like - -- type T a = () -> () - -- f :: T a - -- f () = () - -- Here, 'a' won't appear in qtvs, so we have to add it - - sig_tvs = foldl extendVarSetList emptyVarSet sig_tvs_s - all_tvs = extendVarSetList sig_tvs qtvs - in - returnM (varSetElems all_tvs) + = do { gbl_tvs <- tcGetGlobalTyVars + ; sig_tvs_s <- mappM (check_sig gbl_tvs) sigs + + ; let -- Sigh. Make sure that all the tyvars in the type sigs + -- appear in the returned ty var list, which is what we are + -- going to generalise over. Reason: we occasionally get + -- silly types like + -- type T a = () -> () + -- f :: T a + -- f () = () + -- Here, 'a' won't appear in qtvs, so we have to add it + sig_tvs = foldl extendVarSetList emptyVarSet sig_tvs_s + all_tvs = varSetElems (extendVarSetList sig_tvs qtvs) + ; returnM all_tvs } where - check_one (TcSigInfo {sig_id = id, sig_tvs = tvs, sig_theta = theta, sig_tau = tau}) - = addErrCtxt (ptext SLIT("In the type signature for") - <+> quotes (ppr id)) $ - addErrCtxtM (sigCtxt id tvs theta tau) $ - do { checkSigTyVars tvs; return tvs } -\end{code} + check_sig gbl_tvs (TcSigInfo {sig_id = id, sig_tvs = tvs, + sig_theta = theta, sig_tau = tau}) + = addErrCtxt (ptext SLIT("In the type signature for") <+> quotes (ppr id)) $ + addErrCtxtM (sigCtxt id tvs theta tau) $ + do { tvs' <- checkDistinctTyVars tvs + ; ifM (any (`elemVarSet` gbl_tvs) tvs') + (bleatEscapedTvs gbl_tvs tvs tvs') + ; return tvs' } + +checkDistinctTyVars :: [TcTyVar] -> TcM [TcTyVar] +-- (checkDistinctTyVars tvs) checks that the tvs from one type signature +-- are still all type variables, and all distinct from each other. +-- It returns a zonked set of type variables. +-- For example, if the type sig is +-- f :: forall a b. a -> b -> b +-- we want to check that 'a' and 'b' haven't +-- (a) been unified with a non-tyvar type +-- (b) been unified with each other (all distinct) + +checkDistinctTyVars sig_tvs + = do { zonked_tvs <- mapM zonk_one sig_tvs + ; foldlM check_dup emptyVarEnv (sig_tvs `zip` zonked_tvs) + ; return zonked_tvs } + where + zonk_one sig_tv = do { ty <- zonkTcTyVar sig_tv + ; return (tcGetTyVar "checkDistinctTyVars" ty) } + -- 'ty' is bound to be a type variable, because SigSkolTvs + -- can only be unified with type variables + + check_dup :: TyVarEnv TcTyVar -> (TcTyVar, TcTyVar) -> TcM (TyVarEnv TcTyVar) + -- The TyVarEnv maps each zonked type variable back to its + -- corresponding user-written signature type variable + check_dup acc (sig_tv, zonked_tv) + = case lookupVarEnv acc zonked_tv of + Just sig_tv' -> bomb_out sig_tv sig_tv' + + Nothing -> return (extendVarEnv acc zonked_tv sig_tv) + + bomb_out sig_tv1 sig_tv2 + = failWithTc (ptext SLIT("Quantified type variable") <+> quotes (ppr tidy_tv1) + <+> ptext SLIT("is unified with another quantified type variable") + <+> ppr tidy_tv2) + where + (env1, tidy_tv1) = tidyOpenTyVar emptyTidyEnv sig_tv1 + (_env2, tidy_tv2) = tidyOpenTyVar env1 sig_tv2 +\end{code} + @getTyVarsToGen@ decides what type variables to generalise over. @@ -834,11 +881,14 @@ valSpecSigCtxt v ty nest 4 (ppr v <+> dcolon <+> ppr ty)] ----------------------------------------------- -sigContextsErr id1 name ty - = vcat [ptext SLIT("Mis-match between the contexts of the signatures for"), +sigContextsCtxt sig1 sig2 + = vcat [ptext SLIT("When matching the contexts of the signatures for"), nest 2 (vcat [ppr id1 <+> dcolon <+> ppr (idType id1), - ppr name <+> dcolon <+> ppr ty]), + ppr id2 <+> dcolon <+> ppr (idType id2)]), ptext SLIT("The signature contexts in a mutually recursive group should all be identical")] + where + id1 = sig_id sig1 + id2 = sig_id sig2 ----------------------------------------------- @@ -861,9 +911,4 @@ restrictedBindCtxtErr binder_names genCtxt binder_names = ptext SLIT("When generalising the type(s) for") <+> pprBinders binder_names - --- Used in error messages --- Use quotes for a single one; they look a bit "busy" for several -pprBinders [bndr] = quotes (ppr bndr) -pprBinders bndrs = pprWithCommas ppr bndrs \end{code}