+ We will slightly limit our view on Core's type system, since the more
+ complicated parts of it are only meant to support Haskell's (or rather,
+ \GHC's) type extensions, such as existential types, type families and
+ other non-standard Haskell stuff which we don't (plan to) support.
+
+ In Core, every expression is typed. The translation to Core happens
+ after the typechecker, so types in Core are always correct as well
+ (though you could of course construct invalidly typed expressions).
+
+ Any type in core is one of the following:
+
+ \startdesc{A type variable}
+ \startlambda
+ a
+ \stoplambda
+
+ This is a reference to a type defined elsewhere. This can either be a
+ polymorphic type (like \hs{a} in \hs{id :: a -> a}), or a type
+ constructor (like \hs{Bool} in \hs{null :: [a] -> Bool}).
+
+ A special case of a type constructor is the \emph{function type
+ constructor}, \hs{->}. This is a type constructor taking two arguments
+ (using application below). The function type constructor is commonly
+ written inline, so we write \hs{a -> b} when we really mean \hs{-> a
+ b}, the function type constructor applied to a and b.
+
+ Polymorphic type variables can only be defined by a lambda
+ abstraction, see the forall type below.
+ \stopdesc
+
+ \startdesc{A type application}
+ \startlambda
+ Maybe Int
+ \stoplambda
+
+ This applies a some type to another type. This is particularly used to
+ apply type variables (type constructors) to their arguments.
+
+ As mentioned above, some type applications have special notation. In
+ particular, these are applications of the \emph{function type
+ constructor} and \emph{tuple type constructors}:
+ \starthaskell
+ foo :: a -> b
+ foo' :: -> a b
+ bar :: (a, b, c)
+ bar' :: (,,) a b c
+ \stophaskell
+ \stopdesc
+
+ \startdesc{The forall type}
+ \startlambda
+ id :: \forall a . a -> a
+ \stoplambda
+ The forall type introduces polymorphism. It is the only way to
+ introduce new type variables, which are completely unconstrained (Any
+ possible type can be assigned to it). Constraints can be added later
+ using predicate types, see below.
+
+ A forall type is always (and only) introduced by a type lambda
+ expression. For example, the Core translation of the
+ id function is:
+ \startlambda
+ id = λa.λx.x
+ \stoplambda
+
+ here, type type of the binder \lam{x} is \lam{a}, referring to the
+ binder in the topmost lambda.
+
+ When using a value with a forall type, the actual type
+ used must be applied first. For example haskell expression \hs{id
+ True} translates to the following Core:
+
+ \startlambda
+ id @Bool True
+ \stoplambda
+
+ Here, id is first applied to the type to work with. Note that the type
+ then changes from \lam{id :: \forall a . a -> a} to \lam{id @Bool ::
+ Bool -> Bool}. Note that the type variable \lam{a} has been
+ substituted with the actual type.
+ \stopdesc
+
+ \startdesc{Predicate type}
+ \startlambda
+ show :: \forall a. Show s => s -> String
+ \stoplambda
+
+ TODO: Introduce type classes?
+
+ A predicate type introduces a constraint on a type variable introduced
+ by a forall type (or type lambda). In the example above, the type
+ variable \lam{a} can only contain types that are an \emph{instance} of
+ the \emph{type class} \lam{Show}.
+
+ There are other sorts of predicate types, used for the type families
+ extension, which we will not discuss here.
+
+ A predicate type is introduced by a lambda abstraction. Unlike with
+ the forall type, this is a value lambda abstraction, that must be
+ applied to a value. We call this value a \emph{dictionary}.
+
+ Without going into the implementation details, a dictionary can be
+ seen as a lookup table all the methods for a given (single) type class
+ instance. This means that all the dictionaries for the same type class
+ look the same (\eg contain methods with the same names). However,
+ dictionaries for different instances of the same class contain
+ different methods, of course.
+
+ A dictionary is introduced by \small{GHC} whenever it encounters an
+ instance declaration. This dictionary, as well as the binder
+ introduced by a lambda that introduces a dictionary, have the
+ predicate type as their type. These binders are usually named starting
+ with a \lam{\$}. Usually the name of the type concerned is not
+ reflected in the name of the dictionary, but the name of the type
+ class is. The Haskell expression \hs{show True} thus becomes:
+
+ \startlambda
+ show @Bool $dShow True
+ \stoplambda
+ \stopdesc
+
+ Using this set of types, all types in basic Haskell can be represented.
+