Revise the inert-set invariants again

In particular this patch

- Accepts that rewriting with the inert CTyEqCans should be done recursively
  (hence removing the Bool result from flattenTyVarOuter)

- Refines the kick-out criterion, in paticular to avoid kick-out of (a -f-> ty)
  when f cannot rewrite f.  This is true of Wanteds and hence reduces kick-outs
  of Wanteds, perhaps by a lot

This stuff is not fully documented because the details are still settling, but
it's looking good.

(And it validates.)

This patch includes the testsuite wibbles.  perf/compiler/T5030 and
T5837 both improve in bytes-allocated (by 11% and 13% resp), which is
good.  I'm not sure which of today's short series of patches is
responsible, nor do I mind much.  (One could find out if necessary.)

8 files changed, 52 insertions, 24 deletions

diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index 5232e77782..13aa8e724f 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -670,7 +670,7 @@ canEqTyVar ev swapped tv1 ty2 ps_ty2              -- ev :: tv ~ s2
   = do { traceTcS "canEqTyVar" (ppr tv1 $$ ppr ty2 $$ ppr swapped)
        ; mb_yes <- flattenTyVarOuter ev tv1
        ; case mb_yes of
-           Right (ty1, co1, _) -- co1 :: ty1 ~ tv1
+           Right (ty1, co1)  -- co1 :: ty1 ~ tv1
                      -> do { mb <- rewriteEqEvidence ev swapped  ty1 ps_ty2
                                                      co1 (mkTcNomReflCo ps_ty2)
                            ; traceTcS "canEqTyVar2" (vcat [ppr tv1, ppr ty2, ppr swapped, ppr ty1,
diff --git a/compiler/typecheck/TcFlatten.hs b/compiler/typecheck/TcFlatten.hs
index 10adc9432a..01d5a101ab 100644
--- a/compiler/typecheck/TcFlatten.hs
+++ b/compiler/typecheck/TcFlatten.hs
@@ -826,11 +826,7 @@ flattenTyVar fmode tv
                     where
                        ty' = mkTyVarTy tv'
 
-           Right (ty1, co1, True)   -- No need to recurse
-                    -> do { traceTcS "flattenTyVar2" (ppr tv $$ ppr ty1)
-                          ; return (ty1, co1) }
-
-           Right (ty1, co1, False)  -- Recurse
+           Right (ty1, co1)  -- Recurse
                     -> do { (ty2, co2) <- flatten fmode ty1
                           ; traceTcS "flattenTyVar3" (ppr tv $$ ppr ty2)
                           ; return (ty2, co2 `mkTcTransCo` co1) }
@@ -838,14 +834,13 @@ flattenTyVar fmode tv
 
 flattenTyVarOuter, flattenTyVarFinal
    :: CtEvidence -> TcTyVar
-   -> TcS (Either TyVar (TcType, TcCoercion, Bool))
+   -> TcS (Either TyVar (TcType, TcCoercion))
 -- Look up the tyvar in
 --   a) the internal MetaTyVar box
 --   b) the tyvar binds
 --   c) the inerts
--- Return (Left tv')                if it is not found, tv' has a properly zonked kind
---        (Right (ty, co, is_flat)) if found, with co :: ty ~ tv;
---                                  is_flat says if the result is guaranteed flattened
+-- Return (Left tv')      if it is not found, tv' has a properly zonked kind
+--        (Right (ty, co) if found, with co :: ty ~ tv;
 
 flattenTyVarOuter ctxt_ev tv
   | not (isTcTyVar tv)             -- Happens when flatten under a (forall a. ty)
@@ -854,7 +849,7 @@ flattenTyVarOuter ctxt_ev tv
   = do { mb_ty <- isFilledMetaTyVar_maybe tv
        ; case mb_ty of {
            Just ty -> do { traceTcS "Following filled tyvar" (ppr tv <+> equals <+> ppr ty)
-                         ; return (Right (ty, mkTcNomReflCo ty, False)) } ;
+                         ; return (Right (ty, mkTcNomReflCo ty)) } ;
            Nothing ->
 
     -- Try in the inert equalities
@@ -866,7 +861,7 @@ flattenTyVarOuter ctxt_ev tv
              | CTyEqCan { cc_ev = ctev, cc_tyvar = tv, cc_rhs = rhs_ty } <- ct
              , eqCanRewrite ctev ctxt_ev
              ->  do { traceTcS "Following inert tyvar" (ppr tv <+> equals <+> ppr rhs_ty $$ ppr ctev)
-                    ; return (Right (rhs_ty, mkTcSymCo (ctEvCoercion ctev), True)) }
+                    ; return (Right (rhs_ty, mkTcSymCo (ctEvCoercion ctev))) }
                     -- NB: ct is Derived then (fe_ev fmode) must be also, hence
                     -- we are not going to touch the returned coercion
                     -- so ctEvCoercion is fine.
@@ -884,9 +879,12 @@ flattenTyVarFinal ctxt_ev tv
 {-
 Note [Applying the inert substitution]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+  -- NB: 8 Dec 14: These notes are now not correct
+  --               Need to rewrite then when matters have settled
+
 The inert CTyEqCans (a ~ ty), inert_eqs, can be treated as a
 substitution, and indeed flattenTyVarOuter applies it to the type
-being flattened.  It has the following properties:
+being flattened (recursively).  This process should terminate.
 
  * 'a' is not in fvs(ty)
  * They are *inert*; that is the eqCanRewrite relation is everywhere false
diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs
index a9ed64acfb..c6e9fb6324 100644
--- a/compiler/typecheck/TcInteract.hs
+++ b/compiler/typecheck/TcInteract.hs
@@ -42,7 +42,7 @@ import Data.List( partition, foldl', deleteFirstsBy )
 
 import VarEnv
 
-import Control.Monad( when, unless, forM, foldM )
+import Control.Monad
 import Pair (Pair(..))
 import Unique( hasKey )
 import FastString ( sLit )
@@ -952,7 +952,9 @@ kickOutRewritable new_ev new_tv
        ; unless (isEmptyWorkList kicked_out) $
          csTraceTcS $
          hang (ptext (sLit "Kick out, tv =") <+> ppr new_tv)
-            2 (ppr kicked_out)
+            2 (vcat [ text "n-kicked =" <+> int (workListSize kicked_out)
+                    , text "n-kept fun-eqs =" <+> int (sizeFunEqMap (inert_funeqs ics'))
+                    , ppr kicked_out ])
        ; return (workListSize kicked_out) }
 
 kick_out :: CtEvidence -> TcTyVar -> InertCans -> (WorkList, InertCans)
@@ -987,8 +989,10 @@ kick_out new_ev new_tv (IC { inert_eqs = tv_eqs
       -- Kick out even insolubles; see Note [Kick out insolubles]
 
     kick_out_ct :: Ct -> Bool
-    kick_out_ct ct =  eqCanRewrite new_ev (ctEvidence ct)
-                   && new_tv `elemVarSet` tyVarsOfCt ct
+    kick_out_ct ct = kick_out_ctev (ctEvidence ct)
+
+    kick_out_ctev ev =  eqCanRewrite new_ev ev
+                     && new_tv `elemVarSet` tyVarsOfType (ctEvPred ev)
          -- See Note [Kicking out inert constraints]
 
     kick_out_irred :: Ct -> Bool
@@ -1003,7 +1007,17 @@ kick_out new_ev new_tv (IC { inert_eqs = tv_eqs
                                []      -> acc_in
                                (eq1:_) -> extendVarEnv acc_in (cc_tyvar eq1) eqs_in)
       where
-        (eqs_out, eqs_in) = partition kick_out_ct eqs
+        (eqs_out, eqs_in) = partition kick_out_eq eqs
+
+    kick_out_eq (CTyEqCan { cc_tyvar = tv, cc_rhs = rhs_ty, cc_ev = ev })
+       =  eqCanRewrite new_ev ev
+       && (tv == new_tv
+           || (ev `eqCanRewrite` ev && new_tv `elemVarSet` tyVarsOfType rhs_ty)
+           || case getTyVar_maybe rhs_ty of { Just tv_r -> tv_r == new_tv; Nothing -> False })
+    kick_out_eq ct = pprPanic "kick_out_eq" (ppr ct)
+    -- SLPJ new piece: Don't kick out a constraint unless it can rewrite itself,
+    --                 If not, it can't rewrite anything else, so no point in
+    --                 kicking it out
 
 {-
 Note [Kicking out inert constraints]
diff --git a/testsuite/tests/indexed-types/should_compile/GADT1.hs b/testsuite/tests/indexed-types/should_compile/GADT1.hs
index 7761eafe97..5d09713c9b 100644
--- a/testsuite/tests/indexed-types/should_compile/GADT1.hs
+++ b/testsuite/tests/indexed-types/should_compile/GADT1.hs
@@ -25,3 +25,17 @@ plus_zero Zero = EQUIV
 plus_zero (Succ n) = case plus_zero n of
                        EQUIV -> EQUIV 
 
+{-
+
+From Succ branch of plus_zero
+
+[G] n ~ SUCC n1     -- n1 existentially bound
+[G] PLUS n1 ZERO ~ n1
+
+[W] PLUS n ZERO ~ n
+
+--> [W] PLUS (SUCC n1) ZERO ~ SUCC n1
+--> [W] SUCC (PLUS n1 ZERO) ~ SUCC n1
+--> [W] SUCC n1 ~ SUCC n1
+
+-}
\ No newline at end of file
diff --git a/testsuite/tests/perf/compiler/all.T b/testsuite/tests/perf/compiler/all.T
index 4add8e4bf0..0023ce83c1 100644
--- a/testsuite/tests/perf/compiler/all.T
+++ b/testsuite/tests/perf/compiler/all.T
@@ -314,7 +314,7 @@ test('T5030',
            # previous:    196457520
            # 2012-10-08:  259547660 (x86/Linux, new codegen)
            # 2013-11-21:  198573456 (x86 Windows, 64 bit machine)
-           (wordsize(64), 385152728, 10)]),
+           (wordsize(64), 340969128, 10)]),
              # Previously 530000000 (+/- 10%)
              # 17/1/13:   602993184  (x86_64/Linux)
              #            (new demand analyser)
@@ -327,6 +327,7 @@ test('T5030',
              # 2014-07-17 409314320  (amd64/Linux)
              # general round of updates
              # 2014-09-10 385152728  post-AMP-cleanup
+             # 2014-12-08 340969128  constraint solver perf improvements (esp kick-out)
 
        only_ways(['normal'])
       ],
@@ -464,7 +465,7 @@ test('T5837',
              # 2014-09-03: 37096484  (Windows laptop, w/w for INLINABLE things
              # 2014-12-01: 135914136 (Windows laptop, regression see below)
  
-           (wordsize(64), 271028976, 10)])
+           (wordsize(64), 234790312, 10)])
              # sample: 3926235424 (amd64/Linux, 15/2/2012)
              # 2012-10-02 81879216
              # 2012-09-20 87254264 amd64/Linux
@@ -475,6 +476,7 @@ test('T5837',
              # 2014-10-08 73639840 amd64/Linux, Burning Bridges and other small changes
              # 2014-11-06 271028976       Linux, Accept big regression;
              #   See Note [An alternative story for the inert substitution] in TcFlatten
+             # 2014-12-08 234790312 Constraint solver perf improvements (esp kick-out)
       ],
       compile_fail,['-ftype-function-depth=50'])
 
diff --git a/testsuite/tests/typecheck/should_fail/FrozenErrorTests.stderr b/testsuite/tests/typecheck/should_fail/FrozenErrorTests.stderr
index d8bec07269..1261408eb8 100644
--- a/testsuite/tests/typecheck/should_fail/FrozenErrorTests.stderr
+++ b/testsuite/tests/typecheck/should_fail/FrozenErrorTests.stderr
@@ -27,7 +27,7 @@ FrozenErrorTests.hs:29:15:
     In an equation for ‘test2’: test2 = goo2 (goo1 False undefined)
 
 FrozenErrorTests.hs:30:9:
-    Couldn't match type ‘Int’ with ‘[Int]’
+    Couldn't match type ‘[Int]’ with ‘Int’
     Expected type: [[Int]]
       Actual type: F [Int] Bool
     In the expression: goo1 False (goo2 undefined)
diff --git a/testsuite/tests/typecheck/should_fail/T7856.hs b/testsuite/tests/typecheck/should_fail/T7856.hs
index 825bc0bd2f..21bd41701d 100644
--- a/testsuite/tests/typecheck/should_fail/T7856.hs
+++ b/testsuite/tests/typecheck/should_fail/T7856.hs
@@ -6,8 +6,8 @@ tmp = sequence_ lst
 
 -- sequence_ :: Monad m => [m a] -> m ()
 
-{-    m () ~ (->) String (IO ())
-      m a  ~ IO ()
+{-    m () ~ (->) String (IO ())    -- From result of sequence_
+      m a  ~ IO ()                  -- From argument of sequence_
 
 Depends which one gets treated first.
   m := IO 
diff --git a/testsuite/tests/typecheck/should_fail/T8603.stderr b/testsuite/tests/typecheck/should_fail/T8603.stderr
index d9d2aafd53..4e79b012a9 100644
--- a/testsuite/tests/typecheck/should_fail/T8603.stderr
+++ b/testsuite/tests/typecheck/should_fail/T8603.stderr
@@ -16,7 +16,7 @@ T8603.hs:29:17:
            return False }
 
 T8603.hs:29:22:
-    Couldn't match type ‘StateT s RV t0’ with ‘RV a0’
+    Couldn't match type ‘RV a0’ with ‘StateT s RV t0’
     Expected type: [a0] -> StateT s RV t0
       Actual type: [a0] -> RV a0
     Relevant bindings include