From af20907ae1c9901b457cbab57e9d533e66e5aa07 Mon Sep 17 00:00:00 2001 From: "simonpj@microsoft.com" Date: Fri, 4 Aug 2006 21:49:42 +0000 Subject: [PATCH] Do pre-subsumption in the main subsumption check This patch improves the subsumption check (in TcUnify.tc_sub) so that it does pre-subsumption first. The key code is in the case with guard (isSigmaTy actual_ty); note the new call to preSubType. Shorn of details, the question is this. Should this hold? forall a. a->a <= Int -> (forall b. Int) Really, it should; just instantiate 'a' to Int. This is just what the pre-subsumption phase (which used in function applications), will do. I did a bit of refactoring to achieve this. Fixes Trac #821. Test tc205 tests. --- compiler/rename/RnExpr.lhs | 2 +- compiler/typecheck/TcExpr.lhs | 43 +++------- compiler/typecheck/TcMType.lhs | 11 +-- compiler/typecheck/TcPat.lhs | 3 +- compiler/typecheck/TcType.lhs | 4 +- compiler/typecheck/TcUnify.lhs | 183 +++++++++++++++++++++++++++------------- 6 files changed, 143 insertions(+), 103 deletions(-) diff --git a/compiler/rename/RnExpr.lhs b/compiler/rename/RnExpr.lhs index e968590..c14909e 100644 --- a/compiler/rename/RnExpr.lhs +++ b/compiler/rename/RnExpr.lhs @@ -459,7 +459,7 @@ methodNamesCmd other = emptyFVs -- The type checker will complain later --------------------------------------------------- -methodNamesMatch (MatchGroup ms ty) +methodNamesMatch (MatchGroup ms _) = plusFVs (map do_one ms) where do_one (L _ (Match pats sig_ty grhss)) = methodNamesGRHSs grhss diff --git a/compiler/typecheck/TcExpr.lhs b/compiler/typecheck/TcExpr.lhs index 36cda5a..e897420 100644 --- a/compiler/typecheck/TcExpr.lhs +++ b/compiler/typecheck/TcExpr.lhs @@ -26,7 +26,7 @@ import HsSyn ( HsExpr(..), LHsExpr, ArithSeqInfo(..), recBindFields, import TcHsSyn ( hsLitType ) import TcRnMonad import TcUnify ( tcInfer, tcSubExp, tcFunResTy, tcGen, boxyUnify, subFunTys, zapToMonotype, stripBoxyType, - boxySplitListTy, boxySplitTyConApp, wrapFunResCoercion, boxySubMatchType, + boxySplitListTy, boxySplitTyConApp, wrapFunResCoercion, preSubType,, unBox ) import BasicTypes ( Arity, isMarkedStrict ) import Inst ( newMethodFromName, newIPDict, instToId, @@ -648,26 +648,7 @@ tcIdApp fun_name n_args arg_checker res_ty ; extra_arg_boxes <- newBoxyTyVars (replicate n_missing_args argTypeKind) ; let extra_arg_tys' = mkTyVarTys extra_arg_boxes res_ty' = mkFunTys extra_arg_tys' res_ty - subst = boxySubMatchType arg_qtvs fun_res_ty res_ty' - -- Only bind arg_qtvs, since only they will be - -- *definitely* be filled in by arg_checker - -- E.g. error :: forall a. String -> a - -- (error "foo") :: bx5 - -- Don't make subst [a |-> bx5] - -- because then the result subsumption becomes - -- bx5 ~ bx5 - -- and the unifer doesn't expect the - -- same box on both sides - inst_qtv tv | Just boxy_ty <- lookupTyVar subst tv = return boxy_ty - | tv `elemVarSet` tau_qtvs = do { tv' <- tcInstBoxyTyVar tv - ; return (mkTyVarTy tv') } - | otherwise = do { tv' <- tcInstTyVar tv - ; return (mkTyVarTy tv') } - -- The 'otherwise' case handles type variables that are - -- mentioned only in the constraints, not in argument or - -- result types. We'll make them tau-types - - ; qtys' <- mapM inst_qtv qtvs + ; qtys' <- preSubType qtvs tau_qtvs fun_res_ty res_ty' ; let arg_subst = zipOpenTvSubst qtvs qtys' fun_arg_tys' = substTys arg_subst fun_arg_tys @@ -675,8 +656,12 @@ tcIdApp fun_name n_args arg_checker res_ty -- Doing so will fill arg_qtvs and extra_arg_tys' ; args' <- arg_checker (fun_arg_tys' ++ extra_arg_tys') + -- Strip boxes from the qtvs that have been filled in by the arg checking + -- AND any variables that are mentioned in neither arg nor result + -- the latter are mentioned only in constraints; stripBoxyType will + -- fill them with a monotype ; let strip qtv qty' | qtv `elemVarSet` arg_qtvs = stripBoxyType qty' - | otherwise = return qty' + | otherwise = return qty' ; qtys'' <- zipWithM strip qtvs qtys' ; extra_arg_tys'' <- mapM readFilledBox extra_arg_boxes @@ -722,17 +707,13 @@ tcId orig fun_name res_ty -- Split up the function type ; let (tv_theta_prs, fun_tau) = tcMultiSplitSigmaTy (idType fun_id) - qtvs = concatMap fst tv_theta_prs -- Quantified tyvars - tau_qtvs = exactTyVarsOfType fun_tau -- Mentiond in the tau part - inst_qtv tv | tv `elemVarSet` tau_qtvs = do { tv' <- tcInstBoxyTyVar tv - ; return (mkTyVarTy tv') } - | otherwise = do { tv' <- tcInstTyVar tv - ; return (mkTyVarTy tv') } + qtvs = concatMap fst tv_theta_prs -- Quantified tyvars + tau_qtvs = exactTyVarsOfType fun_tau -- Mentioned in the tau part + ; qtv_tys <- preSubType qtvs tau_qtvs fun_tau res_ty -- Do the subsumption check wrt the result type - ; qtv_tys <- mapM inst_qtv qtvs - ; let res_subst = zipTopTvSubst qtvs qtv_tys - fun_tau' = substTy res_subst fun_tau + ; let res_subst = zipTopTvSubst qtvs qtv_tys + fun_tau' = substTy res_subst fun_tau ; co_fn <- tcFunResTy fun_name fun_tau' res_ty diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs index 6a2041e..fe51df1 100644 --- a/compiler/typecheck/TcMType.lhs +++ b/compiler/typecheck/TcMType.lhs @@ -24,7 +24,7 @@ module TcMType ( -------------------------------- -- Instantiation - tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxy, tcInstBoxyTyVar, + tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxyTyVar, tcInstSigTyVars, zonkSigTyVar, tcInstSkolTyVar, tcInstSkolTyVars, tcInstSkolType, tcSkolSigType, tcSkolSigTyVars, @@ -58,8 +58,7 @@ import TypeRep ( Type(..), PredType(..), -- Friend; can see representation import TcType ( TcType, TcThetaType, TcTauType, TcPredType, TcTyVarSet, TcKind, TcTyVar, TcTyVarDetails(..), MetaDetails(..), SkolemInfo(..), BoxInfo(..), - BoxyTyVar, BoxyType, BoxyThetaType, BoxySigmaType, - UserTypeCtxt(..), + BoxyTyVar, BoxyType, UserTypeCtxt(..), isMetaTyVar, isSigTyVar, metaTvRef, tcCmpPred, isClassPred, tcGetTyVar, tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe, @@ -327,12 +326,6 @@ readFilledBox box_tv = ASSERT( isBoxyTyVar box_tv ) tcInstBoxyTyVar :: TyVar -> TcM BoxyTyVar -- Instantiate with a BOXY type variable tcInstBoxyTyVar tyvar = instMetaTyVar BoxTv tyvar - -tcInstBoxy :: TcType -> TcM ([BoxyTyVar], BoxyThetaType, BoxySigmaType) --- tcInstType instantiates the outer-level for-alls of a TcType with --- fresh BOXY type variables, splits off the dictionary part, --- and returns the pieces. -tcInstBoxy ty = tcInstType (mapM tcInstBoxyTyVar) ty \end{code} diff --git a/compiler/typecheck/TcPat.lhs b/compiler/typecheck/TcPat.lhs index 4c56b08..3c1c3ba 100644 --- a/compiler/typecheck/TcPat.lhs +++ b/compiler/typecheck/TcPat.lhs @@ -683,8 +683,7 @@ newLitInst orig lit res_ty -- Make a LitInst = do { loc <- getInstLoc orig ; res_tau <- zapToMonotype res_ty ; new_uniq <- newUnique - ; let - lit_nm = mkSystemVarName new_uniq FSLIT("lit") + ; let lit_nm = mkSystemVarName new_uniq FSLIT("lit") lit_inst = LitInst lit_nm lit res_tau loc ; extendLIE lit_inst ; return (HsVar (instToId lit_inst)) } diff --git a/compiler/typecheck/TcType.lhs b/compiler/typecheck/TcType.lhs index b60936d..5ad9a10 100644 --- a/compiler/typecheck/TcType.lhs +++ b/compiler/typecheck/TcType.lhs @@ -170,7 +170,7 @@ import TyCon ( TyCon, isUnLiftedTyCon, isSynTyCon, synTyConDefn, tyConUnique ) import DataCon ( DataCon, dataConStupidTheta, dataConResTys ) import Class ( Class ) import Var ( TyVar, Id, isTcTyVar, mkTcTyVar, tyVarName, tyVarKind, tcTyVarDetails ) -import ForeignCall ( Safety, playSafe, DNType(..) ) +import ForeignCall ( Safety, DNType(..) ) import Unify ( tcMatchTys ) import VarSet @@ -966,7 +966,7 @@ smart-app checking code --- see TcExpr.tcIdApp \begin{code} exactTyVarsOfType :: TcType -> TyVarSet -- Find the free type variables (of any kind) --- but *expand* type synonyms. See Note [Silly type synonym] belos. +-- but *expand* type synonyms. See Note [Silly type synonym] above. exactTyVarsOfType ty = go ty where diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs index 1a61822..c13da2c 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 @@ -29,8 +29,8 @@ import HsSyn ( ExprCoFn(..), idCoercion, isIdCoercion, (<.>) ) import TypeRep ( Type(..), PredType(..) ) import TcMType ( lookupTcTyVar, LookupTyVarResult(..), - tcInstSkolType, newKindVar, newMetaTyVar, - tcInstBoxy, newBoxyTyVar, newBoxyTyVarTys, readFilledBox, + tcInstSkolType, tcInstBoxyTyVar, newKindVar, newMetaTyVar, + newBoxyTyVar, newBoxyTyVarTys, readFilledBox, readMetaTyVar, writeMetaTyVar, newFlexiTyVarTy, tcInstSkolTyVars, tcInstTyVar, zonkTcKind, zonkType, zonkTcType, zonkTcTyVarsAndFV, @@ -46,11 +46,13 @@ import TcType ( TcKind, TcType, TcTyVar, BoxyTyVar, TcTauType, 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, + exactTyVarsOfType, tidyOpenType, tidyOpenTyVar, tidyOpenTyVars, pprType, tidyKind, tidySkolemTyVar, isSkolemTyVar, tcView, - TvSubst, mkTvSubst, zipTyEnv, substTy, emptyTvSubst, + TvSubst, mkTvSubst, zipTyEnv, zipOpenTvSubst, emptyTvSubst, + substTy, substTheta, lookupTyVar, extendTvSubst ) import Kind ( Kind(..), SimpleKind, KindVar, isArgTypeKind, openTypeKind, liftedTypeKind, unliftedTypeKind, @@ -334,16 +336,95 @@ withBox kind thing_inside %************************************************************************ \begin{code} +preSubType :: [TcTyVar] -- Quantified type variables + -> TcTyVarSet -- Subset of quantified type variables + -- that can be instantiated with boxy types + -> 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 +-- +-- 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 + +preSubType qtvs btvs qty expected_ty + = mapM inst_tv qtvs + 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_ty emptyVarSet boxy_ty + where + go t_ty b_tvs b_ty + | Just t_ty' <- tcView t_ty = go t_ty' b_tvs b_ty + | Just b_ty' <- tcView b_ty = go t_ty b_tvs b_ty' + + go (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 (ForAllTy tv t_ty) b_tvs b_ty = go t_ty b_tvs b_ty -- Rule S-SPEC + go t_ty b_tvs (ForAllTy tv b_ty) = go t_ty b_tvs' b_ty -- Rule S-SKOL + where b_tvs' = extendVarSet b_tvs tv + + go (FunTy arg1 res1) b_tvs (FunTy arg2 res2) -- Rule S-FUN + = boxy_match tmpl_tvs arg1 b_tvs arg2 (go res1 b_tvs res2) + -- Match the args, and sub-match the results + + go t_ty b_tvs b_ty = boxy_match tmpl_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; @@ -352,57 +433,12 @@ 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 -- --- 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 ) @@ -452,7 +488,7 @@ 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 + , typeKind b_ty `isSubKind` tyVarKind tv -- See Note [Matching kinds] = extendTvSubst subst tv boxy_ty' where boxy_ty' = case lookupTyVar subst tv of @@ -489,6 +525,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. %************************************************************************ %* * @@ -563,8 +612,8 @@ tc_sub outer act_sty act_ty exp_sty 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): @@ -573,13 +622,31 @@ tc_sub outer act_sty act_ty exp_sty exp_ty -- co_fn e = e Int dOrdInt tc_sub outer act_sty actual_ty 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 + = 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 <- preSubType tyvars tau_tvs tau expected_ty + ; let subst' = zipOpenTvSubst tyvars inst_tys + tau' = substTy subst' tau + + -- Perform a full subsumption check + ; co_fn <- tc_sub False tau' tau' exp_sty expected_ty + + -- Deal with the dictionaries + ; dicts <- newDicts InstSigOrigin (substTheta subst' theta) ; extendLIEs dicts - ; let inst_fn = CoApps (CoTyApps CoHole (mkTyVarTys tyvars)) + ; let inst_fn = CoApps (CoTyApps CoHole inst_tys) (map instToId dicts) - ; co_fn <- tc_sub False tau tau exp_sty expected_ty ; return (co_fn <.> inst_fn) } ----------------------------------- @@ -1288,7 +1355,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 -- -- 1.7.10.4