X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcUnify.lhs;h=dac7803638c2c85924621e87a55af602f788aceb;hb=bcbb5b1e74623fe8d97ae711854c7925ed4ec0b4;hp=5fcaea6cf1bc25d61f67f2ea3c50d3096a72ee25;hpb=e68a891932d615590d9b1ab5752ada8142db5053;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs index 5fcaea6..dac7803 100644 --- a/compiler/typecheck/TcUnify.lhs +++ b/compiler/typecheck/TcUnify.lhs @@ -19,7 +19,7 @@ module TcUnify ( -------------------------------- -- Holes - tcInfer, subFunTys, unBox, stripBoxyType, withBox, + tcInfer, subFunTys, unBox, refineBox, refineBoxToTau, withBox, boxyUnify, boxyUnifyList, zapToMonotype, boxySplitListTy, boxySplitTyConApp, boxySplitAppTy, wrapFunResCoercion @@ -112,6 +112,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 +143,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 +194,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 +208,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 +221,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 +236,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 @@ -607,7 +611,8 @@ tc_sub :: SubCtxt -- How to add an error-context -- e.g. in the SPEC rule where we just use splitSigmaTy tc_sub sub_ctxt act_sty act_ty exp_ib exp_sty exp_ty - = tc_sub1 sub_ctxt act_sty act_ty exp_ib exp_sty exp_ty + = traceTc (text "tc_sub" <+> ppr act_ty $$ ppr exp_ty) >> + tc_sub1 sub_ctxt act_sty act_ty exp_ib exp_sty exp_ty -- This indirection is just here to make -- it easy to insert a debug trace! @@ -637,9 +642,11 @@ tc_sub1 sub_ctxt act_sty (TyVarTy tv) exp_ib exp_sty exp_ty -- Consider f g ! tc_sub1 sub_ctxt act_sty act_ty exp_ib exp_sty exp_ty - | not exp_ib, -- SKOL does not apply if exp_ty is inside a box - isSigmaTy exp_ty - = do { (gen_fn, co_fn) <- tcGen exp_ty act_tvs $ \ _ body_exp_ty -> + | isSigmaTy exp_ty + = if exp_ib then -- SKOL does not apply if exp_ty is inside a box + defer_to_boxy_matching sub_ctxt act_sty act_ty exp_ib exp_sty exp_ty + else do + { (gen_fn, co_fn) <- tcGen exp_ty act_tvs $ \ _ body_exp_ty -> tc_sub sub_ctxt act_sty act_ty False body_exp_ty body_exp_ty ; return (gen_fn <.> co_fn) } where @@ -682,7 +689,13 @@ tc_sub1 sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty ; co_fn2 <- tc_sub sub_ctxt tau' tau' exp_ib exp_sty expected_ty -- Deal with the dictionaries - ; co_fn1 <- instCall InstSigOrigin inst_tys (substTheta subst' theta) + -- The origin gives a helpful origin when we have + -- a function with type f :: Int -> forall a. Num a => ... + -- This way the (Num a) dictionary gets an OccurrenceOf f origin + ; let orig = case sub_ctxt of + SubFun n -> OccurrenceOf n + other -> InstSigOrigin -- Unhelpful + ; co_fn1 <- instCall orig inst_tys (substTheta subst' theta) ; return (co_fn2 <.> co_fn1) } ----------------------------------- @@ -707,10 +720,17 @@ tc_sub1 sub_ctxt act_sty act_ty@(FunTy act_arg act_res) _ exp_sty (TyVarTy exp_t -- Everything else: defer to boxy matching 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 + +----------------------------------- +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 @@ -841,7 +861,8 @@ unifyTheta :: TcThetaType -> TcThetaType -> TcM () -- Acutal and expected types unifyTheta theta1 theta2 = do { checkTc (equalLength theta1 theta2) - (ptext SLIT("Contexts differ in length")) + (vcat [ptext SLIT("Contexts differ in length"), + nest 2 $ parens $ ptext SLIT("Use -fglasgow-exts to allow this")]) ; uList unifyPred theta1 theta2 } --------------- @@ -935,8 +956,51 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2 go outer (TyVarTy tyvar1) ty2 = uVar outer False tyvar1 nb2 orig_ty2 ty2 go outer ty1 (TyVarTy tyvar2) = uVar outer True tyvar2 nb1 orig_ty1 ty1 -- "True" means args swapped + + -- The case for sigma-types must *follow* the variable cases + -- because a boxy variable can be filed with a polytype; + -- but must precede FunTy, because ((?x::Int) => ty) look + -- like a FunTy; there isn't necy a forall at the top + go _ ty1 ty2 + | isSigmaTy ty1 || isSigmaTy ty2 + = do { checkM (equalLength tvs1 tvs2) + (unifyMisMatch outer False orig_ty1 orig_ty2) + + ; tvs <- tcInstSkolTyVars UnkSkol tvs1 -- Not a helpful SkolemInfo + -- Get location from monad, not from tvs1 + ; let tys = mkTyVarTys tvs + in_scope = mkInScopeSet (mkVarSet tvs) + 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 + + ; 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 + -- the same polytype... but it should be a monotype. + -- 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 + -- Predicates - go outer (PredTy p1) (PredTy p2) = uPred outer nb1 p1 nb2 p2 + go outer (PredTy p1) (PredTy p2) = uPred False nb1 p1 nb2 p2 -- Type constructors must match go _ (TyConApp con1 tys1) (TyConApp con2 tys2) @@ -962,27 +1026,6 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2 | Just (s1,t1) <- tcSplitAppTy_maybe ty1 = do { uTys nb1 s1 nb2 s2; uTys nb1 t1 nb2 t2 } - go _ ty1@(ForAllTy _ _) ty2@(ForAllTy _ _) - | length tvs1 == length tvs2 - = do { tvs <- tcInstSkolTyVars UnkSkol tvs1 -- Not a helpful SkolemInfo - -- 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) - ; uTys nb1 (substTy subst1 body1) nb2 (substTy subst2 body2) - - -- 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 - -- the same polytype... but it should be a monotype. - -- 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 -- Anything else fails go outer _ _ = unifyMisMatch outer False orig_ty1 orig_ty2 @@ -993,6 +1036,10 @@ uPred outer nb1 (IParam n1 t1) nb2 (IParam n2 t2) uPred outer nb1 (ClassP c1 tys1) nb2 (ClassP c2 tys2) | c1 == c2 = uTys_s nb1 tys1 nb2 tys2 -- Guaranteed equal lengths because the kinds check uPred outer _ p1 _ p2 = unifyMisMatch outer False (mkPredTy p1) (mkPredTy p2) + +uPreds outer nb1 [] nb2 [] = return () +uPreds outer nb1 (p1:ps1) nb2 (p2:ps2) = uPred outer nb1 p1 nb2 p2 >> uPreds outer nb1 ps1 nb2 ps2 +uPreds outer nb1 ps1 nb2 ps2 = panic "uPreds" \end{code} Note [Tycon app] @@ -1333,7 +1380,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 } @@ -1373,16 +1424,27 @@ But we should not reject the program, because A t = (). Rather, we should bind t to () (= non_var_ty2). \begin{code} -stripBoxyType :: BoxyType -> TcM TcType --- Strip all boxes from the input type, returning a non-boxy type. --- It's fine for there to be a polytype inside a box (c.f. unBox) --- All of the boxes should have been filled in by now; --- hence we return a TcType -stripBoxyType ty = zonkType strip_tv ty - where - strip_tv tv = ASSERT( not (isBoxyTyVar tv) ) return (TyVarTy tv) - -- strip_tv will be called for *Flexi* meta-tyvars - -- There should not be any Boxy ones; hence the ASSERT +refineBox :: TcType -> TcM TcType +-- Unbox the outer box of a boxy type (if any) +refineBox ty@(TyVarTy box_tv) + | isMetaTyVar box_tv + = do { cts <- readMetaTyVar box_tv + ; case cts of + Flexi -> return ty + Indirect ty -> return ty } +refineBox other_ty = return other_ty + +refineBoxToTau :: TcType -> TcM TcType +-- Unbox the outer box of a boxy type, filling with a monotype if it is empty +-- Like refineBox except for the "fill with monotype" part. +refineBoxToTau ty@(TyVarTy box_tv) + | isMetaTyVar box_tv + , MetaTv BoxTv ref <- tcTyVarDetails box_tv + = do { cts <- readMutVar ref + ; case cts of + Flexi -> fillBoxWithTau box_tv ref + Indirect ty -> return ty } +refineBoxToTau other_ty = return other_ty zapToMonotype :: BoxySigmaType -> TcM TcTauType -- Subtle... we must zap the boxy res_ty @@ -1489,6 +1551,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 @@ -1544,6 +1616,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