Be a bit more selective about improvement

This patch makes [W] constraints not participate in
improvement.   See Note [Do not do improvement for WOnly]
in TcSMonad.

Removes some senseless work duplication in some cases (notably
Trac #12860); should not change behaviour.

2 files changed, 57 insertions, 6 deletions

diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs
index 4d49ede3c9..0ff7a976ab 100644
--- a/compiler/typecheck/TcInteract.hs
+++ b/compiler/typecheck/TcInteract.hs
@@ -728,25 +728,32 @@ interactDict _ wi = pprPanic "interactDict" (ppr wi)
 addFunDepWork :: InertCans -> CtEvidence -> Class -> TcS ()
 -- Add derived constraints from type-class functional dependencies.
 addFunDepWork inerts work_ev cls
+  | isImprovable work_ev
   = mapBagM_ add_fds (findDictsByClass (inert_dicts inerts) cls)
                -- No need to check flavour; fundeps work between
                -- any pair of constraints, regardless of flavour
                -- Importantly we don't throw workitem back in the
                -- worklist because this can cause loops (see #5236)
+  | otherwise
+  = return ()
   where
     work_pred = ctEvPred work_ev
     work_loc  = ctEvLoc work_ev
 
     add_fds inert_ct
+      | isImprovable inert_ev
       = emitFunDepDeriveds $
         improveFromAnother derived_loc inert_pred work_pred
                -- We don't really rewrite tys2, see below _rewritten_tys2, so that's ok
                -- NB: We do create FDs for given to report insoluble equations that arise
                -- from pairs of Givens, and also because of floating when we approximate
                -- implications. The relevant test is: typecheck/should_fail/FDsFromGivens.hs
+      | otherwise
+      = return ()
       where
-        inert_pred = ctPred inert_ct
-        inert_loc  = ctLoc inert_ct
+        inert_ev   = ctEvidence inert_ct
+        inert_pred = ctEvPred inert_ev
+        inert_loc  = ctEvLoc inert_ev
         derived_loc = work_loc { ctl_depth  = ctl_depth work_loc `maxSubGoalDepth`
                                               ctl_depth inert_loc
                                , ctl_origin = FunDepOrigin1 work_pred  work_loc
@@ -895,8 +902,11 @@ improveLocalFunEqs :: CtEvidence -> InertCans -> TyCon -> [TcType] -> TcTyVar
 -- Generate derived improvement equalities, by comparing
 -- the current work item with inert CFunEqs
 -- E.g.   x + y ~ z,   x + y' ~ z   =>   [D] y ~ y'
+--
+-- See Note [FunDep and implicit parameter reactions]
 improveLocalFunEqs work_ev inerts fam_tc args fsk
-  | isGiven work_ev   -- See Note [No FunEq improvement for Givens]
+  | isGiven work_ev -- See Note [No FunEq improvement for Givens]
+    || not (isImprovable work_ev)
   = return ()
 
   | not (null improvement_eqns)
@@ -943,7 +953,8 @@ improveLocalFunEqs work_ev inerts fam_tc args fsk
     -- See Note [Type inference for type families with injectivity]
     do_one_injective inj_args (CFunEqCan { cc_tyargs = inert_args
                                          , cc_fsk = ifsk, cc_ev = inert_ev })
-      | rhs `tcEqType` lookupFlattenTyVar ieqs ifsk
+      | isImprovable inert_ev
+      , rhs `tcEqType` lookupFlattenTyVar ieqs ifsk
       = mk_fd_eqns inert_ev $
             [ Pair arg iarg
             | (arg, iarg, True) <- zip3 args inert_args inj_args ]
@@ -1460,7 +1471,8 @@ reduce_top_fun_eq old_ev fsk (ax_co, rhs_ty)
 improveTopFunEqs :: CtEvidence -> TyCon -> [TcType] -> TcTyVar -> TcS ()
 -- See Note [FunDep and implicit parameter reactions]
 improveTopFunEqs ev fam_tc args fsk
-  | isGiven ev    -- See Note [No FunEq improvement for Givens]
+  | isGiven ev            -- See Note [No FunEq improvement for Givens]
+    || not (isImprovable ev)
   = return ()
 
   | otherwise
@@ -1824,7 +1836,8 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls
                     ; if isDerived fl then finish_derived theta
                                       else finish_wanted  theta mk_ev }
                NoInstance ->
-                 do { try_fundep_improvement
+                 do { when (isImprovable fl) $
+                      try_fundep_improvement
                     ; continueWith work_item } }
    where
      dict_pred   = mkClassPred cls xis
diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs
index 7665e440d5..aa7a6e1cf2 100644
--- a/compiler/typecheck/TcSMonad.hs
+++ b/compiler/typecheck/TcSMonad.hs
@@ -57,6 +57,7 @@ module TcSMonad (
     removeInertCts, getPendingScDicts,
     addInertCan, addInertEq, insertFunEq,
     emitInsoluble, emitWorkNC, emitWork,
+    isImprovable,
 
     -- The Model
     kickOutAfterUnification,
@@ -1148,6 +1149,37 @@ them.  If we forget the pend_sc flag, our cunning scheme for avoiding
 generating superclasses repeatedly will fail.
 
 See Trac #11379 for a case of this.
+
+Note [Do not do improvement for WOnly]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We do improvement between two constraints (e.g. for injectivity
+or functional dependencies) only if both are "improvable". And
+we improve a constraint wrt the top-level instances only if
+it is improveable.
+
+Improvable:     [G] [WD] [D}
+Not improvable: [W]
+
+Reasons:
+
+* It's less work: fewer pairs to compare
+
+* Every [W] has a shadow [D] so nothing is lost
+
+* Consider [WD] C Int b,  where 'b' is a skolem, and
+    class C a b | a -> b
+    instance C Int Bool
+  We'll do a fundep on it and emit [D] b ~ Bool
+  That will kick out constraint [WD] C Int b
+  Then we'll split it to [W] C Int b (keep in inert)
+                     and [D] C Int b (in work list)
+  When processing the latter we'll rewrite it to
+        [D] C Int Bool
+  At that point it would be /stupid/ to interact it
+  with the inert [W] C Int b in the inert set; after all,
+  it's the very constraint from which the [D] C Int Bool
+  was split!  We can avoid this by not doing improvement
+  on [W] constraints. This came up in Trac #12860.
 -}
 
 maybeEmitShadow :: InertCans -> Ct -> TcS Ct
@@ -1199,6 +1231,12 @@ intersects_with inert_eqs free_vars
       -- to the underlying UniqFM.  A bit yukky, but efficient.
 
 
+isImprovable :: CtEvidence -> Bool
+-- See Note [Do not do improvement for WOnly]
+isImprovable (CtWanted { ctev_nosh = WOnly }) = False
+isImprovable _                                = True
+
+
 {- *********************************************************************
 *                                                                      *
                    Inert equalities