TyCoRep

Documentation

data TyThing

A global typecheckable-thing, essentially anything that has a name. Not to be confused with a TcTyThing, which is also a typecheckable thing but in the *local* context. See TcEnv for how to retrieve a TyThing given a Name.

Constructors

AnId Id

AConLike ConLike

ATyCon TyCon

ACoAxiom (CoAxiom Branched)

Instances

Outputable TyThing

Defined in TyCoRep

Methods

ppr :: TyThing -> SDoc

pprPrec :: Rational -> TyThing -> SDoc

NamedThing TyThing

Defined in TyCoRep

Methods

getOccName :: TyThing -> OccName

getName :: TyThing -> Name

tyThingCategory :: TyThing -> String

pprTyThingCategory :: TyThing -> SDoc

pprShortTyThing :: TyThing -> SDoc

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 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 !TyCoVarBinder Type

A Π type.

FunTy

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

Fields

• ft_af :: AnonArgFlag
• 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 refl. INVARIANT: The Type is not a CastTy (use TransCo instead) See Note Respecting definitional equality and (EQ3)

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 TyCoRep

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 :: (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 TyCoRep

Methods

ppr :: Type -> SDoc

pprPrec :: Rational -> Type -> SDoc

data TyLit

Constructors

NumTyLit Integer

StrTyLit FastString

Instances

Eq TyLit

Defined in TyCoRep

Methods

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

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

Data TyLit

Defined in TyCoRep

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

Ord TyLit

Defined in TyCoRep

Methods

compare :: TyLit -> TyLit -> Ordering

(<) :: TyLit -> TyLit -> Bool

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

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

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

max :: TyLit -> TyLit -> TyLit

min :: TyLit -> TyLit -> TyLit

Outputable TyLit

Defined in TyCoRep

Methods

ppr :: TyLit -> SDoc

pprPrec :: Rational -> TyLit -> SDoc

type KindOrType = Type

The key representation of types within the compiler

type Kind = Type

The key type representing kinds in the compiler.

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 TcTyClsDecls

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

data ArgFlag

Argument Flag

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, TyCoVarBinders, TyConBinders, and visibility] in TyCoRep

Constructors

Inferred

Specified

Required

Instances

Eq ArgFlag

Defined in Var

Methods

(==) :: ArgFlag -> ArgFlag -> Bool

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

Data ArgFlag

Defined in Var

Methods

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

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

toConstr :: ArgFlag -> Constr

dataTypeOf :: ArgFlag -> DataType

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

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

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

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

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

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

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

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

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

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

Ord ArgFlag

Defined in Var

Methods

compare :: ArgFlag -> ArgFlag -> Ordering

(<) :: ArgFlag -> ArgFlag -> Bool

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

(>) :: ArgFlag -> ArgFlag -> Bool

(>=) :: ArgFlag -> ArgFlag -> Bool

max :: ArgFlag -> ArgFlag -> ArgFlag

min :: ArgFlag -> ArgFlag -> ArgFlag

Outputable ArgFlag

Defined in Var

Methods

ppr :: ArgFlag -> SDoc

pprPrec :: Rational -> ArgFlag -> SDoc

Binary ArgFlag

Defined in Var

Methods

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

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

get :: BinHandle -> IO ArgFlag

Outputable tv => Outputable (VarBndr tv ArgFlag)

Defined in Var

Methods

ppr :: VarBndr tv ArgFlag -> SDoc

pprPrec :: Rational -> VarBndr tv ArgFlag -> SDoc

data AnonArgFlag

The non-dependent version of ArgFlag.

Constructors

VisArg

Used for (->): an ordinary non-dependent arrow. The argument is visible in source code.

InvisArg

Used for (=>): a non-dependent predicate arrow. The argument is invisible in source code.

Instances

Eq AnonArgFlag

Defined in Var

Methods

(==) :: AnonArgFlag -> AnonArgFlag -> Bool

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

Data AnonArgFlag

Defined in Var

Methods

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

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

toConstr :: AnonArgFlag -> Constr

dataTypeOf :: AnonArgFlag -> DataType

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

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

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

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

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

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

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

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

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

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

Ord AnonArgFlag

Defined in Var

Methods

compare :: AnonArgFlag -> AnonArgFlag -> Ordering

(<) :: AnonArgFlag -> AnonArgFlag -> Bool

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

(>) :: AnonArgFlag -> AnonArgFlag -> Bool

(>=) :: AnonArgFlag -> AnonArgFlag -> Bool

max :: AnonArgFlag -> AnonArgFlag -> AnonArgFlag

min :: AnonArgFlag -> AnonArgFlag -> AnonArgFlag

Outputable AnonArgFlag

Defined in Var

Methods

ppr :: AnonArgFlag -> SDoc

pprPrec :: Rational -> AnonArgFlag -> SDoc

Binary AnonArgFlag

Defined in Var

Methods

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

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

get :: BinHandle -> IO AnonArgFlag

data ForallVisFlag

Is a forall invisible (e.g., forall a b. {...}, with a dot) or visible (e.g., forall a b -> {...}, with an arrow)?

Constructors

ForallVis

A visible forall (with an arrow)

ForallInvis

An invisible forall (with a dot)

Instances

Eq ForallVisFlag

Defined in Var

Methods

(==) :: ForallVisFlag -> ForallVisFlag -> Bool

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

Data ForallVisFlag

Defined in Var

Methods

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

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

toConstr :: ForallVisFlag -> Constr

dataTypeOf :: ForallVisFlag -> DataType

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

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

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

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

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

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

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

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

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

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

Ord ForallVisFlag

Defined in Var

Methods

compare :: ForallVisFlag -> ForallVisFlag -> Ordering

(<) :: ForallVisFlag -> ForallVisFlag -> Bool

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

(>) :: ForallVisFlag -> ForallVisFlag -> Bool

(>=) :: ForallVisFlag -> ForallVisFlag -> Bool

max :: ForallVisFlag -> ForallVisFlag -> ForallVisFlag

min :: ForallVisFlag -> ForallVisFlag -> ForallVisFlag

Outputable ForallVisFlag

Defined in Var

Methods

ppr :: ForallVisFlag -> SDoc

pprPrec :: Rational -> ForallVisFlag -> SDoc

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

CoVarCo CoVar

AxiomInstCo (CoAxiom Branched) BranchIndex [Coercion]

AxiomRuleCo CoAxiomRule [Coercion]

UnivCo UnivCoProvenance Role Type Type

SymCo Coercion

TransCo Coercion Coercion

NthCo Role Int 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 TyCoRep

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 :: (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 TyCoRep

Methods

ppr :: Coercion -> SDoc

pprPrec :: Rational -> Coercion -> SDoc

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

UnsafeCoerceProv

From unsafeCoerce#. These are unsound.

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.

Instances

Data UnivCoProvenance

Defined in TyCoRep

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 :: (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 TyCoRep

Methods

ppr :: UnivCoProvenance -> SDoc

pprPrec :: Rational -> 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 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

Defined in TyCoRep

Methods

ppr :: CoercionHole -> SDoc

pprPrec :: Rational -> 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 TyCoRep

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 :: (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 TyCoRep

Methods

ppr :: MCoercion -> SDoc

pprPrec :: Rational -> MCoercion -> SDoc

type MCoercionR = MCoercion

type MCoercionN = MCoercion

Functions over types

mkTyConTy :: TyCon -> Type

Create the plain type constructor type which has been applied to no type arguments at all.

mkTyVarTy :: TyVar -> Type

mkTyVarTys :: [TyVar] -> [Type]

mkTyCoVarTy :: TyCoVar -> Type

mkTyCoVarTys :: [TyCoVar] -> [Type]

mkFunTy :: AnonArgFlag -> Type -> Type -> Type infixr 3

mkVisFunTy :: Type -> Type -> Type infixr 3

mkInvisFunTy :: Type -> Type -> Type infixr 3

mkVisFunTys :: [Type] -> Type -> Type

Make nested arrow types

mkInvisFunTys :: [Type] -> Type -> Type

Make nested arrow types

mkForAllTy :: TyCoVar -> ArgFlag -> Type -> Type

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

mkForAllTys :: [TyCoVarBinder] -> Type -> Type

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

mkPiTy :: TyCoBinder -> Type -> Type

mkPiTys :: [TyCoBinder] -> Type -> Type

Functions over binders

data TyCoBinder

A TyCoBinder represents an argument to a function. TyCoBinders can be dependent (Named) or nondependent (Anon). They may also be visible or not. See Note [TyCoBinders]

Constructors

Named TyCoVarBinder

Anon AnonArgFlag Type

Instances

Data TyCoBinder

Defined in TyCoRep

Methods

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

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

toConstr :: TyCoBinder -> Constr

dataTypeOf :: TyCoBinder -> DataType

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

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

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

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

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

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

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

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

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

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

Outputable TyCoBinder

Defined in TyCoRep

Methods

ppr :: TyCoBinder -> SDoc

pprPrec :: Rational -> TyCoBinder -> SDoc

type TyCoVarBinder = VarBndr TyCoVar ArgFlag

Variable Binder

A TyCoVarBinder is the binder of a ForAllTy It's convenient to define this synonym here rather its natural home in TyCoRep, because it's used in DataCon.hs-boot

A TyVarBinder is a binder with only TyVar

type TyBinder = TyCoBinder

TyBinder is like TyCoBinder, but there can only be TyVarBinder in the Named field.

binderVar :: VarBndr tv argf -> tv

binderVars :: [VarBndr tv argf] -> [tv]

binderType :: VarBndr TyCoVar argf -> Type

binderArgFlag :: VarBndr tv argf -> argf

delBinderVar :: VarSet -> TyCoVarBinder -> VarSet

Remove the binder's variable from the set, if the binder has a variable.

isInvisibleArgFlag :: ArgFlag -> Bool

Does this ArgFlag classify an argument that is not written in Haskell?

isVisibleArgFlag :: ArgFlag -> Bool

Does this ArgFlag classify an argument that is written in Haskell?

isInvisibleBinder :: TyCoBinder -> Bool

Does this binder bind an invisible argument?

isVisibleBinder :: TyCoBinder -> Bool

Does this binder bind a visible argument?

isTyBinder :: TyCoBinder -> Bool

If its a named binder, is the binder a tyvar? Returns True for nondependent binder. This check that we're really returning a *Ty*Binder (as opposed to a coercion binder). That way, if/when we allow coercion quantification in more places, we'll know we missed updating some function.

isNamedBinder :: TyCoBinder -> Bool

Functions over coercions

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

Sizes

typeSize :: Type -> Int

coercionSize :: Coercion -> Int

provSize :: UnivCoProvenance -> Int