A typecheckable-thing, essentially anything that has a name

The key representation of types within the compiler

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

Essentially a typed Name, that may also contain some additional information about the Var and it's use sites.

Attempts to obtain the type variable underlying a Type, and panics with the given message if this is not a type variable type. See also getTyVar_maybe

Attempts to obtain the type variable underlying a Type

Applies a type to another, as in e.g. k a

Attempts to take a type application apart, as in splitAppTy_maybe, and panics if this is not possible

Recursively splits a type as far as is possible, leaving a residual type being applied to and the type arguments applied to it. Never fails, even if that means returning an empty list of type applications.

Attempt to take a type application apart, whether it is a function, type constructor, or plain type application. Note that type family applications are NEVER unsaturated by this!

Does the AppTy split as in splitAppTy_maybe, but assumes that any Core view stuff is already done

Creates a function type from the given argument and result type

Attempts to extract the argument and result types from a type, and panics if that is not possible. See also splitFunTy_maybe

Attempts to extract the argument and result types from a type

Split off exactly the given number argument types, and panics if that is not possible

Extract the function result type and panic if that is not possible

Extract the function argument type and panic if that is not possible

Splits off argument types from the given type and associating them with the things in the input list from left to right. The final result type is returned, along with the resulting pairs of objects and types, albeit with the list of pairs in reverse order. Panics if there are not enough argument types for the input list.

A key function: builds a TyConApp or FunTy as apppropriate to its arguments. Applies its arguments to the constructor from left to right.

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

The same as fst . splitTyConApp

The same as snd . splitTyConApp

Attempts to tease a type apart into a type constructor and the application of a number of arguments to that constructor

Attempts to tease a type apart into a type constructor and the application of a number of arguments to that constructor. Panics if that is not possible. See also splitTyConApp_maybe

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

Attempts to take a forall type apart, returning the bound type variable and the remainder of the type

Attempts to take a forall type apart, returning all the immediate such bound type variables and the remainder of the type. Always suceeds, even if that means returning an empty list of TyVars

Makes a (->) type or a forall type, depending on whether it is given a type variable or a term variable.

mkPiType for multiple type or value arguments

Instantiate a forall type with one or more type arguments. Used when we have a polymorphic function applied to type args:

f t1 t2

We use applyTys type-of-f [t1,t2] to compute the type of the expression. Panics if no application is possible.

This function is interesting because:

1. The function may have more for-alls than there are args
   1. Less obviously, it may have fewer for-alls

For case 2. think of:

applyTys (forall a.a) [forall b.b, Int]

This really can happen, but only (I think) in situations involving undefined. For example: undefined :: forall a. a Term: undefined (forall b. b->b) Int This term should have type (Int -> Int), but notice that there are more type args than foralls in undefineds type.

Equivalent to snd . splitForAllTys

Is this a numeric literal. We also look through type synonyms.

Is this a symbol literal. We also look through type synonyms.

Get the type on the LHS of a coercion induced by a type/data family instance.

Unwrap one layer of newtype on a type constructor and its arguments, using an eta-reduced version of the newtype if possible. This requires tys to have at least newTyConInstArity tycon elements.

Given a family instance TyCon and its arg types, return the corresponding family type. E.g:

data family T a
data instance T (Maybe b) = MkT b

Where the instance tycon is :RTL, so:

mkFamilyTyConApp :RTL Int  =  T (Maybe Int)

Creates a type equality predicate

See Type for what an unlifted type is

See Type for what an algebraic type is. Should only be applied to types, as opposed to e.g. partially saturated type constructors

See Type for what an algebraic type is. Should only be applied to types, as opposed to e.g. partially saturated type constructors. Closed type constructors are those with a fixed right hand side, as opposed to e.g. associated types

Returns true of types that are opaque to Haskell. Most of these are unlifted, but now that we interact with .NET, we may have primtive (foreign-imported) types that are lifted

Computes whether an argument (or let right hand side) should be computed strictly or lazily, based only on its type. Currently, it's just isUnLiftedType.

The key type representing kinds in the compiler. Invariant: a kind is always in one of these forms:

FunTy k1 k2
TyConApp PrimTyCon [...]
TyVar kv   -- (during inference only)
ForAll ... -- (for top-level coercions)

See Type for details of the distinction between these Kinds

See Type for details of the distinction between these Kinds

See Type for details of the distinction between these Kinds

See Type for details of the distinction between these Kinds

See Type for details of the distinction between these Kinds

See Type for details of the distinction between these Kinds

See Type for details of the distinction between the Kind TyCons

See Type for details of the distinction between the Kind TyCons

See Type for details of the distinction between the Kind TyCons

See Type for details of the distinction between the Kind TyCons

See Type for details of the distinction between the Kind TyCons

NB: for type synonyms tyVarsOfType does not expand the synonym tyVarsOfType returns only the free variables of a type For example, tyVarsOfType (a::k) returns {a}, not including the kind variable {k}

Expand out all type synonyms. Actually, it'd suffice to expand out just the ones that discard type variables (e.g. type Funny a = Int) But we don't know which those are currently, so we just expand all.

Type equality on source types. Does not look through newtypes or PredTypes, but it does look through type synonyms. Watch out for horrible hack: See Note [Comparison with OpenTypeKind]

In Core, we "look through" non-recursive newtypes and PredTypes: this function tries to obtain a different view of the supplied type given this

Strips off the top layer only of a type to give its underlying representation type. Returns Nothing if there is nothing to look through.

By being non-recursive and inlined, this case analysis gets efficiently joined onto the case analysis that the caller is already doing

Similar to coreView, but for the type checker, which just looks through synonyms

Looks through:

1. For-alls
2. Synonyms
3. Predicates
4. All newtypes, including recursive ones, but not newtype families

It's useful in the back end of the compiler.

All type constructors occurring in the type; looking through type synonyms, but not newtypes. When it finds a Class, it returns the class TyCon.

Discovers the primitive representation of a more abstract UnaryType

A substitition of Types for TyVars and Kinds for KindVars

Type substitution

The following invariants must hold of a TvSubst:

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 substition is only applied ONCE! This is because in general such application will not reached a fixed point.

Generates the in-scope set for the TvSubst from the types in the incoming environment, hence "open"

Generates the in-scope set for the TvSubst from the types in the incoming environment, hence "open"

Called when doing top-level substitutions. Here we expect that the free vars of the range of the substitution will be empty.

(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

Substitute within a Type

Substitute within several Types

Type substitution making use of an TvSubst that is assumed to be open, see zipOpenTvSubst

Type substitution making use of an TvSubst that is assumed to be open, see zipOpenTvSubst

Substitute within a ThetaType

Remove any nested binders mentioning the TyVars in the TyVarSet

Pretty prints a TyCon, using the family instance in case of a representation tycon. For example:

data T [a] = ...

In that case we want to print T [a], where T is the family TyCon

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 TyVar as a binder, and give it a fresh tidy name using the environment if one has not already been allocated. See also tidyTyVarBndr

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