X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcUnify.lhs;h=86928b7099341d7e2d3978db4a9a25edf9bebc6a;hb=f59d6c9d6ead47a61681b1086b313c2fad225912;hp=233e87d49ac6bf3e986e2384f7ec6f05698fd796;hpb=1b6b0ba3b93351045e19df9fa9cb0f8baf033afc;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs index 233e87d..86928b7 100644 --- a/compiler/typecheck/TcUnify.lhs +++ b/compiler/typecheck/TcUnify.lhs @@ -15,7 +15,7 @@ Type subsumption and unification module TcUnify ( -- Full-blown subsumption - tcSubExp, tcFunResTy, tcGen, + tcSubExp, tcGen, checkSigTyVars, checkSigTyVarsWrt, bleatEscapedTvs, sigCtxt, -- Various unifications @@ -28,7 +28,7 @@ module TcUnify ( -- Holes tcInfer, subFunTys, unBox, refineBox, refineBoxToTau, withBox, boxyUnify, boxyUnifyList, zapToMonotype, - boxySplitListTy, boxySplitTyConApp, boxySplitAppTy, + boxySplitListTy, boxySplitPArrTy, boxySplitTyConApp, boxySplitAppTy, wrapFunResCoercion ) where @@ -60,6 +60,8 @@ import BasicTypes import Util import Outputable import Unique + +import Control.Monad \end{code} %************************************************************************ @@ -70,11 +72,7 @@ import Unique \begin{code} tcInfer :: (BoxyType -> TcM a) -> TcM (a, TcType) -tcInfer tc_infer - = do { box <- newBoxyTyVar openTypeKind - ; res <- tc_infer (mkTyVarTy box) - ; res_ty <- {- pprTrace "tcInfer" (ppr (mkTyVarTy box)) $ -} readFilledBox box -- Guaranteed filled-in by now - ; return (res, res_ty) } +tcInfer tc_infer = withBox openTypeKind tc_infer \end{code} @@ -128,7 +126,8 @@ subFunTys error_herald n_pats res_ty thing_inside loop n args_so_far res_ty | isSigmaTy res_ty -- Do this before checking n==0, because we - -- guarantee to return a BoxyRhoType, not a BoxySigmaType + -- guarantee to return a BoxyRhoType, not a + -- BoxySigmaType = do { (gen_fn, (co_fn, res)) <- tcGen res_ty emptyVarSet $ \ _ res_ty' -> loop n args_so_far res_ty' ; return (gen_fn <.> co_fn, res) } @@ -142,29 +141,47 @@ subFunTys error_herald n_pats res_ty thing_inside ; co_fn' <- wrapFunResCoercion [arg_ty] co_fn ; return (co_fn', res) } + -- Try to normalise synonym families and defer if that's not possible + loop n args_so_far ty@(TyConApp tc tys) + | isOpenSynTyCon tc + = do { (coi1, ty') <- tcNormaliseFamInst ty + ; case coi1 of + IdCo -> defer n args_so_far ty + -- no progress, but maybe solvable => defer + ACo _ -> -- progress: so lets try again + do { (co_fn, res) <- loop n args_so_far ty' + ; return $ (co_fn <.> coiToHsWrapper (mkSymCoI coi1), res) + } + } + -- res_ty might have a type variable at the head, such as (a b c), -- in which case we must fill in with (->). Simplest thing to do -- is to use boxyUnify, but we catch failure and generate our own -- error message on failure loop n args_so_far res_ty@(AppTy _ _) = do { [arg_ty',res_ty'] <- newBoxyTyVarTys [argTypeKind, openTypeKind] - ; (_, mb_coi) <- tryTcErrs $ boxyUnify res_ty (FunTy arg_ty' res_ty') + ; (_, mb_coi) <- tryTcErrs $ + boxyUnify res_ty (FunTy arg_ty' res_ty') ; if isNothing mb_coi then bale_out args_so_far - else do { case expectJust "subFunTys" mb_coi of - IdCo -> return () - ACo co -> traceTc (text "you're dropping a coercion: " <+> ppr co) - ; loop n args_so_far (FunTy arg_ty' res_ty') + else do { let coi = expectJust "subFunTys" mb_coi + ; (co_fn, res) <- loop n args_so_far (FunTy arg_ty' + res_ty') + ; return (co_fn <.> coiToHsWrapper coi, res) } } - loop n args_so_far (TyVarTy tv) + loop n args_so_far ty@(TyVarTy tv) | isTyConableTyVar tv = do { cts <- readMetaTyVar tv ; case cts of Indirect ty -> loop n args_so_far ty - Flexi -> do { (res_ty:arg_tys) <- withMetaTvs tv kinds mk_res_ty - ; res <- thing_inside (reverse args_so_far ++ arg_tys) res_ty - ; return (idHsWrapper, res) } } + Flexi -> + do { (res_ty:arg_tys) <- withMetaTvs tv kinds mk_res_ty + ; res <- thing_inside (reverse args_so_far ++ arg_tys) + res_ty + ; return (idHsWrapper, res) } } + | otherwise -- defer as tyvar may be refined by equalities + = defer n args_so_far ty where mk_res_ty (res_ty' : arg_tys') = mkFunTys arg_tys' res_ty' mk_res_ty [] = panic "TcUnify.mk_res_ty1" @@ -174,6 +191,21 @@ subFunTys error_herald n_pats res_ty thing_inside loop n args_so_far res_ty = bale_out args_so_far + -- build a template type a1 -> ... -> an -> b and defer an equality + -- between that template and the expected result type res_ty; then, + -- use the template to type the thing_inside + defer n args_so_far ty + = do { arg_tys <- newFlexiTyVarTys n argTypeKind + ; res_ty' <- newFlexiTyVarTy openTypeKind + ; let fun_ty = mkFunTys arg_tys res_ty' + err = error_herald <> comma $$ + text "which does not match its type" + ; coi <- addErrCtxt err $ + defer_unification False False fun_ty ty + ; res <- thing_inside (reverse args_so_far ++ arg_tys) res_ty' + ; return (coiToHsWrapper coi, res) + } + bale_out args_so_far = do { env0 <- tcInitTidyEnv ; res_ty' <- zonkTcType res_ty @@ -191,8 +223,9 @@ subFunTys error_herald n_pats res_ty thing_inside ---------------------- boxySplitTyConApp :: TyCon -- T :: k1 -> ... -> kn -> * -> BoxyRhoType -- Expected type (T a b c) - -> TcM [BoxySigmaType] -- Element types, a b c - -- It's used for wired-in tycons, so we call checkWiredInTyCOn + -> TcM ([BoxySigmaType], -- Element types, a b c + CoercionI) -- T a b c ~ orig_ty + -- It's used for wired-in tycons, so we call checkWiredInTyCon -- Precondition: never called with FunTyCon -- Precondition: input type :: * @@ -203,14 +236,28 @@ boxySplitTyConApp tc orig_ty loop n_req args_so_far ty | Just ty' <- tcView ty = loop n_req args_so_far ty' - loop n_req args_so_far (TyConApp tycon args) + loop n_req args_so_far ty@(TyConApp tycon args) | tc == tycon = ASSERT( n_req == length args) -- ty::* - return (args ++ args_so_far) + return (args ++ args_so_far, IdCo) + + | isOpenSynTyCon tycon -- try to normalise type family application + = do { (coi1, ty') <- tcNormaliseFamInst ty + ; traceTc $ text "boxySplitTyConApp:" <+> + ppr ty <+> text "==>" <+> ppr ty' + ; case coi1 of + IdCo -> defer -- no progress, but maybe solvable => defer + ACo _ -> -- progress: so lets try again + do { (args, coi2) <- loop n_req args_so_far ty' + ; return $ (args, coi2 `mkTransCoI` mkSymCoI coi1) + } + } loop n_req args_so_far (AppTy fun arg) | n_req > 0 - = loop (n_req - 1) (arg:args_so_far) fun + = do { (args, coi) <- loop (n_req - 1) (arg:args_so_far) fun + ; return (args, mkAppTyCoI fun coi arg IdCo) + } loop n_req args_so_far (TyVarTy tv) | isTyConableTyVar tv @@ -219,23 +266,42 @@ boxySplitTyConApp tc orig_ty ; case cts of Indirect ty -> loop n_req args_so_far ty Flexi -> do { arg_tys <- withMetaTvs tv arg_kinds mk_res_ty - ; return (arg_tys ++ args_so_far) } - } + ; return (arg_tys ++ args_so_far, IdCo) } + } + | otherwise -- defer as tyvar may be refined by equalities + = defer where - mk_res_ty arg_tys' = mkTyConApp tc arg_tys' (arg_kinds, res_kind) = splitKindFunTysN n_req (tyConKind tc) - loop _ _ _ = boxySplitFailure (mkTyConApp tc (mkTyVarTys (tyConTyVars tc))) orig_ty + loop _ _ _ = boxySplitFailure (mkTyConApp tc (mkTyVarTys (tyConTyVars tc))) + orig_ty + + -- defer splitting by generating an equality constraint + defer = boxySplitDefer arg_kinds mk_res_ty orig_ty + where + (arg_kinds, _) = splitKindFunTys (tyConKind tc) + + -- apply splitted tycon to arguments + mk_res_ty = mkTyConApp tc ---------------------- -boxySplitListTy :: BoxyRhoType -> TcM BoxySigmaType -- Special case for lists -boxySplitListTy exp_ty = do { [elt_ty] <- boxySplitTyConApp listTyCon exp_ty - ; return elt_ty } +boxySplitListTy :: BoxyRhoType -> TcM (BoxySigmaType, CoercionI) +-- Special case for lists +boxySplitListTy exp_ty + = do { ([elt_ty], coi) <- boxySplitTyConApp listTyCon exp_ty + ; return (elt_ty, coi) } +---------------------- +boxySplitPArrTy :: BoxyRhoType -> TcM (BoxySigmaType, CoercionI) +-- Special case for parrs +boxySplitPArrTy exp_ty + = do { ([elt_ty], coi) <- boxySplitTyConApp parrTyCon exp_ty + ; return (elt_ty, coi) } ---------------------- boxySplitAppTy :: BoxyRhoType -- Type to split: m a - -> TcM (BoxySigmaType, BoxySigmaType) -- Returns m, a + -> TcM ((BoxySigmaType, BoxySigmaType), -- Returns m, a + CoercionI) -- 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 @@ -248,18 +314,29 @@ boxySplitAppTy orig_ty loop ty | Just (fun_ty, arg_ty) <- tcSplitAppTy_maybe ty - = return (fun_ty, arg_ty) + = return ((fun_ty, arg_ty), IdCo) + + loop ty@(TyConApp tycon _args) + | isOpenSynTyCon tycon -- try to normalise type family application + = do { (coi1, ty') <- tcNormaliseFamInst ty + ; case coi1 of + IdCo -> defer -- no progress, but maybe solvable => defer + ACo co -> -- progress: so lets try again + do { (args, coi2) <- loop ty' + ; return $ (args, coi2 `mkTransCoI` mkSymCoI coi1) + } + } loop (TyVarTy tv) | isTyConableTyVar tv = do { cts <- readMetaTyVar tv ; case cts of Indirect ty -> loop ty - Flexi -> do { [fun_ty,arg_ty] <- withMetaTvs tv kinds mk_res_ty - ; return (fun_ty, arg_ty) } } + Flexi -> do { [fun_ty, arg_ty] <- withMetaTvs tv kinds mk_res_ty + ; return ((fun_ty, arg_ty), IdCo) } } + | otherwise -- defer as tyvar may be refined by equalities + = defer where - mk_res_ty [fun_ty', arg_ty'] = mkAppTy fun_ty' arg_ty' - mk_res_ty other = panic "TcUnify.mk_res_ty2" tv_kind = tyVarKind tv kinds = [mkArrowKind liftedTypeKind (defaultKind tv_kind), -- m :: * -> k @@ -271,11 +348,36 @@ boxySplitAppTy orig_ty loop _ = boxySplitFailure (mkAppTy alphaTy betaTy) orig_ty + -- defer splitting by generating an equality constraint + defer = do { ([ty1, ty2], coi) <- boxySplitDefer arg_kinds mk_res_ty orig_ty + ; return ((ty1, ty2), coi) + } + where + orig_kind = typeKind orig_ty + arg_kinds = [mkArrowKind liftedTypeKind (defaultKind orig_kind), + -- m :: * -> k + liftedTypeKind] -- arg type :: * + + -- build type application + mk_res_ty [fun_ty', arg_ty'] = mkAppTy fun_ty' arg_ty' + mk_res_ty _other = panic "TcUnify.mk_res_ty2" + ------------------ boxySplitFailure actual_ty expected_ty = unifyMisMatch False False actual_ty expected_ty -- "outer" is False, so we don't pop the context -- which is what we want since we have not pushed one! + +------------------ +boxySplitDefer :: [Kind] -- kinds of required arguments + -> ([TcType] -> TcTauType) -- construct lhs from argument tyvars + -> BoxyRhoType -- type to split + -> TcM ([TcType], CoercionI) +boxySplitDefer kinds mkTy orig_ty + = do { tau_tys <- mapM newFlexiTyVarTy kinds + ; coi <- defer_unification False False (mkTy tau_tys) orig_ty + ; return (tau_tys, coi) + } \end{code} @@ -313,7 +415,7 @@ withMetaTvs tv kinds mk_res_ty withBox :: Kind -> (BoxySigmaType -> TcM a) -> TcM (a, TcType) -- Allocate a *boxy* tyvar withBox kind thing_inside - = do { box_tv <- newMetaTyVar BoxTv kind + = do { box_tv <- newBoxyTyVar kind ; res <- thing_inside (mkTyVarTy box_tv) ; ty <- {- pprTrace "with_box" (ppr (mkTyVarTy box_tv)) $ -} readFilledBox box_tv ; return (res, ty) } @@ -571,24 +673,24 @@ Later stuff will fail. All the tcSub calls have the form - tcSub expected_ty offered_ty + tcSub actual_ty expected_ty which checks - offered_ty <= expected_ty + actual_ty <= expected_ty -That is, that a value of type offered_ty is acceptable in +That is, that a value of type actual_ty is acceptable in a place expecting a value of type expected_ty. It returns a coercion function - co_fn :: offered_ty ~ expected_ty -which takes an HsExpr of type offered_ty into one of type + co_fn :: actual_ty ~ expected_ty +which takes an HsExpr of type actual_ty into one of type expected_ty. \begin{code} ----------------- -tcSubExp :: BoxySigmaType -> BoxySigmaType -> TcM HsWrapper -- Locally used only +tcSubExp :: InstOrigin -> BoxySigmaType -> BoxySigmaType -> TcM HsWrapper -- (tcSub act exp) checks that -- act <= exp -tcSubExp actual_ty expected_ty +tcSubExp orig actual_ty expected_ty = -- addErrCtxtM (unifyCtxt actual_ty expected_ty) $ -- Adding the error context here leads to some very confusing error -- messages, such as "can't match forall a. a->a with forall a. a->a" @@ -601,19 +703,10 @@ tcSubExp actual_ty expected_ty -- So instead I'm adding the error context when moving from tc_sub to u_tys traceTc (text "tcSubExp" <+> ppr actual_ty <+> ppr expected_ty) >> - tc_sub SubOther actual_ty actual_ty False expected_ty expected_ty + tc_sub orig actual_ty actual_ty False expected_ty expected_ty -tcFunResTy :: Name -> BoxySigmaType -> BoxySigmaType -> TcM HsWrapper -- Locally used only -tcFunResTy fun actual_ty expected_ty - = traceTc (text "tcFunResTy" <+> ppr actual_ty <+> ppr expected_ty) >> - tc_sub (SubFun fun) actual_ty actual_ty False expected_ty expected_ty - ----------------- -data SubCtxt = SubDone -- Error-context already pushed - | SubFun Name -- Context is tcFunResTy - | SubOther -- Context is something else - -tc_sub :: SubCtxt -- How to add an error-context +tc_sub :: InstOrigin -> BoxySigmaType -- actual_ty, before expanding synonyms -> BoxySigmaType -- ..and after -> InBox -- True <=> expected_ty is inside a box @@ -627,31 +720,29 @@ tc_sub :: SubCtxt -- How to add an error-context -- This invariant is needed so that we can "see" the foralls, ad -- 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_sub orig 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 + tc_sub1 orig act_sty act_ty exp_ib exp_sty exp_ty -- This indirection is just here to make -- it easy to insert a debug trace! -tc_sub1 sub_ctxt act_sty act_ty exp_ib exp_sty exp_ty - | Just exp_ty' <- tcView exp_ty = 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 - | Just act_ty' <- tcView act_ty = tc_sub sub_ctxt act_sty act_ty' exp_ib exp_sty exp_ty +tc_sub1 orig act_sty act_ty exp_ib exp_sty exp_ty + | Just exp_ty' <- tcView exp_ty = tc_sub orig act_sty act_ty exp_ib exp_sty exp_ty' +tc_sub1 orig act_sty act_ty exp_ib exp_sty exp_ty + | Just act_ty' <- tcView act_ty = tc_sub orig act_sty act_ty' exp_ib exp_sty exp_ty ----------------------------------- -- Rule SBOXY, plus other cases when act_ty is a type variable -- Just defer to boxy matching -- This rule takes precedence over SKOL! -tc_sub1 sub_ctxt act_sty (TyVarTy tv) exp_ib exp_sty exp_ty +tc_sub1 orig act_sty (TyVarTy tv) exp_ib exp_sty exp_ty = do { traceTc (text "tc_sub1 - case 1") - ; coi <- addSubCtxt sub_ctxt act_sty exp_sty $ + ; coi <- addSubCtxt orig act_sty exp_sty $ uVar True False tv exp_ib exp_sty exp_ty ; traceTc (case coi of IdCo -> text "tc_sub1 (Rule SBOXY) IdCo" ACo co -> text "tc_sub1 (Rule SBOXY) ACo" <+> ppr co) - ; return $ case coi of - IdCo -> idHsWrapper - ACo co -> WpCo co + ; return $ coiToHsWrapper coi } ----------------------------------- @@ -665,14 +756,14 @@ tc_sub1 sub_ctxt act_sty (TyVarTy tv) exp_ib exp_sty exp_ty -- g :: Ord b => b->b -- Consider f g ! -tc_sub1 sub_ctxt act_sty act_ty exp_ib exp_sty exp_ty - | isSigmaTy exp_ty - = do { traceTc (text "tc_sub1 - case 2") ; +tc_sub1 orig act_sty act_ty exp_ib exp_sty exp_ty + | isSigmaTy exp_ty = do + { traceTc (text "tc_sub1 - case 2") ; 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 + defer_to_boxy_matching orig 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 + tc_sub orig act_sty act_ty False body_exp_ty body_exp_ty ; return (gen_fn <.> co_fn) } } where @@ -686,7 +777,7 @@ tc_sub1 sub_ctxt act_sty act_ty exp_ib exp_sty exp_ty -- expected_ty: Int -> Int -- co_fn e = e Int dOrdInt -tc_sub1 sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty +tc_sub1 orig act_sty actual_ty exp_ib exp_sty expected_ty -- Implements the new SPEC rule in the Appendix of the paper -- "Boxy types: inference for higher rank types and impredicativity" -- (This appendix isn't in the published version.) @@ -713,75 +804,60 @@ tc_sub1 sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty ; traceTc (text "tc_sub_spec" <+> vcat [ppr actual_ty, ppr tyvars <+> ppr theta <+> ppr tau, ppr tau']) - ; co_fn2 <- tc_sub sub_ctxt tau' tau' exp_ib exp_sty expected_ty + ; co_fn2 <- tc_sub orig tau' tau' exp_ib exp_sty expected_ty -- Deal with the dictionaries - -- 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) } ----------------------------------- -- Function case (rule F1) -tc_sub1 sub_ctxt act_sty (FunTy act_arg act_res) exp_ib exp_sty (FunTy exp_arg exp_res) +tc_sub1 orig act_sty (FunTy act_arg act_res) exp_ib exp_sty (FunTy exp_arg exp_res) = do { traceTc (text "tc_sub1 - case 4") - ; addSubCtxt sub_ctxt act_sty exp_sty $ - tc_sub_funs act_arg act_res exp_ib exp_arg exp_res + ; tc_sub_funs orig act_arg act_res exp_ib exp_arg exp_res } -- Function case (rule F2) -tc_sub1 sub_ctxt act_sty act_ty@(FunTy act_arg act_res) _ exp_sty (TyVarTy exp_tv) +tc_sub1 orig act_sty act_ty@(FunTy act_arg act_res) _ exp_sty (TyVarTy exp_tv) | isBoxyTyVar exp_tv - = addSubCtxt sub_ctxt act_sty exp_sty $ - do { traceTc (text "tc_sub1 - case 5") + = do { traceTc (text "tc_sub1 - case 5") ; cts <- readMetaTyVar exp_tv ; case cts of - Indirect ty -> tc_sub SubDone act_sty act_ty True exp_sty ty + Indirect ty -> tc_sub orig act_sty act_ty True exp_sty ty Flexi -> do { [arg_ty,res_ty] <- withMetaTvs exp_tv fun_kinds mk_res_ty - ; tc_sub_funs act_arg act_res True arg_ty res_ty } } + ; tc_sub_funs orig act_arg act_res True arg_ty res_ty } } where mk_res_ty [arg_ty', res_ty'] = mkFunTy arg_ty' res_ty' mk_res_ty other = panic "TcUnify.mk_res_ty3" fun_kinds = [argTypeKind, openTypeKind] -- Everything else: defer to boxy matching -tc_sub1 sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty@(TyVarTy exp_tv) +tc_sub1 orig act_sty actual_ty exp_ib exp_sty expected_ty@(TyVarTy exp_tv) = do { traceTc (text "tc_sub1 - case 6a" <+> ppr [isBoxyTyVar exp_tv, isMetaTyVar exp_tv, isSkolemTyVar exp_tv, isExistentialTyVar exp_tv,isSigTyVar exp_tv] ) - ; defer_to_boxy_matching sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty + ; defer_to_boxy_matching orig act_sty actual_ty exp_ib exp_sty expected_ty } -tc_sub1 sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty +tc_sub1 orig act_sty actual_ty exp_ib exp_sty expected_ty = do { traceTc (text "tc_sub1 - case 6") - ; defer_to_boxy_matching sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty + ; defer_to_boxy_matching orig 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 { coi <- addSubCtxt sub_ctxt act_sty exp_sty $ - u_tys outer False act_sty actual_ty exp_ib exp_sty expected_ty - ; return $ case coi of - IdCo -> idHsWrapper - ACo co -> WpCo co - } - where - outer = case sub_ctxt of -- Ugh - SubDone -> False - other -> True +defer_to_boxy_matching orig act_sty actual_ty exp_ib exp_sty expected_ty + = do { coi <- addSubCtxt orig act_sty exp_sty $ + u_tys True False act_sty actual_ty exp_ib exp_sty expected_ty + ; return $ coiToHsWrapper coi } ----------------------------------- -tc_sub_funs act_arg act_res exp_ib exp_arg exp_res - = do { arg_coi <- uTys False act_arg exp_ib exp_arg - ; co_fn_res <- tc_sub SubDone act_res act_res exp_ib exp_res exp_res +tc_sub_funs orig act_arg act_res exp_ib exp_arg exp_res + = do { arg_coi <- addSubCtxt orig act_arg exp_arg $ + uTysOuter False act_arg exp_ib exp_arg + ; co_fn_res <- tc_sub orig act_res act_res exp_ib exp_res exp_res ; wrapper1 <- wrapFunResCoercion [exp_arg] co_fn_res ; let wrapper2 = case arg_coi of IdCo -> idHsWrapper ACo co -> WpCo $ FunTy co act_res - ; return (wrapper1 <.> wrapper2) - } + ; return (wrapper1 <.> wrapper2) } ----------------------------------- wrapFunResCoercion @@ -793,7 +869,7 @@ wrapFunResCoercion arg_tys co_fn_res = return idHsWrapper | null arg_tys = return co_fn_res - | otherwise + | otherwise = do { arg_ids <- newSysLocalIds FSLIT("sub") arg_tys ; return (mkWpLams arg_ids <.> co_fn_res <.> mkWpApps arg_ids) } \end{code} @@ -850,7 +926,7 @@ tcGen expected_ty extra_tvs thing_inside -- We expect expected_ty to be a forall -- list of "free vars" for the signature check. ; loc <- getInstLoc (SigOrigin skol_info) - ; dicts <- newDictBndrs loc theta' + ; dicts <- newDictBndrs loc theta' -- Includes equalities ; inst_binds <- tcSimplifyCheck loc tvs' dicts lie ; checkSigTyVarsWrt free_tvs tvs' @@ -860,7 +936,7 @@ tcGen expected_ty extra_tvs thing_inside -- We expect expected_ty to be a forall -- The WpLet binds any Insts which came out of the simplification. dict_vars = map instToVar dicts co_fn = mkWpTyLams tvs' <.> mkWpLams dict_vars <.> WpLet inst_binds - ; returnM (co_fn, result) } + ; return (co_fn, result) } where free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs \end{code} @@ -934,8 +1010,8 @@ lists, when all the elts should be of the same type. \begin{code} unifyTypeList :: [TcTauType] -> TcM () -unifyTypeList [] = returnM () -unifyTypeList [ty] = returnM () +unifyTypeList [] = return () +unifyTypeList [ty] = return () unifyTypeList (ty1:tys@(ty2:_)) = do { unifyType ty1 ty2 ; unifyTypeList tys } \end{code} @@ -989,7 +1065,7 @@ uTys nb1 ty1 nb2 ty2 uTys_s :: InBox -> [TcType] -- tys1 are the *actual* types -> InBox -> [TcType] -- tys2 are the *expected* types -> TcM [CoercionI] -uTys_s nb1 [] nb2 [] = returnM [] +uTys_s nb1 [] nb2 [] = return [] uTys_s nb1 (ty1:tys1) nb2 (ty2:tys2) = do { coi <- uTys nb1 ty1 nb2 ty2 ; cois <- uTys_s nb1 tys1 nb2 tys2 ; return (coi:cois) @@ -1038,7 +1114,7 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2 go1 _ ty1 ty2 | isSigmaTy ty1 || isSigmaTy ty2 = do { traceTc (text "We have sigma types: equalLength" <+> ppr tvs1 <+> ppr tvs2) - ; checkM (equalLength tvs1 tvs2) + ; unless (equalLength tvs1 tvs2) (unifyMisMatch outer False orig_ty1 orig_ty2) ; traceTc (text "We're past the first length test") ; tvs <- tcInstSkolTyVars UnkSkol tvs1 -- Not a helpful SkolemInfo @@ -1051,7 +1127,7 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2 (theta2,tau2) = tcSplitPhiTy phi2 ; addErrCtxtM (unifyForAllCtxt tvs phi1 phi2) $ do - { checkM (equalLength theta1 theta2) + { unless (equalLength theta1 theta2) (unifyMisMatch outer False orig_ty1 orig_ty2) ; cois <- uPreds False nb1 theta1 nb2 theta2 -- TOMDO: do something with these pred_cois @@ -1060,7 +1136,7 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2 -- 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) + ; when (any (`elemVarSet` free_tvs) tvs) (bleatEscapedTvs free_tvs tvs tvs) -- If both sides are inside a box, we are in a "box-meets-box" @@ -1069,7 +1145,7 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2 -- 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) + ; when (nb1 && nb2) (notMonoType ty1) ; return coi }} where @@ -1306,7 +1382,7 @@ uUnfilledVar outer swapped tv1 details1 ps_ty2 (TyVarTy tv2) ; updateMeta tv1 ref1 (mkTyVarTy tau_tv) ; return IdCo } - other -> returnM IdCo -- No-op + other -> return IdCo -- No-op | otherwise -- Distinct type variables = do { lookup2 <- lookupTcTyVar tv2 @@ -1614,9 +1690,7 @@ mkExpectedActualMsg act_ty exp_ty ---------------- -- If an error happens we try to figure out whether the function -- function has been given too many or too few arguments, and say so. -addSubCtxt SubDone actual_res_ty expected_res_ty thing_inside - = thing_inside -addSubCtxt sub_ctxt actual_res_ty expected_res_ty thing_inside +addSubCtxt orig actual_res_ty expected_res_ty thing_inside = addErrCtxtM mk_err thing_inside where mk_err tidy_env @@ -1630,10 +1704,11 @@ addSubCtxt sub_ctxt actual_res_ty expected_res_ty thing_inside len_act_args = length act_args len_exp_args = length exp_args - message = case sub_ctxt of - SubFun fun | len_exp_args < len_act_args -> wrongArgsCtxt "too few" fun - | len_exp_args > len_act_args -> wrongArgsCtxt "too many" fun - other -> mkExpectedActualMsg act_ty'' exp_ty'' + message = case orig of + OccurrenceOf fun + | len_exp_args < len_act_args -> wrongArgsCtxt "too few" fun + | len_exp_args > len_act_args -> wrongArgsCtxt "too many" fun + other -> mkExpectedActualMsg act_ty'' exp_ty'' ; return (env2, message) } wrongArgsCtxt too_many_or_few fun @@ -1643,7 +1718,7 @@ addSubCtxt sub_ctxt actual_res_ty expected_res_ty thing_inside ------------------ unifyForAllCtxt tvs phi1 phi2 env - = returnM (env2, msg) + = return (env2, msg) where (env', tvs') = tidyOpenTyVars env tvs -- NB: not tidyTyVarBndrs (env1, phi1') = tidyOpenType env' phi1 @@ -1653,13 +1728,9 @@ unifyForAllCtxt tvs phi1 phi2 env ----------------------- unifyMisMatch outer swapped ty1 ty2 - = do { (env, msg) <- if swapped then misMatchMsg ty2 ty1 - else misMatchMsg ty1 ty2 - - -- This is the whole point of the 'outer' stuff - ; if outer then popErrCtxt (failWithTcM (env, msg)) - else failWithTcM (env, msg) - } + | swapped = unifyMisMatch outer False ty2 ty1 + | outer = popErrCtxt $ unifyMisMatch False swapped ty1 ty2 -- This is the whole point of the 'outer' stuff + | otherwise = failWithMisMatch ty1 ty2 \end{code} @@ -1676,7 +1747,7 @@ unifyKind :: TcKind -- Expected -> TcKind -- Actual -> TcM () unifyKind (TyConApp kc1 []) (TyConApp kc2 []) - | isSubKindCon kc2 kc1 = returnM () + | isSubKindCon kc2 kc1 = return () unifyKind (FunTy a1 r1) (FunTy a2 r2) = do { unifyKind a2 a1; unifyKind r1 r2 } @@ -1687,10 +1758,10 @@ unifyKind k1 (TyVarTy kv2) = uKVar True kv2 k1 unifyKind k1 k2 = unifyKindMisMatch k1 k2 unifyKinds :: [TcKind] -> [TcKind] -> TcM () -unifyKinds [] [] = returnM () -unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2 `thenM_` - unifyKinds ks1 ks2 -unifyKinds _ _ = panic "unifyKinds: length mis-match" +unifyKinds [] [] = return () +unifyKinds (k1:ks1) (k2:ks2) = do unifyKind k1 k2 + unifyKinds ks1 ks2 +unifyKinds _ _ = panic "unifyKinds: length mis-match" ---------------- uKVar :: Bool -> KindVar -> TcKind -> TcM () @@ -1704,7 +1775,7 @@ uKVar swapped kv1 k2 ---------------- uUnboundKVar :: Bool -> KindVar -> TcKind -> TcM () uUnboundKVar swapped kv1 k2@(TyVarTy kv2) - | kv1 == kv2 = returnM () + | kv1 == kv2 = return () | otherwise -- Distinct kind variables = do { mb_k2 <- readKindVar kv2 ; case mb_k2 of @@ -1765,18 +1836,18 @@ kindOccurCheckErr tyvar ty unifyFunKind :: TcKind -> TcM (Maybe (TcKind, TcKind)) -- Like unifyFunTy, but does not fail; instead just returns Nothing -unifyFunKind (TyVarTy kvar) - = readKindVar kvar `thenM` \ maybe_kind -> +unifyFunKind (TyVarTy kvar) = do + maybe_kind <- readKindVar kvar case maybe_kind of Indirect fun_kind -> unifyFunKind fun_kind Flexi -> do { arg_kind <- newKindVar ; res_kind <- newKindVar ; writeKindVar kvar (mkArrowKind arg_kind res_kind) - ; returnM (Just (arg_kind,res_kind)) } + ; return (Just (arg_kind,res_kind)) } -unifyFunKind (FunTy arg_kind res_kind) = returnM (Just (arg_kind,res_kind)) -unifyFunKind other = returnM Nothing +unifyFunKind (FunTy arg_kind res_kind) = return (Just (arg_kind,res_kind)) +unifyFunKind other = return Nothing \end{code} %************************************************************************ @@ -1803,50 +1874,49 @@ checkExpectedKind :: Outputable a => a -> TcKind -> TcKind -> TcM () -- 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 () - | otherwise - = tryTc (unifyKind exp_kind act_kind) `thenM` \ (_errs, mb_r) -> - case mb_r of { - Just r -> returnM () ; -- Unification succeeded - Nothing -> + = return () + | otherwise = do + (_errs, mb_r) <- tryTc (unifyKind exp_kind act_kind) + case mb_r of + Just r -> return () ; -- Unification succeeded + Nothing -> do -- So there's definitely an error -- Now to find out what sort - zonkTcKind exp_kind `thenM` \ exp_kind -> - zonkTcKind act_kind `thenM` \ act_kind -> - - tcInitTidyEnv `thenM` \ env0 -> - let (exp_as, _) = splitKindFunTys exp_kind - (act_as, _) = splitKindFunTys act_kind - n_exp_as = length exp_as - n_act_as = length act_as - - (env1, tidy_exp_kind) = tidyKind env0 exp_kind - (env2, tidy_act_kind) = tidyKind env1 act_kind - - err | n_exp_as < n_act_as -- E.g. [Maybe] - = quotes (ppr ty) <+> ptext SLIT("is not applied to enough type arguments") - - -- Now n_exp_as >= n_act_as. In the next two cases, - -- n_exp_as == 0, and hence so is n_act_as - | isLiftedTypeKind exp_kind && isUnliftedTypeKind act_kind - = ptext SLIT("Expecting a lifted type, but") <+> quotes (ppr ty) - <+> ptext SLIT("is unlifted") - - | isUnliftedTypeKind exp_kind && isLiftedTypeKind act_kind - = ptext SLIT("Expecting an unlifted type, but") <+> quotes (ppr ty) - <+> ptext SLIT("is lifted") - - | otherwise -- E.g. Monad [Int] - = ptext SLIT("Kind mis-match") - - more_info = sep [ ptext SLIT("Expected kind") <+> - quotes (pprKind tidy_exp_kind) <> comma, - ptext SLIT("but") <+> quotes (ppr ty) <+> - ptext SLIT("has kind") <+> quotes (pprKind tidy_act_kind)] - in - failWithTcM (env2, err $$ more_info) - } + exp_kind <- zonkTcKind exp_kind + act_kind <- zonkTcKind act_kind + + env0 <- tcInitTidyEnv + let (exp_as, _) = splitKindFunTys exp_kind + (act_as, _) = splitKindFunTys act_kind + n_exp_as = length exp_as + n_act_as = length act_as + + (env1, tidy_exp_kind) = tidyKind env0 exp_kind + (env2, tidy_act_kind) = tidyKind env1 act_kind + + err | n_exp_as < n_act_as -- E.g. [Maybe] + = quotes (ppr ty) <+> ptext SLIT("is not applied to enough type arguments") + + -- Now n_exp_as >= n_act_as. In the next two cases, + -- n_exp_as == 0, and hence so is n_act_as + | isLiftedTypeKind exp_kind && isUnliftedTypeKind act_kind + = ptext SLIT("Expecting a lifted type, but") <+> quotes (ppr ty) + <+> ptext SLIT("is unlifted") + + | isUnliftedTypeKind exp_kind && isLiftedTypeKind act_kind + = ptext SLIT("Expecting an unlifted type, but") <+> quotes (ppr ty) + <+> ptext SLIT("is lifted") + + | otherwise -- E.g. Monad [Int] + = ptext SLIT("Kind mis-match") + + more_info = sep [ ptext SLIT("Expected kind") <+> + quotes (pprKind tidy_exp_kind) <> comma, + ptext SLIT("but") <+> quotes (ppr ty) <+> + ptext SLIT("has kind") <+> quotes (pprKind tidy_act_kind)] + + failWithTcM (env2, err $$ more_info) \end{code} %************************************************************************ @@ -1900,7 +1970,7 @@ check_sig_tyvars -- Guaranteed to be skolems -> TcM () check_sig_tyvars extra_tvs [] - = returnM () + = return () check_sig_tyvars extra_tvs sig_tvs = ASSERT( all isSkolemTyVar sig_tvs ) do { gbl_tvs <- tcGetGlobalTyVars @@ -1909,8 +1979,8 @@ check_sig_tyvars extra_tvs sig_tvs text "extra_tvs" <+> ppr extra_tvs])) ; let env_tvs = gbl_tvs `unionVarSet` extra_tvs - ; ifM (any (`elemVarSet` env_tvs) sig_tvs) - (bleatEscapedTvs env_tvs sig_tvs sig_tvs) + ; when (any (`elemVarSet` env_tvs) sig_tvs) + (bleatEscapedTvs env_tvs sig_tvs sig_tvs) } bleatEscapedTvs :: TcTyVarSet -- The global tvs @@ -1935,7 +2005,7 @@ bleatEscapedTvs globals sig_tvs zonked_tvs | not (zonked_tv `elemVarSet` globals) = return (tidy_env, msgs) | otherwise = do { (tidy_env1, globs) <- findGlobals (unitVarSet zonked_tv) tidy_env - ; returnM (tidy_env1, escape_msg sig_tv zonked_tv globs : msgs) } + ; return (tidy_env1, escape_msg sig_tv zonked_tv globs : msgs) } ----------------------- escape_msg sig_tv zonked_tv globs @@ -1959,8 +2029,8 @@ These two context are used with checkSigTyVars \begin{code} sigCtxt :: Id -> [TcTyVar] -> TcThetaType -> TcTauType -> TidyEnv -> TcM (TidyEnv, Message) -sigCtxt id sig_tvs sig_theta sig_tau tidy_env - = zonkTcType sig_tau `thenM` \ actual_tau -> +sigCtxt id sig_tvs sig_theta sig_tau tidy_env = do + actual_tau <- zonkTcType sig_tau let (env1, tidy_sig_tvs) = tidyOpenTyVars tidy_env sig_tvs (env2, tidy_sig_rho) = tidyOpenType env1 (mkPhiTy sig_theta sig_tau) @@ -1970,6 +2040,6 @@ sigCtxt id sig_tvs sig_theta sig_tau tidy_env ] msg = vcat [ptext SLIT("When trying to generalise the type inferred for") <+> quotes (ppr id), nest 2 sub_msg] - in - returnM (env3, msg) + + return (env3, msg) \end{code}