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 pattern-match 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:
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 Core-language type, where class and implicit parameter constraints are treated as function arguments:
Functions in Type take this view.
The data type Type represents type synonym applications in un-expanded form. E.g.
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 <expanded-type>. Otherwise it returns Nothing.
Now, other functions use coreView to expand where necessary, thus:
typeTyVar=VardataType=TyVarTyTyVar-- Type variable|AppTyTypeType-- Application|TyConAppTyCon[Type]-- Type constructor application|FunTyTypeType-- Arrow type|ForAllTyVarType-- Polymorphic type|LitTyTyLit-- Type literalsdataTyLit=NumTyLitInteger-- A number|StrTyLitFastString-- 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.
In Haskell we write
but in Core the => is represented by an ordinary FunTy. So f's type looks like this:
Nevertheless, we can tell when a function argument is actually a predicate (and hence should be displayed with =>, etc), using
The various forms of predicate can be extracted thus:
classifyPredType::Type->PredTreedataPredTree=ClassPredClass[Type]-- Class predicates e.g. (Num a)|EqPredTypeType-- Equality predicates e.g. (a ~ b)|TuplePred[PredType]-- Tuples of predicates e.g. (Num a, a~b)|IrredPredPredType-- Higher order predicates e.g. (c a)
These functions are defined in module Type.
GHC uses the following nomenclature for types:
A type is unboxed iff its representation is other than a pointer. Unboxed types are also unlifted.
A type is 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.
A type declared with data. Also boxed tuples.
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".
a type is 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. (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.