[commit: ghc] wip/rae-new-coercible: Update Note [eqCanRewrite]; don't search in an EqualCtList (eac5875)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : wip/rae-new-coercible
Link       : http://ghc.haskell.org/trac/ghc/changeset/eac58758c488a0ec8ef9b697f196fd6177bdaa34/ghc

>---------------------------------------------------------------

commit eac58758c488a0ec8ef9b697f196fd6177bdaa34
Author: Richard Eisenberg <eir at cis.upenn.edu>
Date:   Mon Dec 8 12:11:50 2014 -0500

    Update Note [eqCanRewrite]; don't search in an EqualCtList


>---------------------------------------------------------------

eac58758c488a0ec8ef9b697f196fd6177bdaa34
 compiler/typecheck/TcFlatten.hs  | 20 +++++++++++---------
 compiler/typecheck/TcInteract.hs |  7 +++----
 compiler/typecheck/TcSMonad.hs   |  2 +-
 3 files changed, 15 insertions(+), 14 deletions(-)

diff --git a/compiler/typecheck/TcFlatten.hs b/compiler/typecheck/TcFlatten.hs
index 4a8b026..fa03499 100644
--- a/compiler/typecheck/TcFlatten.hs
+++ b/compiler/typecheck/TcFlatten.hs
@@ -32,7 +32,6 @@ import MonadUtils   ( zipWithAndUnzipM )
 import Bag
 import FastString
 import Control.Monad( when, liftM )
-import Data.List ( find )
 
 {-
 Note [The flattening story]
@@ -952,12 +951,10 @@ flattenTyVarOuter fmode tv
     -- See Note [Applying the inert substitution]
     do { ieqs <- getInertEqs
        ; case lookupVarEnv ieqs tv of
-           Just cts
-               -- we need to search for one that can rewrite, because you
-               -- can have, for example, a Derived among a bunch of Wanteds
-             | Just (CTyEqCan { cc_ev = ctev, cc_tyvar = tv, cc_rhs = rhs_ty })
-                 <- find ((`eqCanRewriteFR` feFlavourRole fmode)
-                          . ctFlavourRole) cts
+           Just (ct:_)   -- If the first doesn't work,
+                         -- the subsequent ones won't either
+             | CTyEqCan { cc_ev = ctev, cc_tyvar = tv, cc_rhs = rhs_ty } <- ct
+             , ctev `eqCanRewrite` ctxt_ev
              ->  do { traceTcS "Following inert tyvar" (ppr tv <+> equals <+> ppr rhs_ty $$ ppr ctev)
                     ; let rewrite_co1 = mkTcSymCo (ctEvCoercion ctev)
                           rewrite_co = case (ctEvEqRel ctev, fe_eq_rel fmode) of
@@ -1193,8 +1190,6 @@ canRewriteOrSame ev1 ev2 = ev1 `eqCanRewrite` ev2 ||
 {-
 Note [eqCanRewrite]
 ~~~~~~~~~~~~~~~~~~~
-TODO (RAE): Update this note!
-
 (eqCanRewrite ct1 ct2) holds if the constraint ct1 (a CTyEqCan of form
 tv ~ ty) can be used to rewrite ct2.
 
@@ -1203,6 +1198,7 @@ The EqCanRewrite Property:
                             then a eqCanRewrite a
   This is what guarantees that canonicalisation will terminate.
   See Note [Applying the inert substitution]
+  But this isn't the whole story; see Note [Flattener smelliness]
 
 At the moment we don't allow Wanteds to rewrite Wanteds, because that can give
 rise to very confusing type error messages.  A good example is Trac #8450.
@@ -1214,6 +1210,12 @@ Here we get
   [W] a ~ Bool
 but we do not want to complain about Bool ~ Char!
 
+Accordingly, we also don't let Deriveds rewrite Deriveds.
+
+With the solver handling Coercible constraints like equality constraints,
+the rewrite conditions must take role into account, never allowing
+a representational equality to rewrite a nominal one.
+
 Note [canRewriteOrSame]
 ~~~~~~~~~~~~~~~~~~~~~~~
 canRewriteOrSame is similar but
diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs
index d4f14d1..b0644a3 100644
--- a/compiler/typecheck/TcInteract.hs
+++ b/compiler/typecheck/TcInteract.hs
@@ -700,10 +700,9 @@ lookupFlattenTyVar :: TyVarEnv EqualCtList -> TcTyVar -> TcType
 -- ^ Look up a flatten-tyvar in the inert nominal TyVarEqs;
 -- this is used only when dealing with a CFunEqCan
 lookupFlattenTyVar inert_eqs ftv
-    -- TODO (RAE): This is fishy. Why only return one equality?
-  = case lookupVarEnv inert_eqs ftv >>= find ((== NomEq) . ctEqRel) of
-      Just (CTyEqCan { cc_rhs = rhs }) -> rhs
-      _                                -> mkTyVarTy ftv
+  = case lookupVarEnv inert_eqs ftv of
+      Just (CTyEqCan { cc_rhs = rhs, cc_eq_rel = NomEq } : _) -> rhs
+      _                                                       -> mkTyVarTy ftv
 
 reactFunEq :: CtEvidence -> TcTyVar    -- From this  :: F tys ~ fsk1
            -> CtEvidence -> TcTyVar    -- Solve this :: F tys ~ fsk2
diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs
index 55f75c8..3cd14c5 100644
--- a/compiler/typecheck/TcSMonad.hs
+++ b/compiler/typecheck/TcSMonad.hs
@@ -381,7 +381,7 @@ Note [EqualCtList invariants]
 
  From the fourth invariant it follows that the list is
    - A single Given, or
-   - Any number of Wanteds, along with 0 or 1 Derived
+   - Any number of Wanteds and/or Deriveds
 -}
 
 -- The Inert Set