| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
TcEvidence
- data HsWrapper
- (<.>) :: HsWrapper -> HsWrapper -> HsWrapper
- mkWpTyApps :: [Type] -> HsWrapper
- mkWpEvApps :: [EvTerm] -> HsWrapper
- mkWpEvVarApps :: [EvVar] -> HsWrapper
- mkWpTyLams :: [TyVar] -> HsWrapper
- mkWpLams :: [Var] -> HsWrapper
- mkWpLet :: TcEvBinds -> HsWrapper
- mkWpCast :: TcCoercion -> HsWrapper
- mkWpFun :: HsWrapper -> HsWrapper -> TcType -> TcType -> HsWrapper
- idHsWrapper :: HsWrapper
- isIdHsWrapper :: HsWrapper -> Bool
- pprHsWrapper :: SDoc -> HsWrapper -> SDoc
- data TcEvBinds
- = TcEvBinds EvBindsVar
- | EvBinds (Bag EvBind)
- data EvBindsVar = EvBindsVar (IORef EvBindMap) Unique
- newtype EvBindMap = EvBindMap {}
- emptyEvBindMap :: EvBindMap
- extendEvBinds :: EvBindMap -> EvVar -> EvTerm -> EvBindMap
- lookupEvBind :: EvBindMap -> EvVar -> Maybe EvBind
- evBindMapBinds :: EvBindMap -> Bag EvBind
- data EvBind = EvBind EvVar EvTerm
- emptyTcEvBinds :: TcEvBinds
- isEmptyTcEvBinds :: TcEvBinds -> Bool
- data EvTerm
- mkEvCast :: EvTerm -> TcCoercion -> EvTerm
- evVarsOfTerm :: EvTerm -> VarSet
- data EvLit
- evTermCoercion :: EvTerm -> TcCoercion
- data EvTypeable
- = EvTypeableTyCon TyCon [Kind] [(EvTerm, Type)]
- | EvTypeableTyApp (EvTerm, Type) (EvTerm, Type)
- | EvTypeableTyLit Type
- data TcCoercion
- = TcRefl Role TcType
- | TcTyConAppCo Role TyCon [TcCoercion]
- | TcAppCo TcCoercion TcCoercion
- | TcForAllCo TyVar TcCoercion
- | TcCoVarCo EqVar
- | TcAxiomInstCo (CoAxiom Branched) Int [TcCoercion]
- | TcAxiomRuleCo CoAxiomRule [TcType] [TcCoercion]
- | TcPhantomCo TcType TcType
- | TcSymCo TcCoercion
- | TcTransCo TcCoercion TcCoercion
- | TcNthCo Int TcCoercion
- | TcLRCo LeftOrRight TcCoercion
- | TcSubCo TcCoercion
- | TcCastCo TcCoercion TcCoercion
- | TcLetCo TcEvBinds TcCoercion
- | TcCoercion Coercion
- data LeftOrRight
- pickLR :: LeftOrRight -> (a, a) -> a
- mkTcReflCo :: Role -> TcType -> TcCoercion
- mkTcNomReflCo :: TcType -> TcCoercion
- mkTcRepReflCo :: TcType -> TcCoercion
- mkTcTyConAppCo :: Role -> TyCon -> [TcCoercion] -> TcCoercion
- mkTcAppCo :: TcCoercion -> TcCoercion -> TcCoercion
- mkTcAppCos :: TcCoercion -> [TcCoercion] -> TcCoercion
- mkTcFunCo :: Role -> TcCoercion -> TcCoercion -> TcCoercion
- mkTcAxInstCo :: Role -> CoAxiom br -> Int -> [TcType] -> TcCoercion
- mkTcUnbranchedAxInstCo :: Role -> CoAxiom Unbranched -> [TcType] -> TcCoercion
- mkTcForAllCo :: Var -> TcCoercion -> TcCoercion
- mkTcForAllCos :: [Var] -> TcCoercion -> TcCoercion
- mkTcSymCo :: TcCoercion -> TcCoercion
- mkTcTransCo :: TcCoercion -> TcCoercion -> TcCoercion
- mkTcNthCo :: Int -> TcCoercion -> TcCoercion
- mkTcLRCo :: LeftOrRight -> TcCoercion -> TcCoercion
- mkTcSubCo :: TcCoercion -> TcCoercion
- maybeTcSubCo :: EqRel -> TcCoercion -> TcCoercion
- tcDowngradeRole :: Role -> Role -> TcCoercion -> TcCoercion
- mkTcTransAppCo :: Role -> TcCoercion -> TcType -> TcType -> Role -> TcCoercion -> TcType -> TcType -> Role -> TcCoercion
- mkTcAxiomRuleCo :: CoAxiomRule -> [TcType] -> [TcCoercion] -> TcCoercion
- mkTcPhantomCo :: TcType -> TcType -> TcCoercion
- tcCoercionKind :: TcCoercion -> Pair Type
- coVarsOfTcCo :: TcCoercion -> VarSet
- isEqVar :: Var -> Bool
- mkTcCoVarCo :: EqVar -> TcCoercion
- isTcReflCo :: TcCoercion -> Bool
- getTcCoVar_maybe :: TcCoercion -> Maybe CoVar
- tcCoercionRole :: TcCoercion -> Role
- eqVarRole :: EqVar -> Role
Documentation
Constructors
| WpHole | |
| WpCompose HsWrapper HsWrapper | |
| WpFun HsWrapper HsWrapper TcType TcType | |
| WpCast TcCoercion | |
| WpEvLam EvVar | |
| WpEvApp EvTerm | |
| WpTyLam TyVar | |
| WpTyApp KindOrType | |
| WpLet TcEvBinds |
Instances
mkWpTyApps :: [Type] -> HsWrapper Source
mkWpEvApps :: [EvTerm] -> HsWrapper Source
mkWpEvVarApps :: [EvVar] -> HsWrapper Source
mkWpTyLams :: [TyVar] -> HsWrapper Source
mkWpCast :: TcCoercion -> HsWrapper Source
isIdHsWrapper :: HsWrapper -> Bool Source
pprHsWrapper :: SDoc -> HsWrapper -> SDoc Source
Constructors
| TcEvBinds EvBindsVar | |
| EvBinds (Bag EvBind) |
Instances
evBindMapBinds :: EvBindMap -> Bag EvBind Source
isEmptyTcEvBinds :: TcEvBinds -> Bool Source
Constructors
Instances
mkEvCast :: EvTerm -> TcCoercion -> EvTerm Source
evVarsOfTerm :: EvTerm -> VarSet Source
evTermCoercion :: EvTerm -> TcCoercion Source
data EvTypeable Source
Instructions on how to make a Typeable dictionary.
Constructors
| EvTypeableTyCon TyCon [Kind] [(EvTerm, Type)] | Dicitionary for concrete type constructors. |
| EvTypeableTyApp (EvTerm, Type) (EvTerm, Type) | Dictionary for type applications; this is used when we have
a type expression starting with a type variable (e.g., |
| EvTypeableTyLit Type | Dictionary for a type literal. |
Instances
data TcCoercion Source
Constructors
Instances
data LeftOrRight Source
pickLR :: LeftOrRight -> (a, a) -> a Source
mkTcReflCo :: Role -> TcType -> TcCoercion Source
mkTcNomReflCo :: TcType -> TcCoercion Source
mkTcRepReflCo :: TcType -> TcCoercion Source
mkTcTyConAppCo :: Role -> TyCon -> [TcCoercion] -> TcCoercion Source
mkTcAppCo :: TcCoercion -> TcCoercion -> TcCoercion Source
mkTcAppCos :: TcCoercion -> [TcCoercion] -> TcCoercion Source
mkTcFunCo :: Role -> TcCoercion -> TcCoercion -> TcCoercion Source
mkTcAxInstCo :: Role -> CoAxiom br -> Int -> [TcType] -> TcCoercion Source
mkTcUnbranchedAxInstCo :: Role -> CoAxiom Unbranched -> [TcType] -> TcCoercion Source
mkTcForAllCo :: Var -> TcCoercion -> TcCoercion Source
mkTcForAllCos :: [Var] -> TcCoercion -> TcCoercion Source
mkTcSymCo :: TcCoercion -> TcCoercion Source
mkTcTransCo :: TcCoercion -> TcCoercion -> TcCoercion Source
mkTcNthCo :: Int -> TcCoercion -> TcCoercion Source
mkTcLRCo :: LeftOrRight -> TcCoercion -> TcCoercion Source
mkTcSubCo :: TcCoercion -> TcCoercion Source
maybeTcSubCo :: EqRel -> TcCoercion -> TcCoercion Source
If the EqRel is ReprEq, makes a TcSubCo; otherwise, does nothing. Note that the input coercion should always be nominal.
Arguments
| :: Role | desired role |
| -> Role | current role |
| -> TcCoercion | |
| -> TcCoercion |
Change the role of a TcCoercion. Panics if this isn't a downgrade.
Arguments
| :: Role | r1 |
| -> TcCoercion | co1 :: ty1a ~r1 ty1b |
| -> TcType | ty1a |
| -> TcType | ty1b |
| -> Role | r2 |
| -> TcCoercion | co2 :: ty2a ~r2 ty2b |
| -> TcType | ty2a |
| -> TcType | ty2b |
| -> Role | r3 |
| -> TcCoercion | :: ty1a ty2a ~r3 ty1b ty2b |
Like mkTcAppCo, but allows the second coercion to be other than
nominal. See Note [mkTcTransAppCo]. Role r3 cannot be more stringent
than either r1 or r2.
mkTcAxiomRuleCo :: CoAxiomRule -> [TcType] -> [TcCoercion] -> TcCoercion Source
mkTcPhantomCo :: TcType -> TcType -> TcCoercion Source
tcCoercionKind :: TcCoercion -> Pair Type Source
coVarsOfTcCo :: TcCoercion -> VarSet Source
mkTcCoVarCo :: EqVar -> TcCoercion Source
isTcReflCo :: TcCoercion -> Bool Source
tcCoercionRole :: TcCoercion -> Role Source