Types are one of:

Unboxed

Iff its representation is other than a pointer Unboxed types are also unlifted.

Lifted

Iff it has bottom as an element. Closures always have lifted types: i.e. any let-bound identifier in Core must have a lifted type. Operationally, a lifted object is one that can be entered. Only lifted types may be unified with a type variable.

Algebraic

Iff it is a type with one or more constructors, whether declared with data or newtype. An algebraic type is one that can be deconstructed with a case expression. This is not the same as lifted types, because we also include unboxed tuples in this classification.

Data

Iff it is a type declared with data, or a boxed tuple.

Primitive

Iff it is a built-in type that can't be expressed in Haskell.

Currently, all primitive types are unlifted, but that's not necessarily the case: for example, Int could be primitive.

Some primitive types are unboxed, such as Int#, whereas some are boxed but unlifted (such as ByteArray#). The only primitive types that we classify as algebraic are the unboxed tuples.

Some examples of type classifications that may make this a bit clearer are:

 Type         primitive       boxed           lifted          algebraic
 -----------------------------------------------------------------------------
 Int#         Yes             No              No              No
 ByteArray#   Yes             Yes             No              No
 (# a, b #)   Yes             No              No              Yes
 (  a, b  )   No              Yes             Yes             Yes
 [a]          No              Yes             Yes             Yes

A source type is a type that is a separate type as far as the type checker is concerned, but which has a more low-level representation as far as Core-to-Core passes and the rest of the back end is concerned. Notably, PredTys are removed from the representation type while they do exist in the source types.

You don't normally have to worry about this, as the utility functions in this module will automatically convert a source into a representation type if they are spotted, to the best of it's abilities. If you don't want this to happen, use the equivalent functions from the TcType module.

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

2. 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, via dressing up polymorphic types with newtype clothing. Here's an example:

 newtype R = R (forall a. a->a)
 foo = case undefined :: R of
            R f -> f ()

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)

We may be strict in dictionary types, but only if it has more than one component.

(Being strict in a single-component dictionary risks poking the dictionary component, which is wrong.)

There's a little subtyping at the kind level:

               ?
              / \
             /   \
            ??   (#)
           /  \
          *    #
 .
 Where:        *    [LiftedTypeKind]   means boxed type
              #    [UnliftedTypeKind] means unboxed type
              (#)  [UbxTupleKind]     means unboxed tuple
              ??   [ArgTypeKind]      is the lub of {*, #}
              ?    [OpenTypeKind]	means any type at all

In particular:

 error :: forall a:?. String -> a
 (->)  :: ?? -> ? -> \*
 (\\(x::t) -> ...)

Where in the last example t :: ?? (i.e. is not an unboxed tuple)

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)

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.

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.

In the case of newtypes, it returns one of:

1) A vanilla TyConApp (recursive newtype, or non-saturated)

2) The newtype representation (otherwise), meaning the type written in the RHS of the newtype declaration, which may itself be a newtype

For example, with:

 newtype R = MkR S
 newtype S = MkS T
 newtype T = MkT (T -> T)

expandNewTcApp on:

• R gives Just S * S gives Just T * T gives Nothing (no expansion)

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.

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