X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcUnify.lhs;h=e5e16fc392fbe49fe5ccc9e0fed9e149d79a4e22;hp=ecee5ac4e8a130a5ee7e842ab0a8127fe0ab4104;hb=9a4ef343a46e823bcf949af8501c13cc8ca98fb1;hpb=bb7ffa1642e2110e26e1243c42a8a24adafa985d diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs index ecee5ac..e5e16fc 100644 --- a/compiler/typecheck/TcUnify.lhs +++ b/compiler/typecheck/TcUnify.lhs @@ -14,7 +14,6 @@ module TcUnify ( -- Various unifications unifyType, unifyTypeList, unifyTheta, unifyKind, unifyKinds, unifyFunKind, - checkExpectedKind, preSubType, boxyMatchTypes, -------------------------------- @@ -79,7 +78,9 @@ tcInfer tc_infer = withBox openTypeKind tc_infer subFunTys :: SDoc -- Something like "The function f has 3 arguments" -- or "The abstraction (\x.e) takes 1 argument" -> Arity -- Expected # of args - -> BoxyRhoType -- res_ty + -> BoxySigmaType -- res_ty + -> Maybe UserTypeCtxt -- Whether res_ty arises from a user signature + -- Only relevant if we encounter a sigma-type -> ([BoxySigmaType] -> BoxyRhoType -> TcM a) -> TcM (HsWrapper, a) -- Attempt to decompse res_ty to have enough top-level arrows to @@ -108,7 +109,7 @@ subFunTys :: SDoc -- Something like "The function f has 3 arguments" -} -subFunTys error_herald n_pats res_ty thing_inside +subFunTys error_herald n_pats res_ty mb_ctxt thing_inside = loop n_pats [] res_ty where -- In 'loop', the parameter 'arg_tys' accumulates @@ -121,8 +122,8 @@ subFunTys error_herald n_pats res_ty thing_inside | 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' -> - loop n args_so_far res_ty' + = do { (gen_fn, (co_fn, res)) <- tcGen res_ty emptyVarSet mb_ctxt $ \ _ res_ty -> + loop n args_so_far res_ty ; return (gen_fn <.> co_fn, res) } loop 0 args_so_far res_ty @@ -609,7 +610,10 @@ boxy_match tmpl_tvs orig_tmpl_ty boxy_tvs orig_boxy_ty subst Nothing -> orig_boxy_ty Just ty -> ty `boxyLub` orig_boxy_ty - go _ (TyVarTy tv) | isMetaTyVar tv + go _ (TyVarTy tv) | isTcTyVar tv && isMetaTyVar tv + -- NB: A TyVar (not TcTyVar) is possible here, representing + -- a skolem, because in this pure boxy_match function + -- we don't instantiate foralls to TcTyVars; cf Trac #2714 = subst -- Don't fail if the template has more info than the target! -- Otherwise, with tmpl_tvs = [a], matching (a -> Int) ~ (Bool -> beta) -- would fail to instantiate 'a', because the meta-type-variable @@ -768,7 +772,7 @@ tc_sub1 orig act_sty act_ty exp_ib exp_sty exp_ty if exp_ib then -- SKOL does not apply if exp_ty is inside a box defer_to_boxy_matching orig act_sty act_ty exp_ib exp_sty exp_ty else do - { (gen_fn, co_fn) <- tcGen exp_ty act_tvs $ \ _ body_exp_ty -> + { (gen_fn, co_fn) <- tcGen exp_ty act_tvs Nothing $ \ _ body_exp_ty -> tc_sub orig act_sty act_ty False body_exp_ty body_exp_ty ; return (gen_fn <.> co_fn) } } @@ -894,26 +898,21 @@ wrapFunResCoercion arg_tys co_fn_res %************************************************************************ \begin{code} -tcGen :: BoxySigmaType -- expected_ty - -> TcTyVarSet -- Extra tyvars that the universally - -- quantified tyvars of expected_ty - -- must not be unified +tcGen :: BoxySigmaType -- expected_ty + -> TcTyVarSet -- Extra tyvars that the universally + -- quantified tyvars of expected_ty + -- must not be unified + -> Maybe UserTypeCtxt -- Just ctxt => this polytype arose directly + -- from a user type sig + -- Nothing => a higher order situation -> ([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 - -- If not, the call is a no-op +tcGen expected_ty extra_tvs mb_ctxt thing_inside -- We expect expected_ty to be a forall-type + -- If not, the call is a no-op = 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) -> - 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) - ; return ((forall_tvs, theta, rho_ty), skol_info) }) + ; ((tvs', theta', rho'), skol_info) <- instantiate expected_ty ; when debugIsOn $ traceTc (text "tcGen" <+> vcat [ @@ -924,7 +923,8 @@ tcGen expected_ty extra_tvs thing_inside -- We expect expected_ty to be a text "free_tvs" <+> ppr free_tvs]) -- Type-check the arg and unify with poly type - ; (result, lie) <- getLIE (thing_inside tvs' rho') + ; (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 @@ -951,6 +951,23 @@ tcGen expected_ty extra_tvs thing_inside -- We expect expected_ty to be a ; return (co_fn, result) } where free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs + + instantiate :: TcType -> TcM (([TcTyVar],ThetaType,TcRhoType), SkolemInfo) + instantiate expected_ty + | Just ctxt <- mb_ctxt -- This case split is the wohle reason for mb_ctxt + = do { let skol_info = SigSkol ctxt + ; stuff <- tcInstSigType True skol_info expected_ty + ; return (stuff, skol_info) } + + | otherwise -- 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 + = fixM $ \ ~(_, skol_info) -> + do { stuff@(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) + ; return (stuff, skol_info) } \end{code} @@ -1177,13 +1194,13 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2 go outer _ (PredTy p1) _ (PredTy p2) = uPred outer nb1 p1 nb2 p2 - -- Type constructors must match + -- Non-synonym type constructors must match go _ _ (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] + -- Family synonyms See Note [TyCon app] | con1 == con2 && identicalOpenSynTyConApp = do { cois <- uTys_s nb1 tys1' nb2 tys2' ; return $ mkTyConAppCoI con1 tys1 (replicate n IdCo ++ cois) @@ -1195,6 +1212,29 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2 identicalOpenSynTyConApp = idxTys1 `tcEqTypes` idxTys2 -- See Note [OpenSynTyCon app] + -- If we can reduce a family app => proceed with reduct + -- NB: We use isOpenSynTyCon, not isOpenSynTyConApp as we also must + -- defer oversaturated applications! + go outer sty1 ty1@(TyConApp con1 _) sty2 ty2 + | isOpenSynTyCon con1 + = do { (coi1, ty1') <- tcNormaliseFamInst ty1 + ; case coi1 of + IdCo -> defer -- no reduction, see [Deferred Unification] + _ -> liftM (coi1 `mkTransCoI`) $ go outer sty1 ty1' sty2 ty2 + } + + -- If we can reduce a family app => proceed with reduct + -- NB: We use isOpenSynTyCon, not isOpenSynTyConApp as we also must + -- defer oversaturated applications! + go outer sty1 ty1 sty2 ty2@(TyConApp con2 _) + | isOpenSynTyCon con2 + = do { (coi2, ty2') <- tcNormaliseFamInst ty2 + ; case coi2 of + IdCo -> defer -- no reduction, see [Deferred Unification] + _ -> liftM (`mkTransCoI` mkSymCoI coi2) $ + go outer sty1 ty1 sty2 ty2' + } + -- Functions; just check the two parts go _ _ (FunTy fun1 arg1) _ (FunTy fun2 arg2) = do { coi_l <- uTys nb1 fun1 nb2 fun2 @@ -1220,36 +1260,12 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2 ; 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. - go outer sty1 ty1 sty2 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 sty1 ty1' sty2 ty2' - ; return $ coi1 `mkTransCoI` coi `mkTransCoI` (mkSymCoI coi2) - } - where - ty1_is_fun = isOpenSynTyConApp ty1 - ty2_is_fun = isOpenSynTyConApp ty2 - -- Anything else fails go outer _ _ _ _ = bale_out outer + defer = defer_unification outer False orig_ty1 orig_ty2 + + ---------- uPred :: Outer -> InBox -> PredType -> InBox -> PredType -> TcM CoercionI uPred _ nb1 (IParam n1 t1) nb2 (IParam n2 t2) @@ -1280,8 +1296,8 @@ 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 the same. The only way it can become not the same is when unifying two -AppTys (f1 a1):=:(f2 a2). In that case there can't be a TyConApp in -the f1,f2 (because it'd absorb the app). If we unify f1:=:f2 first, +AppTys (f1 a1)~(f2 a2). In that case there can't be a TyConApp in +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. @@ -1856,7 +1872,7 @@ kindSimpleKind :: Bool -> Kind -> TcM SimpleKind -- (kindSimpleKind True k) returns a simple kind sk such that sk <: k -- If the flag is False, it requires k <: sk -- E.g. kindSimpleKind False ?? = * --- What about (kv -> *) :=: ?? -> * +-- What about (kv -> *) ~ ?? -> * kindSimpleKind orig_swapped orig_kind = go orig_swapped orig_kind where @@ -1904,75 +1920,6 @@ unifyFunKind _ = return Nothing %************************************************************************ %* * - Checking kinds -%* * -%************************************************************************ - ---------------------------- --- We would like to get a decent error message from --- (a) Under-applied type constructors --- f :: (Maybe, Maybe) --- (b) Over-applied type constructors --- f :: Int x -> Int x --- - -\begin{code} -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 - = return () - | otherwise = do - (_errs, mb_r) <- tryTc (unifyKind exp_kind act_kind) - case mb_r of - Just _ -> return () -- Unification succeeded - Nothing -> do - - -- So there's definitely an error - -- Now to find out what sort - exp_kind <- zonkTcKind exp_kind - act_kind <- zonkTcKind act_kind - - env0 <- tcInitTidyEnv - let (exp_as, _) = splitKindFunTys exp_kind - (act_as, _) = splitKindFunTys act_kind - n_exp_as = length exp_as - n_act_as = length act_as - - (env1, tidy_exp_kind) = tidyKind env0 exp_kind - (env2, tidy_act_kind) = tidyKind env1 act_kind - - err | n_exp_as < n_act_as -- E.g. [Maybe] - = quotes (ppr ty) <+> ptext (sLit "is not applied to enough type arguments") - - -- Now n_exp_as >= n_act_as. In the next two cases, - -- n_exp_as == 0, and hence so is n_act_as - | isLiftedTypeKind exp_kind && isUnliftedTypeKind act_kind - = ptext (sLit "Expecting a lifted type, but") <+> quotes (ppr ty) - <+> ptext (sLit "is unlifted") - - | isUnliftedTypeKind exp_kind && isLiftedTypeKind act_kind - = ptext (sLit "Expecting an unlifted type, but") <+> quotes (ppr ty) - <+> ptext (sLit "is lifted") - - | otherwise -- E.g. Monad [Int] - = ptext (sLit "Kind mis-match") - - more_info = sep [ ptext (sLit "Expected kind") <+> - quotes (pprKind tidy_exp_kind) <> comma, - ptext (sLit "but") <+> quotes (ppr ty) <+> - ptext (sLit "has kind") <+> quotes (pprKind tidy_act_kind)] - - failWithTcM (env2, err $$ more_info) -\end{code} - -%************************************************************************ -%* * \subsection{Checking signature type variables} %* * %************************************************************************ @@ -2024,7 +1971,7 @@ check_sig_tyvars check_sig_tyvars _ [] = return () check_sig_tyvars extra_tvs sig_tvs - = ASSERT( all isSkolemTyVar sig_tvs ) + = ASSERT( all isTcTyVar sig_tvs && all isSkolemTyVar sig_tvs ) do { gbl_tvs <- tcGetGlobalTyVars ; traceTc (text "check_sig_tyvars" <+> (vcat [text "sig_tys" <+> ppr sig_tvs, text "gbl_tvs" <+> ppr gbl_tvs,