+ \subsection[sec:prototype:coretypes]{Core type system}
+ Whereas the expression syntax of Core is very simple, its type system is
+ a bit more complicated. It turns out it is harder to \quote{desugar}
+ Haskell's complex type system into something more simple. Most of the
+ type system is thus very similar to that of Haskell.
+
+ 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, \small{GADT}s, 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
+ t
+ \stoplambda
+
+ This is a reference to a type defined elsewhere. This can either be a
+ polymorphic type (like the latter two \lam{t}'s in \lam{id :: \forall t.
+ t -> t}), or a type constructor (like \lam{Bool} in \lam{not :: Bool ->
+ Bool}). Like in Haskell, polymorphic type variables always
+ start with a lowercase letter, while type constructors always start
+ with an uppercase letter.
+
+ \todo{How to define (new) type constructors?}
+
+ A special case of a type constructor is the \emph{function type
+ constructor}, \lam{->}. This is a type constructor taking two arguments
+ (using application below). The function type constructor is commonly
+ written inline, so we write \lam{a -> b} when we really mean \lam{-> a
+ b}, the function type constructor applied to \lam{a} and \lam{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, applications of some type constructors have
+ special notation. In particular, these are applications of the
+ \emph{function type constructor} and \emph{tuple type constructors}:
+ \startlambda
+ foo :: a -> b
+ foo' :: -> a b
+ bar :: (a, b, c)
+ bar' :: (,,) a b c
+ \stoplambda
+ \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, the 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} (the function \hs{id} appleid to the dataconstructor \hs{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.
+
+ In Haskell, forall types are usually not explicitly specified (The use
+ of a lowercase type variable implicitly introduces a forall type for
+ that variable). In fact, in standard Haskell there is no way to
+ explicitly specify forall types. Through a language extension, the
+ \hs{forall} keyword is available, but still optional for normal forall
+ types (it is needed for \emph{existentially quantified types}, which
+ Cλash does not support).
+ \stopdesc