Safe Haskell	None
Language	Haskell2010

TcEvidence

Synopsis

Documentation

data HsWrapper Source #

Constructors

WpHole
WpCompose HsWrapper HsWrapper
WpFun HsWrapper HsWrapper TcType SDoc
WpCast TcCoercionR
WpEvLam EvVar
WpEvApp EvTerm
WpTyLam TyVar
WpTyApp KindOrType
WpLet TcEvBinds

Instances

Data HsWrapper #
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 :: (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 #
Outputable HsWrapper #
Methods ppr :: HsWrapper -> SDoc Source # pprPrec :: Rational -> HsWrapper -> SDoc Source #

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

mkWpTyApps :: [Type] -> HsWrapper Source #

mkWpEvApps :: [EvTerm] -> HsWrapper Source #

mkWpEvVarApps :: [EvVar] -> HsWrapper Source #

mkWpTyLams :: [TyVar] -> HsWrapper Source #

mkWpLams :: [Var] -> HsWrapper Source #

mkWpLet :: TcEvBinds -> HsWrapper Source #

mkWpCastN :: TcCoercionN -> HsWrapper Source #

mkWpCastR :: TcCoercionR -> HsWrapper Source #

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

mkWpFun :: HsWrapper -> HsWrapper -> TcType -> TcType -> SDoc -> HsWrapper Source #

mkWpFuns :: [(TcType, HsWrapper)] -> TcType -> HsWrapper -> SDoc -> HsWrapper Source #

mkWpFuns [(ty1, wrap1), (ty2, wrap2)] ty_res wrap_res, where wrap1 :: ty1 "->" ty1' and wrap2 :: ty2 "->" ty2', wrap3 :: ty3 "->" ty3' and ty_res is either ty3 or ty3', gives a wrapper (ty1' -> ty2' -> ty3) "->" (ty1 -> ty2 -> ty3'). Notice that the result wrapper goes the other way round to all the others. This is a result of sub-typing contravariance. The SDoc is a description of what you were doing when you called mkWpFuns.

idHsWrapper :: HsWrapper Source #

isIdHsWrapper :: HsWrapper -> Bool Source #

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

data TcEvBinds Source #

Constructors

TcEvBinds EvBindsVar
EvBinds (Bag EvBind)

Instances

Data TcEvBinds #
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 :: (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 #
Outputable TcEvBinds #
Methods ppr :: TcEvBinds -> SDoc Source # pprPrec :: Rational -> TcEvBinds -> SDoc Source #

data EvBindsVar Source #

Constructors

EvBindsVar
Fields ebv_uniq :: Unique ebv_binds :: IORef EvBindMap ebv_tcvs :: IORef CoVarSet

Instances

Outputable EvBindsVar #
Methods ppr :: EvBindsVar -> SDoc Source # pprPrec :: Rational -> EvBindsVar -> SDoc Source #
Uniquable EvBindsVar #
Methods getUnique :: EvBindsVar -> Unique Source #

newtype EvBindMap Source #

Constructors

EvBindMap
Fields ev_bind_varenv :: DVarEnv EvBind

Instances

Outputable EvBindMap #
Methods ppr :: EvBindMap -> SDoc Source # pprPrec :: Rational -> EvBindMap -> SDoc Source #

emptyEvBindMap :: EvBindMap Source #

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

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

evBindMapBinds :: EvBindMap -> Bag EvBind Source #

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

isEmptyEvBindMap :: EvBindMap -> Bool Source #

data EvBind Source #

Constructors

EvBind
Fields eb_lhs :: EvVar eb_rhs :: EvTerm eb_is_given :: Bool

Instances

Outputable EvBind #
Methods ppr :: EvBind -> SDoc Source # pprPrec :: Rational -> EvBind -> SDoc Source #

emptyTcEvBinds :: TcEvBinds Source #

isEmptyTcEvBinds :: TcEvBinds -> Bool Source #

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

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

sccEvBinds :: Bag EvBind -> [SCC EvBind] Source #

Do SCC analysis on a bag of EvBinds.

evBindVar :: EvBind -> EvVar Source #

data EvTerm Source #

Instances

Data EvTerm #
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 :: (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 #
Outputable EvTerm #
Methods ppr :: EvTerm -> SDoc Source # pprPrec :: Rational -> EvTerm -> SDoc Source #

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

evVarsOfTerm :: EvTerm -> VarSet Source #

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

data EvLit Source #

Constructors

EvNum Integer
EvStr FastString

Instances

Data EvLit #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> EvLit -> c EvLit Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c EvLit Source # toConstr :: EvLit -> Constr Source # dataTypeOf :: EvLit -> DataType Source # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c EvLit) Source # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EvLit) Source # gmapT :: (forall b. Data b => b -> b) -> EvLit -> EvLit Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EvLit -> r Source # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EvLit -> r Source # gmapQ :: (forall d. Data d => d -> u) -> EvLit -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> EvLit -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> EvLit -> m EvLit Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> EvLit -> m EvLit Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> EvLit -> m EvLit Source #
Outputable EvLit #
Methods ppr :: EvLit -> SDoc Source # pprPrec :: Rational -> EvLit -> SDoc Source #

evTermCoercion :: EvTerm -> TcCoercion Source #

data EvCallStack Source #

Evidence for CallStack implicit parameters.

Constructors

EvCsEmpty
EvCsPushCall Name RealSrcSpan EvTerm	`EvCsPushCall name loc stk` represents a call to `name`, occurring at `loc`, in a calling context `stk`.

Instances

Data EvCallStack #
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 :: (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 #
Outputable EvCallStack #
Methods ppr :: EvCallStack -> SDoc Source # pprPrec :: Rational -> EvCallStack -> SDoc 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	Dictionary for `Typeable (s -> t)`, given a dictionaries for `s` and `t`.
EvTypeableTyLit EvTerm	Dictionary for a type literal, e.g. `Typeable "foo"` or `Typeable 3` The `EvTerm` is evidence of, e.g., `KnownNat 3` (see Trac #10348)

Instances

Data EvTypeable #
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 :: (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 #
Outputable EvTypeable #
Methods ppr :: EvTypeable -> SDoc Source # pprPrec :: Rational -> EvTypeable -> SDoc Source #

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

Data CoercionHole #
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 :: (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 #
Outputable CoercionHole #
Methods ppr :: CoercionHole -> SDoc Source # pprPrec :: Rational -> CoercionHole -> SDoc Source #

data Role Source #

Constructors

Nominal
Representational
Phantom

Instances

Eq Role #
Methods (==) :: Role -> Role -> Bool # (/=) :: Role -> Role -> Bool #
Data Role #
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 :: (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 #
Ord Role #
Methods compare :: Role -> Role -> Ordering # (<) :: Role -> Role -> Bool # (<=) :: Role -> Role -> Bool # (>) :: Role -> Role -> Bool # (>=) :: Role -> Role -> Bool # max :: Role -> Role -> Role # min :: Role -> Role -> Role #
Outputable Role #
Methods ppr :: Role -> SDoc Source # pprPrec :: Rational -> Role -> SDoc Source #
Binary Role #
Methods put_ :: BinHandle -> Role -> IO () Source # put :: BinHandle -> Role -> IO (Bin * Role) Source # get :: BinHandle -> IO Role Source #

data LeftOrRight Source #

Constructors

CLeft
CRight

Instances

Eq LeftOrRight #
Methods (==) :: LeftOrRight -> LeftOrRight -> Bool # (/=) :: LeftOrRight -> LeftOrRight -> Bool #
Data LeftOrRight #
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 :: (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 #
Outputable LeftOrRight #
Methods ppr :: LeftOrRight -> SDoc Source # pprPrec :: Rational -> LeftOrRight -> SDoc Source #
Binary LeftOrRight #
Methods put_ :: BinHandle -> LeftOrRight -> IO () Source # put :: BinHandle -> LeftOrRight -> IO (Bin * LeftOrRight) Source # get :: BinHandle -> IO LeftOrRight Source #

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

mkTcReflCo :: Role -> TcType -> TcCoercion Source #

mkTcNomReflCo :: TcType -> TcCoercionN Source #

mkTcRepReflCo :: TcType -> TcCoercionR Source #

mkTcTyConAppCo :: Role -> TyCon -> [TcCoercion] -> TcCoercion Source #

mkTcAppCo :: TcCoercion -> TcCoercionN -> TcCoercion Source #

mkTcFunCo :: Role -> TcCoercion -> TcCoercion -> TcCoercion Source #

mkTcAxInstCo :: Role -> CoAxiom br -> BranchIndex -> [TcType] -> [TcCoercion] -> TcCoercion Source #

mkTcUnbranchedAxInstCo :: CoAxiom Unbranched -> [TcType] -> [TcCoercion] -> TcCoercionR Source #

mkTcForAllCo :: TyVar -> TcCoercionN -> TcCoercion -> TcCoercion Source #

mkTcForAllCos :: [(TyVar, TcCoercionN)] -> TcCoercion -> TcCoercion Source #

mkTcSymCo :: TcCoercion -> TcCoercion Source #

mkTcTransCo :: TcCoercion -> TcCoercion -> TcCoercion Source #

mkTcNthCo :: Int -> TcCoercion -> TcCoercion Source #

mkTcLRCo :: LeftOrRight -> TcCoercion -> TcCoercion Source #

mkTcSubCo :: TcCoercionN -> TcCoercionR Source #

maybeTcSubCo :: EqRel -> TcCoercion -> TcCoercion Source #

tcDowngradeRole :: Role -> Role -> TcCoercion -> TcCoercion Source #

mkTcAxiomRuleCo :: CoAxiomRule -> [TcCoercion] -> TcCoercionR Source #

mkTcCoherenceLeftCo :: TcCoercion -> TcCoercionN -> TcCoercion Source #

mkTcCoherenceRightCo :: TcCoercion -> TcCoercionN -> TcCoercion Source #

mkTcPhantomCo :: TcCoercionN -> TcType -> TcType -> TcCoercionP Source #

mkTcKindCo :: TcCoercion -> TcCoercionN Source #

tcCoercionKind :: TcCoercion -> Pair TcType Source #

coVarsOfTcCo :: TcCoercion -> TcTyCoVarSet Source #

mkTcCoVarCo :: CoVar -> TcCoercion Source #

isTcReflCo :: TcCoercion -> Bool Source #

tcCoercionRole :: TcCoercion -> Role Source #

unwrapIP :: Type -> CoercionR Source #

Create a Coercion that unwraps an implicit-parameter or overloaded-label dictionary to expose the underlying value. We expect the Type to have the form `IP sym ty` or `IsLabel sym ty`, and return a Coercion `co :: IP sym ty ~ ty` or `co :: IsLabel sym ty ~ Proxy# sym -> ty`. See also Note [Type-checking overloaded labels] in TcExpr.

wrapIP :: Type -> CoercionR Source #

Create a Coercion that wraps a value in an implicit-parameter dictionary. See unwrapIP.

EvId EvId
EvCoercion TcCoercion
EvCast EvTerm TcCoercionR
EvDFunApp DFunId [Type] [EvTerm]
EvDelayedError Type FastString
EvSuperClass EvTerm Int
EvLit EvLit
EvCallStack EvCallStack
EvTypeable Type EvTypeable
EvSelector Id [Type] [EvTerm]