Safe Haskell | None |
---|---|
Language | Haskell2010 |
TcEvidence
Synopsis
- data HsWrapper
- (<.>) :: 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
- mkWpFuns :: [(TcType, HsWrapper)] -> TcType -> HsWrapper -> SDoc -> HsWrapper
- idHsWrapper :: HsWrapper
- isIdHsWrapper :: HsWrapper -> Bool
- pprHsWrapper :: HsWrapper -> (Bool -> SDoc) -> SDoc
- data TcEvBinds
- = TcEvBinds EvBindsVar
- | EvBinds (Bag EvBind)
- data EvBindsVar = EvBindsVar {}
- newtype EvBindMap = EvBindMap {}
- 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 = EvBind {}
- emptyTcEvBinds :: TcEvBinds
- isEmptyTcEvBinds :: TcEvBinds -> Bool
- mkGivenEvBind :: EvVar -> EvTerm -> EvBind
- mkWantedEvBind :: EvVar -> EvTerm -> EvBind
- sccEvBinds :: Bag EvBind -> [SCC EvBind]
- evBindVar :: EvBind -> EvVar
- data EvTerm
- mkEvCast :: EvTerm -> TcCoercion -> EvTerm
- evVarsOfTerm :: EvTerm -> VarSet
- mkEvScSelectors :: EvTerm -> Class -> [TcType] -> [(TcPredType, EvTerm)]
- data EvLit
- evTermCoercion :: EvTerm -> TcCoercion
- data EvCallStack
- data EvTypeable
- type TcCoercion = Coercion
- type TcCoercionR = CoercionR
- type TcCoercionN = CoercionN
- type TcCoercionP = CoercionP
- data CoercionHole
- data Role
- data 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 :: Int -> TcCoercion -> TcCoercion
- mkTcLRCo :: LeftOrRight -> TcCoercion -> TcCoercion
- mkTcSubCo :: TcCoercionN -> TcCoercionR
- maybeTcSubCo :: EqRel -> TcCoercion -> TcCoercion
- tcDowngradeRole :: Role -> Role -> TcCoercion -> TcCoercion
- mkTcAxiomRuleCo :: CoAxiomRule -> [TcCoercion] -> TcCoercionR
- mkTcCoherenceLeftCo :: TcCoercion -> TcCoercionN -> TcCoercion
- mkTcCoherenceRightCo :: TcCoercion -> TcCoercionN -> TcCoercion
- mkTcPhantomCo :: TcCoercionN -> TcType -> TcType -> TcCoercionP
- mkTcKindCo :: TcCoercion -> TcCoercionN
- tcCoercionKind :: TcCoercion -> Pair TcType
- coVarsOfTcCo :: TcCoercion -> TcTyCoVarSet
- mkTcCoVarCo :: CoVar -> TcCoercion
- isTcReflCo :: TcCoercion -> Bool
- isTcReflexiveCo :: TcCoercion -> Bool
- tcCoercionRole :: TcCoercion -> Role
- unwrapIP :: Type -> CoercionR
- wrapIP :: Type -> CoercionR
Documentation
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 Source # | |
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 Source # | |
mkWpTyApps :: [Type] -> HsWrapper Source #
mkWpEvApps :: [EvTerm] -> HsWrapper Source #
mkWpEvVarApps :: [EvVar] -> HsWrapper Source #
mkWpTyLams :: [TyVar] -> HsWrapper Source #
mkWpCastN :: TcCoercionN -> HsWrapper Source #
mkWpCastR :: TcCoercionR -> 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.
isIdHsWrapper :: HsWrapper -> Bool Source #
Constructors
TcEvBinds EvBindsVar | |
EvBinds (Bag EvBind) |
Instances
Data TcEvBinds Source # | |
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 Source # | |
data EvBindsVar Source #
Constructors
EvBindsVar | |
Instances
Outputable EvBindsVar Source # | |
Uniquable EvBindsVar Source # | |
Methods getUnique :: EvBindsVar -> Unique Source # |
Constructors
EvBindMap | |
Fields |
foldEvBindMap :: (EvBind -> a -> a) -> a -> EvBindMap -> a Source #
isEmptyEvBindMap :: EvBindMap -> Bool Source #
isEmptyTcEvBinds :: TcEvBinds -> Bool Source #
Constructors
Instances
Data EvTerm Source # | |
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 Source # | |
evVarsOfTerm :: EvTerm -> VarSet Source #
mkEvScSelectors :: EvTerm -> Class -> [TcType] -> [(TcPredType, EvTerm)] Source #
Constructors
EvNum Integer | |
EvStr FastString |
Instances
Data EvLit Source # | |
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 Source # | |
evTermCoercion :: EvTerm -> TcCoercion Source #
data EvCallStack Source #
Evidence for CallStack
implicit parameters.
Constructors
EvCsEmpty | |
EvCsPushCall Name RealSrcSpan EvTerm |
|
Instances
Data EvCallStack Source # | |
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 Source # | |
data EvTypeable Source #
Instructions on how to make a Typeable
dictionary.
See Note [Typeable evidence terms]
Constructors
EvTypeableTyCon TyCon [EvTerm] | Dictionary for |
EvTypeableTyApp EvTerm EvTerm | Dictionary for |
EvTypeableTrFun EvTerm EvTerm | Dictionary for |
EvTypeableTyLit EvTerm | Dictionary for a type literal,
e.g. |
Instances
Data EvTypeable Source # | |
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 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 Source # | |
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 Source # | |
Constructors
Nominal | |
Representational | |
Phantom |
Instances
Eq Role Source # | |
Data Role Source # | |
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 Source # | |
Outputable Role Source # | |
Binary Role Source # | |
data LeftOrRight Source #
Instances
Eq LeftOrRight Source # | |
Data LeftOrRight Source # | |
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 Source # | |
Binary LeftOrRight Source # | |
Methods put_ :: BinHandle -> LeftOrRight -> IO () Source # put :: BinHandle -> LeftOrRight -> IO (Bin 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 #
mkTcPhantomCo :: TcCoercionN -> TcType -> TcType -> TcCoercionP Source #
mkTcKindCo :: TcCoercion -> TcCoercionN Source #
tcCoercionKind :: TcCoercion -> Pair TcType Source #
mkTcCoVarCo :: CoVar -> TcCoercion Source #
isTcReflCo :: TcCoercion -> Bool Source #
isTcReflexiveCo :: TcCoercion -> Bool Source #
This version does a slow check, calculating the related types and seeing if they are equal.
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.