X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcUnify.lhs;h=2b42d0b9e37e9251333880d4ba91599c046f3db6;hb=f493bc7c7325a3809dda3637c12e5d9383ba8117;hp=de9c34191cc5983d81ad773b649a29bcffa562ae;hpb=a2fcf3aa210edff15c5f4603ac267171f89366f0;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs index de9c341..2b42d0b 100644 --- a/compiler/typecheck/TcUnify.lhs +++ b/compiler/typecheck/TcUnify.lhs @@ -44,6 +44,7 @@ import TysWiredIn import Var import VarSet import VarEnv +import Module import Name import ErrUtils import Maybes @@ -112,6 +113,7 @@ subFunTys error_herald n_pats res_ty thing_inside where -- In 'loop', the parameter 'arg_tys' accumulates -- the arg types so far, in *reverse order* + -- INVARIANT: res_ty :: * loop n args_so_far res_ty | Just res_ty' <- tcView res_ty = loop n args_so_far res_ty' @@ -142,7 +144,7 @@ subFunTys error_herald n_pats res_ty thing_inside else loop n args_so_far (FunTy arg_ty' res_ty') } loop n args_so_far (TyVarTy tv) - | not (isImmutableTyVar tv) + | isTyConableTyVar tv = do { cts <- readMetaTyVar tv ; case cts of Indirect ty -> loop n args_so_far ty @@ -193,10 +195,12 @@ boxySplitTyConApp tc orig_ty return (args ++ args_so_far) loop n_req args_so_far (AppTy fun arg) + | n_req > 0 = loop (n_req - 1) (arg:args_so_far) fun loop n_req args_so_far (TyVarTy tv) - | not (isImmutableTyVar tv) + | isTyConableTyVar tv + , res_kind `isSubKind` tyVarKind tv = do { cts <- readMetaTyVar tv ; case cts of Indirect ty -> loop n_req args_so_far ty @@ -205,7 +209,7 @@ boxySplitTyConApp tc orig_ty } where mk_res_ty arg_tys' = mkTyConApp tc arg_tys' - arg_kinds = map tyVarKind (take n_req (tyConTyVars tc)) + (arg_kinds, res_kind) = splitKindFunTysN n_req (tyConKind tc) loop _ _ _ = boxySplitFailure (mkTyConApp tc (mkTyVarTys (tyConTyVars tc))) orig_ty @@ -218,7 +222,8 @@ boxySplitListTy exp_ty = do { [elt_ty] <- boxySplitTyConApp listTyCon exp_ty ---------------------- boxySplitAppTy :: BoxyRhoType -- Type to split: m a -> TcM (BoxySigmaType, BoxySigmaType) -- Returns m, a --- Assumes (m: * -> k), where k is the kind of the incoming type +-- If the incoming type is a mutable type variable of kind k, then +-- boxySplitAppTy returns a new type variable (m: * -> k); note the *. -- If the incoming type is boxy, then so are the result types; and vice versa boxySplitAppTy orig_ty @@ -232,7 +237,7 @@ boxySplitAppTy orig_ty = return (fun_ty, arg_ty) loop (TyVarTy tv) - | not (isImmutableTyVar tv) + | isTyConableTyVar tv = do { cts <- readMetaTyVar tv ; case cts of Indirect ty -> loop ty @@ -522,7 +527,7 @@ boxyLub orig_ty1 orig_ty2 -- Look inside type synonyms, but only if the naive version fails go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2 - | Just ty2' <- tcView ty1 = go ty1 ty2' + | Just ty2' <- tcView ty2 = go ty1 ty2' -- For now, we don't look inside ForAlls, PredTys go ty1 ty2 = orig_ty1 -- Default @@ -721,8 +726,12 @@ tc_sub1 sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty ----------------------------------- defer_to_boxy_matching sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty = do { addSubCtxt sub_ctxt act_sty exp_sty $ - u_tys True False act_sty actual_ty exp_ib exp_sty expected_ty + u_tys outer False act_sty actual_ty exp_ib exp_sty expected_ty ; return idHsWrapper } + where + outer = case sub_ctxt of -- Ugh + SubDone -> False + other -> True ----------------------------------- tc_sub_funs act_arg act_res exp_ib exp_arg exp_res @@ -962,17 +971,23 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2 -- Get location from monad, not from tvs1 ; let tys = mkTyVarTys tvs in_scope = mkInScopeSet (mkVarSet tvs) - subst1 = mkTvSubst in_scope (zipTyEnv tvs1 tys) - subst2 = mkTvSubst in_scope (zipTyEnv tvs2 tys) - (theta1,tau1) = tcSplitPhiTy (substTy subst1 body1) - (theta2,tau2) = tcSplitPhiTy (substTy subst2 body2) + phi1 = substTy (mkTvSubst in_scope (zipTyEnv tvs1 tys)) body1 + phi2 = substTy (mkTvSubst in_scope (zipTyEnv tvs2 tys)) body2 + (theta1,tau1) = tcSplitPhiTy phi1 + (theta2,tau2) = tcSplitPhiTy phi2 - ; checkM (equalLength theta1 theta2) + ; addErrCtxtM (unifyForAllCtxt tvs phi1 phi2) $ do + { checkM (equalLength theta1 theta2) (unifyMisMatch outer False orig_ty1 orig_ty2) ; uPreds False nb1 theta1 nb2 theta2 ; uTys nb1 tau1 nb2 tau2 + -- Check for escape; e.g. (forall a. a->b) ~ (forall a. a->a) + ; free_tvs <- zonkTcTyVarsAndFV (varSetElems (tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2)) + ; ifM (any (`elemVarSet` free_tvs) tvs) + (bleatEscapedTvs free_tvs tvs tvs) + -- If both sides are inside a box, we are in a "box-meets-box" -- situation, and we should not have a polytype at all. -- If we get here we have two boxes, already filled with @@ -980,7 +995,7 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2 -- This check comes last, because the error message is -- extremely unhelpful. ; ifM (nb1 && nb2) (notMonoType ty1) - } + }} where (tvs1, body1) = tcSplitForAllTys ty1 (tvs2, body2) = tcSplitForAllTys ty2 @@ -1366,7 +1381,11 @@ checkTauTvUpdate orig_tv orig_ty ; case mb_tys' of Just tys' -> return (TyConApp tc tys') -- Retain the synonym (the common case) - Nothing -> go (expectJust "checkTauTvUpdate" + Nothing | isOpenTyCon tc + -> notMonoArgs (TyConApp tc tys) + -- Synonym families must have monotype args + | otherwise + -> go (expectJust "checkTauTvUpdate" (tcView (TyConApp tc tys))) -- Try again, expanding the synonym } @@ -1533,6 +1552,16 @@ addSubCtxt sub_ctxt actual_res_ty expected_res_ty thing_inside <+> ptext SLIT("arguments") ------------------ +unifyForAllCtxt tvs phi1 phi2 env + = returnM (env2, msg) + where + (env', tvs') = tidyOpenTyVars env tvs -- NB: not tidyTyVarBndrs + (env1, phi1') = tidyOpenType env' phi1 + (env2, phi2') = tidyOpenType env1 phi2 + msg = vcat [ptext SLIT("When matching") <+> quotes (ppr (mkForAllTys tvs' phi1')), + ptext SLIT(" and") <+> quotes (ppr (mkForAllTys tvs' phi2'))] + +------------------ unifyKindCtxt swapped tv1 ty2 tidy_env -- not swapped => tv1 expected, ty2 inferred -- tv1 and ty2 are zonked already = returnM msg @@ -1556,31 +1585,52 @@ unifyMisMatch outer swapped ty1 ty2 else failWithTcM (env, msg) } +----------------------- +misMatchMsg :: TcType -> TcType -> TcM (TidyEnv, SDoc) +-- Generate the message when two types fail to match, +-- going to some trouble to make it helpful misMatchMsg ty1 ty2 = do { env0 <- tcInitTidyEnv - ; (env1, pp1, extra1) <- ppr_ty env0 ty1 - ; (env2, pp2, extra2) <- ppr_ty env1 ty2 + ; (env1, pp1, extra1) <- ppr_ty env0 ty1 ty2 + ; (env2, pp2, extra2) <- ppr_ty env1 ty2 ty1 ; return (env2, sep [sep [ptext SLIT("Couldn't match expected type") <+> pp1, nest 7 (ptext SLIT("against inferred type") <+> pp2)], - nest 2 extra1, nest 2 extra2]) } - -ppr_ty :: TidyEnv -> TcType -> TcM (TidyEnv, SDoc, SDoc) -ppr_ty env ty - = do { ty' <- zonkTcType ty - ; let (env1,tidy_ty) = tidyOpenType env ty' - simple_result = (env1, quotes (ppr tidy_ty), empty) - ; case tidy_ty of - TyVarTy tv - | isSkolemTyVar tv || isSigTyVar tv - -> return (env2, pp_rigid tv', pprSkolTvBinding tv') - | otherwise -> return simple_result - where - (env2, tv') = tidySkolemTyVar env1 tv - other -> return simple_result } + nest 2 (extra1 $$ extra2)]) } + +ppr_ty :: TidyEnv -> TcType -> TcType -> TcM (TidyEnv, SDoc, SDoc) +ppr_ty env ty other_ty + = do { ty' <- zonkTcType ty + ; let (env1, tidy_ty) = tidyOpenType env ty' + ; (env2, extra) <- ppr_extra env1 ty' other_ty + ; return (env2, quotes (ppr tidy_ty), extra) } + +-- (ppr_extra env ty other_ty) shows extra info about 'ty' +ppr_extra env (TyVarTy tv) other_ty + | isSkolemTyVar tv || isSigTyVar tv + = return (env1, pprSkolTvBinding tv1) + where + (env1, tv1) = tidySkolemTyVar env tv + +ppr_extra env (TyConApp tc1 _) (TyConApp tc2 _) + | getOccName tc1 == getOccName tc2 + = -- This case helps with messages that would otherwise say + -- Could not match 'T' does not match 'M.T' + -- which is not helpful + do { this_mod <- getModule + ; return (env, quotes (ppr tc1) <+> ptext SLIT("is defined in") <+> mk_mod this_mod) } where - pp_rigid tv = quotes (ppr tv) <+> parens (ptext SLIT("a rigid variable")) + tc_mod = nameModule (getName tc1) + tc_pkg = modulePackageId tc_mod + mk_mod this_mod + | tc_mod == this_mod = ptext SLIT("this module") + | otherwise = ptext SLIT("module") <+> quotes (ppr tc_mod) <+> mk_pkg this_mod + mk_pkg this_mod + | tc_pkg == modulePackageId this_mod = empty + | otherwise = ptext SLIT("from package") <+> quotes (ppr tc_pkg) +ppr_extra env ty other_ty = return (env, empty) -- Normal case +----------------------- notMonoType ty = do { ty' <- zonkTcType ty ; env0 <- tcInitTidyEnv @@ -1588,6 +1638,13 @@ notMonoType ty msg = ptext SLIT("Cannot match a monotype with") <+> quotes (ppr tidy_ty) ; failWithTcM (env1, msg) } +notMonoArgs ty + = do { ty' <- zonkTcType ty + ; env0 <- tcInitTidyEnv + ; let (env1, tidy_ty) = tidyOpenType env0 ty' + msg = ptext SLIT("Arguments of synonym family must be monotypes") <+> quotes (ppr tidy_ty) + ; failWithTcM (env1, msg) } + occurCheck tyvar ty = do { env0 <- tcInitTidyEnv ; ty' <- zonkTcType ty @@ -1745,6 +1802,10 @@ unifyFunKind other = returnM Nothing checkExpectedKind :: Outputable a => a -> TcKind -> TcKind -> TcM () -- A fancy wrapper for 'unifyKind', which tries -- to give decent error messages. +-- (checkExpectedKind ty act_kind exp_kind) +-- checks that the actual kind act_kind is compatible +-- with the expected kind exp_kind +-- The first argument, ty, is used only in the error message generation checkExpectedKind ty act_kind exp_kind | act_kind `isSubKind` exp_kind -- Short cut for a very common case = returnM ()