Commit 0e022e56 authored by Joachim Breitner's avatar Joachim Breitner
Browse files

Turn EvTerm (almost) into CoreExpr (#14691)

Ideally, I'd like to do

    type EvTerm = CoreExpr

and the type checker builds the evidence terms as it goes. This failed,
becuase the evidence for `Typeable` refers to local identifiers that are
added *after* the typechecker solves constraints. Therefore, `EvTerm`
stays a data type with two constructors: `EvExpr` for `CoreExpr`
evidence, and `EvTypeable` for the others.

Delted `Note [Memoising typeOf]`, its reference (and presumably
relevance) was removed in 8fa4bf9a.

Differential Revision: https://phabricator.haskell.org/D4341
parent 40c753f1
......@@ -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,41 +1154,8 @@ 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
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 (EvTypeable ty ev) = dsEvTypeable ty ev
{-**********************************************************************
* *
......@@ -1312,58 +1277,3 @@ tyConRep tc
; return (Var tc_rep_id) }
| otherwise
= pprPanic "tyConRep" (ppr tc)
{- Note [Memoising typeOf]
~~~~~~~~~~~~~~~~~~~~~~~~~~
See #3245, #9203
IMPORTANT: we don't want to recalculate the TypeRep once per call with
the proxy argument. This is what went wrong in #3245 and #9203. So we
help GHC by manually keeping the 'rep' *outside* the lambda.
-}
{-**********************************************************************
* *
Desugaring EvCallStack evidence
* *
**********************************************************************-}
dsEvCallStack :: EvCallStack -> DsM CoreExpr
-- See Note [Overview of implicit CallStacks] in TcEvidence.hs
dsEvCallStack cs = do
df <- getDynFlags
m <- getModule
srcLocDataCon <- dsLookupDataCon srcLocDataConName
let mkSrcLoc l =
liftM (mkCoreConApps srcLocDataCon)
(sequence [ mkStringExprFS (unitIdFS $ moduleUnitId m)
, mkStringExprFS (moduleNameFS $ moduleName m)
, mkStringExprFS (srcSpanFile l)
, return $ mkIntExprInt df (srcSpanStartLine l)
, return $ mkIntExprInt df (srcSpanStartCol l)
, return $ mkIntExprInt df (srcSpanEndLine l)
, return $ mkIntExprInt df (srcSpanEndCol l)
])
emptyCS <- Var <$> dsLookupGlobalId emptyCallStackName
pushCSVar <- dsLookupGlobalId pushCallStackName
let pushCS name loc rest =
mkCoreApps (Var pushCSVar) [mkCoreTup [name, loc], rest]
let mkPush name loc tm = do
nameExpr <- mkStringExprFS name
locExpr <- mkSrcLoc loc
case tm of
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,
-- so we use unwrapIP to strip the dictionary wrapper
-- See Note [Overview of implicit CallStacks]
let ip_co = unwrapIP (exprType tmExpr)
return (pushCS nameExpr locExpr (mkCastDs tmExpr ip_co))
case cs of
EvCsPushCall name loc tm -> mkPush (occNameFS $ getOccName name) loc tm
EvCsEmpty -> return emptyCS
......@@ -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
---------
......
......@@ -471,6 +471,7 @@ Library
TcTypeable
TcType
TcEvidence
TcEvTerm
TcUnify
TcInteract
TcCanonical
......
......@@ -355,13 +355,13 @@ instCallConstraints orig preds
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
......
......@@ -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) (ctEvExpr new_ev)
; solveCallStack ev ev_cs
; canClass new_ev cls tys False }
......@@ -171,8 +172,9 @@ 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
cs_tm <- evCallStack ev_cs
let ev_tm = mkEvCast cs_tm (wrapIP (ctEvPred ev))
setWantedEvBind (ctEvEvId ev) (EvExpr ev_tm)
canClass :: CtEvidence
-> Class -> [Type]
......@@ -443,7 +445,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 +994,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 )
, evCoercion co_s )
; evar_t <- newGivenEvVar loc ( mkTcEqPredLikeEv ev t1 t2
, EvCoercion co_t )
, evCoercion co_t )
; emitWorkNC [evar_t]
; canEqNC evar_s NomEq s1 s2 }
| otherwise -- Can't happen
......@@ -1264,7 +1266,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) )
, 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 +1461,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 $
(evCoercion $
if isSwapped swapped
then mkTcSymCo $ mkTcKindCo $ mkTcCoVarCo evar
else mkTcKindCo $ mkTcCoVarCo evar)
......@@ -1476,10 +1478,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 $
, evCoercion $
mkTcCoherenceLeftCo (mkTcCoVarCo evar) homo_co )
else ( mkTcEqPredLikeEv ev lhs rhs'
, EvCoercion $
, 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 +1591,7 @@ canEqReflexive :: CtEvidence -- ty ~ ty
-> TcType -- ty
-> TcS (StopOrContinue Ct) -- always Stop
canEqReflexive ev eq_rel ty
= do { setEvBindIfWanted ev (EvCoercion $
= do { setEvBindIfWanted ev (evCoercion $
mkTcReflCo (eqRelRole eq_rel) ty)
; stopWith ev "Solved by reflexivity" }
......@@ -1843,7 +1845,7 @@ rewriteEvidence old_ev@(CtDerived {}) new_pred _co
-- rewriteEvidence to put the isTcReflCo test first!
-- Why? Because for *Derived* constraints, c, the coercion, which
-- was produced by flattening, may contain suspended calls to
-- (ctEvTerm c), which fails for Derived constraints.
-- (ctEvExpr c), which fails for Derived constraints.
-- (Getting this wrong caused Trac #7384.)
continueWith (old_ev { ctev_pred = new_pred })
......@@ -1856,7 +1858,7 @@ rewriteEvidence ev@(CtGiven { ctev_evar = old_evar, ctev_loc = loc }) new_pred c
; 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 +1867,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,7 +1907,7 @@ 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)
......
......@@ -31,6 +31,7 @@ import TyCon
import Class
import DataCon
import TcEvidence
import TcEvTerm
import HsExpr ( UnboundVar(..) )
import HsBinds ( PatSynBind(..) )
import Name
......@@ -806,16 +807,16 @@ 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
EvVarDest evar
-> addTcEvBind ev_binds_var $ mkWantedEvBind evar err_tm
-> addTcEvBind ev_binds_var $ mkWantedEvBind evar (EvExpr err_tm)
HoleDest hole
-> do { -- See Note [Deferred errors for coercion holes]
let co_var = coHoleCoVar hole
; addTcEvBind ev_binds_var $ mkWantedEvBind co_var err_tm
; addTcEvBind ev_binds_var $ mkWantedEvBind co_var (EvExpr err_tm)
; fillCoercionHole hole (mkTcCoVarCo co_var) }}
| otherwise -- Do not set any evidence for Given/Derived
......
-- (those who have too heavy dependencies for TcEvidence)
module TcEvTerm
( evDelayedError, evCallStack )
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 -> EvExpr
evDelayedError ty msg
= Var errorId `mkTyApps` [getRuntimeRep ty, ty] `mkApps` [litMsg]
where
errorId = tYPE_ERROR_ID
litMsg = Lit (MachStr (fastStringToByteString msg))
-- Dictionary for CallStack implicit parameters
evCallStack :: (MonadThings m, HasModule m, HasDynFlags m) =>
EvCallStack -> m EvExpr
-- See Note [Overview of implicit CallStacks] in TcEvidence.hs
evCallStack cs = do
df <- getDynFlags
m <- getModule
srcLocDataCon <- lookupDataCon srcLocDataConName
let mkSrcLoc l = mkCoreConApps srcLocDataCon <$>
sequence [ mkStringExprFS (unitIdFS $ moduleUnitId m)
, mkStringExprFS (moduleNameFS $ moduleName m)
, mkStringExprFS (srcSpanFile l)
, return $ mkIntExprInt df (srcSpanStartLine l)
, return $ mkIntExprInt df (srcSpanStartCol l)
, return $ mkIntExprInt df (srcSpanEndLine l)
, return $ mkIntExprInt df (srcSpanEndCol l)
]
emptyCS <- Var <$> lookupId emptyCallStackName
pushCSVar <- lookupId pushCallStackName
let pushCS name loc rest =
mkCoreApps (Var pushCSVar) [mkCoreTup [name, loc], rest]
let mkPush name loc tm = do
nameExpr <- mkStringExprFS name
locExpr <- mkSrcLoc loc
-- at this point tm :: IP sym CallStack
-- but we need the actual CallStack to pass to pushCS,
-- so we use unwrapIP to strip the dictionary wrapper
-- See Note [Overview of implicit CallStacks]
let ip_co = unwrapIP (exprType tm)
return (pushCS nameExpr locExpr (Cast tm ip_co))
case cs of
EvCsPushCall name loc tm -> mkPush (occNameFS $ getOccName name) loc tm
EvCsEmpty -> return emptyCS
......@@ -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, evSelector,
mkEvCast, evVarsOfTerm, mkEvScSelectors, evTypeable,
evTermCoercion,
EvCallStack(..),
EvTypeable(..),
......@@ -57,12 +62,16 @@ 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 UniqSet
......@@ -306,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
......@@ -465,43 +474,54 @@ 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]
| EvCast EvTerm TcCoercionR -- d |> co
= EvExpr EvExpr
| EvTypeable Type EvTypeable -- Dictionary for (Typeable ty)
deriving Data.Data
| EvDFunApp DFunId -- Dictionary instance application
[Type] [EvTerm]
type EvExpr = CoreExpr
| EvDelayedError Type FastString -- Used with Opt_DeferTypeErrors
-- See Note [Deferring coercion errors to runtime]
-- in TcSimplify
-- An EvTerm is (usually) constructed by any of the constructors here
-- and those more complicates ones who were moved to module TcEvTerm
| 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_
-- | Any sort of evidence Id, including coercions
evId :: EvId -> EvExpr
evId = Var
| EvLit EvLit -- Dictionary for KnownNat and KnownSymbol classes.
-- Note [KnownNat & KnownSymbol and EvLit]
-- coercion bindings
-- See Note [Coercion evidence terms]
evCoercion :: TcCoercion -> EvExpr
evCoercion = Coercion
| EvCallStack EvCallStack -- Dictionary for CallStack implicit parameters
-- | d |> co
evCast :: EvExpr -> TcCoercion -> EvExpr
evCast et tc | isReflCo tc = et
| otherwise = Cast et tc
| EvTypeable Type EvTypeable -- Dictionary for (Typeable ty)
-- Dictionary instance application
evDFunApp :: DFunId -> [Type] -> [EvExpr] -> EvExpr
evDFunApp df tys ets = Var df `mkTyApps` tys `mkApps` ets
| 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
-- 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]
......@@ -526,16 +546,11 @@ 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]
= 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
......@@ -597,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 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)
......@@ -769,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
......@@ -788,30 +757,29 @@ isEmptyTcEvBinds :: TcEvBinds -> Bool
isEmptyTcEvBinds (EvBinds b) = isEmptyBag b
isEmptyTcEvBinds (TcEvBinds {}) = panic "isEmptyTcEvBinds"