A few more constraint solver improvements

* Get rid of the lookupInInerts stage

* Re-introduce the flat-cache for flattening type-family equations
  See Note [Type family equations] in TcSMonad. My previous clever attempt
  with organising the work list proved too fragile.

  There's a (static) flag -fno-flat-cache to switch if off,
  so you can try with and without

* Improve the -ddump-cs-trace output

* The usual round of refactoring

5 files changed, 198 insertions, 150 deletions

diff --git a/compiler/main/StaticFlagParser.hs b/compiler/main/StaticFlagParser.hs
index 36b32fa45f..aa1cd1b8f1 100644
--- a/compiler/main/StaticFlagParser.hs
+++ b/compiler/main/StaticFlagParser.hs
@@ -131,6 +131,7 @@ isStaticFlag f =
     "fruntime-types",
     "fno-pre-inlining",
     "fno-opt-coercion",
+    "fno-flat-cache",
     "fexcess-precision",
     "fhardwire-lib-paths",
     "fcpr-off",
diff --git a/compiler/main/StaticFlags.hs b/compiler/main/StaticFlags.hs
index 3165c6944b..fa4b61e287 100644
--- a/compiler/main/StaticFlags.hs
+++ b/compiler/main/StaticFlags.hs
@@ -48,6 +48,7 @@ module StaticFlags (
 	opt_SimplExcessPrecision,
 	opt_NoOptCoercion,
 	opt_MaxWorkerArgs,
+        opt_NoFlatCache,
 
 	-- Unfolding control
 	opt_UF_CreationThreshold,
@@ -243,6 +244,9 @@ opt_SimplExcessPrecision	= lookUp  (fsLit "-fexcess-precision")
 opt_NoOptCoercion :: Bool
 opt_NoOptCoercion    	        = lookUp  (fsLit "-fno-opt-coercion")
 
+opt_NoFlatCache :: Bool
+opt_NoFlatCache    	        = lookUp  (fsLit "-fno-flat-cache")
+
 -- Unfolding control
 -- See Note [Discounts and thresholds] in CoreUnfold
 
diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs
index a966a39f4e..33c62dcc15 100644
--- a/compiler/typecheck/TcCanonical.lhs
+++ b/compiler/typecheck/TcCanonical.lhs
@@ -532,9 +532,8 @@ flatten loc f ctxt (TyConApp tc tys)
                FMFullFlatten -> 
                  do { mb_ct <- lookupFlatEqn fam_ty
                     ; case mb_ct of
-                        Just ct 
-                          | let ctev = cc_ev ct
-                                flav = ctEvFlavour ctev
+                        Just (ctev, rhs_ty)
+                          | let flav = ctEvFlavour ctev
                           , flav `canRewrite` ctxt 
                           -> -- You may think that we can just return (cc_rhs ct) but not so. 
                              --            return (mkTcCoVarCo (ctId ct), cc_rhs ct, []) 
@@ -544,40 +543,21 @@ flatten loc f ctxt (TyConApp tc tys)
                              -- cache as well when we interact an equality with the inert. 
                              -- The design choice is: do we keep the flat cache rewritten or not?
                              -- For now I say we don't keep it fully rewritten.
-                            do { traceTcS "flatten/flat-cache hit" $ ppr ct
-                               ; let rhs_xi = cc_rhs ct
-                               ; (flat_rhs_xi,co) <- flatten (cc_loc ct) f flav rhs_xi
+                            do { traceTcS "flatten/flat-cache hit" $ ppr ctev
+                               ; (rhs_xi,co) <- flatten loc f flav rhs_ty
                                ; let final_co = evTermCoercion (ctEvTerm ctev)
                                                 `mkTcTransCo` mkTcSymCo co
-                               ; return (final_co, flat_rhs_xi) }
+                               ; return (final_co, rhs_xi) }
                           
-                        _ | Given <- ctxt -- Given: make new flatten skolem
-                          -> do { traceTcS "flatten/flat-cache miss" $ empty 
-                                ; rhs_ty <- newFlattenSkolemTy fam_ty
-                                ; let co     = mkTcReflCo fam_ty
-                                      new_ev = CtGiven { ctev_pred = mkTcEqPred fam_ty rhs_ty
-                                                       , ctev_evtm = EvCoercion co }
-                                      ct = CFunEqCan { cc_ev = new_ev
-                                                     , cc_fun    = tc 
-                            			     , cc_tyargs = xi_args    
-                            			     , cc_rhs    = rhs_ty
-                            			     , cc_loc  = loc }
+                        _ -> do { traceTcS "flatten/flat-cache miss" $ ppr fam_ty
+                                ; (ctev, rhs_xi) <- newFlattenSkolem ctxt fam_ty
+                                ; let ct = CFunEqCan { cc_ev     = ctev
+                                                     , cc_fun    = tc
+                                                     , cc_tyargs = xi_args
+                                                     , cc_rhs    = rhs_xi
+                                                     , cc_loc    = loc }
                                 ; updWorkListTcS $ extendWorkListFunEq ct
-                                ; return (co, rhs_ty) }
-
-                         | otherwise -- Wanted or Derived: make new unification variable
-                         -> do { traceTcS "flatten/flat-cache miss" $ empty 
-                               ; rhs_xi_var <- newFlexiTcSTy (typeKind fam_ty)
-                               ; ctev <- newWantedEvVarNC (mkTcEqPred fam_ty rhs_xi_var)
-                                   -- NC (no-cache) version because we've already
-                                   -- looked in the solved goals an inerts (lookupFlatEqn)
-                               ; let ct = CFunEqCan { cc_ev = ctev
-                                                    , cc_fun = tc
-                                                    , cc_tyargs = xi_args
-                                                    , cc_rhs    = rhs_xi_var 
-                                                    , cc_loc    = loc }
-                               ; updWorkListTcS $ extendWorkListFunEq ct
-                               ; return (evTermCoercion (ctEvTerm ctev), rhs_xi_var) }
+                                ; return (evTermCoercion (ctEvTerm ctev), rhs_xi) }
                     }
                   -- Emit the flat constraints
          ; return ( mkAppTys rhs_xi xi_rest -- NB mkAppTys: rhs_xi might not be a type variable
@@ -1140,9 +1120,9 @@ canEqLeafFunEq loc ev fn tys1 ty2  -- ev :: F tys1 ~ ty2
        ; mb <- rewriteCtFlavor ev (mkTcEqPred fam_head xi2) xco
        ; case mb of {
            Nothing -> return Stop ;
-           Just new_ev 
-             | isTcReflCo xco -> continueWith new_ct
-             | otherwise      -> do { updWorkListTcS (extendWorkListFunEq new_ct); return Stop }
+           Just new_ev -> continueWith new_ct
+--             | isTcReflCo xco -> continueWith new_ct
+--             | otherwise      -> do { updWorkListTcS (extendWorkListFunEq new_ct); return Stop }
              where
                new_ct = CFunEqCan { cc_ev = new_ev, cc_loc = loc
                                   , cc_fun = fn, cc_tyargs = xis1, cc_rhs = xi2 } } } 
diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index 4d468721d8..db7f36297f 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -171,6 +171,7 @@ runSolverPipeline pipeline workItem
                   vcat [ ptext (sLit "work item = ") <+> ppr workItem 
                        , ptext (sLit "inerts    = ") <+> ppr initial_is]
 
+       ; bumpStepCountTcS    -- One step for each constraint processed
        ; final_res  <- run_pipeline pipeline (ContinueWith workItem)
 
        ; final_is <- getTcSInerts
@@ -178,7 +179,8 @@ runSolverPipeline pipeline workItem
            Stop            -> do { traceTcS "End solver pipeline (discharged) }" 
                                        (ptext (sLit "inerts    = ") <+> ppr final_is)
                                  ; return () }
-           ContinueWith ct -> do { traceTcS "End solver pipeline (not discharged) }" $
+           ContinueWith ct -> do { traceFireTcS ct (ptext (sLit "Kept as inert:") <+> ppr ct)
+                                 ; traceTcS "End solver pipeline (not discharged) }" $
                                        vcat [ ptext (sLit "final_item = ") <+> ppr ct
                                             , ptext (sLit "inerts     = ") <+> ppr final_is]
                                  ; insertInertItemTcS ct }
@@ -220,39 +222,13 @@ React with (F Int ~ b) ==> IR Stop True []    -- after substituting we re-canoni
 
 \begin{code}
 thePipeline :: [(String,SimplifierStage)]
-thePipeline = [ ("lookup-in-inerts",        lookupInInertsStage)
-              , ("canonicalization",        canonicalizationStage)
+thePipeline = [ ("canonicalization",        TcCanonical.canonicalize)
               , ("spontaneous solve",       spontaneousSolveStage)
               , ("interact with inerts",    interactWithInertsStage)
               , ("top-level reactions",     topReactionsStage) ]
 \end{code}
 
 
-\begin{code}
-
--- A quick lookup everywhere to see if we know about this constraint
---------------------------------------------------------------------
-lookupInInertsStage :: SimplifierStage
-lookupInInertsStage ct
-  | CtWanted { ctev_evar = ev_id, ctev_pred = pred } <- cc_ev ct
-  = do { mb_ct <- lookupInInerts pred
-       ; case mb_ct of
-           Just ctev
-             |  not (isDerived ctev)
-             -> do { setEvBind ev_id (ctEvTerm ctev)
-                   ; return Stop }
-           _ -> continueWith ct }
-  | otherwise -- I could do something like that for givens 
-              -- as well I suppose but it is not a big deal
-  = continueWith ct
-
-
--- The canonicalization stage, see TcCanonical for details
-----------------------------------------------------------
-canonicalizationStage :: SimplifierStage
-canonicalizationStage = TcCanonical.canonicalize 
-\end{code}
-
 *********************************************************************************
 *                                                                               * 
                        The spontaneous-solve Stage
@@ -287,7 +263,10 @@ spontaneousSolveStage workItem
            SPCantSolve
               | CTyEqCan { cc_tyvar = tv, cc_ev = fl } <- workItem
               -- Unsolved equality
-              -> do { kickOutRewritable (ctEvFlavour fl) tv
+              -> do { n_kicked <- kickOutRewritable (ctEvFlavour fl) tv
+                    ; traceFireTcS workItem $
+                      ptext (sLit "Kept as inert") <+> ppr_kicked n_kicked <> colon 
+                      <+> ppr workItem
                     ; insertInertItemTcS workItem
                     ; return Stop }
               | otherwise
@@ -296,10 +275,15 @@ spontaneousSolveStage workItem
            SPSolved new_tv
               -- Post: tv ~ xi is now in TyBinds, no need to put in inerts as well
               -- see Note [Spontaneously solved in TyBinds]
-              -> do { traceFireTcS workItem $
-                      ptext (sLit "Spontaneously solved:") <+> ppr workItem
-                    ; kickOutRewritable Given new_tv
+              -> do { n_kicked <- kickOutRewritable Given new_tv
+                    ; traceFireTcS workItem $
+                      ptext (sLit "Spontaneously solved") <+> ppr_kicked n_kicked <> colon 
+                      <+> ppr workItem
                     ; return Stop } }
+
+ppr_kicked :: Int -> SDoc
+ppr_kicked 0 = empty
+ppr_kicked n = parens (int n <+> ptext (sLit "kicked out")) 
 \end{code}
 Note [Spontaneously solved in TyBinds]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -320,13 +304,14 @@ these binds /and/ the inerts for potentially unsolved or other given equalities.
 kickOutRewritable :: CtFlavour    -- Flavour of the equality that is 
                                   -- being added to the inert set
                   -> TcTyVar      -- The new equality is tv ~ ty
-                  -> TcS ()
+                  -> TcS Int
 kickOutRewritable new_flav new_tv
   = do { wl <- modifyInertTcS kick_out
        ; traceTcS "kickOutRewritable" $ 
             vcat [ text "tv = " <+> ppr new_tv  
                  , ptext (sLit "Kicked out =") <+> ppr wl]
-       ; updWorkListTcS (appendWorkList wl) }
+       ; updWorkListTcS (appendWorkList wl)
+       ; return (workListSize wl)  }
   where
     kick_out :: InertSet -> (WorkList, InertSet)
     kick_out (is@(IS { inert_cans = IC { inert_eqs = tv_eqs
@@ -660,7 +645,7 @@ interactWithInertsStage wi
                        -> do { traceFireTcS atomic_inert 
                                             (mk_msg rule (text "InertItemConsumed"))
                              ; return (ContinueWith wi) }
-                   IRKeepGoing {} -- Should we do a bumpStepCountTcS? No for now.
+                   IRKeepGoing {}
                        -> do { insertInertItemTcS atomic_inert
                              ; return (ContinueWith wi) }
                }
@@ -1384,23 +1369,31 @@ doTopReactDict :: InertSet -> WorkItem -> CtEvidence -> Class -> [Xi]
                -> CtLoc -> TcS TopInteractResult
 doTopReactDict inerts workItem fl cls xis loc
   = do { instEnvs <- getInstEnvs 
-       ; let fd_eqns = improveFromInstEnv instEnvs 
-                           (mkClassPred cls xis, arising_sdoc)
+       ; let pred = mkClassPred cls xis
+             fd_eqns = improveFromInstEnv instEnvs (pred, arising_sdoc)
              
        ; fd_work <- rewriteWithFunDeps fd_eqns loc
        ; if not (null fd_work) then
             do { updWorkListTcS (extendWorkListEqs fd_work)
                ; return SomeTopInt { tir_rule = "Dict/Top (fundeps)"
-                                    , tir_new_item = ContinueWith workItem } }
-         else -- No fundeps
-         if isWanted fl then
-            do { lkup_inst_res  <- matchClassInst inerts cls xis loc
-               ; case lkup_inst_res of
-                   GenInst wtvs ev_term -> do { addSolvedDict fl 
-                                              ; doSolveFromInstance wtvs ev_term }
-                   NoInstance -> return NoTopInt }
-         else 
-            return NoTopInt }
+                                   , tir_new_item = ContinueWith workItem } }
+         else if not (isWanted fl) then 
+            return NoTopInt
+         else do
+
+       { solved_dicts <- getTcSInerts >>= (return . inert_solved_dicts)
+       ; case lookupSolvedDict solved_dicts pred of {
+            Just ev -> do { setEvBind dict_id (ctEvTerm ev); 
+                          ; return $ 
+                            SomeTopInt { tir_rule = "Dict/Top (cached)" 
+                                       , tir_new_item = Stop } } ;
+            Nothing -> do
+
+      { lkup_inst_res  <- matchClassInst inerts cls xis loc
+      ; case lkup_inst_res of
+           GenInst wtvs ev_term -> do { addSolvedDict fl 
+                                      ; doSolveFromInstance wtvs ev_term }
+           NoInstance -> return NoTopInt } } } }
    where 
      arising_sdoc = pprArisingAt loc
      dict_id = ctEvId fl
@@ -1430,18 +1423,17 @@ doTopReactDict inerts workItem fl cls xis loc
 --------------------
 doTopReactFunEq :: Ct -> CtEvidence -> TyCon -> [Xi] -> Xi
                 -> CtLoc -> TcS TopInteractResult
-doTopReactFunEq ct fl fun_tc args xi loc
+doTopReactFunEq _ct fl fun_tc args xi loc
   = ASSERT (isSynFamilyTyCon fun_tc) -- No associated data families have 
                                      -- reached this far 
     -- Look in the cache of solved funeqs
     do { fun_eq_cache <- getTcSInerts >>= (return . inert_solved_funeqs)
        ; case lookupFamHead fun_eq_cache fam_ty of {
-           Just (CFunEqCan { cc_ev = ctev, cc_rhs = rhs_ty })
+           Just (ctev, rhs_ty)
              | ctEvFlavour ctev `canRewrite` ctEvFlavour fl
              -> ASSERT( not (isDerived ctev) )
                 succeed_with "Fun/Cache" (evTermCoercion (ctEvTerm ctev)) rhs_ty ;
-           Just ct' -> pprPanic "doTopReactFunEq" (ppr ct') ;
-           Nothing -> 
+           _other -> 
 
     -- Look up in top-level instances
     do { match_res <- matchFam fun_tc args   -- See Note [MATCHING-SYNONYMS]
@@ -1451,7 +1443,7 @@ doTopReactFunEq ct fl fun_tc args xi loc
 
     -- Found a top-level instance
     do {    -- Add it to the solved goals
-         unless (isDerived fl) (addSolvedFunEq ct fam_ty)
+         unless (isDerived fl) (addSolvedFunEq fam_ty fl xi)
 
        ; let coe_ax = famInstAxiom famInst 
        ; succeed_with "Fun/Top" (mkTcAxInstCo coe_ax rep_tys)
diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs
index f4c0c4af2e..63c475d24a 100644
--- a/compiler/typecheck/TcSMonad.lhs
+++ b/compiler/typecheck/TcSMonad.lhs
@@ -16,7 +16,7 @@ module TcSMonad (
     extendWorkListEq, extendWorkListFunEq, 
     extendWorkListNonEq, extendWorkListCt, 
     extendWorkListCts, extendWorkListEqs, appendWorkList, selectWorkItem,
-    withWorkList,
+    withWorkList, workListSize,
 
     updWorkListTcS, updWorkListTcS_return,
     
@@ -32,7 +32,7 @@ module TcSMonad (
     mkGivenLoc, 
 
     TcS, runTcS, runTcSWithEvBinds, failTcS, panicTcS, traceTcS, -- Basic functionality 
-    traceFireTcS, 
+    traceFireTcS, bumpStepCountTcS, 
     tryTcS, nestTcS, nestImplicTcS, recoverTcS,
     wrapErrTcS, wrapWarnTcS,
 
@@ -58,7 +58,7 @@ module TcSMonad (
     getTcEvBindsMap, getTcSTyBinds, getTcSTyBindsMap,
 
 
-    newFlattenSkolemTy,                         -- Flatten skolems 
+    lookupFlatEqn, newFlattenSkolem,            -- Flatten skolems 
 
         -- Deque
     Deque(..), insertDeque, emptyDeque,
@@ -66,7 +66,7 @@ module TcSMonad (
         -- Inerts 
     InertSet(..), InertCans(..), 
     getInertEqs, 
-    emptyInert, getTcSInerts, lookupInInerts, lookupFlatEqn,
+    emptyInert, getTcSInerts, lookupInInerts, 
     getInertUnsolved, checkAllSolved, 
     prepareInertsForImplications,
     modifyInertTcS,
@@ -74,7 +74,7 @@ module TcSMonad (
     getRelevantCts, extractRelevantInerts,
     CCanMap(..), CtTypeMap, CtFamHeadMap, CtPredMap,
     PredMap, FamHeadMap,
-    partCtFamHeadMap, lookupFamHead,
+    partCtFamHeadMap, lookupFamHead, lookupSolvedDict,
     filterSolved,
 
     instDFunType,                              -- Instantiation
@@ -134,6 +134,7 @@ import TcRnTypes
 import Unique 
 import UniqFM
 import Maybes ( orElse, catMaybes, firstJust )
+import StaticFlags( opt_NoFlatCache )
 
 import Control.Monad( unless, when, zipWithM )
 import Data.IORef
@@ -208,6 +209,9 @@ emptyDeque = DQ [] []
 isEmptyDeque :: Deque a -> Bool
 isEmptyDeque (DQ as bs) = null as && null bs
 
+dequeSize :: Deque a -> Int
+dequeSize (DQ as bs) = length as + length bs
+
 insertDeque :: a -> Deque a -> Deque a
 insertDeque b (DQ as bs) = DQ as (b:bs)
 
@@ -235,6 +239,10 @@ appendWorkList new_wl orig_wl
               , wl_rest   = wl_rest new_wl   ++            wl_rest orig_wl }
 
 
+workListSize :: WorkList -> Int
+workListSize (WorkList { wl_eqs = eqs, wl_funeqs = funeqs, wl_rest = rest })
+  = length eqs + dequeSize funeqs + length rest
+
 extendWorkListEq :: Ct -> WorkList -> WorkList
 -- Extension by equality
 extendWorkListEq ct wl 
@@ -406,6 +414,9 @@ instance Outputable a => Outputable (FamHeadMap a) where
 sizePredMap :: PredMap a -> Int
 sizePredMap (PredMap m) = foldTypeMap (\_ x -> x+1) 0 m
 
+emptyFamHeadMap :: FamHeadMap a
+emptyFamHeadMap = FamHeadMap emptyTM
+
 sizeFamHeadMap :: FamHeadMap a -> Int
 sizeFamHeadMap (FamHeadMap m) = foldTypeMap (\_ x -> x+1) 0 m
 
@@ -453,31 +464,6 @@ filterSolved p (PredMap mp) = PredMap (foldTM upd mp emptyTM)
 %*									*
 %************************************************************************
 
-\begin{code}
--- All Given (fully known) or Wanted or Derived
--- See Note [Detailed InertCans Invariants] for more
-data InertCans 
-  = IC { inert_eqs :: TyVarEnv Ct
-              -- Must all be CTyEqCans! If an entry exists of the form: 
-              --   a |-> ct,co
-              -- Then ct = CTyEqCan { cc_tyvar = a, cc_rhs = xi } 
-              -- And  co : a ~ xi
-       , inert_dicts :: CCanMap Class
-              -- Dictionaries only, index is the class
-              -- NB: index is /not/ the whole type because FD reactions 
-              -- need to match the class but not necessarily the whole type.
-       , inert_funeqs :: CtFamHeadMap
-              -- Family equations, index is the whole family head type.
-       , inert_irreds :: Cts       
-              -- Irreducible predicates
-
-       , inert_insols :: Cts       
-              -- Frozen errors (as non-canonicals)
-       }
-    
-                     
-\end{code}
-
 Note [Detailed InertCans Invariants]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 The InertCans represents a collection of constraints with the following properties:
@@ -536,24 +522,76 @@ The reason for all this is simply to avoid re-solving goals we have solved alrea
 
   But there are no solved Deriveds in inert_solved_funeqs
 
+Note [Type family equations]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Type-family equations, of form (ev : F tys ~ ty), live in four places
+
+  * The work-list, of course
+
+  * The inert_flat_cache.  This is used when flattening, to get maximal
+    sharing.  It contains lots of things that are still in the work-list.
+    E.g Suppose we have (w1: F (G a) ~ Int), and (w2: H (G a) ~ Int) in the
+        work list.  Then we flatten w1, dumping (w3: G a ~ f1) in the work
+        list.  Now if we flatten w2 before we get to w3, we still want to 
+        share that (G a).
+
+    Because it contains work-list things, DO NOT use the flat cache to solve
+    a top-level goal.  Eg in the above example we don't want to solve w3 
+    using w3 itself!  
+
+  * The inert_solved_funeqs.  These are all "solved" goals (see Note [Solved constraints]),
+    the result of using a top-level type-family instance.
+
+  * THe inert_funeqs are un-solved but fully processed and in the InertCans.
+
 
 \begin{code}
+-- All Given (fully known) or Wanted or Derived
+-- See Note [Detailed InertCans Invariants] for more
+data InertCans 
+  = IC { inert_eqs :: TyVarEnv Ct
+              -- Must all be CTyEqCans! If an entry exists of the form: 
+              --   a |-> ct,co
+              -- Then ct = CTyEqCan { cc_tyvar = a, cc_rhs = xi } 
+              -- And  co : a ~ xi
+       , inert_dicts :: CCanMap Class
+              -- Dictionaries only, index is the class
+              -- NB: index is /not/ the whole type because FD reactions 
+              -- need to match the class but not necessarily the whole type.
+       , inert_funeqs :: CtFamHeadMap
+              -- Family equations, index is the whole family head type.
+       , inert_irreds :: Cts       
+              -- Irreducible predicates
+
+       , inert_insols :: Cts       
+              -- Frozen errors (as non-canonicals)
+       }
+    
+                     
 -- The Inert Set
 data InertSet
   = IS { inert_cans :: InertCans
               -- Canonical Given, Wanted, Derived (no Solved)
 	      -- Sometimes called "the inert set"
 
-       , inert_fsks :: [TcTyVar]  -- Flatten-skolems allocated in this local scope
-              -- All ``flattening equations'' are kept here. 
-              -- Always canonical CTyFunEqs (Given or Wanted only!)
-              -- Key is by family head. We use this field during flattening only
+       , inert_flat_cache :: FamHeadMap (CtEvidence, TcType)
+              -- See Note [Type family equations]
+              -- Just a hash-cons cache for use when flattening only
+              -- These include entirely un-processed goals, so don't use
+              -- them to solve a top-level goal, else you may end up solving
+              -- (w:F ty ~ a) by setting w:=w!  We just use the flat-cache
+              -- when allocating a new flatten-skolem.
               -- Not necessarily inert wrt top-level equations (or inert_cans)
+ 
+       , inert_fsks :: [TcTyVar]  -- Rigid flatten-skolems (arising from givens)
+                                  -- allocated in this local scope
 
-       , inert_solved_funeqs :: CtFamHeadMap  
+       , inert_solved_funeqs :: FamHeadMap (CtEvidence, TcType)
+              -- See Note [Type family equations]
               -- Of form co :: F xis ~ xi 
               -- Always the result of using a top-level family axiom F xis ~ tau
               -- No Deriveds 
+              -- Not necessarily fully rewritten (by type substitutions)
 
        , inert_solved_dicts   :: PredMap CtEvidence 
        	      -- Of form ev :: C t1 .. tn
@@ -589,12 +627,13 @@ emptyInert :: InertSet
 emptyInert
   = IS { inert_cans = IC { inert_eqs    = emptyVarEnv
                          , inert_dicts  = emptyCCanMap
-                         , inert_funeqs = FamHeadMap emptyTM 
+                         , inert_funeqs = emptyFamHeadMap
                          , inert_irreds = emptyCts
                          , inert_insols = emptyCts }
        , inert_fsks          = []
+       , inert_flat_cache    = emptyFamHeadMap
        , inert_solved_dicts  = PredMap emptyTM 
-       , inert_solved_funeqs = FamHeadMap emptyTM }
+       , inert_solved_funeqs = emptyFamHeadMap }
 
 insertInertItem :: Ct -> InertSet -> InertSet 
 -- Add a new inert element to the inert set. 
@@ -661,12 +700,11 @@ addSolvedDict item
     pred = ctEvPred item
     upd_solved _ = Just item
 
-addSolvedFunEq :: Ct -> TcType -> TcS ()
-addSolvedFunEq fun_eq fam_ty
-  = updInertTcS upd_solved_funeqs
-  where 
-    upd_solved_funeqs inert 
-      = inert { inert_solved_funeqs = insertFamHead (inert_solved_funeqs inert) fam_ty fun_eq }
+addSolvedFunEq :: TcType -> CtEvidence -> TcType -> TcS ()
+addSolvedFunEq fam_ty ev rhs_ty
+  = updInertTcS $ \ inert -> 
+    inert { inert_solved_funeqs = insertFamHead (inert_solved_funeqs inert) 
+                                                fam_ty (ev, rhs_ty) }
 
 modifyInertTcS :: (InertSet -> (a,InertSet)) -> TcS a 
 -- Modify the inert set with the supplied function
@@ -689,7 +727,8 @@ prepareInertsForImplications :: InertSet -> InertSet
 -- See Note [Preparing inert set for implications]
 prepareInertsForImplications is
   = is { inert_cans   = getGivens (inert_cans is)
-       , inert_fsks   = [] }
+       , inert_fsks   = []
+       , inert_flat_cache = emptyFamHeadMap }
   where
     getGivens (IC { inert_eqs    = eqs
                   , inert_irreds = irreds
@@ -831,25 +870,31 @@ extractRelevantInerts wi
         extract_ics_relevants _ ics = (emptyCts,ics)
         
 
-lookupFlatEqn :: TcType -> TcS (Maybe Ct)
+lookupFlatEqn :: TcType -> TcS (Maybe (CtEvidence, TcType))
 lookupFlatEqn fam_ty 
   = do { IS { inert_solved_funeqs = solved_funeqs
+            , inert_flat_cache = flat_cache
             , inert_cans = IC { inert_funeqs = inert_funeqs } } <- getTcSInerts
-       ; return (lookupFamHead solved_funeqs fam_ty 
-                 `firstJust` lookupFamHead inert_funeqs fam_ty  
-                )  }
+       ; return (lookupFamHead solved_funeqs fam_ty `firstJust` 
+                 lookupFamHead flat_cache fam_ty    `firstJust`
+                 lookup_in_inerts inert_funeqs) }
+  where
+    lookup_in_inerts inert_funeqs 
+        = case lookupFamHead inert_funeqs fam_ty of
+            Nothing -> Nothing
+            Just ct -> Just (ctEvidence ct, cc_rhs ct)
 
 lookupInInerts :: TcPredType -> TcS (Maybe CtEvidence)
 -- Is this exact predicate type cached in the solved or canonicals of the InertSet
 lookupInInerts pty
   = do { IS { inert_solved_dicts = solved, inert_cans = ics } <- getTcSInerts
-       ; case lookupInSolved solved pty of
+       ; case lookupSolvedDict solved pty of
            Just ctev -> return (Just ctev)
            Nothing   -> return (lookupInInertCans ics pty) }
 
-lookupInSolved :: PredMap CtEvidence -> TcPredType -> Maybe CtEvidence
+lookupSolvedDict :: PredMap CtEvidence -> TcPredType -> Maybe CtEvidence
 -- Returns just if exactly this predicate type exists in the solved.
-lookupInSolved tm pty = lookupTM pty $ unPredMap tm
+lookupSolvedDict tm pty = lookupTM pty $ unPredMap tm
 
 lookupInInertCans :: InertCans -> TcPredType -> Maybe CtEvidence
 -- Returns Just if exactly this pred type exists in the inert canonicals
@@ -960,14 +1005,17 @@ traceTcS herald doc = wrapTcS (TcM.traceTc herald doc)
 instance HasDynFlags TcS where
     getDynFlags = wrapTcS getDynFlags
 
+bumpStepCountTcS :: TcS ()
+bumpStepCountTcS = TcS $ \env -> do { let ref = tcs_count env
+                                    ; n <- TcM.readTcRef ref
+                                    ; TcM.writeTcRef ref (n+1) }
+
 traceFireTcS :: Ct -> SDoc -> TcS ()
--- Dump a rule-firing trace, and bumpt the counter
+-- Dump a rule-firing trace
 traceFireTcS ct doc 
   = TcS $ \env -> 
     TcM.ifDOptM Opt_D_dump_cs_trace $ 
-    do { let count_ref = tcs_count env
-       ; n <- TcM.readTcRef count_ref
-       ; TcM.writeTcRef count_ref (n+1)
+    do { n <- TcM.readTcRef (tcs_count env)
        ; let msg = int n <> brackets (int (ctLocDepth (cc_loc ct))) <+> doc
        ; TcM.dumpTcRn msg }
 
@@ -1304,19 +1352,42 @@ which will result in two Deriveds to end up in the insoluble set:
 \begin{code}
 -- Flatten skolems
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-newFlattenSkolemTy :: TcType -> TcS TcType
-newFlattenSkolemTy fam_ty
+newFlattenSkolem :: CtFlavour 
+                 -> TcType                      -- F xis
+                 -> TcS (CtEvidence, TcType)    -- co :: F xis ~ ty
+-- We have already looked up in the cache; no need to so so again
+newFlattenSkolem Given fam_ty
   = do { tv <- wrapTcS $ 
                do { uniq <- TcM.newUnique
                   ; let name = TcM.mkTcTyVarName uniq (fsLit "f")
                   ; return $ mkTcTyVar name (typeKind fam_ty) (FlatSkol fam_ty) } 
        ; traceTcS "New Flatten Skolem Born" $
          ppr tv <+> text "[:= " <+> ppr fam_ty <+> text "]"
-       ; updInertTcS (add_fsk tv)
-       ; return (mkTyVarTy tv) }
-  where
-    add_fsk :: TcTyVar -> InertSet -> InertSet
-    add_fsk tv is = is { inert_fsks = tv : inert_fsks is }
+
+       ; let rhs_ty = mkTyVarTy tv
+             ctev = CtGiven { ctev_pred = mkTcEqPred fam_ty rhs_ty
+                            , ctev_evtm = EvCoercion (mkTcReflCo fam_ty) }
+       ; updInertTcS $ \ is@(IS { inert_fsks = fsks }) -> 
+            extendFlatCache fam_ty ctev rhs_ty
+            is { inert_fsks       = tv : fsks }
+
+       ; return (ctev, rhs_ty) }
+
+newFlattenSkolem _ fam_ty  -- Wanted or Derived: make new unification variable
+  = do { rhs_ty <- newFlexiTcSTy (typeKind fam_ty)
+       ; ctev <- newWantedEvVarNC (mkTcEqPred fam_ty rhs_ty)
+                                   -- NC (no-cache) version because we've already
+                                   -- looked in the solved goals an inerts (lookupFlatEqn)
+       ; updInertTcS $ extendFlatCache fam_ty ctev rhs_ty
+       ; return (ctev, rhs_ty) }
+
+extendFlatCache :: TcType -> CtEvidence -> TcType -> InertSet -> InertSet
+extendFlatCache 
+  | opt_NoFlatCache
+  = \ _ _ _ is -> is
+  | otherwise
+  = \ fam_ty ctev rhs_ty is@(IS { inert_flat_cache = fc }) -> 
+      is { inert_flat_cache = insertFamHead fc fam_ty (ctev,rhs_ty) }
 
 -- Instantiations 
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~