diff options
author | Richard Eisenberg <eir@cis.upenn.edu> | 2014-12-08 12:11:50 -0500 |
---|---|---|
committer | Richard Eisenberg <eir@cis.upenn.edu> | 2014-12-08 12:11:50 -0500 |
commit | eac58758c488a0ec8ef9b697f196fd6177bdaa34 (patch) | |
tree | f96405265a8e28111ccdc97a1b7f23223a753d66 | |
parent | 1383e0d72788959c8be9877b7c451e6f271d61f0 (diff) | |
download | haskell-eac58758c488a0ec8ef9b697f196fd6177bdaa34.tar.gz |
Update Note [eqCanRewrite]; don't search in an EqualCtList
-rw-r--r-- | compiler/typecheck/TcFlatten.hs | 20 | ||||
-rw-r--r-- | compiler/typecheck/TcInteract.hs | 7 | ||||
-rw-r--r-- | 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 4a8b026f9f..fa03499ea0 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 d4f14d150b..b0644a3e5a 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 55f75c821b..3cd14c5958 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 |