TcEvidence

Documentation

data HsWrapper

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

Defined in TcEvidence

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> HsWrapper -> c HsWrapper

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c HsWrapper

toConstr :: HsWrapper -> Constr

dataTypeOf :: HsWrapper -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c HsWrapper)

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

gmapT :: (forall b. Data b => b -> b) -> HsWrapper -> HsWrapper

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> HsWrapper -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> HsWrapper -> r

gmapQ :: (forall d. Data d => d -> u) -> HsWrapper -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> HsWrapper -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> HsWrapper -> m HsWrapper

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> HsWrapper -> m HsWrapper

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> HsWrapper -> m HsWrapper

Outputable HsWrapper

Defined in TcEvidence

Methods

ppr :: HsWrapper -> SDoc

pprPrec :: Rational -> HsWrapper -> SDoc

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

mkWpTyApps :: [Type] -> HsWrapper

mkWpEvApps :: [EvTerm] -> HsWrapper

mkWpEvVarApps :: [EvVar] -> HsWrapper

mkWpTyLams :: [TyVar] -> HsWrapper

mkWpLams :: [Var] -> HsWrapper

mkWpLet :: TcEvBinds -> HsWrapper

mkWpCastN :: TcCoercionN -> HsWrapper

mkWpCastR :: TcCoercionR -> HsWrapper

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

mkWpFun :: HsWrapper -> HsWrapper -> TcType -> TcType -> SDoc -> HsWrapper

idHsWrapper :: HsWrapper

isIdHsWrapper :: HsWrapper -> Bool

isErasableHsWrapper :: HsWrapper -> Bool

Is the wrapper erasable, i.e., will not affect runtime semantics?

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

data TcEvBinds

Constructors

TcEvBinds EvBindsVar

EvBinds (Bag EvBind)

Instances

Data TcEvBinds

Defined in TcEvidence

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TcEvBinds -> c TcEvBinds

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TcEvBinds

toConstr :: TcEvBinds -> Constr

dataTypeOf :: TcEvBinds -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TcEvBinds)

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

gmapT :: (forall b. Data b => b -> b) -> TcEvBinds -> TcEvBinds

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TcEvBinds -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TcEvBinds -> r

gmapQ :: (forall d. Data d => d -> u) -> TcEvBinds -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> TcEvBinds -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> TcEvBinds -> m TcEvBinds

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TcEvBinds -> m TcEvBinds

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TcEvBinds -> m TcEvBinds

Outputable TcEvBinds

Defined in TcEvidence

Methods

ppr :: TcEvBinds -> SDoc

pprPrec :: Rational -> TcEvBinds -> SDoc

data EvBindsVar

Constructors

EvBindsVar

Fields

• ebv_uniq :: Unique
• ebv_binds :: IORef EvBindMap
• ebv_tcvs :: IORef CoVarSet

CoEvBindsVar

Fields

• ebv_uniq :: Unique
• ebv_tcvs :: IORef CoVarSet

Instances

Outputable EvBindsVar

Defined in TcEvidence

Methods

ppr :: EvBindsVar -> SDoc

pprPrec :: Rational -> EvBindsVar -> SDoc

Uniquable EvBindsVar

Defined in TcEvidence

Methods

getUnique :: EvBindsVar -> Unique

newtype EvBindMap

Constructors

EvBindMap

Fields

• ev_bind_varenv :: DVarEnv EvBind

Instances

Outputable EvBindMap

Defined in TcEvidence

Methods

ppr :: EvBindMap -> SDoc

pprPrec :: Rational -> EvBindMap -> SDoc

emptyEvBindMap :: EvBindMap

extendEvBinds :: EvBindMap -> EvBind -> EvBindMap

lookupEvBind :: EvBindMap -> EvVar -> Maybe EvBind

evBindMapBinds :: EvBindMap -> Bag EvBind

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

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

isEmptyEvBindMap :: EvBindMap -> Bool

data EvBind

Constructors

EvBind

Fields

• eb_lhs :: EvVar
• eb_rhs :: EvTerm
• eb_is_given :: Bool

Instances

Outputable EvBind

Defined in TcEvidence

Methods

ppr :: EvBind -> SDoc

pprPrec :: Rational -> EvBind -> SDoc

emptyTcEvBinds :: TcEvBinds

isEmptyTcEvBinds :: TcEvBinds -> Bool

mkGivenEvBind :: EvVar -> EvTerm -> EvBind

mkWantedEvBind :: EvVar -> EvTerm -> EvBind

evBindVar :: EvBind -> EvVar

isCoEvBindsVar :: EvBindsVar -> Bool

data EvTerm

Constructors

EvExpr EvExpr

EvTypeable Type EvTypeable

EvFun

Fields

• et_tvs :: [TyVar]
• et_given :: [EvVar]
• et_binds :: TcEvBinds
• et_body :: EvVar

Instances

Data EvTerm

Defined in TcEvidence

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> EvTerm -> c EvTerm

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c EvTerm

toConstr :: EvTerm -> Constr

dataTypeOf :: EvTerm -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c EvTerm)

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

gmapT :: (forall b. Data b => b -> b) -> EvTerm -> EvTerm

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EvTerm -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EvTerm -> r

gmapQ :: (forall d. Data d => d -> u) -> EvTerm -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> EvTerm -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> EvTerm -> m EvTerm

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> EvTerm -> m EvTerm

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> EvTerm -> m EvTerm

Outputable EvTerm

Defined in TcEvidence

Methods

ppr :: EvTerm -> SDoc

pprPrec :: Rational -> EvTerm -> SDoc

type EvExpr = CoreExpr

evId :: EvId -> EvExpr

Any sort of evidence Id, including coercions

evCoercion :: TcCoercion -> EvTerm

evCast :: EvExpr -> TcCoercion -> EvTerm

d |> co

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

evDataConApp :: DataCon -> [Type] -> [EvExpr] -> EvTerm

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

mkEvCast :: EvExpr -> TcCoercion -> EvTerm

evVarsOfTerm :: EvTerm -> VarSet

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

evTypeable :: Type -> EvTypeable -> EvTerm

findNeededEvVars :: EvBindMap -> VarSet -> VarSet

evTermCoercion :: EvTerm -> TcCoercion

evTermCoercion_maybe :: EvTerm -> Maybe TcCoercion

data EvCallStack

Evidence for CallStack implicit parameters.

Constructors

EvCsEmpty

EvCsPushCall Name RealSrcSpan EvExpr

EvCsPushCall name loc stk represents a call to name, occurring at loc, in a calling context stk.

Instances

Data EvCallStack

Defined in TcEvidence

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> EvCallStack -> c EvCallStack

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c EvCallStack

toConstr :: EvCallStack -> Constr

dataTypeOf :: EvCallStack -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c EvCallStack)

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

gmapT :: (forall b. Data b => b -> b) -> EvCallStack -> EvCallStack

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EvCallStack -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EvCallStack -> r

gmapQ :: (forall d. Data d => d -> u) -> EvCallStack -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> EvCallStack -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> EvCallStack -> m EvCallStack

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> EvCallStack -> m EvCallStack

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> EvCallStack -> m EvCallStack

Outputable EvCallStack

Defined in TcEvidence

Methods

ppr :: EvCallStack -> SDoc

pprPrec :: Rational -> EvCallStack -> SDoc

data EvTypeable

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 #10348)

Instances

Data EvTypeable

Defined in TcEvidence

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> EvTypeable -> c EvTypeable

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c EvTypeable

toConstr :: EvTypeable -> Constr

dataTypeOf :: EvTypeable -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c EvTypeable)

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

gmapT :: (forall b. Data b => b -> b) -> EvTypeable -> EvTypeable

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EvTypeable -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EvTypeable -> r

gmapQ :: (forall d. Data d => d -> u) -> EvTypeable -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> EvTypeable -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> EvTypeable -> m EvTypeable

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> EvTypeable -> m EvTypeable

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> EvTypeable -> m EvTypeable

Outputable EvTypeable

Defined in TcEvidence

Methods

ppr :: EvTypeable -> SDoc

pprPrec :: Rational -> EvTypeable -> SDoc

type TcCoercion = Coercion

type TcCoercionR = CoercionR

type TcCoercionN = CoercionN

type TcCoercionP = CoercionP

data CoercionHole

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

Instances

Data CoercionHole

Defined in TyCoRep

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CoercionHole -> c CoercionHole

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CoercionHole

toConstr :: CoercionHole -> Constr

dataTypeOf :: CoercionHole -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c CoercionHole)

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

gmapT :: (forall b. Data b => b -> b) -> CoercionHole -> CoercionHole

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CoercionHole -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CoercionHole -> r

gmapQ :: (forall d. Data d => d -> u) -> CoercionHole -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> CoercionHole -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> CoercionHole -> m CoercionHole

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CoercionHole -> m CoercionHole

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CoercionHole -> m CoercionHole

Outputable CoercionHole

Defined in TyCoRep

Methods

ppr :: CoercionHole -> SDoc

pprPrec :: Rational -> CoercionHole -> SDoc

type TcMCoercion = MCoercion

data Role

Constructors

Nominal

Representational

Phantom

Instances

Eq Role

Defined in CoAxiom

Methods

(==) :: Role -> Role -> Bool

(/=) :: Role -> Role -> Bool

Data Role

Defined in CoAxiom

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Role -> c Role

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Role

toConstr :: Role -> Constr

dataTypeOf :: Role -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Role)

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

gmapT :: (forall b. Data b => b -> b) -> Role -> Role

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Role -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Role -> r

gmapQ :: (forall d. Data d => d -> u) -> Role -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Role -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Role -> m Role

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Role -> m Role

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Role -> m Role

Ord Role

Defined in CoAxiom

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

Defined in CoAxiom

Methods

ppr :: Role -> SDoc

pprPrec :: Rational -> Role -> SDoc

Binary Role

Defined in CoAxiom

Methods

put_ :: BinHandle -> Role -> IO ()

put :: BinHandle -> Role -> IO (Bin Role)

get :: BinHandle -> IO Role

data LeftOrRight

Constructors

CLeft

CRight

Instances

Eq LeftOrRight

Defined in BasicTypes

Methods

(==) :: LeftOrRight -> LeftOrRight -> Bool

(/=) :: LeftOrRight -> LeftOrRight -> Bool

Data LeftOrRight

Defined in BasicTypes

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LeftOrRight -> c LeftOrRight

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LeftOrRight

toConstr :: LeftOrRight -> Constr

dataTypeOf :: LeftOrRight -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LeftOrRight)

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

gmapT :: (forall b. Data b => b -> b) -> LeftOrRight -> LeftOrRight

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LeftOrRight -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LeftOrRight -> r

gmapQ :: (forall d. Data d => d -> u) -> LeftOrRight -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> LeftOrRight -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> LeftOrRight -> m LeftOrRight

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LeftOrRight -> m LeftOrRight

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LeftOrRight -> m LeftOrRight

Outputable LeftOrRight

Defined in BasicTypes

Methods

ppr :: LeftOrRight -> SDoc

pprPrec :: Rational -> LeftOrRight -> SDoc

Binary LeftOrRight

Defined in Binary

Methods

put_ :: BinHandle -> LeftOrRight -> IO ()

put :: BinHandle -> LeftOrRight -> IO (Bin LeftOrRight)

get :: BinHandle -> IO LeftOrRight

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

mkTcReflCo :: Role -> TcType -> TcCoercion

mkTcNomReflCo :: TcType -> TcCoercionN

mkTcRepReflCo :: TcType -> TcCoercionR

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

mkTcAppCo :: TcCoercion -> TcCoercionN -> TcCoercion

mkTcFunCo :: Role -> TcCoercion -> TcCoercion -> TcCoercion

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

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

mkTcForAllCo :: TyVar -> TcCoercionN -> TcCoercion -> TcCoercion

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

mkTcSymCo :: TcCoercion -> TcCoercion

mkTcTransCo :: TcCoercion -> TcCoercion -> TcCoercion

mkTcNthCo :: Role -> Int -> TcCoercion -> TcCoercion

mkTcLRCo :: LeftOrRight -> TcCoercion -> TcCoercion

mkTcSubCo :: TcCoercionN -> TcCoercionR

maybeTcSubCo :: EqRel -> TcCoercion -> TcCoercion

If the EqRel is ReprEq, makes a SubCo; otherwise, does nothing. Note that the input coercion should always be nominal.

tcDowngradeRole :: Role -> Role -> TcCoercion -> TcCoercion

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

mkTcGReflRightCo :: Role -> TcType -> TcCoercionN -> TcCoercion

mkTcGReflLeftCo :: Role -> TcType -> TcCoercionN -> TcCoercion

mkTcPhantomCo :: TcCoercionN -> TcType -> TcType -> TcCoercionP

mkTcCoherenceLeftCo :: Role -> TcType -> TcCoercionN -> TcCoercion -> TcCoercion

mkTcCoherenceRightCo :: Role -> TcType -> TcCoercionN -> TcCoercion -> TcCoercion

mkTcKindCo :: TcCoercion -> TcCoercionN

tcCoercionKind :: TcCoercion -> Pair TcType

coVarsOfTcCo :: TcCoercion -> TcTyCoVarSet

mkTcCoVarCo :: CoVar -> TcCoercion

isTcReflCo :: TcCoercion -> Bool

isTcReflexiveCo :: TcCoercion -> Bool

This version does a slow check, calculating the related types and seeing if they are equal.

isTcGReflMCo :: TcMCoercion -> Bool

tcCoToMCo :: TcCoercion -> TcMCoercion

tcCoercionRole :: TcCoercion -> Role

unwrapIP :: Type -> CoercionR

Create a Expr that unwraps an implicit-parameter or overloaded-label dictionary to expose the underlying value. We expect the Expr to have the form `IP sym ty` or `IsLabel sym ty`, and return a Expr `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

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