GHC.Tc.Types.Evidence

HsWrapper

data HsWrapper

Constructors

WpHole

WpCompose HsWrapper HsWrapper

WpFun HsWrapper HsWrapper (Scaled TcType)

WpCast TcCoercionR

WpEvLam EvVar

WpEvApp EvTerm

WpTyLam TyVar

WpTyApp KindOrType

WpLet TcEvBinds

WpMultCoercion Coercion

Instances

Data HsWrapper

Defined in GHC.Tc.Types.Evidence

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 :: forall r r'. (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

Semigroup HsWrapper

The Semigroup instance is a bit fishy, since WpCompose, as a data constructor, is "syntactic" and not associative. Concretely, if a, b, and c aren't WpHole:

(a <> b) <> c ?= a <> (b <> c)

>

(a `WpCompose` b) `WpCompose` c /= @ a `WpCompose` (b `WpCompose` c)

However these two associations are are "semantically equal" in the sense that they produce equal functions when passed to GHC.HsToCore.Binds.dsHsWrapper.

Defined in GHC.Tc.Types.Evidence

Methods

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

sconcat :: NonEmpty HsWrapper -> HsWrapper

stimes :: Integral b => b -> HsWrapper -> HsWrapper

Monoid HsWrapper

Defined in GHC.Tc.Types.Evidence

Methods

mempty :: HsWrapper

mappend :: HsWrapper -> HsWrapper -> HsWrapper

mconcat :: [HsWrapper] -> HsWrapper

Outputable HsWrapper

Defined in GHC.Tc.Types.Evidence

Methods

ppr :: 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)

idHsWrapper :: HsWrapper

isIdHsWrapper :: HsWrapper -> Bool

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

hsWrapDictBinders :: HsWrapper -> Bag DictId

Identifies the lambda-bound dictionaries of an HsWrapper. This is used (only) to allow the pattern-match overlap checker to know what Given dictionaries are in scope.

We specifically do not collect dictionaries bound in a WpLet. These are either superclasses of lambda-bound ones, or (extremely numerous) results of binding Wanted dictionaries. We definitely don't want all those cluttering up the Given dictionaries for pattern-match overlap checking!

Evidence bindings

data TcEvBinds

Constructors

TcEvBinds EvBindsVar

EvBinds (Bag EvBind)

Instances

Data TcEvBinds

Defined in GHC.Tc.Types.Evidence

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 :: forall r r'. (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 GHC.Tc.Types.Evidence

Methods

ppr :: 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 GHC.Tc.Types.Evidence

Methods

ppr :: EvBindsVar -> SDoc

Uniquable EvBindsVar

Defined in GHC.Tc.Types.Evidence

Methods

getUnique :: EvBindsVar -> Unique

newtype EvBindMap

Constructors

EvBindMap

Fields

• ev_bind_varenv :: DVarEnv EvBind

Instances

Outputable EvBindMap

Defined in GHC.Tc.Types.Evidence

Methods

ppr :: EvBindMap -> SDoc

emptyEvBindMap :: EvBindMap

extendEvBinds :: EvBindMap -> EvBind -> EvBindMap

lookupEvBind :: EvBindMap -> EvVar -> Maybe EvBind

evBindMapBinds :: EvBindMap -> Bag EvBind

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

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

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

isEmptyEvBindMap :: EvBindMap -> Bool

evBindMapToVarSet :: EvBindMap -> VarSet

varSetMinusEvBindMap :: VarSet -> EvBindMap -> VarSet

data EvBind

Constructors

EvBind

Fields

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

Instances

Outputable EvBind

Defined in GHC.Tc.Types.Evidence

Methods

ppr :: EvBind -> SDoc

emptyTcEvBinds :: TcEvBinds

isEmptyTcEvBinds :: TcEvBinds -> Bool

mkGivenEvBind :: EvVar -> EvTerm -> EvBind

mkWantedEvBind :: EvVar -> EvTerm -> EvBind

evBindVar :: EvBind -> EvVar

isCoEvBindsVar :: EvBindsVar -> Bool

EvTerm (already a CoreExpr)

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 GHC.Tc.Types.Evidence

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 :: forall r r'. (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 GHC.Tc.Types.Evidence

Methods

ppr :: 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 FastString RealSrcSpan EvExpr

EvCsPushCall origin loc stk represents a call from origin, occurring at loc, in a calling context stk.

Instances

Data EvCallStack

Defined in GHC.Tc.Types.Evidence

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 :: forall r r'. (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 GHC.Tc.Types.Evidence

Methods

ppr :: 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 EvTerm

Dictionary for Typeable (s % w -> t), given a dictionaries for w, 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 GHC.Tc.Types.Evidence

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 :: forall r r'. (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 GHC.Tc.Types.Evidence

Methods

ppr :: EvTypeable -> SDoc

HoleExprRef

data HoleExprRef

Where to store evidence for expression holes See Note [Holes] in GHC.Tc.Types.Constraint

Constructors

HER

Fields

• (IORef EvTerm)

  where to write the erroring expression

• TcType

  expected type of that expression

• Unique

  for debug output only

Instances

Data HoleExprRef

Defined in GHC.Tc.Types.Evidence

Methods

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

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

toConstr :: HoleExprRef -> Constr

dataTypeOf :: HoleExprRef -> DataType

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

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

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

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

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

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

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

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

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

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

Outputable HoleExprRef

Defined in GHC.Tc.Types.Evidence

Methods

ppr :: HoleExprRef -> SDoc

TcCoercion

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 GHC.Core.TyCo.Rep

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 :: forall r r'. (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 GHC.Core.TyCo.Rep

Methods

ppr :: CoercionHole -> SDoc

Uniquable CoercionHole

Defined in GHC.Core.TyCo.Rep

Methods

getUnique :: CoercionHole -> Unique

type TcMCoercion = MCoercion

type TcMCoercionN = MCoercionN

type TcMCoercionR = MCoercionR

data Role

Constructors

Nominal

Representational

Phantom

Instances

Eq Role

Defined in GHC.Core.Coercion.Axiom

Methods

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

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

Data Role

Defined in GHC.Core.Coercion.Axiom

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 :: forall r r'. (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 GHC.Core.Coercion.Axiom

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 GHC.Core.Coercion.Axiom

Methods

ppr :: Role -> SDoc

Binary Role

Defined in GHC.Core.Coercion.Axiom

Methods

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

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

get :: BinHandle -> IO Role

type Anno (Maybe Role)

Defined in GHC.Hs.Decls

type Anno (Maybe Role) = SrcAnn NoEpAnns

type Anno (Maybe Role)

Defined in GHC.Hs.Decls

type Anno (Maybe Role) = SrcAnn NoEpAnns

data LeftOrRight

Constructors

CLeft

CRight

Instances

Eq LeftOrRight

Defined in GHC.Types.Basic

Methods

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

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

Data LeftOrRight

Defined in GHC.Types.Basic

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 :: forall r r'. (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 GHC.Types.Basic

Methods

ppr :: LeftOrRight -> SDoc

Binary LeftOrRight

Defined in GHC.Types.Basic

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

mkTcSymMCo :: TcMCoercion -> TcMCoercion

mkTcTransCo :: TcCoercion -> TcCoercion -> TcCoercion

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

mkTcLRCo :: LeftOrRight -> TcCoercion -> TcCoercion

mkTcSubCo :: HasDebugCallStack => TcCoercionN -> TcCoercionR

maybeTcSymCo :: SwapFlag -> TcCoercion -> TcCoercion

If a SwapFlag is IsSwapped, flip the orientation of a coercion

maybeTcSubCo :: HasDebugCallStack => EqRel -> TcCoercionN -> 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

mkTcGReflRightMCo :: Role -> TcType -> TcMCoercionN -> TcCoercion

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

mkTcGReflLeftMCo :: Role -> TcType -> TcMCoercionN -> 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

mkTcCoVarCo :: CoVar -> TcCoercion

mkTcFamilyTyConAppCo :: TyCon -> [TcCoercionN] -> TcCoercionN

isTcReflCo :: TcCoercion -> Bool

isTcReflexiveCo :: TcCoercion -> Bool

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

tcCoercionRole :: TcCoercion -> Role

unwrapIP :: Type -> CoercionR

Create a Coercion that unwraps an implicit-parameter dictionary to expose the underlying value. We expect the Type to have the form `IP sym ty`, and return a Coercion `co :: IP sym ty ~ ty`

wrapIP :: Type -> CoercionR

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

QuoteWrapper

data QuoteWrapper

Constructors

QuoteWrapper EvVar Type

Instances

Data QuoteWrapper

Defined in GHC.Tc.Types.Evidence

Methods

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

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

toConstr :: QuoteWrapper -> Constr

dataTypeOf :: QuoteWrapper -> DataType

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

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

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

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

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

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

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

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

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

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

applyQuoteWrapper :: QuoteWrapper -> HsWrapper

Convert the QuoteWrapper into a normal HsWrapper which can be used to apply its contents.

quoteWrapperTyVarTy :: QuoteWrapper -> Type