Trying to add EvTypeable back to to EvTerm (checkpoint)

but without the other constructors.

This is trying to include an EvCallStack constructor, but it turns out
that `solveCallStack` in `TcCanonical` tries to wrap that in an
`mkEvCast`. So lets defer this casting until the desugarer runs.

16 files changed, 262 insertions, 274 deletions

diff --git a/compiler/deSugar/DsBinds.hs b/compiler/deSugar/DsBinds.hs
index f8becffe10..c093f210d2 100644
--- a/compiler/deSugar/DsBinds.hs
+++ b/compiler/deSugar/DsBinds.hs
@@ -30,7 +30,6 @@ import DsUtils
 
 import HsSyn            -- lots of things
 import CoreSyn          -- lots of things
-import Literal          ( Literal(MachStr) )
 import CoreOpt          ( simpleOptExpr )
 import OccurAnal        ( occurAnalyseExpr )
 import MkCore
@@ -49,7 +48,6 @@ import Coercion
 import TysWiredIn ( typeNatKind, typeSymbolKind )
 import Id
 import MkId(proxyHashId)
-import Class
 import Name
 import VarSet
 import Rules
@@ -1156,42 +1154,9 @@ dsEvBind (EvBind { eb_lhs = v, eb_rhs = r}) = liftM ((,) v) (dsEvTerm r)
 **********************************************************************-}
 
 dsEvTerm :: EvTerm -> DsM CoreExpr
-dsEvTerm (EvId v)           = return (Var v)
-dsEvTerm (EvCallStack cs)   = dsEvCallStack cs
-dsEvTerm (EvTypeable ty ev) = dsEvTypeable ty ev
-dsEvTerm (EvLit (EvNum n))  = mkNaturalExpr n
-dsEvTerm (EvLit (EvStr s))  = mkStringExprFS s
-
-dsEvTerm (EvCast tm co)
-  = do { tm' <- dsEvTerm tm
-       ; return $ mkCastDs tm' co }
-
-dsEvTerm (EvDFunApp df tys tms)
-  = do { tms' <- mapM dsEvTerm tms
-       ; return $ Var df `mkTyApps` tys `mkApps` tms' }
-  -- The use of mkApps here is OK vis-a-vis levity polymorphism because
-  -- the terms are always evidence variables with types of kind Constraint
-
-dsEvTerm (EvCoercion co) = return (Coercion co)
-dsEvTerm (EvSuperClass d n)
-  = do { d' <- dsEvTerm d
-       ; let (cls, tys) = getClassPredTys (exprType d')
-             sc_sel_id  = classSCSelId cls n    -- Zero-indexed
-       ; return $ Var sc_sel_id `mkTyApps` tys `App` d' }
-
-dsEvTerm (EvSelector sel_id tys tms)
-  = do { tms' <- mapM dsEvTerm tms
-       ; return $ Var sel_id `mkTyApps` tys `mkApps` tms' }
-
-dsEvTerm (EvDelayedError ty msg) = return $ dsEvDelayedError ty msg
-dsEvTerm (EvExpr e)         = return e
-
-dsEvDelayedError :: Type -> FastString -> CoreExpr
-dsEvDelayedError ty msg
-  = Var errorId `mkTyApps` [getRuntimeRep ty, ty] `mkApps` [litMsg]
-  where
-    errorId = tYPE_ERROR_ID
-    litMsg  = Lit (MachStr (fastStringToByteString msg))
+dsEvTerm (EvExpr e)          = return e
+dsEvTerm (EvCallStack ty cs) = dsEvCallStack ty cs
+dsEvTerm (EvTypeable ty ev)  = dsEvTypeable ty ev
 
 {-**********************************************************************
 *                                                                      *
@@ -1320,9 +1285,9 @@ tyConRep tc
 *                                                                      *
 **********************************************************************-}
 
-dsEvCallStack :: EvCallStack -> DsM CoreExpr
+dsEvCallStack :: PredType -> EvCallStack -> DsM CoreExpr
 -- See Note [Overview of implicit CallStacks] in TcEvidence.hs
-dsEvCallStack cs = do
+dsEvCallStack ty cs = do
   df            <- getDynFlags
   m             <- getModule
   srcLocDataCon <- dsLookupDataCon srcLocDataConName
@@ -1347,7 +1312,7 @@ dsEvCallStack cs = do
         nameExpr <- mkStringExprFS name
         locExpr <- mkSrcLoc loc
         case tm of
-          EvCallStack EvCsEmpty -> return (pushCS nameExpr locExpr emptyCS)
+          EvCallStack _ EvCsEmpty -> return (pushCS nameExpr locExpr emptyCS)
           _ -> do tmExpr  <- dsEvTerm tm
                   -- at this point tmExpr :: IP sym CallStack
                   -- but we need the actual CallStack to pass to pushCS,
@@ -1355,6 +1320,7 @@ dsEvCallStack cs = do
                   -- See Note [Overview of implicit CallStacks]
                   let ip_co = unwrapIP (exprType tmExpr)
                   return (pushCS nameExpr locExpr (mkCastDs tmExpr ip_co))
-  case cs of
+  cs_expr <- case cs of
     EvCsPushCall name loc tm -> mkPush (occNameFS $ getOccName name) loc tm
     EvCsEmpty -> return emptyCS
+  return $ Cast cs_expr (wrapIP ty)
diff --git a/compiler/deSugar/Match.hs b/compiler/deSugar/Match.hs
index 7a3ee6853c..5f9f8dca8b 100644
--- a/compiler/deSugar/Match.hs
+++ b/compiler/deSugar/Match.hs
@@ -1053,8 +1053,8 @@ viewLExprEq (e1,_) (e2,_) = lexp e1 e2
 
     ---------
     ev_term :: EvTerm -> EvTerm -> Bool
-    ev_term (EvId a)       (EvId b)       = a==b
-    ev_term (EvCoercion a) (EvCoercion b) = a `eqCoercion` b
+    ev_term (EvExpr (Var a)) (EvExpr  (Var b)) = a==b
+    ev_term (EvExpr (Coercion a)) (EvExpr (Coercion b)) = a `eqCoercion` b
     ev_term _ _ = False
 
     ---------
diff --git a/compiler/ghc.cabal.in b/compiler/ghc.cabal.in
index 1e3447b49f..d4387cbab0 100644
--- a/compiler/ghc.cabal.in
+++ b/compiler/ghc.cabal.in
@@ -471,6 +471,7 @@ Library
         TcTypeable
         TcType
         TcEvidence
+        TcEvTerm
         TcUnify
         TcInteract
         TcCanonical
diff --git a/compiler/typecheck/Inst.hs b/compiler/typecheck/Inst.hs
index 9da96c4cc0..a68b80deff 100644
--- a/compiler/typecheck/Inst.hs
+++ b/compiler/typecheck/Inst.hs
@@ -350,18 +350,18 @@ instCallConstraints orig preds
   | otherwise
   = do { evs <- mapM go preds
        ; traceTc "instCallConstraints" (ppr evs)
-       ; return (mkWpEvApps evs) }
+       ; return (mkWpEvApps (map EvExpr evs)) }
   where
     go pred
      | Just (Nominal, ty1, ty2) <- getEqPredTys_maybe pred -- Try short-cut #1
      = do  { co <- unifyType Nothing ty1 ty2
-           ; return (EvCoercion co) }
+           ; return (evCoercion co) }
 
        -- Try short-cut #2
      | Just (tc, args@[_, _, ty1, ty2]) <- splitTyConApp_maybe pred
      , tc `hasKey` heqTyConKey
      = do { co <- unifyType Nothing ty1 ty2
-          ; return (EvDFunApp (dataConWrapId heqDataCon) args [EvCoercion co]) }
+          ; return (evDFunApp (dataConWrapId heqDataCon) args [evCoercion co]) }
 
      | otherwise
      = emitWanted orig pred
diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index 907f31b65a..2ef4d31f80 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -19,6 +19,7 @@ import Type
 import TcFlatten
 import TcSMonad
 import TcEvidence
+import TcEvTerm
 import Class
 import TyCon
 import TyCoRep   -- cleverly decomposes types, good for completeness checking
@@ -152,7 +153,7 @@ canClassNC ev cls tys
 
          -- Then we solve the wanted by pushing the call-site
          -- onto the newly emitted CallStack
-       ; let ev_cs = EvCsPushCall func (ctLocSpan loc) (ctEvTerm new_ev)
+       ; let ev_cs = EvCsPushCall func (ctLocSpan loc) (EvExpr (ctEvTerm new_ev))
        ; solveCallStack ev ev_cs
 
        ; canClass new_ev cls tys False }
@@ -171,8 +172,7 @@ solveCallStack ev ev_cs = do
   -- We're given ev_cs :: CallStack, but the evidence term should be a
   -- dictionary, so we have to coerce ev_cs to a dictionary for
   -- `IP ip CallStack`. See Note [Overview of implicit CallStacks]
-  let ev_tm = mkEvCast (EvCallStack ev_cs) (wrapIP (ctEvPred ev))
-  setWantedEvBind (ctEvEvId ev) ev_tm
+  setWantedEvBind (ctEvEvId ev) (EvCallStack (ctEvPred ev) ev_cs)
 
 canClass :: CtEvidence
          -> Class -> [Type]
@@ -443,7 +443,7 @@ mk_strict_superclasses :: NameSet -> CtEvidence -> Class -> [Type] -> TcS [Ct]
 mk_strict_superclasses rec_clss ev cls tys
   | CtGiven { ctev_evar = evar, ctev_loc = loc } <- ev
   = do { sc_evs <- newGivenEvVars (mk_given_loc loc)
-                                  (mkEvScSelectors (EvId evar) cls tys)
+                                  (mkEvScSelectors (evId evar) cls tys)
        ; concatMapM (mk_superclasses rec_clss) sc_evs }
 
   | all noFreeVarsOfType tys
@@ -992,9 +992,9 @@ can_eq_app ev NomEq s1 t1 s2 t2
              co_s = mkTcLRCo CLeft  co
              co_t = mkTcLRCo CRight co
        ; evar_s <- newGivenEvVar loc ( mkTcEqPredLikeEv ev s1 s2
-                                     , EvCoercion co_s )
+                                     , EvExpr $ evCoercion co_s )
        ; evar_t <- newGivenEvVar loc ( mkTcEqPredLikeEv ev t1 t2
-                                     , EvCoercion co_t )
+                                     , EvExpr $ evCoercion co_t )
        ; emitWorkNC [evar_t]
        ; canEqNC evar_s NomEq s1 s2 }
   | otherwise  -- Can't happen
@@ -1264,7 +1264,7 @@ canDecomposableTyConAppOK ev eq_rel tc tys1 tys2
         -> do { let ev_co = mkCoVarCo evar
               ; given_evs <- newGivenEvVars loc $
                              [ ( mkPrimEqPredRole r ty1 ty2
-                               , EvCoercion (mkNthCo i ev_co) )
+                               , EvExpr $ evCoercion $ mkNthCo i ev_co )
                              | (r, ty1, ty2, i) <- zip4 tc_roles tys1 tys2 [0..]
                              , r /= Phantom
                              , not (isCoercionTy ty1) && not (isCoercionTy ty2) ]
@@ -1459,7 +1459,7 @@ canEqTyVar ev eq_rel swapped tv1 co1 ps_ty1 xi2 ps_xi2
     -- unswapped: tm :: (lhs :: k1) ~ (rhs :: k2)
     -- swapped  : tm :: (rhs :: k2) ~ (lhs :: k1)
   = do { kind_ev_id <- newBoundEvVarId kind_pty
-                                       (EvCoercion $
+                                       (EvExpr $ evCoercion $
                                         if isSwapped swapped
                                         then mkTcSymCo $ mkTcKindCo $ mkTcCoVarCo evar
                                         else             mkTcKindCo $ mkTcCoVarCo evar)
@@ -1476,10 +1476,10 @@ canEqTyVar ev eq_rel swapped tv1 co1 ps_ty1 xi2 ps_xi2
        ; type_ev <- newGivenEvVar loc $
                     if isSwapped swapped
                     then ( mkTcEqPredLikeEv ev rhs' lhs
-                         , EvCoercion $
+                         , EvExpr $ evCoercion $
                            mkTcCoherenceLeftCo (mkTcCoVarCo evar) homo_co )
                     else ( mkTcEqPredLikeEv ev lhs rhs'
-                         , EvCoercion $
+                         , EvExpr $ evCoercion $
                            mkTcCoherenceRightCo (mkTcCoVarCo evar) homo_co )
           -- unswapped: type_ev :: (lhs :: k1) ~ ((rhs |> sym kind_ev_id) :: k1)
           -- swapped  : type_ev :: ((rhs |> sym kind_ev_id) :: k1) ~ (lhs :: k1)
@@ -1589,7 +1589,7 @@ canEqReflexive :: CtEvidence    -- ty ~ ty
                -> TcType        -- ty
                -> TcS (StopOrContinue Ct)   -- always Stop
 canEqReflexive ev eq_rel ty
-  = do { setEvBindIfWanted ev (EvCoercion $
+  = do { setEvBindIfWanted ev (EvExpr $ evCoercion $
                                mkTcReflCo (eqRelRole eq_rel) ty)
        ; stopWith ev "Solved by reflexivity" }
 
@@ -1852,11 +1852,11 @@ rewriteEvidence old_ev new_pred co
   = continueWith (old_ev { ctev_pred = new_pred })
 
 rewriteEvidence ev@(CtGiven { ctev_evar = old_evar, ctev_loc = loc }) new_pred co
-  = do { new_ev <- newGivenEvVar loc (new_pred, new_tm)
+  = do { new_ev <- newGivenEvVar loc (new_pred, (EvExpr new_tm))
        ; continueWith new_ev }
   where
     -- mkEvCast optimises ReflCo
-    new_tm = mkEvCast (EvId old_evar) (tcDowngradeRole Representational
+    new_tm = mkEvCast (evId old_evar) (tcDowngradeRole Representational
                                                        (ctEvRole ev)
                                                        (mkTcSymCo co))
 
@@ -1865,8 +1865,8 @@ rewriteEvidence ev@(CtWanted { ctev_dest = dest
   = do { mb_new_ev <- newWanted loc new_pred
        ; MASSERT( tcCoercionRole co == ctEvRole ev )
        ; setWantedEvTerm dest
-                   (mkEvCast (getEvTerm mb_new_ev)
-                             (tcDowngradeRole Representational (ctEvRole ev) co))
+            (EvExpr (mkEvCast (getEvExpr mb_new_ev)
+                              (tcDowngradeRole Representational (ctEvRole ev) co)))
        ; case mb_new_ev of
             Fresh  new_ev -> continueWith new_ev
             Cached _      -> stopWith ev "Cached wanted" }
@@ -1905,10 +1905,10 @@ rewriteEqEvidence old_ev swapped nlhs nrhs lhs_co rhs_co
   = continueWith (old_ev { ctev_pred = new_pred })
 
   | CtGiven { ctev_evar = old_evar } <- old_ev
-  = do { let new_tm = EvCoercion (lhs_co
+  = do { let new_tm = evCoercion (lhs_co
                                   `mkTcTransCo` maybeSym swapped (mkTcCoVarCo old_evar)
                                   `mkTcTransCo` mkTcSymCo rhs_co)
-       ; new_ev <- newGivenEvVar loc' (new_pred, new_tm)
+       ; new_ev <- newGivenEvVar loc' (new_pred, EvExpr new_tm)
        ; continueWith new_ev }
 
   | CtWanted { ctev_dest = dest } <- old_ev
diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs
index 1c7d643bc1..2f8f4cf379 100644
--- a/compiler/typecheck/TcErrors.hs
+++ b/compiler/typecheck/TcErrors.hs
@@ -31,6 +31,7 @@ import TyCon
 import Class
 import DataCon
 import TcEvidence
+import TcEvTerm
 import HsExpr  ( UnboundVar(..) )
 import HsBinds ( PatSynBind(..) )
 import Name
@@ -806,7 +807,7 @@ addDeferredBinding ctxt err ct
        ; let err_msg = pprLocErrMsg err
              err_fs  = mkFastString $ showSDoc dflags $
                        err_msg $$ text "(deferred type error)"
-             err_tm  = EvDelayedError pred err_fs
+             err_tm  = evDelayedError pred err_fs
              ev_binds_var = cec_binds ctxt
 
        ; case dest of
diff --git a/compiler/typecheck/TcEvTerm.hs b/compiler/typecheck/TcEvTerm.hs
new file mode 100644
index 0000000000..dca3d48978
--- /dev/null
+++ b/compiler/typecheck/TcEvTerm.hs
@@ -0,0 +1,31 @@
+
+-- (those who have too heavy dependencies for TcEvidence)
+module TcEvTerm
+    ( evDelayedError )
+where
+
+import GhcPrelude
+
+import FastString
+import Type
+import CoreSyn
+import MkCore
+import Literal ( Literal(..) )
+import TcEvidence
+import HscTypes
+import DynFlags
+import Name
+import Module
+import CoreUtils
+import PrelNames
+import SrcLoc
+
+-- Used with Opt_DeferTypeErrors
+-- See Note [Deferring coercion errors to runtime]
+-- in TcSimplify
+evDelayedError :: Type -> FastString -> EvTerm
+evDelayedError ty msg
+  = EvExpr $ Var errorId `mkTyApps` [getRuntimeRep ty, ty] `mkApps` [litMsg]
+  where
+    errorId = tYPE_ERROR_ID
+    litMsg  = Lit (MachStr (fastStringToByteString msg))
diff --git a/compiler/typecheck/TcEvidence.hs b/compiler/typecheck/TcEvidence.hs
index 3e7e701d18..8f29de9c0e 100644
--- a/compiler/typecheck/TcEvidence.hs
+++ b/compiler/typecheck/TcEvidence.hs
@@ -1,4 +1,4 @@
-
+-- (c) The University of Glasgow 2006
 
 {-# LANGUAGE CPP, DeriveDataTypeable #-}
 
@@ -17,8 +17,13 @@ module TcEvidence (
   isEmptyEvBindMap,
   EvBind(..), emptyTcEvBinds, isEmptyTcEvBinds, mkGivenEvBind, mkWantedEvBind,
   sccEvBinds, evBindVar,
-  EvTerm(..), mkEvCast, evVarsOfTerm, mkEvScSelectors,
-  EvLit(..), evTermCoercion,
+
+  -- EvTerm (already a CoreExpr)
+  EvTerm(..), EvExpr,
+  evId, evCoercion, evCast, evDFunApp,  evSuperClass, evSelector,
+  mkEvCast, evVarsOfTerm, mkEvScSelectors, evTypeable,
+
+  evTermCoercion,
   EvCallStack(..),
   EvTypeable(..),
 
@@ -58,6 +63,8 @@ import Name
 import Pair
 
 import CoreSyn
+import CoreUtils
+import Class ( classSCSelId )
 import Id ( isEvVar )
 import CoreFVs ( exprSomeFreeVars )
 
@@ -66,7 +73,6 @@ import Bag
 import Digraph
 import qualified Data.Data as Data
 import Outputable
-import FastString
 import SrcLoc
 import Data.IORef( IORef )
 import UniqSet
@@ -314,7 +320,7 @@ mkWpEvApps :: [EvTerm] -> HsWrapper
 mkWpEvApps args = mk_co_app_fn WpEvApp 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
@@ -473,39 +479,62 @@ 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 }
 
-data EvTerm
-  = EvId EvId                    -- Any sort of evidence Id, including coercions
 
-  | EvCoercion TcCoercion        -- coercion bindings
-                                 -- See Note [Coercion evidence terms]
-
-  | EvCast EvTerm TcCoercionR    -- d |> co
-
-  | EvDFunApp DFunId             -- Dictionary instance application
-       [Type] [EvTerm]
+-- 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
+    | EvCallStack TcPredType EvCallStack
+        -- Dictionary for CallStack implicit parameters, toether with the
+        -- Predtype for coercion
+    | EvTypeable Type EvTypeable   -- Dictionary for (Typeable ty)
+  deriving Data.Data
 
-  | EvDelayedError Type FastString  -- Used with Opt_DeferTypeErrors
-                               -- See Note [Deferring coercion errors to runtime]
-                               -- in TcSimplify
+type EvExpr = CoreExpr
 
-  | 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_
+-- An EvTerm is (usually) constructed by any of the constructors here
+-- and those more complicates ones who were moved to module TcEvTerm
 
-  | EvLit EvLit       -- Dictionary for KnownNat and KnownSymbol classes.
-                      -- Note [KnownNat & KnownSymbol and EvLit]
+-- | Any sort of evidence Id, including coercions
+evId ::  EvId -> EvExpr
+evId = Var
 
-  | EvCallStack EvCallStack      -- Dictionary for CallStack implicit parameters
+-- coercion bindings
+-- See Note [Coercion evidence terms]
+evCoercion :: TcCoercion -> EvExpr
+evCoercion = Coercion
+
+-- | d |> co
+evCast :: EvExpr -> TcCoercion -> EvExpr
+evCast et tc | isReflCo tc = et
+             | otherwise   = Cast et tc
+
+-- Dictionary instance application
+evDFunApp :: DFunId -> [Type] -> [EvExpr] -> EvExpr
+evDFunApp df tys ets = Var df `mkTyApps` tys `mkApps` ets
+
+-- n'th superclass. Used for both equalities and
+-- dictionaries, even though the former have no
+-- selector Id.  We count up from _0_
+evSuperClass :: EvExpr -> Int -> EvExpr
+evSuperClass d n = Var sc_sel_id `mkTyApps` tys `App` d
+  where
+    (cls, tys) = getClassPredTys (exprType d)
+    sc_sel_id  = classSCSelId cls n -- Zero-indexed
 
-  | 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
 
-  | EvSelector Id [Type] [EvTerm] -- Selector id plus the types at which it
-                                  -- should be instantiated, used for HasField
-                                  -- dictionaries; see Note [HasField instances]
-                                  -- in TcInterface
-  | EvExpr CoreExpr  -- A arbitrary dictionary, possibly created by a plugin
-  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]
@@ -530,11 +559,6 @@ data EvTypeable
     -- (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]
@@ -601,54 +625,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 infinitely 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)
@@ -773,17 +749,17 @@ 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, EvTerm)]
 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, EvExpr (evSuperClass ev i))
 
 emptyTcEvBinds :: TcEvBinds
 emptyTcEvBinds = EvBinds emptyBag
@@ -792,31 +768,35 @@ 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)
 
 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 (EvSelector _ _ evs) = mapUnionVarSet evVarsOfTerm evs
-evVarsOfTerm (EvExpr e)           = exprSomeFreeVars isEvVar e
+evVarsOfTerm (EvExpr e)         = exprSomeFreeVars isEvVar e
+evVarsOfTerm (EvCallStack _ cs) = evVarsOfCallStack cs
+evVarsOfTerm (EvTypeable _ ev)  = evVarsOfTypeable ev
 
 evVarsOfTerms :: [EvTerm] -> VarSet
 evVarsOfTerms = mapUnionVarSet evVarsOfTerm
 
+evVarsOfCallStack :: EvCallStack -> VarSet
+evVarsOfCallStack cs = case cs of
+  EvCsEmpty -> emptyVarSet
+  EvCsPushCall _ _ tm -> evVarsOfTerm tm
+
+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 = stronglyConnCompFromEdgedVerticesUniq edges
@@ -832,19 +812,6 @@ sccEvBinds bs = stronglyConnCompFromEdgedVerticesUniq edges
       -- 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 _ e   -> mapUnionVarSet evVarsOfTerm e
-    EvTypeableTyApp e1 e2 -> evVarsOfTerms [e1,e2]
-    EvTypeableTrFun e1 e2 -> evVarsOfTerms [e1,e2]
-    EvTypeableTyLit e     -> evVarsOfTerm e
-
 {-
 ************************************************************************
 *                                                                      *
@@ -909,22 +876,9 @@ 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
-  ppr (EvSelector sel tys ts) = ppr sel <+> sep [ char '@' <> ppr tys, ppr ts]
-  ppr (EvExpr e)              = ppr e
-
-instance Outputable EvLit where
-  ppr (EvNum n) = integer n
-  ppr (EvStr s) = text (show s)
+  ppr (EvExpr e)         = ppr e
+  ppr (EvCallStack _ cs) = ppr cs
+  ppr (EvTypeable ty ev) = ppr ev <+> dcolon <+> text "Typeable" <+> ppr ty
 
 instance Outputable EvCallStack where
   ppr EvCsEmpty
diff --git a/compiler/typecheck/TcFlatten.hs b/compiler/typecheck/TcFlatten.hs
index bb7bb06467..5152841db5 100644
--- a/compiler/typecheck/TcFlatten.hs
+++ b/compiler/typecheck/TcFlatten.hs
@@ -1644,7 +1644,7 @@ tryFill ev tv rhs
 
 setReflEvidence :: CtEvidence -> EqRel -> TcType -> TcS ()
 setReflEvidence ev eq_rel rhs
-  = setEvBindIfWanted ev (EvCoercion refl_co)
+  = setEvBindIfWanted ev (EvExpr (evCoercion refl_co))
   where
     refl_co = mkTcReflCo (eqRelRole eq_rel) rhs
 
diff --git a/compiler/typecheck/TcHsSyn.hs b/compiler/typecheck/TcHsSyn.hs
index dccc6ae9d0..43ff2217ee 100644
--- a/compiler/typecheck/TcHsSyn.hs
+++ b/compiler/typecheck/TcHsSyn.hs
@@ -334,12 +334,14 @@ zonkEvBndr env var
            zonkTcTypeToType env var_ty
        ; return (setVarType var ty) }
 
+{-
 zonkEvVarOcc :: ZonkEnv -> EvVar -> TcM EvTerm
 zonkEvVarOcc env v
   | isCoVar v
   = EvCoercion <$> zonkCoVarOcc env v
   | otherwise
   = return (EvId $ zonkIdOcc env v)
+-}
 
 zonkTyBndrsX :: ZonkEnv -> [TcTyVar] -> TcM (ZonkEnv, [TyVar])
 zonkTyBndrsX = mapAccumLM zonkTyBndrX
@@ -1421,36 +1423,8 @@ zonkVect _ (HsVectInstIn _) = panic "TcHsSyn.zonkVect: HsVectInstIn"
 zonkEvTerm :: ZonkEnv -> EvTerm -> TcM EvTerm
 zonkEvTerm env (EvExpr e) =
   EvExpr <$> zonkCoreExpr env e
-zonkEvTerm env (EvId v)           = ASSERT2( isId v, ppr v )
-                                    zonkEvVarOcc env v
-zonkEvTerm env (EvCoercion co)    = do { co' <- zonkCoToCo env co
-                                       ; return (EvCoercion co') }
-zonkEvTerm env (EvCast tm co)     = do { tm' <- zonkEvTerm env tm
-                                       ; co' <- zonkCoToCo env co
-                                       ; return (mkEvCast tm' co') }
-zonkEvTerm _   (EvLit l)          = return (EvLit l)
 zonkEvTerm env (EvTypeable ty ev) =
   EvTypeable <$> zonkTcTypeToType env ty <*> zonkEvTypeable env ev
-zonkEvTerm env (EvCallStack cs)
-  = case cs of
-      EvCsEmpty -> return (EvCallStack cs)
-      EvCsPushCall n l tm -> do { tm' <- zonkEvTerm env tm
-                                ; return (EvCallStack (EvCsPushCall n l tm')) }
-
-zonkEvTerm env (EvSuperClass d n) = do { d' <- zonkEvTerm env d
-                                       ; return (EvSuperClass d' n) }
-zonkEvTerm env (EvDFunApp df tys tms)
-  = do { tys' <- zonkTcTypeToTypes env tys
-       ; tms' <- mapM (zonkEvTerm env) tms
-       ; return (EvDFunApp (zonkIdOcc env df) tys' tms') }
-zonkEvTerm env (EvDelayedError ty msg)
-  = do { ty' <- zonkTcTypeToType env ty
-       ; return (EvDelayedError ty' msg) }
-zonkEvTerm env (EvSelector sel_id tys tms)
-  = do { sel_id' <- zonkIdBndr env sel_id
-       ; tys'    <- zonkTcTypeToTypes env tys
-       ; tms' <- mapM (zonkEvTerm env) tms
-       ; return (EvSelector sel_id' tys' tms') }
 
 zonkCoreExpr :: ZonkEnv -> CoreExpr -> TcM CoreExpr
 zonkCoreExpr env (Var v)
@@ -1567,7 +1541,7 @@ zonkEvBind env bind@(EvBind { eb_lhs = var, eb_rhs = term })
 
        ; term' <- case getEqPredTys_maybe (idType var') of
            Just (r, ty1, ty2) | ty1 `eqType` ty2
-                  -> return (EvCoercion (mkTcReflCo r ty1))
+                  -> return (EvExpr (evCoercion (mkTcReflCo r ty1)))
            _other -> zonkEvTerm env term
 
        ; return (bind { eb_lhs = var', eb_rhs = term' }) }
diff --git a/compiler/typecheck/TcInstDcls.hs b/compiler/typecheck/TcInstDcls.hs
index e5960cb1b1..9f623fc0a5 100644
--- a/compiler/typecheck/TcInstDcls.hs
+++ b/compiler/typecheck/TcInstDcls.hs
@@ -1034,7 +1034,7 @@ tcSuperClasses dfun_id cls tyvars dfun_evs inst_tys dfun_ev_binds sc_theta
 
            ; sc_top_name  <- newName (mkSuperDictAuxOcc n (getOccName cls))
            ; sc_ev_id     <- newEvVar sc_pred
-           ; addTcEvBind ev_binds_var $ mkWantedEvBind sc_ev_id sc_ev_tm
+           ; addTcEvBind ev_binds_var $ mkWantedEvBind sc_ev_id (EvExpr sc_ev_tm)
            ; let sc_top_ty = mkInvForAllTys tyvars (mkLamTypes dfun_evs sc_pred)
                  sc_top_id = mkLocalId sc_top_name sc_top_ty
                  export = ABE { abe_wrap = idHsWrapper
diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs
index bdb11e236c..7b58cc6ad8 100644
--- a/compiler/typecheck/TcInteract.hs
+++ b/compiler/typecheck/TcInteract.hs
@@ -47,6 +47,7 @@ import FamInstEnv
 import Unify ( tcUnifyTyWithTFs )
 
 import TcEvidence
+import MkCore ( mkStringExprFS, mkNaturalExpr )
 import Outputable
 
 import TcRnTypes
@@ -680,9 +681,9 @@ interactIrred inerts workItem@(CIrredCan { cc_ev = ev_w, cc_insol = insoluble })
     do { what_next <- solveOneFromTheOther ev_i ev_w
        ; traceTcS "iteractIrred" (ppr workItem $$ ppr what_next $$ ppr ct_i)
        ; case what_next of
-            KeepInert -> do { setEvBindIfWanted ev_w (swap_me swap ev_i)
+            KeepInert -> do { setEvBindIfWanted ev_w (EvExpr (swap_me swap ev_i))
                             ; return (Stop ev_w (text "Irred equal" <+> parens (ppr what_next))) }
-            KeepWork ->  do { setEvBindIfWanted ev_i (swap_me swap ev_w)
+            KeepWork ->  do { setEvBindIfWanted ev_i (EvExpr (swap_me swap ev_w))
                             ; updInertIrreds (\_ -> others)
                             ; continueWith workItem } }
 
@@ -690,11 +691,11 @@ interactIrred inerts workItem@(CIrredCan { cc_ev = ev_w, cc_insol = insoluble })
   = continueWith workItem
 
   where
-    swap_me :: SwapFlag -> CtEvidence -> EvTerm
+    swap_me :: SwapFlag -> CtEvidence -> EvExpr
     swap_me swap ev
       = case swap of
            NotSwapped -> ctEvTerm ev
-           IsSwapped  -> EvCoercion (mkTcSymCo (evTermCoercion (ctEvTerm ev)))
+           IsSwapped  -> evCoercion (mkTcSymCo (evTermCoercion (EvExpr (ctEvTerm ev))))
 
 interactIrred _ wi = pprPanic "interactIrred" (ppr wi)
 
@@ -1000,9 +1001,9 @@ interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs
              { what_next <- solveOneFromTheOther ev_i ev_w
              ; traceTcS "lookupInertDict" (ppr what_next)
              ; case what_next of
-                 KeepInert -> do { setEvBindIfWanted ev_w (ctEvTerm ev_i)
+                 KeepInert -> do { setEvBindIfWanted ev_w (EvExpr $ ctEvTerm ev_i)
                                  ; return $ Stop ev_w (text "Dict equal" <+> parens (ppr what_next)) }
-                 KeepWork  -> do { setEvBindIfWanted ev_i (ctEvTerm ev_w)
+                 KeepWork  -> do { setEvBindIfWanted ev_i (EvExpr $ ctEvTerm ev_w)
                                  ; updInertDicts $ \ ds -> delDict ds cls tys
                                  ; continueWith workItem } } }
 
@@ -1092,7 +1093,7 @@ shortCutSolver dflags ev_w ev_i
                                   -- so we can solve recursive dictionaries.
                        ; subgoalBinds <- mapM (try_solve_from_instance loc' cache')
                                               (freshGoals evc_vs)
-                       ; return $ (mk_ev (map getEvTerm evc_vs), ev, cls, preds)
+                       ; return $ (mk_ev (map getEvExpr evc_vs), ev, cls, preds)
                                 : concat subgoalBinds }
 
                  | otherwise -> mzero
@@ -1361,7 +1362,7 @@ reactFunEq from_this fsk1 solve_this fsk2
              fsk_eq_pred = mkTcEqPredLikeEv solve_this
                              (mkTyVarTy fsk2) (mkTyVarTy fsk1)
 
-       ; new_ev <- newGivenEvVar loc (fsk_eq_pred, EvCoercion fsk_eq_co)
+       ; new_ev <- newGivenEvVar loc (fsk_eq_pred, EvExpr $ evCoercion fsk_eq_co)
        ; emitWorkNC [new_ev] }
 
   | CtDerived { ctev_loc = loc } <- solve_this
@@ -1549,7 +1550,7 @@ interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv
   | Just (ev_i, swapped, keep_deriv)
        <- inertsCanDischarge inerts tv rhs (ctEvFlavour ev, eq_rel)
   = do { setEvBindIfWanted ev $
-         EvCoercion (maybeSym swapped $
+         EvExpr $ evCoercion (maybeSym swapped $
                      tcDowngradeRole (eqRelRole eq_rel)
                                      (ctEvRole ev_i)
                                      (ctEvCoercion ev_i))
@@ -1615,7 +1616,7 @@ solveByUnification wd tv xi
                              text "Right Kind is:" <+> ppr (typeKind xi) ]
 
        ; unifyTyVar tv xi
-       ; setEvBindIfWanted wd (EvCoercion (mkTcNomReflCo xi)) }
+       ; setEvBindIfWanted wd (EvExpr (evCoercion (mkTcNomReflCo xi))) }
 
 ppr_kicked :: Int -> SDoc
 ppr_kicked 0 = empty
@@ -1825,7 +1826,7 @@ reduce_top_fun_eq old_ev fsk (ax_co, rhs_ty)
   = do { let final_co = mkTcSymCo (ctEvCoercion old_ev) `mkTcTransCo` ax_co
               -- final_co :: fsk ~ rhs_ty
        ; new_ev <- newGivenEvVar deeper_loc (mkPrimEqPred (mkTyVarTy fsk) rhs_ty,
-                                             EvCoercion final_co)
+                                             EvExpr (evCoercion final_co))
        ; emitWorkNC [new_ev] -- Non-cannonical; that will mean we flatten rhs_ty
        ; stopWith old_ev "Fun/Top (given)" }
 
@@ -1948,7 +1949,7 @@ shortCutReduction old_ev fsk ax_co fam_tc tc_args
        ; new_ev <- case ctEvFlavour old_ev of
            Given -> newGivenEvVar deeper_loc
                          ( mkPrimEqPred (mkTyConApp fam_tc xis) (mkTyVarTy fsk)
-                         , EvCoercion (mkTcTyConAppCo Nominal fam_tc cos
+                         , EvExpr $ evCoercion (mkTcTyConAppCo Nominal fam_tc cos
                                         `mkTcTransCo` mkTcSymCo ax_co
                                         `mkTcTransCo` ctEvCoercion old_ev) )
 
@@ -1984,7 +1985,7 @@ dischargeFmv :: CtEvidence -> TcTyVar -> TcCoercion -> TcType -> TcS ()
 -- Does not evaluate 'co' if 'ev' is Derived
 dischargeFmv ev@(CtWanted { ctev_dest = dest }) fmv co xi
   = ASSERT2( not (fmv `elemVarSet` tyCoVarsOfType xi), ppr ev $$ ppr fmv $$ ppr xi )
-    do { setWantedEvTerm dest (EvCoercion co)
+    do { setWantedEvTerm dest (EvExpr (evCoercion co))
        ; unflattenFmv fmv xi
        ; n_kicked <- kickOutAfterUnification fmv
        ; traceTcS "dischargeFmv" (ppr fmv <+> equals <+> ppr xi $$ ppr_kicked n_kicked) }
@@ -2201,7 +2202,7 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls
        ; continueWith work_item }
 
   | Just ev <- lookupSolvedDict inerts dict_loc cls xis   -- Cached
-  = do { setEvBindIfWanted fl (ctEvTerm ev)
+  = do { setEvBindIfWanted fl (EvExpr (ctEvTerm ev))
        ; stopWith fl "Dict/Top (cached)" }
 
   | otherwise  -- Wanted or Derived, but not cached
@@ -2234,12 +2235,12 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls
        = loc
 
      finish_wanted :: [TcPredType]
-                   -> ([EvTerm] -> EvTerm) -> TcS (StopOrContinue Ct)
+                   -> ([EvExpr] -> EvTerm) -> TcS (StopOrContinue Ct)
       -- Precondition: evidence term matches the predicate workItem
      finish_wanted theta mk_ev
         = do { addSolvedDict fl cls xis
              ; evc_vars <- mapM (newWanted deeper_loc) theta
-             ; setWantedEvBind (ctEvEvId fl) (mk_ev (map getEvTerm evc_vars))
+             ; setWantedEvBind (ctEvEvId fl) (mk_ev (map getEvExpr evc_vars))
              ; emitWorkNC (freshGoals evc_vars)
              ; stopWith fl "Dict/Top (solved wanted)" }
 
@@ -2286,7 +2287,7 @@ type SafeOverlapping = Bool
 data LookupInstResult
   = NoInstance
   | GenInst { lir_new_theta :: [TcPredType]
-            , lir_mk_ev     :: [EvTerm] -> EvTerm
+            , lir_mk_ev     :: [EvExpr] -> EvTerm
             , lir_safe_over :: SafeOverlapping }
 
 instance Outputable LookupInstResult where
@@ -2530,7 +2531,7 @@ matchInstEnv dflags short_cut_solver clas tys loc
        = do { checkWellStagedDFun pred dfun_id loc
             ; (tys, theta) <- instDFunType dfun_id mb_inst_tys
             ; return $ GenInst { lir_new_theta = theta
-                               , lir_mk_ev     = EvDFunApp dfun_id tys
+                               , lir_mk_ev     = EvExpr . evDFunApp dfun_id tys
                                , lir_safe_over = so } }
 
 
@@ -2548,7 +2549,7 @@ matchCTuple clas tys   -- (isCTupleClass clas) holds
             -- The dfun *is* the data constructor!
   where
      data_con = tyConSingleDataCon (classTyCon clas)
-     tuple_ev = EvDFunApp (dataConWrapId data_con) tys
+     tuple_ev = EvExpr . evDFunApp (dataConWrapId data_con) tys
 
 {- ********************************************************************
 *                                                                     *
@@ -2556,17 +2557,70 @@ matchCTuple clas tys   -- (isCTupleClass clas) holds
 *                                                                     *
 ***********************************************************************-}
 
+{-
+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 infinitely 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 entire function,
+especially when the `KnowNat` evidence is packaged up in an existential.
+
+The story for kind `Symbol` is analogous:
+  * class KnownSymbol
+  * newtype SSymbol
+  * Evidence: a Core literal (e.g. mkNaturalExpr)
+-}
+
 matchKnownNat :: Class -> [Type] -> TcS LookupInstResult
 matchKnownNat clas [ty]     -- clas = KnownNat
-  | Just n <- isNumLitTy ty = makeLitDict clas ty (EvNum n)
+  | Just n <- isNumLitTy ty = do
+        et <- mkNaturalExpr n
+        makeLitDict clas ty et
 matchKnownNat _ _           = return NoInstance
 
 matchKnownSymbol :: Class -> [Type] -> TcS LookupInstResult
 matchKnownSymbol clas [ty]  -- clas = KnownSymbol
-  | Just n <- isStrLitTy ty = makeLitDict clas ty (EvStr n)
+  | Just s <- isStrLitTy ty = do
+        et <- mkStringExprFS s
+        makeLitDict clas ty et
 matchKnownSymbol _ _       = return NoInstance
 
-makeLitDict :: Class -> Type -> EvLit -> TcS LookupInstResult
+makeLitDict :: Class -> Type -> EvExpr -> TcS LookupInstResult
 -- makeLitDict adds a coercion that will convert the literal into a dictionary
 -- of the appropriate type.  See Note [KnownNat & KnownSymbol and EvLit]
 -- in TcEvidence.  The coercion happens in 2 steps:
@@ -2577,7 +2631,7 @@ makeLitDict :: Class -> Type -> EvLit -> TcS LookupInstResult
 --     The process is mirrored for Symbols:
 --     String    -> SSymbol n
 --     SSymbol n -> KnownSymbol n
-makeLitDict clas ty evLit
+makeLitDict clas ty et
     | Just (_, co_dict) <- tcInstNewTyCon_maybe (classTyCon clas) [ty]
           -- co_dict :: KnownNat n ~ SNat n
     , [ meth ]   <- classMethods clas
@@ -2587,7 +2641,7 @@ makeLitDict clas ty evLit
                       $ idType meth         -- forall n. KnownNat n => SNat n
     , Just (_, co_rep) <- tcInstNewTyCon_maybe tcRep [ty]
           -- SNat n ~ Integer
-    , let ev_tm = mkEvCast (EvLit evLit) (mkTcSymCo (mkTcTransCo co_dict co_rep))
+    , let ev_tm = EvExpr $ mkEvCast et (mkTcSymCo (mkTcTransCo co_dict co_rep))
     = return $ GenInst { lir_new_theta = []
                        , lir_mk_ev     = \_ -> ev_tm
                        , lir_safe_over = True }
@@ -2626,7 +2680,7 @@ doFunTy :: Class -> Type -> Type -> Type -> TcS LookupInstResult
 doFunTy clas ty arg_ty ret_ty
   = do { let preds = map (mk_typeable_pred clas) [arg_ty, ret_ty]
              build_ev [arg_ev, ret_ev] =
-                 EvTypeable ty $ EvTypeableTrFun arg_ev ret_ev
+                 evTypeable ty $ EvTypeableTrFun (EvExpr arg_ev) (EvExpr ret_ev)
              build_ev _ = panic "TcInteract.doFunTy"
        ; return $ GenInst preds build_ev True
        }
@@ -2637,7 +2691,7 @@ doFunTy clas ty arg_ty ret_ty
 doTyConApp :: Class -> Type -> TyCon -> [Kind] -> TcS LookupInstResult
 doTyConApp clas ty tc kind_args
   = return $ GenInst (map (mk_typeable_pred clas) kind_args)
-                     (\kinds -> EvTypeable ty $ EvTypeableTyCon tc kinds)
+                     (\kinds -> evTypeable ty $ EvTypeableTyCon tc (map EvExpr kinds))
                      True
 
 -- | Representation for TyCon applications of a concrete kind. We just use the
@@ -2664,7 +2718,7 @@ doTyApp clas ty f tk
   = return NoInstance -- We can't solve until we know the ctr.
   | otherwise
   = return $ GenInst (map (mk_typeable_pred clas) [f, tk])
-                     (\[t1,t2] -> EvTypeable ty $ EvTypeableTyApp t1 t2)
+                     (\[t1,t2] -> evTypeable ty $ EvTypeableTyApp (EvExpr t1) (EvExpr t2))
                      True
 
 -- Emit a `Typeable` constraint for the given type.
@@ -2677,7 +2731,7 @@ mk_typeable_pred clas ty = mkClassPred clas [ typeKind ty, ty ]
 doTyLit :: Name -> Type -> TcS LookupInstResult
 doTyLit kc t = do { kc_clas <- tcLookupClass kc
                   ; let kc_pred    = mkClassPred kc_clas [ t ]
-                        mk_ev [ev] = EvTypeable t $ EvTypeableTyLit ev
+                        mk_ev [ev] = evTypeable t $ EvTypeableTyLit (EvExpr ev)
                         mk_ev _    = panic "doTyLit"
                   ; return (GenInst [kc_pred] mk_ev True) }
 
@@ -2730,14 +2784,14 @@ a TypeRep for them.  For qualified but not polymorphic types, like
 matchLiftedEquality :: [Type] -> TcS LookupInstResult
 matchLiftedEquality args
   = return (GenInst { lir_new_theta = [ mkTyConApp eqPrimTyCon args ]
-                    , lir_mk_ev     = EvDFunApp (dataConWrapId heqDataCon) args
+                    , lir_mk_ev     = EvExpr . evDFunApp (dataConWrapId heqDataCon) args
                     , lir_safe_over = True })
 
 -- See also Note [The equality types story] in TysPrim
 matchLiftedCoercible :: [Type] -> TcS LookupInstResult
 matchLiftedCoercible args@[k, t1, t2]
   = return (GenInst { lir_new_theta = [ mkTyConApp eqReprPrimTyCon args' ]
-                    , lir_mk_ev     = EvDFunApp (dataConWrapId coercibleDataCon)
+                    , lir_mk_ev     = EvExpr . evDFunApp (dataConWrapId coercibleDataCon)
                                                 args
                     , lir_safe_over = True })
   where
@@ -2839,9 +2893,9 @@ matchHasField dflags short_cut clas tys loc
                          -- Use the equality proof to cast the selector Id to
                          -- type (r -> a), then use the newtype coercion to cast
                          -- it to a HasField dictionary.
-                         mk_ev (ev1:evs) = EvSelector sel_id tvs evs `EvCast` co
+                         mk_ev (ev1:evs) = EvExpr $ evSelector sel_id tvs evs `evCast` co
                            where
-                             co = mkTcSubCo (evTermCoercion ev1)
+                             co = mkTcSubCo (evTermCoercion (EvExpr ev1))
                                       `mkTcTransCo` mkTcSymCo co2
                          mk_ev [] = panic "matchHasField.mk_ev"
 
diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs
index 79e337d905..2881491760 100644
--- a/compiler/typecheck/TcMType.hs
+++ b/compiler/typecheck/TcMType.hs
@@ -203,7 +203,7 @@ cloneWC wc@(WC { wc_simple = simples, wc_impl = implics })
            ; return (implic { ic_wanted = inner_wanted' }) }
 
 -- | Emits a new Wanted. Deals with both equalities and non-equalities.
-emitWanted :: CtOrigin -> TcPredType -> TcM EvTerm
+emitWanted :: CtOrigin -> TcPredType -> TcM EvExpr
 emitWanted origin pty
   = do { ev <- newWanted origin Nothing pty
        ; emitSimple $ mkNonCanonical ev
diff --git a/compiler/typecheck/TcPatSyn.hs b/compiler/typecheck/TcPatSyn.hs
index a5526d267b..1aadf8cc23 100644
--- a/compiler/typecheck/TcPatSyn.hs
+++ b/compiler/typecheck/TcPatSyn.hs
@@ -117,7 +117,7 @@ tcInferPatSynDecl PSB{ psb_id = lname@(L _ name), psb_args = details,
                           (mkTyVarBinders Inferred univ_tvs
                             , req_theta,  ev_binds, req_dicts)
                           (mkTyVarBinders Inferred ex_tvs
-                            , mkTyVarTys ex_tvs, prov_theta, map EvId filtered_prov_dicts)
+                            , mkTyVarTys ex_tvs, prov_theta, map evId filtered_prov_dicts)
                           (map nlHsVar args, map idType args)
                           pat_ty rec_fields }
 
@@ -540,7 +540,7 @@ tc_patsyn_finish :: Located Name      -- ^ PatSyn Name
                  -> Bool              -- ^ Whether infix
                  -> LPat GhcTc        -- ^ Pattern of the PatSyn
                  -> ([TcTyVarBinder], [PredType], TcEvBinds, [EvVar])
-                 -> ([TcTyVarBinder], [TcType], [PredType], [EvTerm])
+                 -> ([TcTyVarBinder], [TcType], [PredType], [EvExpr])
                  -> ([LHsExpr GhcTcId], [TcType])   -- ^ Pattern arguments and
                                                     -- types
                  -> TcType            -- ^ Pattern type
@@ -626,7 +626,7 @@ tc_patsyn_finish lname dir is_infix lpat'
 tcPatSynMatcher :: Located Name
                 -> LPat GhcTc
                 -> ([TcTyVar], ThetaType, TcEvBinds, [EvVar])
-                -> ([TcTyVar], [TcType], ThetaType, [EvTerm])
+                -> ([TcTyVar], [TcType], ThetaType, [EvExpr])
                 -> ([LHsExpr GhcTcId], [TcType])
                 -> TcType
                 -> TcM ((Id, Bool), LHsBinds GhcTc)
@@ -660,7 +660,7 @@ tcPatSynMatcher (L loc name) lpat
              matcher_id    = mkExportedVanillaId matcher_name matcher_sigma
                              -- See Note [Exported LocalIds] in Id
 
-             inst_wrap = mkWpEvApps prov_dicts <.> mkWpTyApps ex_tys
+             inst_wrap = mkWpEvApps (map EvExpr prov_dicts) <.> mkWpTyApps ex_tys
              cont' = foldl nlHsApp (mkLHsWrap inst_wrap (nlHsVar cont)) cont_args
 
              fail' = nlHsApps fail [nlHsVar voidPrimId]
diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs
index 5e97935f55..2718d6be71 100644
--- a/compiler/typecheck/TcRnTypes.hs
+++ b/compiler/typecheck/TcRnTypes.hs
@@ -2674,9 +2674,9 @@ ctEvEqRel = predTypeEqRel . ctEvPred
 ctEvRole :: CtEvidence -> Role
 ctEvRole = eqRelRole . ctEvEqRel
 
-ctEvTerm :: CtEvidence -> EvTerm
-ctEvTerm ev@(CtWanted { ctev_dest = HoleDest _ }) = EvCoercion $ ctEvCoercion ev
-ctEvTerm ev = EvId (ctEvEvId ev)
+ctEvTerm :: CtEvidence -> EvExpr
+ctEvTerm ev@(CtWanted { ctev_dest = HoleDest _ }) = evCoercion $ ctEvCoercion ev
+ctEvTerm ev = evId (ctEvEvId ev)
 
 -- Always returns a coercion whose type is precisely ctev_pred of the CtEvidence.
 -- See also Note [Given in ctEvCoercion]
diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs
index 60c3ea670f..90592d711a 100644
--- a/compiler/typecheck/TcSMonad.hs
+++ b/compiler/typecheck/TcSMonad.hs
@@ -26,7 +26,7 @@ module TcSMonad (
     wrapErrTcS, wrapWarnTcS,
 
     -- Evidence creation and transformation
-    MaybeNew(..), freshGoals, isFresh, getEvTerm,
+    MaybeNew(..), freshGoals, isFresh, getEvExpr,
 
     newTcEvBinds,
     newWantedEq, emitNewWantedEq,
@@ -143,6 +143,7 @@ import TyCon
 import TcErrors   ( solverDepthErrorTcS )
 
 import Name
+import Module ( HasModule, getModule )
 import RdrName ( GlobalRdrEnv, GlobalRdrElt )
 import qualified RnEnv as TcM
 import Var
@@ -2385,6 +2386,12 @@ instance MonadFail.MonadFail TcS where
 instance MonadUnique TcS where
    getUniqueSupplyM = wrapTcS getUniqueSupplyM
 
+instance HasModule TcS where
+   getModule = wrapTcS getModule
+
+instance MonadThings TcS where
+   lookupThing n = wrapTcS (lookupThing n)
+
 -- Basic functionality
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 wrapTcS :: TcM a -> TcS a
@@ -2869,7 +2876,7 @@ newFlattenSkolem flav loc tc xis
            -- Construct the Refl evidence
            ; let pred = mkPrimEqPred fam_ty (mkTyVarTy fsk)
                  co   = mkNomReflCo fam_ty
-           ; ev  <- newGivenEvVar loc (pred, EvCoercion co)
+           ; ev  <- newGivenEvVar loc (pred, EvExpr (evCoercion co))
            ; return (ev, co, fsk) }
 
       | otherwise  -- Generate a [WD] for both Wanted and Derived
@@ -2981,7 +2988,7 @@ tcInstSkolTyVarsX subst tvs = wrapTcS $ TcM.tcInstSkolTyVarsX subst tvs
 -- Creating and setting evidence variables and CtFlavors
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-data MaybeNew = Fresh CtEvidence | Cached EvTerm
+data MaybeNew = Fresh CtEvidence | Cached EvExpr
 
 isFresh :: MaybeNew -> Bool
 isFresh (Fresh {})  = True
@@ -2990,9 +2997,9 @@ isFresh (Cached {}) = False
 freshGoals :: [MaybeNew] -> [CtEvidence]
 freshGoals mns = [ ctev | Fresh ctev <- mns ]
 
-getEvTerm :: MaybeNew -> EvTerm
-getEvTerm (Fresh ctev) = ctEvTerm ctev
-getEvTerm (Cached evt) = evt
+getEvExpr :: MaybeNew -> EvExpr
+getEvExpr (Fresh ctev) = ctEvTerm ctev
+getEvExpr (Cached evt) = evt
 
 setEvBind :: EvBind -> TcS ()
 setEvBind ev_bind