X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcSimplify.lhs;h=853e2c491ef16c4e072da8d667218cfbfba2f72d;hb=14a496fd0b3aa821b69eb02736d5f41086576761;hp=57e91251d284d54d06cc64e5c7b6f1dc7fe3ab0c;hpb=b3e722e9ff0aeedceeeeacc67d61e11a5ee5b92a;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs index 57e9125..853e2c4 100644 --- a/compiler/typecheck/TcSimplify.lhs +++ b/compiler/typecheck/TcSimplify.lhs @@ -18,6 +18,8 @@ import TcInteract import Inst import Var import VarSet +import VarEnv ( varEnvElts ) + import Name import NameEnv ( emptyNameEnv ) import Bag @@ -185,7 +187,7 @@ simplifyInfer :: Bool -- Apply monomorphism restriction TcEvBinds) -- ... binding these evidence variables simplifyInfer apply_mr tau_tvs wanted | isEmptyBag wanted -- Trivial case is quite common - = do { zonked_tau_tvs <- zonkTcTyVarsAndFV (varSetElems tau_tvs) + = do { zonked_tau_tvs <- zonkTcTyVarsAndFV tau_tvs ; gbl_tvs <- tcGetGlobalTyVars -- Already zonked ; qtvs <- zonkQuantifiedTyVars (varSetElems (zonked_tau_tvs `minusVarSet` gbl_tvs)) ; return (qtvs, [], emptyTcEvBinds) } @@ -198,26 +200,50 @@ simplifyInfer apply_mr tau_tvs wanted , ptext (sLit "tau_tvs =") <+> ppr tau_tvs ] - ; (simple_wanted, tc_binds) - <- simplifyAsMuchAsPossible SimplInfer zonked_wanted + -- Make a guess at the quantified type variables + -- Then split the constraints on the baisis of those tyvars + -- to avoid unnecessarily simplifying a class constraint + -- See Note [Avoid unecessary constraint simplification] + ; gbl_tvs <- tcGetGlobalTyVars + ; zonked_tau_tvs <- zonkTcTyVarsAndFV tau_tvs + ; let proto_qtvs = growWanteds gbl_tvs zonked_wanted $ + zonked_tau_tvs `minusVarSet` gbl_tvs + (perhaps_bound, surely_free) + = partitionBag (quantifyMeWC proto_qtvs) zonked_wanted + + ; emitConstraints surely_free + ; traceTc "sinf" $ vcat + [ ptext (sLit "perhaps_bound =") <+> ppr perhaps_bound + , ptext (sLit "surely_free =") <+> ppr surely_free + ] + + -- Now simplify the possibly-bound constraints + ; (simplified_perhaps_bound, tc_binds) + <- simplifyAsMuchAsPossible SimplInfer perhaps_bound + -- Sigh: must re-zonk because because simplifyAsMuchAsPossible + -- may have done some unification ; gbl_tvs <- tcGetGlobalTyVars - ; zonked_tau_tvs <- zonkTcTyVarsAndFV (varSetElems tau_tvs) - ; zonked_simples <- mapBagM zonkWantedEvVar simple_wanted - ; let qtvs = findQuantifiedTyVars apply_mr zonked_simples zonked_tau_tvs gbl_tvs - (bound, free) | apply_mr = (emptyBag, zonked_simples) - | otherwise = partitionBag (quantifyMe qtvs) zonked_simples + ; zonked_tau_tvs <- zonkTcTyVarsAndFV tau_tvs + ; zonked_simples <- mapBagM zonkWantedEvVar simplified_perhaps_bound + ; let init_tvs = zonked_tau_tvs `minusVarSet` gbl_tvs + mr_qtvs = init_tvs `minusVarSet` constrained_tvs + constrained_tvs = tyVarsOfWantedEvVars zonked_simples + qtvs = growWantedEVs gbl_tvs zonked_simples init_tvs + (final_qtvs, (bound, free)) + | apply_mr = (mr_qtvs, (emptyBag, zonked_simples)) + | otherwise = (qtvs, partitionBag (quantifyMe qtvs) zonked_simples) ; traceTc "end simplifyInfer }" $ vcat [ ptext (sLit "apply_mr =") <+> ppr apply_mr , text "wanted = " <+> ppr zonked_wanted - , text "qtvs = " <+> ppr qtvs + , text "qtvs = " <+> ppr final_qtvs , text "free = " <+> ppr free , text "bound = " <+> ppr bound ] -- Turn the quantified meta-type variables into real type variables ; emitConstraints (mapBag WcEvVar free) - ; qtvs_to_return <- zonkQuantifiedTyVars (varSetElems qtvs) + ; qtvs_to_return <- zonkQuantifiedTyVars (varSetElems final_qtvs) ; let bound_evvars = bagToList $ mapBag wantedEvVarToVar bound ; return (qtvs_to_return, bound_evvars, EvBinds tc_binds) } @@ -227,7 +253,7 @@ simplifyAsMuchAsPossible :: SimplContext -> WantedConstraints -- We use this function when inferring the type of a function -- The wanted constraints are already zonked simplifyAsMuchAsPossible ctxt wanteds - = do { let untch = emptyVarSet + = do { let untch = NoUntouchables -- We allow ourselves to unify environment -- variables; hence *no untouchables* @@ -236,7 +262,7 @@ simplifyAsMuchAsPossible ctxt wanteds simplifyApproxLoop 0 wanteds -- Report any errors - ; mapBagM_ reportUnsolvedImplication unsolved_implics + ; reportUnsolved (emptyBag, unsolved_implics) ; let final_wanted_evvars = mapBag deCanonicaliseWanted unsolved_flats ; return (final_wanted_evvars, ev_binds) } @@ -308,25 +334,37 @@ approximateImplications impls \end{code} \begin{code} -findQuantifiedTyVars :: Bool -- Apply the MR - -> Bag WantedEvVar -- Simplified constraints from RHS - -> TyVarSet -- Free in tau-type of definition - -> TyVarSet -- Free in the envt - -> TyVarSet -- Quantify over these - -findQuantifiedTyVars apply_mr wanteds tau_tvs gbl_tvs - | isEmptyBag wanteds = init_tvs - | apply_mr = init_tvs `minusVarSet` constrained_tvs - | otherwise = fixVarSet mk_next init_tvs +growWantedEVs :: TyVarSet -> Bag WantedEvVar -> TyVarSet -> TyVarSet +growWanteds :: TyVarSet -> Bag WantedConstraint -> TyVarSet -> TyVarSet +growWanteds gbl_tvs ws tvs + | isEmptyBag ws = tvs + | otherwise = fixVarSet (\tvs -> foldrBag (growWanted gbl_tvs) tvs ws) tvs +growWantedEVs gbl_tvs ws tvs + | isEmptyBag ws = tvs + | otherwise = fixVarSet (\tvs -> foldrBag (growWantedEV gbl_tvs) tvs ws) tvs + +growEvVar :: TyVarSet -> EvVar -> TyVarSet -> TyVarSet +growWantedEV :: TyVarSet -> WantedEvVar -> TyVarSet -> TyVarSet +growWanted :: TyVarSet -> WantedConstraint -> TyVarSet -> TyVarSet +-- (growX gbls wanted tvs) grows a seed 'tvs' against the +-- X-constraint 'wanted', nuking the 'gbls' at each stage + +growEvVar gbl_tvs ev tvs + = tvs `unionVarSet` (ev_tvs `minusVarSet` gbl_tvs) where - init_tvs = tau_tvs `minusVarSet` gbl_tvs - mk_next tvs = foldrBag grow_one tvs wanteds + ev_tvs = growPredTyVars (evVarPred ev) tvs - grow_one wev tvs = tvs `unionVarSet` (extra_tvs `minusVarSet` gbl_tvs) - where - extra_tvs = growPredTyVars (wantedEvVarPred wev) tvs +growWantedEV gbl_tvs wev tvs = growEvVar gbl_tvs (wantedEvVarToVar wev) tvs - constrained_tvs = tyVarsOfWantedEvVars wanteds +growWanted gbl_tvs (WcEvVar wev) tvs + = growWantedEV gbl_tvs wev tvs +growWanted gbl_tvs (WcImplic implic) tvs + = foldrBag (growWanted inner_gbl_tvs) + (foldr (growEvVar inner_gbl_tvs) tvs (ic_given implic)) + -- Must grow over inner givens too + (ic_wanted implic) + where + inner_gbl_tvs = gbl_tvs `unionVarSet` ic_skols implic -------------------- quantifyMe :: TyVarSet -- Quantifying over these @@ -337,8 +375,37 @@ quantifyMe qtvs wev | otherwise = tyVarsOfPred pred `intersectsVarSet` qtvs where pred = wantedEvVarPred wev + +quantifyMeWC :: TyVarSet -> WantedConstraint -> Bool +-- False => we can *definitely* float the WantedConstraint out +quantifyMeWC qtvs (WcImplic implic) + = (tyVarsOfEvVars (ic_given implic) `intersectsVarSet` inner_qtvs) + || anyBag (quantifyMeWC inner_qtvs) (ic_wanted implic) + where + inner_qtvs = qtvs `minusVarSet` ic_skols implic + +quantifyMeWC qtvs (WcEvVar wev) + = quantifyMe qtvs wev \end{code} +Note [Avoid unecessary constraint simplification] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +When inferring the type of a let-binding, with simplifyInfer, +try to avoid unnecessariliy simplifying class constraints. +Doing so aids sharing, but it also helps with delicate +situations like + instance C t => C [t] where .. + f :: C [t] => .... + f x = let g y = ...(constraint C [t])... + in ... +When inferring a type for 'g', we don't want to apply the +instance decl, because then we can't satisfy (C t). So we +just notice that g isn't quantified over 't' and partition +the contraints before simplifying. + +This only half-works, but then let-generalisation only half-works. + + Note [Inheriting implicit parameters] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider this: @@ -403,9 +470,9 @@ simplifySuperClass self wanteds = do { wanteds <- mapBagM zonkWanted wanteds ; loc <- getCtLoc NoScSkol ; (unsolved, ev_binds) - <- runTcS SimplCheck emptyVarSet $ + <- runTcS SimplCheck NoUntouchables $ do { can_self <- canGivens loc [self] - ; let inert = foldlBag extendInertSet emptyInert can_self + ; let inert = foldlBag updInertSet emptyInert can_self -- No need for solveInteract; we know it's inert ; solveWanteds inert wanteds } @@ -512,7 +579,7 @@ simplifyRule name tv_bndrs lhs_wanted rhs_wanted ; rhs_binds_var@(EvBindsVar evb_ref _) <- newTcEvBinds ; loc <- getCtLoc (RuleSkol name) ; rhs_binds1 <- simplifyCheck SimplCheck $ unitBag $ WcImplic $ - Implic { ic_env_tvs = emptyVarSet -- No untouchables + Implic { ic_untch = NoUntouchables , ic_env = emptyNameEnv , ic_skols = mkVarSet tv_bndrs , ic_scoped = panic "emitImplication" @@ -556,7 +623,7 @@ simplifyCheck ctxt wanteds ; traceTc "simplifyCheck {" (vcat [ ptext (sLit "wanted =") <+> ppr wanteds ]) - ; (unsolved, ev_binds) <- runTcS ctxt emptyVarSet $ + ; (unsolved, ev_binds) <- runTcS ctxt NoUntouchables $ solveWanteds emptyInert wanteds ; traceTc "simplifyCheck }" $ @@ -581,10 +648,13 @@ solveWanteds inert wanteds , text "inert =" <+> ppr inert ] ; (unsolved_flats, unsolved_implics) <- simpl_loop 1 can_flats implic_wanteds + ; bb <- getTcEvBindsBag ; traceTcS "solveWanteds }" $ vcat [ text "wanteds =" <+> ppr wanteds , text "unsolved_flats =" <+> ppr unsolved_flats - , text "unsolved_implics =" <+> ppr unsolved_implics ] + , text "unsolved_implics =" <+> ppr unsolved_implics + , text "current evbinds =" <+> vcat (map ppr (varEnvElts bb)) + ] ; return (unsolved_flats, unsolved_implics) } where simpl_loop :: Int @@ -642,13 +712,17 @@ solveImplication :: InertSet -- Given -- -- Precondition: everything is zonked by now solveImplication inert - imp@(Implic { ic_env_tvs = untch - , ic_binds = ev_binds - , ic_skols = skols - , ic_given = givens + imp@(Implic { ic_untch = untch + , ic_binds = ev_binds + , ic_skols = skols + , ic_given = givens , ic_wanted = wanteds - , ic_loc = loc }) + , ic_loc = loc }) = nestImplicTcS ev_binds untch $ + recoverTcS (return (emptyBag, emptyBag)) $ + -- Recover from nested failures. Even the top level is + -- just a bunch of implications, so failing at the first + -- one is bad do { traceTcS "solveImplication {" (ppr imp) -- Solve flat givens @@ -753,13 +827,13 @@ applyDefaultingRules inert wanteds | isEmptyBag wanteds = return emptyBag | otherwise - = do { untch <- getUntouchablesTcS + = do { untch <- getUntouchables ; tv_cts <- mapM (defaultTyVar untch) $ - varSetElems (tyVarsOfCanonicals wanteds) + varSetElems (tyVarsOfCDicts wanteds) ; info@(_, default_tys, _) <- getDefaultInfo ; let groups = findDefaultableGroups info untch wanteds - ; deflt_cts <- mapM (disambigGroup default_tys untch inert) groups + ; deflt_cts <- mapM (disambigGroup default_tys inert) groups ; traceTcS "deflt2" (vcat [ text "Tyvar defaults =" <+> ppr tv_cts , text "Type defaults =" <+> ppr deflt_cts]) @@ -767,7 +841,7 @@ applyDefaultingRules inert wanteds ; return (unionManyBags deflt_cts `andCCan` unionManyBags tv_cts) } ------------------ -defaultTyVar :: TcTyVarSet -> TcTyVar -> TcS CanonicalCts +defaultTyVar :: Untouchables -> TcTyVar -> TcS CanonicalCts -- defaultTyVar is used on any un-instantiated meta type variables to -- default the kind of ? and ?? etc to *. This is important to ensure -- that instance declarations match. For example consider @@ -783,10 +857,9 @@ defaultTyVar :: TcTyVarSet -> TcTyVar -> TcS CanonicalCts -- whatever, because the type-class defaulting rules have yet to run. defaultTyVar untch the_tv - | isMetaTyVar the_tv - , not (the_tv `elemVarSet` untch) + | isTouchableMetaTyVar_InRange untch the_tv , not (k `eqKind` default_k) - = do { (ev, better_ty) <- TcSMonad.newKindConstraint (mkTyVarTy the_tv) default_k + = do { (ev, better_ty) <- TcSMonad.newKindConstraint the_tv default_k ; let loc = CtLoc DefaultOrigin (getSrcSpan the_tv) [] -- Yuk -- 'DefaultOrigin' is strictly the declaration, but it's convenient wanted_eq = CTyEqCan { cc_id = ev @@ -807,7 +880,7 @@ findDefaultableGroups :: ( SimplContext , [Type] , (Bool,Bool) ) -- (Overloaded strings, extended default rules) - -> TcTyVarSet -- Untouchable + -> Untouchables -- Untouchable -> CanonicalCts -- Unsolved -> [[(CanonicalCt,TcTyVar)]] findDefaultableGroups (ctxt, default_tys, (ovl_strings, extended_defaults)) @@ -834,7 +907,7 @@ findDefaultableGroups (ctxt, default_tys, (ovl_strings, extended_defaults)) is_defaultable_group ds@((_,tv):_) = isTyConableTyVar tv -- Note [Avoiding spurious errors] && not (tv `elemVarSet` bad_tvs) - && not (tv `elemVarSet` untch) -- Non untouchable + && isTouchableMetaTyVar_InRange untch tv && defaultable_classes [cc_class cc | (cc,_) <- ds] is_defaultable_group [] = panic "defaultable_group" @@ -856,15 +929,14 @@ findDefaultableGroups (ctxt, default_tys, (ovl_strings, extended_defaults)) ------------------------------ disambigGroup :: [Type] -- The default types - -> TcTyVarSet -- Untouchables -> InertSet -- Given inert -> [(CanonicalCt, TcTyVar)] -- All classes of the form (C a) -- sharing same type variable -> TcS CanonicalCts -disambigGroup [] _inert _untch _grp +disambigGroup [] _inert _grp = return emptyBag -disambigGroup (default_ty:default_tys) untch inert group +disambigGroup (default_ty:default_tys) inert group = do { traceTcS "disambigGroup" (ppr group $$ ppr default_ty) ; ev <- newGivOrDerCoVar (mkTyVarTy the_tv) default_ty default_ty -- Refl -- We know this equality is canonical, @@ -874,7 +946,7 @@ disambigGroup (default_ty:default_tys) untch inert group , cc_tyvar = the_tv , cc_rhs = default_ty } - ; success <- tryTcS (extendVarSet untch the_tv) $ + ; success <- tryTcS $ do { given_inert <- solveOne inert given_eq ; final_inert <- solveInteract given_inert (listToBag wanteds) ; let (_, unsolved) = extractUnsolved final_inert @@ -888,7 +960,7 @@ disambigGroup (default_ty:default_tys) untch inert group ; return (unitBag given_eq) } False -> -- Failure: try with the next type do { traceTcS "disambigGoup succeeded" (ppr default_ty) - ; disambigGroup default_tys untch inert group } } + ; disambigGroup default_tys inert group } } where ((the_ct,the_tv):_) = group wanteds = map fst group