X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=ghc%2Fcompiler%2Ftypecheck%2FTcBinds.lhs;h=c4e1b92f6c981640dce050094c6cfaeafa1b4d51;hb=ff818166a0a06e77becad9e28ed116f3b7f5cc8b;hp=395744d7c0bdc6f605bf78cb5ade89b37ec1bf44;hpb=508a505e9853984bfdaa3ad855ae3fcbc6d31787;p=ghc-hetmet.git diff --git a/ghc/compiler/typecheck/TcBinds.lhs b/ghc/compiler/typecheck/TcBinds.lhs index 395744d..c4e1b92 100644 --- a/ghc/compiler/typecheck/TcBinds.lhs +++ b/ghc/compiler/typecheck/TcBinds.lhs @@ -22,8 +22,11 @@ import TcHsSyn ( TcId, TcDictBinds, zonkId, mkHsLet ) import TcRnMonad import Inst ( InstOrigin(..), newDictsAtLoc, newIPDict, instToId ) -import TcEnv ( tcExtendIdEnv, tcExtendIdEnv2, tcExtendTyVarEnv2, 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, @@ -31,16 +34,15 @@ import TcHsType ( tcHsSigType, UserTypeCtxt(..), tcAddLetBoundTyVars, ) 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 ) + mkForAllTy, isUnLiftedType, tcGetTyVar, + mkTyVarTys, tidyOpenTyVar, tidyOpenType ) import Kind ( argTypeKind ) -import VarEnv ( lookupVarEnv ) +import VarEnv ( TyVarEnv, emptyVarEnv, lookupVarEnv, extendVarEnv, emptyTidyEnv ) import TysPrim ( alphaTyVar ) import Id ( mkLocalId, mkSpecPragmaId, setInlinePragma ) import Var ( idType, idName ) @@ -50,7 +52,6 @@ import VarSet import SrcLoc ( Located(..), unLoc, noLoc, getLoc ) import Bag import Util ( isIn ) -import Maybes ( orElse ) import BasicTypes ( TopLevelFlag(..), RecFlag(..), isNonRec, isRec, isNotTopLevel, isAlwaysActive ) import FiniteMap ( listToFM, lookupFM ) @@ -291,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 @@ -463,6 +464,7 @@ tcMonoBinds binds lookup_sig is_rec ; 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 @@ -559,6 +561,8 @@ getMonoBindInfo tc_binds %* * %************************************************************************ +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 @@ -569,15 +573,30 @@ tcTySigs [] = return [] tcTySigs sigs = do { (tc_sig1 : tc_sigs) <- mappM tcTySig sigs - ; tc_sigs' <- mapM (checkSigCtxt tc_sig1) tc_sigs - ; return (tc_sig1 : tc_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 - ; let rigid_info = SigSkol name - poly_id = mkLocalId name sigma_ty + ; (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 @@ -586,57 +605,15 @@ tcTySig (L span (Sig (L _ name) ty)) L _ (HsForAllTy _ tvs _ _) -> hsLTyVarNames tvs other -> [] - ; (tvs, theta, tau) <- tcSkolType rigid_info sigma_ty - ; loc <- getInstLoc (SigOrigin rigid_info) ; return (TcSigInfo { sig_id = poly_id, sig_scoped = scoped_names, sig_tvs = tvs, sig_theta = theta, sig_tau = tau, sig_loc = loc }) } - -checkSigCtxt :: TcSigInfo -> TcSigInfo -> TcM TcSigInfo -checkSigCtxt sig1 sig@(TcSigInfo { sig_tvs = tvs, sig_theta = theta, sig_tau = tau }) - = -- Try to match the context of this signature with - -- that of the first signature - case tcMatchPreds (sig_tvs sig) (sig_theta sig) (sig_theta sig1) of { - Nothing -> bale_out ; - Just tenv -> - - case check_tvs tenv tvs of { - Nothing -> bale_out ; - Just tvs' -> - - let - subst = mkTvSubst tenv - in - return (sig { sig_tvs = tvs', - sig_theta = substTheta subst theta, - sig_tau = substTy subst tau }) }} - - where - bale_out = setSrcSpan (instLocSrcSpan (sig_loc sig)) $ - failWithTc $ - sigContextsErr (sig_id sig1) (sig_id sig) - - -- 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) - = do { let ty = lookupVarEnv tenv tv `orElse` mkTyVarTy tv - ; tv' <- tcGetTyVar_maybe ty - ; tvs' <- check_tvs tenv tvs - ; if tv' `elem` tvs' - then Nothing - else Just (tv':tvs') } \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) @@ -644,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 @@ -678,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. @@ -863,11 +881,14 @@ valSpecSigCtxt v ty nest 4 (ppr v <+> dcolon <+> ppr ty)] ----------------------------------------------- -sigContextsErr id1 id2 - = 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 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 ----------------------------------------------- @@ -890,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}