GHC.Core.TyCo.Rep

Types

data Type

Constructors

TyVarTy Var

Vanilla type or kind variable (*never* a coercion variable)

AppTy Type Type

Type application to something other than a TyCon. Parameters:

1) Function: must not be a TyConApp or CastTy, must be another AppTy, or TyVarTy See Note [Respecting definitional equality] (EQ1) about the no CastTy requirement

2) Argument type

TyConApp TyCon [KindOrType]

Application of a TyCon, including newtypes and synonyms. Invariant: saturated applications of FunTyCon must use FunTy and saturated synonyms must use their own constructors. However, unsaturated FunTyCons do appear as TyConApps. Parameters:

1) Type constructor being applied to.

2) Type arguments. Might not have enough type arguments here to saturate the constructor. Even type synonyms are not necessarily saturated; for example unsaturated type synonyms can appear as the right hand side of a type synonym.

ForAllTy !ForAllTyBinder Type

A Π type. Note [When we quantify over a coercion variable] INVARIANT: If the binder is a coercion variable, it must be mentioned in the Type. See Note [Unused coercion variable in ForAllTy]

FunTy

FUN m t1 t2 Very common, so an important special case See Note [Function types]

Fields

• ft_af :: FunTyFlag
• ft_mult :: Mult
• ft_arg :: Type
• ft_res :: Type

LitTy TyLit

Type literals are similar to type constructors.

CastTy Type KindCoercion

A kind cast. The coercion is always nominal. INVARIANT: The cast is never reflexive (EQ2) INVARIANT: The Type is not a CastTy (use TransCo instead) (EQ3) INVARIANT: The Type is not a ForAllTy over a tyvar (EQ4) See Note [Respecting definitional equality]

CoercionTy Coercion

Injection of a Coercion into a type This should only ever be used in the RHS of an AppTy, in the list of a TyConApp, when applying a promoted GADT data constructor

Instances

Data Type

Defined in GHC.Core.TyCo.Rep

Methods

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

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

toConstr :: Type -> Constr

dataTypeOf :: Type -> DataType

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

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

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

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

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

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

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

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

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

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

Outputable Type

Defined in GHC.Core.TyCo.Rep

Methods

ppr :: Type -> SDoc

Eq (DeBruijn Type)

Defined in GHC.Core.Map.Type

Methods

(==) :: DeBruijn Type -> DeBruijn Type -> Bool

(/=) :: DeBruijn Type -> DeBruijn Type -> Bool

data TyLit

Constructors

NumTyLit Integer

StrTyLit FastString

CharTyLit Char

Instances

Data TyLit

Defined in GHC.Core.TyCo.Rep

Methods

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

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

toConstr :: TyLit -> Constr

dataTypeOf :: TyLit -> DataType

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

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

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

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

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

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

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

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

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

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

Outputable TyLit

Defined in GHC.Core.TyCo.Rep

Methods

ppr :: TyLit -> SDoc

Eq TyLit

Defined in GHC.Core.TyCo.Rep

Methods

(==) :: TyLit -> TyLit -> Bool

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

type KindOrType = Type

The key representation of types within the compiler

type Kind = Type

The key type representing kinds in the compiler.

type RuntimeRepType = Type

Type synonym used for types of kind RuntimeRep.

type LevityType = Type

Type synonym used for types of kind Levity.

type KnotTied ty = ty

A type labeled KnotTied might have knot-tied tycons in it. See Note [Type checking recursive type and class declarations] in GHC.Tc.TyCl

type PredType = Type

A type of the form p of constraint kind represents a value whose type is the Haskell predicate p, where a predicate is what occurs before the => in a Haskell type.

We use PredType as documentation to mark those types that we guarantee to have this kind.

It can be expanded into its representation, but:

• The type checker must treat it as opaque
• The rest of the compiler treats it as transparent

Consider these examples:

f :: (Eq a) => a -> Int
g :: (?x :: Int -> Int) => a -> Int
h :: (r\l) => {r} => {l::Int | r}

Here the Eq a and ?x :: Int -> Int and rl are all called "predicates"

type ThetaType = [PredType]

A collection of PredTypes

type FRRType = Type

data ForAllTyFlag

ForAllTyFlag

Is something required to appear in source Haskell (Required), permitted by request (Specified) (visible type application), or prohibited entirely from appearing in source Haskell (Inferred)? See Note [VarBndrs, ForAllTyBinders, TyConBinders, and visibility] in GHC.Core.TyCo.Rep

Constructors

Invisible Specificity

Required

Bundled Patterns

pattern Specified :: ForAllTyFlag

pattern Inferred :: ForAllTyFlag

Instances

Data ForAllTyFlag

Defined in GHC.Types.Var

Methods

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

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

toConstr :: ForAllTyFlag -> Constr

dataTypeOf :: ForAllTyFlag -> DataType

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

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

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

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

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

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

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

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

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

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

Binary ForAllTyFlag

Defined in GHC.Types.Var

Methods

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

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

get :: BinHandle -> IO ForAllTyFlag

Outputable ForAllTyFlag

Defined in GHC.Types.Var

Methods

ppr :: ForAllTyFlag -> SDoc

Eq ForAllTyFlag

Defined in GHC.Types.Var

Methods

(==) :: ForAllTyFlag -> ForAllTyFlag -> Bool

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

Ord ForAllTyFlag

Defined in GHC.Types.Var

Methods

compare :: ForAllTyFlag -> ForAllTyFlag -> Ordering

(<) :: ForAllTyFlag -> ForAllTyFlag -> Bool

(<=) :: ForAllTyFlag -> ForAllTyFlag -> Bool

(>) :: ForAllTyFlag -> ForAllTyFlag -> Bool

(>=) :: ForAllTyFlag -> ForAllTyFlag -> Bool

max :: ForAllTyFlag -> ForAllTyFlag -> ForAllTyFlag

min :: ForAllTyFlag -> ForAllTyFlag -> ForAllTyFlag

Outputable tv => Outputable (VarBndr tv ForAllTyFlag)

Defined in GHC.Types.Var

Methods

ppr :: VarBndr tv ForAllTyFlag -> SDoc

data FunTyFlag

The non-dependent version of ForAllTyFlag. See Note [FunTyFlag] Appears here partly so that it's together with its friends ForAllTyFlag and ForallVisFlag, but also because it is used in IfaceType, rather early in the compilation chain

Constructors

FTF_T_T

FTF_T_C

FTF_C_T

FTF_C_C

Instances

Data FunTyFlag

Defined in GHC.Types.Var

Methods

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

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

toConstr :: FunTyFlag -> Constr

dataTypeOf :: FunTyFlag -> DataType

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

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

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

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

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

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

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

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

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

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

Binary FunTyFlag

Defined in GHC.Types.Var

Methods

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

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

get :: BinHandle -> IO FunTyFlag

Outputable FunTyFlag

Defined in GHC.Types.Var

Methods

ppr :: FunTyFlag -> SDoc

Eq FunTyFlag

Defined in GHC.Types.Var

Methods

(==) :: FunTyFlag -> FunTyFlag -> Bool

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

Ord FunTyFlag

Defined in GHC.Types.Var

Methods

compare :: FunTyFlag -> FunTyFlag -> Ordering

(<) :: FunTyFlag -> FunTyFlag -> Bool

(<=) :: FunTyFlag -> FunTyFlag -> Bool

(>) :: FunTyFlag -> FunTyFlag -> Bool

(>=) :: FunTyFlag -> FunTyFlag -> Bool

max :: FunTyFlag -> FunTyFlag -> FunTyFlag

min :: FunTyFlag -> FunTyFlag -> FunTyFlag

Coercions

data Coercion

A Coercion is concrete evidence of the equality/convertibility of two types.

Constructors

Refl Type

GRefl Role Type MCoercionN

TyConAppCo Role TyCon [Coercion]

AppCo Coercion CoercionN

ForAllCo TyCoVar KindCoercion Coercion

FunCo

Fields

• fco_role :: Role
• fco_afl :: FunTyFlag
• fco_afr :: FunTyFlag
• fco_mult :: CoercionN
• fco_arg, fco_res :: Coercion

CoVarCo CoVar

AxiomInstCo (CoAxiom Branched) BranchIndex [Coercion]

AxiomRuleCo CoAxiomRule [Coercion]

UnivCo UnivCoProvenance Role Type Type

SymCo Coercion

TransCo Coercion Coercion

SelCo CoSel Coercion

LRCo LeftOrRight CoercionN

InstCo Coercion CoercionN

KindCo Coercion

SubCo CoercionN

HoleCo CoercionHole

See Note [Coercion holes] Only present during typechecking

Instances

Data Coercion

Defined in GHC.Core.TyCo.Rep

Methods

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

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

toConstr :: Coercion -> Constr

dataTypeOf :: Coercion -> DataType

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

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

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

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

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

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

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

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

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

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

Outputable Coercion

Defined in GHC.Core.TyCo.Rep

Methods

ppr :: Coercion -> SDoc

Eq (DeBruijn Coercion)

Defined in GHC.Core.Map.Type

Methods

(==) :: DeBruijn Coercion -> DeBruijn Coercion -> Bool

(/=) :: DeBruijn Coercion -> DeBruijn Coercion -> Bool

data CoSel

Constructors

SelTyCon Int Role

SelFun FunSel

SelForAll

Instances

Data CoSel

Defined in GHC.Core.TyCo.Rep

Methods

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

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

toConstr :: CoSel -> Constr

dataTypeOf :: CoSel -> DataType

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

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

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

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

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

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

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

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

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

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

NFData CoSel

Defined in GHC.Core.TyCo.Rep

Methods

rnf :: CoSel -> ()

Binary CoSel

Defined in GHC.Core.TyCo.Rep

Methods

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

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

get :: BinHandle -> IO CoSel

Outputable CoSel

Defined in GHC.Core.TyCo.Rep

Methods

ppr :: CoSel -> SDoc

Eq CoSel

Defined in GHC.Core.TyCo.Rep

Methods

(==) :: CoSel -> CoSel -> Bool

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

data FunSel

Constructors

SelMult

SelArg

SelRes

Instances

Data FunSel

Defined in GHC.Core.TyCo.Rep

Methods

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

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

toConstr :: FunSel -> Constr

dataTypeOf :: FunSel -> DataType

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

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

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

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

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

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

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

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

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

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

Outputable FunSel

Defined in GHC.Core.TyCo.Rep

Methods

ppr :: FunSel -> SDoc

Eq FunSel

Defined in GHC.Core.TyCo.Rep

Methods

(==) :: FunSel -> FunSel -> Bool

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

data UnivCoProvenance

For simplicity, we have just one UnivCo that represents a coercion from some type to some other type, with (in general) no restrictions on the type. The UnivCoProvenance specifies more exactly what the coercion really is and why a program should (or shouldn't!) trust the coercion. It is reasonable to consider each constructor of UnivCoProvenance as a totally independent coercion form; their only commonality is that they don't tell you what types they coercion between. (That info is in the UnivCo constructor of Coercion.

Constructors

PhantomProv KindCoercion

See Note [Phantom coercions]. Only in Phantom roled coercions

ProofIrrelProv KindCoercion

From the fact that any two coercions are considered equivalent. See Note [ProofIrrelProv]. Can be used in Nominal or Representational coercions

PluginProv String

From a plugin, which asserts that this coercion is sound. The string is for the use of the plugin.

CorePrepProv Bool

Instances

Data UnivCoProvenance

Defined in GHC.Core.TyCo.Rep

Methods

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

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

toConstr :: UnivCoProvenance -> Constr

dataTypeOf :: UnivCoProvenance -> DataType

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

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

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

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

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

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

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

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

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

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

Outputable UnivCoProvenance

Defined in GHC.Core.TyCo.Rep

Methods

ppr :: UnivCoProvenance -> SDoc

data CoercionHole

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

Constructors

CoercionHole

Fields

• ch_co_var :: CoVar
• ch_ref :: IORef (Maybe Coercion)

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

Uniquable CoercionHole

Defined in GHC.Core.TyCo.Rep

Methods

getUnique :: CoercionHole -> Unique

Outputable CoercionHole

Defined in GHC.Core.TyCo.Rep

Methods

ppr :: CoercionHole -> SDoc

coHoleCoVar :: CoercionHole -> CoVar

setCoHoleCoVar :: CoercionHole -> CoVar -> CoercionHole

type CoercionN = Coercion

type CoercionR = Coercion

type CoercionP = Coercion

type KindCoercion = CoercionN

data MCoercion

A semantically more meaningful type to represent what may or may not be a useful Coercion.

Constructors

MRefl

MCo Coercion

Instances

Data MCoercion

Defined in GHC.Core.TyCo.Rep

Methods

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

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

toConstr :: MCoercion -> Constr

dataTypeOf :: MCoercion -> DataType

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

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

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

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

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

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

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

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

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

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

Outputable MCoercion

Defined in GHC.Core.TyCo.Rep

Methods

ppr :: MCoercion -> SDoc

type MCoercionR = MCoercion

type MCoercionN = MCoercion

Functions over types

mkNakedTyConTy :: TyCon -> Type

mkNakedTyConTy creates a nullary TyConApp. In general you should rather use mkTyConTy, which picks the shared nullary TyConApp from inside the TyCon (via tyConNullaryTy. But we have to build the TyConApp tc [] in that TyCon field; that's what mkNakedTyConTy is for.

mkTyVarTy :: TyVar -> Type

mkTyVarTys :: [TyVar] -> [Type]

mkTyCoVarTy :: TyCoVar -> Type

mkTyCoVarTys :: [TyCoVar] -> [Type]

mkFunTy :: HasDebugCallStack => FunTyFlag -> Mult -> Type -> Type -> Type infixr 3

mkNakedFunTy :: FunTyFlag -> Kind -> Kind -> Kind

mkVisFunTy :: HasDebugCallStack => Mult -> Type -> Type -> Type

mkScaledFunTys :: HasDebugCallStack => [Scaled Type] -> Type -> Type

mkInvisFunTy :: HasDebugCallStack => Type -> Type -> Type infixr 3

mkInvisFunTys :: HasDebugCallStack => [Type] -> Type -> Type

tcMkVisFunTy :: Mult -> Type -> Type -> Type

tcMkInvisFunTy :: TypeOrConstraint -> Type -> Type -> Type

tcMkScaledFunTys :: [Scaled Type] -> Type -> Type

mkForAllTy :: ForAllTyBinder -> Type -> Type

Like mkTyCoForAllTy, but does not check the occurrence of the binder See Note [Unused coercion variable in ForAllTy]

mkForAllTys :: [ForAllTyBinder] -> Type -> Type

Wraps foralls over the type using the provided TyCoVars from left to right

mkInvisForAllTys :: [InvisTVBinder] -> Type -> Type

Wraps foralls over the type using the provided InvisTVBinders from left to right

mkPiTy :: PiTyBinder -> Type -> Type

mkPiTys :: [PiTyBinder] -> Type -> Type

mkVisFunTyMany :: HasDebugCallStack => Type -> Type -> Type infixr 3

Make nested arrow types | Special, common, case: Arrow type with mult Many

mkVisFunTysMany :: [Type] -> Type -> Type

nonDetCmpTyLit :: TyLit -> TyLit -> Ordering

cmpTyLit :: TyLit -> TyLit -> Ordering

Functions over coercions

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

Analyzing types

data TyCoFolder env a

Constructors

TyCoFolder

Fields

• tcf_view :: Type -> Maybe Type
• tcf_tyvar :: env -> TyVar -> a
• tcf_covar :: env -> CoVar -> a
• tcf_hole :: env -> CoercionHole -> a

  What to do with coercion holes. See Note [Coercion holes] in GHC.Core.TyCo.Rep.

• tcf_tycobinder :: env -> TyCoVar -> ForAllTyFlag -> env

  The returned env is used in the extended scope

foldTyCo :: Monoid a => TyCoFolder env a -> env -> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)

noView :: Type -> Maybe Type

A view function that looks through nothing.

Sizes

typeSize :: Type -> Int

coercionSize :: Coercion -> Int

provSize :: UnivCoProvenance -> Int

Multiplicities

data Scaled a

A shorthand for data with an attached Mult element (the multiplicity).

Constructors

Scaled !Mult a

Instances

Data a => Data (Scaled a)

Defined in GHC.Core.TyCo.Rep

Methods

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

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

toConstr :: Scaled a -> Constr

dataTypeOf :: Scaled a -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> Scaled a -> Scaled a

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

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

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

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

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

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

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

Outputable a => Outputable (Scaled a)

Defined in GHC.Core.TyCo.Rep

Methods

ppr :: Scaled a -> SDoc

scaledMult :: Scaled a -> Mult

scaledThing :: Scaled a -> a

mapScaledType :: (Type -> Type) -> Scaled Type -> Scaled Type

Apply a function to both the Mult and the Type in a 'Scaled Type'

type Mult = Type

Mult is a type alias for Type.

Mult must contain Type because multiplicity variables are mere type variables (of kind Multiplicity) in Haskell. So the simplest implementation is to make Mult be Type.

Multiplicities can be formed with: - One: GHC.Types.One (= oneDataCon) - Many: GHC.Types.Many (= manyDataCon) - Multiplication: GHC.Types.MultMul (= multMulTyCon)

So that Mult feels a bit more structured, we provide pattern synonyms and smart constructors for these.