From a2fcf3aa210edff15c5f4603ac267171f89366f0 Mon Sep 17 00:00:00 2001 From: "simonpj@microsoft.com" Date: Wed, 13 Dec 2006 16:29:15 +0000 Subject: [PATCH] Add left-to-right impredicative instantiation People keep complaining, with some justification, that runST $ foo doesn't work. So I've finally caved in. The difficulty with the above is that we need to decide how to instantiate ($)'s type arguments based on the first argument (runST), and then use that info to check the second argumnent. There is a left-to-right flow of information. It's not hard to implement this, and it's clearly useful. The main change is in TcExpr.tcArgs, with some knock-on effects elsewhere. I was finally provoked into this by Trac #981, which turned out, after some head-scratching, to be another instance of the same problem. (There was some bug-fixing too; a type like ((?x::Int) => ...) is a polytype even though it has no leading for-alls, but the new TcUnify code was not treating it right.) Test for this is tc222 --- compiler/typecheck/TcExpr.lhs | 97 +++++++++++++++++++++------------- compiler/typecheck/TcMType.lhs | 3 +- compiler/typecheck/TcUnify.lhs | 113 ++++++++++++++++++++++++++-------------- 3 files changed, 136 insertions(+), 77 deletions(-) diff --git a/compiler/typecheck/TcExpr.lhs b/compiler/typecheck/TcExpr.lhs index 18bef23..fa0e419 100644 --- a/compiler/typecheck/TcExpr.lhs +++ b/compiler/typecheck/TcExpr.lhs @@ -228,10 +228,12 @@ tcExpr in_expr@(SectionR lop@(L loc op) arg2) res_ty where doc = ptext SLIT("The section") <+> quotes (ppr in_expr) <+> ptext SLIT("takes one argument") - tc_args arg1_ty' [arg1_ty, arg2_ty] - = do { boxyUnify arg1_ty' arg1_ty - ; tcArg lop (arg2, arg2_ty, 2) } - tc_args arg1_ty' other = panic "tcExpr SectionR" + tc_args arg1_ty' qtvs qtys [arg1_ty, arg2_ty] + = do { boxyUnify arg1_ty' (substTyWith qtvs qtys arg1_ty) + ; arg2' <- tcArg lop 2 arg2 qtvs qtys arg2_ty + ; qtys' <- mapM refineBox qtys -- c.f. tcArgs + ; return (qtys', arg2') } + tc_args arg1_ty' _ _ _ = panic "tcExpr SectionR" \end{code} \begin{code} @@ -321,12 +323,15 @@ tcExpr expr@(RecordCon (L loc con_name) _ rbinds) res_ty ; checkMissingFields data_con rbinds ; let arity = dataConSourceArity data_con - check_fields arg_tys - = do { rbinds' <- tcRecordBinds data_con arg_tys rbinds - ; mapM unBox arg_tys - ; return rbinds' } - -- The unBox ensures that all the boxes in arg_tys are indeed + check_fields qtvs qtys arg_tys + = do { let arg_tys' = substTys (zipOpenTvSubst qtvs qtys) arg_tys + ; rbinds' <- tcRecordBinds data_con arg_tys' rbinds + ; qtys' <- mapM refineBoxToTau qtys + ; return (qtys', rbinds') } + -- The refineBoxToTau ensures that all the boxes in arg_tys are indeed -- filled, which is the invariant expected by tcIdApp + -- How could this not be the case? Consider a record construction + -- that does not mention all the fields. ; (con_expr, rbinds') <- tcIdApp con_name arity check_fields res_ty @@ -571,9 +576,9 @@ tcExpr other _ = pprPanic "tcMonoExpr" (ppr other) --------------------------- tcApp :: HsExpr Name -- Function -> Arity -- Number of args reqd - -> ([BoxySigmaType] -> TcM arg_results) -- Argument type-checker + -> ArgChecker results -> BoxyRhoType -- Result type - -> TcM (HsExpr TcId, arg_results) + -> TcM (HsExpr TcId, results) -- (tcFun fun n_args arg_checker res_ty) -- The argument type checker, arg_checker, will be passed exactly n_args types @@ -582,19 +587,18 @@ tcApp (HsVar fun_name) n_args arg_checker res_ty = tcIdApp fun_name n_args arg_checker res_ty tcApp fun n_args arg_checker res_ty -- The vanilla case (rula APP) - = do { arg_boxes <- newBoxyTyVars (replicate n_args argTypeKind) - ; fun' <- tcExpr fun (mkFunTys (mkTyVarTys arg_boxes) res_ty) - ; arg_tys' <- mapM readFilledBox arg_boxes - ; args' <- arg_checker arg_tys' + = do { arg_boxes <- newBoxyTyVars (replicate n_args argTypeKind) + ; fun' <- tcExpr fun (mkFunTys (mkTyVarTys arg_boxes) res_ty) + ; arg_tys' <- mapM readFilledBox arg_boxes + ; (_, args') <- arg_checker [] [] arg_tys' -- Yuk ; return (fun', args') } --------------------------- tcIdApp :: Name -- Function -> Arity -- Number of args reqd - -> ([BoxySigmaType] -> TcM arg_results) -- Argument type-checker - -- The arg-checker guarantees to fill all boxes in the arg types + -> ArgChecker results -- The arg-checker guarantees to fill all boxes in the arg types -> BoxyRhoType -- Result type - -> TcM (HsExpr TcId, arg_results) + -> TcM (HsExpr TcId, results) -- Call (f e1 ... en) :: res_ty -- Type f :: forall a b c. theta => fa_1 -> ... -> fa_k -> fres @@ -627,23 +631,16 @@ tcIdApp fun_name n_args arg_checker res_ty ; let extra_arg_tys' = mkTyVarTys extra_arg_boxes res_ty' = mkFunTys extra_arg_tys' res_ty ; qtys' <- preSubType qtvs tau_qtvs fun_res_ty res_ty' - ; let arg_subst = zipOpenTvSubst qtvs qtys' - fun_arg_tys' = substTys arg_subst fun_arg_tys -- Typecheck the arguments! -- Doing so will fill arg_qtvs and extra_arg_tys' - ; args' <- arg_checker (fun_arg_tys' ++ extra_arg_tys') + ; (qtys'', args') <- arg_checker qtvs qtys' (fun_arg_tys ++ extra_arg_tys') -- Strip boxes from the qtvs that have been filled in by the arg checking - -- AND any variables that are mentioned in neither arg nor result - -- the latter are mentioned only in constraints; stripBoxyType will - -- fill them with a monotype - ; let strip qtv qty' | qtv `elemVarSet` arg_qtvs = stripBoxyType qty' - | otherwise = return qty' - ; qtys'' <- zipWithM strip qtvs qtys' ; extra_arg_tys'' <- mapM readFilledBox extra_arg_boxes -- Result subsumption + -- This fills in res_qtvs ; let res_subst = zipOpenTvSubst qtvs qtys'' fun_res_ty'' = substTy res_subst fun_res_ty res_ty'' = mkFunTys extra_arg_tys'' res_ty @@ -653,7 +650,7 @@ tcIdApp fun_name n_args arg_checker res_ty -- By applying the coercion just to the *function* we can make -- tcFun work nicely for OpApp and Sections too ; fun' <- instFun orig fun res_subst tv_theta_prs - ; co_fn' <- wrapFunResCoercion fun_arg_tys' co_fn + ; co_fn' <- wrapFunResCoercion (substTys res_subst fun_arg_tys) co_fn ; return (mkHsWrap co_fn' fun', args') } \end{code} @@ -818,19 +815,45 @@ This gets a bit less sharing, but a) it's better for RULEs involving overloaded functions b) perhaps fewer separated lambdas +Note [Left to right] +~~~~~~~~~~~~~~~~~~~~ +tcArgs implements a left-to-right order, which goes beyond what is described in the +impredicative type inference paper. In particular, it allows + runST $ foo +where runST :: (forall s. ST s a) -> a +When typechecking the application of ($)::(a->b) -> a -> b, we first check that +runST has type (a->b), thereby filling in a=forall s. ST s a. Then we un-box this type +before checking foo. The left-to-right order really helps here. + \begin{code} tcArgs :: LHsExpr Name -- The function (for error messages) - -> [LHsExpr Name] -> [TcSigmaType] -- Actual arguments and expected arg types - -> TcM [LHsExpr TcId] -- Resulting args + -> [LHsExpr Name] -- Actual args + -> ArgChecker [LHsExpr TcId] -tcArgs fun args expected_arg_tys - = mapM (tcArg fun) (zip3 args expected_arg_tys [1..]) +type ArgChecker results + = [TyVar] -> [TcSigmaType] -- Current instantiation + -> [TcSigmaType] -- Expected arg types (**before** applying the instantiation) + -> TcM ([TcSigmaType], results) -- Resulting instaniation and args -tcArg :: LHsExpr Name -- The function (for error messages) - -> (LHsExpr Name, BoxySigmaType, Int) -- Actual argument and expected arg type - -> TcM (LHsExpr TcId) -- Resulting argument -tcArg fun (arg, ty, arg_no) = addErrCtxt (funAppCtxt fun arg arg_no) $ - tcPolyExprNC arg ty +tcArgs fun args qtvs qtys arg_tys + = go 1 qtys args arg_tys + where + go n qtys [] [] = return (qtys, []) + go n qtys (arg:args) (arg_ty:arg_tys) + = do { arg' <- tcArg fun n arg qtvs qtys arg_ty + ; qtys' <- mapM refineBox qtys -- Exploit new info + ; (qtys'', args') <- go (n+1) qtys' args arg_tys + ; return (qtys'', arg':args') } + +tcArg :: LHsExpr Name -- The function + -> Int -- and arg number (for error messages) + -> LHsExpr Name + -> [TyVar] -> [TcSigmaType] -- Instantiate the arg type like this + -> BoxySigmaType + -> TcM (LHsExpr TcId) -- Resulting argument +tcArg fun arg_no arg qtvs qtys ty + = addErrCtxt (funAppCtxt fun arg arg_no) $ + tcPolyExprNC arg (substTyWith qtvs qtys ty) \end{code} diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs index 0845853..b4e89b0 100644 --- a/compiler/typecheck/TcMType.lhs +++ b/compiler/typecheck/TcMType.lhs @@ -62,7 +62,6 @@ module TcMType ( import TypeRep import TcType import Type -import Type import Coercion import Class import TyCon @@ -360,7 +359,7 @@ data LookupTyVarResult -- The result of a lookupTcTyVar call lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult lookupTcTyVar tyvar - = ASSERT( isTcTyVar tyvar ) + = ASSERT2( isTcTyVar tyvar, ppr tyvar ) case details of SkolemTv _ -> return (DoneTv details) MetaTv _ ref -> do { meta_details <- readMutVar ref diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs index 1868ad0..de9c341 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 @@ -607,7 +607,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 +638,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 @@ -713,11 +716,14 @@ 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 ; return idHsWrapper } - ----------------------------------- tc_sub_funs act_arg act_res exp_ib exp_arg exp_res = do { uTys False act_arg exp_ib exp_arg @@ -942,8 +948,45 @@ 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) + 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) + + ; checkM (equalLength theta1 theta2) + (unifyMisMatch outer False orig_ty1 orig_ty2) + + ; uPreds False nb1 theta1 nb2 theta2 + ; uTys nb1 tau1 nb2 tau2 + + -- 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) @@ -969,27 +1012,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 @@ -1000,6 +1022,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] @@ -1380,16 +1406,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 -- 1.7.10.4