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.

The key representation of types within the compiler

The key type representing kinds in the compiler.

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

A type of the form p of kind Constraint 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"

A collection of PredTypes

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

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

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.

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

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

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

Make an arrow type

Make nested arrow types

If tv is a coercion variable and it is not used in the body, returns a FunTy, otherwise makes a forall type. See Note [Unused coercion variable in ForAllTy]

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

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

Like mkTyCoPiTys, but does not check the occurrence of the binder

Given a kind (TYPE rr), extract its RuntimeRep classifier rr. For example, kindRep_maybe * = Just LiftedRep Returns Nothing if the kind is not of form (TYPE rr) Treats * and Constraint as the same

Extract the RuntimeRep classifier of a type from its kind. For example, kindRep * = LiftedRep; Panics if this is not possible. Treats * and Constraint as the same

This version considers Constraint to be the same as *. Returns True if the argument is equivalent to Type/Constraint and False otherwise. See Note [Kind Constraint and kind Type]

Returns True if the kind classifies unlifted types and False otherwise. Note that this returns False for levity-polymorphic kinds, which may be specialized to a kind that classifies unlifted types.

Is this the type RuntimeRep?

Is a tyvar of type RuntimeRep?

Do these denote the same level of visibility? Required arguments are visible, others are not. So this function equates Specified and Inferred. Used for printing.

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]

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

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

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

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

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

Does this binder bind an invisible argument?

Does this binder bind a visible argument?

If its a named binder, is the binder a tyvar? Returns True for nondependent binder.

Print a user-level forall; see Note [When to print foralls]

A general-purpose pretty-printing precedence type.

Display all kind information (with -fprint-explicit-kinds) when the provided Bool argument is True. See Note [Kind arguments in error messages] in TcErrors.

debugPprType is a simple pretty printer that prints a type without going through IfaceType. It does not format as prettily as the normal route, but it's much more direct, and that can be useful for debugging. E.g. with -dppr-debug it prints the kind on type-variable occurrences which the normal route fundamentally cannot do.

tyCoFVsOfType that returns free variables of a type in a deterministic set. For explanation of why using VarSet is not deterministic see Note [Deterministic FV] in FV.

Returns free variables of types, including kind variables as a deterministic set. For type synonyms it does not expand the synonym.

The worker for tyCoFVsOfType and tyCoFVsOfTypeList. The previous implementation used unionVarSet which is O(n+m) and can make the function quadratic. It's exported, so that it can be composed with other functions that compute free variables. See Note [FV naming conventions] in FV.

Eta-expanded because that makes it run faster (apparently) See Note [FV eta expansion] in FV for explanation.

tyCoFVsOfType that returns free variables of a type in deterministic order. For explanation of why using VarSet is not deterministic see Note [Deterministic FV] in FV.

Returns free variables of types, including kind variables as a deterministically ordered list. For type synonyms it does not expand the synonym.

Get a deterministic set of the vars free in a coercion

Given a covar and a coercion, returns True if covar is almost devoid in the coercion. That is, covar can only appear in Refl and GRefl. See last wrinkle in Note [Unused coercion variable in ForAllCo] in Coercion

Returns the free variables of a Type that are in injective positions. For example, if F is a non-injective type family, then:

injectiveTyVarsOf( Either c (Maybe (a, F b c)) ) = {a,c}

If injectiveVarsOfType ty = itvs, then knowing ty fixes itvs. More formally, if a is in injectiveVarsOfType ty and S1(ty) ~ S2(ty), then S1(a) ~ S2(a), where S1 and S2 are arbitrary substitutions.

See Note [When does a tycon application need an explicit kind signature?].

Does a TyCon (that is applied to some number of arguments) need to be ascribed with an explicit kind signature to resolve ambiguity if rendered as a source-syntax type? (See Note [When does a tycon application need an explicit kind signature?] for a full explanation of what this function checks for.)

Returns True if this type has no free variables. Should be the same as isEmptyVarSet . tyCoVarsOfType, but faster in the non-forall case.

Returns True if this coercion has no free variables. Should be the same as isEmptyVarSet . tyCoVarsOfCo, but faster in the non-forall case.

Type & coercion substitution

The following invariants must hold of a TCvSubst:

1. The in-scope set is needed only to guide the generation of fresh uniques
2. In particular, the kind of the type variables in the in-scope set is not relevant
3. The substitution is only applied ONCE! This is because in general such application will not reach a fixed point.

A substitution of Types for TyVars and Kinds for KindVars

A substitution of Coercions for CoVars

(compose env1 env2)(x) is env1(env2(x)); i.e. apply env2 then env1. It assumes that both are idempotent. Typically, env1 is the refinement to a base substitution env2

Composes two substitutions, applying the second one provided first, like in function composition.

Make a TCvSubst with specified tyvar subst and empty covar subst

Make a TCvSubst with specified covar subst and empty tyvar subst

Returns the free variables of the types in the range of a substitution as a non-deterministic set.

Generates an in-scope set from the free variables in a list of types and a list of coercions

Generates the in-scope set for the TCvSubst from the types in the incoming environment. No CoVars, please!

Generates the in-scope set for the TCvSubst from the types in the incoming environment. No TyVars, please!

Generates the in-scope set for the TCvSubst from the types in the incoming environment. No CoVars, please!

Type substitution, see zipTvSubst

Substitute covars within a type

Type substitution, see zipTvSubst

Type substitution, see zipTvSubst

Coercion substitution, see zipTvSubst

Substitute within a Type The substitution has to satisfy the invariants described in Note [The substitution invariant].

Substitute within a Type after adding the free variables of the type to the in-scope set. This is useful for the case when the free variables aren't already in the in-scope set or easily available. See also Note [The substitution invariant].

Substitute within a Type disabling the sanity checks. The problems that the sanity checks in substTy catch are described in Note [The substitution invariant]. The goal of #11371 is to migrate all the calls of substTyUnchecked to substTy and remove this function. Please don't use in new code.

Substitute within several Types disabling the sanity checks. The problems that the sanity checks in substTys catch are described in Note [The substitution invariant]. The goal of #11371 is to migrate all the calls of substTysUnchecked to substTys and remove this function. Please don't use in new code.

Substitute within a ThetaType disabling the sanity checks. The problems that the sanity checks in substTys catch are described in Note [The substitution invariant]. The goal of #11371 is to migrate all the calls of substThetaUnchecked to substTheta and remove this function. Please don't use in new code.

Type substitution, see zipTvSubst. Disables sanity checks. The problems that the sanity checks in substTy catch are described in Note [The substitution invariant]. The goal of #11371 is to migrate all the calls of substTyUnchecked to substTy and remove this function. Please don't use in new code.

Substitute within a Coercion disabling sanity checks. The problems that the sanity checks in substCo catch are described in Note [The substitution invariant]. The goal of #11371 is to migrate all the calls of substCoUnchecked to substCo and remove this function. Please don't use in new code.

Coercion substitution, see zipTvSubst. Disables sanity checks. The problems that the sanity checks in substCo catch are described in Note [The substitution invariant]. The goal of #11371 is to migrate all the calls of substCoUnchecked to substCo and remove this function. Please don't use in new code.

Substitute tyvars within a type using a known InScopeSet. Pre-condition: the in_scope set should satisfy Note [The substitution invariant]; specifically it should include the free vars of tys, and of ty minus the domain of the subst.

Substitute within several Types The substitution has to satisfy the invariants described in Note [The substitution invariant].

Substitute within a ThetaType The substitution has to satisfy the invariants described in Note [The substitution invariant].

Substitute within a Coercion The substitution has to satisfy the invariants described in Note [The substitution invariant].

Substitute within several Coercions The substitution has to satisfy the invariants described in Note [The substitution invariant].

This checks if the substitution satisfies the invariant from Note [The substitution invariant].

When calling substTy it should be the case that the in-scope set in the substitution is a superset of the free vars of the range of the substitution. See also Note [The substitution invariant].

Grabs the free type variables, tidies them and then uses tidyType to work over the type itself

This tidies up a type for printing in an error message, or in an interface file.

It doesn't change the uniques at all, just the print names.

Add the free TyVars to the env in tidy form, so that we can tidy the type they are free in

Treat a new TyCoVar as a binder, and give it a fresh tidy name using the environment if one has not already been allocated. See also tidyVarBndr

Calls tidyType on a top-level type (i.e. with an empty tidying environment)