X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcUnify.lhs;h=821a1cc086112319b5d0662bca8f9c6146d8e852;hp=0d850def51356b9255261195a35d3bebe899e659;hb=a13551ce57c67a333f41f0a6fe7e05a09d0c3614;hpb=7de28fe1fe62b9fee93567224584dc7b1095f7db diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs index 0d850de..821a1cc 100644 --- a/compiler/typecheck/TcUnify.lhs +++ b/compiler/typecheck/TcUnify.lhs @@ -1,7 +1,9 @@ % +% (c) The University of Glasgow 2006 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998 % -\section{Type subsumption and unification} + +Type subsumption and unification \begin{code} module TcUnify ( @@ -17,7 +19,7 @@ module TcUnify ( -------------------------------- -- Holes - tcInfer, subFunTys, unBox, stripBoxyType, withBox, + tcInfer, subFunTys, unBox, refineBox, refineBoxToTau, withBox, boxyUnify, boxyUnifyList, zapToMonotype, boxySplitListTy, boxySplitTyConApp, boxySplitAppTy, wrapFunResCoercion @@ -25,61 +27,30 @@ module TcUnify ( #include "HsVersions.h" -import HsSyn ( ExprCoFn(..), idCoercion, isIdCoercion, (<.>), - mkCoLams, mkCoTyLams, mkCoApps ) -import TypeRep ( Type(..), PredType(..) ) - -import TcMType ( lookupTcTyVar, LookupTyVarResult(..), - tcInstSkolType, tcInstBoxyTyVar, newKindVar, newMetaTyVar, - newBoxyTyVar, newBoxyTyVarTys, readFilledBox, - readMetaTyVar, writeMetaTyVar, newFlexiTyVarTy, - tcInstSkolTyVars, tcInstTyVar, - zonkTcKind, zonkType, zonkTcType, zonkTcTyVarsAndFV, - readKindVar, writeKindVar ) -import TcSimplify ( tcSimplifyCheck ) -import TcEnv ( tcGetGlobalTyVars, findGlobals ) -import TcIface ( checkWiredInTyCon ) +import HsSyn +import TypeRep + +import TcMType +import TcSimplify +import TcEnv +import TcIface import TcRnMonad -- TcType, amongst others -import TcType ( TcKind, TcType, TcTyVar, BoxyTyVar, TcTauType, - BoxySigmaType, BoxyRhoType, BoxyType, - TcTyVarSet, TcThetaType, TcTyVarDetails(..), BoxInfo(..), - SkolemInfo( GenSkol, UnkSkol ), MetaDetails(..), isImmutableTyVar, - pprSkolTvBinding, isTauTy, isTauTyCon, isSigmaTy, - mkFunTy, mkFunTys, mkTyConApp, isMetaTyVar, - tcSplitForAllTys, tcSplitAppTy_maybe, tcSplitFunTys, mkTyVarTys, - tcSplitSigmaTy, tyVarsOfType, mkPhiTy, mkTyVarTy, mkPredTy, - typeKind, mkForAllTys, mkAppTy, isBoxyTyVar, - tcView, exactTyVarsOfType, - tidyOpenType, tidyOpenTyVar, tidyOpenTyVars, - pprType, tidyKind, tidySkolemTyVar, isSkolemTyVar, isSigTyVar, - TvSubst, mkTvSubst, zipTyEnv, zipOpenTvSubst, emptyTvSubst, - substTy, substTheta, - lookupTyVar, extendTvSubst ) -import Type ( Kind, SimpleKind, KindVar, - openTypeKind, liftedTypeKind, unliftedTypeKind, - mkArrowKind, defaultKind, - argTypeKind, isLiftedTypeKind, isUnliftedTypeKind, - isSubKind, pprKind, splitKindFunTys, isSubKindCon, - isOpenTypeKind, isArgTypeKind ) -import TysPrim ( alphaTy, betaTy ) -import Inst ( newDictBndrsO, instCall, instToId ) -import TyCon ( TyCon, tyConArity, tyConTyVars, isSynTyCon ) -import TysWiredIn ( listTyCon ) -import Id ( Id ) -import Var ( Var, varName, tyVarKind, isTcTyVar, tcTyVarDetails ) +import TcType +import Type +import TysPrim +import Inst +import TyCon +import TysWiredIn +import Var import VarSet import VarEnv -import Name ( Name, isSystemName ) -import ErrUtils ( Message ) -import Maybes ( expectJust, isNothing ) -import BasicTypes ( Arity ) -import Util ( notNull, equalLength ) +import Module +import Name +import ErrUtils +import Maybes +import BasicTypes +import Util import Outputable - --- Assertion imports -#ifdef DEBUG -import TcType ( isBoxyTy, isFlexi ) -#endif \end{code} %************************************************************************ @@ -95,7 +66,7 @@ tcInfer tc_infer ; res <- tc_infer (mkTyVarTy box) ; res_ty <- readFilledBox box -- Guaranteed filled-in by now ; return (res, res_ty) } -\end{code} +\end{code} %************************************************************************ @@ -110,7 +81,7 @@ subFunTys :: SDoc -- Somthing like "The function f has 3 arguments" -> Arity -- Expected # of args -> BoxyRhoType -- res_ty -> ([BoxySigmaType] -> BoxyRhoType -> TcM a) - -> TcM (ExprCoFn, a) + -> TcM (HsWrapper, a) -- Attempt to decompse res_ty to have enough top-level arrows to -- match the number of patterns in the match group -- @@ -142,19 +113,20 @@ 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' 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 - = do { (gen_fn, (co_fn, res)) <- tcGen res_ty emptyVarSet $ \ res_ty' -> + = 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) } loop 0 args_so_far res_ty = do { res <- thing_inside (reverse args_so_far) res_ty - ; return (idCoercion, res) } + ; return (idHsWrapper, res) } loop n args_so_far (FunTy arg_ty res_ty) = do { (co_fn, res) <- loop (n-1) (arg_ty:args_so_far) res_ty @@ -172,13 +144,13 @@ 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 Flexi -> do { (res_ty:arg_tys) <- withMetaTvs tv kinds mk_res_ty ; res <- thing_inside (reverse args_so_far ++ arg_tys) res_ty - ; return (idCoercion, res) } } + ; return (idHsWrapper, res) } } where mk_res_ty (res_ty' : arg_tys') = mkFunTys arg_tys' res_ty' mk_res_ty [] = panic "TcUnify.mk_res_ty1" @@ -223,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 @@ -235,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 @@ -248,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 @@ -262,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 @@ -552,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 @@ -594,30 +569,41 @@ expected_ty. \begin{code} ----------------- -tcSubExp :: BoxySigmaType -> BoxySigmaType -> TcM ExprCoFn -- Locally used only +tcSubExp :: BoxySigmaType -> BoxySigmaType -> TcM HsWrapper -- Locally used only -- (tcSub act exp) checks that -- act <= exp tcSubExp 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 foarall a. a->a with forall a. a->a" - -- So instead I'm adding it when moving from tc_sub to u_tys + -- messages, such as "can't match forall a. a->a with forall a. a->a" + -- Example is tcfail165: + -- do var <- newEmptyMVar :: IO (MVar (forall a. Show a => a -> String)) + -- putMVar var (show :: forall a. Show a => a -> String) + -- Here the info does not flow from the 'var' arg of putMVar to its 'show' arg + -- but after zonking it looks as if it does! + -- + -- 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 Nothing actual_ty actual_ty False expected_ty expected_ty + tc_sub SubOther actual_ty actual_ty False expected_ty expected_ty -tcFunResTy :: Name -> BoxySigmaType -> BoxySigmaType -> TcM ExprCoFn -- Locally used only +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 (Just fun) actual_ty actual_ty False expected_ty expected_ty + tc_sub (SubFun fun) actual_ty actual_ty False expected_ty expected_ty ----------------- -tc_sub :: Maybe Name -- Just fun => we're looking at a function result type +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 -> BoxySigmaType -- actual_ty, before expanding synonyms -> BoxySigmaType -- ..and after -> InBox -- True <=> expected_ty is inside a box -> BoxySigmaType -- expected_ty, before -> BoxySigmaType -- ..and after - -> TcM ExprCoFn + -> TcM HsWrapper -- The acual_ty is never inside a box -- IMPORTANT pre-condition: if the args contain foralls, the bound type -- variables are visible non-monadically @@ -625,24 +611,25 @@ tc_sub :: Maybe Name -- Just fun => we're looking at a function result type -- 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 mb_fun act_sty act_ty exp_ib exp_sty exp_ty - = tc_sub1 mb_fun act_sty act_ty exp_ib exp_sty exp_ty +tc_sub 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! -tc_sub1 mb_fun act_sty act_ty exp_ib exp_sty exp_ty - | Just exp_ty' <- tcView exp_ty = tc_sub mb_fun act_sty act_ty exp_ib exp_sty exp_ty' -tc_sub1 mb_fun act_sty act_ty exp_ib exp_sty exp_ty - | Just act_ty' <- tcView act_ty = tc_sub mb_fun 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 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 ----------------------------------- -- 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 mb_fun act_sty (TyVarTy tv) exp_ib exp_sty exp_ty - = do { addErrCtxtM (subCtxt mb_fun act_sty exp_sty) $ +tc_sub1 sub_ctxt act_sty (TyVarTy tv) exp_ib exp_sty exp_ty + = do { addSubCtxt sub_ctxt act_sty exp_sty $ uVar True False tv exp_ib exp_sty exp_ty - ; return idCoercion } + ; return idHsWrapper } ----------------------------------- -- Skolemisation case (rule SKOL) @@ -655,11 +642,13 @@ tc_sub1 mb_fun act_sty (TyVarTy tv) exp_ib exp_sty exp_ty -- g :: Ord b => b->b -- Consider f g ! -tc_sub1 mb_fun 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 -> - tc_sub mb_fun act_sty act_ty False body_exp_ty body_exp_ty +tc_sub1 sub_ctxt act_sty act_ty exp_ib exp_sty 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 act_tvs = tyVarsOfType act_ty @@ -672,7 +661,7 @@ tc_sub1 mb_fun act_sty act_ty exp_ib exp_sty exp_ty -- expected_ty: Int -> Int -- co_fn e = e Int dOrdInt -tc_sub1 mb_fun act_sty actual_ty exp_ib exp_sty expected_ty +tc_sub1 sub_ctxt 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.) @@ -698,54 +687,69 @@ tc_sub1 mb_fun 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 mb_fun tau' tau' 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) } ----------------------------------- -- Function case (rule F1) -tc_sub1 mb_fun _ (FunTy act_arg act_res) exp_ib _ (FunTy exp_arg exp_res) - = tc_sub_funs mb_fun act_arg act_res exp_ib exp_arg exp_res +tc_sub1 sub_ctxt act_sty (FunTy act_arg act_res) exp_ib exp_sty (FunTy exp_arg exp_res) + = addSubCtxt sub_ctxt act_sty exp_sty $ + tc_sub_funs act_arg act_res exp_ib exp_arg exp_res -- Function case (rule F2) -tc_sub1 mb_fun act_sty act_ty@(FunTy act_arg act_res) _ exp_sty (TyVarTy exp_tv) +tc_sub1 sub_ctxt act_sty act_ty@(FunTy act_arg act_res) _ exp_sty (TyVarTy exp_tv) | isBoxyTyVar exp_tv - = do { cts <- readMetaTyVar exp_tv + = addSubCtxt sub_ctxt act_sty exp_sty $ + do { cts <- readMetaTyVar exp_tv ; case cts of - Indirect ty -> tc_sub mb_fun act_sty act_ty True exp_sty ty + Indirect ty -> tc_sub SubDone 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 mb_fun act_arg act_res True arg_ty res_ty } } + ; tc_sub_funs 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 mb_fun act_sty actual_ty exp_ib exp_sty expected_ty - = do { addErrCtxtM (subCtxt mb_fun act_sty exp_sty) $ - u_tys True False act_sty actual_ty exp_ib exp_sty expected_ty - ; return idCoercion } +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 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 mb_fun act_arg act_res exp_ib exp_arg exp_res +tc_sub_funs act_arg act_res exp_ib exp_arg exp_res = do { uTys False act_arg exp_ib exp_arg - ; co_fn_res <- tc_sub mb_fun act_res act_res exp_ib exp_res exp_res + ; co_fn_res <- tc_sub SubDone act_res act_res exp_ib exp_res exp_res ; wrapFunResCoercion [exp_arg] co_fn_res } ----------------------------------- wrapFunResCoercion :: [TcType] -- Type of args - -> ExprCoFn -- HsExpr a -> HsExpr b - -> TcM ExprCoFn -- HsExpr (arg_tys -> a) -> HsExpr (arg_tys -> b) + -> HsWrapper -- HsExpr a -> HsExpr b + -> TcM HsWrapper -- HsExpr (arg_tys -> a) -> HsExpr (arg_tys -> b) wrapFunResCoercion arg_tys co_fn_res - | isIdCoercion co_fn_res = return idCoercion + | isIdHsWrapper co_fn_res = return idHsWrapper | null arg_tys = return co_fn_res | otherwise = do { arg_ids <- newSysLocalIds FSLIT("sub") arg_tys - ; return (mkCoLams arg_ids <.> co_fn_res <.> mkCoApps arg_ids) } + ; return (mkWpLams arg_ids <.> co_fn_res <.> mkWpApps arg_ids) } \end{code} @@ -761,8 +765,8 @@ tcGen :: BoxySigmaType -- expected_ty -> TcTyVarSet -- Extra tyvars that the universally -- quantified tyvars of expected_ty -- must not be unified - -> (BoxyRhoType -> TcM result) -- spec_ty - -> TcM (ExprCoFn, result) + -> ([TcTyVar] -> BoxyRhoType -> TcM result) + -> TcM (HsWrapper, result) -- The expression has type: spec_ty -> expected_ty tcGen expected_ty extra_tvs thing_inside -- We expect expected_ty to be a forall-type @@ -771,22 +775,21 @@ tcGen expected_ty extra_tvs thing_inside -- We expect expected_ty to be a forall -- mention the *instantiated* tyvar names, so that we get a -- good error message "Rigid variable 'a' is bound by (forall a. a->a)" -- Hence the tiresome but innocuous fixM - ((forall_tvs, theta, rho_ty), skol_info) <- fixM (\ ~(_, skol_info) -> + ((tvs', theta', rho'), skol_info) <- fixM (\ ~(_, skol_info) -> do { (forall_tvs, theta, rho_ty) <- tcInstSkolType skol_info expected_ty - ; span <- getSrcSpanM - ; let skol_info = GenSkol forall_tvs (mkPhiTy theta rho_ty) span + -- Get loation from monad, not from expected_ty + ; let skol_info = GenSkol forall_tvs (mkPhiTy theta rho_ty) ; return ((forall_tvs, theta, rho_ty), skol_info) }) #ifdef DEBUG ; traceTc (text "tcGen" <+> vcat [text "extra_tvs" <+> ppr extra_tvs, text "expected_ty" <+> ppr expected_ty, - text "inst ty" <+> ppr forall_tvs <+> ppr theta <+> ppr rho_ty, - text "free_tvs" <+> ppr free_tvs, - text "forall_tvs" <+> ppr forall_tvs]) + text "inst ty" <+> ppr tvs' <+> ppr theta' <+> ppr rho', + text "free_tvs" <+> ppr free_tvs]) #endif -- Type-check the arg and unify with poly type - ; (result, lie) <- getLIE (thing_inside rho_ty) + ; (result, lie) <- getLIE (thing_inside tvs' rho') -- Check that the "forall_tvs" havn't been constrained -- The interesting bit here is that we must include the free variables @@ -799,20 +802,20 @@ tcGen expected_ty extra_tvs thing_inside -- We expect expected_ty to be a forall -- Conclusion: include the free vars of the expected_ty in the -- list of "free vars" for the signature check. - ; dicts <- newDictBndrsO (SigOrigin skol_info) theta - ; inst_binds <- tcSimplifyCheck sig_msg forall_tvs dicts lie + ; loc <- getInstLoc (SigOrigin skol_info) + ; dicts <- newDictBndrs loc theta' + ; inst_binds <- tcSimplifyCheck loc tvs' dicts lie - ; checkSigTyVarsWrt free_tvs forall_tvs + ; checkSigTyVarsWrt free_tvs tvs' ; traceTc (text "tcGen:done") ; let - -- The CoLet binds any Insts which came out of the simplification. + -- The WpLet binds any Insts which came out of the simplification. dict_ids = map instToId dicts - co_fn = mkCoTyLams forall_tvs <.> mkCoLams dict_ids <.> CoLet inst_binds + co_fn = mkWpTyLams tvs' <.> mkWpLams dict_ids <.> WpLet inst_binds ; returnM (co_fn, result) } where free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs - sig_msg = ptext SLIT("expected type of an expression") \end{code} @@ -859,7 +862,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 } --------------- @@ -953,8 +957,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) @@ -980,26 +1027,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 - ; 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 @@ -1010,6 +1037,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] @@ -1249,7 +1280,7 @@ uUnfilledVars outer swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2) k1_sub_k2 = k1 `isSubKind` k2 k2_sub_k1 = k2 `isSubKind` k1 - nicer_to_update_tv1 = isSystemName (varName tv1) + nicer_to_update_tv1 = isSystemName (Var.varName tv1) -- Try to update sys-y type variables in preference to ones -- gotten (say) by instantiating a polymorphic function with -- a user-written type sig @@ -1350,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 } @@ -1390,16 +1425,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 @@ -1448,6 +1494,7 @@ unBox (TyVarTy tv) unBoxPred (ClassP cls tys) = do { tys' <- mapM unBox tys; return (ClassP cls tys') } unBoxPred (IParam ip ty) = do { ty' <- unBox ty; return (IParam ip ty') } +unBoxPred (EqPred ty1 ty2) = do { ty1' <- unBox ty1; ty2' <- unBox ty2; return (EqPred ty1' ty2') } \end{code} @@ -1477,31 +1524,44 @@ 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. -subCtxt mb_fun actual_res_ty expected_res_ty tidy_env - = do { exp_ty' <- zonkTcType expected_res_ty - ; act_ty' <- zonkTcType actual_res_ty - ; let - (env1, exp_ty'') = tidyOpenType tidy_env exp_ty' - (env2, act_ty'') = tidyOpenType env1 act_ty' - (exp_args, _) = tcSplitFunTys exp_ty'' - (act_args, _) = tcSplitFunTys act_ty'' +addSubCtxt SubDone actual_res_ty expected_res_ty thing_inside + = thing_inside +addSubCtxt sub_ctxt actual_res_ty expected_res_ty thing_inside + = addErrCtxtM mk_err thing_inside + where + mk_err tidy_env + = do { exp_ty' <- zonkTcType expected_res_ty + ; act_ty' <- zonkTcType actual_res_ty + ; let (env1, exp_ty'') = tidyOpenType tidy_env exp_ty' + (env2, act_ty'') = tidyOpenType env1 act_ty' + (exp_args, _) = tcSplitFunTys exp_ty'' + (act_args, _) = tcSplitFunTys act_ty'' - len_act_args = length act_args - len_exp_args = length exp_args + len_act_args = length act_args + len_exp_args = length exp_args - message = case mb_fun of - Just 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) } + 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'' + ; return (env2, message) } - where wrongArgsCtxt too_many_or_few fun = ptext SLIT("Probable cause:") <+> quotes (ppr fun) <+> ptext SLIT("is applied to") <+> text too_many_or_few <+> 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 @@ -1525,31 +1585,59 @@ 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 tidy_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") <+> 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 + tc2_pkg = modulePackageId (nameModule (getName tc2)) + mk_mod this_mod + | tc_mod == this_mod = ptext SLIT("in this module") + | not home_pkg && tc2_pkg /= tc_pkg = pp_pkg + -- Suppress the module name if (a) it's from another package + -- (b) other_ty isn't from that same package + + | otherwise = ptext SLIT("in module") <+> quotes (ppr tc_mod) <+> pp_pkg + where + home_pkg = tc_pkg == modulePackageId this_mod + pp_pkg | home_pkg = empty + | otherwise = ptext SLIT("in package") <+> quotes (ppr tc_pkg) +ppr_extra env ty other_ty = return (env, empty) -- Normal case + +----------------------- notMonoType ty = do { ty' <- zonkTcType ty ; env0 <- tcInitTidyEnv @@ -1557,6 +1645,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 @@ -1714,6 +1809,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 ()