From: dimitris@microsoft.com Date: Thu, 9 Dec 2010 14:12:15 +0000 (+0000) Subject: Moved canonicalisation inside solveInteract X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=commitdiff_plain;h=ef6d82a4e1d4ba4884c322be85cff291e017f0e6 Moved canonicalisation inside solveInteract Moreover canonicalisation now is "clever", i.e. it never canonicalizes a class constraint if it can already discharge it from some other inert or previously encountered constraints. See Note [Avoiding the superclass explosion] --- diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs index e1ea65f..aeb78d8 100644 --- a/compiler/typecheck/TcInteract.lhs +++ b/compiler/typecheck/TcInteract.lhs @@ -187,6 +187,8 @@ foldISEqCts k z IS { inert_eqs = eqs } = Bag.foldlBag k z eqs extractUnsolved :: InertSet -> (InertSet, CanonicalCts) +-- Postcondition: the canonical cts returnd are the very same as the +-- WantedEvVars in their canonical form. extractUnsolved is@(IS {inert_eqs = eqs}) = let is_solved = is { inert_eqs = solved_eqs , inert_dicts = solved_dicts @@ -397,11 +399,62 @@ React with (F Int ~ b) ==> IR Stop True [] -- after substituting we re-canoni -- returning an extended inert set. -- -- See Note [Touchables and givens]. -solveInteract :: InertSet -> CanonicalCts -> TcS InertSet +solveInteract :: InertSet -> Bag (CtFlavor,EvVar) -> TcS InertSet solveInteract inert ws = do { dyn_flags <- getDynFlags - ; solveInteractWithDepth (ctxtStkDepth dyn_flags,0,[]) inert ws - } + ; can_ws <- foldlBagM (tryPreSolveAndCanon inert) emptyCCan ws + ; solveInteractWithDepth (ctxtStkDepth dyn_flags,0,[]) inert can_ws } + +tryPreSolveAndCanon :: InertSet -> CanonicalCts -> (CtFlavor, EvVar) -> TcS CanonicalCts +-- Checks if this constraint can be immediately solved from a constraint in the +-- inert set or in the previously encountered CanonicalCts and only then +-- canonicalise it. See Note [Avoiding the superclass explosion] +tryPreSolveAndCanon is cts_acc (fl,ev_var) + | ClassP clas tys <- evVarPred ev_var + = do { let (relevant_inert_dicts,_) = getRelevantCts clas (inert_dicts is) + ; b <- dischargeFromCans (cts_acc `unionBags` relevant_inert_dicts) + (fl,ev_var,clas,tys) + ; extra_cts <- if b then return emptyCCan else mkCanonical fl ev_var + ; return (cts_acc `unionBags` extra_cts) } + | otherwise + = do { extra_cts <- mkCanonical fl ev_var + ; return (cts_acc `unionBags` extra_cts) } + +dischargeFromCans :: CanonicalCts -> (CtFlavor,EvVar,Class,[Type]) -> TcS Bool +dischargeFromCans cans (fl,ev,clas,tys) + = Bag.foldlBagM discharge_ct False cans + where discharge_ct :: Bool -> CanonicalCt -> TcS Bool + discharge_ct True _ct = return True + discharge_ct False (CDictCan { cc_id = ev1, cc_flavor = fl1 + , cc_class = clas1, cc_tyargs = tys1 }) + | clas1 == clas + , (and $ zipWith tcEqType tys tys1) + , fl1 `canSolve` fl + = setEvBind ev (EvId ev1) >> return True + discharge_ct False _ct = return False +\end{code} + +Note [Avoiding the superclass explosion] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Consider the example: + f = [(0,1,0,1,0)] +We have 5 wanted (Num alpha) constraints. If we simply try to canonicalize and add them +in our worklist, we will also get all of their superclasses as Derived, hence we will +have an inert set that contains 5*n constraints, where n is the number of superclasses +of of Num. That is bad for the additional reason that we keep *all* the Derived, even +for identical class constraints (for reasons related to recursive dictionaries). + +Instead, what we do with tryPreSolveAndCanon, is when we encounter a new constraint, +such as the second (Num alpha) above we very quickly see if it can be immediately +discharged by a class constraint in our inert set or the previous canonicals. If so, +we add nothing to the returned canonical constraints. + +For our particular example this will reduce the size of the inert set that we use from +5*n to just n. And hence the number of all possible interactions that we have to look +through is significantly smaller! + +\begin{code} solveOne :: InertSet -> WorkItem -> TcS InertSet solveOne inerts workItem = do { dyn_flags <- getDynFlags diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs index 7b7a9f4..0920a8b 100644 --- a/compiler/typecheck/TcSMonad.lhs +++ b/compiler/typecheck/TcSMonad.lhs @@ -181,8 +181,9 @@ data CanonicalCt compatKind :: Kind -> Kind -> Bool compatKind k1 k2 = k1 `isSubKind` k2 || k2 `isSubKind` k1 -makeGivens :: CanonicalCts -> CanonicalCts -makeGivens = mapBag (\ct -> ct { cc_flavor = mkGivenFlavor (cc_flavor ct) UnkSkol }) +makeGivens :: Bag WantedEvVar -> Bag (CtFlavor,EvVar) +makeGivens = mapBag (\(WantedEvVar ev wloc) -> (mkGivenFlavor (Wanted wloc) UnkSkol, ev)) +-- ct { cc_flavor = mkGivenFlavor (cc_flavor ct) UnkSkol }) -- The UnkSkol doesn't matter because these givens are -- not contradictory (else we'd have rejected them already) diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs index 0da5eec..b312d09 100644 --- a/compiler/typecheck/TcSimplify.lhs +++ b/compiler/typecheck/TcSimplify.lhs @@ -10,7 +10,6 @@ module TcSimplify( import HsSyn import TcRnMonad import TcErrors -import TcCanonical import TcMType import TcType import TcSMonad @@ -518,12 +517,11 @@ simplifySuperClass tvs inst_givens sc_dict (EvBind self_dict self_ev) -- with a Derived origin, which in turn triggers the -- goodRecEv recursive-evidence check ; setEvBind self_dict self_ev_with_dep - ; can_selfs <- mkCanonical (Derived want_loc DerSelf) self_dict - -- The rest is just like solveImplication - ; can_inst_givens <- mkCanonicals (Given giv_loc) inst_givens - ; inert <- solveInteract emptyInert $ - can_inst_givens `andCCan` can_selfs + ; let cts = mapBag (\d -> (Given giv_loc, d)) (listToBag inst_givens) + `snocBag` (Derived want_loc DerSelf, self_dict) + ; inert <- solveInteract emptyInert cts + ; solveWanteds inert wanted } -- For error reporting, conjure up a fake implication, @@ -705,12 +703,11 @@ solveWanteds :: InertSet -- Given -- out of one or more of the implications solveWanteds inert wanteds = do { let (flat_wanteds, implic_wanteds) = splitWanteds wanteds - ; can_flats <- canWanteds $ bagToList flat_wanteds ; traceTcS "solveWanteds {" $ vcat [ text "wanteds =" <+> ppr wanteds , text "inert =" <+> ppr inert ] ; (unsolved_flats, unsolved_implics) - <- simpl_loop 1 inert can_flats implic_wanteds + <- simpl_loop 1 inert flat_wanteds implic_wanteds ; bb <- getTcEvBindsBag ; tb <- getTcSTyBindsMap ; traceTcS "solveWanteds }" $ @@ -726,63 +723,66 @@ solveWanteds inert wanteds where simpl_loop :: Int -> InertSet - -> CanonicalCts -- May inlude givens (in the recursive call) + -> Bag WantedEvVar -> Bag Implication -> TcS (CanonicalCts, Bag Implication) - simpl_loop n inert can_ws implics + simpl_loop n inert work_items implics | n>10 - = trace "solveWanteds: loop" $ -- Always bleat + = trace "solveWanteds: loop" $ -- Always bleat do { traceTcS "solveWanteds: loop" (ppr inert) -- Bleat more informatively - ; return (can_ws, implics) } + + -- We don't want to call the canonicalizer on those wanted ev vars + -- so try one last time to solveInteract them + ; inert1 <- solveInteract inert $ + mapBag (\(WantedEvVar ev wloc) -> (Wanted wloc, ev)) work_items + ; let (_, unsolved_cans) = extractUnsolved inert1 + ; return (unsolved_cans, implics) } | otherwise = do { traceTcS "solveWanteds: simpl_loop start {" $ vcat [ text "n =" <+> ppr n - , text "can_ws =" <+> ppr can_ws + , text "work_items =" <+> ppr work_items , text "implics =" <+> ppr implics , text "inert =" <+> ppr inert ] - ; inert1 <- solveInteract inert can_ws - ; let (inert2, unsolved_flats) = extractUnsolved inert1 + ; inert1 <- solveInteract inert $ + mapBag (\(WantedEvVar ev wloc) -> (Wanted wloc,ev)) work_items + ; let (inert2, unsolved_cans) = extractUnsolved inert1 + unsolved_wevvars + = mapBag (\ct -> WantedEvVar (cc_id ct) (getWantedLoc ct)) unsolved_cans -- NB: Importantly, inerts2 may contain *more* givens than inert -- because of having solved equalities from can_ws ; traceTcS "solveWanteds: done flats" $ vcat [ text "inerts =" <+> ppr inert2 - , text "unsolved =" <+> ppr unsolved_flats ] + , text "unsolved =" <+> ppr unsolved_cans ] -- Go inside each implication ; (implic_eqs, unsolved_implics) - <- solveNestedImplications inert2 unsolved_flats implics + <- solveNestedImplications inert2 unsolved_wevvars implics -- Apply defaulting rules if and only if there -- no floated equalities. If there are, they may -- solve the remaining wanteds, so don't do defaulting. ; final_eqs <- if not (isEmptyBag implic_eqs) then return implic_eqs - else applyDefaultingRules inert2 unsolved_flats - - -- default_eqs are *givens*, so simpl_loop may - -- recurse with givens in the argument + else applyDefaultingRules inert2 unsolved_cans ; traceTcS "solveWanteds: simpl_loop end }" $ vcat [ text "final_eqs =" <+> ppr final_eqs - , text "unsolved_flats =" <+> ppr unsolved_flats + , text "unsolved_flats =" <+> ppr unsolved_cans , text "unsolved_implics =" <+> ppr unsolved_implics ] ; if isEmptyBag final_eqs then - return (unsolved_flats, unsolved_implics) + return (unsolved_cans, unsolved_implics) else - do { can_final_eqs <- canWanteds (Bag.bagToList final_eqs) - -- final eqs is *just* a bunch of WantedEvVars - ; simpl_loop (n+1) inert2 - (can_final_eqs `andCCan` unsolved_flats) unsolved_implics + simpl_loop (n+1) inert2 -- final_eqs are just some WantedEvVars + (final_eqs `unionBags` unsolved_wevvars) unsolved_implics -- Important: reiterate with inert2, not plainly inert -- because inert2 may contain more givens, as the result of solving - -- some wanteds in the incoming can_ws - } + -- some wanteds in the incoming can_ws } -solveNestedImplications :: InertSet -> CanonicalCts -> Bag Implication +solveNestedImplications :: InertSet -> Bag WantedEvVar -> Bag Implication -> TcS (Bag WantedEvVar, Bag Implication) solveNestedImplications inerts unsolved implics | isEmptyBag implics @@ -836,8 +836,10 @@ solveImplication tcs_untouchables inert do { traceTcS "solveImplication {" (ppr imp) -- Solve flat givens - ; can_givens <- canGivens loc givens - ; given_inert <- solveInteract inert can_givens +-- ; can_givens <- canGivens loc givens +-- ; let given_fl = Given loc + ; given_inert <- solveInteract inert $ + mapBag (\c -> (Given loc,c)) (listToBag givens) -- Simplify the wanteds ; (unsolved_flats, unsolved_implics) <- solveWanteds given_inert wanteds @@ -1096,7 +1098,7 @@ Basic plan behind applyDefaulting rules: \begin{code} applyDefaultingRules :: InertSet - -> CanonicalCts -- All wanteds + -> CanonicalCts -- All wanteds -> TcS (Bag WantedEvVar) -- All wanteds again! -- Return some *extra* givens, which express the -- type-class-default choice @@ -1212,16 +1214,12 @@ disambigGroup (default_ty:default_tys) inert group = do { traceTcS "disambigGroup" (ppr group $$ ppr default_ty) ; let ct_loc = get_ct_loc (cc_flavor the_ct) ; ev <- TcSMonad.newWantedCoVar (mkTyVarTy the_tv) default_ty - ; let wanted_eq = CTyEqCan { cc_id = ev - , cc_flavor = Wanted ct_loc - , cc_tyvar = the_tv - , cc_rhs = default_ty } ; success <- tryTcS $ - do { final_inert <- solveInteract inert(listToBag $ wanted_eq:wanteds) - ; let (_, unsolved) = extractUnsolved final_inert - ; errs <- getTcSErrorsBag + do { final_inert <- solveInteract inert $ + consBag (Wanted ct_loc, ev) wanted_to_solve + ; let (_, unsolved) = extractUnsolved final_inert + ; errs <- getTcSErrorsBag ; return (isEmptyBag unsolved && isEmptyBag errs) } - ; case success of True -> -- Success: record the type variable binding, and return do { wrapWarnTcS $ warnDefaulting wanted_ev_vars default_ty @@ -1232,8 +1230,10 @@ disambigGroup (default_ty:default_tys) inert group ; disambigGroup default_tys inert group } } where ((the_ct,the_tv):_) = group - wanteds = map fst group - wanted_ev_vars = map deCanonicaliseWanted wanteds + wanteds = map fst group + wanted_ev_vars = map deCanonicaliseWanted wanteds + wanted_to_solve = listToBag $ + map (\(WantedEvVar ev wloc) -> (Wanted wloc,ev)) wanted_ev_vars get_ct_loc (Wanted l) = l get_ct_loc _ = panic "Asked to disambiguate given or derived!"