Safe Haskell	None
Language	GHC2024

GHC.Tc.Types.Evidence

Contents

HsWrapper
Evidence bindings
EvTerm (already a CoreExpr)
HoleExprRef
TcCoercion
QuoteWrapper

Synopsis

data HsWrapper
- = WpHole
- | WpSubType HsWrapper
- | WpCompose HsWrapper HsWrapper
- | WpFun {
  - mult_co :: SubMultCo
  - arg_wrap :: HsWrapper
  - res_wrap :: HsWrapper
  - arg_type :: TcTypeFRR
  - res_type :: TcType
  }
- | WpCast TcCoercionR
- | WpEvLam EvVar
- | WpEvApp EvTerm
- | WpTyLam TyVar
- | WpTyApp KindOrType
- | WpLet TcEvBinds
(<.>) :: HsWrapper -> HsWrapper -> HsWrapper
mkWpTyApps :: [Type] -> HsWrapper
mkWpEvApps :: [EvTerm] -> HsWrapper
mkWpEvVarApps :: [EvVar] -> HsWrapper
mkWpTyLams :: [TyVar] -> HsWrapper
mkWpForAllCast :: [ForAllTyBinder] -> Type -> HsWrapper
mkWpEvLams :: [Var] -> HsWrapper
mkWpLet :: TcEvBinds -> HsWrapper
mkWpFun :: HsWrapper -> HsWrapper -> (SubMultCo, TcTypeFRR) -> TcType -> HsWrapper
mkWpCastN :: TcCoercionN -> HsWrapper
mkWpCastR :: TcCoercionR -> HsWrapper
mkWpEta :: Type -> [Id] -> HsWrapper -> HsWrapper
mkWpSubType :: HsWrapper -> HsWrapper
data SubMultCo
- = EqMultCo TcCoercionN
- | OneSubMult Mult
mkSubMultFunCo :: FunTyFlag -> FunTyFlag -> SubMultCo -> TcCoercionR -> TcCoercionR -> TcCoercionR
subMultCoRKind :: SubMultCo -> Mult
collectHsWrapBinders :: HsWrapper -> ([Var], HsWrapper)
idHsWrapper :: HsWrapper
isIdHsWrapper :: HsWrapper -> Bool
pprHsWrapper :: HsWrapper -> (Bool -> SDoc) -> SDoc
hsWrapDictBinders :: HsWrapper -> Bag DictId
optSubTypeHsWrapper :: HsWrapper -> HsWrapper
data TcEvBinds
- = TcEvBinds EvBindsVar
- | EvBinds (Bag EvBind)
data EvBindsVar
- = EvBindsVar {
  - ebv_uniq :: Unique
  - ebv_binds :: IORef EvBindMap
  - ebv_tcvs :: IORef [TcCoercion]
  }
- | CoEvBindsVar {
  - ebv_uniq :: Unique
  - ebv_tcvs :: IORef [TcCoercion]
  }
newtype EvBindMap = EvBindMap {
- ev_bind_varenv :: DVarEnv EvBind
}
emptyEvBindMap :: EvBindMap
extendEvBinds :: EvBindMap -> EvBind -> EvBindMap
unionEvBindMap :: EvBindMap -> EvBindMap -> EvBindMap
lookupEvBind :: EvBindMap -> EvVar -> Maybe EvBind
evBindMapBinds :: EvBindMap -> Bag EvBind
foldEvBindMap :: (EvBind -> a -> a) -> a -> EvBindMap -> a
nonDetStrictFoldEvBindMap :: (EvBind -> a -> a) -> a -> EvBindMap -> a
filterEvBindMap :: (EvBind -> Bool) -> EvBindMap -> EvBindMap
isEmptyEvBindMap :: EvBindMap -> Bool
evBindMapToVarSet :: EvBindMap -> VarSet
varSetMinusEvBindMap :: VarSet -> EvBindMap -> VarSet
data EvBindInfo
- = EvBindGiven
- | EvBindWanted {
  - ebi_canonical :: CanonicalEvidence
  }
data EvBind = EvBind {
- eb_lhs :: EvVar
- eb_rhs :: EvTerm
- eb_info :: EvBindInfo
}
emptyTcEvBinds :: TcEvBinds
isEmptyTcEvBinds :: TcEvBinds -> Bool
mkGivenEvBind :: EvVar -> EvTerm -> EvBind
mkWantedEvBind :: EvVar -> CanonicalEvidence -> EvTerm -> EvBind
evBindVar :: EvBind -> EvVar
isCoEvBindsVar :: EvBindsVar -> Bool
data EvTerm
- = EvExpr EvExpr
- | EvTypeable Type EvTypeable
- | EvFun {
  - et_tvs :: [TyVar]
  - et_given :: [EvVar]
  - et_binds :: TcEvBinds
  - et_body :: EvVar
  }
type EvExpr = CoreExpr
evId :: EvId -> EvExpr
evCoercion :: TcCoercion -> EvTerm
evCast :: EvExpr -> TcCoercion -> EvTerm
evCastE :: EvExpr -> TcCoercion -> EvExpr
evDFunApp :: DFunId -> [Type] -> [EvExpr] -> EvTerm
evDictApp :: Class -> [Type] -> [EvExpr] -> EvTerm
evSelector :: Id -> [Type] -> [EvExpr] -> EvExpr
evDelayedError :: Type -> String -> EvTerm
mkEvScSelectors :: Class -> [TcType] -> [(TcPredType, EvExpr)]
evTypeable :: Type -> EvTypeable -> EvTerm
evWrapIPE :: PredType -> EvExpr -> EvExpr
evUnwrapIPE :: PredType -> EvExpr -> EvExpr
evUnaryDictAppE :: Class -> [Type] -> EvExpr -> EvExpr
mkEvCast :: EvExpr -> TcCoercion -> EvTerm
nestedEvIdsOfTerm :: EvTerm -> VarSet
evTermFVs :: EvTerm -> FV
evTermCoercion :: EvTerm -> TcCoercion
evTermCoercion_maybe :: EvTerm -> Maybe TcCoercion
evExprCoercion :: EvExpr -> TcCoercion
evExprCoercion_maybe :: EvExpr -> Maybe TcCoercion
data EvCallStack
- = EvCsEmpty
- | EvCsPushCall FastString RealSrcSpan EvExpr
data EvTypeable
- = EvTypeableTyCon TyCon [EvTerm]
- | EvTypeableTyApp EvTerm EvTerm
- | EvTypeableTrFun EvTerm EvTerm EvTerm
- | EvTypeableTyLit EvTerm
data HoleExprRef = HER (IORef EvTerm) TcType Unique
type TcCoercion = Coercion
type TcCoercionR = CoercionR
type TcCoercionN = CoercionN
type TcCoercionP = CoercionP
data CoercionHole
type TcMCoercion = MCoercion
type TcMCoercionN = MCoercionN
type TcMCoercionR = MCoercionR
data Role
- = Nominal
- | Representational
- | Phantom
data LeftOrRight
- = CLeft
- | CRight
pickLR :: LeftOrRight -> (a, a) -> a
maybeSymCo :: SwapFlag -> TcCoercion -> TcCoercion
data QuoteWrapper = QuoteWrapper EvVar Type
applyQuoteWrapper :: QuoteWrapper -> HsWrapper
quoteWrapperTyVarTy :: QuoteWrapper -> Type

HsWrapper

data HsWrapper Source #

HsWrappers are produced by the typechecker to insert pieces of Core syntax.

For example:

User writes: id False. Typechecker elaborates to id @Bool False using WpTyApp.
User writes: compare True False. Typechecker elaborates to compare $dOrdBool True False using WpEvApp.

A wrapper can be thought of as a function CoreExpr -> CoreExpr which transforms Core syntax by elaboration; we usually write this as expr ↦ wrap[expr]. We often write a wrapper as an "expression with a hole", e.g. WpTyApp Int is hole @Int.

NOTATION ~~>: if wrap[ e::t1 ] :: t2, we write the type of wrap as wrap :: t1 ~~> t2.

Constructors

WpHole	The identity `HsWrapper` (similar to the `Refl` coercion).
WpSubType HsWrapper	`WpSubType wp` is the same as `wp`, but with extra invariants. See Note Deep subsumption and WpSubType
WpCompose HsWrapper HsWrapper	(wrap1 `WpCompose` wrap2)[e] = wrap1[ wrap2[ e ]] Hence `(\a. hole) WpCompose (\b. hole) = (\a b. hole)` But `(hole a) WpCompose (hole b) = (hole b a)` If `wrap1 :: t2 ~> t3` and `wrap2 :: t1 ~~> t2`, then `(wrap1 WpCompose wrap2) :: t1 ~~> t3`
WpFun	(WpFun mult_co arg_wrap res_wrap t1 t2)[e] = (x :: exp_arg). res_wrap[ e arg_wrap[x] ] INVARIANT: both input and output types of `arg_wrap` have a fixed runtime-rep See Note [WpFun-FRR-INVARIANT] Typing rules: given: - `mult_co :: act_mult ~ exp_mult` - `arg_wrap :: exp_arg ~~> act_arg` - `res_wrap :: act_res ~~> exp_res` then `WpFun mult_co arg_wrap res_wrap :: (act_arg %act_mult -> arg_res) ~~> (exp_arg %exp_mult -> exp_res)`. This isn't the same as for `mkFunCo`, but it has to be this way because we can't use `mkSymCo` to flip around these `HsWrapper`s. NB: a `WpFun` is always for type-like function arrows; no constraints. Use `mkWpFun` to construct such a wrapper.
Fields mult_co :: SubMultCo arg_wrap :: HsWrapper res_wrap :: HsWrapper arg_type :: TcTypeFRR The "from" type of the argument wrapper res_type :: TcType Either the "from" or the "to" type of the result wrapper
WpCast	A cast: `hole cast co`
Fields TcCoercionR Invariants: `Representational` role. Never the identity coercion.
WpEvLam EvVar	Evidence abstraction `d. hole`, where `d` is an evidence variable
WpEvApp EvTerm	`hole d, where` d@ is evidence for a constraint
WpTyLam TyVar	Type abstraction `a. hole`, where `a` is a type/kind variable (not a coercion variable)
WpTyApp KindOrType	Type application `hole t`, where `t` is a type/kind (not a coercion)
WpLet TcEvBinds	Evidence bindings: `let binds in hole`. The set of evidence bindings should be non-empty (or possibly non-empty), so that the identity `HsWrapper` is always exactly `WpHole`.

Instances

Instances details

Outputable HsWrapper Source #
Instance details Defined in GHC.Tc.Types.Evidence Methods ppr :: HsWrapper -> SDoc Source #
Monoid HsWrapper Source #
Instance details Defined in GHC.Tc.Types.Evidence Methods mempty :: HsWrapper Source # mappend :: HsWrapper -> HsWrapper -> HsWrapper Source # mconcat :: [HsWrapper] -> HsWrapper Source #
Semigroup HsWrapper Source #	The Semigroup instance is a bit fishy, since `WpCompose`, as a data constructor, is "syntactic" and not associative. Concretely, if `a`, `b`, and `c` aren't `WpHole`: (a <> b) <> c ?= a <> (b <> c) > (a `WpCompose` b) `WpCompose` c /= @ a `WpCompose` (b `WpCompose` c) However these two associations are are "semantically equal" in the sense that they produce equal functions when passed to `GHC.HsToCore.Binds.dsHsWrapper`.
Instance details Defined in GHC.Tc.Types.Evidence Methods (<>) :: HsWrapper -> HsWrapper -> HsWrapper Source # sconcat :: NonEmpty HsWrapper -> HsWrapper Source # stimes :: Integral b => b -> HsWrapper -> HsWrapper Source #
Data HsWrapper Source #
Instance details Defined in GHC.Tc.Types.Evidence Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> HsWrapper -> c HsWrapper Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c HsWrapper Source # toConstr :: HsWrapper -> Constr Source # dataTypeOf :: HsWrapper -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c HsWrapper) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c HsWrapper) Source # gmapT :: (forall b. Data b => b -> b) -> HsWrapper -> HsWrapper Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> HsWrapper -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> HsWrapper -> r Source # gmapQ :: (forall d. Data d => d -> u) -> HsWrapper -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> HsWrapper -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> HsWrapper -> m HsWrapper Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> HsWrapper -> m HsWrapper Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> HsWrapper -> m HsWrapper Source #

(<.>) :: HsWrapper -> HsWrapper -> HsWrapper Source #

mkWpTyApps :: [Type] -> HsWrapper Source #

mkWpEvApps :: [EvTerm] -> HsWrapper Source #

mkWpEvVarApps :: [EvVar] -> HsWrapper Source #

mkWpTyLams :: [TyVar] -> HsWrapper Source #

mkWpForAllCast :: [ForAllTyBinder] -> Type -> HsWrapper Source #

mkWpEvLams :: [Var] -> HsWrapper Source #

mkWpLet :: TcEvBinds -> HsWrapper Source #

mkWpFun Source #

Arguments

:: HsWrapper
-> HsWrapper
-> (SubMultCo, TcTypeFRR)	the "from" type of the first wrapper
-> TcType	Either "from" type or "to" type of the second wrapper (used only when the second wrapper is the identity)
-> HsWrapper

Smart constructor to create a WpFun HsWrapper, which avoids introducing a lambda abstraction if the two supplied wrappers are either identities or casts.

PRECONDITION: same as Note [WpFun-FRR-INVARIANT]

mkWpCastN :: TcCoercionN -> HsWrapper Source #

mkWpCastR :: TcCoercionR -> HsWrapper Source #

mkWpEta :: Type -> [Id] -> HsWrapper -> HsWrapper Source #

mkWpSubType :: HsWrapper -> HsWrapper Source #

data SubMultCo Source #

A sub-multiplicity coercion.

Used only to get multiplicities to line up when typechecking partial applications of data constructors, as per Note [Typechecking data constructors] in GHC.Tc.Gen.Head.

See Note [Multiplicity in deep subsumption]

Constructors

EqMultCo TcCoercionN	Equality of multiplicities
OneSubMult Mult	One is a submultiplicity of any other multiplicity.

Instances

Instances details

Outputable SubMultCo Source #
Instance details Defined in GHC.Tc.Types.Evidence Methods ppr :: SubMultCo -> SDoc Source #
Data SubMultCo Source #
Instance details Defined in GHC.Tc.Types.Evidence Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SubMultCo -> c SubMultCo Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SubMultCo Source # toConstr :: SubMultCo -> Constr Source # dataTypeOf :: SubMultCo -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SubMultCo) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SubMultCo) Source # gmapT :: (forall b. Data b => b -> b) -> SubMultCo -> SubMultCo Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SubMultCo -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SubMultCo -> r Source # gmapQ :: (forall d. Data d => d -> u) -> SubMultCo -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> SubMultCo -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> SubMultCo -> m SubMultCo Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SubMultCo -> m SubMultCo Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SubMultCo -> m SubMultCo Source #

mkSubMultFunCo Source #

Arguments

:: FunTyFlag
-> FunTyFlag
-> SubMultCo	act_mult ~~> exp_mult
-> TcCoercionR	act_arg ~~> exp_arg
-> TcCoercionR	act_res ~~> exp_res
-> TcCoercionR

Like mkFunCo2 except that it allows for sub-multiplicity instead of a multiplicity coercion.

subMultCoRKind :: SubMultCo -> Mult Source #

collectHsWrapBinders :: HsWrapper -> ([Var], HsWrapper) Source #

idHsWrapper :: HsWrapper Source #

isIdHsWrapper :: HsWrapper -> Bool Source #

pprHsWrapper :: HsWrapper -> (Bool -> SDoc) -> SDoc Source #

hsWrapDictBinders :: HsWrapper -> Bag DictId Source #

Identifies the lambda-bound dictionaries of an HsWrapper. This is used (only) to allow the pattern-match overlap checker to know what Given dictionaries are in scope.

We specifically do not collect dictionaries bound in a WpLet. These are either superclasses of lambda-bound ones, or (extremely numerous) results of binding Wanted dictionaries. We definitely don't want all those cluttering up the Given dictionaries for pattern-match overlap checking!

optSubTypeHsWrapper :: HsWrapper -> HsWrapper Source #

Evidence bindings

data TcEvBinds Source #

Constructors

TcEvBinds EvBindsVar
EvBinds (Bag EvBind)

Instances

Instances details

Outputable TcEvBinds Source #
Instance details Defined in GHC.Tc.Types.Evidence Methods ppr :: TcEvBinds -> SDoc Source #
Data TcEvBinds Source #
Instance details Defined in GHC.Tc.Types.Evidence Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TcEvBinds -> c TcEvBinds Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TcEvBinds Source # toConstr :: TcEvBinds -> Constr Source # dataTypeOf :: TcEvBinds -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TcEvBinds) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TcEvBinds) Source # gmapT :: (forall b. Data b => b -> b) -> TcEvBinds -> TcEvBinds Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TcEvBinds -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TcEvBinds -> r Source # gmapQ :: (forall d. Data d => d -> u) -> TcEvBinds -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> TcEvBinds -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> TcEvBinds -> m TcEvBinds Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TcEvBinds -> m TcEvBinds Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TcEvBinds -> m TcEvBinds Source #

data EvBindsVar Source #

Constructors

EvBindsVar
Fields ebv_uniq :: Unique ebv_binds :: IORef EvBindMap ebv_tcvs :: IORef [TcCoercion]
CoEvBindsVar
Fields ebv_uniq :: Unique ebv_tcvs :: IORef [TcCoercion]

Instances

Instances details

Uniquable EvBindsVar Source #
Instance details Defined in GHC.Tc.Types.Evidence Methods getUnique :: EvBindsVar -> Unique Source #
Outputable EvBindsVar Source #
Instance details Defined in GHC.Tc.Types.Evidence Methods ppr :: EvBindsVar -> SDoc Source #

newtype EvBindMap Source #

Constructors

EvBindMap
Fields ev_bind_varenv :: DVarEnv EvBind

Instances

Instances details

Outputable EvBindMap Source #
Instance details Defined in GHC.Tc.Types.Evidence Methods ppr :: EvBindMap -> SDoc Source #

emptyEvBindMap :: EvBindMap Source #

extendEvBinds :: EvBindMap -> EvBind -> EvBindMap Source #

unionEvBindMap :: EvBindMap -> EvBindMap -> EvBindMap Source #

Union two evidence binding maps

lookupEvBind :: EvBindMap -> EvVar -> Maybe EvBind Source #

evBindMapBinds :: EvBindMap -> Bag EvBind Source #

foldEvBindMap :: (EvBind -> a -> a) -> a -> EvBindMap -> a Source #

nonDetStrictFoldEvBindMap :: (EvBind -> a -> a) -> a -> EvBindMap -> a Source #

filterEvBindMap :: (EvBind -> Bool) -> EvBindMap -> EvBindMap Source #

isEmptyEvBindMap :: EvBindMap -> Bool Source #

evBindMapToVarSet :: EvBindMap -> VarSet Source #

varSetMinusEvBindMap :: VarSet -> EvBindMap -> VarSet Source #

data EvBindInfo Source #

Constructors

EvBindGiven
EvBindWanted
Fields ebi_canonical :: CanonicalEvidence

data EvBind Source #

Constructors

EvBind
Fields eb_lhs :: EvVar eb_rhs :: EvTerm eb_info :: EvBindInfo

Instances

Instances details

Outputable EvBind Source #
Instance details Defined in GHC.Tc.Types.Evidence Methods ppr :: EvBind -> SDoc Source #
Data EvBind Source #
Instance details Defined in GHC.Tc.Types.Evidence Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> EvBind -> c EvBind Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c EvBind Source # toConstr :: EvBind -> Constr Source # dataTypeOf :: EvBind -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c EvBind) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EvBind) Source # gmapT :: (forall b. Data b => b -> b) -> EvBind -> EvBind Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EvBind -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EvBind -> r Source # gmapQ :: (forall d. Data d => d -> u) -> EvBind -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> EvBind -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> EvBind -> m EvBind Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> EvBind -> m EvBind Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> EvBind -> m EvBind Source #

emptyTcEvBinds :: TcEvBinds Source #

isEmptyTcEvBinds :: TcEvBinds -> Bool Source #

mkGivenEvBind :: EvVar -> EvTerm -> EvBind Source #

mkWantedEvBind :: EvVar -> CanonicalEvidence -> EvTerm -> EvBind Source #

evBindVar :: EvBind -> EvVar Source #

isCoEvBindsVar :: EvBindsVar -> Bool Source #

EvTerm (already a CoreExpr)

data EvTerm Source #

Constructors

EvExpr EvExpr
EvTypeable Type EvTypeable
EvFun
Fields et_tvs :: [TyVar] et_given :: [EvVar] et_binds :: TcEvBinds et_body :: EvVar

Instances

Instances details

Outputable EvTerm Source #
Instance details Defined in GHC.Tc.Types.Evidence Methods ppr :: EvTerm -> SDoc Source #
Data EvTerm Source #
Instance details Defined in GHC.Tc.Types.Evidence Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> EvTerm -> c EvTerm Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c EvTerm Source # toConstr :: EvTerm -> Constr Source # dataTypeOf :: EvTerm -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c EvTerm) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EvTerm) Source # gmapT :: (forall b. Data b => b -> b) -> EvTerm -> EvTerm Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EvTerm -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EvTerm -> r Source # gmapQ :: (forall d. Data d => d -> u) -> EvTerm -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> EvTerm -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> EvTerm -> m EvTerm Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> EvTerm -> m EvTerm Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> EvTerm -> m EvTerm Source #

type EvExpr = CoreExpr Source #

evId :: EvId -> EvExpr Source #

Any sort of evidence Id, including coercions

evCoercion :: TcCoercion -> EvTerm Source #

evCast :: EvExpr -> TcCoercion -> EvTerm Source #

evCastE :: EvExpr -> TcCoercion -> EvExpr Source #

d |> co

evDFunApp :: DFunId -> [Type] -> [EvExpr] -> EvTerm Source #

evDictApp :: Class -> [Type] -> [EvExpr] -> EvTerm Source #

evSelector :: Id -> [Type] -> [EvExpr] -> EvExpr Source #

evDelayedError :: Type -> String -> EvTerm Source #

mkEvScSelectors :: Class -> [TcType] -> [(TcPredType, EvExpr)] Source #

evTypeable :: Type -> EvTypeable -> EvTerm Source #

evWrapIPE :: PredType -> EvExpr -> EvExpr Source #

evUnwrapIPE :: PredType -> EvExpr -> EvExpr Source #

evUnaryDictAppE :: Class -> [Type] -> EvExpr -> EvExpr Source #

mkEvCast :: EvExpr -> TcCoercion -> EvTerm Source #

Deprecated: Please use evCast instead

nestedEvIdsOfTerm :: EvTerm -> VarSet Source #

evTermFVs :: EvTerm -> FV Source #

evTermCoercion :: EvTerm -> TcCoercion Source #

evTermCoercion_maybe :: EvTerm -> Maybe TcCoercion Source #

evExprCoercion :: EvExpr -> TcCoercion Source #

evExprCoercion_maybe :: EvExpr -> Maybe TcCoercion Source #

data EvCallStack Source #

Evidence for CallStack implicit parameters.

Constructors

EvCsEmpty
EvCsPushCall FastString RealSrcSpan EvExpr	`EvCsPushCall origin loc stk` represents a call from `origin`, occurring at `loc`, in a calling context `stk`.

Instances

Instances details

Outputable EvCallStack Source #
Instance details Defined in GHC.Tc.Types.Evidence Methods ppr :: EvCallStack -> SDoc Source #
Data EvCallStack Source #
Instance details Defined in GHC.Tc.Types.Evidence Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> EvCallStack -> c EvCallStack Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c EvCallStack Source # toConstr :: EvCallStack -> Constr Source # dataTypeOf :: EvCallStack -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c EvCallStack) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EvCallStack) Source # gmapT :: (forall b. Data b => b -> b) -> EvCallStack -> EvCallStack Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EvCallStack -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EvCallStack -> r Source # gmapQ :: (forall d. Data d => d -> u) -> EvCallStack -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> EvCallStack -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> EvCallStack -> m EvCallStack Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> EvCallStack -> m EvCallStack Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> EvCallStack -> m EvCallStack Source #

data EvTypeable Source #

Instructions on how to make a Typeable dictionary. See Note [Typeable evidence terms]

Constructors

EvTypeableTyCon TyCon [EvTerm]	Dictionary for `Typeable T` where `T` is a type constructor with all of its kind variables saturated. The `[EvTerm]` is `Typeable` evidence for the applied kinds..
EvTypeableTyApp EvTerm EvTerm	Dictionary for `Typeable (s t)`, given a dictionaries for `s` and `t`.
EvTypeableTrFun EvTerm EvTerm EvTerm	Dictionary for `Typeable (s % w -> t)`, given a dictionaries for `w`, `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 #10348)

Instances

Instances details

Outputable EvTypeable Source #
Instance details Defined in GHC.Tc.Types.Evidence Methods ppr :: EvTypeable -> SDoc Source #
Data EvTypeable Source #
Instance details Defined in GHC.Tc.Types.Evidence Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> EvTypeable -> c EvTypeable Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c EvTypeable Source # toConstr :: EvTypeable -> Constr Source # dataTypeOf :: EvTypeable -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c EvTypeable) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EvTypeable) Source # gmapT :: (forall b. Data b => b -> b) -> EvTypeable -> EvTypeable Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EvTypeable -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EvTypeable -> r Source # gmapQ :: (forall d. Data d => d -> u) -> EvTypeable -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> EvTypeable -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> EvTypeable -> m EvTypeable Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> EvTypeable -> m EvTypeable Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> EvTypeable -> m EvTypeable Source #

HoleExprRef

data HoleExprRef Source #

Where to store evidence for expression holes See Note [Holes in expressions] in GHC.Hs.Expr.

Constructors

HER
Fields (IORef EvTerm) where to write the erroring expression TcType expected type of that expression Unique for debug output only

Instances

Instances details

Outputable HoleExprRef Source #
Instance details Defined in GHC.Tc.Types.Evidence Methods ppr :: HoleExprRef -> SDoc Source #
Data HoleExprRef Source #
Instance details Defined in GHC.Tc.Types.Evidence Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> HoleExprRef -> c HoleExprRef Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c HoleExprRef Source # toConstr :: HoleExprRef -> Constr Source # dataTypeOf :: HoleExprRef -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c HoleExprRef) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c HoleExprRef) Source # gmapT :: (forall b. Data b => b -> b) -> HoleExprRef -> HoleExprRef Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> HoleExprRef -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> HoleExprRef -> r Source # gmapQ :: (forall d. Data d => d -> u) -> HoleExprRef -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> HoleExprRef -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> HoleExprRef -> m HoleExprRef Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> HoleExprRef -> m HoleExprRef Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> HoleExprRef -> m HoleExprRef Source #

TcCoercion

type TcCoercion = Coercion Source #

type TcCoercionR = CoercionR Source #

type TcCoercionN = CoercionN Source #

type TcCoercionP = CoercionP Source #

data CoercionHole Source #

A coercion to be filled in by the type-checker. See Note [Coercion holes]

Instances

Instances details

Uniquable CoercionHole Source #
Instance details Defined in GHC.Core.TyCo.Rep Methods getUnique :: CoercionHole -> Unique Source #
Outputable CoercionHole Source #
Instance details Defined in GHC.Core.TyCo.Rep Methods ppr :: CoercionHole -> SDoc Source #
Data CoercionHole Source #
Instance details Defined in GHC.Core.TyCo.Rep Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CoercionHole -> c CoercionHole Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CoercionHole Source # toConstr :: CoercionHole -> Constr Source # dataTypeOf :: CoercionHole -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c CoercionHole) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CoercionHole) Source # gmapT :: (forall b. Data b => b -> b) -> CoercionHole -> CoercionHole Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CoercionHole -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CoercionHole -> r Source # gmapQ :: (forall d. Data d => d -> u) -> CoercionHole -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> CoercionHole -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> CoercionHole -> m CoercionHole Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CoercionHole -> m CoercionHole Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CoercionHole -> m CoercionHole Source #

type TcMCoercion = MCoercion Source #

type TcMCoercionN = MCoercionN Source #

type TcMCoercionR = MCoercionR Source #

data Role Source #

See Note [Roles] in GHC.Core.Coercion

Order of constructors matters: the Ord instance coincides with the *super*typing relation on roles.

Constructors

Nominal
Representational
Phantom

Instances

Instances details

NFData Role Source #
Instance details Defined in GHC.Core.Coercion.Axiom Methods rnf :: Role -> () Source #
Binary Role Source #
Instance details Defined in GHC.Core.Coercion.Axiom Methods put_ :: WriteBinHandle -> Role -> IO () Source # put :: WriteBinHandle -> Role -> IO (Bin Role) Source # get :: ReadBinHandle -> IO Role Source #
Outputable Role Source #
Instance details Defined in GHC.Core.Coercion.Axiom Methods ppr :: Role -> SDoc Source #
Eq Role Source #
Instance details Defined in Language.Haskell.Syntax.Basic Methods (==) :: Role -> Role -> Bool Source # (/=) :: Role -> Role -> Bool Source #
Ord Role Source #
Instance details Defined in Language.Haskell.Syntax.Basic Methods compare :: Role -> Role -> Ordering Source # (<) :: Role -> Role -> Bool Source # (<=) :: Role -> Role -> Bool Source # (>) :: Role -> Role -> Bool Source # (>=) :: Role -> Role -> Bool Source # max :: Role -> Role -> Role Source # min :: Role -> Role -> Role Source #
Data Role Source #
Instance details Defined in Language.Haskell.Syntax.Basic Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Role -> c Role Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Role Source # toConstr :: Role -> Constr Source # dataTypeOf :: Role -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Role) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Role) Source # gmapT :: (forall b. Data b => b -> b) -> Role -> Role Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Role -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Role -> r Source # gmapQ :: (forall d. Data d => d -> u) -> Role -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> Role -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Role -> m Role Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Role -> m Role Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Role -> m Role Source #
type Anno (Maybe Role) Source #
Instance details Defined in GHC.Hs.Decls type Anno (Maybe Role) = EpAnnCO

data LeftOrRight Source #

Constructors

CLeft
CRight

Instances

Instances details

NFData LeftOrRight Source #
Instance details Defined in GHC.Types.Basic Methods rnf :: LeftOrRight -> () Source #
Binary LeftOrRight Source #
Instance details Defined in GHC.Types.Basic Methods put_ :: WriteBinHandle -> LeftOrRight -> IO () Source # put :: WriteBinHandle -> LeftOrRight -> IO (Bin LeftOrRight) Source # get :: ReadBinHandle -> IO LeftOrRight Source #
Outputable LeftOrRight Source #
Instance details Defined in GHC.Types.Basic Methods ppr :: LeftOrRight -> SDoc Source #
Eq LeftOrRight Source #
Instance details Defined in GHC.Types.Basic Methods (==) :: LeftOrRight -> LeftOrRight -> Bool Source # (/=) :: LeftOrRight -> LeftOrRight -> Bool Source #
Ord LeftOrRight Source #
Instance details Defined in GHC.Types.Basic Methods compare :: LeftOrRight -> LeftOrRight -> Ordering Source # (<) :: LeftOrRight -> LeftOrRight -> Bool Source # (<=) :: LeftOrRight -> LeftOrRight -> Bool Source # (>) :: LeftOrRight -> LeftOrRight -> Bool Source # (>=) :: LeftOrRight -> LeftOrRight -> Bool Source # max :: LeftOrRight -> LeftOrRight -> LeftOrRight Source # min :: LeftOrRight -> LeftOrRight -> LeftOrRight Source #
Data LeftOrRight Source #
Instance details Defined in GHC.Types.Basic Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LeftOrRight -> c LeftOrRight Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LeftOrRight Source # toConstr :: LeftOrRight -> Constr Source # dataTypeOf :: LeftOrRight -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LeftOrRight) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LeftOrRight) Source # gmapT :: (forall b. Data b => b -> b) -> LeftOrRight -> LeftOrRight Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LeftOrRight -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LeftOrRight -> r Source # gmapQ :: (forall d. Data d => d -> u) -> LeftOrRight -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> LeftOrRight -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> LeftOrRight -> m LeftOrRight Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LeftOrRight -> m LeftOrRight Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LeftOrRight -> m LeftOrRight Source #

pickLR :: LeftOrRight -> (a, a) -> a Source #

maybeSymCo :: SwapFlag -> TcCoercion -> TcCoercion Source #

If a SwapFlag is IsSwapped, flip the orientation of a coercion

QuoteWrapper

data QuoteWrapper Source #

Constructors

QuoteWrapper EvVar Type

Instances

Instances details

Data QuoteWrapper Source #

Instance details

Defined in GHC.Tc.Types.Evidence

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> QuoteWrapper -> c QuoteWrapper Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c QuoteWrapper Source #

toConstr :: QuoteWrapper -> Constr Source #

dataTypeOf :: QuoteWrapper -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c QuoteWrapper) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c QuoteWrapper) Source #

gmapT :: (forall b. Data b => b -> b) -> QuoteWrapper -> QuoteWrapper Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> QuoteWrapper -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> QuoteWrapper -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> QuoteWrapper -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> QuoteWrapper -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> QuoteWrapper -> m QuoteWrapper Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> QuoteWrapper -> m QuoteWrapper Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> QuoteWrapper -> m QuoteWrapper Source #

applyQuoteWrapper :: QuoteWrapper -> HsWrapper Source #

Convert the QuoteWrapper into a normal HsWrapper which can be used to apply its contents.

quoteWrapperTyVarTy :: QuoteWrapper -> Type Source #