[commit: ghc] master: Comments in Note [Efficient orientation] about interacting CFunEqCans (b6acaf0)
Simon Peyton Jones <[email protected]>
| Newsgroups | gmane.comp.lang.haskell.cvs.ghc |
|---|---|
| Message-ID | <[email protected]> |
Repository : ssh://darcs.haskell.org//srv/darcs/ghc On branch : master http://hackage.haskell.org/trac/ghc/changeset/b6acaf08ff5740ecd9349db530db3b911badb71a >--------------------------------------------------------------- commit b6acaf08ff5740ecd9349db530db3b911badb71a Author: Simon Peyton Jones <[email protected]> Date: Fri Oct 26 11:05:57 2012 +0100 Comments in Note [Efficient orientation] about interacting CFunEqCans >--------------------------------------------------------------- compiler/typecheck/TcInteract.lhs | 48 +++++++++++++++++++----------------- compiler/typecheck/TcRnTypes.lhs | 16 +++++++---- 2 files changed, 35 insertions(+), 29 deletions(-) diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs index d6044d0..a75890f 100644 --- a/compiler/typecheck/TcInteract.lhs +++ b/compiler/typecheck/TcInteract.lhs @@ -236,26 +236,6 @@ thePipeline = [ ("canonicalization", TcCanonical.canonicalize) * * ********************************************************************************* -Note [Efficient Orientation] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -There are two cases where we have to be careful about -orienting equalities to get better efficiency. - -Case 1: In Rewriting Equalities (function rewriteEqLHS) - - When rewriting two equalities with the same LHS: - (a) (tv ~ xi1) - (b) (tv ~ xi2) - We have a choice of producing work (xi1 ~ xi2) (up-to the - canonicalization invariants) However, to prevent the inert items - from getting kicked out of the inerts first, we prefer to - canonicalize (xi1 ~ xi2) if (b) comes from the inert set, or (xi2 - ~ xi1) if (a) comes from the inert set. - -Case 2: Functional Dependencies - Again, we should prefer, if possible, the inert variables on the RHS - \begin{code} spontaneousSolveStage :: SimplifierStage spontaneousSolveStage workItem @@ -723,8 +703,8 @@ doInteractWithInert ii@(CFunEqCan { cc_ev = ev1, cc_fun = tc1 xdecomp x = [EvCoercion (mk_sym_co x `mkTcTransCo` co1)] ; ctevs <- xCtFlavor ev2 [mkTcEqPred xi2 xi1] xev - -- No caching! See Note [Cache-caused loops] - -- Why not (mkTcEqPred xi1 xi2)? See Note [Efficient orientation] + -- No caching! See Note [Cache-caused loops] + -- Why not (mkTcEqPred xi1 xi2)? See Note [Efficient orientation] ; emitWorkNC d2 ctevs ; return (IRWorkItemConsumed "FunEq/FunEq") } @@ -742,7 +722,7 @@ doInteractWithInert ii@(CFunEqCan { cc_ev = ev1, cc_fun = tc1 xdecomp x = [EvCoercion (mkTcSymCo co2 `mkTcTransCo` evTermCoercion x)] ; ctevs <- xCtFlavor ev1 [mkTcEqPred xi2 xi1] xev - -- Why not (mkTcEqPred xi1 xi2)? See Note [Efficient orientation] + -- Why not (mkTcEqPred xi1 xi2)? See Note [Efficient orientation] ; emitWorkNC d1 ctevs ; return (IRInertConsumed "FunEq/FunEq") } @@ -761,6 +741,28 @@ doInteractWithInert ii@(CFunEqCan { cc_ev = ev1, cc_fun = tc1 doInteractWithInert _ _ = return (IRKeepGoing "NOP") \end{code} +Note [Efficient Orientation] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Suppose we are interacting two FunEqCans with the same LHS: + (inert) ci :: (F ty ~ xi_i) + (work) cw :: (F ty ~ xi_w) +We prefer to keep the inert (else we pass the work item on down +the pipeline, which is a bit silly). If we keep the inert, we +will (a) discharge 'cw' + (b) produce a new equality work-item (xi_w ~ xi_i) +Notice the orientation (xi_w ~ xi_i) NOT (xi_i ~ xi_w): + new_work :: xi_w ~ xi_i + cw := ci ; sym new_work +Why? Consider the simplest case when xi1 is a type variable. If +we generate xi1~xi2, porcessing that constraint will kick out 'ci'. +If we generate xi2~xi1, there is less chance of that happening. +Of course it can and should still happen if xi1=a, xi1=Int, say. +But we want to avoid it happening needlessly. + +Similarly, if we *can't* keep the inert item (because inert is Wanted, +and work is Given, say), we prefer to orient the new equality (xi_i ~ +xi_w). + Note [Carefully solve the right CFunEqCan] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider the constraints diff --git a/compiler/typecheck/TcRnTypes.lhs b/compiler/typecheck/TcRnTypes.lhs index 42e9d55..9c5249a 100644 --- a/compiler/typecheck/TcRnTypes.lhs +++ b/compiler/typecheck/TcRnTypes.lhs @@ -909,10 +909,14 @@ data Ct Note [Ct/evidence invariant] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ If ct :: Ct, then extra fields of 'ct' cache precisely the ctev_pred field -of (cc_ev ct). Eg for CDictCan, +of (cc_ev ct), and is fully rewritten wrt the substitution. Eg for CDictCan, ctev_pred (cc_ev ct) = (cc_class ct) (cc_tyargs ct) This holds by construction; look at the unique place where CDictCan is -built (in TcCanonical) +built (in TcCanonical). + +In contrast, the type of the evidence *term* (ccev_evtm or ctev_evar) in +the evidence may *not* be fully zonked; we are careful not to look at it +during constraint solving. Seee Note [Evidence field of CtEvidence] \begin{code} mkNonCanonical :: CtLoc -> CtEvidence -> Ct @@ -1228,13 +1232,13 @@ may be un-zonked. \begin{code} data CtEvidence - = CtGiven { ctev_pred :: TcPredType - , ctev_evtm :: EvTerm } -- See Note [Evidence field of CtEvidence] + = CtGiven { ctev_pred :: TcPredType -- See Note [Ct/evidence invariant] + , ctev_evtm :: EvTerm } -- See Note [Evidence field of CtEvidence] -- Truly given, not depending on subgoals -- NB: Spontaneous unifications belong here - | CtWanted { ctev_pred :: TcPredType - , ctev_evar :: EvVar } -- See Note [Evidence field of CtEvidence] + | CtWanted { ctev_pred :: TcPredType -- See Note [Ct/evidence invariant] + , ctev_evar :: EvVar } -- See Note [Evidence field of CtEvidence] -- Wanted goal | CtDerived { ctev_pred :: TcPredType }