Type
and its friends
The data type GHC compiles a typed programming language, and GHC's intermediate language is explicitly typed. So the data type that GHC uses to represent types is of central importance.
The single data type Type
is used to represent
 Types (possibly of higher kind); e.g.
[Int]
,Maybe
 Kinds (which classify types and coercions); e.g.
(* > *)
,T :=: [Int]
. See Commentary/Compiler/Kinds  Sorts (which classify types); e.g.
TY
,CO
GHC's use of coercions and equality constraints is important enough to deserve its own page.
The module GHC.Core.TyCo.Rep
exposes the representation because a few other modules (GHC.Core.Type
, GHC.Tc.Utils.TcType
, GHC.Core.Unify
, etc) work directly on its representation. However, you should not lightly patternmatch on Type
; it is meant to be an abstract type. Instead, try to use functions defined by Type
, TcType
etc.
Views of types
Even when considering only types (not kinds, sorts, coercions) you need to know that GHC uses a single data type for types. You can look at the same type in different ways:

The "typechecker view" regards the type as a Haskell type, complete with implicit parameters, class constraints, and the like. For example:
forall a. (Eq a, ?x::Int) => a > Int
Functions in
TcType
take this view of types; e.g.tcSplitSigmaTy
splits up a type into its forall'd type variables, its constraints, and the rest. 
The "core view" regards the type as a Corelanguage type, where class and implicit parameter constraints are treated as function arguments:
forall a. Eq a > Int > a > Int
Functions in
Type
take this view.
The data type Type
represents type synonym applications in unexpanded form. E.g.
type T a = a > a
f :: T Int
Here f
's type doesn't look like a function type, but it really is. The function Type.coreView :: Type > Maybe Type
takes a type and, if it's a type synonym application, it expands the synonym and returns Just <expandedtype>
. Otherwise it returns Nothing
.
Now, other functions use coreView
to expand where necessary, thus:
splitFunTy_maybe :: Type > Maybe (Type,Type)
splitFunTy_maybe ty  Just ty' < coreView ty = splitFunTy_maybe ty'
splitFunTy_maybe (FunTy t1 t2) = Just (t1,t2)
splitFunTy_maybe other = Nothing
Notice the first line, which uses the view, and recurses when the view 'fires'. Since coreView
is nonrecursive, GHC will inline it, and the optimiser will ultimately produce something like:
splitFunTy_maybe :: Type > Maybe (Type,Type)
splitFunTy_maybe (PredTy p) = splitFunTy_maybe (predTypeRep p)
splitFunTy_maybe (NoteTy _ ty) = splitFunTy_maybe ty
splitFunTy_maybe (FunTy t1 t2) = Just (t1,t2)
splitFunTy_maybe other = Nothing
Type
The representation of Here, then is the representation of types (see compiler/GHC/Core/TyCo/Rep.hs for more details):
type TyVar = Var
data Type = TyVarTy TyVar  Type variable
 AppTy Type Type  Application
 TyConApp TyCon [Type]  Type constructor application
 FunTy Type Type  Arrow type
 ForAllTy Var Type  Polymorphic type
 LitTy TyLit  Type literals
data TyLit = NumTyLit Integer  A number
 StrTyLit FastString  A string
Invariant: if the head of a type application is a TyCon
, GHC always uses the TyConApp
constructor, not AppTy
.
This invariant is maintained internally by 'smart constructors'.
A similar invariant applies to FunTy
; TyConApp
is never used with an arrow type.
Type variables are represented by the TyVar
constructor of the data type Var.
Overloaded types
In Haskell we write
f :: forall a. Num a => a > a
but in Core the =>
is represented by an ordinary FunTy
. So f's type looks like this:
ForAllTy a (TyConApp num [TyVarTy a] `FunTy` TyVarTy a `FunTy` TyVarTy a)
where
a :: TyVar
num :: TyCon
Nevertheless, we can tell when a function argument is actually a predicate (and hence should be displayed with =>
, etc), using
isPredTy :: Type > Bool
The various forms of predicate can be extracted thus:
classifyPredType :: Type > PredTree
data PredTree = ClassPred Class [Type]  Class predicates e.g. (Num a)
 EqPred Type Type  Equality predicates e.g. (a ~ b)
 TuplePred [PredType]  Tuples of predicates e.g. (Num a, a~b)
 IrredPred PredType  Higher order predicates e.g. (c a)
These functions are defined in module Type
.
Classifying types
GHC uses the following nomenclature for types:
Unboxed  A type is unboxed iff its representation is other than a pointer. Unboxed types are also unlifted. 

Lifted  A type is lifted iff it has bottom as an element. Closures always have lifted types: i.e. any letbound 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. 

Data  A type declared with data. Also boxed tuples. 

Algebraic  An algebraic data type is a data 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. "Algebraic" is NOT the same as "lifted", because unboxed (and thus unlifted) tuples count as "algebraic". 

Primitive  a type is primitive iff it is a builtin type that can't be expressed in Haskell.
Currently, all primitive types are unlifted, but that's not necessarily the case. (E.g. 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.
Examples of type classifications:
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 