+ </p>
+
+ <h4>Type Representation</h4>
+ <p>
+ The representation of types is fixed in the module <a
+ href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/typecheck/TcRep.lhs"><code>TcRep</code></a>
+ and exported as the data type <code>Type</code>. As explained in <a
+ href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/typecheck/TcType.lhs"><code>TcType</code></a>,
+ GHC supports rank-N types, but, in the type checker, maintains the
+ restriction that type variables cannot be instantiated to quantified
+ types (i.e., the type system is predicative). The type checker floats
+ universal quantifiers outside and maintains types in prenex form.
+ (However, quantifiers can, of course, not float out of negative
+ positions.) Overall, we have
+ </p>
+ <blockquote>
+ <pre>
+sigma -> forall tyvars. phi
+phi -> theta => rho
+rho -> sigma -> rho
+ | tau
+tau -> tyvar
+ | tycon tau_1 .. tau_n
+ | tau_1 tau_2
+ | tau_1 -> tau_2</pre>
+ </blockquote>
+ <p>
+ where <code>sigma</code> is in prenex form; i.e., there is never a
+ forall to the right of an arrow in a <code>phi</code> type. Moreover, a
+ type of the form <code>tau</code> never contains a quantifier (which
+ includes arguments to type constructors).
+ </p>
+ <p>
+ Of particular interest are the variants <code>SourceTy</code> and
+ <code>NoteTy</code> of <a
+ href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/typecheck/TypeRep.lhs"><code>TypeRep</code></a>.<code>Type</code>.
+ The constructor <code>SourceTy :: SourceType -> Type</code> represents a
+ type constraint; that is, a predicate over types represented by a
+ dictionary. The type checker treats a <code>SourceTy</code> as opaque,
+ but during the translation to core it will be expanded into its concrete
+ representation (i.e., a dictionary type) by the function <a
+ href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/types/Type.lhs"><code>Type</code></a>.<code>sourceTypeRep</code>.
+ Note that newtypes are not covered by <code>SourceType</code>s anymore,
+ even if some comments in GHC still suggest this. Instead, all newtype
+ applications are initially represented as a <code>NewTcApp</code>, until
+ they are eliminated by calls to <a
+ href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/types/Type.lhs"><code>Type</code></a>.<code>newTypeRep</code>.
+ </p>
+ <p>
+ The <code>NoteTy</code> constructor is used to add non-essential
+ information to a type term. Such information has the type
+ <code>TypeRep.TyNote</code> and is either the set of free type variables
+ of the annotated expression or the unexpanded version of a type synonym.
+ Free variables sets are cached as notes to save the overhead of
+ repeatedly computing the same set for a given term. Unexpanded type
+ synonyms are useful for generating comprehensible error messages, but
+ have no influence on the process of type checking.
+ </p>