Add valid refinement substitution suggestions for typed holes
[ghc.git] / compiler / typecheck / TcEvidence.hs
index e08d0d5..0930d7a 100644 (file)
@@ -6,61 +6,75 @@ module TcEvidence (
 
   -- HsWrapper
   HsWrapper(..),
-  (<.>), mkWpTyApps, mkWpEvApps, mkWpEvVarApps, mkWpTyLams, mkWpLams, mkWpLet, mkWpCast,
-  mkWpFun, idHsWrapper, isIdHsWrapper, pprHsWrapper,
+  (<.>), mkWpTyApps, mkWpEvApps, mkWpEvVarApps, mkWpTyLams,
+  mkWpLams, mkWpLet, mkWpCastN, mkWpCastR, collectHsWrapBinders,
+  mkWpFun, mkWpFuns, idHsWrapper, isIdHsWrapper, pprHsWrapper,
 
   -- Evidence bindings
   TcEvBinds(..), EvBindsVar(..),
   EvBindMap(..), emptyEvBindMap, extendEvBinds,
-                 lookupEvBind, evBindMapBinds, foldEvBindMap,
+  lookupEvBind, evBindMapBinds, foldEvBindMap, filterEvBindMap,
+  isEmptyEvBindMap,
   EvBind(..), emptyTcEvBinds, isEmptyTcEvBinds, mkGivenEvBind, mkWantedEvBind,
-  EvTerm(..), mkEvCast, evVarsOfTerm, mkEvScSelectors,
-  EvLit(..), evTermCoercion,
+  sccEvBinds, evBindVar,
+
+  -- EvTerm (already a CoreExpr)
+  EvTerm(..), EvExpr,
+  evId, evCoercion, evCast, evDFunApp,  evSelector,
+  mkEvCast, evVarsOfTerm, mkEvScSelectors, evTypeable, findNeededEvVars,
+
+  evTermCoercion,
   EvCallStack(..),
   EvTypeable(..),
 
   -- TcCoercion
-  TcCoercion(..), TcCoercionR, TcCoercionN,
-  LeftOrRight(..), pickLR,
+  TcCoercion, TcCoercionR, TcCoercionN, TcCoercionP, CoercionHole,
+  Role(..), LeftOrRight(..), pickLR,
   mkTcReflCo, mkTcNomReflCo, mkTcRepReflCo,
-  mkTcTyConAppCo, mkTcAppCo, mkTcAppCos, mkTcFunCo,
+  mkTcTyConAppCo, mkTcAppCo, mkTcFunCo,
   mkTcAxInstCo, mkTcUnbranchedAxInstCo, mkTcForAllCo, mkTcForAllCos,
   mkTcSymCo, mkTcTransCo, mkTcNthCo, mkTcLRCo, mkTcSubCo, maybeTcSubCo,
-  tcDowngradeRole, mkTcTransAppCo,
-  mkTcAxiomRuleCo, mkTcPhantomCo,
-  tcCoercionKind, coVarsOfTcCo, isEqVar, mkTcCoVarCo,
-  isTcReflCo, getTcCoVar_maybe,
-  tcCoercionRole, eqVarRole,
+  tcDowngradeRole,
+  mkTcAxiomRuleCo, mkTcCoherenceLeftCo, mkTcCoherenceRightCo, mkTcPhantomCo,
+  mkTcKindCo,
+  tcCoercionKind, coVarsOfTcCo,
+  mkTcCoVarCo,
+  isTcReflCo, isTcReflexiveCo,
+  tcCoercionRole,
   unwrapIP, wrapIP
   ) where
 #include "HsVersions.h"
 
+import GhcPrelude
+
 import Var
+import CoAxiom
 import Coercion
 import PprCore ()   -- Instance OutputableBndr TyVar
-import TypeRep      -- Knows type representation
 import TcType
 import Type
 import TyCon
 import Class( Class )
-import CoAxiom
 import PrelNames
+import DynFlags   ( gopt, GeneralFlag(Opt_PrintTypecheckerElaboration) )
 import VarEnv
 import VarSet
 import Name
+import Pair
+
+import CoreSyn
+import Class ( classSCSelId )
+import Id ( isEvVar )
+import CoreFVs ( exprSomeFreeVars )
 
 import Util
 import Bag
-import Pair
-#if __GLASGOW_HASKELL__ < 709
-import Control.Applicative
-import Data.Traversable (traverse, sequenceA)
-#endif
+import Digraph
 import qualified Data.Data as Data
 import Outputable
-import FastString
 import SrcLoc
 import Data.IORef( IORef )
+import UniqSet
 
 {-
 Note [TcCoercions]
@@ -70,484 +84,86 @@ Coercions have free variables of type (a ~# b): we call these
 CoVars. However, the type checker passes around equality evidence
 (boxed up) at type (a ~ b).
 
-An TcCoercion is simply a Coercion whose free variables have the
-boxed type (a ~ b). After we are done with typechecking the
-desugarer finds the free variables, unboxes them, and creates a
-resulting real Coercion with kosher free variables.
-
-We can use most of the Coercion "smart constructors" to build TcCoercions.
-However, mkCoVarCo will not work! The equivalent is mkTcCoVarCo.
-
-The data type is similar to Coercion.Coercion, with the following
-differences
-  * Most important, TcLetCo adds let-bindings for coercions.
-    This is what lets us unify two for-all types and generate
-    equality constraints underneath
-
-  * The kind of a TcCoercion is  t1 ~  t2  (resp. Coercible t1 t2)
-             of a Coercion   is  t1 ~# t2  (resp. t1 ~#R t2)
-
-  * UnsafeCo aren't required, but we do have TcPhantomCo
-
-  * Representation invariants are weaker:
-     - we are allowed to have type synonyms in TcTyConAppCo
-     - the first arg of a TcAppCo can be a TcTyConAppCo
-     - TcSubCo is not applied as deep as done with mkSubCo
-    Reason: they'll get established when we desugar to Coercion
-
-  * TcAxiomInstCo has a [TcCoercion] parameter, and not a [Type] parameter.
-    This differs from the formalism, but corresponds to AxiomInstCo (see
-    [Coercion axioms applied to coercions]).
-
-Note [mkTcTransAppCo]
-~~~~~~~~~~~~~~~~~~~~~
-Suppose we have
-
-  co1 :: a ~R Maybe
-  co2 :: b ~R Int
-
-and we want
-
-  co3 :: a b ~R Maybe Int
-
-This seems sensible enough. But, we can't let (co3 = co1 co2), because
-that's ill-roled! Note that mkTcAppCo requires a *nominal* second coercion.
-
-The way around this is to use transitivity:
-
-  co3 = (co1 <b>_N) ; (Maybe co2) :: a b ~R Maybe Int
-
-Or, it's possible everything is the other way around:
-
-  co1' :: Maybe ~R a
-  co2' :: Int   ~R b
-
-and we want
-
-  co3' :: Maybe Int ~R a b
+An TcCoercion is simply a Coercion whose free variables have may be either
+boxed or unboxed. After we are done with typechecking the desugarer finds the
+boxed free variables, unboxes them, and creates a resulting real Coercion with
+kosher free variables.
 
-then
-
-  co3' = (Maybe co2') ; (co1' <b>_N)
-
-This is exactly what `mkTcTransAppCo` builds for us. Information for all
-the arguments tends to be to hand at call sites, so it's quicker than
-using, say, tcCoercionKind.
 -}
 
-type TcCoercionN = TcCoercion    -- A Nominal          corecion ~N
-type TcCoercionR = TcCoercion    -- A Representational corecion ~R
-
-data TcCoercion
-  = TcRefl Role TcType
-  | TcTyConAppCo Role TyCon [TcCoercion]
-  | TcAppCo TcCoercion TcCoercion
-  | TcForAllCo TyVar TcCoercion
-  | TcCoVarCo EqVar
-  | TcAxiomInstCo (CoAxiom Branched) Int [TcCoercion] -- Int specifies branch number
-                                                      -- See [CoAxiom Index] in Coercion.hs
-  -- This is number of types and coercions are expected to match to CoAxiomRule
-  -- (i.e., the CoAxiomRules are always fully saturated)
-  | TcAxiomRuleCo CoAxiomRule [TcType] [TcCoercion]
-  | TcPhantomCo TcType TcType
-  | TcSymCo TcCoercion
-  | TcTransCo TcCoercion TcCoercion
-  | TcNthCo Int TcCoercion
-  | TcLRCo LeftOrRight TcCoercion
-  | TcSubCo TcCoercion                 -- Argument is never TcRefl
-  | TcCastCo TcCoercion TcCoercion     -- co1 |> co2
-  | TcLetCo TcEvBinds TcCoercion
-  | TcCoercion Coercion            -- embed a Core Coercion
-  deriving (Data.Data, Data.Typeable)
-
-isEqVar :: Var -> Bool
--- Is lifted coercion variable (only!)
-isEqVar v = case tyConAppTyCon_maybe (varType v) of
-               Just tc -> tc `hasKey` eqTyConKey
-               Nothing -> False
-
-isTcReflCo_maybe :: TcCoercion -> Maybe TcType
-isTcReflCo_maybe (TcRefl _ ty)   = Just ty
-isTcReflCo_maybe (TcCoercion co) = isReflCo_maybe co
-isTcReflCo_maybe _               = Nothing
-
-isTcReflCo :: TcCoercion -> Bool
-isTcReflCo (TcRefl {})     = True
-isTcReflCo (TcCoercion co) = isReflCo co
-isTcReflCo _               = False
-
-getTcCoVar_maybe :: TcCoercion -> Maybe CoVar
-getTcCoVar_maybe (TcCoVarCo v) = Just v
-getTcCoVar_maybe _             = Nothing
-
-mkTcReflCo :: Role -> TcType -> TcCoercion
-mkTcReflCo = TcRefl
-
-mkTcNomReflCo :: TcType -> TcCoercion
-mkTcNomReflCo = TcRefl Nominal
-
-mkTcRepReflCo :: TcType -> TcCoercion
-mkTcRepReflCo = TcRefl Representational
-
-mkTcFunCo :: Role -> TcCoercion -> TcCoercion -> TcCoercion
-mkTcFunCo role co1 co2 = mkTcTyConAppCo role funTyCon [co1, co2]
-
-mkTcTyConAppCo :: Role -> TyCon -> [TcCoercion] -> TcCoercion
-mkTcTyConAppCo role tc cos -- No need to expand type synonyms
-                           -- See Note [TcCoercions]
-  | Just tys <- traverse isTcReflCo_maybe cos
-  = TcRefl role (mkTyConApp tc tys)  -- See Note [Refl invariant]
-
-  | otherwise = TcTyConAppCo role tc cos
-
--- Input coercion is Nominal
--- mkSubCo will do some normalisation. We do not do it for TcCoercions, but
--- defer that to desugaring; just to reduce the code duplication a little bit
-mkTcSubCo :: TcCoercion -> TcCoercion
-mkTcSubCo (TcRefl _ ty)
-  = TcRefl Representational ty
-mkTcSubCo co
-   = ASSERT2( tcCoercionRole co == Nominal, ppr co)
-     TcSubCo co
-
--- See Note [Role twiddling functions] in Coercion
--- | Change the role of a 'TcCoercion'. Returns 'Nothing' if this isn't
--- a downgrade.
-tcDowngradeRole_maybe :: Role   -- desired role
-                      -> Role   -- current role
-                      -> TcCoercion -> Maybe TcCoercion
-tcDowngradeRole_maybe Representational Nominal = Just . mkTcSubCo
-tcDowngradeRole_maybe Nominal Representational = const Nothing
-tcDowngradeRole_maybe Phantom _
-  = panic "tcDowngradeRole_maybe Phantom"
-    -- not supported (not needed at the moment)
-tcDowngradeRole_maybe _ Phantom                = const Nothing
-tcDowngradeRole_maybe _ _                      = Just
-
--- See Note [Role twiddling functions] in Coercion
--- | Change the role of a 'TcCoercion'. Panics if this isn't a downgrade.
-tcDowngradeRole :: Role  -- ^ desired role
-                -> Role  -- ^ current role
-                -> TcCoercion -> TcCoercion
-tcDowngradeRole r1 r2 co
-  = case tcDowngradeRole_maybe r1 r2 co of
-      Just co' -> co'
-      Nothing  -> pprPanic "tcDowngradeRole" (ppr r1 <+> ppr r2 <+> ppr co)
-
--- | If the EqRel is ReprEq, makes a TcSubCo; otherwise, does nothing.
--- Note that the input coercion should always be nominal.
-maybeTcSubCo :: EqRel -> TcCoercion -> TcCoercion
-maybeTcSubCo NomEq  = id
-maybeTcSubCo ReprEq = mkTcSubCo
-
-mkTcAxInstCo :: Role -> CoAxiom br -> Int -> [TcType] -> TcCoercion
-mkTcAxInstCo role ax index tys
-  | ASSERT2( not (role == Nominal && ax_role == Representational) , ppr (ax, tys) )
-    arity == n_tys = tcDowngradeRole role ax_role $
-                     TcAxiomInstCo ax_br index rtys
-  | otherwise      = ASSERT( arity < n_tys )
-                     tcDowngradeRole role ax_role $
-                     foldl TcAppCo (TcAxiomInstCo ax_br index (take arity rtys))
-                                   (drop arity rtys)
-  where
-    n_tys     = length tys
-    ax_br     = toBranchedAxiom ax
-    branch    = coAxiomNthBranch ax_br index
-    arity     = length $ coAxBranchTyVars branch
-    ax_role   = coAxiomRole ax
-    arg_roles = coAxBranchRoles branch
-    rtys      = zipWith mkTcReflCo (arg_roles ++ repeat Nominal) tys
-
-mkTcAxiomRuleCo :: CoAxiomRule -> [TcType] -> [TcCoercion] -> TcCoercion
-mkTcAxiomRuleCo = TcAxiomRuleCo
-
-mkTcUnbranchedAxInstCo :: Role -> CoAxiom Unbranched -> [TcType] -> TcCoercion
-mkTcUnbranchedAxInstCo role ax tys
-  = mkTcAxInstCo role ax 0 tys
-
-mkTcAppCo :: TcCoercion -> TcCoercion -> TcCoercion
--- No need to deal with TyConApp on the left; see Note [TcCoercions]
--- Second coercion *must* be nominal
-mkTcAppCo (TcRefl r ty1) (TcRefl _ ty2) = TcRefl r (mkAppTy ty1 ty2)
-mkTcAppCo co1 co2                       = TcAppCo co1 co2
-
--- | Like `mkTcAppCo`, but allows the second coercion to be other than
--- nominal. See Note [mkTcTransAppCo]. Role r3 cannot be more stringent
--- than either r1 or r2.
-mkTcTransAppCo :: Role           -- ^ r1
-               -> TcCoercion     -- ^ co1 :: ty1a ~r1 ty1b
-               -> TcType         -- ^ ty1a
-               -> TcType         -- ^ ty1b
-               -> Role           -- ^ r2
-               -> TcCoercion     -- ^ co2 :: ty2a ~r2 ty2b
-               -> TcType         -- ^ ty2a
-               -> TcType         -- ^ ty2b
-               -> Role           -- ^ r3
-               -> TcCoercion     -- ^ :: ty1a ty2a ~r3 ty1b ty2b
-mkTcTransAppCo r1 co1 ty1a ty1b r2 co2 ty2a ty2b r3
--- How incredibly fiddly! Is there a better way??
-  = case (r1, r2, r3) of
-      (_,                _,                Phantom)
-        -> mkTcPhantomCo (mkAppTy ty1a ty2a) (mkAppTy ty1b ty2b)
-      (_,                _,                Nominal)
-        -> ASSERT( r1 == Nominal && r2 == Nominal )
-           mkTcAppCo co1 co2
-      (Nominal,          Nominal,          Representational)
-        -> mkTcSubCo (mkTcAppCo co1 co2)
-      (_,                Nominal,          Representational)
-        -> ASSERT( r1 == Representational )
-           mkTcAppCo co1 co2
-      (Nominal,          Representational, Representational)
-        -> go (mkTcSubCo co1)
-      (_               , _,                Representational)
-        -> ASSERT( r1 == Representational && r2 == Representational )
-           go co1
-  where
-    go co1_repr
-      | Just (tc1b, tys1b) <- tcSplitTyConApp_maybe ty1b
-      , nextRole ty1b == r2
-      = (co1_repr `mkTcAppCo` mkTcNomReflCo ty2a) `mkTcTransCo`
-        (mkTcTyConAppCo Representational tc1b
-           (zipWith mkTcReflCo (tyConRolesX Representational tc1b) tys1b
-            ++ [co2]))
-
-      | Just (tc1a, tys1a) <- tcSplitTyConApp_maybe ty1a
-      , nextRole ty1a == r2
-      = (mkTcTyConAppCo Representational tc1a
-           (zipWith mkTcReflCo (tyConRolesX Representational tc1a) tys1a
-            ++ [co2]))
-        `mkTcTransCo`
-        (co1_repr `mkTcAppCo` mkTcNomReflCo ty2b)
-
-      | otherwise
-      = pprPanic "mkTcTransAppCo" (vcat [ ppr r1, ppr co1, ppr ty1a, ppr ty1b
-                                        , ppr r2, ppr co2, ppr ty2a, ppr ty2b
-                                        , ppr r3 ])
-
-mkTcSymCo :: TcCoercion -> TcCoercion
-mkTcSymCo co@(TcRefl {})  = co
-mkTcSymCo    (TcSymCo co) = co
-mkTcSymCo co              = TcSymCo co
-
-mkTcTransCo :: TcCoercion -> TcCoercion -> TcCoercion
-mkTcTransCo (TcRefl {}) co = co
-mkTcTransCo co (TcRefl {}) = co
-mkTcTransCo co1 co2        = TcTransCo co1 co2
-
-mkTcNthCo :: Int -> TcCoercion -> TcCoercion
-mkTcNthCo n (TcRefl r ty) = TcRefl r (tyConAppArgN n ty)
-mkTcNthCo n co            = TcNthCo n co
-
-mkTcLRCo :: LeftOrRight -> TcCoercion -> TcCoercion
-mkTcLRCo lr (TcRefl r ty) = TcRefl r (pickLR lr (tcSplitAppTy ty))
-mkTcLRCo lr co            = TcLRCo lr co
-
-mkTcPhantomCo :: TcType -> TcType -> TcCoercion
-mkTcPhantomCo = TcPhantomCo
-
-mkTcAppCos :: TcCoercion -> [TcCoercion] -> TcCoercion
-mkTcAppCos co1 tys = foldl mkTcAppCo co1 tys
-
-mkTcForAllCo :: Var -> TcCoercion -> TcCoercion
--- note that a TyVar should be used here, not a CoVar (nor a TcTyVar)
-mkTcForAllCo tv (TcRefl r ty) = ASSERT( isTyVar tv ) TcRefl r (mkForAllTy tv ty)
-mkTcForAllCo tv  co           = ASSERT( isTyVar tv ) TcForAllCo tv co
-
-mkTcForAllCos :: [Var] -> TcCoercion -> TcCoercion
-mkTcForAllCos tvs (TcRefl r ty) = ASSERT( all isTyVar tvs ) TcRefl r (mkForAllTys tvs ty)
-mkTcForAllCos tvs co            = ASSERT( all isTyVar tvs ) foldr TcForAllCo co tvs
-
-mkTcCoVarCo :: EqVar -> TcCoercion
--- ipv :: s ~ t  (the boxed equality type) or Coercible s t (the boxed representational equality type)
-mkTcCoVarCo ipv = TcCoVarCo ipv
-  -- Previously I checked for (ty ~ ty) and generated Refl,
-  -- but in fact ipv may not even (visibly) have a (t1 ~ t2) type, because
-  -- the constraint solver does not substitute in the types of
-  -- evidence variables as it goes.  In any case, the optimisation
-  -- will be done in the later zonking phase
-
-tcCoercionKind :: TcCoercion -> Pair Type
-tcCoercionKind co = go co
-  where
-    go (TcRefl _ ty)          = Pair ty ty
-    go (TcLetCo _ co)         = go co
-    go (TcCastCo _ co)        = case getEqPredTys (pSnd (go co)) of
-                                   (ty1,ty2) -> Pair ty1 ty2
-    go (TcTyConAppCo _ tc cos)= mkTyConApp tc <$> (sequenceA $ map go cos)
-    go (TcAppCo co1 co2)      = mkAppTy <$> go co1 <*> go co2
-    go (TcForAllCo tv co)     = mkForAllTy tv <$> go co
-    go (TcCoVarCo cv)         = eqVarKind cv
-    go (TcAxiomInstCo ax ind cos)
-      = let branch = coAxiomNthBranch ax ind
-            tvs = coAxBranchTyVars branch
-            Pair tys1 tys2 = sequenceA (map go cos)
-        in ASSERT( cos `equalLength` tvs )
-           Pair (substTyWith tvs tys1 (coAxNthLHS ax ind))
-                (substTyWith tvs tys2 (coAxBranchRHS branch))
-    go (TcPhantomCo ty1 ty2)  = Pair ty1 ty2
-    go (TcSymCo co)           = swap (go co)
-    go (TcTransCo co1 co2)    = Pair (pFst (go co1)) (pSnd (go co2))
-    go (TcNthCo d co)         = tyConAppArgN d <$> go co
-    go (TcLRCo lr co)         = (pickLR lr . tcSplitAppTy) <$> go co
-    go (TcSubCo co)           = go co
-    go (TcAxiomRuleCo ax ts cs) =
-       case coaxrProves ax ts (map tcCoercionKind cs) of
-         Just res -> res
-         Nothing -> panic "tcCoercionKind: malformed TcAxiomRuleCo"
-    go (TcCoercion co)        = coercionKind co
-
-eqVarRole :: EqVar -> Role
-eqVarRole cv = getEqPredRole (varType cv)
-
-eqVarKind :: EqVar -> Pair Type
-eqVarKind cv
- | Just (tc, [_kind,ty1,ty2]) <- tcSplitTyConApp_maybe (varType cv)
- = ASSERT(tc `hasKey` eqTyConKey)
-   Pair ty1 ty2
- | otherwise = pprPanic "eqVarKind, non coercion variable" (ppr cv <+> dcolon <+> ppr (varType cv))
-
-tcCoercionRole :: TcCoercion -> Role
-tcCoercionRole = go
-  where
-    go (TcRefl r _)           = r
-    go (TcTyConAppCo r _ _)   = r
-    go (TcAppCo co _)         = go co
-    go (TcForAllCo _ co)      = go co
-    go (TcCoVarCo cv)         = eqVarRole cv
-    go (TcAxiomInstCo ax _ _) = coAxiomRole ax
-    go (TcPhantomCo _ _)      = Phantom
-    go (TcSymCo co)           = go co
-    go (TcTransCo co1 _)      = go co1 -- same as go co2
-    go (TcNthCo n co)         = let Pair ty1 _ = tcCoercionKind co
-                                    (tc, _) = tcSplitTyConApp ty1
-                                in nthRole (go co) tc n
-    go (TcLRCo _ _)           = Nominal
-    go (TcSubCo _)            = Representational
-    go (TcAxiomRuleCo c _ _)  = coaxrRole c
-    go (TcCastCo c _)         = go c
-    go (TcLetCo _ c)          = go c
-    go (TcCoercion co)        = coercionRole co
-
-
-coVarsOfTcCo :: TcCoercion -> VarSet
--- Only works on *zonked* coercions, because of TcLetCo
-coVarsOfTcCo tc_co
-  = go tc_co
-  where
-    go (TcRefl _ _)              = emptyVarSet
-    go (TcTyConAppCo _ _ cos)    = mapUnionVarSet go cos
-    go (TcAppCo co1 co2)         = go co1 `unionVarSet` go co2
-    go (TcCastCo co1 co2)        = go co1 `unionVarSet` go co2
-    go (TcForAllCo _ co)         = go co
-    go (TcCoVarCo v)             = unitVarSet v
-    go (TcAxiomInstCo _ _ cos)   = mapUnionVarSet go cos
-    go (TcPhantomCo _ _)         = emptyVarSet
-    go (TcSymCo co)              = go co
-    go (TcTransCo co1 co2)       = go co1 `unionVarSet` go co2
-    go (TcNthCo _ co)            = go co
-    go (TcLRCo  _ co)            = go co
-    go (TcSubCo co)              = go co
-    go (TcLetCo (EvBinds bs) co) = foldrBag (unionVarSet . go_bind) (go co) bs
-                                   `minusVarSet` get_bndrs bs
-    go (TcLetCo {}) = emptyVarSet    -- Harumph. This does legitimately happen in the call
-                                     -- to evVarsOfTerm in the DEBUG check of setEvBind
-    go (TcAxiomRuleCo _ _ cos)   = mapUnionVarSet go cos
-    go (TcCoercion co)           = -- the use of coVarsOfTcCo in dsTcCoercion will
-                                   -- fail if there are any proper, unlifted covars
-                                   ASSERT( isEmptyVarSet (coVarsOfCo co) )
-                                   emptyVarSet
-
-    -- We expect only coercion bindings, so use evTermCoercion
-    go_bind :: EvBind -> VarSet
-    go_bind (EvBind { eb_rhs =tm }) = go (evTermCoercion tm)
-
-    get_bndrs :: Bag EvBind -> VarSet
-    get_bndrs = foldrBag (\ (EvBind { eb_lhs = b }) bs -> extendVarSet bs b) emptyVarSet
-
--- Pretty printing
-
-instance Outputable TcCoercion where
-  ppr = pprTcCo
-
-pprTcCo, pprParendTcCo :: TcCoercion -> SDoc
-pprTcCo       co = ppr_co TopPrec   co
-pprParendTcCo co = ppr_co TyConPrec co
-
-ppr_co :: TyPrec -> TcCoercion -> SDoc
-ppr_co _ (TcRefl r ty) = angleBrackets (ppr ty) <> ppr_role r
-
-ppr_co p co@(TcTyConAppCo _ tc [_,_])
-  | tc `hasKey` funTyConKey = ppr_fun_co p co
-
-ppr_co p (TcTyConAppCo r tc cos) = pprTcApp   p ppr_co tc cos <> ppr_role r
-ppr_co p (TcLetCo bs co)         = maybeParen p TopPrec $
-                                   sep [ptext (sLit "let") <+> braces (ppr bs), ppr co]
-ppr_co p (TcAppCo co1 co2)       = maybeParen p TyConPrec $
-                                   pprTcCo co1 <+> ppr_co TyConPrec co2
-ppr_co p (TcCastCo co1 co2)      = maybeParen p FunPrec $
-                                   ppr_co FunPrec co1 <+> ptext (sLit "|>") <+> ppr_co FunPrec co2
-ppr_co p co@(TcForAllCo {})      = ppr_forall_co p co
-
-ppr_co _ (TcCoVarCo cv)          = parenSymOcc (getOccName cv) (ppr cv)
-
-ppr_co p (TcAxiomInstCo con ind cos)
-  = pprPrefixApp p (ppr (getName con) <> brackets (ppr ind)) (map pprParendTcCo cos)
-
-ppr_co p (TcTransCo co1 co2) = maybeParen p FunPrec $
-                               ppr_co FunPrec co1
-                               <+> ptext (sLit ";")
-                               <+> ppr_co FunPrec co2
-ppr_co p (TcPhantomCo t1 t2)  = pprPrefixApp p (ptext (sLit "PhantomCo")) [pprParendType t1, pprParendType t2]
-ppr_co p (TcSymCo co)         = pprPrefixApp p (ptext (sLit "Sym")) [pprParendTcCo co]
-ppr_co p (TcNthCo n co)       = pprPrefixApp p (ptext (sLit "Nth:") <+> int n) [pprParendTcCo co]
-ppr_co p (TcLRCo lr co)       = pprPrefixApp p (ppr lr) [pprParendTcCo co]
-ppr_co p (TcSubCo co)         = pprPrefixApp p (ptext (sLit "Sub")) [pprParendTcCo co]
-ppr_co p (TcAxiomRuleCo co ts ps) = maybeParen p TopPrec
-                                  $ ppr_tc_axiom_rule_co co ts ps
-ppr_co p (TcCoercion co)      = pprPrefixApp p (text "Core co:") [ppr co]
-
-ppr_tc_axiom_rule_co :: CoAxiomRule -> [TcType] -> [TcCoercion] -> SDoc
-ppr_tc_axiom_rule_co co ts ps = ppr (coaxrName co) <> ppTs ts $$ nest 2 (ppPs ps)
-  where
-  ppTs []   = Outputable.empty
-  ppTs [t]  = ptext (sLit "@") <> ppr_type TopPrec t
-  ppTs ts   = ptext (sLit "@") <>
-                parens (hsep $ punctuate comma $ map pprType ts)
-
-  ppPs []   = Outputable.empty
-  ppPs [p]  = pprParendTcCo p
-  ppPs (p : ps) = ptext (sLit "(") <+> pprTcCo p $$
-                  vcat [ ptext (sLit ",") <+> pprTcCo q | q <- ps ] $$
-                  ptext (sLit ")")
-
-ppr_role :: Role -> SDoc
-ppr_role r = underscore <> pp_role
-  where pp_role = case r of
-                    Nominal          -> char 'N'
-                    Representational -> char 'R'
-                    Phantom          -> char 'P'
-
-ppr_fun_co :: TyPrec -> TcCoercion -> SDoc
-ppr_fun_co p co = pprArrowChain p (split co)
-  where
-    split :: TcCoercion -> [SDoc]
-    split (TcTyConAppCo _ f [arg,res])
-      | f `hasKey` funTyConKey
-      = ppr_co FunPrec arg : split res
-    split co = [ppr_co TopPrec co]
-
-ppr_forall_co :: TyPrec -> TcCoercion -> SDoc
-ppr_forall_co p ty
-  = maybeParen p FunPrec $
-    sep [pprForAll tvs, ppr_co TopPrec rho]
-  where
-    (tvs,  rho) = split1 [] ty
-    split1 tvs (TcForAllCo tv ty) = split1 (tv:tvs) ty
-    split1 tvs ty                 = (reverse tvs, ty)
+type TcCoercion  = Coercion
+type TcCoercionN = CoercionN    -- A Nominal          coercion ~N
+type TcCoercionR = CoercionR    -- A Representational coercion ~R
+type TcCoercionP = CoercionP    -- a phantom coercion
+
+mkTcReflCo             :: Role -> TcType -> TcCoercion
+mkTcSymCo              :: TcCoercion -> TcCoercion
+mkTcTransCo            :: TcCoercion -> TcCoercion -> TcCoercion
+mkTcNomReflCo          :: TcType -> TcCoercionN
+mkTcRepReflCo          :: TcType -> TcCoercionR
+mkTcTyConAppCo         :: Role -> TyCon -> [TcCoercion] -> TcCoercion
+mkTcAppCo              :: TcCoercion -> TcCoercionN -> TcCoercion
+mkTcFunCo              :: Role -> TcCoercion -> TcCoercion -> TcCoercion
+mkTcAxInstCo           :: Role -> CoAxiom br -> BranchIndex
+                       -> [TcType] -> [TcCoercion] -> TcCoercion
+mkTcUnbranchedAxInstCo :: CoAxiom Unbranched -> [TcType]
+                       -> [TcCoercion] -> TcCoercionR
+mkTcForAllCo           :: TyVar -> TcCoercionN -> TcCoercion -> TcCoercion
+mkTcForAllCos          :: [(TyVar, TcCoercionN)] -> TcCoercion -> TcCoercion
+mkTcNthCo              :: Int -> TcCoercion -> TcCoercion
+mkTcLRCo               :: LeftOrRight -> TcCoercion -> TcCoercion
+mkTcSubCo              :: TcCoercionN -> TcCoercionR
+maybeTcSubCo           :: EqRel -> TcCoercion -> TcCoercion
+tcDowngradeRole        :: Role -> Role -> TcCoercion -> TcCoercion
+mkTcAxiomRuleCo        :: CoAxiomRule -> [TcCoercion] -> TcCoercionR
+mkTcCoherenceLeftCo    :: TcCoercion -> TcCoercionN -> TcCoercion
+mkTcCoherenceRightCo   :: TcCoercion -> TcCoercionN -> TcCoercion
+mkTcPhantomCo          :: TcCoercionN -> TcType -> TcType -> TcCoercionP
+mkTcKindCo             :: TcCoercion -> TcCoercionN
+mkTcCoVarCo            :: CoVar -> TcCoercion
+
+tcCoercionKind         :: TcCoercion -> Pair TcType
+tcCoercionRole         :: TcCoercion -> Role
+coVarsOfTcCo           :: TcCoercion -> TcTyCoVarSet
+isTcReflCo             :: TcCoercion -> Bool
+
+-- | This version does a slow check, calculating the related types and seeing
+-- if they are equal.
+isTcReflexiveCo        :: TcCoercion -> Bool
+
+mkTcReflCo             = mkReflCo
+mkTcSymCo              = mkSymCo
+mkTcTransCo            = mkTransCo
+mkTcNomReflCo          = mkNomReflCo
+mkTcRepReflCo          = mkRepReflCo
+mkTcTyConAppCo         = mkTyConAppCo
+mkTcAppCo              = mkAppCo
+mkTcFunCo              = mkFunCo
+mkTcAxInstCo           = mkAxInstCo
+mkTcUnbranchedAxInstCo = mkUnbranchedAxInstCo Representational
+mkTcForAllCo           = mkForAllCo
+mkTcForAllCos          = mkForAllCos
+mkTcNthCo              = mkNthCo
+mkTcLRCo               = mkLRCo
+mkTcSubCo              = mkSubCo
+maybeTcSubCo           = maybeSubCo
+tcDowngradeRole        = downgradeRole
+mkTcAxiomRuleCo        = mkAxiomRuleCo
+mkTcCoherenceLeftCo    = mkCoherenceLeftCo
+mkTcCoherenceRightCo   = mkCoherenceRightCo
+mkTcPhantomCo          = mkPhantomCo
+mkTcKindCo             = mkKindCo
+mkTcCoVarCo            = mkCoVarCo
+
+tcCoercionKind         = coercionKind
+tcCoercionRole         = coercionRole
+coVarsOfTcCo           = coVarsOfCo
+isTcReflCo             = isReflCo
+isTcReflexiveCo        = isReflexiveCo
 
 {-
-************************************************************************
-*                                                                      *
+%************************************************************************
+%*                                                                      *
                   HsWrapper
 *                                                                      *
 ************************************************************************
@@ -562,23 +178,26 @@ data HsWrapper
        -- Hence  (\a. []) `WpCompose` (\b. []) = (\a b. [])
        -- But    ([] a)   `WpCompose` ([] b)   = ([] b a)
 
-  | WpFun HsWrapper HsWrapper TcType TcType
-       -- (WpFun wrap1 wrap2 t1 t2)[e] = \(x:t1). wrap2[ e wrap1[x] ] :: t2
+  | WpFun HsWrapper HsWrapper TcType SDoc
+       -- (WpFun wrap1 wrap2 t1)[e] = \(x:t1). wrap2[ e wrap1[x] ]
        -- So note that if  wrap1 :: exp_arg <= act_arg
        --                  wrap2 :: act_res <= exp_res
        --           then   WpFun wrap1 wrap2 : (act_arg -> arg_res) <= (exp_arg -> exp_res)
-       -- This isn't the same as for mkTcFunCo, but it has to be this way
+       -- This isn't the same as for mkFunCo, but it has to be this way
        -- because we can't use 'sym' to flip around these HsWrappers
+       -- The TcType is the "from" type of the first wrapper
+       -- The SDoc explains the circumstances under which we have created this
+       -- WpFun, in case we run afoul of levity polymorphism restrictions in
+       -- the desugarer. See Note [Levity polymorphism checking] in DsMonad
 
-  | WpCast TcCoercion         -- A cast:  [] `cast` co
+  | WpCast TcCoercionR        -- A cast:  [] `cast` co
                               -- Guaranteed not the identity coercion
                               -- At role Representational
 
         -- Evidence abstraction and application
         -- (both dictionaries and coercions)
-  | WpEvLam  EvVar               -- \d. []       the 'd' is an evidence variable
-  | WpEvApp  EvTerm              -- [] d         the 'd' is evidence for a constraint
-
+  | WpEvLam EvVar               -- \d. []       the 'd' is an evidence variable
+  | WpEvApp EvTerm              -- [] d         the 'd' is evidence for a constraint
         -- Kind and Type abstraction and application
   | WpTyLam TyVar       -- \a. []  the 'a' is a type/kind variable (not coercion var)
   | WpTyApp KindOrType  -- [] t    the 't' is a type (not coercion)
@@ -586,35 +205,121 @@ data HsWrapper
 
   | WpLet TcEvBinds             -- Non-empty (or possibly non-empty) evidence bindings,
                                 -- so that the identity coercion is always exactly WpHole
-  deriving (Data.Data, Data.Typeable)
 
+-- Cannot derive Data instance because SDoc is not Data (it stores a function).
+-- So we do it manually:
+instance Data.Data HsWrapper where
+  gfoldl _ z WpHole             = z WpHole
+  gfoldl k z (WpCompose a1 a2)  = z WpCompose `k` a1 `k` a2
+  gfoldl k z (WpFun a1 a2 a3 _) = z wpFunEmpty `k` a1 `k` a2 `k` a3
+  gfoldl k z (WpCast a1)        = z WpCast `k` a1
+  gfoldl k z (WpEvLam a1)       = z WpEvLam `k` a1
+  gfoldl k z (WpEvApp a1)       = z WpEvApp `k` a1
+  gfoldl k z (WpTyLam a1)       = z WpTyLam `k` a1
+  gfoldl k z (WpTyApp a1)       = z WpTyApp `k` a1
+  gfoldl k z (WpLet a1)         = z WpLet `k` a1
+
+  gunfold k z c = case Data.constrIndex c of
+                    1 -> z WpHole
+                    2 -> k (k (z WpCompose))
+                    3 -> k (k (k (z wpFunEmpty)))
+                    4 -> k (z WpCast)
+                    5 -> k (z WpEvLam)
+                    6 -> k (z WpEvApp)
+                    7 -> k (z WpTyLam)
+                    8 -> k (z WpTyApp)
+                    _ -> k (z WpLet)
+
+  toConstr WpHole          = wpHole_constr
+  toConstr (WpCompose _ _) = wpCompose_constr
+  toConstr (WpFun _ _ _ _) = wpFun_constr
+  toConstr (WpCast _)      = wpCast_constr
+  toConstr (WpEvLam _)     = wpEvLam_constr
+  toConstr (WpEvApp _)     = wpEvApp_constr
+  toConstr (WpTyLam _)     = wpTyLam_constr
+  toConstr (WpTyApp _)     = wpTyApp_constr
+  toConstr (WpLet _)       = wpLet_constr
+
+  dataTypeOf _ = hsWrapper_dataType
+
+hsWrapper_dataType :: Data.DataType
+hsWrapper_dataType
+  = Data.mkDataType "HsWrapper"
+      [ wpHole_constr, wpCompose_constr, wpFun_constr, wpCast_constr
+      , wpEvLam_constr, wpEvApp_constr, wpTyLam_constr, wpTyApp_constr
+      , wpLet_constr]
+
+wpHole_constr, wpCompose_constr, wpFun_constr, wpCast_constr, wpEvLam_constr,
+  wpEvApp_constr, wpTyLam_constr, wpTyApp_constr, wpLet_constr :: Data.Constr
+wpHole_constr    = mkHsWrapperConstr "WpHole"
+wpCompose_constr = mkHsWrapperConstr "WpCompose"
+wpFun_constr     = mkHsWrapperConstr "WpFun"
+wpCast_constr    = mkHsWrapperConstr "WpCast"
+wpEvLam_constr   = mkHsWrapperConstr "WpEvLam"
+wpEvApp_constr   = mkHsWrapperConstr "WpEvApp"
+wpTyLam_constr   = mkHsWrapperConstr "WpTyLam"
+wpTyApp_constr   = mkHsWrapperConstr "WpTyApp"
+wpLet_constr     = mkHsWrapperConstr "WpLet"
+
+mkHsWrapperConstr :: String -> Data.Constr
+mkHsWrapperConstr name = Data.mkConstr hsWrapper_dataType name [] Data.Prefix
+
+wpFunEmpty :: HsWrapper -> HsWrapper -> TcType -> HsWrapper
+wpFunEmpty c1 c2 t1 = WpFun c1 c2 t1 empty
 
 (<.>) :: HsWrapper -> HsWrapper -> HsWrapper
 WpHole <.> c = c
 c <.> WpHole = c
 c1 <.> c2    = c1 `WpCompose` c2
 
-mkWpFun :: HsWrapper -> HsWrapper -> TcType -> TcType -> HsWrapper
-mkWpFun WpHole       WpHole       _  _  = WpHole
-mkWpFun WpHole       (WpCast co2) t1 _  = WpCast (mkTcFunCo Representational (mkTcRepReflCo t1) co2)
-mkWpFun (WpCast co1) WpHole       _  t2 = WpCast (mkTcFunCo Representational (mkTcSymCo co1) (mkTcRepReflCo t2))
-mkWpFun (WpCast co1) (WpCast co2) _  _  = WpCast (mkTcFunCo Representational (mkTcSymCo co1) co2)
-mkWpFun co1          co2          t1 t2 = WpFun co1 co2 t1 t2
+mkWpFun :: HsWrapper -> HsWrapper
+        -> TcType    -- the "from" type of the first wrapper
+        -> TcType    -- either type of the second wrapper (used only when the
+                     -- second wrapper is the identity)
+        -> SDoc      -- what caused you to want a WpFun? Something like "When converting ..."
+        -> HsWrapper
+mkWpFun WpHole       WpHole       _  _  _ = WpHole
+mkWpFun WpHole       (WpCast co2) t1 _  _ = WpCast (mkTcFunCo Representational (mkTcRepReflCo t1) co2)
+mkWpFun (WpCast co1) WpHole       _  t2 _ = WpCast (mkTcFunCo Representational (mkTcSymCo co1) (mkTcRepReflCo t2))
+mkWpFun (WpCast co1) (WpCast co2) _  _  _ = WpCast (mkTcFunCo Representational (mkTcSymCo co1) co2)
+mkWpFun co1          co2          t1 _  d = WpFun co1 co2 t1 d
+
+-- | @mkWpFuns [(ty1, wrap1), (ty2, wrap2)] ty_res wrap_res@,
+-- where @wrap1 :: ty1 "->" ty1'@ and @wrap2 :: ty2 "->" ty2'@,
+-- @wrap3 :: ty3 "->" ty3'@ and @ty_res@ is /either/ @ty3@ or @ty3'@,
+-- gives a wrapper @(ty1' -> ty2' -> ty3) "->" (ty1 -> ty2 -> ty3')@.
+-- Notice that the result wrapper goes the other way round to all
+-- the others. This is a result of sub-typing contravariance.
+-- The SDoc is a description of what you were doing when you called mkWpFuns.
+mkWpFuns :: [(TcType, HsWrapper)] -> TcType -> HsWrapper -> SDoc -> HsWrapper
+mkWpFuns args res_ty res_wrap doc = snd $ go args res_ty res_wrap
+  where
+    go [] res_ty res_wrap = (res_ty, res_wrap)
+    go ((arg_ty, arg_wrap) : args) res_ty res_wrap
+      = let (tail_ty, tail_wrap) = go args res_ty res_wrap in
+        (arg_ty `mkFunTy` tail_ty, mkWpFun arg_wrap tail_wrap arg_ty tail_ty doc)
 
-mkWpCast :: TcCoercion -> HsWrapper
-mkWpCast co
+mkWpCastR :: TcCoercionR -> HsWrapper
+mkWpCastR co
   | isTcReflCo co = WpHole
   | otherwise     = ASSERT2(tcCoercionRole co == Representational, ppr co)
                     WpCast co
 
+mkWpCastN :: TcCoercionN -> HsWrapper
+mkWpCastN co
+  | isTcReflCo co = WpHole
+  | otherwise     = ASSERT2(tcCoercionRole co == Nominal, ppr co)
+                    WpCast (mkTcSubCo co)
+    -- The mkTcSubCo converts Nominal to Representational
+
 mkWpTyApps :: [Type] -> HsWrapper
 mkWpTyApps tys = mk_co_app_fn WpTyApp tys
 
-mkWpEvApps :: [EvTerm] -> HsWrapper
-mkWpEvApps args = mk_co_app_fn WpEvApp args
+mkWpEvApps :: [EvExpr] -> HsWrapper
+mkWpEvApps args = mk_co_app_fn WpEvApp (map EvExpr args)
 
 mkWpEvVarApps :: [EvVar] -> HsWrapper
-mkWpEvVarApps vs = mkWpEvApps (map EvId vs)
+mkWpEvVarApps vs = mk_co_app_fn WpEvApp (map (EvExpr . evId) vs)
 
 mkWpTyLams :: [TyVar] -> HsWrapper
 mkWpTyLams ids = mk_co_lam_fn WpTyLam ids
@@ -642,6 +347,23 @@ isIdHsWrapper :: HsWrapper -> Bool
 isIdHsWrapper WpHole = True
 isIdHsWrapper _      = False
 
+collectHsWrapBinders :: HsWrapper -> ([Var], HsWrapper)
+-- Collect the outer lambda binders of a HsWrapper,
+-- stopping as soon as you get to a non-lambda binder
+collectHsWrapBinders wrap = go wrap []
+  where
+    -- go w ws = collectHsWrapBinders (w <.> w1 <.> ... <.> wn)
+    go :: HsWrapper -> [HsWrapper] -> ([Var], HsWrapper)
+    go (WpEvLam v)       wraps = add_lam v (gos wraps)
+    go (WpTyLam v)       wraps = add_lam v (gos wraps)
+    go (WpCompose w1 w2) wraps = go w1 (w2:wraps)
+    go wrap              wraps = ([], foldl (<.>) wrap wraps)
+
+    gos []     = ([], WpHole)
+    gos (w:ws) = go w ws
+
+    add_lam v (vs,w) = (v:vs, w)
+
 {-
 ************************************************************************
 *                                                                      *
@@ -658,10 +380,26 @@ data TcEvBinds
   | EvBinds             -- Immutable after zonking
        (Bag EvBind)
 
-  deriving( Data.Typeable )
-
-data EvBindsVar = EvBindsVar (IORef EvBindMap) Unique
-     -- The Unique is only for debug printing
+data EvBindsVar
+  = EvBindsVar {
+      ebv_uniq :: Unique,
+         -- The Unique is for debug printing only
+
+      ebv_binds :: IORef EvBindMap,
+      -- The main payload: the value-level evidence bindings
+      --     (dictionaries etc)
+      -- Some Given, some Wanted
+
+      ebv_tcvs :: IORef CoVarSet
+      -- The free coercion vars of the (rhss of) the coercion bindings
+      -- All of these are Wanted
+      --
+      -- Coercions don't actually have bindings
+      -- because we plug them in-place (via a mutable
+      -- variable); but we keep their free variables
+      -- so that we can report unused given constraints
+      -- See Note [Tracking redundant constraints] in TcSimplify
+    }
 
 instance Data.Data TcEvBinds where
   -- Placeholder; we can't travers into TcEvBinds
@@ -672,26 +410,54 @@ instance Data.Data TcEvBinds where
 -----------------
 newtype EvBindMap
   = EvBindMap {
-       ev_bind_varenv :: VarEnv EvBind
+       ev_bind_varenv :: DVarEnv EvBind
     }       -- Map from evidence variables to evidence terms
+            -- We use @DVarEnv@ here to get deterministic ordering when we
+            -- turn it into a Bag.
+            -- If we don't do that, when we generate let bindings for
+            -- dictionaries in dsTcEvBinds they will be generated in random
+            -- order.
+            --
+            -- For example:
+            --
+            -- let $dEq = GHC.Classes.$fEqInt in
+            -- let $$dNum = GHC.Num.$fNumInt in ...
+            --
+            -- vs
+            --
+            -- let $dNum = GHC.Num.$fNumInt in
+            -- let $dEq = GHC.Classes.$fEqInt in ...
+            --
+            -- See Note [Deterministic UniqFM] in UniqDFM for explanation why
+            -- @UniqFM@ can lead to nondeterministic order.
 
 emptyEvBindMap :: EvBindMap
-emptyEvBindMap = EvBindMap { ev_bind_varenv = emptyVarEnv }
+emptyEvBindMap = EvBindMap { ev_bind_varenv = emptyDVarEnv }
 
 extendEvBinds :: EvBindMap -> EvBind -> EvBindMap
 extendEvBinds bs ev_bind
-  = EvBindMap { ev_bind_varenv = extendVarEnv (ev_bind_varenv bs)
-                                              (eb_lhs ev_bind)
-                                              ev_bind }
+  = EvBindMap { ev_bind_varenv = extendDVarEnv (ev_bind_varenv bs)
+                                               (eb_lhs ev_bind)
+                                               ev_bind }
+
+isEmptyEvBindMap :: EvBindMap -> Bool
+isEmptyEvBindMap (EvBindMap m) = isEmptyDVarEnv m
 
 lookupEvBind :: EvBindMap -> EvVar -> Maybe EvBind
-lookupEvBind bs = lookupVarEnv (ev_bind_varenv bs)
+lookupEvBind bs = lookupDVarEnv (ev_bind_varenv bs)
 
 evBindMapBinds :: EvBindMap -> Bag EvBind
 evBindMapBinds = foldEvBindMap consBag emptyBag
 
 foldEvBindMap :: (EvBind -> a -> a) -> a -> EvBindMap -> a
-foldEvBindMap k z bs = foldVarEnv k z (ev_bind_varenv bs)
+foldEvBindMap k z bs = foldDVarEnv k z (ev_bind_varenv bs)
+
+filterEvBindMap :: (EvBind -> Bool) -> EvBindMap -> EvBindMap
+filterEvBindMap k (EvBindMap { ev_bind_varenv = env })
+  = EvBindMap { ev_bind_varenv = filterDVarEnv k env }
+
+instance Outputable EvBindMap where
+  ppr (EvBindMap m) = ppr m
 
 -----------------
 -- All evidence is bound by EvBinds; no side effects
@@ -702,84 +468,119 @@ data EvBind
                  -- See Note [Tracking redundant constraints] in TcSimplify
     }
 
+evBindVar :: EvBind -> EvVar
+evBindVar = eb_lhs
+
 mkWantedEvBind :: EvVar -> EvTerm -> EvBind
 mkWantedEvBind ev tm = EvBind { eb_is_given = False, eb_lhs = ev, eb_rhs = tm }
 
-mkGivenEvBind :: EvVar -> EvTerm -> EvBind
-mkGivenEvBind ev tm = EvBind { eb_is_given = True, eb_lhs = ev, eb_rhs = tm }
+-- EvTypeable are never given, so we can work with EvExpr here instead of EvTerm
+mkGivenEvBind :: EvVar -> EvExpr -> EvBind
+mkGivenEvBind ev tm = EvBind { eb_is_given = True, eb_lhs = ev, eb_rhs = EvExpr tm }
 
-data EvTerm
-  = EvId EvId                    -- Any sort of evidence Id, including coercions
 
-  | EvCoercion TcCoercion        -- (Boxed) coercion bindings
-                                 -- See Note [Coercion evidence terms]
+-- An EvTerm is, conceptually, a CoreExpr that implements the constraint.
+-- Unfortunately, we cannot just do
+--   type EvTerm  = CoreExpr
+-- Because of staging problems issues around EvTypeable
+data EvTerm
+    = EvExpr EvExpr
+    | EvTypeable Type EvTypeable   -- Dictionary for (Typeable ty)
+  deriving Data.Data
 
-  | EvCast EvTerm TcCoercion     -- d |> co, the coercion being at role representational
+type EvExpr = CoreExpr
 
-  | EvDFunApp DFunId             -- Dictionary instance application
-       [Type] [EvId]
+-- An EvTerm is (usually) constructed by any of the constructors here
+-- and those more complicates ones who were moved to module TcEvTerm
 
-  | EvDelayedError Type FastString  -- Used with Opt_DeferTypeErrors
-                               -- See Note [Deferring coercion errors to runtime]
-                               -- in TcSimplify
+-- | Any sort of evidence Id, including coercions
+evId ::  EvId -> EvExpr
+evId = Var
 
-  | EvSuperClass EvTerm Int      -- n'th superclass. Used for both equalities and
-                                 -- dictionaries, even though the former have no
-                                 -- selector Id.  We count up from _0_
+-- coercion bindings
+-- See Note [Coercion evidence terms]
+evCoercion :: TcCoercion -> EvExpr
+evCoercion = Coercion
 
-  | EvLit EvLit       -- Dictionary for KnownNat and KnownSymbol classes.
-                      -- Note [KnownNat & KnownSymbol and EvLit]
+-- | d |> co
+evCast :: EvExpr -> TcCoercion -> EvExpr
+evCast et tc | isReflCo tc = et
+             | otherwise   = Cast et tc
 
-  | EvCallStack EvCallStack -- Dictionary for CallStack implicit parameters
+-- Dictionary instance application
+evDFunApp :: DFunId -> [Type] -> [EvExpr] -> EvExpr
+evDFunApp df tys ets = Var df `mkTyApps` tys `mkApps` ets
 
-  | EvTypeable EvTypeable   -- Dictionary for `Typeable`
+-- Selector id plus the types at which it
+-- should be instantiated, used for HasField
+-- dictionaries; see Note [HasField instances]
+-- in TcInterface
+evSelector :: Id -> [Type] -> [EvExpr] -> EvExpr
+evSelector sel_id tys tms = Var sel_id `mkTyApps` tys `mkApps` tms
 
-  deriving( Data.Data, Data.Typeable )
 
+-- Dictionary for (Typeable ty)
+evTypeable :: Type -> EvTypeable -> EvTerm
+evTypeable = EvTypeable
 
 -- | Instructions on how to make a 'Typeable' dictionary.
+-- See Note [Typeable evidence terms]
 data EvTypeable
-  = EvTypeableTyCon TyCon [Kind]
-    -- ^ Dictionary for concrete type constructors.
-
-  | EvTypeableTyApp (EvTerm,Type) (EvTerm,Type)
-    -- ^ Dictionary for type applications;  this is used when we have
-    -- a type expression starting with a type variable (e.g., @Typeable (f a)@)
-
-  | EvTypeableTyLit (EvTerm,Type)
-    -- ^ Dictionary for a type literal.
-
-  deriving ( Data.Data, Data.Typeable )
-
-data EvLit
-  = EvNum Integer
-  | EvStr FastString
-    deriving( Data.Data, Data.Typeable )
+  = EvTypeableTyCon TyCon [EvTerm]
+    -- ^ Dictionary for @Typeable T@ where @T@ is a type constructor with all of
+    -- its kind variables saturated. The @[EvTerm]@ is @Typeable@ evidence for
+    -- the applied kinds..
+
+  | EvTypeableTyApp EvTerm EvTerm
+    -- ^ Dictionary for @Typeable (s t)@,
+    -- given a dictionaries for @s@ and @t@.
+
+  | EvTypeableTrFun EvTerm EvTerm
+    -- ^ Dictionary for @Typeable (s -> t)@,
+    -- given a dictionaries for @s@ and @t@.
+
+  | EvTypeableTyLit EvTerm
+    -- ^ Dictionary for a type literal,
+    -- e.g. @Typeable "foo"@ or @Typeable 3@
+    -- The 'EvTerm' is evidence of, e.g., @KnownNat 3@
+    -- (see Trac #10348)
+  deriving Data.Data
 
 -- | Evidence for @CallStack@ implicit parameters.
 data EvCallStack
   -- See Note [Overview of implicit CallStacks]
   = EvCsEmpty
-  | EvCsPushCall Name RealSrcSpan EvTerm
+  | EvCsPushCall Name RealSrcSpan EvExpr
     -- ^ @EvCsPushCall name loc stk@ represents a call to @name@, occurring at
     -- @loc@, in a calling context @stk@.
-  | EvCsTop FastString RealSrcSpan EvTerm
-    -- ^ @EvCsTop name loc stk@ represents a use of an implicit parameter
-    -- @?name@, occurring at @loc@, in a calling context @stk@.
-  deriving( Data.Data, Data.Typeable )
+  deriving Data.Data
 
 {-
+Note [Typeable evidence terms]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The EvTypeable data type looks isomorphic to Type, but the EvTerms
+inside can be EvIds.  Eg
+    f :: forall a. Typeable a => a -> TypeRep
+    f x = typeRep (undefined :: Proxy [a])
+Here for the (Typeable [a]) dictionary passed to typeRep we make
+evidence
+    dl :: Typeable [a] = EvTypeable [a]
+                            (EvTypeableTyApp (EvTypeableTyCon []) (EvId d))
+where
+    d :: Typable a
+is the lambda-bound dictionary passed into f.
+
 Note [Coercion evidence terms]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 A "coercion evidence term" takes one of these forms
-   co_tm ::= EvId v           where v :: t1 ~ t2
+   co_tm ::= EvId v           where v :: t1 ~# t2
            | EvCoercion co
            | EvCast co_tm co
 
 We do quite often need to get a TcCoercion from an EvTerm; see
 'evTermCoercion'.
 
-INVARIANT: The evidence for any constraint with type (t1~t2) is
+INVARIANT: The evidence for any constraint with type (t1 ~# t2) is
 a coercion evidence term.  Consider for example
     [G] d :: F Int a
 If we have
@@ -811,139 +612,104 @@ Conclusion: a new wanted coercion variable should be made mutable.
  from super classes will be "given" and hence rigid]
 
 
-Note [KnownNat & KnownSymbol and EvLit]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-A part of the type-level literals implementation are the classes
-"KnownNat" and "KnownSymbol", which provide a "smart" constructor for
-defining singleton values.  Here is the key stuff from GHC.TypeLits
-
-  class KnownNat (n :: Nat) where
-    natSing :: SNat n
-
-  newtype SNat (n :: Nat) = SNat Integer
-
-Conceptually, this class has infinitely many instances:
+Note [Overview of implicit CallStacks]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+(See https://ghc.haskell.org/trac/ghc/wiki/ExplicitCallStack/ImplicitLocations)
 
-  instance KnownNat 0       where natSing = SNat 0
-  instance KnownNat 1       where natSing = SNat 1
-  instance KnownNat 2       where natSing = SNat 2
-  ...
+The goal of CallStack evidence terms is to reify locations
+in the program source as runtime values, without any support
+from the RTS. We accomplish this by assigning a special meaning
+to constraints of type GHC.Stack.Types.HasCallStack, an alias
 
-In practice, we solve `KnownNat` predicates in the type-checker
-(see typecheck/TcInteract.hs) because we can't have infinately many instances.
-The evidence (aka "dictionary") for `KnownNat` is of the form `EvLit (EvNum n)`.
+  type HasCallStack = (?callStack :: CallStack)
 
-We make the following assumptions about dictionaries in GHC:
-  1. The "dictionary" for classes with a single method---like `KnownNat`---is
-     a newtype for the type of the method, so using a evidence amounts
-     to a coercion, and
-  2. Newtypes use the same representation as their definition types.
+Implicit parameters of type GHC.Stack.Types.CallStack (the name is not
+important) are solved in three steps:
 
-So, the evidence for `KnownNat` is just a value of the representation type,
-wrapped in two newtype constructors: one to make it into a `SNat` value,
-and another to make it into a `KnownNat` dictionary.
+1. Occurrences of CallStack IPs are solved directly from the given IP,
+   just like a regular IP. For example, the occurrence of `?stk` in
 
-Also note that `natSing` and `SNat` are never actually exposed from the
-library---they are just an implementation detail.  Instead, users see
-a more convenient function, defined in terms of `natSing`:
+     error :: (?stk :: CallStack) => String -> a
+     error s = raise (ErrorCall (s ++ prettyCallStack ?stk))
 
-  natVal :: KnownNat n => proxy n -> Integer
+   will be solved for the `?stk` in `error`s context as before.
 
-The reason we don't use this directly in the class is that it is simpler
-and more efficient to pass around an integer rather than an entier function,
-especialy when the `KnowNat` evidence is packaged up in an existential.
+2. In a function call, instead of simply passing the given IP, we first
+   append the current call-site to it. For example, consider a
+   call to the callstack-aware `error` above.
 
-The story for kind `Symbol` is analogous:
-  * class KnownSymbol
-  * newtype SSymbol
-  * Evidence: EvLit (EvStr n)
+     undefined :: (?stk :: CallStack) => a
+     undefined = error "undefined!"
 
+   Here we want to take the given `?stk` and append the current
+   call-site, before passing it to `error`. In essence, we want to
+   rewrite `error "undefined!"` to
 
-Note [Overview of implicit CallStacks]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-(See https://ghc.haskell.org/trac/ghc/wiki/ExplicitCallStack/ImplicitLocations)
+     let ?stk = pushCallStack <error's location> ?stk
+     in error "undefined!"
 
-The goal of CallStack evidence terms is to reify locations
-in the program source as runtime values, without any support
-from the RTS. We accomplish this by assigning a special meaning
-to implicit parameters of type GHC.Stack.CallStack. A use of
-a CallStack IP, e.g.
+   We achieve this effect by emitting a NEW wanted
 
-  head []    = error (show (?loc :: CallStack))
-  head (x:_) = x
+     [W] d :: IP "stk" CallStack
 
-will be solved with the source location that gave rise to the IP
-constraint (here, the use of ?loc). If there is already
-a CallStack IP in scope, e.g. passed-in as an argument
+   from which we build the evidence term
 
-  head :: (?loc :: CallStack) => [a] -> a
-  head []    = error (show (?loc :: CallStack))
-  head (x:_) = x
+     EvCsPushCall "error" <error's location> (EvId d)
 
-we will push the new location onto the CallStack that was passed
-in. These two cases are reflected by the EvCallStack evidence
-type. In the first case, we will create an evidence term
+   that we use to solve the call to `error`. The new wanted `d` will
+   then be solved per rule (1), ie as a regular IP.
 
-  EvCsTop "?loc" <?loc's location> EvCsEmpty
+   (see TcInteract.interactDict)
 
-and in the second we'll have a given constraint
+3. We default any insoluble CallStacks to the empty CallStack. Suppose
+   `undefined` did not request a CallStack, ie
 
-  [G] d :: IP "loc" CallStack
+     undefinedNoStk :: a
+     undefinedNoStk = error "undefined!"
 
-in scope, and will create an evidence term
+   Under the usual IP rules, the new wanted from rule (2) would be
+   insoluble as there's no given IP from which to solve it, so we
+   would get an "unbound implicit parameter" error.
 
-  EvCsTop "?loc" <?loc's location> d
+   We don't ever want to emit an insoluble CallStack IP, so we add a
+   defaulting pass to default any remaining wanted CallStacks to the
+   empty CallStack with the evidence term
 
-When we call a function that uses a CallStack IP, e.g.
+     EvCsEmpty
 
-  f = head xs
-
-we create an evidence term
-
-  EvCsPushCall "head" <head's location> EvCsEmpty
-
-again pushing onto a given evidence term if one exists.
+   (see TcSimplify.simpl_top and TcSimplify.defaultCallStacks)
 
 This provides a lightweight mechanism for building up call-stacks
 explicitly, but is notably limited by the fact that the stack will
 stop at the first function whose type does not include a CallStack IP.
-For example, using the above definition of head:
+For example, using the above definition of `undefined`:
 
-  f :: [a] -> a
-  f = head
+  head :: [a] -> a
+  head []    = undefined
+  head (x:_) = x
 
-  g = f []
+  g = head []
+
+the resulting CallStack will include the call to `undefined` in `head`
+and the call to `error` in `undefined`, but *not* the call to `head`
+in `g`, because `head` did not explicitly request a CallStack.
 
-the resulting CallStack will include use of ?loc inside head and
-the call to head inside f, but NOT the call to f inside g, because f
-did not explicitly request a CallStack.
 
 Important Details:
 - GHC should NEVER report an insoluble CallStack constraint.
 
-- A CallStack (defined in GHC.Stack) is a [(String, SrcLoc)], where the String
-  is the name of the binder that is used at the SrcLoc. SrcLoc is defined in
-  GHC.SrcLoc and contains the package/module/file name, as well as the full
-  source-span. Both CallStack and SrcLoc are kept abstract so only GHC can
-  construct new values.
-
-- Consider the use of ?stk in:
-
-    head :: (?stk :: CallStack) => [a] -> a
-    head [] = error (show ?stk)
+- GHC should NEVER infer a CallStack constraint unless one was requested
+  with a partial type signature (See TcType.pickQuantifiablePreds).
 
-  When solving the use of ?stk we'll have a given
+- A CallStack (defined in GHC.Stack.Types) is a [(String, SrcLoc)],
+  where the String is the name of the binder that is used at the
+  SrcLoc. SrcLoc is also defined in GHC.Stack.Types and contains the
+  package/module/file name, as well as the full source-span. Both
+  CallStack and SrcLoc are kept abstract so only GHC can construct new
+  values.
 
-   [G] d :: IP "stk" CallStack
-
-  in scope. In the interaction phase, GHC would normally solve the use of ?stk
-  directly from the given, i.e. re-using the dicionary. But this is NOT what we
-  want! We want to generate a *new* CallStack with ?loc's SrcLoc pushed onto
-  the given CallStack. So we must take care in TcInteract.interactDict to
-  prioritize solving wanted CallStacks.
-
-- We will automatically solve any wanted CallStack regardless of the name of the
-  IP, i.e.
+- We will automatically solve any wanted CallStack regardless of the
+  name of the IP, i.e.
 
     f = show (?stk :: CallStack)
     g = show (?loc :: CallStack)
@@ -955,34 +721,34 @@ Important Details:
     head [] = error (show (?stk :: CallStack))
 
   the printed CallStack will NOT include head's call-site. This reflects the
-  standard scoping rules of implicit-parameters. (See TcInteract.interactDict)
+  standard scoping rules of implicit-parameters.
 
 - An EvCallStack term desugars to a CoreExpr of type `IP "some str" CallStack`.
   The desugarer will need to unwrap the IP newtype before pushing a new
   call-site onto a given stack (See DsBinds.dsEvCallStack)
 
-- We only want to intercept constraints that arose due to the use of an IP or a
-  function call. In particular, we do NOT want to intercept the
+- When we emit a new wanted CallStack from rule (2) we set its origin to
+  `IPOccOrigin ip_name` instead of the original `OccurrenceOf func`
+  (see TcInteract.interactDict).
 
-    (?stk :: CallStack) => [a] -> a
-      ~
-    (?stk :: CallStack) => [a] -> a
+  This is a bit shady, but is how we ensure that the new wanted is
+  solved like a regular IP.
 
-  constraint that arises from the ambiguity check on `head`s type signature.
-  (See TcEvidence.isCallStackIP)
 -}
 
-mkEvCast :: EvTerm -> TcCoercion -> EvTerm
+mkEvCast :: EvExpr -> TcCoercion -> EvExpr
 mkEvCast ev lco
-  | ASSERT2(tcCoercionRole lco == Representational, (vcat [ptext (sLit "Coercion of wrong role passed to mkEvCast:"), ppr ev, ppr lco]))
+  | ASSERT2(tcCoercionRole lco == Representational, (vcat [text "Coercion of wrong role passed to mkEvCast:", ppr ev, ppr lco]))
     isTcReflCo lco = ev
-  | otherwise      = EvCast ev lco
+  | otherwise      = evCast ev lco
 
-mkEvScSelectors :: EvTerm -> Class -> [TcType] -> [(TcPredType, EvTerm)]
+mkEvScSelectors :: EvExpr -> Class -> [TcType] -> [(TcPredType, EvExpr)]
 mkEvScSelectors ev cls tys
    = zipWith mk_pr (immSuperClasses cls tys) [0..]
   where
-    mk_pr pred i = (pred, EvSuperClass ev i)
+    mk_pr pred i = (pred, Var sc_sel_id `mkTyApps` tys `App` ev)
+      where
+        sc_sel_id  = classSCSelId cls i -- Zero-indexed
 
 emptyTcEvBinds :: TcEvBinds
 emptyTcEvBinds = EvBinds emptyBag
@@ -991,41 +757,70 @@ isEmptyTcEvBinds :: TcEvBinds -> Bool
 isEmptyTcEvBinds (EvBinds b)    = isEmptyBag b
 isEmptyTcEvBinds (TcEvBinds {}) = panic "isEmptyTcEvBinds"
 
-
 evTermCoercion :: EvTerm -> TcCoercion
 -- Applied only to EvTerms of type (s~t)
 -- See Note [Coercion evidence terms]
-evTermCoercion (EvId v)        = mkTcCoVarCo v
-evTermCoercion (EvCoercion co) = co
-evTermCoercion (EvCast tm co)  = TcCastCo (evTermCoercion tm) co
-evTermCoercion tm = pprPanic "evTermCoercion" (ppr tm)
+evTermCoercion (EvExpr (Var v))       = mkCoVarCo v
+evTermCoercion (EvExpr (Coercion co)) = co
+evTermCoercion (EvExpr (Cast tm co))  = mkCoCast (evTermCoercion (EvExpr tm)) co
+evTermCoercion tm                     = pprPanic "evTermCoercion" (ppr tm)
+
+
+{-
+************************************************************************
+*                                                                      *
+                  Free variables
+*                                                                      *
+************************************************************************
+-}
+
+findNeededEvVars :: EvBindMap -> VarSet -> VarSet
+findNeededEvVars ev_binds seeds
+  = transCloVarSet also_needs seeds
+  where
+   also_needs :: VarSet -> VarSet
+   also_needs needs = nonDetFoldUniqSet add emptyVarSet needs
+     -- It's OK to use nonDetFoldUFM here because we immediately
+     -- forget about the ordering by creating a set
+
+   add :: Var -> VarSet -> VarSet
+   add v needs
+     | Just ev_bind <- lookupEvBind ev_binds v
+     , EvBind { eb_is_given = is_given, eb_rhs = rhs } <- ev_bind
+     , is_given
+     = evVarsOfTerm rhs `unionVarSet` needs
+     | otherwise
+     = needs
 
 evVarsOfTerm :: EvTerm -> VarSet
-evVarsOfTerm (EvId v)             = unitVarSet v
-evVarsOfTerm (EvCoercion co)      = coVarsOfTcCo co
-evVarsOfTerm (EvDFunApp _ _ evs)  = mkVarSet evs
-evVarsOfTerm (EvSuperClass v _)   = evVarsOfTerm v
-evVarsOfTerm (EvCast tm co)       = evVarsOfTerm tm `unionVarSet` coVarsOfTcCo co
-evVarsOfTerm (EvDelayedError _ _) = emptyVarSet
-evVarsOfTerm (EvLit _)            = emptyVarSet
-evVarsOfTerm (EvCallStack cs)     = evVarsOfCallStack cs
-evVarsOfTerm (EvTypeable ev)      = evVarsOfTypeable ev
+evVarsOfTerm (EvExpr e)         = exprSomeFreeVars isEvVar e
+evVarsOfTerm (EvTypeable _ ev)  = evVarsOfTypeable ev
 
 evVarsOfTerms :: [EvTerm] -> VarSet
 evVarsOfTerms = mapUnionVarSet evVarsOfTerm
 
-evVarsOfCallStack :: EvCallStack -> VarSet
-evVarsOfCallStack cs = case cs of
-  EvCsEmpty -> emptyVarSet
-  EvCsTop _ _ tm -> evVarsOfTerm tm
-  EvCsPushCall _ _ tm -> evVarsOfTerm tm
-
 evVarsOfTypeable :: EvTypeable -> VarSet
 evVarsOfTypeable ev =
   case ev of
-    EvTypeableTyCon _ _    -> emptyVarSet
-    EvTypeableTyApp e1 e2  -> evVarsOfTerms (map fst [e1,e2])
-    EvTypeableTyLit e      -> evVarsOfTerm (fst e)
+    EvTypeableTyCon _ e   -> mapUnionVarSet evVarsOfTerm e
+    EvTypeableTyApp e1 e2 -> evVarsOfTerms [e1,e2]
+    EvTypeableTrFun e1 e2 -> evVarsOfTerms [e1,e2]
+    EvTypeableTyLit e     -> evVarsOfTerm e
+
+-- | Do SCC analysis on a bag of 'EvBind's.
+sccEvBinds :: Bag EvBind -> [SCC EvBind]
+sccEvBinds bs = stronglyConnCompFromEdgedVerticesUniq edges
+  where
+    edges :: [ Node EvVar EvBind ]
+    edges = foldrBag ((:) . mk_node) [] bs
+
+    mk_node :: EvBind -> Node EvVar EvBind
+    mk_node b@(EvBind { eb_lhs = var, eb_rhs = term })
+      = DigraphNode b var (nonDetEltsUniqSet (evVarsOfTerm term `unionVarSet`
+                                coVarsOfType (varType var)))
+      -- It's OK to use nonDetEltsUniqSet here as stronglyConnCompFromEdgedVertices
+      -- is still deterministic even if the edges are in nondeterministic order
+      -- as explained in Note [Deterministic SCC] in Digraph.
 
 {-
 ************************************************************************
@@ -1036,42 +831,51 @@ evVarsOfTypeable ev =
 -}
 
 instance Outputable HsWrapper where
-  ppr co_fn = pprHsWrapper (ptext (sLit "<>")) co_fn
-
-pprHsWrapper :: SDoc -> HsWrapper -> SDoc
--- In debug mode, print the wrapper
--- otherwise just print what's inside
-pprHsWrapper doc wrap
-  = getPprStyle (\ s -> if debugStyle s then (help (add_parens doc) wrap False) else doc)
+  ppr co_fn = pprHsWrapper co_fn (no_parens (text "<>"))
+
+pprHsWrapper :: HsWrapper -> (Bool -> SDoc) -> SDoc
+-- With -fprint-typechecker-elaboration, print the wrapper
+--   otherwise just print what's inside
+-- The pp_thing_inside function takes Bool to say whether
+--    it's in a position that needs parens for a non-atomic thing
+pprHsWrapper wrap pp_thing_inside
+  = sdocWithDynFlags $ \ dflags ->
+    if gopt Opt_PrintTypecheckerElaboration dflags
+    then help pp_thing_inside wrap False
+    else pp_thing_inside False
   where
     help :: (Bool -> SDoc) -> HsWrapper -> Bool -> SDoc
     -- True  <=> appears in function application position
     -- False <=> appears as body of let or lambda
     help it WpHole             = it
     help it (WpCompose f1 f2)  = help (help it f2) f1
-    help it (WpFun f1 f2 t1 _) = add_parens $ ptext (sLit "\\(x") <> dcolon <> ppr t1 <> ptext (sLit ").") <+>
-                                              help (\_ -> it True <+> help (\_ -> ptext (sLit "x")) f1 True) f2 False
-    help it (WpCast co)   = add_parens $ sep [it False, nest 2 (ptext (sLit "|>")
-                                              <+> pprParendTcCo co)]
-    help it (WpEvApp id)    = no_parens  $ sep [it True, nest 2 (ppr id)]
-    help it (WpTyApp ty)    = no_parens  $ sep [it True, ptext (sLit "@") <+> pprParendType ty]
-    help it (WpEvLam id)    = add_parens $ sep [ ptext (sLit "\\") <> pp_bndr id, it False]
-    help it (WpTyLam tv)    = add_parens $ sep [ptext (sLit "/\\") <> pp_bndr tv, it False]
-    help it (WpLet binds)   = add_parens $ sep [ptext (sLit "let") <+> braces (ppr binds), it False]
+    help it (WpFun f1 f2 t1 _) = add_parens $ text "\\(x" <> dcolon <> ppr t1 <> text ")." <+>
+                                              help (\_ -> it True <+> help (\_ -> text "x") f1 True) f2 False
+    help it (WpCast co)   = add_parens $ sep [it False, nest 2 (text "|>"
+                                              <+> pprParendCo co)]
+    help it (WpEvApp id)  = no_parens  $ sep [it True, nest 2 (ppr id)]
+    help it (WpTyApp ty)  = no_parens  $ sep [it True, text "@" <+> pprParendType ty]
+    help it (WpEvLam id)  = add_parens $ sep [ text "\\" <> pp_bndr id, it False]
+    help it (WpTyLam tv)  = add_parens $ sep [text "/\\" <> pp_bndr tv, it False]
+    help it (WpLet binds) = add_parens $ sep [text "let" <+> braces (ppr binds), it False]
 
     pp_bndr v = pprBndr LambdaBind v <> dot
 
-    add_parens, no_parens :: SDoc -> Bool -> SDoc
-    add_parens d True  = parens d
-    add_parens d False = d
-    no_parens d _ = d
+add_parens, no_parens :: SDoc -> Bool -> SDoc
+add_parens d True  = parens d
+add_parens d False = d
+no_parens d _ = d
 
 instance Outputable TcEvBinds where
   ppr (TcEvBinds v) = ppr v
-  ppr (EvBinds bs)  = ptext (sLit "EvBinds") <> braces (vcat (map ppr (bagToList bs)))
+  ppr (EvBinds bs)  = text "EvBinds" <> braces (vcat (map ppr (bagToList bs)))
 
 instance Outputable EvBindsVar where
-  ppr (EvBindsVar _ u) = ptext (sLit "EvBindsVar") <> angleBrackets (ppr u)
+  ppr (EvBindsVar { ebv_uniq = u })
+     = text "EvBindsVar" <> angleBrackets (ppr u)
+
+instance Uniquable EvBindsVar where
+  getUnique (EvBindsVar { ebv_uniq = u }) = u
 
 instance Outputable EvBind where
   ppr (EvBind { eb_lhs = v, eb_rhs = e, eb_is_given = is_given })
@@ -1082,48 +886,36 @@ instance Outputable EvBind where
    -- We cheat a bit and pretend EqVars are CoVars for the purposes of pretty printing
 
 instance Outputable EvTerm where
-  ppr (EvId v)              = ppr v
-  ppr (EvCast v co)         = ppr v <+> (ptext (sLit "`cast`")) <+> pprParendTcCo co
-  ppr (EvCoercion co)       = ptext (sLit "CO") <+> ppr co
-  ppr (EvSuperClass d n)    = ptext (sLit "sc") <> parens (ppr (d,n))
-  ppr (EvDFunApp df tys ts) = ppr df <+> sep [ char '@' <> ppr tys, ppr ts ]
-  ppr (EvLit l)             = ppr l
-  ppr (EvCallStack cs)      = ppr cs
-  ppr (EvDelayedError ty msg) =     ptext (sLit "error")
-                                <+> sep [ char '@' <> ppr ty, ppr msg ]
-  ppr (EvTypeable ev)    = ppr ev
-
-instance Outputable EvLit where
-  ppr (EvNum n) = integer n
-  ppr (EvStr s) = text (show s)
+  ppr (EvExpr e)         = ppr e
+  ppr (EvTypeable ty ev) = ppr ev <+> dcolon <+> text "Typeable" <+> ppr ty
 
 instance Outputable EvCallStack where
   ppr EvCsEmpty
-    = ptext (sLit "[]")
-  ppr (EvCsTop name loc tm)
-    = angleBrackets (ppr (name,loc)) <+> ptext (sLit ":") <+> ppr tm
+    = text "[]"
   ppr (EvCsPushCall name loc tm)
-    = angleBrackets (ppr (name,loc)) <+> ptext (sLit ":") <+> ppr tm
+    = ppr (name,loc) <+> text ":" <+> ppr tm
 
 instance Outputable EvTypeable where
-  ppr ev =
-    case ev of
-      EvTypeableTyCon tc ks    -> parens (ppr tc <+> sep (map ppr ks))
-      EvTypeableTyApp t1 t2    -> parens (ppr (fst t1) <+> ppr (fst t2))
-      EvTypeableTyLit x        -> ppr (fst x)
+  ppr (EvTypeableTyCon ts _)  = text "TyCon" <+> ppr ts
+  ppr (EvTypeableTyApp t1 t2) = parens (ppr t1 <+> ppr t2)
+  ppr (EvTypeableTrFun t1 t2) = parens (ppr t1 <+> arrow <+> ppr t2)
+  ppr (EvTypeableTyLit t1)    = text "TyLit" <> ppr t1
 
 
 ----------------------------------------------------------------------
 -- Helper functions for dealing with IP newtype-dictionaries
 ----------------------------------------------------------------------
 
--- | Create a 'Coercion' that unwraps an implicit-parameter dictionary
--- to expose the underlying value. We expect the 'Type' to have the form
--- `IP sym ty`, return a 'Coercion' `co :: IP sym ty ~ ty`.
-unwrapIP :: Type -> Coercion
+-- | Create a 'Coercion' that unwraps an implicit-parameter or
+-- overloaded-label dictionary to expose the underlying value. We
+-- expect the 'Type' to have the form `IP sym ty` or `IsLabel sym ty`,
+-- and return a 'Coercion' `co :: IP sym ty ~ ty` or
+-- `co :: IsLabel sym ty ~ Proxy# sym -> ty`.  See also
+-- Note [Type-checking overloaded labels] in TcExpr.
+unwrapIP :: Type -> CoercionR
 unwrapIP ty =
   case unwrapNewTyCon_maybe tc of
-    Just (_,_,ax) -> mkUnbranchedAxInstCo Representational ax tys
+    Just (_,_,ax) -> mkUnbranchedAxInstCo Representational ax tys []
     Nothing       -> pprPanic "unwrapIP" $
                        text "The dictionary for" <+> quotes (ppr tc)
                          <+> text "is not a newtype!"
@@ -1132,5 +924,5 @@ unwrapIP ty =
 
 -- | Create a 'Coercion' that wraps a value in an implicit-parameter
 -- dictionary. See 'unwrapIP'.
-wrapIP :: Type -> Coercion
+wrapIP :: Type -> CoercionR
 wrapIP ty = mkSymCo (unwrapIP ty)