Add valid refinement substitution suggestions for typed holes
[ghc.git] / compiler / typecheck / TcEvidence.hs
index f54ff57..0930d7a 100644 (file)
@@ -7,17 +7,23 @@ module TcEvidence (
   -- HsWrapper
   HsWrapper(..),
   (<.>), mkWpTyApps, mkWpEvApps, mkWpEvVarApps, mkWpTyLams,
-  mkWpLams, mkWpLet, mkWpCastN, mkWpCastR,
+  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,
   sccEvBinds, evBindVar,
-  EvTerm(..), mkEvCast, evVarsOfTerm, mkEvScSelectors,
-  EvLit(..), evTermCoercion,
+
+  -- EvTerm (already a CoreExpr)
+  EvTerm(..), EvExpr,
+  evId, evCoercion, evCast, evDFunApp,  evSelector,
+  mkEvCast, evVarsOfTerm, mkEvScSelectors, evTypeable, findNeededEvVars,
+
+  evTermCoercion,
   EvCallStack(..),
   EvTypeable(..),
 
@@ -33,12 +39,14 @@ module TcEvidence (
   mkTcKindCo,
   tcCoercionKind, coVarsOfTcCo,
   mkTcCoVarCo,
-  isTcReflCo,
+  isTcReflCo, isTcReflexiveCo,
   tcCoercionRole,
   unwrapIP, wrapIP
   ) where
 #include "HsVersions.h"
 
+import GhcPrelude
+
 import Var
 import CoAxiom
 import Coercion
@@ -54,15 +62,19 @@ import VarSet
 import Name
 import Pair
 
+import CoreSyn
+import Class ( classSCSelId )
+import Id ( isEvVar )
+import CoreFVs ( exprSomeFreeVars )
+
 import Util
 import Bag
 import Digraph
 import qualified Data.Data as Data
 import Outputable
-import FastString
 import SrcLoc
 import Data.IORef( IORef )
-import UniqFM
+import UniqSet
 
 {-
 Note [TcCoercions]
@@ -80,8 +92,8 @@ kosher free variables.
 -}
 
 type TcCoercion  = Coercion
-type TcCoercionN = CoercionN    -- A Nominal          corecion ~N
-type TcCoercionR = CoercionR    -- A Representational corecion ~R
+type TcCoercionN = CoercionN    -- A Nominal          coercion ~N
+type TcCoercionR = CoercionR    -- A Representational coercion ~R
 type TcCoercionP = CoercionP    -- a phantom coercion
 
 mkTcReflCo             :: Role -> TcType -> TcCoercion
@@ -115,6 +127,10 @@ 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
@@ -143,7 +159,7 @@ tcCoercionKind         = coercionKind
 tcCoercionRole         = coercionRole
 coVarsOfTcCo           = coVarsOfCo
 isTcReflCo             = isReflCo
-
+isTcReflexiveCo        = isReflexiveCo
 
 {-
 %************************************************************************
@@ -162,7 +178,7 @@ data HsWrapper
        -- Hence  (\a. []) `WpCompose` (\b. []) = (\a b. [])
        -- But    ([] a)   `WpCompose` ([] b)   = ([] b a)
 
-  | WpFun HsWrapper HsWrapper TcType
+  | 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
@@ -170,6 +186,9 @@ data HsWrapper
        -- 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 TcCoercionR        -- A cast:  [] `cast` co
                               -- Guaranteed not the identity coercion
@@ -186,8 +205,67 @@ data HsWrapper
 
   | WpLet TcEvBinds             -- Non-empty (or possibly non-empty) evidence bindings,
                                 -- so that the identity coercion is always exactly WpHole
-  deriving Data.Data
 
+-- 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
@@ -198,12 +276,13 @@ 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 _  = WpFun co1 co2 t1
+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'@,
@@ -211,13 +290,14 @@ mkWpFun co1          co2          t1 _  = WpFun co1 co2 t1
 -- 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.
-mkWpFuns :: [(TcType, HsWrapper)] -> TcType -> HsWrapper -> HsWrapper
-mkWpFuns args res_ty res_wrap = snd $ go args res_ty res_wrap
+-- 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)
+        (arg_ty `mkFunTy` tail_ty, mkWpFun arg_wrap tail_wrap arg_ty tail_ty doc)
 
 mkWpCastR :: TcCoercionR -> HsWrapper
 mkWpCastR co
@@ -235,11 +315,11 @@ mkWpCastN co
 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 = mk_co_app_fn WpEvApp (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
@@ -267,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)
+
 {-
 ************************************************************************
 *                                                                      *
@@ -283,8 +380,26 @@ data TcEvBinds
   | EvBinds             -- Immutable after zonking
        (Bag EvBind)
 
-data EvBindsVar = EvBindsVar (IORef EvBindMap) Unique
-     -- The Unique is for debug printing only
+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
@@ -325,6 +440,9 @@ extendEvBinds bs ev_bind
                                                (eb_lhs ev_bind)
                                                ev_bind }
 
+isEmptyEvBindMap :: EvBindMap -> Bool
+isEmptyEvBindMap (EvBindMap m) = isEmptyDVarEnv m
+
 lookupEvBind :: EvBindMap -> EvVar -> Maybe EvBind
 lookupEvBind bs = lookupDVarEnv (ev_bind_varenv bs)
 
@@ -334,6 +452,13 @@ evBindMapBinds = foldEvBindMap consBag emptyBag
 foldEvBindMap :: (EvBind -> a -> a) -> a -> EvBindMap -> a
 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
 data EvBind
@@ -349,67 +474,83 @@ evBindVar = eb_lhs
 mkWantedEvBind :: EvVar -> EvTerm -> EvBind
 mkWantedEvBind ev tm = EvBind { eb_is_given = False, 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 }
 
-mkGivenEvBind :: EvVar -> EvTerm -> EvBind
-mkGivenEvBind ev tm = EvBind { eb_is_given = True, eb_lhs = ev, eb_rhs = tm }
 
+-- 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
-  = EvId EvId                    -- Any sort of evidence Id, including coercions
-
-  | EvCoercion TcCoercion        -- coercion bindings
-                                 -- See Note [Coercion evidence terms]
+    = EvExpr EvExpr
+    | EvTypeable Type EvTypeable   -- Dictionary for (Typeable ty)
+  deriving Data.Data
 
-  | EvCast EvTerm TcCoercionR    -- d |> co
+type EvExpr = CoreExpr
 
-  | EvDFunApp DFunId             -- Dictionary instance application
-       [Type] [EvTerm]
+-- 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 Type EvTypeable   -- Dictionary for (Typeable ty)
+-- 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
 
+-- 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 [EvTerm]  -- ^ Dictionary for @Typeable (T k1..kn)@.
-                              -- The EvTerms are for the arguments
+  = 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@
+    -- 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
 
-data EvLit
-  = EvNum Integer
-  | EvStr FastString
-    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@.
   deriving Data.Data
@@ -471,54 +612,6 @@ 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:
-
-  instance KnownNat 0       where natSing = SNat 0
-  instance KnownNat 1       where natSing = SNat 1
-  instance KnownNat 2       where natSing = SNat 2
-  ...
-
-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)`.
-
-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.
-
-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.
-
-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`:
-
-  natVal :: KnownNat n => proxy n -> Integer
-
-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,
-especially when the `KnowNat` evidence is packaged up in an existential.
-
-The story for kind `Symbol` is analogous:
-  * class KnownSymbol
-  * newtype SSymbol
-  * Evidence: EvLit (EvStr n)
-
-
 Note [Overview of implicit CallStacks]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 (See https://ghc.haskell.org/trac/ghc/wiki/ExplicitCallStack/ImplicitLocations)
@@ -643,17 +736,19 @@ Important Details:
 
 -}
 
-mkEvCast :: EvTerm -> TcCoercion -> EvTerm
+mkEvCast :: EvExpr -> TcCoercion -> EvExpr
 mkEvCast ev 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
@@ -662,56 +757,71 @@ 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)        = mkCoVarCo v
-evTermCoercion (EvCoercion co) = co
-evTermCoercion (EvCast tm co)  = mkCoCast (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)      = coVarsOfCo co
-evVarsOfTerm (EvDFunApp _ _ evs)  = mapUnionVarSet evVarsOfTerm evs
-evVarsOfTerm (EvSuperClass v _)   = evVarsOfTerm v
-evVarsOfTerm (EvCast tm co)       = evVarsOfTerm tm `unionVarSet` coVarsOfCo 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
 
+evVarsOfTypeable :: EvTypeable -> VarSet
+evVarsOfTypeable ev =
+  case ev of
+    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 = stronglyConnCompFromEdgedVertices edges
+sccEvBinds bs = stronglyConnCompFromEdgedVerticesUniq edges
   where
-    edges :: [(EvBind, EvVar, [EvVar])]
+    edges :: [ Node EvVar EvBind ]
     edges = foldrBag ((:) . mk_node) [] bs
 
-    mk_node :: EvBind -> (EvBind, EvVar, [EvVar])
+    mk_node :: EvBind -> Node EvVar EvBind
     mk_node b@(EvBind { eb_lhs = var, eb_rhs = term })
-      = (b, var, nonDetEltsUFM (evVarsOfTerm term `unionVarSet`
+      = DigraphNode b var (nonDetEltsUniqSet (evVarsOfTerm term `unionVarSet`
                                 coVarsOfType (varType var)))
-      -- It's OK to use nonDetEltsUFM here as stronglyConnCompFromEdgedVertices
+      -- 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.
 
-evVarsOfCallStack :: EvCallStack -> VarSet
-evVarsOfCallStack cs = case cs of
-  EvCsEmpty -> emptyVarSet
-  EvCsPushCall _ _ tm -> evVarsOfTerm tm
-
-evVarsOfTypeable :: EvTypeable -> VarSet
-evVarsOfTypeable ev =
-  case ev of
-    EvTypeableTyCon es    -> evVarsOfTerms es
-    EvTypeableTyApp e1 e2 -> evVarsOfTerms [e1,e2]
-    EvTypeableTyLit e     -> evVarsOfTerm e
-
 {-
 ************************************************************************
 *                                                                      *
@@ -723,7 +833,7 @@ evVarsOfTypeable ev =
 instance Outputable HsWrapper where
   ppr co_fn = pprHsWrapper co_fn (no_parens (text "<>"))
 
-pprHsWrapper ::HsWrapper ->  (Bool -> SDoc) -> SDoc
+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
@@ -739,7 +849,7 @@ pprHsWrapper wrap pp_thing_inside
     -- 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 $ text "\\(x" <> dcolon <> ppr t1 <> text ")." <+>
+    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)]
@@ -761,10 +871,11 @@ instance Outputable TcEvBinds where
   ppr (EvBinds bs)  = text "EvBinds" <> braces (vcat (map ppr (bagToList bs)))
 
 instance Outputable EvBindsVar where
-  ppr (EvBindsVar _ u) = text "EvBindsVar" <> angleBrackets (ppr u)
+  ppr (EvBindsVar { ebv_uniq = u })
+     = text "EvBindsVar" <> angleBrackets (ppr u)
 
 instance Uniquable EvBindsVar where
-  getUnique (EvBindsVar _ u) = u
+  getUnique (EvBindsVar { ebv_uniq = u }) = u
 
 instance Outputable EvBind where
   ppr (EvBind { eb_lhs = v, eb_rhs = e, eb_is_given = is_given })
@@ -775,20 +886,8 @@ 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 <+> (text "`cast`") <+> pprParendCo co
-  ppr (EvCoercion co)       = text "CO" <+> ppr co
-  ppr (EvSuperClass d n)    = text "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) =     text "error"
-                                <+> sep [ char '@' <> ppr ty, ppr msg ]
-  ppr (EvTypeable ty ev)      = ppr ev <+> dcolon <+> text "Typeable" <+> ppr ty
-
-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
@@ -797,8 +896,9 @@ instance Outputable EvCallStack where
     = ppr (name,loc) <+> text ":" <+> ppr tm
 
 instance Outputable EvTypeable where
-  ppr (EvTypeableTyCon ts)    = text "TC" <+> ppr ts
+  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