X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcUnify.lhs;h=67cdf20bd507d129a373ccf4c9fea55e4308e001;hp=18cf1bed08fcbd5c363b0f066319b03563c5ac78;hb=bfe55fb767d566b5105c5584f698af1dd4a57346;hpb=393b4f6cbd7a3581975c3530bf210219b0f65939 diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs index 18cf1be..67cdf20 100644 --- a/compiler/typecheck/TcUnify.lhs +++ b/compiler/typecheck/TcUnify.lhs @@ -10,7 +10,7 @@ Type subsumption and unification -- 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/CodingStyle#Warnings +-- http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings -- for details module TcUnify ( @@ -22,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 @@ -191,8 +191,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 :: * @@ -203,14 +204,26 @@ 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 + ; 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 +232,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 +280,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 +314,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} @@ -858,8 +926,8 @@ 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 @@ -1126,9 +1194,9 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2 -- 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 tcNormalizeFamInst ty1 + = do { (coi1, ty1') <- if ty1_is_fun then tcNormaliseFamInst ty1 else return (IdCo, ty1) - ; (coi2, ty2') <- if ty2_is_fun then tcNormalizeFamInst ty2 + ; (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 @@ -1318,18 +1386,16 @@ uUnfilledVar outer swapped tv1 details1 ps_ty2 (TyVarTy tv2) 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 -> - do { uMetaVar swapped tv1 info ref1 ps_ty2 non_var_ty2 - ; return IdCo - } - SkolemTv _ -> rigid_variable + MetaTv (SigTv _) _ -> rigid_variable + MetaTv info ref1 -> + uMetaVar outer swapped tv1 info ref1 ps_ty2 non_var_ty2 + SkolemTv _ -> rigid_variable where 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') <- tcNormalizeFamInst non_var_ty2 + 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 @@ -1390,7 +1456,7 @@ 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 <- newMetaTyVar TauTv (mkCoKind ty1' ty2') + ; cotv <- newMetaCoVar ty1' ty2' -- put ty1 ~ ty2 in LIE -- Left means "wanted" ; inst <- (if outer then popErrCtxt else id) $ @@ -1399,14 +1465,15 @@ defer_unification outer False ty1 ty2 ; return $ ACo $ TyVarTy cotv } ---------------- -uMetaVar :: SwapFlag +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 -- @@ -1422,11 +1489,21 @@ uMetaVar swapped tv1 BoxTv ref1 ps_ty2 non_var_ty2 return () -- This really should *not* happen Flexi -> return () #endif - ; checkUpdateMeta swapped tv1 ref1 final_ty } + ; checkUpdateMeta swapped tv1 ref1 final_ty + ; return IdCo + } -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 } +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 @@ -1503,148 +1580,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 :: SwapFlag - -> 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) @@ -1782,21 +1719,7 @@ 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 ty2 ty1 else misMatchMsg ty1 ty2 @@ -1805,31 +1728,6 @@ unifyMisMatch outer swapped ty1 ty2 ; if outer then popErrCtxt (failWithTcM (env, msg)) else failWithTcM (env, msg) } - ------------------------ -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:") \end{code} @@ -1929,17 +1827,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}