Commit ef6d82a4 authored by dimitris@microsoft.com's avatar dimitris@microsoft.com
Browse files

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]
parent 4f7d5513
......@@ -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
......
......@@ -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)
......
......@@ -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!"
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment