X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcUnify.lhs;h=e9f0301b4a6913c8b940fb400623fe2d615c0b05;hp=23cc9e21760724b982b42322863af6001fe1b13b;hb=9da4639011348fb6c318e3cba4b08622f811d9c4;hpb=0065d5ab628975892cea1ec7303f968c3338cbe1 diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs index 23cc9e2..e9f0301 100644 --- a/compiler/typecheck/TcUnify.lhs +++ b/compiler/typecheck/TcUnify.lhs @@ -13,7 +13,7 @@ module TcUnify ( unifyType, unifyTypeList, unifyTheta, unifyKind, unifyKinds, unifyFunKind, checkExpectedKind, - boxySubMatchType, boxyMatchTypes, + preSubType, boxyMatchTypes, -------------------------------- -- Holes @@ -25,51 +25,54 @@ module TcUnify ( #include "HsVersions.h" -import HsSyn ( ExprCoFn(..), idCoercion, isIdCoercion, (<.>) ) +import HsSyn ( HsWrapper(..), idHsWrapper, isIdHsWrapper, (<.>), + mkWpLams, mkWpTyLams, mkWpApps ) import TypeRep ( Type(..), PredType(..) ) import TcMType ( lookupTcTyVar, LookupTyVarResult(..), - tcInstSkolType, newKindVar, newMetaTyVar, - tcInstBoxy, newBoxyTyVar, newBoxyTyVarTys, readFilledBox, + tcInstBoxyTyVar, newKindVar, newMetaTyVar, + newBoxyTyVar, newBoxyTyVarTys, readFilledBox, readMetaTyVar, writeMetaTyVar, newFlexiTyVarTy, - tcInstSkolTyVars, + tcInstSkolTyVars, tcInstTyVar, tcInstSkolType, zonkTcKind, zonkType, zonkTcType, zonkTcTyVarsAndFV, readKindVar, writeKindVar ) import TcSimplify ( tcSimplifyCheck ) import TcEnv ( tcGetGlobalTyVars, findGlobals ) import TcIface ( checkWiredInTyCon ) import TcRnMonad -- TcType, amongst others -import TcType ( TcKind, TcType, TcTyVar, TcTauType, +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, - tyVarsOfType, mkPhiTy, mkTyVarTy, mkPredTy, + tcSplitSigmaTy, tyVarsOfType, mkPhiTy, mkTyVarTy, mkPredTy, typeKind, mkForAllTys, mkAppTy, isBoxyTyVar, + tcView, exactTyVarsOfType, tidyOpenType, tidyOpenTyVar, tidyOpenTyVars, - pprType, tidyKind, tidySkolemTyVar, isSkolemTyVar, tcView, - TvSubst, mkTvSubst, zipTyEnv, substTy, emptyTvSubst, + pprType, tidyKind, tidySkolemTyVar, isSkolemTyVar, isSigTyVar, + TvSubst, mkTvSubst, zipTyEnv, zipOpenTvSubst, emptyTvSubst, + substTy, substTheta, lookupTyVar, extendTvSubst ) -import Kind ( Kind(..), SimpleKind, KindVar, isArgTypeKind, - openTypeKind, liftedTypeKind, mkArrowKind, defaultKind, - isOpenTypeKind, argTypeKind, isLiftedTypeKind, isUnliftedTypeKind, - isSubKind, pprKind, splitKindFunTys ) +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 ( newDicts, instToId ) +import Inst ( newDictBndrsO, instCall, instToId ) import TyCon ( TyCon, tyConArity, tyConTyVars, isSynTyCon ) import TysWiredIn ( listTyCon ) -import Id ( Id, mkSysLocal ) +import Id ( Id ) import Var ( Var, varName, tyVarKind, isTcTyVar, tcTyVarDetails ) -import VarSet ( emptyVarSet, mkVarSet, unitVarSet, unionVarSet, elemVarSet, varSetElems, - extendVarSet, intersectsVarSet ) +import VarSet import VarEnv import Name ( Name, isSystemName ) import ErrUtils ( Message ) import Maybes ( expectJust, isNothing ) import BasicTypes ( Arity ) -import UniqSupply ( uniqsFromSupply ) import Util ( notNull, equalLength ) import Outputable @@ -107,7 +110,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 -- @@ -145,13 +148,13 @@ 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 - = 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 @@ -165,7 +168,7 @@ subFunTys error_herald n_pats res_ty thing_inside 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 res_ty + ; if isNothing mb_unit then bale_out args_so_far else loop n args_so_far (FunTy arg_ty' res_ty') } loop n args_so_far (TyVarTy tv) @@ -175,16 +178,17 @@ subFunTys error_herald n_pats res_ty thing_inside 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" kinds = openTypeKind : take n (repeat argTypeKind) -- Note argTypeKind: the args can have an unboxed type, -- but not an unboxed tuple. - loop n args_so_far res_ty = bale_out args_so_far res_ty + loop n args_so_far res_ty = bale_out args_so_far - bale_out args_so_far res_ty + bale_out args_so_far = do { env0 <- tcInitTidyEnv ; res_ty' <- zonkTcType res_ty ; let (env1, res_ty'') = tidyOpenType env0 res_ty' @@ -266,6 +270,7 @@ boxySplitAppTy orig_ty ; return (fun_ty, arg_ty) } } 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 @@ -333,16 +338,112 @@ withBox kind thing_inside %************************************************************************ \begin{code} +preSubType :: [TcTyVar] -- Quantified type variables + -> TcTyVarSet -- Subset of quantified type variables + -- see Note [Pre-sub boxy] + -> TcType -- The rho-type part; quantified tyvars scopes over this + -> BoxySigmaType -- Matching type from the context + -> TcM [TcType] -- Types to instantiate the tyvars +-- Perform pre-subsumption, and return suitable types +-- to instantiate the quantified type varibles: +-- info from the pre-subsumption, if there is any +-- a boxy type variable otherwise +-- +-- Note [Pre-sub boxy] +-- The 'btvs' are a subset of 'qtvs'. They are the ones we can +-- instantiate to a boxy type variable, because they'll definitely be +-- filled in later. This isn't always the case; sometimes we have type +-- variables mentioned in the context of the type, but not the body; +-- f :: forall a b. C a b => a -> a +-- Then we may land up with an unconstrained 'b', so we want to +-- instantiate it to a monotype (non-boxy) type variable +-- +-- The 'qtvs' that are *neither* fixed by the pre-subsumption, *nor* are in 'btvs', +-- are instantiated to TauTv meta variables. + +preSubType qtvs btvs qty expected_ty + = do { tys <- mapM inst_tv qtvs + ; traceTc (text "preSubType" <+> (ppr qtvs $$ ppr btvs $$ ppr qty $$ ppr expected_ty $$ ppr pre_subst $$ ppr tys)) + ; return tys } + where + pre_subst = boxySubMatchType (mkVarSet qtvs) qty expected_ty + inst_tv tv + | Just boxy_ty <- lookupTyVar pre_subst tv = return boxy_ty + | tv `elemVarSet` btvs = do { tv' <- tcInstBoxyTyVar tv + ; return (mkTyVarTy tv') } + | otherwise = do { tv' <- tcInstTyVar tv + ; return (mkTyVarTy tv') } + boxySubMatchType :: TcTyVarSet -> TcType -- The "template"; the tyvars are skolems -> BoxyRhoType -- Type to match (note a *Rho* type) -> TvSubst -- Substitution of the [TcTyVar] to BoxySigmaTypes +-- boxySubMatchType implements the Pre-subsumption judgement, in Fig 5 of the paper +-- "Boxy types: inference for higher rank types and impredicativity" + +boxySubMatchType tmpl_tvs tmpl_ty boxy_ty + = go tmpl_tvs tmpl_ty emptyVarSet boxy_ty + where + go t_tvs t_ty b_tvs b_ty + | Just t_ty' <- tcView t_ty = go t_tvs t_ty' b_tvs b_ty + | Just b_ty' <- tcView b_ty = go t_tvs t_ty b_tvs b_ty' + + go t_tvs (TyVarTy _) b_tvs b_ty = emptyTvSubst -- Rule S-ANY; no bindings + -- Rule S-ANY covers (a) type variables and (b) boxy types + -- in the template. Both look like a TyVarTy. + -- See Note [Sub-match] below + + go t_tvs t_ty b_tvs b_ty + | isSigmaTy t_ty, (tvs, _, t_tau) <- tcSplitSigmaTy t_ty + = go (t_tvs `delVarSetList` tvs) t_tau b_tvs b_ty -- Rule S-SPEC + -- Under a forall on the left, if there is shadowing, + -- do not bind! Hence the delVarSetList. + | isSigmaTy b_ty, (tvs, _, b_tau) <- tcSplitSigmaTy b_ty + = go t_tvs t_ty (extendVarSetList b_tvs tvs) b_tau -- Rule S-SKOL + -- Add to the variables we must not bind to + -- NB: it's *important* to discard the theta part. Otherwise + -- consider (forall a. Eq a => a -> b) ~<~ (Int -> Int -> Bool) + -- and end up with a completely bogus binding (b |-> Bool), by lining + -- up the (Eq a) with the Int, whereas it should be (b |-> (Int->Bool)). + -- This pre-subsumption stuff can return too few bindings, but it + -- must *never* return bogus info. + + go t_tvs (FunTy arg1 res1) b_tvs (FunTy arg2 res2) -- Rule S-FUN + = boxy_match t_tvs arg1 b_tvs arg2 (go t_tvs res1 b_tvs res2) + -- Match the args, and sub-match the results + + go t_tvs t_ty b_tvs b_ty = boxy_match t_tvs t_ty b_tvs b_ty emptyTvSubst + -- Otherwise defer to boxy matching + -- This covers TyConApp, AppTy, PredTy +\end{code} + +Note [Sub-match] +~~~~~~~~~~~~~~~~ +Consider this + head :: [a] -> a + |- head xs : +We will do a boxySubMatchType between a ~ +But we *don't* want to match [a |-> ] because + (a) The box should be filled in with a rho-type, but + but the returned substitution maps TyVars to boxy + *sigma* types + (b) In any case, the right final answer might be *either* + instantiate 'a' with a rho-type or a sigma type + head xs : Int vs head xs : forall b. b->b +So the matcher MUST NOT make a choice here. In general, we only +bind a template type variable in boxyMatchType, not in boxySubMatchType. + + +\begin{code} boxyMatchTypes :: TcTyVarSet -> [TcType] -- The "template"; the tyvars are skolems -> [BoxySigmaType] -- Type to match -> TvSubst -- Substitution of the [TcTyVar] to BoxySigmaTypes +-- boxyMatchTypes implements the Pre-matching judgement, in Fig 5 of the paper +-- "Boxy types: inference for higher rank types and impredicativity" + -- Find a *boxy* substitution that makes the template look as much -- like the BoxySigmaType as possible. -- It's always ok to return an empty substitution; @@ -351,57 +452,10 @@ boxyMatchTypes -- NB1: This is a pure, non-monadic function. -- It does no unification, and cannot fail -- --- Note [Matching kinds] --- The target type might legitimately not be a sub-kind of template. --- For example, suppose the target is simply a box with an OpenTypeKind, --- and the template is a type variable with LiftedTypeKind. --- Then it's ok (because the target type will later be refined). --- We simply don't bind the template type variable. --- --- It might also be that the kind mis-match is an error. For example, --- suppose we match the template (a -> Int) against (Int# -> Int), --- where the template type variable 'a' has LiftedTypeKind. This --- matching function does not fail; it simply doesn't bind the template. --- Later stuff will fail. --- -- Precondition: the arg lengths are equal --- Precondition: none of the template type variables appear in the [BoxySigmaType] --- Precondition: any nested quantifiers in either type differ from --- the template type variables passed as arguments +-- Precondition: none of the template type variables appear anywhere in the [BoxySigmaType] -- --- Note [Sub-match] --- ~~~~~~~~~~~~~~~~ --- Consider this --- head :: [a] -> a --- |- head xs : --- We will do a boxySubMatchType between a ~ --- But we *don't* want to match [a |-> ] because --- (a) The box should be filled in with a rho-type, but --- but the returned substitution maps TyVars to boxy *sigma* --- types --- (b) In any case, the right final answer might be *either* --- instantiate 'a' with a rho-type or a sigma type --- head xs : Int vs head xs : forall b. b->b --- So the matcher MUST NOT make a choice here. In general, we only --- bind a template type variable in boxyMatchType, not in boxySubMatchType. -boxySubMatchType tmpl_tvs tmpl_ty boxy_ty - = go tmpl_ty boxy_ty - where - go t_ty b_ty - | Just t_ty' <- tcView t_ty = go t_ty' b_ty - | Just b_ty' <- tcView b_ty = go t_ty b_ty' - - go (FunTy arg1 res1) (FunTy arg2 res2) - = do_match arg1 arg2 (go res1 res2) - -- Match the args, and sub-match the results - - go (TyVarTy _) b_ty = emptyTvSubst -- Do not bind! See Note [Sub-match] - - go t_ty b_ty = do_match t_ty b_ty emptyTvSubst -- Otherwise we are safe to bind - - do_match t_ty b_ty subst = boxy_match tmpl_tvs t_ty emptyVarSet b_ty subst - ------------ boxyMatchTypes tmpl_tvs tmpl_tys boxy_tys = ASSERT( length tmpl_tys == length boxy_tys ) @@ -411,8 +465,11 @@ boxyMatchTypes tmpl_tvs tmpl_tys boxy_tys boxy_match_s tmpl_tvs [] boxy_tvs [] subst = subst boxy_match_s tmpl_tvs (t_ty:t_tys) boxy_tvs (b_ty:b_tys) subst - = boxy_match_s tmpl_tvs t_tys boxy_tvs b_tys $ - boxy_match tmpl_tvs t_ty boxy_tvs b_ty subst + = boxy_match tmpl_tvs t_ty boxy_tvs b_ty $ + boxy_match_s tmpl_tvs t_tys boxy_tvs b_tys subst +boxy_match_s tmpl_tvs _ boxy_tvs _ subst + = panic "boxy_match_s" -- Lengths do not match + ------------ boxy_match :: TcTyVarSet -> TcType -- Template @@ -433,8 +490,13 @@ boxy_match tmpl_tvs orig_tmpl_ty boxy_tvs orig_boxy_ty subst | Just t_ty' <- tcView t_ty = go t_ty' b_ty | Just b_ty' <- tcView b_ty = go t_ty b_ty' - go (ForAllTy _ ty1) (ForAllTy tv2 ty2) - = boxy_match tmpl_tvs ty1 (boxy_tvs `extendVarSet` tv2) ty2 subst + go ty1 ty2 -- C.f. the isSigmaTy case for boxySubMatchType + | isSigmaTy ty1 + , (tvs1, _, tau1) <- tcSplitSigmaTy ty1 + , (tvs2, _, tau2) <- tcSplitSigmaTy ty2 + , equalLength tvs1 tvs2 + = boxy_match (tmpl_tvs `delVarSetList` tvs1) tau1 + (boxy_tvs `extendVarSetList` tvs2) tau2 subst go (TyConApp tc1 tys1) (TyConApp tc2 tys2) | tc1 == tc2 = go_s tys1 tys2 @@ -450,15 +512,23 @@ boxy_match tmpl_tvs orig_tmpl_ty boxy_tvs orig_boxy_ty subst go (TyVarTy tv) b_ty | tv `elemVarSet` tmpl_tvs -- Template type variable in the template - , not (intersectsVarSet boxy_tvs (tyVarsOfType orig_boxy_ty)) - , typeKind b_ty `isSubKind` tyVarKind tv + , boxy_tvs `disjointVarSet` tyVarsOfType orig_boxy_ty + , typeKind b_ty `isSubKind` tyVarKind tv -- See Note [Matching kinds] = extendTvSubst subst tv boxy_ty' + | otherwise + = subst -- Ignore others where boxy_ty' = case lookupTyVar subst tv of Nothing -> orig_boxy_ty Just ty -> ty `boxyLub` orig_boxy_ty - go _ _ = subst -- Always safe + go _ _ = emptyTvSubst -- It's important to *fail* by returning the empty substitution + -- Example: Tree a ~ Maybe Int + -- We do not want to bind (a |-> Int) in pre-matching, because that can give very + -- misleading error messages. An even more confusing case is + -- a -> b ~ Maybe Int + -- Then we do not want to bind (b |-> Int)! It's always safe to discard bindings + -- from this pre-matching phase. -------- go_s tys1 tys2 = boxy_match_s tmpl_tvs tys1 boxy_tvs tys2 subst @@ -477,8 +547,8 @@ boxyLub orig_ty1 orig_ty2 = TyConApp tc1 (zipWith boxyLub ts1 ts2) go (TyVarTy tv1) ty2 -- This is the whole point; - | isTcTyVar tv1, isMetaTyVar tv1 -- choose ty2 if ty2 is a box - = ty2 + | isTcTyVar tv1, isBoxyTyVar tv1 -- choose ty2 if ty2 is a box + = orig_ty2 -- Look inside type synonyms, but only if the naive version fails go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2 @@ -488,6 +558,19 @@ boxyLub orig_ty1 orig_ty2 go ty1 ty2 = orig_ty1 -- Default \end{code} +Note [Matching kinds] +~~~~~~~~~~~~~~~~~~~~~ +The target type might legitimately not be a sub-kind of template. +For example, suppose the target is simply a box with an OpenTypeKind, +and the template is a type variable with LiftedTypeKind. +Then it's ok (because the target type will later be refined). +We simply don't bind the template type variable. + +It might also be that the kind mis-match is an error. For example, +suppose we match the template (a -> Int) against (Int# -> Int), +where the template type variable 'a' has LiftedTypeKind. This +matching function does not fail; it simply doesn't bind the template. +Later stuff will fail. %************************************************************************ %* * @@ -511,38 +594,66 @@ 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) - (tc_sub True actual_ty actual_ty expected_ty expected_ty) - -tcFunResTy :: Name -> BoxySigmaType -> BoxySigmaType -> TcM ExprCoFn -- Locally used only + = -- addErrCtxtM (unifyCtxt actual_ty expected_ty) $ + -- Adding the error context here leads to some very confusing error + -- messages, such as "can't match forall a. a->a with forall a. a->a" + -- 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 SubOther actual_ty actual_ty False expected_ty expected_ty + +tcFunResTy :: Name -> BoxySigmaType -> BoxySigmaType -> TcM HsWrapper -- Locally used only tcFunResTy fun actual_ty expected_ty - = addErrCtxtM (checkFunResCtxt fun actual_ty expected_ty) $ - (tc_sub True actual_ty actual_ty expected_ty expected_ty) + = traceTc (text "tcFunResTy" <+> ppr actual_ty <+> ppr expected_ty) >> + tc_sub (SubFun fun) actual_ty actual_ty False expected_ty expected_ty ----------------- -tc_sub :: Outer -- See comments with uTys +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 +-- (i.e. tha args are sufficiently zonked) +-- This invariant is needed so that we can "see" the foralls, ad +-- e.g. in the SPEC rule where we just use splitSigmaTy + +tc_sub sub_ctxt act_sty act_ty exp_ib exp_sty exp_ty + = tc_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_sub outer act_sty act_ty exp_sty exp_ty - | Just exp_ty' <- tcView exp_ty = tc_sub False act_sty act_ty exp_sty exp_ty' -tc_sub outer act_sty act_ty exp_sty exp_ty - | Just act_ty' <- tcView act_ty = tc_sub False act_sty act_ty' 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_sub outer act_sty (TyVarTy tv) exp_sty exp_ty - = do { uVar outer False tv False exp_sty exp_ty - ; return idCoercion } +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 } ----------------------------------- -- Skolemisation case (rule SKOL) @@ -555,15 +666,16 @@ tc_sub outer act_sty (TyVarTy tv) exp_sty exp_ty -- g :: Ord b => b->b -- Consider f g ! -tc_sub outer act_sty act_ty exp_sty exp_ty - | isSigmaTy exp_ty - = do { (gen_fn, co_fn) <- tcGen exp_ty act_tvs $ \ body_exp_ty -> - tc_sub False act_sty act_ty body_exp_ty body_exp_ty +tc_sub1 sub_ctxt 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 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 the free vars of - -- both expected_ty *and* actual_ty + -- It's really important to check for escape wrt + -- the free vars of both expected_ty *and* actual_ty ----------------------------------- -- Specialisation case (rule ASPEC): @@ -571,58 +683,82 @@ tc_sub outer act_sty act_ty exp_sty exp_ty -- expected_ty: Int -> Int -- co_fn e = e Int dOrdInt -tc_sub outer act_sty actual_ty 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.) +-- The idea is to *first* do pre-subsumption, and then full subsumption +-- Example: forall a. a->a <= Int -> (forall b. Int) +-- Pre-subsumpion finds a|->Int, and that works fine, whereas +-- just running full subsumption would fail. | isSigmaTy actual_ty - = do { (tyvars, theta, tau) <- tcInstBoxy actual_ty - ; dicts <- newDicts InstSigOrigin theta - ; extendLIEs dicts - ; let inst_fn = CoApps (CoTyApps CoHole (mkTyVarTys tyvars)) - (map instToId dicts) - ; co_fn <- tc_sub False tau tau exp_sty expected_ty - ; return (co_fn <.> inst_fn) } + = do { -- 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 + tau_tvs = exactTyVarsOfType tau + ; inst_tys <- if exp_ib then -- Inside a box, do not do clever stuff + do { tyvars' <- mapM tcInstBoxyTyVar tyvars + ; return (mkTyVarTys tyvars') } + else -- Outside, do clever stuff + preSubType tyvars tau_tvs tau expected_ty + ; let subst' = zipOpenTvSubst tyvars inst_tys + tau' = substTy subst' tau + + -- Perform a full subsumption check + ; traceTc (text "tc_sub_spec" <+> vcat [ppr actual_ty, + ppr tyvars <+> ppr theta <+> ppr tau, + ppr tau']) + ; co_fn2 <- tc_sub sub_ctxt tau' tau' exp_ib exp_sty expected_ty + + -- Deal with the dictionaries + ; co_fn1 <- instCall InstSigOrigin inst_tys (substTheta subst' theta) + ; return (co_fn2 <.> co_fn1) } ----------------------------------- -- Function case (rule F1) -tc_sub _ _ (FunTy act_arg act_res) _ (FunTy exp_arg exp_res) - = tc_sub_funs act_arg act_res 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_sub outer 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 -> do { u_tys outer False act_sty act_ty True exp_sty ty - ; return idCoercion } + 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 act_arg act_res 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_sub outer act_sty actual_ty exp_sty expected_ty - = do { u_tys outer False act_sty actual_ty False exp_sty expected_ty - ; return idCoercion } +tc_sub1 sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty + = do { addSubCtxt sub_ctxt act_sty exp_sty $ + u_tys True False act_sty actual_ty exp_ib exp_sty expected_ty + ; return idHsWrapper } ----------------------------------- -tc_sub_funs act_arg act_res exp_arg exp_res - = do { uTys False act_arg False exp_arg - ; co_fn_res <- tc_sub False act_res act_res exp_res 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 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 { us <- newUniqueSupply - ; let arg_ids = zipWith (mkSysLocal FSLIT("sub")) (uniqsFromSupply us) arg_tys - ; return (CoLams arg_ids (co_fn_res <.> (CoApps CoHole arg_ids))) } + = do { arg_ids <- newSysLocalIds FSLIT("sub") arg_tys + ; return (mkWpLams arg_ids <.> co_fn_res <.> mkWpApps arg_ids) } \end{code} @@ -638,8 +774,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 @@ -648,7 +784,7 @@ 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 @@ -657,13 +793,12 @@ tcGen expected_ty extra_tvs thing_inside -- We expect expected_ty to be a forall #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 @@ -676,18 +811,16 @@ 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 <- newDicts (SigOrigin skol_info) theta - ; inst_binds <- tcSimplifyCheck sig_msg forall_tvs dicts lie + ; dicts <- newDictBndrsO (SigOrigin skol_info) theta' + ; inst_binds <- tcSimplifyCheck sig_msg tvs' dicts lie - ; checkSigTyVarsWrt free_tvs forall_tvs + ; checkSigTyVarsWrt free_tvs tvs' ; traceTc (text "tcGen:done") ; let - -- This HsLet binds any Insts which came out of the simplification. - -- It's a bit out of place here, but using AbsBind involves inventing - -- a couple of new names which seems worse. - dict_ids = map instToId dicts - co_fn = CoTyLams forall_tvs $ CoLams dict_ids $ CoLet inst_binds CoHole + -- 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 ; returnM (co_fn, result) } where free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs @@ -779,8 +912,12 @@ 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 NoBoxes = Bool -- True <=> definitely no boxes in this type - -- False <=> there might be boxes (always safe) +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 + -- filled-box", we'll look into the boxes and unify... but + -- we must not allow polytypes. But if we are in a box on + -- just one side, then we can allow polytypes type Outer = Bool -- True <=> this is the outer level of a unification -- so that the types being unified are the @@ -790,16 +927,18 @@ type Outer = Bool -- True <=> this is the outer level of a unification -- pop the context to remove the "Expected/Acutal" context uTysOuter, uTys - :: NoBoxes -> TcType -- ty1 is the *expected* type - -> NoBoxes -> TcType -- ty2 is the *actual* type + :: InBox -> TcType -- ty1 is the *expected* type + -> InBox -> TcType -- ty2 is the *actual* type -> TcM () -uTysOuter nb1 ty1 nb2 ty2 = u_tys True nb1 ty1 ty1 nb2 ty2 ty2 -uTys nb1 ty1 nb2 ty2 = u_tys False nb1 ty1 ty1 nb2 ty2 ty2 +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 :: NoBoxes -> [TcType] -- ty1 is the *actual* types - -> NoBoxes -> [TcType] -- ty2 is the *expected* types +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 @@ -808,8 +947,8 @@ uTys_s nb1 ty1s nb2 ty2s = panic "Unify.uTys_s: mismatched type lists!" -------------- u_tys :: Outer - -> NoBoxes -> TcType -> TcType -- ty1 is the *actual* type - -> NoBoxes -> TcType -> TcType -- ty2 is the *expected* type + -> InBox -> TcType -> TcType -- ty1 is the *actual* type + -> InBox -> TcType -> TcType -- ty2 is the *expected* type -> TcM () u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2 @@ -862,9 +1001,12 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2 subst2 = mkTvSubst in_scope (zipTyEnv tvs2 tys) ; uTys nb1 (substTy subst1 body1) nb2 (substTy subst2 body2) - -- If both sides are inside a box, we should not have - -- a polytype at all. This check comes last, because - -- the error message is extremely unhelpful. + -- 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 @@ -961,7 +1103,7 @@ uVar :: Outer -> Bool -- False => tyvar is the "expected" -- True => ty is the "expected" thing -> TcTyVar - -> NoBoxes -- True <=> definitely no boxes in t2 + -> InBox -- True <=> definitely no boxes in t2 -> TcTauType -> TcTauType -- printing and real versions -> TcM () @@ -970,48 +1112,51 @@ uVar outer swapped tv1 nb2 ps_ty2 ty2 | otherwise = brackets (equals <+> ppr ty2) ; traceTc (text "uVar" <+> ppr swapped <+> sep [ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1 ), - nest 2 (ptext SLIT(" :=: ")), + nest 2 (ptext SLIT(" <-> ")), ppr ps_ty2 <+> dcolon <+> ppr (typeKind ty2) <+> expansion]) ; details <- lookupTcTyVar tv1 ; case details of IndirectTv ty1 | swapped -> u_tys outer nb2 ps_ty2 ty2 True ty1 ty1 -- Swap back | otherwise -> u_tys outer True ty1 ty1 nb2 ps_ty2 ty2 -- Same order - -- The 'True' here says that ty1 - -- is definitely box-free - DoneTv details1 -> uUnfilledVar outer swapped tv1 details1 nb2 ps_ty2 ty2 + -- The 'True' here says that ty1 is now inside a box + DoneTv details1 -> uUnfilledVar outer swapped tv1 details1 ps_ty2 ty2 } ---------------- uUnfilledVar :: Outer -> Bool -- Args are swapped - -> TcTyVar -> TcTyVarDetails -- Tyvar 1 - -> NoBoxes -> TcTauType -> TcTauType -- Type 2 + -> TcTyVar -> TcTyVarDetails -- Tyvar 1 + -> TcTauType -> TcTauType -- Type 2 -> TcM () -- Invariant: tyvar 1 is not unified with anything -uUnfilledVar outer swapped tv1 details1 nb2 ps_ty2 ty2 +uUnfilledVar outer swapped tv1 details1 ps_ty2 ty2 | Just ty2' <- tcView ty2 = -- Expand synonyms; ignore FTVs - uUnfilledVar False swapped tv1 details1 nb2 ps_ty2 ty2' + uUnfilledVar False swapped tv1 details1 ps_ty2 ty2' -uUnfilledVar outer swapped tv1 details1 nb2 ps_ty2 ty2@(TyVarTy tv2) - -- Same type variable => no-op - | tv1 == tv2 - = returnM () +uUnfilledVar outer swapped tv1 details1 ps_ty2 (TyVarTy tv2) + | tv1 == tv2 -- Same type variable => no-op (but watch out for the boxy case) + = case details1 of + 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 -- Distinct type variables | otherwise = do { lookup2 <- lookupTcTyVar tv2 ; case lookup2 of - IndirectTv ty2' -> uUnfilledVar outer swapped tv1 details1 True 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 nb2 ps_ty2 non_var_ty2 -- ty2 is not a type variable +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 nb2 ps_ty2 non_var_ty2 + MetaTv info ref1 -> uMetaVar swapped tv1 info ref1 ps_ty2 non_var_ty2 skolem_details -> mis_match where mis_match = unifyMisMatch outer swapped (TyVarTy tv1) ps_ty2 @@ -1019,15 +1164,31 @@ uUnfilledVar outer swapped tv1 details1 nb2 ps_ty2 non_var_ty2 -- ty2 is not a t ---------------- uMetaVar :: Bool -> TcTyVar -> BoxInfo -> IORef MetaDetails - -> NoBoxes -> TcType -> TcType + -> TcType -> TcType -> TcM () -- tv1 is an un-filled-in meta type variable (maybe boxy, maybe tau) -- ty2 is not a type variable -uMetaVar swapped tv1 info1 ref1 nb2 ps_ty2 non_var_ty2 - = do { final_ty <- case info1 of - BoxTv -> unBox ps_ty2 -- No occurs check - other -> checkTauTvUpdate tv1 ps_ty2 -- Occurs check + monotype check +uMetaVar 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 + -- + -- It should not be the case that tv1 occurs in ty2 + -- (i.e. no occurs check should be needed), but if perchance + -- it does, the unbox operation will fill it, and the DEBUG + -- checks for that. + do { final_ty <- unBox ps_ty2 +#ifdef DEBUG + ; meta_details <- readMutVar ref1 + ; case meta_details of + Indirect ty -> WARN( True, ppr tv1 <+> ppr ty ) + return () -- This really should *not* happen + 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 } ---------------- @@ -1079,13 +1240,18 @@ uUnfilledVars outer swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2) update_tv1 = updateMeta tv1 ref1 (mkTyVarTy tv2) update_tv2 = updateMeta tv2 ref2 (mkTyVarTy tv1) - box_meets_box | k1_sub_k2 = fill_with k1 - | k2_sub_k1 = fill_with k2 + box_meets_box | k1_sub_k2 = if k2_sub_k1 && nicer_to_update_tv1 + then fill_from tv2 + else fill_from tv1 + | k2_sub_k1 = fill_from tv2 | otherwise = kind_err - fill_with kind = do { tau_ty <- newFlexiTyVarTy kind - ; updateMeta tv1 ref1 tau_ty - ; updateMeta tv2 ref2 tau_ty } + -- Update *both* tyvars with a TauTv whose name and kind + -- are gotten from tv (avoid losing nice names is poss) + fill_from tv = do { tv' <- tcInstTyVar tv + ; let tau_ty = mkTyVarTy tv' + ; updateMeta tv1 ref1 tau_ty + ; updateMeta tv2 ref2 tau_ty } kind_err = addErrCtxtM (unifyKindCtxt swapped tv1 (mkTyVarTy tv2)) $ unifyKindMisMatch k1 k2 @@ -1174,6 +1340,7 @@ checkTauTvUpdate orig_tv orig_ty 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) @@ -1181,9 +1348,7 @@ checkTauTvUpdate orig_tv orig_ty ; case cts of Indirect ty -> go ty Flexi -> case box of - BoxTv -> do { tau <- newFlexiTyVarTy (tyVarKind tv) - ; writeMutVar ref (Indirect tau) - ; return tau } + BoxTv -> fillBoxWithTau tv ref other -> return (TyVarTy tv) } @@ -1201,6 +1366,19 @@ checkTauTvUpdate orig_tv orig_ty (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] @@ -1251,7 +1429,7 @@ unBox :: BoxyType -> TcM TcType -- |- s' ~ box(s) -- with input s', and result s -- --- It remove all boxes from the input type, returning a non-boxy type. +-- It removes all boxes from the input type, returning a non-boxy type. -- A filled box in the type can only contain a monotype; unBox fails if not -- The type can have empty boxes, which unBox fills with a monotype -- @@ -1271,19 +1449,18 @@ 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 Indirect ty -> do { non_boxy_ty <- unBox ty ; if isTauTy non_boxy_ty then return non_boxy_ty else notMonoType non_boxy_ty } - Flexi -> do { tau <- newFlexiTyVarTy (tyVarKind tv) - ; writeMutVar ref (Indirect tau) - ; return tau } } | otherwise -- Skolems, and meta-tau-variables = return (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} @@ -1313,24 +1490,28 @@ 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. -checkFunResCtxt 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 | len_exp_args < len_act_args = wrongArgsCtxt "too few" fun - | len_exp_args > len_act_args = wrongArgsCtxt "too many" fun - | otherwise = 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 @@ -1375,8 +1556,8 @@ ppr_ty env ty simple_result = (env1, quotes (ppr tidy_ty), empty) ; case tidy_ty of TyVarTy tv - | isSkolemTyVar tv -> return (env2, pp_rigid tv', - pprSkolTvBinding tv') + | isSkolemTyVar tv || isSigTyVar tv + -> return (env2, pp_rigid tv', pprSkolTvBinding tv') | otherwise -> return simple_result where (env2, tv') = tidySkolemTyVar env1 tv @@ -1389,7 +1570,7 @@ notMonoType ty = do { ty' <- zonkTcType ty ; env0 <- tcInitTidyEnv ; let (env1, tidy_ty) = tidyOpenType env0 ty' - msg = ptext SLIT("Cannot match a monotype with") <+> ppr tidy_ty + msg = ptext SLIT("Cannot match a monotype with") <+> quotes (ppr tidy_ty) ; failWithTcM (env1, msg) } occurCheck tyvar ty @@ -1416,20 +1597,15 @@ Unifying kinds is much, much simpler than unifying types. unifyKind :: TcKind -- Expected -> TcKind -- Actual -> TcM () -unifyKind LiftedTypeKind LiftedTypeKind = returnM () -unifyKind UnliftedTypeKind UnliftedTypeKind = returnM () +unifyKind (TyConApp kc1 []) (TyConApp kc2 []) + | isSubKindCon kc2 kc1 = returnM () -unifyKind OpenTypeKind k2 | isOpenTypeKind k2 = returnM () -unifyKind ArgTypeKind k2 | isArgTypeKind k2 = returnM () - -- Respect sub-kinding - -unifyKind (FunKind a1 r1) (FunKind a2 r2) - = do { unifyKind a2 a1; unifyKind r1 r2 } +unifyKind (FunTy a1 r1) (FunTy a2 r2) + = do { unifyKind a2 a1; unifyKind r1 r2 } -- Notice the flip in the argument, -- so that the sub-kinding works right - -unifyKind (KindVar kv1) k2 = uKVar False kv1 k2 -unifyKind k1 (KindVar kv2) = uKVar True kv2 k1 +unifyKind (TyVarTy kv1) k2 = uKVar False kv1 k2 +unifyKind k1 (TyVarTy kv2) = uKVar True kv2 k1 unifyKind k1 k2 = unifyKindMisMatch k1 k2 unifyKinds :: [TcKind] -> [TcKind] -> TcM () @@ -1443,19 +1619,19 @@ uKVar :: Bool -> KindVar -> TcKind -> TcM () uKVar swapped kv1 k2 = do { mb_k1 <- readKindVar kv1 ; case mb_k1 of - Nothing -> uUnboundKVar swapped kv1 k2 - Just k1 | swapped -> unifyKind k2 k1 - | otherwise -> unifyKind k1 k2 } + Flexi -> uUnboundKVar swapped kv1 k2 + Indirect k1 | swapped -> unifyKind k2 k1 + | otherwise -> unifyKind k1 k2 } ---------------- uUnboundKVar :: Bool -> KindVar -> TcKind -> TcM () -uUnboundKVar swapped kv1 k2@(KindVar kv2) +uUnboundKVar swapped kv1 k2@(TyVarTy kv2) | kv1 == kv2 = returnM () | otherwise -- Distinct kind variables = do { mb_k2 <- readKindVar kv2 ; case mb_k2 of - Just k2 -> uUnboundKVar swapped kv1 k2 - Nothing -> writeKindVar kv1 k2 } + Indirect k2 -> uUnboundKVar swapped kv1 k2 + Flexi -> writeKindVar kv1 k2 } uUnboundKVar swapped kv1 non_var_k2 = do { k2' <- zonkTcKind non_var_k2 @@ -1472,9 +1648,9 @@ uUnboundKVar swapped kv1 non_var_k2 kindOccurCheck kv1 k2 -- k2 is zonked = checkTc (not_in k2) (kindOccurCheckErr kv1 k2) where - not_in (KindVar kv2) = kv1 /= kv2 - not_in (FunKind a2 r2) = not_in a2 && not_in r2 - not_in other = True + not_in (TyVarTy kv2) = kv1 /= kv2 + not_in (FunTy a2 r2) = not_in a2 && not_in r2 + not_in other = True kindSimpleKind :: Bool -> Kind -> TcM SimpleKind -- (kindSimpleKind True k) returns a simple kind sk such that sk <: k @@ -1484,13 +1660,16 @@ kindSimpleKind :: Bool -> Kind -> TcM SimpleKind kindSimpleKind orig_swapped orig_kind = go orig_swapped orig_kind where - go sw (FunKind k1 k2) = do { k1' <- go (not sw) k1 - ; k2' <- go sw k2 - ; return (FunKind k1' k2') } - go True OpenTypeKind = return liftedTypeKind - go True ArgTypeKind = return liftedTypeKind - go sw LiftedTypeKind = return liftedTypeKind - go sw k@(KindVar _) = return k -- KindVars are always simple + go sw (FunTy k1 k2) = do { k1' <- go (not sw) k1 + ; k2' <- go sw k2 + ; return (mkArrowKind k1' k2') } + go True k + | isOpenTypeKind k = return liftedTypeKind + | isArgTypeKind k = return liftedTypeKind + go sw k + | isLiftedTypeKind k = return liftedTypeKind + | isUnliftedTypeKind k = return unliftedTypeKind + go sw k@(TyVarTy _) = return k -- KindVars are always simple go swapped kind = failWithTc (ptext SLIT("Unexpected kind unification failure:") <+> ppr orig_swapped <+> ppr orig_kind) -- I think this can't actually happen @@ -1519,17 +1698,18 @@ unifyKindMisMatch ty1 ty2 unifyFunKind :: TcKind -> TcM (Maybe (TcKind, TcKind)) -- Like unifyFunTy, but does not fail; instead just returns Nothing -unifyFunKind (KindVar kvar) - = readKindVar kvar `thenM` \ maybe_kind -> +unifyFunKind (TyVarTy kvar) + = readKindVar kvar `thenM` \ maybe_kind -> case maybe_kind of - Just fun_kind -> unifyFunKind fun_kind - Nothing -> do { arg_kind <- newKindVar - ; res_kind <- newKindVar - ; writeKindVar kvar (mkArrowKind arg_kind res_kind) - ; returnM (Just (arg_kind,res_kind)) } + Indirect fun_kind -> unifyFunKind fun_kind + Flexi -> + do { arg_kind <- newKindVar + ; res_kind <- newKindVar + ; writeKindVar kvar (mkArrowKind arg_kind res_kind) + ; returnM (Just (arg_kind,res_kind)) } -unifyFunKind (FunKind arg_kind res_kind) = returnM (Just (arg_kind,res_kind)) -unifyFunKind other = returnM Nothing +unifyFunKind (FunTy arg_kind res_kind) = returnM (Just (arg_kind,res_kind)) +unifyFunKind other = returnM Nothing \end{code} %************************************************************************