Comments in Note [Efficient orientation] about interacting CFunEqCans

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

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 }