Solved goal caching and zonking optimisations.

1) Stopped rewriting and caching solveds in the inerts because
profiling showed that a lot of time was spent on rewriting
already solved goals.

2) Optimisations in zonkEvBinds for common-case
evidence bindings generated from the constraint solver.

3) Now solved goals cache their evidence terms, so that we can more
aggressively optimize Refl coercions during constraint solving.
This patch also includes a rewrite of rewriteInertEqsFromInertEq
which greatly improves its efficiency.

7 files changed, 415 insertions, 302 deletions

diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs
index 16dea420ac..c1f679ee70 100644
--- a/compiler/typecheck/TcCanonical.lhs
+++ b/compiler/typecheck/TcCanonical.lhs
@@ -32,7 +32,7 @@ import Name ( Name )
 import Var
 import VarEnv
 import Outputable
-import Control.Monad    ( when, unless, zipWithM, zipWithM_, foldM )
+import Control.Monad    ( when, unless, zipWithM, foldM )
 import MonadUtils
 import Control.Applicative ( (<|>) )
 
@@ -166,25 +166,29 @@ are again good.
 canonicalize :: Ct -> TcS StopOrContinue
 canonicalize ct@(CNonCanonical { cc_id = ev, cc_flavor = fl, cc_depth  = d })
   = do { traceTcS "canonicalize (non-canonical)" (ppr ct)
-       ; canEvVar ev (classifyPredType (evVarPred ev)) d fl }
+       ; {-# SCC "canEvVar" #-}
+         canEvVar ev (classifyPredType (evVarPred ev)) d fl }
 
 canonicalize (CDictCan { cc_id = ev, cc_depth = d
                        , cc_flavor = fl
                        , cc_class  = cls
                        , cc_tyargs = xis })
-  = canClass d fl ev cls xis -- Do not add any superclasses
+  = {-# SCC "canClass" #-}
+    canClass d fl ev cls xis -- Do not add any superclasses
 canonicalize (CTyEqCan { cc_id = ev, cc_depth = d
                        , cc_flavor = fl
                        , cc_tyvar  = tv
                        , cc_rhs    = xi })
-  = canEqLeafTyVarLeftRec d fl ev tv xi
+  = {-# SCC "canEqLeafTyVarLeftRec" #-}
+    canEqLeafTyVarLeftRec d fl ev tv xi
 
 canonicalize (CFunEqCan { cc_id = ev, cc_depth = d
                         , cc_flavor = fl
                         , cc_fun    = fn
                         , cc_tyargs = xis1
                         , cc_rhs    = xi2 })
-  = canEqLeafFunEqLeftRec d fl ev (fn,xis1) xi2
+  = {-# SCC "canEqLeafFunEqLeftRec" #-}
+    canEqLeafFunEqLeftRec d fl ev (fn,xis1) xi2
 
 canonicalize (CIPCan { cc_id = ev, cc_depth = d
                      , cc_flavor = fl
@@ -225,16 +229,19 @@ canTuple :: SubGoalDepth -- Depth
 canTuple d fl ev tys
   = do { traceTcS "can_pred" (text "TuplePred!") 
        ; evs <- zipWithM can_pred_tup_one tys [0..]
-       ; when (isWanted fl) $ setEvBind ev (EvTupleMk evs)
-       ; return Stop }
+       ; if (isWanted fl) then 
+             do {_unused_fl <- setEvBind ev (EvTupleMk evs) fl
+                ; return Stop }
+         else return Stop }
   where 
      can_pred_tup_one ty n
           = do { evc <- newEvVar fl ty
-               ; let ev' = evc_the_evvar evc 
-               ; when (isGivenOrSolved fl) $ 
-                      setEvBind ev' (EvTupleSel ev n)
-               ; when (isNewEvVar evc)     $ 
-                      addToWork (canEvVar ev' (classifyPredType (evVarPred ev')) d fl)
+               ; let ev' = evc_the_evvar evc
+               ; fl' <- if isGivenOrSolved fl then 
+                            setEvBind ev' (EvTupleSel ev n) fl
+                        else return fl
+               ; when (isNewEvVar evc) $
+                      addToWork (canEvVar ev' (classifyPredType (evVarPred ev')) d fl')
                ; return ev' }
 
 -- Implicit Parameter Canonicalization
@@ -255,13 +262,13 @@ canIP d fl v nm ty
          else do { evc <- newEvVar fl xi
                  ; let v_new          = evc_the_evvar evc
                        IPPred _ ip_xi = classifyPredType xi
-                 ; case fl of 
-                     Wanted {}  -> setEvBind v (EvCast v_new co)
-                     Given {}   -> setEvBind v_new (EvCast v (mkSymCo co))
-                     Derived {} -> return ()
+                 ; fl_new <- case fl of 
+                               Wanted {}  -> setEvBind v (EvCast v_new co) fl 
+                               Given {}   -> setEvBind v_new (EvCast v (mkSymCo co)) fl
+                               Derived {} -> return fl
                  ; if isNewEvVar evc then
                        continueWith $ CIPCan { cc_id     = v_new
-                                             , cc_flavor = fl, cc_ip_nm = nm
+                                             , cc_flavor = fl_new, cc_ip_nm = nm
                                              , cc_ip_ty  = ip_xi
                                              , cc_depth  = d }
                    else return Stop } }
@@ -301,13 +308,13 @@ canClass d fl v cls tys
                    -- Flattening happened
          else do { evc <- newEvVar fl xi
                  ; let v_new = evc_the_evvar evc
-                 ; case fl of
-                     Wanted  {} -> setEvBind v (EvCast v_new co)
-                     Given   {} -> setEvBind v_new (EvCast v (mkSymCo co))
-                     Derived {} -> return ()
+                 ; fl_new <- case fl of
+                     Wanted  {} -> setEvBind v (EvCast v_new co) fl
+                     Given   {} -> setEvBind v_new (EvCast v (mkSymCo co)) fl
+                     Derived {} -> return fl
                     -- Continue only if flat constraint is new
                  ; if isNewEvVar evc then
-                        continueWith $ CDictCan { cc_id = v_new, cc_flavor = fl
+                        continueWith $ CDictCan { cc_id = v_new, cc_flavor = fl_new
                                                 , cc_tyargs = xis, cc_class = cls
                                                 , cc_depth  = d }
                    else return Stop } }
@@ -392,7 +399,8 @@ newSCWorkFromFlavored d ev flavor cls xis
                       ; sc_vars <- mapM (newEvVar flavor) sc_theta
                       ; sc_cts <- zipWithM (\scv ev_trm -> 
                                                 do { let sc_evvar = evc_the_evvar scv
-                                                   ; setEvBind sc_evvar ev_trm
+                                                   ; _unused_fl <- setEvBind sc_evvar ev_trm flavor
+                                                      -- unused because it's the same
                                                    ; return $ 
                                                      CNonCanonical { cc_id = sc_evvar
                                                                    , cc_flavor = flavor
@@ -402,7 +410,7 @@ newSCWorkFromFlavored d ev flavor cls xis
                       ; traceTcS "newSCWorkFromFlavored" $
                                  text "Emitting superclass work:" <+> ppr sc_cts
                       ; updWorkListTcS $ appendWorkListCt sc_cts }
-      GivenSolved -> return ()
+      GivenSolved {} -> return ()
       -- Seems very dangerous to add the superclasses for dictionaries that may be 
       -- partially solved because we may end up with evidence loops.
 
@@ -458,13 +466,13 @@ canIrred d fl v ty
           -- canonicalise the resulting evidence variable
         evc <- newEvVar fl xi
       ; let v' = evc_the_evvar evc
-      ; case fl of 
-          Wanted  {} -> setEvBind v (EvCast v' co)
-          Given   {} -> setEvBind v' (EvCast v (mkSymCo co)) 
-          Derived {} -> return ()
+      ; fl' <- case fl of 
+          Wanted  {} -> setEvBind v (EvCast v' co) fl
+          Given   {} -> setEvBind v' (EvCast v (mkSymCo co)) fl
+          Derived {} -> return fl
       
       ; if isNewEvVar evc then 
-            canEvVar v' (classifyPredType (evVarPred v')) d fl
+            canEvVar v' (classifyPredType (evVarPred v')) d fl'
         else
             return Stop }
       }
@@ -588,16 +596,16 @@ flatten d fl (TyConApp tc tys)
                     Nothing
                         | isGivenOrSolved fl ->
                             do { rhs_xi_var <- newFlattenSkolemTy fam_ty
-                               ; eqv <- newGivenEqVar fl fam_ty rhs_xi_var (mkReflCo fam_ty)
+                               ; (fl',eqv) 
+                                   <- newGivenEqVar fl fam_ty rhs_xi_var (mkReflCo fam_ty)
                                ; let ct  = CFunEqCan { cc_id     = eqv
-                                                     , cc_flavor = fl -- Given
+                                                     , cc_flavor = fl' -- Given
                                                      , cc_fun    = tc 
                                                      , cc_tyargs = xi_args 
                                                      , cc_rhs    = rhs_xi_var 
                                                      , cc_depth  = d }
                                            -- Update the flat cache: just an optimisation!
                                ; updateFlatCache eqv fl tc xi_args rhs_xi_var WhileFlattening
-
                                ; return (mkEqVarLCo eqv, rhs_xi_var, [ct]) }
                         | otherwise ->
                     -- Derived or Wanted: make a new /unification/ flatten variable
@@ -688,11 +696,11 @@ addToWork tcs_action = tcs_action >>= stop_or_emit
         stop_or_emit (ContinueWith ct) = updWorkListTcS $ 
                                          extendWorkListCt ct
 
-canEqEvVarsCreated :: SubGoalDepth -> CtFlavor 
-                   -> [EvVarCreated] -> [Type] -> [Type]
+canEqEvVarsCreated :: SubGoalDepth 
+                   -> [CtFlavor] -> [EvVarCreated] -> [Type] -> [Type]
                    -> TcS StopOrContinue
 canEqEvVarsCreated _d _fl [] _ _    = return Stop
-canEqEvVarsCreated d fl (evc:evcs) (ty1:tys1) (ty2:tys2) 
+canEqEvVarsCreated d (fl:fls) (evc:evcs) (ty1:tys1) (ty2:tys2) 
   | isNewEvVar evc 
   = let do_one evc0 sy1 sy2
           | isNewEvVar evc0 
@@ -701,7 +709,7 @@ canEqEvVarsCreated d fl (evc:evcs) (ty1:tys1) (ty2:tys2)
     in do { _unused <- zipWith3M do_one evcs tys1 tys2 
           ; canEq d fl (evc_the_evvar evc) ty1 ty2 }
   | otherwise 
-  = canEqEvVarsCreated d fl evcs tys1 tys2
+  = canEqEvVarsCreated d fls evcs tys1 tys2
 canEqEvVarsCreated _ _ _ _ _ = return Stop
 
 
@@ -714,7 +722,8 @@ canEq :: SubGoalDepth
 canEq _d fl eqv ty1 ty2
   | eqType ty1 ty2	-- Dealing with equality here avoids
     	     	 	-- later spurious occurs checks for a~a
-  = do { when (isWanted fl) (setEqBind eqv (mkReflCo ty1))
+  = do { when (isWanted fl) $ 
+              do { _ <- setEqBind eqv (mkReflCo ty1) fl; return () }
        ; return Stop }
 
 -- Split up an equality between function types into two equalities.
@@ -723,16 +732,19 @@ canEq d fl eqv (FunTy s1 t1) (FunTy s2 t2)
        ; reseqv <- newEqVar fl t1 t2
        ; let argeqv_v = evc_the_evvar argeqv
              reseqv_v = evc_the_evvar reseqv
-       ; case fl of
+       ; (fl1,fl2) <- case fl of
            Wanted {} ->
-               setEqBind eqv (mkFunCo (mkEqVarLCo argeqv_v) (mkEqVarLCo reseqv_v))
+               do { _ <- setEqBind eqv (mkFunCo (mkEqVarLCo argeqv_v) (mkEqVarLCo reseqv_v)) fl
+                  ; return (fl,fl) }
            Given {} ->
-               do { setEqBind argeqv_v (mkNthCo 0 (mkEqVarLCo eqv))
-                  ; setEqBind reseqv_v (mkNthCo 1 (mkEqVarLCo eqv)) }
+               do { fl1 <- setEqBind argeqv_v (mkNthCo 0 (mkEqVarLCo eqv)) fl
+                  ; fl2 <- setEqBind reseqv_v (mkNthCo 1 (mkEqVarLCo eqv)) fl 
+                  ; return (fl1,fl2)
+                  }
            Derived {} ->
-               return ()
+               return (fl,fl)
 
-       ; canEqEvVarsCreated d fl [reseqv,argeqv] [t1,s1] [t2,s2] }
+       ; canEqEvVarsCreated d [fl2,fl1] [reseqv,argeqv] [t1,s1] [t2,s2] }
 
 -- If one side is a variable, orient and flatten,
 -- WITHOUT expanding type synonyms, so that we tend to 
@@ -759,17 +771,18 @@ canEq d fl eqv (TyConApp tc1 tys1) (TyConApp tc2 tys2)
        ; let kicos = map mkReflCo kis1
 
        ; argeqvs <- zipWithM (newEqVar fl) tys1' tys2'
-       ; case fl of 
+       ; fls <- case fl of 
            Wanted {} -> 
-             setEqBind eqv $ 
-             mkTyConAppCo tc1 (kicos ++ map (mkEqVarLCo . evc_the_evvar) argeqvs)
+             do { _ <- setEqBind eqv
+                         (mkTyConAppCo tc1 (kicos ++ map (mkEqVarLCo . evc_the_evvar) argeqvs)) fl
+                ; return (map (\_ -> fl) argeqvs) }
            Given {} ->
              let do_one argeqv n = setEqBind (evc_the_evvar argeqv) 
-                                             (mkNthCo n (mkEqVarLCo eqv))
-             in zipWithM_ do_one argeqvs [(length kicos)..]
-           Derived {} -> return ()
+                                             (mkNthCo n (mkEqVarLCo eqv)) fl
+             in zipWithM do_one argeqvs [(length kicos)..]
+           Derived {} -> return (map (\_ -> fl) argeqvs)
 
-       ; canEqEvVarsCreated d fl argeqvs tys1' tys2' }
+       ; canEqEvVarsCreated d fls argeqvs tys1' tys2' }
 
 -- See Note [Equality between type applications]
 --     Note [Care with type applications] in TcUnify
@@ -793,9 +806,10 @@ canEq d fl eqv ty1 ty2
                  eqv2 = evc_the_evvar evc2
  
            ; when (isWanted fl) $
-                  setEqBind eqv (mkAppCo (mkEqVarLCo eqv1) (mkEqVarLCo eqv2))
+                  do { _ <- setEqBind eqv (mkAppCo (mkEqVarLCo eqv1) (mkEqVarLCo eqv2)) fl
+                     ; return () }
            
-           ; canEqEvVarsCreated d fl [evc1,evc2] [s1,t1] [s2,t2] }
+           ; canEqEvVarsCreated d [fl,fl] [evc1,evc2] [s1,t1] [s2,t2] }
 
 
 canEq d fl eqv s1@(ForAllTy {}) s2@(ForAllTy {})
@@ -1023,15 +1037,15 @@ canEqLeaf :: SubGoalDepth -- Depth
 canEqLeaf d fl eqv s1 s2 
   | cls1 `re_orient` cls2
   = do { traceTcS "canEqLeaf (reorienting)" $ ppr (evVarPred eqv)
-       ; delCachedEvVar eqv
+       ; delCachedEvVar eqv fl
        ; evc <- newEqVar fl s2 s1
        ; let eqv' = evc_the_evvar evc
-       ; case fl of 
-           Wanted {}  -> setEqBind eqv (mkSymCo (mkEqVarLCo eqv'))
-           Given {}   -> setEqBind eqv' (mkSymCo (mkEqVarLCo eqv))
-           Derived {} -> return ()
+       ; fl' <- case fl of 
+           Wanted {}  -> setEqBind eqv (mkSymCo (mkEqVarLCo eqv')) fl 
+           Given {}   -> setEqBind eqv' (mkSymCo (mkEqVarLCo eqv)) fl 
+           Derived {} -> return fl 
        ; if isNewEvVar evc then 
-             do { canEqLeafOriented d fl eqv' s2 s1 }
+             do { canEqLeafOriented d fl' eqv' s2 s1 }
          else return Stop 
        }
   | otherwise
@@ -1075,15 +1089,24 @@ canEqLeafFunEqLeftRec :: SubGoalDepth
                       -> (TyCon,[TcType]) -> TcType -> TcS StopOrContinue
 canEqLeafFunEqLeftRec d fl eqv (fn,tys1) ty2  -- eqv :: F tys1 ~ ty2
   = do { traceTcS "canEqLeafFunEqLeftRec" $ ppr (evVarPred eqv)
-       ; (xis1,cos1) <- flattenMany d fl tys1 -- Flatten type function arguments
-                                              -- cos1 :: xis1 ~ tys1
+       ; (xis1,cos1) <- 
+           {-# SCC "flattenMany" #-}
+           flattenMany d fl tys1 -- Flatten type function arguments
+                                 -- cos1 :: xis1 ~ tys1
 
        ; let no_flattening = all isReflCo cos1
 
-       ; inerts <- getTcSInerts
-       ; let fam_eqs   = inert_funeqs inerts
+--       ; inerts <- getTcSInerts
+--        ; let fam_eqs   = inert_funeqs inerts
 
-       ; let is_cached = lookupFunEq (mkTyConApp fn xis1) fl fam_eqs
+       ; let flat_ty = mkTyConApp fn xis1
+
+       ; is_cached <- getCachedFlatEq fn xis1 fl WhenSolved
+                      -- Lookup if we have solved this goal already
+{-
+       ; let is_cached = {-# SCC "lookupFunEq" #-} 
+                         lookupFunEq flat_ty fl fam_eqs
+-}
 
        ; if no_flattening && isNothing is_cached then 
              canEqLeafFunEqLeft d fl eqv (fn,xis1) ty2
@@ -1093,23 +1116,24 @@ canEqLeafFunEqLeftRec d fl eqv (fn,tys1) ty2  -- eqv :: F tys1 ~ ty2
                  , Just (rhs_ty, ret_eq) <- is_cached
                  = (mkSymCo ret_eq, rhs_ty)
                  | Nothing <- is_cached -- Just flattening
-                 = (mkTyConAppCo fn cos1, mkTyConApp fn xis1)
+                 = (mkTyConAppCo fn cos1, flat_ty)
                  | Just (rhs_ty, ret_eq) <- is_cached  -- Both
                  = (mkSymCo ret_eq `mkTransCo` mkTyConAppCo fn cos1, rhs_ty)
                  | otherwise = panic "No flattening and not cached!"
-       ; delCachedEvVar eqv
+       ; delCachedEvVar eqv fl
        ; evc <- newEqVar fl final_ty ty2
        ; let new_eqv = evc_the_evvar evc
-       ; case fl of
-           Wanted {}  -> setEqBind eqv $ 
-                         mkSymCo final_co `mkTransCo` (mkEqVarLCo new_eqv)
-           Given {}   -> setEqBind new_eqv $ final_co `mkTransCo` (mkEqVarLCo eqv)
-           Derived {} -> return ()
+       ; fl' <- case fl of
+           Wanted {}  -> setEqBind eqv 
+                           (mkSymCo final_co `mkTransCo` (mkEqVarLCo new_eqv)) fl
+           Given {}   -> setEqBind new_eqv (final_co `mkTransCo` (mkEqVarLCo eqv)) fl
+           Derived {} -> return fl
        ; if isNewEvVar evc then
              if isNothing is_cached then
-                 canEqLeafFunEqLeft d fl new_eqv (fn,xis1) ty2
+                 {-# SCC "canEqLeafFunEqLeft" #-}
+                 canEqLeafFunEqLeft d fl' new_eqv (fn,xis1) ty2
              else
-                 canEq (d+1) fl new_eqv final_ty ty2
+                 canEq (d+1) fl' new_eqv final_ty ty2
          else return Stop
        }
        }
@@ -1148,8 +1172,11 @@ canEqLeafFunEqLeft :: SubGoalDepth -- Depth
                    -> TcType -> TcS StopOrContinue
 -- Precondition: No more flattening is needed for the LHS
 canEqLeafFunEqLeft d fl eqv (fn,xis1) s2
- = do { traceTcS "canEqLeafFunEqLeft" $ ppr (evVarPred eqv)
-      ; (xi2,co2) <- flatten d fl s2 -- co2 :: xi2 ~ s2
+ = {-# SCC "canEqLeafFunEqLeft" #-}
+   do { traceTcS "canEqLeafFunEqLeft" $ ppr (evVarPred eqv)
+      ; (xi2,co2) <- 
+          {-# SCC "flatten" #-} 
+          flatten d fl s2 -- co2 :: xi2 ~ s2
       ; let no_flattening_happened = isReflCo co2
       ; if no_flattening_happened then 
             continueWith $ CFunEqCan { cc_id     = eqv
@@ -1158,19 +1185,21 @@ canEqLeafFunEqLeft d fl eqv (fn,xis1) s2
                                      , cc_tyargs = xis1 
                                      , cc_rhs    = xi2 
                                      , cc_depth  = d }
-        else do { delCachedEvVar eqv
-                ; evc <- newEqVar fl (mkTyConApp fn xis1) xi2
+        else do { delCachedEvVar eqv fl
+                ; evc <- 
+                    {-# SCC "newEqVar" #-}
+                    newEqVar fl (mkTyConApp fn xis1) xi2
                 ; let new_eqv = evc_the_evvar evc -- F xis1 ~ xi2 
                       new_cv  = mkEqVarLCo new_eqv
                       cv      = mkEqVarLCo eqv    -- F xis1 ~ s2
-                ; case fl of
-                    Wanted {} -> setEqBind eqv $ new_cv `mkTransCo` co2
-                    Given {}  -> setEqBind new_eqv $ cv `mkTransCo` mkSymCo co2
-                    Derived {} -> return ()
+                ; fl' <- case fl of
+                    Wanted {} -> setEqBind eqv (new_cv `mkTransCo` co2) fl 
+                    Given {}  -> setEqBind new_eqv (cv `mkTransCo` mkSymCo co2) fl
+                    Derived {} -> return fl
                 ; if isNewEvVar evc then 
                       do { continueWith $
                            CFunEqCan { cc_id = new_eqv
-                                     , cc_flavor = fl
+                                     , cc_flavor = fl'
                                      , cc_fun    = fn
                                      , cc_tyargs = xis1 
                                      , cc_rhs    = xi2 
@@ -1186,17 +1215,17 @@ canEqLeafTyVarLeftRec d fl eqv tv s2              -- eqv :: tv ~ s2
        ; (xi1,co1) <- flatten d fl (mkTyVarTy tv) -- co1 :: xi1 ~ tv
        ; if isReflCo co1 then
              canEqLeafTyVarLeft d fl eqv tv s2
-         else do { delCachedEvVar eqv
+         else do { delCachedEvVar eqv fl
                  ; evc <- newEqVar fl xi1 s2  -- new_ev :: xi1 ~ s2
                  ; let new_ev = evc_the_evvar evc
-                 ; case fl of 
-                    Wanted  {} -> setEqBind eqv $ 
-                                  mkSymCo co1 `mkTransCo` mkEqVarLCo new_ev
-                    Given   {} -> setEqBind new_ev $ 
-                                  co1 `mkTransCo` mkEqVarLCo eqv
-                    Derived {} -> return ()
+                 ; fl' <- case fl of 
+                    Wanted  {} -> setEqBind eqv 
+                                    (mkSymCo co1 `mkTransCo` mkEqVarLCo new_ev) fl
+                    Given   {} -> setEqBind new_ev
+                                    (co1 `mkTransCo` mkEqVarLCo eqv) fl
+                    Derived {} -> return fl
                 ; if isNewEvVar evc then
-                      do { canEq d fl new_ev xi1 s2 }
+                      do { canEq d fl' new_ev xi1 s2 }
                   else return Stop
                  }
        }
@@ -1219,8 +1248,9 @@ canEqLeafTyVarLeft d fl eqv tv s2       -- eqv : tv ~ s2
                = True
                | otherwise = False
        ; if is_same_tv then
-             do { delCachedEvVar eqv
-                ; when (isWanted fl) $ setEqBind eqv co 
+             do { delCachedEvVar eqv fl
+                ; when (isWanted fl) $ 
+                       do { _ <- setEqBind eqv co fl; return () }
                 ; return Stop }
          else
     do { -- Do an occurs check, and return a possibly
@@ -1246,21 +1276,21 @@ canEqLeafTyVarLeft d fl eqv tv s2       -- eqv : tv ~ s2
                                          , cc_depth  = d }
          else -- Flattening happened, in any case we have to create new variable 
               -- even if we report an occurs check error
-             do { delCachedEvVar eqv
+             do { delCachedEvVar eqv fl
                 ; evc <- newEqVar fl (mkTyVarTy tv) xi2' 
                 ; let eqv' = evc_the_evvar evc -- eqv' : tv ~ xi2'
                       cv   = mkEqVarLCo eqv    -- cv : tv ~ s2
                       cv'  = mkEqVarLCo eqv'   -- cv': tv ~ xi2'
-                 ; case fl of 
-                     Wanted {}  -> setEqBind eqv (cv' `mkTransCo` co)         -- tv ~ xi2' ~ s2
-                     Given {}   -> setEqBind eqv' (cv `mkTransCo` mkSymCo co) -- tv ~ s2 ~ xi2'
-                     Derived {} -> return ()
+                 ; fl' <- case fl of 
+                     Wanted {}  -> setEqBind eqv (cv' `mkTransCo` co) fl         -- tv ~ xi2' ~ s2
+                     Given {}   -> setEqBind eqv' (cv `mkTransCo` mkSymCo co) fl -- tv ~ s2 ~ xi2'
+                     Derived {} -> return fl
 
                  ; if isNewEvVar evc then 
                        if isNothing occ_check_result then 
                            canEqFailure d fl eqv'
                        else continueWith CTyEqCan { cc_id     = eqv'
-                                                  , cc_flavor = fl
+                                                  , cc_flavor = fl'
                                                   , cc_tyvar  = tv
                                                   , cc_rhs    = xi2' 
                                                   , cc_depth  = d }
diff --git a/compiler/typecheck/TcHsSyn.lhs b/compiler/typecheck/TcHsSyn.lhs
index 4f8cdb2a77..12bb2821fd 100644
--- a/compiler/typecheck/TcHsSyn.lhs
+++ b/compiler/typecheck/TcHsSyn.lhs
@@ -280,7 +280,10 @@ zonkEvBndr :: ZonkEnv -> EvVar -> TcM EvVar
 -- Works for dictionaries and coercions
 -- Does not extend the ZonkEnv
 zonkEvBndr env var 
-  = do { ty <- zonkTcTypeToType env (varType var)
+  = do { let var_ty = varType var
+       ; ty <- 
+           {-# SCC "zonkEvBndr_zonkTcTypeToType" #-}
+           zonkTcTypeToType env var_ty
        ; return (setVarType var ty) }
 
 zonkEvVarOcc :: ZonkEnv -> EvVar -> EvVar
@@ -1103,7 +1106,8 @@ zonkEvBindsVar env (EvBindsVar ref _) = do { bs <- readMutVar ref
 
 zonkEvBinds :: ZonkEnv -> Bag EvBind -> TcM (ZonkEnv, Bag EvBind)
 zonkEvBinds env binds
-  = fixM (\ ~( _, new_binds) -> do
+  = {-# SCC "zonkEvBinds" #-}
+    fixM (\ ~( _, new_binds) -> do
 	 { let env1 = extendIdZonkEnv env (collect_ev_bndrs new_binds)
          ; binds' <- mapBagM (zonkEvBind env1) binds
          ; return (env1, binds') })
@@ -1113,10 +1117,31 @@ zonkEvBinds env binds
     add (EvBind var _) vars = var : vars
 
 zonkEvBind :: ZonkEnv -> EvBind -> TcM EvBind
+
+
 zonkEvBind env (EvBind var term)
-  = do { var' <- zonkEvBndr env var
-       ; term' <- zonkEvTerm env term
-       ; return (EvBind var' term') }
+  = case term of 
+      -- Fast path for reflexivity coercions:
+      EvCoercionBox co 
+        | Just ty <- isReflCo_maybe co
+        ->
+          do { zty  <- zonkTcTypeToType env ty
+             ; let var' = setVarType var (mkEqPred (zty,zty))
+             ; return (EvBind var' (EvCoercionBox (mkReflCo zty))) }
+
+      -- Fast path for variable-variable bindings 
+      -- NB: could be optimized further! (e.g. SymCo cv)
+        | Just {} <- getCoVar_maybe co 
+        -> do { term'@(EvCoercionBox (CoVarCo cv')) <- zonkEvTerm env term
+              ; let var' = setVarType var (varType cv')
+              ; return (EvBind var' term') }
+
+      -- Ugly safe and slow path
+      _ -> do { var'  <- {-# SCC "zonkEvBndr" #-} zonkEvBndr env var
+              ; term' <- zonkEvTerm env term 
+              ; return (EvBind var' term')
+              }
+
 \end{code}
 
 %************************************************************************
@@ -1186,9 +1211,14 @@ mkZonkTcTyVar unbound_mvar_fn unbound_ivar_fn
          FlatSkol ty    -> zonkType zonk_tv ty
          MetaTv _ ref   -> do { cts <- readMutVar ref
            		      ; case cts of    
-           		           Flexi -> do { kind <- zonkType zonk_tv (tyVarKind tv)
+           		           Flexi -> do { kind <- {-# SCC "zonkKind1" #-}
+                                                         zonkType zonk_tv (tyVarKind tv)
                                                ; unbound_mvar_fn (setTyVarKind tv kind) }
-           		           Indirect ty -> zonkType zonk_tv ty }
+           		           Indirect ty -> do { zty <- zonkType zonk_tv ty 
+                                                     -- Small optimisation: shortern-out indirect steps
+                                                     -- so that the old type may be more easily collected.
+                                                     ; writeMutVar ref (Indirect zty)
+                                                     ; return zty } }
 
 zonkTcTypeToType :: ZonkEnv -> TcType -> TcM Type
 zonkTcTypeToType (ZonkEnv zonk_unbound_tyvar tv_env _id_env)
diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index 7fc6a966a4..18f4e552a4 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -51,6 +51,7 @@ import VarEnv
 import qualified Data.Traversable as Traversable
 
 import Control.Monad( when )
+import Pair ( pSnd )
 import UniqFM
 import FastString ( sLit ) 
 import DynFlags
@@ -107,7 +108,7 @@ solveInteractCts cts
           | Just (ev',fl') <- lookupTM pty acc_cache
           , fl' `canSolve` fl
           , isWanted fl
-          = do { setEvBind ev (EvId ev')
+          = do { _ <- setEvBind ev (EvId ev') fl
                ; return (acc_cts,acc_cache) }
           | otherwise -- If it's a given keep it in the work list, even if it exists in the cache!
           = return (ct:acc_cts, alterTM pty (\_ -> Just (ev,fl)) acc_cache)
@@ -136,10 +137,12 @@ solveInteractWanted wevs
 solveInteract :: TcS ()
 -- Returns the final InertSet in TcS, WorkList will be eventually empty.
 solveInteract
-  = do { dyn_flags <- getDynFlags
+  = {-# SCC "solveInteract" #-}
+    do { dyn_flags <- getDynFlags
        ; let max_depth = ctxtStkDepth dyn_flags
              solve_loop
-              = do { sel <- selectNextWorkItem max_depth
+              = {-# SCC "solve_loop" #-}
+                do { sel <- selectNextWorkItem max_depth
                    ; case sel of 
                       NoWorkRemaining     -- Done, successfuly (modulo frozen)
                         -> return ()
@@ -236,12 +239,7 @@ React with (F Int ~ b) ==> IR Stop True []    -- after substituting we re-canoni
 \begin{code}
 thePipeline :: [(String,SimplifierStage)]
 thePipeline = [ ("canonicalization",        canonicalizationStage)
-                -- If ContinueWith, will be canonical and fully rewritten wrt inert eqs
-              , ("interact the inert eqs", interactWithInertEqsStage)
-                -- If ContinueWith, will be wanted/derived eq or non-eq
-                -- but can't rewrite not can be rewritten by the inerts
               , ("spontaneous solve",       spontaneousSolveStage)
-                -- If ContinueWith its not spontaneously solved equality
               , ("interact with inerts",    interactWithInertsStage)
               , ("top-level reactions",     topReactionsStage) ]
 \end{code}
@@ -292,70 +290,124 @@ spontaneousSolveStage :: SimplifierStage
 spontaneousSolveStage workItem
   = do { mSolve <- trySpontaneousSolve workItem
        ; spont_solve mSolve } 
-  where spont_solve SPCantSolve = continueWith workItem 
-        spont_solve (SPSolved workItem')
+  where spont_solve SPCantSolve 
+          | isCTyEqCan workItem                    -- Unsolved equality
+          = do { kickOutRewritableInerts workItem  -- NB: will add workItem in inerts
+               ; return Stop }
+          | otherwise
+          = continueWith workItem
+        spont_solve (SPSolved workItem')           -- Post: workItem' must be equality
           = do { bumpStepCountTcS
                ; traceFireTcS (cc_depth workItem) $
                  ptext (sLit "Spontaneous") 
                            <+> parens (ppr (cc_flavor workItem)) <+> ppr workItem
-               -- If original was /not/ given we may have to kick out now-rewritable inerts
-               ; when (not (isGivenOrSolvedCt workItem)) $
-                 kickOutRewritableInerts workItem'
-               -- Add solved guy in inerts anyway
-               ; updInertSetTcS workItem'
-               -- .. and Stop 
+
+                 -- NB: will add the item in the inerts
+               ; kickOutRewritableInerts workItem'
+               -- .. and Stop
                ; return Stop }
 
 kickOutRewritableInerts :: Ct -> TcS () 
 -- Pre:  ct is a CTyEqCan 
--- Post: the TcS monad is left with the thinner non-rewritable inerts; the 
---       rewritable end up in the worklist
+-- Post: The TcS monad is left with the thinner non-rewritable inerts; but which
+--       contains the new constraint.
+--       The rewritable end up in the worklist
 kickOutRewritableInerts ct
-  = do { (wl,ieqs,solved_out) <- modifyInertTcS (kick_out_rewritable ct)
-
-       -- Rewrite the inert_eqs on the spot! 
-       ; let ct_subst = unitVarEnv (cc_tyvar ct) (ct, mkEqVarLCo (cc_id ct))
-             inscope  = mkInScopeSet $ tyVarsOfCt ct
-
-       ; new_ieqs <- rewriteInertEqsFromInertEq (ct_subst,inscope) ieqs
+  = {-# SCC "kickOutRewritableInerts" #-}
+    do { (wl,ieqs) <- {-# SCC "kick_out_rewritable" #-}
+                      modifyInertTcS (kick_out_rewritable ct)
+
+       -- Step 1: Rewrite as many of the inert_eqs on the spot! 
+       -- NB: if it is a solved constraint just use the cached evidence
+       ; let ct_coercion 
+               | Just (GivenSolved (Just (EvCoercionBox co))) <- isGiven_maybe (cc_flavor ct)
+               = co 
+               | otherwise 
+               = mkEqVarLCo (cc_id ct)
+
+       ; new_ieqs <- {-# SCC "rewriteInertEqsFromInertEq" #-}
+                     rewriteInertEqsFromInertEq (cc_tyvar ct,ct_coercion, cc_flavor ct) ieqs
        ; modifyInertTcS (\is -> ((), is { inert_eqs = new_ieqs }))
 
-
-       -- Rewrite the rewritable solved on the spot and stick them back in the inerts
-       ; _unused <- mapBagM (rewrite_solved (ct_subst,inscope)) solved_out
+       -- Step 2: Add the new guy in
+       ; updInertSetTcS ct
 
        ; traceTcS "Kick out" (ppr ct $$ ppr wl)
        ; updWorkListTcS (unionWorkList wl) }
 
-  where rewrite_solved inert_eqs solved_ct 
-          = do { (new_ev,_) <- rewriteFromInertEqs inert_eqs fl ev
-               ; mk_canonical new_ev }
-          where fl = cc_flavor solved_ct
-                ev = cc_id solved_ct
-                d  = cc_depth solved_ct
-                mk_canonical new_ev
-                  -- A bit of an overkill to call the canonicalizer, but ok ...
-                  = do { let new_pty = evVarPred new_ev
-                       ; r <- canEvVar new_ev (classifyPredType new_pty) d fl
-                       ; case r of
-                           Stop -> return ()
-                           ContinueWith ct -> updInertSetTcS ct }
-
-
-rewriteInertEqsFromInertEq :: (TyVarEnv (Ct,Coercion), InScopeSet) -- A new substitution
-                           -> TyVarEnv (Ct,Coercion)               -- The inert equalities
-                           -> TcS (TyVarEnv (Ct,Coercion))         -- The new inert equalities
-rewriteInertEqsFromInertEq the_subst ieqs = Traversable.mapM do_one ieqs
- where do_one (ct,co)
-        | ev <- cc_id ct, fl <- cc_flavor ct
-        = do { (new_ev,not_rewritten) <- rewriteFromInertEqs the_subst fl ev
-             ; let EqPred _ xi = classifyPredType (evVarPred new_ev)
-             ; if not_rewritten then 
-                   return (ct,co) -- return the same
+rewriteInertEqsFromInertEq :: (TcTyVar,Coercion, CtFlavor) -- A new substitution
+                           -> TyVarEnv (Ct,Coercion)       -- All inert equalities
+                           -> TcS (TyVarEnv (Ct,Coercion)) -- The new inert equalities
+rewriteInertEqsFromInertEq (subst_tv,subst_co, subst_fl) ieqs
+-- The goal: traverse the inert equalities:
+--    1) If current inert element cannot itself rewrite subst_fl then:
+--           a) if it is rewritable by subst fl throw him out
+--           b) if it is not rewritable by subst keep him in as is
+--    2) otherwise
+--           a) if it is rewritable by subst fl rewrite him on the spot
+--           b) if it is not rewritable by subst fl then keep him as is
+
+ = do { mieqs <- Traversable.mapM do_one ieqs -- mieqs :: TyVarEnv (Maybe (Ct,Coercion))
+      ; case Traversable.sequence mieqs of 
+          Nothing         -> return emptyVarEnv
+          Just final_ieqs -> return final_ieqs }
+
+ where do_one (ct,inert_co)
+        | (not (subst_fl `canRewrite` fl)) || isReflCo co
+        -- If the inert is not rewritable we just keep it
+        = return (Just (ct,inert_co))
+        -- Inert is definitely rewritable
+        | not (fl `canRewrite` subst_fl)  -- But the inert cannot itself rewrite the subst item
+                                          -- so there is need for recanonicalization.
+        = do { updWorkListTcS (extendWorkListEq ct) 
+             ; return Nothing }
+        | otherwise -- Or the inert can rewrite subst as well, so it's safe to rewrite on-the-spot
+        = do { let rhs' = pSnd (liftedCoercionKind co)
+             ; delCachedEvVar ev fl
+             ; evc <- newEqVar fl (mkTyVarTy tv) rhs'
+             ; let ev' = evc_the_evvar evc
+             ; let evco' = mkEqVarLCo ev' 
+             ; fl' <- if isNewEvVar evc then
+                   do { case fl of 
+                          Wanted  {} -> setEqBind ev  
+                                            (evco' `mkTransCo` mkSymCo co) fl
+                          Given   {} -> setEqBind ev' 
+                                            (mkEqVarLCo ev `mkTransCo` co) fl
+                          Derived {} -> return fl }
                else
-                   return (ct { cc_id = new_ev, cc_rhs = xi }, mkEqVarLCo new_ev) }
+                   if (isWanted fl) then 
+                       setEqBind ev (evco' `mkTransCo` mkSymCo co) fl
+                   else
+                       return fl
+
+             ; let ct' = ct { cc_id = ev', cc_flavor = fl', cc_rhs = rhs' }
+             ; return (Just (ct',evco')) }
+        where ev  = cc_id ct
+              fl  = cc_flavor ct
+              tv  = cc_tyvar ct
+              rhs = cc_rhs ct
+              co  = liftCoSubstWith [subst_tv] [subst_co] rhs
+
+
+
+--     (eqs_out,   eqs_in)   = partitionEqMap
+--                                (\inert_ct -> (not (cc_flavor inert_ct `canRewrite` fl)) && 
+--                                              rewritable inert_ct) eqmap
+--          -- Why not just (rewritable_inert ct)? Check out Note [Delicate equality kick-out]
+
 
-kick_out_rewritable :: Ct -> InertSet -> ((WorkList,TyVarEnv (Ct,Coercion),Cts), InertSet)
+
+-- {- 
+--                   traceTcS "rewriteInertEqsFromInertEq" $ 
+--                         vcat [ text "rewriting equality: " <+> ppr ct
+--                              , text "from: " <+> ppr subst_co <+> text "of flavor: " <+> ppr subst_fl 
+--                              , text "can rewrite? " <+> ppr (subst_fl `canRewrite` fl) ]
+--            -}
+
+
+
+kick_out_rewritable :: Ct -> InertSet -> ((WorkList,TyVarEnv (Ct,Coercion)), InertSet)
+-- Returns ALL equalities, to be dealt with later
 kick_out_rewritable ct (IS { inert_eqs    = eqmap
                            , inert_eq_tvs = inscope
                            , inert_dicts  = dictmap
@@ -364,15 +416,14 @@ kick_out_rewritable ct (IS { inert_eqs    = eqmap
                            , inert_irreds = irreds
                            , inert_frozen = frozen
                            } )
-  = ((kicked_out, eqs_in, feqs_out_solved `andCts` dicts_out_solved), remaining)
+  = ((kicked_out, eqmap), remaining)
   where
-
-    kicked_out = WorkList { wl_eqs    = eqs_out
+    kicked_out = WorkList { wl_eqs    = []
                           , wl_funeqs = bagToList feqs_out
                           , wl_rest   = bagToList (fro_out `andCts` dicts_out 
                                           `andCts` ips_out `andCts` irs_out) }
   
-    remaining = IS { inert_eqs = eqs_in
+    remaining = IS { inert_eqs = emptyVarEnv
                    , inert_eq_tvs = inscope -- keep the same, safe and cheap
                    , inert_dicts = dicts_in
                    , inert_ips = ips_in
@@ -383,39 +434,46 @@ kick_out_rewritable ct (IS { inert_eqs    = eqmap
 
     fl = cc_flavor ct
     tv = cc_tyvar ct
-          
-    (eqs_out,   eqs_in)   = partitionEqMap
-                               (\inert_ct -> rewritable inert_ct && 
-                                             not (cc_flavor inert_ct `canRewrite` fl)) eqmap
-                               -- Delicate: 
-                               -- We want to throw out only the rewritables which cannot
-                               -- themselves rewrite the workitem. Because, what will remain
-                               -- in eqs_in, even if rewritable, can be readily substituted
-                               -- in-place from the new item, without dangers for occurs
-                               -- loops or further need for canonicalization.
+                               
+    (ips_out,   ips_in)     = partitionCCanMap rewritable ipmap
 
-    (ips_out,   ips_in)         = partitionCCanMap rewritable ipmap
-
-    (feqs_out_all,  feqs_in)    = partitionCtTypeMap rewritable funeqmap
-    (feqs_out_solved, feqs_out) = partitionBag is_solved feqs_out_all
-
-    (dicts_out_all, dicts_in) = partitionCCanMap rewritable dictmap
-    (dicts_out_solved, dicts_out) = partitionBag is_solved dicts_out_all
+    (feqs_out,  feqs_in)    = partitionCtTypeMap rewritable funeqmap
+    (dicts_out, dicts_in)   = partitionCCanMap rewritable dictmap
 
     (irs_out,   irs_in)   = partitionBag rewritable irreds
     (fro_out,   fro_in)   = partitionBag rewritable frozen
 
     rewritable ct = (fl `canRewrite` cc_flavor ct)  &&
                     (tv `elemVarSet` tyVarsOfCt ct)
+\end{code}
+
+Note [Delicate equality kick-out]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
 
-    is_solved ct
-      | Just GivenSolved <- isGiven_maybe (cc_flavor ct)
-      = True
-      | otherwise = False
+Delicate:
+When kicking out rewritable constraints, it would be safe to simply
+kick out all rewritable equalities, but instead we only kick out those
+that, when rewritten, may result in occur-check errors. We rewrite the
+rest on the spot. Example:
 
-      
+          WorkItem =   [S] a ~ b
+          Inerts   = { [W] b ~ [a] }
+Now at this point the work item cannot be further rewritten by the
+inert (due to the weaker inert flavor), so we are examining if we can
+instead rewrite the inert from the workitem. But if we rewrite it on
+the spot we have to recanonicalize because of the danger of occurs
+errors.  On the other hand if the inert flavor was just as powerful or
+more powerful than the workitem flavor, the work-item could not have
+reached this stage (because it would have already been rewritten by
+the inert).
 
-                             
+The coclusion is: we kick out the 'dangerous' equalities that may
+require recanonicalization (occurs checks) and the rest we rewrite
+unconditionally without further checks, on-the-spot with function
+rewriteInertEqsFromInertEq.
+
+
+\begin{code}
 data SPSolveResult = SPCantSolve
                    | SPSolved WorkItem 
 
@@ -484,21 +542,7 @@ trySpontaneousEqTwoWay d eqv gw tv1 tv2
     k1 = tyVarKind tv1
     k2 = tyVarKind tv2
     nicer_to_update_tv2 = isSigTyVar tv1 || isSystemName (Var.varName tv2)
-{-
--- Previous code below (before kind polymorphism and unification):
-  -- | k1 `isSubKind` k2
-  -- , nicer_to_update_tv2 = solveWithIdentity eqv gw tv2 (mkTyVarTy tv1)
-  -- | k2 `isSubKind` k1 
-  -- = solveWithIdentity eqv gw tv1 (mkTyVarTy tv2)
-  -- | otherwise -- None is a subkind of the other, but they are both touchable! 
-  -- = return SPCantSolve
-  --   -- do { addErrorTcS KindError gw (mkTyVarTy tv1) (mkTyVarTy tv2)
-  --   --   ; return SPError }
-  -- where
-  --   k1 = tyVarKind tv1
-  --   k2 = tyVarKind tv2
-  --   nicer_to_update_tv2 = isSigTyVar tv1 || isSystemName (Var.varName tv2)
--}
+
 \end{code}
 
 Note [Kind errors] 
@@ -584,7 +628,7 @@ solveWithIdentity :: SubGoalDepth
 --        workItem = the new Given constraint
 solveWithIdentity d eqv wd tv xi 
   = do { traceTcS "Sneaky unification:" $ 
-                       vcat [text "Coercion variable:  " <+> ppr wd, 
+                       vcat [text "Coercion variable:  " <+> ppr eqv <+> ppr wd, 
                              text "Coercion:           " <+> pprEq (mkTyVarTy tv) xi,
                              text "Left  Kind is     : " <+> ppr (typeKind (mkTyVarTy tv)),
                              text "Right Kind is     : " <+> ppr (typeKind xi)
@@ -593,36 +637,16 @@ solveWithIdentity d eqv wd tv xi
        ; setWantedTyBind tv xi
        ; let refl_xi = mkReflCo xi
 
-       ; let solved_fl = mkSolvedFlavor wd UnkSkol 
-       ; eqv_given <- newGivenEqVar solved_fl (mkTyVarTy tv) xi refl_xi
+       ; let solved_fl = mkSolvedFlavor wd UnkSkol (EvCoercionBox refl_xi) 
+       ; (_,eqv_given) <- newGivenEqVar solved_fl (mkTyVarTy tv) xi refl_xi
 
-       ; when (isWanted wd) (setEqBind eqv refl_xi)
+       ; when (isWanted wd) $ do { _ <- setEqBind eqv refl_xi wd; return () }
            -- We don't want to do this for Derived, that's why we use 'when (isWanted wd)'
        ; return $ SPSolved (CTyEqCan { cc_id     = eqv_given
                                      , cc_flavor = solved_fl
                                      , cc_tyvar  = tv, cc_rhs = xi, cc_depth = d }) }
 \end{code}
 
-*********************************************************************************
-*                                                                               *
-*                         Interact with inert equalities                        *
-*                                                                               *
-*********************************************************************************
-
-\begin{code}
-
-interactWithInertEqsStage  :: WorkItem -> TcS StopOrContinue
-interactWithInertEqsStage  ct 
-  | isCTyEqCan ct
-  = do { kickOutRewritableInerts ct
-       ; if isGivenOrSolved (cc_flavor ct) then updInertSetTcS ct >> return Stop
-         else continueWith ct } -- If wanted or derived we may spontaneously solve him
-  | isCNonCanonical ct
-  = pprPanic "Interact with inerts eqs stage met non-canonical constraint!" (ppr ct)
-  | otherwise
-  = continueWith ct
-\end{code}
-
 
 *********************************************************************************
 *                                                                               * 
@@ -798,9 +822,8 @@ doInteractWithInert (CIPCan { cc_id = id1, cc_flavor = ifl, cc_ip_nm = nm1, cc_i
            Given   {} -> pprPanic "Unexpected given IP" (ppr workItem)
            Derived {} -> pprPanic "Unexpected derived IP" (ppr workItem)
            Wanted  {} ->
-               do { setEvBind (cc_id workItem) $ 
-                    mkEvCast id1 (mkSymCo (mkTyConAppCo (ipTyCon nm1) [mkEqVarLCo (evc_the_evvar eqv)]))
-                    -- DV: Changing: used to be (mkSymCo (mkEqVarLCo eqv))
+               do { _ <- setEvBind (cc_id workItem) 
+                            (mkEvCast id1 (mkSymCo (mkTyConAppCo (ipTyCon nm1) [mkEqVarLCo (evc_the_evvar eqv)]))) wfl
                   ; irWorkItemConsumed "IP/IP (solved by rewriting)" } }
 
 doInteractWithInert (CFunEqCan { cc_id = eqv1, cc_flavor = fl1, cc_fun = tc1
@@ -808,13 +831,13 @@ doInteractWithInert (CFunEqCan { cc_id = eqv1, cc_flavor = fl1, cc_fun = tc1
                     (CFunEqCan { cc_id = eqv2, cc_flavor = fl2, cc_fun = tc2
                                , cc_tyargs = args2, cc_rhs = xi2, cc_depth = d2 })
   | lhss_match  
-  , Just GivenSolved <- isGiven_maybe fl1 -- Inert is solved and we can simply ignore it
+  , Just (GivenSolved {}) <- isGiven_maybe fl1 -- Inert is solved and we can simply ignore it
                                           -- when workitem is given/solved
   , isGivenOrSolved fl2
   = irInertConsumed "FunEq/FunEq"
   | lhss_match 
-  , Just GivenSolved <- isGiven_maybe fl2 -- Workitem is solved and we can ignore it when
-                                          -- the inert is given/solved
+  , Just (GivenSolved {}) <- isGiven_maybe fl2 -- Workitem is solved and we can ignore it when
+                                               -- the inert is given/solved
   , isGivenOrSolved fl1                 
   = irWorkItemConsumed "FunEq/FunEq" 
   | fl1 `canSolve` fl2 && lhss_match
@@ -839,40 +862,40 @@ rewriteEqLHS :: WhichComesFromInert -> (EqVar,Xi) -> (EqVar,SubGoalDepth,CtFlavo
 -- We have an option of creating new work (xi1 ~ xi2) OR (xi2 ~ xi1), 
 --    See Note [Efficient Orientation] for that 
 rewriteEqLHS LeftComesFromInert (eqv1,xi1) (eqv2,d,gw,xi2) 
-  = do { delCachedEvVar eqv2 -- Similarly to canonicalization!
+  = do { delCachedEvVar eqv2 gw -- Similarly to canonicalization!
        ; evc <- newEqVar gw xi2 xi1
        ; let eqv2' = evc_the_evvar evc
-       ; case gw of 
+       ; gw' <- case gw of 
            Wanted {} 
-               -> setEqBind eqv2 $ 
-                  mkEqVarLCo eqv1 `mkTransCo` mkSymCo (mkEqVarLCo eqv2')
-           Given {}  
-               -> setEqBind eqv2' $ 
-                  mkSymCo (mkEqVarLCo eqv2) `mkTransCo` mkEqVarLCo eqv1
+               -> setEqBind eqv2 
+                    (mkEqVarLCo eqv1 `mkTransCo` mkSymCo (mkEqVarLCo eqv2')) gw
+           Given {}
+               -> setEqBind eqv2'
+                    (mkSymCo (mkEqVarLCo eqv2) `mkTransCo` mkEqVarLCo eqv1) gw
            Derived {} 
-               -> return ()
+               -> return gw
        ; when (isNewEvVar evc) $ 
               updWorkListTcS (extendWorkListEq (CNonCanonical { cc_id     = eqv2'
-                                                              , cc_flavor = gw
+                                                              , cc_flavor = gw'
                                                               , cc_depth  = d } ) ) }
 
 rewriteEqLHS RightComesFromInert (eqv1,xi1) (eqv2,d,gw,xi2) 
-  = do { delCachedEvVar eqv2 -- Similarly to canonicalization!
+  = do { delCachedEvVar eqv2 gw -- Similarly to canonicalization!
        ; evc <- newEqVar gw xi1 xi2
        ; let eqv2' = evc_the_evvar evc
-       ; case gw of
+       ; gw' <- case gw of
            Wanted {} 
-               -> setEqBind eqv2 $ 
-                  mkEqVarLCo eqv1 `mkTransCo` mkEqVarLCo eqv2'
+               -> setEqBind eqv2
+                    (mkEqVarLCo eqv1 `mkTransCo` mkEqVarLCo eqv2') gw
            Given {}  
-               -> setEqBind eqv2' $
-                  mkSymCo (mkEqVarLCo eqv1) `mkTransCo` mkEqVarLCo eqv2
+               -> setEqBind eqv2'
+                    (mkSymCo (mkEqVarLCo eqv1) `mkTransCo` mkEqVarLCo eqv2) gw
            Derived {} 
-               -> return ()
+               -> return gw
 
        ; when (isNewEvVar evc) $
               updWorkListTcS (extendWorkListEq (CNonCanonical { cc_id = eqv2'
-                                                              , cc_flavor = gw
+                                                              , cc_flavor = gw'
                                                               , cc_depth  = d } ) ) }
 
 solveOneFromTheOther :: String             -- Info 
@@ -891,14 +914,14 @@ solveOneFromTheOther info (ev_term,ifl) workItem
 		  -- so it's safe to continue on from this point
   = irInertConsumed ("Solved[DI] " ++ info)
   
-  | Just GivenSolved <- isGiven_maybe ifl, isGivenOrSolved wfl
+  | Just (GivenSolved {}) <- isGiven_maybe ifl, isGivenOrSolved wfl
     -- Same if the inert is a GivenSolved -- just get rid of it
   = irInertConsumed ("Solved[SI] " ++ info)
 
   | otherwise
   = ASSERT( ifl `canSolve` wfl )
       -- Because of Note [The Solver Invariant], plus Derived dealt with
-    do { when (isWanted wfl) $ setEvBind wid ev_term
+    do { when (isWanted wfl) $ do { _ <- setEvBind wid ev_term wfl; return () }
            -- Overwrite the binding, if one exists
 	   -- If both are Given, we already have evidence; no need to duplicate
        ; irWorkItemConsumed ("Solved " ++ info) }
@@ -1350,30 +1373,32 @@ doTopReact inerts workItem@(CDictCan { cc_flavor = fl@(Wanted loc)
          doSolveFromInstance wtvs ev_term workItem
             | null wtvs
             = do { traceTcS "doTopReact/found nullary instance for" (ppr (cc_id workItem))
-                 ; setEvBind (cc_id workItem) ev_term
+                 ; _ <- setEvBind (cc_id workItem) ev_term fl
                  ; return $ 
                    SomeTopInt { tir_rule = "Dict/Top (solved, no new work)" 
                               , tir_new_item = Stop } } -- Don't put him in the inerts
             | otherwise 
             = do { traceTcS "doTopReact/found non-nullary instance for" $ 
                    ppr (cc_id workItem)
-                 ; setEvBind (cc_id workItem) ev_term 
+                 ; _ <- setEvBind (cc_id workItem) ev_term fl
                         -- Solved and new wanted work produced, you may cache the 
                         -- (tentatively solved) dictionary as Solved given.
-                 ; let solved = workItem { cc_flavor = solved_fl }
-                       solved_fl = mkSolvedFlavor fl UnkSkol
+--                 ; let _solved = workItem { cc_flavor = solved_fl }
+--                       solved_fl = mkSolvedFlavor fl UnkSkol
                  ; let ct_from_wev (EvVarX v fl)
                            = CNonCanonical { cc_id = v, cc_flavor = Wanted fl
                                            , cc_depth  = cc_depth workItem + 1 }
                        wtvs_cts = map ct_from_wev wtvs
                  ; updWorkListTcS (appendWorkListCt wtvs_cts)
-                 ; return $ 
+                 ; return $
                    SomeTopInt { tir_rule     = "Dict/Top (solved, more work)"
-                              , tir_new_item = ContinueWith solved } } -- Cache in inerts the Solved item
+                              , tir_new_item = Stop }
+                 }
+--                              , tir_new_item = ContinueWith solved } } -- Cache in inerts the Solved item
 
 -- Type functions
 doTopReact _inerts (CFunEqCan { cc_flavor = fl })
-  | Just GivenSolved <- isGiven_maybe fl
+  | Just (GivenSolved {}) <- isGiven_maybe fl
   = return NoTopInt -- If Solved, no more interactions should happen
 
 -- Otherwise, it's a Given, Derived, or Wanted
@@ -1394,25 +1419,29 @@ doTopReact _inerts workItem@(CFunEqCan { cc_id = eqv, cc_flavor = fl
                    ; case fl of
                        Wanted {} -> do { evc <- newEqVar fl rhs_ty xi -- Wanted version
                                        ; let eqv' = evc_the_evvar evc
-                                       ; setEqBind eqv (coe `mkTransCo` mkEqVarLCo eqv')
+                                       ; let coercion = coe `mkTransCo` mkEqVarLCo eqv'
+                                       ; _ <- setEqBind eqv coercion fl
                                        ; when (isNewEvVar evc) $ 
                                             (let ct = CNonCanonical { cc_id = eqv'
                                                                     , cc_flavor = fl 
                                                                     , cc_depth = cc_depth workItem + 1} 
                                              in updWorkListTcS (extendWorkListEq ct))
 
-                                       ; let solved = workItem { cc_flavor = solved_fl }
-                                             solved_fl = mkSolvedFlavor fl UnkSkol
+                                       ; let _solved   = workItem { cc_flavor = solved_fl }
+                                             solved_fl = mkSolvedFlavor fl UnkSkol (EvCoercionBox coercion)
+
+                                       ; updateFlatCache eqv solved_fl tc args xi WhenSolved
 
                                        ; return $ 
                                          SomeTopInt { tir_rule = "Fun/Top (solved, more work)"
-                                                    , tir_new_item = ContinueWith solved } }
+                                                    , tir_new_item = Stop } }
+                                                  --  , tir_new_item = ContinueWith solved } }
                                                      -- Cache in inerts the Solved item
 
-                       Given {} -> do { eqv' <- newGivenEqVar fl xi rhs_ty $ 
-                                                mkSymCo (mkEqVarLCo eqv) `mkTransCo` coe
+                       Given {} -> do { (fl',eqv') <- newGivenEqVar fl xi rhs_ty $ 
+                                                         mkSymCo (mkEqVarLCo eqv) `mkTransCo` coe
                                       ; let ct = CNonCanonical { cc_id = eqv'
-                                                               , cc_flavor = fl
+                                                               , cc_flavor = fl'
                                                                , cc_depth = cc_depth workItem + 1}  
                                       ; updWorkListTcS (extendWorkListEq ct) 
 
diff --git a/compiler/typecheck/TcRnTypes.lhs b/compiler/typecheck/TcRnTypes.lhs
index da2c8981ed..a7074e6207 100644
--- a/compiler/typecheck/TcRnTypes.lhs
+++ b/compiler/typecheck/TcRnTypes.lhs
@@ -71,7 +71,7 @@ module TcRnTypes(
 	SkolemInfo(..),
 
         CtFlavor(..), pprFlavorArising, isWanted, 
-        isGivenOrSolved, isGiven_maybe,
+        isGivenOrSolved, isGiven_maybe, isSolved,
         isDerived,
 
 	-- Pretty printing
@@ -1210,14 +1210,17 @@ data CtFlavor
 
 data GivenKind
   = GivenOrig   -- Originates in some given, such as signature or pattern match
-  | GivenSolved -- Is given as result of being solved, maybe provisionally on
-                -- some other wanted constraints. 
+  | GivenSolved (Maybe EvTerm) 
+                -- Is given as result of being solved, maybe provisionally on
+                -- some other wanted constraints. We cache the evidence term 
+                -- sometimes here as well /as well as/ in the EvBinds, 
+                -- see note [Optimizing Spontaneously Solved Coercions]
 
 instance Outputable CtFlavor where
-  ppr (Given _ GivenOrig)   = ptext (sLit "[G]")
-  ppr (Given _ GivenSolved) = ptext (sLit "[S]") -- Print [S] for Given/Solved's
-  ppr (Wanted {})           = ptext (sLit "[W]")
-  ppr (Derived {})          = ptext (sLit "[D]") 
+  ppr (Given _ GivenOrig)        = ptext (sLit "[G]")
+  ppr (Given _ (GivenSolved {})) = ptext (sLit "[S]") -- Print [S] for Given/Solved's
+  ppr (Wanted {})                = ptext (sLit "[W]")
+  ppr (Derived {})               = ptext (sLit "[D]")
 
 pprFlavorArising :: CtFlavor -> SDoc
 pprFlavorArising (Derived wl)   = pprArisingAt wl
@@ -1232,6 +1235,10 @@ isGivenOrSolved :: CtFlavor -> Bool
 isGivenOrSolved (Given {}) = True
 isGivenOrSolved _ = False
 
+isSolved :: CtFlavor -> Bool
+isSolved (Given _ (GivenSolved {})) = True
+isSolved _ = False
+
 isGiven_maybe :: CtFlavor -> Maybe GivenKind 
 isGiven_maybe (Given _ gk) = Just gk
 isGiven_maybe _            = Nothing
diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs
index a777706f86..e1e1d96b8e 100644
--- a/compiler/typecheck/TcSMonad.lhs
+++ b/compiler/typecheck/TcSMonad.lhs
@@ -47,8 +47,6 @@ module TcSMonad (
 
        -- Setting evidence variables 
     setEqBind,
-    setIPBind,
-    setDictBind,
     setEvBind,
 
     setWantedTyBind,
@@ -62,7 +60,7 @@ module TcSMonad (
 
         -- Inerts 
     InertSet(..), 
-    getInertEqs, rewriteFromInertEqs, liftInertEqsTy,
+    getInertEqs, liftInertEqsTy,
     emptyInert, getTcSInerts, updInertSet, extractUnsolved,
     extractUnsolvedTcS, modifyInertTcS,
     updInertSetTcS, partitionCCanMap, partitionEqMap,
@@ -125,7 +123,7 @@ import Bag
 import MonadUtils
 import VarSet
 
-import Pair ( pSnd )
+-- import Pair ( pSnd )
 import FastString
 import Util
 
@@ -493,9 +491,17 @@ updInertSet is item
   | isCTyEqCan item                     
   = let upd_err a b = pprPanic "updInertSet" $ 
                       vcat [text "Multiple inert equalities:", ppr a, ppr b]
+                           
+        -- If evidence is cached, pick it up from the flavor!
+        coercion 
+          | Just (GivenSolved (Just (EvCoercionBox co))) <- isGiven_maybe (cc_flavor item)
+          = co
+          | otherwise 
+          = mkEqVarLCo (cc_id item)
+
         eqs'     = extendVarEnv_C upd_err (inert_eqs is)
                                           (cc_tyvar item)
-                                          (item, mkEqVarLCo (cc_id item))
+                                          (item, coercion)
         inscope' = extendInScopeSetSet (inert_eq_tvs is) (tyVarsOfCt item)
     in is { inert_eqs = eqs', inert_eq_tvs = inscope' }
 
@@ -668,11 +674,11 @@ combineCtLoc (Derived loc ) _  = loc
 combineCtLoc _ (Derived loc )  = loc
 combineCtLoc _ _ = panic "combineCtLoc: both given"
 
-mkSolvedFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
+mkSolvedFlavor :: CtFlavor -> SkolemInfo -> EvTerm -> CtFlavor
 -- To be called when we actually solve a wanted/derived (perhaps leaving residual goals)
-mkSolvedFlavor (Wanted  loc) sk  = Given (setCtLocOrigin loc sk) GivenSolved
-mkSolvedFlavor (Derived loc) sk  = Given (setCtLocOrigin loc sk) GivenSolved
-mkSolvedFlavor fl@(Given {}) _sk = pprPanic "Solving a given constraint!" $ ppr fl
+mkSolvedFlavor (Wanted  loc) sk  evterm  = Given (setCtLocOrigin loc sk) (GivenSolved (Just evterm))
+mkSolvedFlavor (Derived loc) sk  evterm  = Given (setCtLocOrigin loc sk) (GivenSolved (Just evterm))
+mkSolvedFlavor fl@(Given {}) _sk _evterm = pprPanic "Solving a given constraint!" $ ppr fl
 
 mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
 mkGivenFlavor (Wanted  loc) sk  = Given (setCtLocOrigin loc sk) GivenOrig
@@ -1058,8 +1064,8 @@ getTcEvBindsMap
        ; wrapTcS $ TcM.readTcRef ev_ref }
 
 
-setEqBind :: EqVar -> LCoercion -> TcS () 
-setEqBind eqv co = setEvBind eqv (EvCoercionBox co)
+setEqBind :: EqVar -> LCoercion -> CtFlavor -> TcS CtFlavor
+setEqBind eqv co fl = setEvBind eqv (EvCoercionBox co) fl
 
 setWantedTyBind :: TcTyVar -> TcType -> TcS () 
 -- Add a type binding
@@ -1075,15 +1081,10 @@ setWantedTyBind tv ty
                        , text "Old value =" <+> ppr (lookupVarEnv_NF ty_binds tv)]
             ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
 
-setIPBind :: EvVar -> EvTerm -> TcS () 
-setIPBind = setEvBind 
-
-setDictBind :: EvVar -> EvTerm -> TcS () 
-setDictBind = setEvBind 
 
-setEvBind :: EvVar -> EvTerm -> TcS () 
--- Internal
-setEvBind ev t
+setEvBind :: EvVar -> EvTerm -> CtFlavor -> TcS CtFlavor
+-- If the flavor is Solved, we cache the new evidence term inside the returned flavor
+setEvBind ev t fl
   = do { tc_evbinds <- getTcEvBinds
        ; wrapTcS $ TcM.addTcEvBind tc_evbinds ev t
 
@@ -1092,6 +1093,11 @@ setEvBind ev t
        ; let cycle = any (reaches binds) (evterm_evs t)
        ; when cycle (fail_if_co_loop binds)
 #endif
+       ; return $ 
+         case fl of 
+           Given gl (GivenSolved _) 
+               -> Given gl (GivenSolved (Just t))
+           _   -> fl
        }
 
 #ifdef DEBUG
@@ -1275,7 +1281,9 @@ newEvVar :: CtFlavor -> TcPredType -> TcS EvVarCreated
 --     the call sites for this invariant to be quickly restored.
 newEvVar fl pty
   | isGivenOrSolved fl    -- Create new variable and update the cache
-  = do { eref <- getTcSEvVarCache
+  = do { 
+{- We lose a lot of time if we enable this check:
+         eref <- getTcSEvVarCache
        ; ecache <- wrapTcS (TcM.readTcRef eref)
        ; case lookupTM pty (evc_cache ecache) of
            Just (_,cached_fl) 
@@ -1283,11 +1291,13 @@ newEvVar fl pty
                -> pprTrace "Interesting: given newEvVar, missed caching opportunity!" empty $
                   return ()
            _ -> return ()
-       ; new <- forceNewEvVar fl pty
+-}
+         new <- forceNewEvVar fl pty
        ; return (EvVarCreated True new) }
 
   | otherwise             -- Otherwise lookup first
-  = do { eref <- getTcSEvVarCache
+  = {-# SCC "newEvVarWanted" #-}
+    do { eref <- getTcSEvVarCache
        ; ecache <- wrapTcS (TcM.readTcRef eref)
        ; case lookupTM pty (evc_cache ecache) of
            Just (cached_evvar, cached_flavor)
@@ -1338,9 +1348,10 @@ updateCache ecache (ev,fl,pty)
         ecache'    = alterTM pty (\_ -> Just (ev,fl)) $
                      evc_cache ecache
 
-delCachedEvVar :: EvVar -> TcS ()
-delCachedEvVar ev
-  = do { eref   <- getTcSEvVarCache
+delCachedEvVar :: EvVar -> CtFlavor -> TcS ()
+delCachedEvVar ev _fl
+  = {-# SCC "delCachedEvVarOther" #-}
+    do { eref   <- getTcSEvVarCache
        ; ecache <- wrapTcS (TcM.readTcRef eref)
        ; wrapTcS $ TcM.writeTcRef eref (delFromCache ecache ev) }
 
@@ -1377,13 +1388,13 @@ pprEvVarCache tm = ppr (foldTM mk_pair tm [])
  where mk_pair (co,_) cos = (co, liftedCoercionKind co) : cos
 
 
-newGivenEqVar :: CtFlavor -> TcType -> TcType -> Coercion -> TcS EvVar
+newGivenEqVar :: CtFlavor -> TcType -> TcType -> Coercion -> TcS (CtFlavor,EvVar)
 -- Pre: fl is Given
 newGivenEqVar fl ty1 ty2 co 
   = do { ecv <- newEqVar fl ty1 ty2
        ; let v = evc_the_evvar ecv -- Will be a new EvVar by post of newEvVar
-       ; setEvBind v (EvCoercionBox co)
-       ; return v }
+       ; fl' <- setEvBind v (EvCoercionBox co) fl
+       ; return (fl',v) }
 
 newEqVar :: CtFlavor -> TcType -> TcType -> TcS EvVarCreated
 newEqVar fl ty1 ty2 
@@ -1447,6 +1458,7 @@ getInertEqs :: TcS (TyVarEnv (Ct,Coercion), InScopeSet)
 getInertEqs = do { inert <- getTcSInerts
                  ; return (inert_eqs inert, inert_eq_tvs inert) }
 
+{-- UNSAFE in the prsence of Solved flavors! Don't use! 
 rewriteFromInertEqs :: (TyVarEnv (Ct,Coercion), InScopeSet)
                     -- Precondition: Ct are CTyEqCans only!
                     -> CtFlavor 
@@ -1458,7 +1470,7 @@ rewriteFromInertEqs (subst,inscope) fl v
        ; if isReflCo co then return (v,True)
          else do { traceTcS "rewriteFromInertEqs" $
                    text "Original item =" <+> ppr v <+> dcolon <+> ppr (evVarPred v)
-                 ; delCachedEvVar v
+                 ; delCachedEvVar v fl
                  ; evc <- newEvVar fl (pSnd (liftedCoercionKind co))
                  ; let v' = evc_the_evvar evc
                  ; if isNewEvVar evc then 
@@ -1476,7 +1488,7 @@ rewriteFromInertEqs (subst,inscope) fl v
                               _ -> return ()
                           ; return (v',True) } -- As if rewriting never happened?
                  } } 
-
+--}
 
 -- See Note [LiftInertEqs]
 liftInertEqsTy :: (TyVarEnv (Ct,Coercion),InScopeSet)
diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs
index 68082d4156..76e02e6629 100644
--- a/compiler/typecheck/TcSimplify.lhs
+++ b/compiler/typecheck/TcSimplify.lhs
@@ -1046,7 +1046,11 @@ solveCTyFunEqs cts
       ; return (niFixTvSubst ni_subst, unsolved_can_cts) }
   where
     solve_one (cv,tv,ty) = do { setWantedTyBind tv ty
-                              ; setEqBind cv (mkReflCo ty) }
+                              ; _ <- setEqBind cv (mkReflCo ty) $
+                                       (Wanted $ panic "Met an already solved function equality!")
+                              ; return () -- Don't care about flavors etc this is
+                                          -- the last thing happening
+                              }
 
 ------------
 type FunEqBinds = (TvSubstEnv, [(CoVar, TcTyVar, TcType)])
diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs
index aaed359a10..17179fd2f1 100644
--- a/compiler/types/Coercion.lhs
+++ b/compiler/types/Coercion.lhs
@@ -22,6 +22,7 @@ module Coercion (
         -- ** Functions over coercions
         coVarKind,
         coercionType, coercionKind, coercionKinds, isReflCo, liftedCoercionKind,
+        isReflCo_maybe,
         mkCoercionType,
 
 	-- ** Constructing coercions