Flat constraint --> Simple constraint
[ghc.git] / compiler / typecheck / TcSMonad.hs
index 204a471..a0dda96 100644 (file)
@@ -26,18 +26,11 @@ module TcSMonad (
     XEvTerm(..),
     Freshness(..), freshGoals, isFresh,
 
-    StopOrContinue(..), continueWith, stopWith, andWhenContinue,
-
-    xCtEvidence,        -- Transform a CtEvidence during a step
-    rewriteEvidence,    -- Specialized version of xCtEvidence for coercions
-    rewriteEqEvidence,  -- Yet more specialised, for equality coercions
-    maybeSym,
-
     newTcEvBinds, newWantedEvVar, newWantedEvVarNC,
     setWantedTyBind, reportUnifications,
     setEvBind,
-    newEvVar, newGivenEvVar,
-    emitNewDerived, emitNewDerivedEq,
+    newEvVar, newGivenEvVar, newGivenEvVars,
+    newDerived, emitNewDerived,
     instDFunConstraints,
 
     getInstEnvs, getFamInstEnvs,                -- Getting the environments
@@ -80,7 +73,7 @@ module TcSMonad (
 
     TcLevel, isTouchableMetaTyVarTcS,
     isFilledMetaTyVar_maybe, isFilledMetaTyVar,
-    zonkTyVarsAndFV, zonkTcType, zonkTcTyVar, zonkFlats,
+    zonkTyVarsAndFV, zonkTcType, zonkTcTyVar, zonkSimples,
 
     -- References
     newTcRef, readTcRef, updTcRef,
@@ -113,7 +106,6 @@ import Kind
 import TcType
 import DynFlags
 import Type
-import CoAxiom(sfMatchFam)
 
 import TcEvidence
 import Class
@@ -134,17 +126,16 @@ import Util
 import Id
 import TcRnTypes
 
-import BasicTypes
 import Unique
 import UniqFM
 import Maybes ( orElse, firstJusts )
 
 import TrieMap
-import Control.Monad( ap, when, unless )
+import Control.Arrow ( first )
+import Control.Monad( ap, when, unless, MonadPlus(..) )
 import MonadUtils
 import Data.IORef
 import Data.List ( partition, foldl' )
-import Pair
 
 #ifdef DEBUG
 import Digraph
@@ -266,11 +257,11 @@ extendWorkListCt :: Ct -> WorkList -> WorkList
 -- Agnostic
 extendWorkListCt ct wl
  = case classifyPredType (ctPred ct) of
-     EqPred ty1 _
+     EqPred NomEq ty1 _
        | Just (tc,_) <- tcSplitTyConApp_maybe ty1
        , isTypeFamilyTyCon tc
        -> extendWorkListFunEq ct wl
-       | otherwise
+     EqPred {}
        -> extendWorkListEq ct wl
 
      _ -> extendWorkListNonEq ct wl
@@ -395,7 +386,7 @@ Type-family equations, of form (ev : F tys ~ ty), live in three places
 -- See Note [Detailed InertCans Invariants] for more
 data InertCans
   = IC { inert_eqs :: TyVarEnv EqualCtList
-              -- All CTyEqCans; index is the LHS tyvar
+              -- All CTyEqCans with NomEq; index is the LHS tyvar
 
        , inert_funeqs :: FunEqMap Ct
               -- All CFunEqCans; index is the whole family head type.
@@ -413,16 +404,18 @@ data InertCans
        }
 
 type EqualCtList = [Ct]
--- EqualCtList invariants:
---    * All are equalities
---    * All these equalities have the same LHS
---    * The list is never empty
---    * No element of the list can rewrite any other
---
--- From the fourth invariant it follows that the list is
---   - A single Given, or
---   - Multiple Wanteds, or
---   - Multiple Deriveds
+{-
+Note [EqualCtList invariants]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+    * All are equalities
+    * All these equalities have the same LHS
+    * The list is never empty
+    * No element of the list can rewrite any other
+
+ From the fourth invariant it follows that the list is
+   - A single Given, or
+   - Any number of Wanteds and/or Deriveds
+-}
 
 -- The Inert Set
 data InertSet
@@ -430,10 +423,11 @@ data InertSet
               -- Canonical Given, Wanted, Derived (no Solved)
               -- Sometimes called "the inert set"
 
-       , inert_flat_cache :: FunEqMap (TcCoercion, TcTyVar)
+       , inert_flat_cache :: FunEqMap (TcCoercion, TcType, CtFlavour)
               -- See Note [Type family equations]
-              -- If    F tys :-> (co, fsk),
-              -- then  co :: F tys ~ fsk
+              -- If    F tys :-> (co, ty, ev),
+              -- then  co :: F tys ~ ty
+              --
               -- 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
@@ -444,7 +438,6 @@ data InertSet
        , inert_solved_dicts   :: DictMap CtEvidence
               -- Of form ev :: C t1 .. tn
               -- Always the result of using a top-level instance declaration
-              -- See Note [Solved constraints]
               -- - Used to avoid creating a new EvVar when we have a new goal
               --   that we have solved in the past
               -- - Stored not necessarily as fully rewritten
@@ -471,11 +464,11 @@ instance Outputable InertSet where
 
 emptyInert :: InertSet
 emptyInert
-  = IS { inert_cans = IC { inert_eqs     = emptyVarEnv
-                         , inert_dicts   = emptyDicts
-                         , inert_funeqs  = emptyFunEqs
-                         , inert_irreds  = emptyCts
-                         , inert_insols  = emptyCts
+  = IS { inert_cans = IC { inert_eqs      = emptyVarEnv
+                         , inert_dicts    = emptyDicts
+                         , inert_funeqs   = emptyFunEqs
+                         , inert_irreds   = emptyCts
+                         , inert_insols   = emptyCts
                          }
        , inert_flat_cache    = emptyFunEqs
        , inert_solved_dicts  = emptyDictMap }
@@ -484,9 +477,12 @@ emptyInert
 addInertCan :: InertCans -> Ct -> InertCans
 -- Precondition: item /is/ canonical
 addInertCan ics item@(CTyEqCan {})
-  = ics { inert_eqs = extendVarEnv_C (\eqs _ -> item : eqs)
-                              (inert_eqs ics)
-                              (cc_tyvar item) [item] }
+  = ics { inert_eqs = add_eq (inert_eqs ics) item }
+  where
+    add_eq :: TyVarEnv EqualCtList -> Ct -> TyVarEnv EqualCtList
+    add_eq old_list it
+      = extendVarEnv_C (\old_eqs _new_eqs -> it : old_eqs)
+                       old_list (cc_tyvar it) [it]
 
 addInertCan ics item@(CFunEqCan { cc_fun = tc, cc_tyargs = tys })
   = ics { inert_funeqs = insertFunEq (inert_funeqs ics) tc tys item }
@@ -568,15 +564,15 @@ prepareInertsForImplications is@(IS { inert_cans = cans })
   = is { inert_cans       = getGivens cans
        , inert_flat_cache = emptyFunEqs }  -- See Note [Do not inherit the flat cache]
   where
-    getGivens (IC { inert_eqs    = eqs
-                  , inert_irreds = irreds
-                  , inert_funeqs = funeqs
-                  , inert_dicts  = dicts })
-      = IC { inert_eqs     = filterVarEnv  is_given_ecl eqs
-           , inert_funeqs  = filterFunEqs  isGivenCt funeqs
-           , inert_irreds  = Bag.filterBag isGivenCt irreds
-           , inert_dicts   = filterDicts   isGivenCt dicts
-           , inert_insols  = emptyCts }
+    getGivens (IC { inert_eqs      = eqs
+                  , inert_irreds   = irreds
+                  , inert_funeqs   = funeqs
+                  , inert_dicts    = dicts })
+      = IC { inert_eqs      = filterVarEnv  is_given_ecl eqs
+           , inert_funeqs   = filterFunEqs  isGivenCt funeqs
+           , inert_irreds   = Bag.filterBag isGivenCt irreds
+           , inert_dicts    = filterDicts   isGivenCt dicts
+           , inert_insols   = emptyCts }
 
     is_given_ecl :: EqualCtList -> Bool
     is_given_ecl (ct:rest) | isGivenCt ct = ASSERT( null rest ) True
@@ -616,8 +612,9 @@ them into Givens.  There can *be* deriving CFunEqCans; see Trac #8129.
 -}
 
 getInertEqs :: TcS (TyVarEnv EqualCtList)
-getInertEqs = do { inert <- getTcSInerts
-                 ; return (inert_eqs (inert_cans inert)) }
+getInertEqs
+  = do { inert <- getTcSInerts
+       ; return (inert_eqs (inert_cans inert)) }
 
 getUnsolvedInerts :: TcS ( Bag Implication
                          , Cts     -- Tyvar eqs: a ~ ty
@@ -625,16 +622,19 @@ getUnsolvedInerts :: TcS ( Bag Implication
                          , Cts     -- Insoluble
                          , Cts )   -- All others
 getUnsolvedInerts
- = do { IC { inert_eqs = tv_eqs, inert_funeqs = fun_eqs
+ = do { IC { inert_eqs    = tv_eqs
+           , inert_funeqs = fun_eqs
            , inert_irreds = irreds, inert_dicts = idicts
            , inert_insols = insols } <- getInertCans
 
-      ; let unsolved_tv_eqs  = foldVarEnv (\cts rest -> foldr add_if_unsolved rest cts)
+      ; let unsolved_tv_eqs   = foldVarEnv (\cts rest ->
+                                             foldr add_if_unsolved rest cts)
                                           emptyCts tv_eqs
-            unsolved_fun_eqs = foldFunEqs add_if_unsolved fun_eqs emptyCts
-            unsolved_irreds  = Bag.filterBag is_unsolved irreds
-            unsolved_dicts   = foldDicts add_if_unsolved idicts emptyCts
-            others = unsolved_irreds `unionBags` unsolved_dicts
+            unsolved_fun_eqs  = foldFunEqs add_if_unsolved fun_eqs emptyCts
+            unsolved_irreds   = Bag.filterBag is_unsolved irreds
+            unsolved_dicts    = foldDicts add_if_unsolved idicts emptyCts
+
+            others       = unsolved_irreds `unionBags` unsolved_dicts
 
       ; implics <- getWorkListImplics
 
@@ -729,6 +729,9 @@ are some wrinkles:
 
  * See Note [Let-bound skolems] for another wrinkle
 
+ * We do *not* need to worry about representational equalities, because
+   these do not affect the ability to float constraints.
+
 Note [Let-bound skolems]
 ~~~~~~~~~~~~~~~~~~~~~~~~
 If   * the inert set contains a canonical Given CTyEqCan (a ~ ty)
@@ -775,8 +778,8 @@ removeInertCt is ct =
     CFunEqCan { cc_fun  = tf,  cc_tyargs = tys } ->
       is { inert_funeqs = delFunEq (inert_funeqs is) tf tys }
 
-    CTyEqCan  { cc_tyvar = x,  cc_rhs    = ty  } ->
-      is { inert_eqs = delTyEq (inert_eqs is) x ty }
+    CTyEqCan  { cc_tyvar = x,  cc_rhs    = ty } ->
+      is { inert_eqs    = delTyEq (inert_eqs is) x ty }
 
     CIrredEvCan {}   -> panic "removeInertCt: CIrredEvCan"
     CNonCanonical {} -> panic "removeInertCt: CNonCanonical"
@@ -790,16 +793,19 @@ checkAllSolved
  = do { is <- getTcSInerts
 
       ; let icans = inert_cans is
-            unsolved_irreds = Bag.anyBag isWantedCt (inert_irreds icans)
-            unsolved_dicts  = foldDicts ((||)  . isWantedCt) (inert_dicts icans)  False
-            unsolved_funeqs = foldFunEqs ((||) . isWantedCt) (inert_funeqs icans) False
-            unsolved_eqs    = foldVarEnv ((||) . any isWantedCt) False (inert_eqs icans)
+            unsolved_irreds  = Bag.anyBag isWantedCt (inert_irreds icans)
+            unsolved_dicts   = foldDicts  ((||)  . isWantedCt)
+                                          (inert_dicts icans)  False
+            unsolved_funeqs  = foldFunEqs ((||) . isWantedCt)
+                                          (inert_funeqs icans) False
+            unsolved_eqs     = foldVarEnv ((||) . any isWantedCt) False
+                                          (inert_eqs icans)
 
       ; return (not (unsolved_eqs || unsolved_irreds
                      || unsolved_dicts || unsolved_funeqs
                      || not (isEmptyBag (inert_insols icans)))) }
 
-lookupFlatCache :: TyCon -> [Type] -> TcS (Maybe (TcCoercion, TcTyVar))
+lookupFlatCache :: TyCon -> [Type] -> TcS (Maybe (TcCoercion, TcType, CtFlavour))
 lookupFlatCache fam_tc tys
   = do { IS { inert_flat_cache = flat_cache
             , inert_cans = IC { inert_funeqs = inert_funeqs } } <- getTcSInerts
@@ -809,7 +815,7 @@ lookupFlatCache fam_tc tys
     lookup_inerts inert_funeqs
       | Just (CFunEqCan { cc_ev = ctev, cc_fsk = fsk })
            <- findFunEqs inert_funeqs fam_tc tys
-      = Just (ctEvCoercion ctev, fsk)
+      = Just (ctEvCoercion ctev, mkTyVarTy fsk, ctEvFlavour ctev)
       | otherwise = Nothing
 
     lookup_flats flat_cache = findFunEq flat_cache fam_tc tys
@@ -818,16 +824,12 @@ lookupFlatCache fam_tc tys
 lookupInInerts :: CtLoc -> TcPredType -> TcS (Maybe CtEvidence)
 -- Is this exact predicate type cached in the solved or canonicals of the InertSet?
 lookupInInerts loc pty
+  | ClassPred cls tys <- classifyPredType pty
   = do { inerts <- getTcSInerts
-       ; return $ case (classifyPredType pty) of
-           ClassPred cls tys
-              | Just ev <- lookupSolvedDict inerts loc cls tys
-              -> Just ev
-              | otherwise
-              -> lookupInertDict (inert_cans inerts) loc cls tys
-
-           _other -> Nothing -- NB: No caching for equalities, IPs, holes, or errors
-      }
+       ; return (lookupSolvedDict inerts loc cls tys `mplus`
+                 lookupInertDict (inert_cans inerts) loc cls tys) }
+  | otherwise -- NB: No caching for equalities, IPs, holes, or errors
+  = return Nothing
 
 lookupInertDict :: InertCans -> CtLoc -> Class -> [Type] -> Maybe CtEvidence
 lookupInertDict (IC { inert_dicts = dicts }) loc cls tys
@@ -854,8 +856,8 @@ lookupSolvedDict (IS { inert_solved_dicts = solved }) loc cls tys
 
 type TyEqMap a = TyVarEnv a
 
-findTyEqs :: TyEqMap EqualCtList -> TyVar -> EqualCtList
-findTyEqs m tv = lookupVarEnv m tv `orElse` []
+findTyEqs :: InertCans -> TyVar -> EqualCtList
+findTyEqs icans tv = lookupVarEnv (inert_eqs icans) tv `orElse` []
 
 delTyEq :: TyEqMap EqualCtList -> TcTyVar -> TcType -> TyEqMap EqualCtList
 delTyEq m tv t = modifyVarEnv (filter (not . isThisOne)) m tv
@@ -1283,7 +1285,7 @@ dictionaries from the thing_inside.
 Consider
    Eq [a]
    forall b. empty =>  Eq [a]
-We solve the flat (Eq [a]), under nestTcS, and then turn our attention to
+We solve the simple (Eq [a]), under nestTcS, and then turn our attention to
 the implications.  It's definitely fine to use the solved dictionaries on
 the inner implications, and it can make a signficant performance difference
 if you do so.
@@ -1463,8 +1465,8 @@ zonkTcType ty = wrapTcS (TcM.zonkTcType ty)
 zonkTcTyVar :: TcTyVar -> TcS TcType
 zonkTcTyVar tv = wrapTcS (TcM.zonkTcTyVar tv)
 
-zonkFlats :: Cts -> TcS Cts
-zonkFlats cts = wrapTcS (TcM.zonkFlats cts)
+zonkSimples :: Cts -> TcS Cts
+zonkSimples cts = wrapTcS (TcM.zonkSimples cts)
 
 {-
 Note [Do not add duplicate derived insolubles]
@@ -1496,11 +1498,11 @@ Example of (b): assume a top-level class and instance declaration:
 
 Assume we have started with an implication:
 
-  forall c. Eq c => { wc_flat = D [c] c [W] }
+  forall c. Eq c => { wc_simple = D [c] c [W] }
 
 which we have simplified to:
 
-  forall c. Eq c => { wc_flat = D [c] c [W]
+  forall c. Eq c => { wc_simple = D [c] c [W]
                     , wc_insols = (c ~ [c]) [D] }
 
 For some reason, e.g. because we floated an equality somewhere else,
@@ -1513,16 +1515,16 @@ constraints the second time:
 
 which will result in two Deriveds to end up in the insoluble set:
 
-  wc_flat   = D [c] c [W]
+  wc_simple   = D [c] c [W]
   wc_insols = (c ~ [c]) [D], (c ~ [c]) [D]
 -}
 
 -- Flatten skolems
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-newFlattenSkolem :: CtEvidence -> TcType         -- F xis
+newFlattenSkolem :: CtFlavour -> CtLoc
+                 -> TcType         -- F xis
                  -> TcS (CtEvidence, TcTyVar)    -- [W] x:: F xis ~ fsk
-newFlattenSkolem ctxt_ev fam_ty
-  | isGiven ctxt_ev   -- Make a given
+newFlattenSkolem Given loc fam_ty
   =  do { fsk <- wrapTcS $
                  do { uniq <- TcM.newUnique
                     ; let name = TcM.mkTcTyVarName uniq (fsLit "fsk")
@@ -1532,7 +1534,7 @@ newFlattenSkolem ctxt_ev fam_ty
                            , ctev_loc  = loc }
         ; return (ev, fsk) }
 
-  | otherwise        -- Make a wanted
+newFlattenSkolem _ loc fam_ty  -- Make a wanted
   = do { fuv <- wrapTcS $
                  do { uniq <- TcM.newUnique
                     ; ref  <- TcM.newMutVar Flexi
@@ -1543,15 +1545,13 @@ newFlattenSkolem ctxt_ev fam_ty
                     ; return (mkTcTyVar name (typeKind fam_ty) details) }
        ; ev <- newWantedEvVarNC loc (mkTcEqPred fam_ty (mkTyVarTy fuv))
        ; return (ev, fuv) }
-  where
-    loc = ctEvLoc ctxt_ev
 
-extendFlatCache :: TyCon -> [Type] -> (TcCoercion, TcTyVar) -> TcS ()
-extendFlatCache tc xi_args (co, fsk)
+extendFlatCache :: TyCon -> [Type] -> (TcCoercion, TcType, CtFlavour) -> TcS ()
+extendFlatCache tc xi_args stuff
   = do { dflags <- getDynFlags
        ; when (gopt Opt_FlatCache dflags) $
          updInertTcS $ \ is@(IS { inert_flat_cache = fc }) ->
-            is { inert_flat_cache = insertFunEq fc tc xi_args (co, fsk) } }
+            is { inert_flat_cache = insertFunEq fc tc xi_args stuff } }
 
 -- Instantiations
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1644,98 +1644,27 @@ newGivenEvVar :: CtLoc -> (TcPredType, EvTerm) -> TcS CtEvidence
 -- Make a new variable of the given PredType,
 -- immediately bind it to the given term
 -- and return its CtEvidence
+-- Precondition: this is not a kind equality
+--               See Note [Do not create Given kind equalities]
 newGivenEvVar loc (pred, rhs)
-  = do { new_ev <- newEvVar pred
+  = ASSERT2( not (isKindEquality pred), ppr pred $$ pprCtOrigin (ctLocOrigin loc) )
+    do { new_ev <- newEvVar pred
        ; setEvBind new_ev rhs
        ; return (CtGiven { ctev_pred = pred, ctev_evtm = EvId new_ev, ctev_loc = loc }) }
 
-newWantedEvVarNC :: CtLoc -> TcPredType -> TcS CtEvidence
--- Don't look up in the solved/inerts; we know it's not there
-newWantedEvVarNC loc pty
-  = do { new_ev <- newEvVar pty
-       ; return (CtWanted { ctev_pred = pty, ctev_evar = new_ev, ctev_loc = loc })}
-
-newWantedEvVar :: CtLoc -> TcPredType -> TcS (CtEvidence, Freshness)
-newWantedEvVar loc pty
-  = do { mb_ct <- lookupInInerts loc pty
-       ; case mb_ct of
-            Just ctev | not (isDerived ctev)
-                      -> do { traceTcS "newWantedEvVar/cache hit" $ ppr ctev
-                            ; return (ctev, Cached) }
-            _ -> do { ctev <- newWantedEvVarNC loc pty
-                    ; traceTcS "newWantedEvVar/cache miss" $ ppr ctev
-                    ; return (ctev, Fresh) } }
-
-emitNewDerivedEq :: CtLoc -> Pair TcType -> TcS ()
--- Create new Derived and put it in the work list
-emitNewDerivedEq loc (Pair ty1 ty2)
-  | ty1 `tcEqType` ty2   -- Quite common!
-  = return ()
-  | otherwise
-  = emitNewDerived loc (mkTcEqPred ty1 ty2)
-
-emitNewDerived :: CtLoc -> TcPredType -> TcS ()
--- Create new Derived and put it in the work list
-emitNewDerived loc pred
-  = do { mb_ev <- newDerived loc pred
-       ; case mb_ev of
-           Nothing -> return ()
-           Just ev -> do { traceTcS "Emitting [D]" (ppr ev)
-                         ; updWorkListTcS (extendWorkListCt (mkNonCanonical ev)) } }
-
-newDerived :: CtLoc -> TcPredType -> TcS (Maybe CtEvidence)
--- Returns Nothing    if cached,
---         Just pred  if not cached
-newDerived loc pred
-  = do { mb_ct <- lookupInInerts loc pred
-       ; return (case mb_ct of
-                    Just {} -> Nothing
-                    Nothing -> Just (CtDerived { ctev_pred = pred, ctev_loc = loc })) }
+newGivenEvVars :: CtLoc -> [(TcPredType, EvTerm)] -> TcS [CtEvidence]
+-- Like newGivenEvVar, but automatically discard kind equalities
+-- See Note [Do not create Given kind equalities]
+newGivenEvVars loc pts = mapM (newGivenEvVar loc) (filterOut (isKindEquality . fst) pts)
 
-instDFunConstraints :: CtLoc -> TcThetaType -> TcS [(CtEvidence, Freshness)]
-instDFunConstraints loc = mapM (newWantedEvVar loc)
+isKindEquality :: TcPredType -> Bool
+-- See Note [Do not create Given kind equalities]
+isKindEquality pred = case classifyPredType pred of
+                        EqPred _ t1 _ -> isKind t1
+                        _             -> False
 
-{-
-Note [xCtEvidence]
-~~~~~~~~~~~~~~~~~~
-A call might look like this:
-
-    xCtEvidence ev evidence-transformer
-
-  ev is Given   => use ev_decomp to create new Givens for ev_preds,
-                   and return them
-
-  ev is Wanted  => create new wanteds for ev_preds,
-                   use ev_comp to bind ev,
-                   return fresh wanteds (ie ones not cached in inert_cans or solved)
-
-  ev is Derived => create new deriveds for ev_preds
-                      (unless cached in inert_cans or solved)
-
-Note: The [CtEvidence] returned is a subset of the subgoal-preds passed in
-      Ones that are already cached are not returned
-
-Example
-    ev : Tree a b ~ Tree c d
-    xCtEvidence ev [a~c, b~d] (XEvTerm { ev_comp = \[c1 c2]. <Tree> c1 c2
-                                       , ev_decomp = \c. [nth 1 c, nth 2 c] })
-              (\fresh-goals.  stuff)
-
-Note [Bind new Givens immediately]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-For Givens we make new EvVars and bind them immediately. We don't worry
-about caching, but we don't expect complicated calculations among Givens.
-It is important to bind each given:
-      class (a~b) => C a b where ....
-      f :: C a b => ....
-Then in f's Givens we have g:(C a b) and the superclass sc(g,0):a~b.
-But that superclass selector can't (yet) appear in a coercion
-(see evTermCoercion), so the easy thing is to bind it to an Id.
-
-See Note [Coercion evidence terms] in TcEvidence.
-
-Note [Do not create Given kind equalities]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{- Note [Do not create Given kind equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We do not want to create a Given kind equality like
 
    [G]  kv ~ k   -- kv is a skolem kind variable
@@ -1769,229 +1698,52 @@ as an Irreducible (see Note [Equalities with incompatible kinds] in
 TcCanonical), and will do no harm.
 -}
 
-xCtEvidence :: CtEvidence            -- Original evidence
-            -> XEvTerm               -- Instructions about how to manipulate evidence
-            -> TcS ()
-
-xCtEvidence (CtWanted { ctev_evar = evar, ctev_loc = loc })
-            (XEvTerm { ev_preds = ptys, ev_comp = comp_fn })
-  = do { new_evars <- mapM (newWantedEvVar loc) ptys
-       ; setEvBind evar (comp_fn (map (ctEvTerm . fst) new_evars))
-       ; emitWorkNC (freshGoals new_evars) }
-         -- Note the "NC": these are fresh goals, not necessarily canonical
-
-xCtEvidence (CtGiven { ctev_evtm = tm, ctev_loc = loc })
-            (XEvTerm { ev_preds = ptys, ev_decomp = decomp_fn })
-  = ASSERT( equalLength ptys (decomp_fn tm) )
-    do { given_evs <- mapM (newGivenEvVar loc) $    -- See Note [Bind new Givens immediately]
-                      filterOut bad_given_pred (ptys `zip` decomp_fn tm)
-       ; emitWorkNC given_evs }
-  where
-    -- See Note [Do not create Given kind equalities]
-    bad_given_pred (pred_ty, _)
-      | EqPred t1 _ <- classifyPredType pred_ty
-      = isKind t1
-      | otherwise
-      = False
-
-xCtEvidence (CtDerived { ctev_loc = loc })
-            (XEvTerm { ev_preds = ptys })
-  = mapM_ (emitNewDerived loc) ptys
-
------------------------------
-data StopOrContinue a
-  = ContinueWith a    -- The constraint was not solved, although it may have
-                      --   been rewritten
-
-  | Stop CtEvidence   -- The (rewritten) constraint was solved
-         SDoc         -- Tells how it was solved
-                      -- Any new sub-goals have been put on the work list
-
-instance Functor StopOrContinue where
-  fmap f (ContinueWith x) = ContinueWith (f x)
-  fmap _ (Stop ev s)      = Stop ev s
-
-instance Outputable a => Outputable (StopOrContinue a) where
-  ppr (Stop ev s)      = ptext (sLit "Stop") <> parens s <+> ppr ev
-  ppr (ContinueWith w) = ptext (sLit "ContinueWith") <+> ppr w
-
-continueWith :: a -> TcS (StopOrContinue a)
-continueWith = return . ContinueWith
-
-stopWith :: CtEvidence -> String -> TcS (StopOrContinue a)
-stopWith ev s = return (Stop ev (text s))
-
-andWhenContinue :: TcS (StopOrContinue a)
-                -> (a -> TcS (StopOrContinue b))
-                -> TcS (StopOrContinue b)
-andWhenContinue tcs1 tcs2
-  = do { r <- tcs1
-       ; case r of
-           Stop ev s       -> return (Stop ev s)
-           ContinueWith ct -> tcs2 ct }
-
-rewriteEvidence :: CtEvidence   -- old evidence
-                -> TcPredType   -- new predicate
-                -> TcCoercion   -- Of type :: new predicate ~ <type of old evidence>
-                -> TcS (StopOrContinue CtEvidence)
--- Returns Just new_ev iff either (i)  'co' is reflexivity
---                             or (ii) 'co' is not reflexivity, and 'new_pred' not cached
--- In either case, there is nothing new to do with new_ev
-{-
-     rewriteEvidence old_ev new_pred co
-Main purpose: create new evidence for new_pred;
-              unless new_pred is cached already
-* Returns a new_ev : new_pred, with same wanted/given/derived flag as old_ev
-* If old_ev was wanted, create a binding for old_ev, in terms of new_ev
-* If old_ev was given, AND not cached, create a binding for new_ev, in terms of old_ev
-* Returns Nothing if new_ev is already cached
-
-        Old evidence    New predicate is               Return new evidence
-        flavour                                        of same flavor
-        -------------------------------------------------------------------
-        Wanted          Already solved or in inert     Nothing
-        or Derived      Not                            Just new_evidence
-
-        Given           Already in inert               Nothing
-                        Not                            Just new_evidence
-
-Note [Rewriting with Refl]
-~~~~~~~~~~~~~~~~~~~~~~~~~~
-If the coercion is just reflexivity then you may re-use the same
-variable.  But be careful!  Although the coercion is Refl, new_pred
-may reflect the result of unification alpha := ty, so new_pred might
-not _look_ the same as old_pred, and it's vital to proceed from now on
-using new_pred.
-
-The flattener preserves type synonyms, so they should appear in new_pred
-as well as in old_pred; that is important for good error messages.
- -}
-
-
-rewriteEvidence old_ev@(CtDerived { ctev_loc = loc }) new_pred _co
-  = -- If derived, don't even look at the coercion.
-    -- This is very important, DO NOT re-order the equations for
-    -- rewriteEvidence to put the isTcReflCo test first!
-    -- Why?  Because for *Derived* constraints, c, the coercion, which
-    -- was produced by flattening, may contain suspended calls to
-    -- (ctEvTerm c), which fails for Derived constraints.
-    -- (Getting this wrong caused Trac #7384.)
-    do { mb_ev <- newDerived loc new_pred
-       ; case mb_ev of
-           Just new_ev -> continueWith new_ev
-           Nothing     -> stopWith old_ev "Cached derived" }
+newWantedEvVarNC :: CtLoc -> TcPredType -> TcS CtEvidence
+-- Don't look up in the solved/inerts; we know it's not there
+newWantedEvVarNC loc pty
+  = do { new_ev <- newEvVar pty
+       ; return (CtWanted { ctev_pred = pty, ctev_evar = new_ev, ctev_loc = loc })}
 
-rewriteEvidence old_ev new_pred co
-  | isTcReflCo co -- See Note [Rewriting with Refl]
-  = return (ContinueWith (old_ev { ctev_pred = new_pred }))
+newWantedEvVar :: CtLoc -> TcPredType -> TcS (CtEvidence, Freshness)
+-- For anything except ClassPred, this is the same as newWantedEvVarNC
+newWantedEvVar loc pty
+  = do { mb_ct <- lookupInInerts loc pty
+       ; case mb_ct of
+            Just ctev | not (isDerived ctev)
+                      -> do { traceTcS "newWantedEvVar/cache hit" $ ppr ctev
+                            ; return (ctev, Cached) }
+            _ -> do { ctev <- newWantedEvVarNC loc pty
+                    ; traceTcS "newWantedEvVar/cache miss" $ ppr ctev
+                    ; return (ctev, Fresh) } }
 
-rewriteEvidence (CtGiven { ctev_evtm = old_tm , ctev_loc = loc }) new_pred co
-  = do { new_ev <- newGivenEvVar loc (new_pred, new_tm)  -- See Note [Bind new Givens immediately]
-       ; return (ContinueWith new_ev) }
-  where
-    new_tm = mkEvCast old_tm (mkTcSubCo (mkTcSymCo co))  -- mkEvCast optimises ReflCo
-
-rewriteEvidence ev@(CtWanted { ctev_evar = evar, ctev_loc = loc }) new_pred co
-  = do { (new_ev, freshness) <- newWantedEvVar loc new_pred
-       ; MASSERT( tcCoercionRole co == Nominal )
-       ; setEvBind evar (mkEvCast (ctEvTerm new_ev) (mkTcSubCo co))
-       ; case freshness of
-            Fresh  -> continueWith new_ev
-            Cached -> stopWith ev "Cached wanted" }
-
-
-rewriteEqEvidence :: CtEvidence         -- Old evidence :: olhs ~ orhs (not swapped)
-                                        --              or orhs ~ olhs (swapped)
-                  -> SwapFlag
-                  -> TcType -> TcType   -- New predicate  nlhs ~ nrhs
-                                        -- Should be zonked, because we use typeKind on nlhs/nrhs
-                  -> TcCoercion         -- lhs_co, of type :: nlhs ~ olhs
-                  -> TcCoercion         -- rhs_co, of type :: nrhs ~ orhs
-                  -> TcS (StopOrContinue CtEvidence)  -- Of type nlhs ~ nrhs
--- For (rewriteEqEvidence (Given g olhs orhs) False nlhs nrhs lhs_co rhs_co)
--- we generate
--- If not swapped
---      g1 : nlhs ~ nrhs = lhs_co ; g ; sym rhs_co
--- If 'swapped'
---      g1 : nlhs ~ nrhs = lhs_co ; Sym g ; sym rhs_co
---
--- For (Wanted w) we do the dual thing.
--- New  w1 : nlhs ~ nrhs
--- If not swapped
---      w : olhs ~ orhs = sym lhs_co ; w1 ; rhs_co
--- If swapped
---      w : orhs ~ olhs = sym rhs_co ; sym w1 ; lhs_co
---
--- It's all a form of rewwriteEvidence, specialised for equalities
-rewriteEqEvidence old_ev swapped nlhs nrhs lhs_co rhs_co
-  | CtDerived { ctev_loc = loc } <- old_ev
-  = do { mb <- newDerived loc (mkTcEqPred nlhs nrhs)
-       ; case mb of
-           Just new_ev -> continueWith new_ev
-           Nothing     -> stopWith old_ev "Cached derived" }
-
-  | NotSwapped <- swapped
-  , isTcReflCo lhs_co      -- See Note [Rewriting with Refl]
-  , isTcReflCo rhs_co
-  = return (ContinueWith (old_ev { ctev_pred = new_pred }))
-
-  | CtGiven { ctev_evtm = old_tm , ctev_loc = loc } <- old_ev
-  = do { let new_tm = EvCoercion (lhs_co
-                                  `mkTcTransCo` maybeSym swapped (evTermCoercion old_tm)
-                                  `mkTcTransCo` mkTcSymCo rhs_co)
-       ; new_ev <- newGivenEvVar loc (new_pred, new_tm)  -- See Note [Bind new Givens immediately]
-       ; return (ContinueWith new_ev) }
-
-  | CtWanted { ctev_evar = evar, ctev_loc = loc } <- old_ev
-  = do { new_evar <- newWantedEvVarNC loc new_pred
-                     -- Not much point in seeking exact-match equality evidence
-       ; let co = maybeSym swapped $
-                  mkTcSymCo lhs_co
-                  `mkTcTransCo` ctEvCoercion new_evar
-                  `mkTcTransCo` rhs_co
-       ; setEvBind evar (EvCoercion co)
-       ; traceTcS "rewriteEqEvidence" (vcat [ppr old_ev, ppr nlhs, ppr nrhs, ppr co])
-       ; return (ContinueWith new_evar) }
+emitNewDerived :: CtLoc -> TcPredType -> TcS ()
+-- Create new Derived and put it in the work list
+emitNewDerived loc pred
+  = do { mb_ev <- newDerived loc pred
+       ; case mb_ev of
+           Nothing -> return ()
+           Just ev -> do { traceTcS "Emitting [D]" (ppr ev)
+                         ; updWorkListTcS (extendWorkListCt (mkNonCanonical ev)) } }
 
-  | otherwise
-  = panic "rewriteEvidence"
-  where
-    new_pred = mkTcEqPred nlhs nrhs
+newDerived :: CtLoc -> TcPredType -> TcS (Maybe CtEvidence)
+-- Returns Nothing    if cached,
+--         Just pred  if not cached
+newDerived loc pred
+  = do { mb_ct <- lookupInInerts loc pred
+       ; return (case mb_ct of
+                    Just {} -> Nothing
+                    Nothing -> Just (CtDerived { ctev_pred = pred, ctev_loc = loc })) }
+
+instDFunConstraints :: CtLoc -> TcThetaType -> TcS [(CtEvidence, Freshness)]
+instDFunConstraints loc = mapM (newWantedEvVar loc)
 
-maybeSym :: SwapFlag -> TcCoercion -> TcCoercion
-maybeSym IsSwapped  co = mkTcSymCo co
-maybeSym NotSwapped co = co
 
 matchFam :: TyCon -> [Type] -> TcS (Maybe (TcCoercion, TcType))
 -- Given (F tys) return (ty, co), where co :: F tys ~ ty
 matchFam tycon args
-  | isOpenTypeFamilyTyCon tycon
   = do { fam_envs <- getFamInstEnvs
-       ; let mb_match = tcLookupFamInst fam_envs tycon args
-       ; traceTcS "lookupFamInst" $
-                  vcat [ ppr tycon <+> ppr args
-                       , pprTvBndrs (varSetElems (tyVarsOfTypes args))
-                       , ppr mb_match ]
-       ; case mb_match of
-           Nothing -> return Nothing
-           Just (FamInstMatch { fim_instance = famInst
-                              , fim_tys      = inst_tys })
-             -> let co = mkTcUnbranchedAxInstCo Nominal (famInstAxiom famInst) inst_tys
-                    ty = pSnd $ tcCoercionKind co
-                in return $ Just (co, ty) }
-
-  | Just ax <- isClosedSynFamilyTyCon_maybe tycon
-  , Just (ind, inst_tys) <- chooseBranch ax args
-  = let co = mkTcAxInstCo Nominal ax ind inst_tys
-        ty = pSnd (tcCoercionKind co)
-    in return $ Just (co, ty)
-
-  | Just ops <- isBuiltInSynFamTyCon_maybe tycon =
-    return $ do (r,ts,ty) <- sfMatchFam ops args
-                return (mkTcAxiomRuleCo r ts [], ty)
-
-  | otherwise
-  = return Nothing
+       ; return $ fmap (first TcCoercion) $
+         reduceTyFamApp_maybe fam_envs Nominal tycon args }
 
 {-
 Note [Residual implications]
@@ -2034,9 +1786,9 @@ deferTcSForAllEq role loc (tvs1,body1) (tvs2,body2)
                                new_ct = mkNonCanonical ctev
                                new_co = ctEvCoercion ctev
                                new_tclvl = pushTcLevel (tcl_tclvl env)
-                         ; let wc = WC { wc_flat  = singleCt new_ct
-                                       , wc_impl  = emptyBag
-                                       , wc_insol = emptyCts }
+                         ; let wc = WC { wc_simple = singleCt new_ct
+                                       , wc_impl   = emptyBag
+                                       , wc_insol  = emptyCts }
                                imp = Implic { ic_tclvl  = new_tclvl
                                             , ic_skols  = skol_tvs
                                             , ic_no_eqs = True
@@ -2050,3 +1802,4 @@ deferTcSForAllEq role loc (tvs1,body1) (tvs2,body2)
                          ; return (TcLetCo ev_binds new_co) }
 
         ; return $ EvCoercion (foldr mkTcForAllCo coe_inside skol_tvs) }
+