Safe Haskell	None
Language	Haskell2010

TcEvidence

Synopsis

data HsWrapper
- = WpHole
- | WpCompose HsWrapper HsWrapper
- | WpFun HsWrapper HsWrapper TcType SDoc
- | 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
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 {
  - ebv_uniq :: Unique
  - ebv_binds :: IORef EvBindMap
  - ebv_tcvs :: IORef CoVarSet
  }
- | CoEvBindsVar {
  - ebv_uniq :: Unique
  - ebv_tcvs :: IORef CoVarSet
  }
newtype EvBindMap = EvBindMap {
- ev_bind_varenv :: DVarEnv EvBind
}
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 {
- eb_lhs :: EvVar
- eb_rhs :: EvTerm
- eb_is_given :: Bool
}
emptyTcEvBinds :: TcEvBinds
isEmptyTcEvBinds :: TcEvBinds -> Bool
mkGivenEvBind :: EvVar -> EvTerm -> EvBind
mkWantedEvBind :: EvVar -> 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
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
- = EvCsEmpty
- | EvCsPushCall Name RealSrcSpan EvExpr
data EvTypeable
- = EvTypeableTyCon TyCon [EvTerm]
- | EvTypeableTyApp EvTerm EvTerm
- | EvTypeableTrFun EvTerm EvTerm
- | EvTypeableTyLit EvTerm
type TcCoercion = Coercion
type TcCoercionR = CoercionR
type TcCoercionN = CoercionN
type TcCoercionP = CoercionP
data CoercionHole
data Role
- = Nominal
- | Representational
- | Phantom
data LeftOrRight
- = CLeft
- | CRight
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
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
tcCoercionRole :: TcCoercion -> Role
unwrapIP :: Type -> CoercionR
wrapIP :: Type -> CoercionR

Documentation

data HsWrapper Source #

Constructors

WpHole

WpCompose HsWrapper HsWrapper

WpFun HsWrapper HsWrapper TcType SDoc

Instances

Data HsWrapper Source #

Instance details

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 Source #

Instance details

Defined in TcEvidence

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 Source #

Instance details

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 Source #

Instance details

Defined in TcEvidence

Methods

ppr :: TcEvBinds -> SDoc Source #

pprPrec :: Rational -> TcEvBinds -> SDoc Source #

data EvBindsVar Source #

Constructors

EvBindsVar

Fields

CoEvBindsVar

Fields

ebv_uniq :: Unique
ebv_tcvs :: IORef CoVarSet

Instances

Outputable EvBindsVar Source #

Instance details

Defined in TcEvidence

Methods

ppr :: EvBindsVar -> SDoc Source #

pprPrec :: Rational -> EvBindsVar -> SDoc Source #

Uniquable EvBindsVar Source #

Instance details

Defined in TcEvidence

Methods

getUnique :: EvBindsVar -> Unique Source #

newtype EvBindMap Source #

Constructors

EvBindMap

Fields

ev_bind_varenv :: DVarEnv EvBind

Instances

Outputable EvBindMap Source #

Instance details

Defined in TcEvidence

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 #

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

isEmptyEvBindMap :: EvBindMap -> Bool Source #

data EvBind Source #

Constructors

EvBind

Fields

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

Instances

Outputable EvBind Source #

Instance details

Defined in TcEvidence

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 #

evBindVar :: EvBind -> EvVar Source #

isCoEvBindsVar :: EvBindsVar -> Bool Source #

data EvTerm Source #

Constructors

EvExpr EvExpr

EvTypeable Type EvTypeable

EvFun

Fields

Instances

Data EvTerm Source #

Instance details

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 Source #

Instance details

Defined in TcEvidence

Methods

ppr :: EvTerm -> SDoc Source #

pprPrec :: Rational -> EvTerm -> SDoc 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 #

d |> co

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

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

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

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

evVarsOfTerm :: EvTerm -> VarSet Source #

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

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

findNeededEvVars :: EvBindMap -> VarSet -> VarSet Source #

evTermCoercion :: EvTerm -> TcCoercion Source #

evTermCoercion_maybe :: EvTerm -> Maybe TcCoercion Source #

data EvCallStack Source #

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 Source #

Instance details

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 Source #

Instance details

Defined in TcEvidence

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

Instances

Data EvTypeable Source #

Instance details

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 Source #

Instance details

Defined in TcEvidence

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 Source #

Instance details

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 Source #

Instance details

Defined in TyCoRep

Methods

ppr :: CoercionHole -> SDoc Source #

pprPrec :: Rational -> CoercionHole -> SDoc Source #

data Role Source #

Constructors

Nominal

Representational

Phantom

Instances

Eq Role Source #

Instance details

Defined in CoAxiom

Methods

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

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

Data Role Source #

Instance details

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 Source #

Instance details

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 Source #

Instance details

Defined in CoAxiom

Methods

ppr :: Role -> SDoc Source #

pprPrec :: Rational -> Role -> SDoc Source #

Binary Role Source #

Instance details

Defined in CoAxiom

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 Source #

Instance details

Defined in BasicTypes

Methods

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

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

Data LeftOrRight Source #

Instance details

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 Source #

Instance details

Defined in BasicTypes

Methods

ppr :: LeftOrRight -> SDoc Source #

pprPrec :: Rational -> LeftOrRight -> SDoc Source #

Binary LeftOrRight Source #

Instance details

Defined in Binary

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 :: Role -> 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 #

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

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

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

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

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

mkTcKindCo :: TcCoercion -> TcCoercionN Source #

tcCoercionKind :: TcCoercion -> Pair TcType Source #

coVarsOfTcCo :: TcCoercion -> TcTyCoVarSet 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 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 Source #

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