X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcUnify.lhs;h=04e9379e7c0b64d9887197d80774e762f6d22dfd;hb=3f1b316d7035c55cd712cd39a9981339bcef2e8c;hp=2b42d0b9e37e9251333880d4ba91599c046f3db6;hpb=f493bc7c7325a3809dda3637c12e5d9383ba8117;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs index 2b42d0b..04e9379 100644 --- a/compiler/typecheck/TcUnify.lhs +++ b/compiler/typecheck/TcUnify.lhs @@ -6,6 +6,13 @@ Type subsumption and unification \begin{code} +{-# OPTIONS -w #-} +-- The above warning supression flag is a temporary kludge. +-- While working on this module you are encouraged to remove it and fix +-- any warnings in the module. See +-- http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings +-- for details + module TcUnify ( -- Full-blown subsumption tcSubExp, tcFunResTy, tcGen, @@ -15,13 +22,13 @@ module TcUnify ( unifyType, unifyTypeList, unifyTheta, unifyKind, unifyKinds, unifyFunKind, checkExpectedKind, - preSubType, boxyMatchTypes, + preSubType, boxyMatchTypes, -------------------------------- -- Holes tcInfer, subFunTys, unBox, refineBox, refineBoxToTau, withBox, boxyUnify, boxyUnifyList, zapToMonotype, - boxySplitListTy, boxySplitTyConApp, boxySplitAppTy, + boxySplitListTy, boxySplitPArrTy, boxySplitTyConApp, boxySplitAppTy, wrapFunResCoercion ) where @@ -33,10 +40,12 @@ import TypeRep import TcMType import TcSimplify import TcEnv +import TcTyFuns import TcIface import TcRnMonad -- TcType, amongst others import TcType import Type +import Coercion import TysPrim import Inst import TyCon @@ -44,13 +53,13 @@ import TysWiredIn import Var import VarSet import VarEnv -import Module import Name import ErrUtils import Maybes import BasicTypes import Util import Outputable +import Unique \end{code} %************************************************************************ @@ -64,7 +73,7 @@ tcInfer :: (BoxyType -> TcM a) -> TcM (a, TcType) tcInfer tc_infer = do { box <- newBoxyTyVar openTypeKind ; res <- tc_infer (mkTyVarTy box) - ; res_ty <- readFilledBox box -- Guaranteed filled-in by now + ; res_ty <- {- pprTrace "tcInfer" (ppr (mkTyVarTy box)) $ -} readFilledBox box -- Guaranteed filled-in by now ; return (res, res_ty) } \end{code} @@ -87,7 +96,7 @@ subFunTys :: SDoc -- Somthing like "The function f has 3 arguments" -- -- If (subFunTys n_args res_ty thing_inside) = (co_fn, res) -- and the inner call to thing_inside passes args: [a1,...,an], b --- then co_fn :: (a1 -> ... -> an -> b) -> res_ty +-- then co_fn :: (a1 -> ... -> an -> b) ~ res_ty -- -- Note that it takes a BoxyRho type, and guarantees to return a BoxyRhoType @@ -119,7 +128,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) } @@ -133,24 +143,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_unit) <- tryTcErrs $ boxyUnify res_ty (FunTy arg_ty' res_ty') - ; if isNothing mb_unit then bale_out args_so_far - else loop n args_so_far (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 { 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" @@ -160,6 +193,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 @@ -177,8 +225,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) + -- It's used for wired-in tycons, so we call checkWiredInTyCon -- Precondition: never called with FunTyCon -- Precondition: input type :: * @@ -189,14 +238,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 @@ -204,24 +267,43 @@ boxySplitTyConApp tc orig_ty = do { cts <- readMetaTyVar tv ; 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) } - } + Flexi -> do { arg_tys <- withMetaTvs tv arg_kinds mk_res_ty + ; 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 @@ -234,18 +316,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 @@ -257,11 +350,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} @@ -301,7 +419,7 @@ withBox :: Kind -> (BoxySigmaType -> TcM a) -> TcM (a, TcType) withBox kind thing_inside = do { box_tv <- newMetaTyVar BoxTv kind ; res <- thing_inside (mkTyVarTy box_tv) - ; ty <- readFilledBox box_tv + ; ty <- {- pprTrace "with_box" (ppr (mkTyVarTy box_tv)) $ -} readFilledBox box_tv ; return (res, ty) } \end{code} @@ -474,7 +592,9 @@ boxy_match tmpl_tvs orig_tmpl_ty boxy_tvs orig_boxy_ty subst (boxy_tvs `extendVarSetList` tvs2) tau2 subst go (TyConApp tc1 tys1) (TyConApp tc2 tys2) - | tc1 == tc2 = go_s tys1 tys2 + | tc1 == tc2 + , not $ isOpenSynTyCon tc1 + = go_s tys1 tys2 go (FunTy arg1 res1) (FunTy arg2 res2) = go_s [arg1,res1] [arg2,res2] @@ -527,7 +647,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 ty2 = go ty1 ty2' + | Just ty2' <- tcView ty1 = go ty1 ty2' -- For now, we don't look inside ForAlls, PredTys go ty1 ty2 = orig_ty1 -- Default @@ -563,7 +683,7 @@ That is, that a value of type offered_ty is acceptable in a place expecting a value of type expected_ty. It returns a coercion function - co_fn :: offered_ty -> expected_ty + co_fn :: offered_ty ~ expected_ty which takes an HsExpr of type offered_ty into one of type expected_ty. @@ -627,9 +747,14 @@ tc_sub1 sub_ctxt act_sty act_ty exp_ib exp_sty exp_ty -- 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 - = do { addSubCtxt sub_ctxt act_sty exp_sty $ - uVar True False tv exp_ib exp_sty exp_ty - ; return idHsWrapper } + = do { traceTc (text "tc_sub1 - case 1") + ; coi <- addSubCtxt sub_ctxt 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 $ coiToHsWrapper coi + } ----------------------------------- -- Skolemisation case (rule SKOL) @@ -644,12 +769,14 @@ tc_sub1 sub_ctxt act_sty (TyVarTy tv) exp_ib exp_sty 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 + = 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 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 -- It's really important to check for escape wrt @@ -670,7 +797,8 @@ tc_sub1 sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty -- Pre-subsumpion finds a|->Int, and that works fine, whereas -- just running full subsumption would fail. | isSigmaTy actual_ty - = do { -- Perform pre-subsumption, and instantiate + = do { traceTc (text "tc_sub1 - case 3") + ; -- Perform pre-subsumption, and instantiate -- the type with info from the pre-subsumption; -- boxy tyvars if pre-subsumption gives no info let (tyvars, theta, tau) = tcSplitSigmaTy actual_ty @@ -702,17 +830,20 @@ tc_sub1 sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty ----------------------------------- -- Function case (rule F1) 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 + = 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 + } -- Function case (rule F2) tc_sub1 sub_ctxt 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 { cts <- readMetaTyVar exp_tv + 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 - Flexi -> do { [arg_ty,res_ty] <- withMetaTvs exp_tv fun_kinds mk_res_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 } } where mk_res_ty [arg_ty', res_ty'] = mkFunTy arg_ty' res_ty' @@ -720,14 +851,22 @@ tc_sub1 sub_ctxt act_sty act_ty@(FunTy act_arg act_res) _ exp_sty (TyVarTy exp_t 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) + = 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 + } + tc_sub1 sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty - = defer_to_boxy_matching sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty + = do { 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 sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty - = do { addSubCtxt sub_ctxt act_sty exp_sty $ + = do { coi <- addSubCtxt sub_ctxt act_sty exp_sty $ u_tys outer False act_sty actual_ty exp_ib exp_sty expected_ty - ; return idHsWrapper } + ; return $ coiToHsWrapper coi + } where outer = case sub_ctxt of -- Ugh SubDone -> False @@ -735,9 +874,14 @@ defer_to_boxy_matching sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty ----------------------------------- tc_sub_funs act_arg act_res exp_ib exp_arg exp_res - = do { uTys False act_arg exp_ib exp_arg + = 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 - ; wrapFunResCoercion [exp_arg] co_fn_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) + } ----------------------------------- wrapFunResCoercion @@ -745,8 +889,10 @@ wrapFunResCoercion -> HsWrapper -- HsExpr a -> HsExpr b -> TcM HsWrapper -- HsExpr (arg_tys -> a) -> HsExpr (arg_tys -> b) wrapFunResCoercion arg_tys co_fn_res - | isIdHsWrapper co_fn_res = return idHsWrapper - | null arg_tys = return co_fn_res + | isIdHsWrapper co_fn_res + = return idHsWrapper + | null arg_tys + = return co_fn_res | otherwise = do { arg_ids <- newSysLocalIds FSLIT("sub") arg_tys ; return (mkWpLams arg_ids <.> co_fn_res <.> mkWpApps arg_ids) } @@ -771,11 +917,12 @@ tcGen :: BoxySigmaType -- expected_ty tcGen expected_ty extra_tvs thing_inside -- We expect expected_ty to be a forall-type -- If not, the call is a no-op - = do { -- We want the GenSkol info in the skolemised type variables to + = do { traceTc (text "tcGen") + -- We want the GenSkol info in the skolemised type variables to -- 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 - ((tvs', theta', rho'), skol_info) <- fixM (\ ~(_, skol_info) -> + ; ((tvs', theta', rho'), skol_info) <- fixM (\ ~(_, skol_info) -> do { (forall_tvs, theta, rho_ty) <- tcInstSkolType skol_info expected_ty -- Get loation from monad, not from expected_ty ; let skol_info = GenSkol forall_tvs (mkPhiTy theta rho_ty) @@ -811,12 +958,12 @@ tcGen expected_ty extra_tvs thing_inside -- We expect expected_ty to be a forall ; let -- The WpLet binds any Insts which came out of the simplification. - dict_ids = map instToId dicts - co_fn = mkWpTyLams tvs' <.> mkWpLams dict_ids <.> WpLet inst_binds + dict_vars = map instToVar dicts + co_fn = mkWpTyLams tvs' <.> mkWpLams dict_vars <.> WpLet inst_binds ; returnM (co_fn, result) } where free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs -\end{code} +\end{code} @@ -830,20 +977,20 @@ The exported functions are all defined as versions of some non-exported generic functions. \begin{code} -boxyUnify :: BoxyType -> BoxyType -> TcM () +boxyUnify :: BoxyType -> BoxyType -> TcM CoercionI -- Acutal and expected, respectively boxyUnify ty1 ty2 = addErrCtxtM (unifyCtxt ty1 ty2) $ uTysOuter False ty1 False ty2 --------------- -boxyUnifyList :: [BoxyType] -> [BoxyType] -> TcM () +boxyUnifyList :: [BoxyType] -> [BoxyType] -> TcM [CoercionI] -- Arguments should have equal length -- Acutal and expected types boxyUnifyList tys1 tys2 = uList boxyUnify tys1 tys2 --------------- -unifyType :: TcTauType -> TcTauType -> TcM () +unifyType :: TcTauType -> TcTauType -> TcM CoercionI -- No boxes expected inside these types -- Acutal and expected types unifyType ty1 ty2 -- ty1 expected, ty2 inferred @@ -853,27 +1000,31 @@ unifyType ty1 ty2 -- ty1 expected, ty2 inferred uTysOuter True ty1 True ty2 --------------- -unifyPred :: PredType -> PredType -> TcM () +unifyPred :: PredType -> PredType -> TcM CoercionI -- Acutal and expected types unifyPred p1 p2 = addErrCtxtM (unifyCtxt (mkPredTy p1) (mkPredTy p2)) $ - uPred True True p1 True p2 + uPred True True p1 True p2 -unifyTheta :: TcThetaType -> TcThetaType -> TcM () +unifyTheta :: TcThetaType -> TcThetaType -> TcM [CoercionI] -- Acutal and expected types unifyTheta theta1 theta2 = do { checkTc (equalLength theta1 theta2) (vcat [ptext SLIT("Contexts differ in length"), nest 2 $ parens $ ptext SLIT("Use -fglasgow-exts to allow this")]) - ; uList unifyPred theta1 theta2 } + ; uList unifyPred theta1 theta2 + } --------------- -uList :: (a -> a -> TcM ()) - -> [a] -> [a] -> TcM () +uList :: (a -> a -> TcM b) + -> [a] -> [a] -> TcM [b] -- Unify corresponding elements of two lists of types, which --- should be f equal length. We charge down the list explicitly so that +-- should be of equal length. We charge down the list explicitly so that -- we can complain if their lengths differ. -uList unify [] [] = return () -uList unify (ty1:tys1) (ty2:tys2) = do { unify ty1 ty2; uList unify tys1 tys2 } +uList unify [] [] = return [] +uList unify (ty1:tys1) (ty2:tys2) = do { x <- unify ty1 ty2; + ; xs <- uList unify tys1 tys2 + ; return (x:xs) + } uList unify ty1s ty2s = panic "Unify.uList: mismatched type lists!" \end{code} @@ -895,8 +1046,8 @@ unifyTypeList (ty1:tys@(ty2:_)) = do { unifyType ty1 ty2 %* * %************************************************************************ -@uTys@ is the heart of the unifier. Each arg happens twice, because -we want to report errors in terms of synomyms if poss. The first of +@uTys@ is the heart of the unifier. Each arg occurs twice, because +we want to report errors in terms of synomyms if possible. The first of the pair is used in error messages only; it is always the same as the second, except that if the first is a synonym then the second may be a de-synonym'd version. This way we get better error messages. @@ -904,6 +1055,10 @@ de-synonym'd version. This way we get better error messages. We call the first one \tr{ps_ty1}, \tr{ps_ty2} for ``possible synomym''. \begin{code} +type SwapFlag = Bool + -- False <=> the two args are (actual, expected) respectively + -- True <=> the two args are (expected, actual) respectively + type InBox = Bool -- True <=> we are inside a box -- False <=> we are outside a box -- The importance of this is that if we get "filled-box meets @@ -919,54 +1074,73 @@ type Outer = Bool -- True <=> this is the outer level of a unification -- pop the context to remove the "Expected/Acutal" context uTysOuter, uTys - :: InBox -> TcType -- ty1 is the *expected* type - -> InBox -> TcType -- ty2 is the *actual* type - -> TcM () -uTysOuter nb1 ty1 nb2 ty2 = do { traceTc (text "uTysOuter" <+> ppr ty1 <+> ppr ty2) - ; u_tys True nb1 ty1 ty1 nb2 ty2 ty2 } -uTys nb1 ty1 nb2 ty2 = do { traceTc (text "uTys" <+> ppr ty1 <+> ppr ty2) - ; u_tys False nb1 ty1 ty1 nb2 ty2 ty2 } + :: InBox -> TcType -- ty1 is the *actual* type + -> InBox -> TcType -- ty2 is the *expected* type + -> TcM CoercionI +uTysOuter nb1 ty1 nb2 ty2 + = do { traceTc (text "uTysOuter" <+> ppr ty1 <+> ppr ty2) + ; u_tys True nb1 ty1 ty1 nb2 ty2 ty2 } +uTys nb1 ty1 nb2 ty2 + = do { traceTc (text "uTys" <+> ppr ty1 <+> ppr ty2) + ; u_tys False nb1 ty1 ty1 nb2 ty2 ty2 } -------------- -uTys_s :: InBox -> [TcType] -- ty1 is the *actual* types - -> InBox -> [TcType] -- ty2 is the *expected* types - -> TcM () -uTys_s nb1 [] nb2 [] = returnM () -uTys_s nb1 (ty1:tys1) nb2 (ty2:tys2) = do { uTys nb1 ty1 nb2 ty2 - ; uTys_s nb1 tys1 nb2 tys2 } +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 (ty1:tys1) nb2 (ty2:tys2) = do { coi <- uTys nb1 ty1 nb2 ty2 + ; cois <- uTys_s nb1 tys1 nb2 tys2 + ; return (coi:cois) + } uTys_s nb1 ty1s nb2 ty2s = panic "Unify.uTys_s: mismatched type lists!" -------------- u_tys :: Outer -> InBox -> TcType -> TcType -- ty1 is the *actual* type -> InBox -> TcType -> TcType -- ty2 is the *expected* type - -> TcM () + -> TcM CoercionI u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2 - = go outer ty1 ty2 + = do { traceTc (text "u_tys " <+> ppr ty1 <+> text " " <+> ppr ty2) + ; coi <- go outer ty1 ty2 + ; traceTc (case coi of + ACo co -> text "u_tys yields coercion: " <+> ppr co + IdCo -> text "u_tys yields no coercion") + ; return coi + } where - -- Always expand synonyms (see notes at end) + go :: Outer -> TcType -> TcType -> TcM CoercionI + go outer ty1 ty2 = + do { traceTc (text "go " <+> ppr orig_ty1 <+> text "/" <+> ppr ty1 + <+> ppr orig_ty2 <+> text "/" <+> ppr ty2) + ; go1 outer ty1 ty2 + } + + go1 :: Outer -> TcType -> TcType -> TcM CoercionI + -- Always expand synonyms: see Note [Unification and synonyms] -- (this also throws away FTVs) - go outer ty1 ty2 + go1 outer ty1 ty2 | Just ty1' <- tcView ty1 = go False ty1' ty2 | Just ty2' <- tcView ty2 = go False ty1 ty2' -- Variables; go for uVar - 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 + go1 outer (TyVarTy tyvar1) ty2 = uVar outer False tyvar1 nb2 orig_ty2 ty2 + go1 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 + go1 _ ty1 ty2 | isSigmaTy ty1 || isSigmaTy ty2 - = do { checkM (equalLength tvs1 tvs2) + = do { traceTc (text "We have sigma types: equalLength" <+> ppr tvs1 <+> ppr tvs2) + ; checkM (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 -- Get location from monad, not from tvs1 ; let tys = mkTyVarTys tvs @@ -980,8 +1154,9 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2 { checkM (equalLength theta1 theta2) (unifyMisMatch outer False orig_ty1 orig_ty2) - ; uPreds False nb1 theta1 nb2 theta2 - ; uTys nb1 tau1 nb2 tau2 + ; cois <- uPreds False nb1 theta1 nb2 theta2 -- TOMDO: do something with these pred_cois + ; traceTc (text "TOMDO!") + ; coi <- 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)) @@ -995,55 +1170,111 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2 -- This check comes last, because the error message is -- extremely unhelpful. ; ifM (nb1 && nb2) (notMonoType ty1) + ; return coi }} where (tvs1, body1) = tcSplitForAllTys ty1 (tvs2, body2) = tcSplitForAllTys ty2 -- Predicates - go outer (PredTy p1) (PredTy p2) = uPred False nb1 p1 nb2 p2 + go1 outer (PredTy p1) (PredTy p2) + = uPred False nb1 p1 nb2 p2 -- Type constructors must match - go _ (TyConApp con1 tys1) (TyConApp con2 tys2) - | con1 == con2 = uTys_s nb1 tys1 nb2 tys2 + go1 _ (TyConApp con1 tys1) (TyConApp con2 tys2) + | con1 == con2 && not (isOpenSynTyCon con1) + = do { cois <- uTys_s nb1 tys1 nb2 tys2 + ; return $ mkTyConAppCoI con1 tys1 cois + } -- See Note [TyCon app] + | con1 == con2 && identicalOpenSynTyConApp + = do { cois <- uTys_s nb1 tys1' nb2 tys2' + ; return $ mkTyConAppCoI con1 tys1 (replicate n IdCo ++ cois) + } + where + n = tyConArity con1 + (idxTys1, tys1') = splitAt n tys1 + (idxTys2, tys2') = splitAt n tys2 + identicalOpenSynTyConApp = idxTys1 `tcEqTypes` idxTys2 + -- See Note [OpenSynTyCon app] -- Functions; just check the two parts - go _ (FunTy fun1 arg1) (FunTy fun2 arg2) - = do { uTys nb1 fun1 nb2 fun2 - ; uTys nb1 arg1 nb2 arg2 } + go1 _ (FunTy fun1 arg1) (FunTy fun2 arg2) + = do { coi_l <- uTys nb1 fun1 nb2 fun2 + ; coi_r <- uTys nb1 arg1 nb2 arg2 + ; return $ mkFunTyCoI fun1 coi_l arg1 coi_r + } -- Applications need a bit of care! -- They can match FunTy and TyConApp, so use splitAppTy_maybe -- NB: we've already dealt with type variables and Notes, -- so if one type is an App the other one jolly well better be too - go outer (AppTy s1 t1) ty2 + go1 outer (AppTy s1 t1) ty2 | Just (s2,t2) <- tcSplitAppTy_maybe ty2 - = do { uTys nb1 s1 nb2 s2; uTys nb1 t1 nb2 t2 } + = do { coi_s <- uTys nb1 s1 nb2 s2; coi_t <- uTys nb1 t1 nb2 t2 + ; return $ mkAppTyCoI s1 coi_s t1 coi_t } -- Now the same, but the other way round -- Don't swap the types, because the error messages get worse - go outer ty1 (AppTy s2 t2) + go1 outer ty1 (AppTy s2 t2) | Just (s1,t1) <- tcSplitAppTy_maybe ty1 - = do { uTys nb1 s1 nb2 s2; uTys nb1 t1 nb2 t2 } + = do { coi_s <- uTys nb1 s1 nb2 s2; coi_t <- uTys nb1 t1 nb2 t2 + ; return $ mkAppTyCoI s1 coi_s t1 coi_t } + + -- One or both outermost constructors are type family applications. + -- If we can normalise them away, proceed as usual; otherwise, we + -- need to defer unification by generating a wanted equality constraint. + go1 outer ty1 ty2 + | ty1_is_fun || ty2_is_fun + = do { (coi1, ty1') <- if ty1_is_fun then tcNormaliseFamInst ty1 + else return (IdCo, ty1) + ; (coi2, ty2') <- if ty2_is_fun then tcNormaliseFamInst ty2 + else return (IdCo, ty2) + ; coi <- if isOpenSynTyConApp ty1' || isOpenSynTyConApp ty2' + then do { -- One type family app can't be reduced yet + -- => defer + ; ty1'' <- zonkTcType ty1' + ; ty2'' <- zonkTcType ty2' + ; if tcEqType ty1'' ty2'' + then return IdCo + else -- see [Deferred Unification] + defer_unification outer False orig_ty1 orig_ty2 + } + else -- unification can proceed + go outer ty1' ty2' + ; return $ coi1 `mkTransCoI` coi `mkTransCoI` (mkSymCoI coi2) + } + where + ty1_is_fun = isOpenSynTyConApp ty1 + ty2_is_fun = isOpenSynTyConApp ty2 + -- Anything else fails + go1 outer _ _ = unifyMisMatch outer False orig_ty1 orig_ty2 - -- Anything else fails - go outer _ _ = unifyMisMatch outer False orig_ty1 orig_ty2 ---------- uPred outer nb1 (IParam n1 t1) nb2 (IParam n2 t2) - | n1 == n2 = uTys nb1 t1 nb2 t2 + | n1 == n2 = + do { coi <- uTys nb1 t1 nb2 t2 + ; return $ mkIParamPredCoI n1 coi + } 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 + | c1 == c2 = + do { cois <- uTys_s nb1 tys1 nb2 tys2 -- Guaranteed equal lengths because the kinds check + ; return $ mkClassPPredCoI c1 tys1 cois + } 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 [] nb2 [] = return [] +uPreds outer nb1 (p1:ps1) nb2 (p2:ps2) = + do { coi <- uPred outer nb1 p1 nb2 p2 + ; cois <- uPreds outer nb1 ps1 nb2 ps2 + ; return (coi:cois) + } uPreds outer nb1 ps1 nb2 ps2 = panic "uPreds" \end{code} -Note [Tycon app] +Note [TyCon app] ~~~~~~~~~~~~~~~~ When we find two TyConApps, the argument lists are guaranteed equal length. Reason: intially the kinds of the two types to be unified is @@ -1053,9 +1284,20 @@ the f1,f2 (because it'd absorb the app). If we unify f1:=:f2 first, which we do, that ensures that f1,f2 have the same kind; and that means a1,a2 have the same kind. And now the argument repeats. +Note [OpenSynTyCon app] +~~~~~~~~~~~~~~~~~~~~~~~ +Given + + type family T a :: * -> * -Notes on synonyms -~~~~~~~~~~~~~~~~~ +the two types (T () a) and (T () Int) must unify, even if there are +no type instances for T at all. Should we just turn them into an +equality (T () a ~ T () Int)? I don't think so. We currently try to +eagerly unify everything we can before generating equalities; otherwise, +we could turn the unification of [Int] with [a] into an equality, too. + +Note [Unification and synonyms] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ If you are tempted to make a short cut on synonyms, as in this pseudocode... @@ -1119,12 +1361,12 @@ back into @uTys@ if it turns out that the variable is already bound. \begin{code} uVar :: Outer - -> Bool -- False => tyvar is the "expected" - -- True => ty is the "expected" thing + -> SwapFlag -- False => tyvar is the "actual" (ty is "expected") + -- True => ty is the "actual" (tyvar is "expected") -> TcTyVar -> InBox -- True <=> definitely no boxes in t2 -> TcTauType -> TcTauType -- printing and real versions - -> TcM () + -> TcM CoercionI uVar outer swapped tv1 nb2 ps_ty2 ty2 = do { let expansion | showSDoc (ppr ty2) == showSDoc (ppr ps_ty2) = empty @@ -1144,10 +1386,10 @@ uVar outer swapped tv1 nb2 ps_ty2 ty2 ---------------- uUnfilledVar :: Outer - -> Bool -- Args are swapped + -> SwapFlag -> TcTyVar -> TcTyVarDetails -- Tyvar 1 -> TcTauType -> TcTauType -- Type 2 - -> TcM () + -> TcM CoercionI -- Invariant: tyvar 1 is not unified with anything uUnfilledVar outer swapped tv1 details1 ps_ty2 ty2 @@ -1161,34 +1403,109 @@ uUnfilledVar outer swapped tv1 details1 ps_ty2 (TyVarTy tv2) MetaTv BoxTv ref1 -- A boxy type variable meets itself; -- this is box-meets-box, so fill in with a tau-type -> do { tau_tv <- tcInstTyVar tv1 - ; updateMeta tv1 ref1 (mkTyVarTy tau_tv) } - other -> returnM () -- No-op + ; updateMeta tv1 ref1 (mkTyVarTy tau_tv) + ; return IdCo + } + other -> returnM IdCo -- No-op - -- Distinct type variables - | otherwise + | otherwise -- Distinct type variables = do { lookup2 <- lookupTcTyVar tv2 ; case lookup2 of - IndirectTv ty2' -> uUnfilledVar outer swapped tv1 details1 ty2' ty2' + IndirectTv ty2' -> uUnfilledVar outer swapped tv1 details1 ty2' ty2' DoneTv details2 -> uUnfilledVars outer swapped tv1 details1 tv2 details2 } -uUnfilledVar outer swapped tv1 details1 ps_ty2 non_var_ty2 -- ty2 is not a type variable - = case details1 of - MetaTv (SigTv _) ref1 -> mis_match -- Can't update a skolem with a non-type-variable - MetaTv info ref1 -> uMetaVar swapped tv1 info ref1 ps_ty2 non_var_ty2 - skolem_details -> mis_match +uUnfilledVar outer swapped tv1 details1 ps_ty2 non_var_ty2 + = -- ty2 is not a type variable + case details1 of + MetaTv (SigTv _) _ -> rigid_variable + MetaTv info ref1 -> + uMetaVar outer swapped tv1 info ref1 ps_ty2 non_var_ty2 + SkolemTv _ -> rigid_variable where - mis_match = unifyMisMatch outer swapped (TyVarTy tv1) ps_ty2 + rigid_variable + | isOpenSynTyConApp non_var_ty2 + = -- 'non_var_ty2's outermost constructor is a type family, + -- which we may may be able to normalise + do { (coi2, ty2') <- tcNormaliseFamInst non_var_ty2 + ; case coi2 of + IdCo -> -- no progress, but maybe after other instantiations + defer_unification outer swapped (TyVarTy tv1) ps_ty2 + ACo co -> -- progress: so lets try again + do { traceTc $ + ppr co <+> text "::"<+> ppr non_var_ty2 <+> text "~" <+> + ppr ty2' + ; coi <- uUnfilledVar outer swapped tv1 details1 ps_ty2 ty2' + ; let coi2' = (if swapped then id else mkSymCoI) coi2 + ; return $ coi2' `mkTransCoI` coi + } + } + | SkolemTv RuntimeUnkSkol <- details1 + -- runtime unknown will never match + = unifyMisMatch outer swapped (TyVarTy tv1) ps_ty2 + | otherwise -- defer as a given equality may still resolve this + = defer_unification outer swapped (TyVarTy tv1) ps_ty2 +\end{code} + +Note [Deferred Unification] +~~~~~~~~~~~~~~~~~~~~ +We may encounter a unification ty1 = ty2 that cannot be performed syntactically, +and yet its consistency is undetermined. Previously, there was no way to still +make it consistent. So a mismatch error was issued. + +Now these unfications are deferred until constraint simplification, where type +family instances and given equations may (or may not) establish the consistency. +Deferred unifications are of the form + F ... ~ ... +or x ~ ... +where F is a type function and x is a type variable. +E.g. + id :: x ~ y => x -> y + id e = e + +involves the unfication x = y. It is deferred until we bring into account the +context x ~ y to establish that it holds. + +If available, we defer original types (rather than those where closed type +synonyms have already been expanded via tcCoreView). This is, as usual, to +improve error messages. + +We need to both 'unBox' and zonk deferred types. We need to unBox as +functions, such as TcExpr.tcMonoExpr promise to fill boxes in the expected +type. We need to zonk as the types go into the kind of the coercion variable +`cotv' and those are not zonked in Inst.zonkInst. (Maybe it would be better +to zonk in zonInst instead. Would that be sufficient?) + +\begin{code} +defer_unification :: Bool -- pop innermost context? + -> SwapFlag + -> TcType + -> TcType + -> TcM CoercionI +defer_unification outer True ty1 ty2 + = defer_unification outer False ty2 ty1 +defer_unification outer False ty1 ty2 + = do { ty1' <- unBox ty1 >>= zonkTcType -- unbox *and* zonk.. + ; ty2' <- unBox ty2 >>= zonkTcType -- ..see preceding note + ; traceTc $ text "deferring:" <+> ppr ty1 <+> text "~" <+> ppr ty2 + ; cotv <- newMetaCoVar ty1' ty2' + -- put ty1 ~ ty2 in LIE + -- Left means "wanted" + ; inst <- (if outer then popErrCtxt else id) $ + mkEqInst (EqPred ty1' ty2') (Left cotv) + ; extendLIE inst + ; return $ ACo $ TyVarTy cotv } ---------------- -uMetaVar :: Bool +uMetaVar :: Bool -- pop innermost context? + -> SwapFlag -> TcTyVar -> BoxInfo -> IORef MetaDetails -> TcType -> TcType - -> TcM () + -> TcM CoercionI -- tv1 is an un-filled-in meta type variable (maybe boxy, maybe tau) -- ty2 is not a type variable -uMetaVar swapped tv1 BoxTv ref1 ps_ty2 non_var_ty2 +uMetaVar outer swapped tv1 BoxTv ref1 ps_ty2 non_var_ty2 = -- tv1 is a BoxTv. So we must unbox ty2, to ensure -- that any boxes in ty2 are filled with monotypes -- @@ -1202,53 +1519,64 @@ uMetaVar swapped tv1 BoxTv ref1 ps_ty2 non_var_ty2 ; case meta_details of Indirect ty -> WARN( True, ppr tv1 <+> ppr ty ) return () -- This really should *not* happen - Flexi -> return () + Flexi -> return () #endif - ; checkUpdateMeta swapped tv1 ref1 final_ty } - -uMetaVar swapped tv1 info1 ref1 ps_ty2 non_var_ty2 - = do { final_ty <- checkTauTvUpdate tv1 ps_ty2 -- Occurs check + monotype check - ; checkUpdateMeta swapped tv1 ref1 final_ty } + ; checkUpdateMeta swapped tv1 ref1 final_ty + ; return IdCo + } + +uMetaVar outer swapped tv1 info1 ref1 ps_ty2 non_var_ty2 + = do { -- Occurs check + monotype check + ; mb_final_ty <- checkTauTvUpdate tv1 ps_ty2 + ; case mb_final_ty of + Nothing -> -- tv1 occured in type family parameter + defer_unification outer swapped (mkTyVarTy tv1) ps_ty2 + Just final_ty -> + do { checkUpdateMeta swapped tv1 ref1 final_ty + ; return IdCo + } + } ---------------- uUnfilledVars :: Outer - -> Bool -- Args are swapped + -> SwapFlag -> TcTyVar -> TcTyVarDetails -- Tyvar 1 -> TcTyVar -> TcTyVarDetails -- Tyvar 2 - -> TcM () + -> TcM CoercionI -- Invarant: The type variables are distinct, -- Neither is filled in yet -- They might be boxy or not uUnfilledVars outer swapped tv1 (SkolemTv _) tv2 (SkolemTv _) - = unifyMisMatch outer swapped (mkTyVarTy tv1) (mkTyVarTy tv2) + = -- see [Deferred Unification] + defer_unification outer swapped (mkTyVarTy tv1) (mkTyVarTy tv2) uUnfilledVars outer swapped tv1 (MetaTv info1 ref1) tv2 (SkolemTv _) - = checkUpdateMeta swapped tv1 ref1 (mkTyVarTy tv2) + = checkUpdateMeta swapped tv1 ref1 (mkTyVarTy tv2) >> return IdCo uUnfilledVars outer swapped tv1 (SkolemTv _) tv2 (MetaTv info2 ref2) - = checkUpdateMeta (not swapped) tv2 ref2 (mkTyVarTy tv1) + = checkUpdateMeta (not swapped) tv2 ref2 (mkTyVarTy tv1) >> return IdCo -- ToDo: this function seems too long for what it acutally does! uUnfilledVars outer swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2) = case (info1, info2) of - (BoxTv, BoxTv) -> box_meets_box + (BoxTv, BoxTv) -> box_meets_box >> return IdCo -- If a box meets a TauTv, but the fomer has the smaller kind -- then we must create a fresh TauTv with the smaller kind - (_, BoxTv) | k1_sub_k2 -> update_tv2 - | otherwise -> box_meets_box - (BoxTv, _ ) | k2_sub_k1 -> update_tv1 - | otherwise -> box_meets_box + (_, BoxTv) | k1_sub_k2 -> update_tv2 >> return IdCo + | otherwise -> box_meets_box >> return IdCo + (BoxTv, _ ) | k2_sub_k1 -> update_tv1 >> return IdCo + | otherwise -> box_meets_box >> return IdCo -- Avoid SigTvs if poss - (SigTv _, _ ) | k1_sub_k2 -> update_tv2 - (_, SigTv _) | k2_sub_k1 -> update_tv1 + (SigTv _, _ ) | k1_sub_k2 -> update_tv2 >> return IdCo + (_, SigTv _) | k2_sub_k1 -> update_tv1 >> return IdCo (_, _) | k1_sub_k2 -> if k2_sub_k1 && nicer_to_update_tv1 - then update_tv1 -- Same kinds - else update_tv2 - | k2_sub_k1 -> update_tv1 - | otherwise -> kind_err + then update_tv1 >> return IdCo -- Same kinds + else update_tv2 >> return IdCo + | k2_sub_k1 -> update_tv1 >> return IdCo + | otherwise -> kind_err >> return IdCo -- Update the variable with least kind info -- See notes on type inference in Kind.lhs @@ -1284,146 +1612,8 @@ uUnfilledVars outer swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2) -- Try to update sys-y type variables in preference to ones -- gotten (say) by instantiating a polymorphic function with -- a user-written type sig - ----------------- -checkUpdateMeta :: Bool -> TcTyVar -> IORef MetaDetails -> TcType -> TcM () --- Update tv1, which is flexi; occurs check is alrady done --- The 'check' version does a kind check too --- We do a sub-kind check here: we might unify (a b) with (c d) --- where b::*->* and d::*; this should fail - -checkUpdateMeta swapped tv1 ref1 ty2 - = do { checkKinds swapped tv1 ty2 - ; updateMeta tv1 ref1 ty2 } - -updateMeta :: TcTyVar -> IORef MetaDetails -> TcType -> TcM () -updateMeta tv1 ref1 ty2 - = ASSERT( isMetaTyVar tv1 ) - ASSERT( isBoxyTyVar tv1 || isTauTy ty2 ) - do { ASSERTM2( do { details <- readMetaTyVar tv1; return (isFlexi details) }, ppr tv1 ) - ; traceTc (text "updateMeta" <+> ppr tv1 <+> text ":=" <+> ppr ty2) - ; writeMutVar ref1 (Indirect ty2) } - ----------------- -checkKinds swapped tv1 ty2 --- We're about to unify a type variable tv1 with a non-tyvar-type ty2. --- ty2 has been zonked at this stage, which ensures that --- its kind has as much boxity information visible as possible. - | tk2 `isSubKind` tk1 = returnM () - - | otherwise - -- Either the kinds aren't compatible - -- (can happen if we unify (a b) with (c d)) - -- or we are unifying a lifted type variable with an - -- unlifted type: e.g. (id 3#) is illegal - = addErrCtxtM (unifyKindCtxt swapped tv1 ty2) $ - unifyKindMisMatch k1 k2 - where - (k1,k2) | swapped = (tk2,tk1) - | otherwise = (tk1,tk2) - tk1 = tyVarKind tv1 - tk2 = typeKind ty2 - ----------------- -checkTauTvUpdate :: TcTyVar -> TcType -> TcM TcType --- (checkTauTvUpdate tv ty) --- We are about to update the TauTv tv with ty. --- Check (a) that tv doesn't occur in ty (occurs check) --- (b) that ty is a monotype --- Furthermore, in the interest of (b), if you find an --- empty box (BoxTv that is Flexi), fill it in with a TauTv --- --- Returns the (non-boxy) type to update the type variable with, or fails - -checkTauTvUpdate orig_tv orig_ty - = go orig_ty - where - go (TyConApp tc tys) - | isSynTyCon tc = go_syn tc tys - | otherwise = do { tys' <- mappM go tys; return (TyConApp tc tys') } - go (NoteTy _ ty2) = go ty2 -- Discard free-tyvar annotations - go (PredTy p) = do { p' <- go_pred p; return (PredTy p') } - go (FunTy arg res) = do { arg' <- go arg; res' <- go res; return (FunTy arg' res') } - go (AppTy fun arg) = do { fun' <- go fun; arg' <- go arg; return (mkAppTy fun' arg') } - -- NB the mkAppTy; we might have instantiated a - -- type variable to a type constructor, so we need - -- to pull the TyConApp to the top. - go (ForAllTy tv ty) = notMonoType orig_ty -- (b) - - go (TyVarTy tv) - | orig_tv == tv = occurCheck tv orig_ty -- (a) - | isTcTyVar tv = go_tyvar tv (tcTyVarDetails tv) - | otherwise = return (TyVarTy tv) - -- Ordinary (non Tc) tyvars - -- occur inside quantified types - - go_pred (ClassP c tys) = do { tys' <- mapM go tys; return (ClassP c tys') } - go_pred (IParam n ty) = do { ty' <- go ty; return (IParam n ty') } - go_pred (EqPred t1 t2) = do { t1' <- go t1; t2' <- go t2; return (EqPred t1' t2') } - - go_tyvar tv (SkolemTv _) = return (TyVarTy tv) - go_tyvar tv (MetaTv box ref) - = do { cts <- readMutVar ref - ; case cts of - Indirect ty -> go ty - Flexi -> case box of - BoxTv -> fillBoxWithTau tv ref - other -> return (TyVarTy tv) - } - - -- go_syn is called for synonyms only - -- See Note [Type synonyms and the occur check] - go_syn tc tys - | not (isTauTyCon tc) - = notMonoType orig_ty -- (b) again - | otherwise - = do { (msgs, mb_tys') <- tryTc (mapM go tys) - ; case mb_tys' of - Just tys' -> return (TyConApp tc tys') - -- Retain the synonym (the common case) - 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 - } - -fillBoxWithTau :: BoxyTyVar -> IORef MetaDetails -> TcM TcType --- (fillBoxWithTau tv ref) fills ref with a freshly allocated --- tau-type meta-variable, whose print-name is the same as tv --- Choosing the same name is good: when we instantiate a function --- we allocate boxy tyvars with the same print-name as the quantified --- tyvar; and then we often fill the box with a tau-tyvar, and again --- we want to choose the same name. -fillBoxWithTau tv ref - = do { tv' <- tcInstTyVar tv -- Do not gratuitously forget - ; let tau = mkTyVarTy tv' -- name of the type variable - ; writeMutVar ref (Indirect tau) - ; return tau } \end{code} -Note [Type synonyms and the occur check] -~~~~~~~~~~~~~~~~~~~~ -Basically we want to update tv1 := ps_ty2 -because ps_ty2 has type-synonym info, which improves later error messages - -But consider - type A a = () - - f :: (A a -> a -> ()) -> () - f = \ _ -> () - - x :: () - x = f (\ x p -> p x) - -In the application (p x), we try to match "t" with "A t". If we go -ahead and bind t to A t (= ps_ty2), we'll lead the type checker into -an infinite loop later. -But we should not reject the program, because A t = (). -Rather, we should bind t to () (= non_var_ty2). - \begin{code} refineBox :: TcType -> TcM TcType -- Unbox the outer box of a boxy type (if any) @@ -1431,7 +1621,7 @@ refineBox ty@(TyVarTy box_tv) | isMetaTyVar box_tv = do { cts <- readMetaTyVar box_tv ; case cts of - Flexi -> return ty + Flexi -> return ty Indirect ty -> return ty } refineBox other_ty = return other_ty @@ -1443,7 +1633,7 @@ refineBoxToTau ty@(TyVarTy box_tv) , MetaTv BoxTv ref <- tcTyVarDetails box_tv = do { cts <- readMutVar ref ; case cts of - Flexi -> fillBoxWithTau box_tv ref + Flexi -> fillBoxWithTau box_tv ref Indirect ty -> return ty } refineBoxToTau other_ty = return other_ty @@ -1483,7 +1673,7 @@ unBox (TyVarTy tv) , MetaTv BoxTv ref <- tcTyVarDetails tv -- NB: non-TcTyVars are possible = do { cts <- readMutVar ref -- under nested quantifiers ; case cts of - Flexi -> fillBoxWithTau tv ref + Flexi -> fillBoxWithTau tv ref Indirect ty -> do { non_boxy_ty <- unBox ty ; if isTauTy non_boxy_ty then return non_boxy_ty @@ -1561,99 +1751,11 @@ unifyForAllCtxt tvs phi1 phi2 env 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 - where - msg = (env2, ptext SLIT("When matching the kinds of") <+> - sep [quotes pp_expected <+> ptext SLIT("and"), quotes pp_actual]) - - (pp_expected, pp_actual) | swapped = (pp2, pp1) - | otherwise = (pp1, pp2) - (env1, tv1') = tidyOpenTyVar tidy_env tv1 - (env2, ty2') = tidyOpenType env1 ty2 - pp1 = ppr tv1' <+> dcolon <+> ppr (tyVarKind tv1) - pp2 = ppr ty2' <+> dcolon <+> ppr (typeKind ty2) - -unifyMisMatch outer swapped ty1 ty2 - = do { (env, msg) <- if swapped then misMatchMsg ty1 ty2 - else misMatchMsg ty2 ty1 - - -- This is the whole point of the 'outer' stuff - ; if outer then popErrCtxt (failWithTcM (env, msg)) - 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 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 $$ extra2)]) } - -ppr_ty :: TidyEnv -> TcType -> TcType -> TcM (TidyEnv, SDoc, SDoc) -ppr_ty env ty other_ty - = do { ty' <- zonkTcType ty - ; let (env1, tidy_ty) = tidyOpenType env ty' - ; (env2, extra) <- ppr_extra env1 ty' other_ty - ; return (env2, quotes (ppr tidy_ty), extra) } - --- (ppr_extra env ty other_ty) shows extra info about 'ty' -ppr_extra env (TyVarTy tv) other_ty - | isSkolemTyVar tv || isSigTyVar tv - = return (env1, pprSkolTvBinding tv1) - where - (env1, tv1) = tidySkolemTyVar env tv - -ppr_extra env (TyConApp tc1 _) (TyConApp tc2 _) - | getOccName tc1 == getOccName tc2 - = -- This case helps with messages that would otherwise say - -- Could not match 'T' does not match 'M.T' - -- which is not helpful - do { this_mod <- getModule - ; return (env, quotes (ppr tc1) <+> ptext SLIT("is defined in") <+> mk_mod this_mod) } - where - tc_mod = nameModule (getName tc1) - tc_pkg = modulePackageId tc_mod - mk_mod this_mod - | tc_mod == this_mod = ptext SLIT("this module") - | otherwise = ptext SLIT("module") <+> quotes (ppr tc_mod) <+> mk_pkg this_mod - mk_pkg this_mod - | tc_pkg == modulePackageId this_mod = empty - | otherwise = ptext SLIT("from package") <+> quotes (ppr tc_pkg) - -ppr_extra env ty other_ty = return (env, empty) -- Normal case - ------------------------ -notMonoType ty - = do { ty' <- zonkTcType ty - ; env0 <- tcInitTidyEnv - ; let (env1, tidy_ty) = tidyOpenType env0 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 - ; let (env1, tidy_tyvar) = tidyOpenTyVar env0 tyvar - (env2, tidy_ty) = tidyOpenType env1 ty' - extra = sep [ppr tidy_tyvar, char '=', ppr tidy_ty] - ; failWithTcM (env2, hang msg 2 extra) } - where - msg = ptext SLIT("Occurs check: cannot construct the infinite type:") +unifyMisMatch outer swapped ty1 ty2 + | 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} @@ -1703,7 +1805,7 @@ uUnboundKVar swapped kv1 k2@(TyVarTy kv2) = do { mb_k2 <- readKindVar kv2 ; case mb_k2 of Indirect k2 -> uUnboundKVar swapped kv1 k2 - Flexi -> writeKindVar kv1 k2 } + Flexi -> writeKindVar kv1 k2 } uUnboundKVar swapped kv1 non_var_k2 = do { k2' <- zonkTcKind non_var_k2 @@ -1753,17 +1855,6 @@ kindSimpleKind orig_swapped orig_kind kindOccurCheckErr tyvar ty = hang (ptext SLIT("Occurs check: cannot construct the infinite kind:")) 2 (sep [ppr tyvar, char '=', ppr ty]) - -unifyKindMisMatch ty1 ty2 - = zonkTcKind ty1 `thenM` \ ty1' -> - zonkTcKind ty2 `thenM` \ ty2' -> - let - msg = hang (ptext SLIT("Couldn't match kind")) - 2 (sep [quotes (ppr ty1'), - ptext SLIT("against"), - quotes (ppr ty2')]) - in - failWithTc msg \end{code} \begin{code} @@ -1774,7 +1865,7 @@ unifyFunKind (TyVarTy kvar) = readKindVar kvar `thenM` \ maybe_kind -> case maybe_kind of Indirect fun_kind -> unifyFunKind fun_kind - Flexi -> + Flexi -> do { arg_kind <- newKindVar ; res_kind <- newKindVar ; writeKindVar kvar (mkArrowKind arg_kind res_kind)