--- /dev/null
+<!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
+<html>
+ <head>
+ <META HTTP-EQUIV="Content-Type" CONTENT="text/html; charset=ISO-8859-1">
+ <title>The GHC Commentary - Checking Types</title>
+ </head>
+
+ <body BGCOLOR="FFFFFF">
+ <h1>The GHC Commentary - Checking Types</h1>
+ <p>
+ Probably the most important phase in the frontend is the type checker,
+ which is located at <a
+ href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/typecheck/"><code>fptools/ghc/compiler/typecheck/</code>.</a>
+ GHC type checks programs in their original Haskell form before the
+ desugarer converts them into Core code. This complicates the type
+ checker as it has to handle the much more verbose Haskell AST, but it
+ improves error messages, as those message are based on the same
+ structure that the user sees.
+ </p>
+ <p>
+ GHC defines the abstract syntax of Haskell programs in <a
+ href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/hsSyn/HsSyn.lhs"><code>HsSyn</code></a>
+ using a structure that abstracts over the concrete representation of
+ bound occurences of identifiers and patterns. The module <a
+ href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/typecheck/TcHsSyn.lhs"><code>TcHsSyn</code></a>
+ defines a number of helper function required by the type checker. Note
+ that the type <a
+ href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/typecheck/TcRnTypes.lhs"><code>TcRnTypes</code></a>.<code>TcId</code>
+ used to represent identifiers in some signatures during type checking
+ is, in fact, nothing but a synonym for a <a href="vars.html">plain
+ <code>Id</code>.</a>
+ </p>
+ <p>
+ It is also noteworthy, that the representations of types changes during
+ type checking from <code>HsType</code> to <code>TypeRep.Type</code>.
+ The latter is a <a href="types.html">hybrid type representation</a> that
+ is used to type Core, but still contains sufficient information to
+ recover source types. In particular, the type checker maintains and
+ compares types in their <code>Type</code> form.
+ </p>
+
+ <h2>The Overall Flow of Things</h2>
+
+ <h4>Entry Points Into the Type Checker</h4>
+ <p>
+ The interface of the type checker (and <a
+ href="renamer.html">renamer</a>) to the rest of the compiler is provided
+ by <a
+ href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/typecheck/TcRnDriver.lhs"><code>TcRnDriver</code></a>.
+ Entire modules are processed by calling <code>tcRnModule</code> and GHCi
+ uses <code>tcRnStmt</code>, <code>tcRnExpr</code>, and
+ <code>tcRnType</code> to typecheck statements and expressions, and to
+ kind check types, respectively. Moreover, <code>tcRnExtCore</code> is
+ provided to typecheck external Core code. Moreover,
+ <code>tcTopSrcDecls</code> is used by Template Haskell - more
+ specifically by <code>TcSplice.tc_bracket</code>
+ - to type check the contents of declaration brackets.
+ </p>
+
+ <h4>Renaming and Type Checking a Module</h4>
+ <p>
+ The function <code>tcRnModule</code> controls the complete static
+ analysis of a Haskell module. It sets up the combined renamer and type
+ checker monad, resolves all import statements, initiates the actual
+ renaming and type checking process, and finally, wraps off by processing
+ the export list.
+ </p>
+ <p>
+ The actual type checking and renaming process is initiated via
+ <code>TcRnDriver.tcRnSrcDecls</code>, which uses a helper called
+ <code>tc_rn_src_decls</code> to implement the iterative renaming and
+ type checking process required by <a href="../exts/th.html">Template
+ Haskell</a>. However, before it invokes <code>tc_rn_src_decls</code>,
+ it takes care of hi-boot files; afterwards, it simplifies type
+ constraints and zonking (see below regarding the later).
+ </p>
+ <p>
+ The function <code>tc_rn_src_decls</code> partitions static analysis of
+ a whole module into multiple rounds, where the initial round is followed
+ by an additional one for each toplevel splice. It collects all
+ declarations up to the next splice into an <code>HsDecl.HsGroup</code>
+ to rename and type check that <em>declaration group</em> by calling
+ <code>TcRnDriver.tcRnGroup</code>. Afterwards, it executes the
+ splice (if there are any left) and proceeds to the next group, which
+ includes the declarations produced by the splice.
+ </p>
+ <p>
+ The function <code>tcRnGroup</code>, finally, gets down to invoke the
+ actual renaming and type checking via
+ <code>TcRnDriver.rnTopSrcDecls</code> and
+ <code>TcRnDriver.tcTopSrcDecls</code>, respectively. The renamer, apart
+ from renaming, computes the global type checking environment, of type
+ <code>TcRnTypes.TcGblEnv</code>, which is stored in the type checking
+ monad before type checking commences.
+ </p>
+
+ <h2>Type Checking a Declaration Group</h2>
+ <p>
+ The type checking of a declaration group, performed by
+ <code>tcTopSrcDecls</code> starts by processing of the type and class
+ declarations of the current module, using the function
+ <code>TcTyClsDecls.tcTyAndClassDecls</code>. This is followed by a
+ first round over instance declarations using
+ <code>TcInstDcls.tcInstDecls1</code>, which in particular generates all
+ additional bindings due to the deriving process. Then come foreign
+ import declarations (<code>TcForeign.tcForeignImports</code>) and
+ default declarations (<code>TcDefaults.tcDefaults</code>).
+ </p>
+ <p>
+ Now, finally, toplevel value declarations (including derived ones) are
+ type checked using <code>TcBinds.tcTopBinds</code>. Afterwards,
+ <code>TcInstDcls.tcInstDecls2</code> traverses instances for the second
+ time. Type checking concludes with processing foreign exports
+ (<code>TcForeign.tcForeignExports</code>) and rewrite rules
+ (<code>TcRules.tcRules</code>). Finally, the global environment is
+ extended with the new bindings.
+ </p>
+
+ <h2>Type checking Type and Class Declarations</h2>
+ <p>
+ Type and class declarations are type checked in a couple of phases that
+ contain recursive dependencies - aka <em>knots.</em> The first knot
+ encompasses almost the whole type checking of these declarations and
+ forms the main piece of <code>TcTyClsDecls.tcTyAndClassDecls</code>.
+ </p>
+ <p>
+ Inside this big knot, the first main operation is kind checking, which
+ again involves a knot. It is implemented by <code>kcTyClDecls</code>,
+ which performs kind checking of potentially recursively-dependent type
+ and class declarations using kind variables for initially unknown kinds.
+ During processing the individual declarations some of these variables
+ will be instantiated depending on the context; the rest gets by default
+ kind <code>*</code> (during <em>zonking</em> of the kind signatures).
+ Type synonyms are treated specially in this process, because they can
+ have an unboxed type, but they cannot be recursive. Hence, their kinds
+ are inferred in dependency order. Moreover, in contrast to class
+ declarations and other type declarations, synonyms are not entered into
+ the global environment as a global <code>TyThing</code>.
+ (<code>TypeRep.TyThing</code> is a sum type that combines the various
+ flavours of typish entities, such that they can be stuck into type
+ environments and similar.)
+ </p>
+
+ <h2>More Details</h2>
+
+ <h4>Types Variables and Zonking</h4>
+ <p>
+ During type checking type variables are represented by mutable variables
+ - cf. the <a href="vars.html#TyVar">variable story.</a> Consequently,
+ unification can instantiate type variables by updating those mutable
+ variables. This process of instantiation is (for reasons that elude me)
+ called <a
+ href="http://www.dictionary.com/cgi-bin/dict.pl?term=zonk&db=*">zonking</a>
+ in GHC's sources. The zonking routines for the various forms of Haskell
+ constructs are responsible for most of the code in the module <a
+ href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/typecheck/TcHsSyn.lhs"><code>TcHsSyn</code>,</a>
+ whereas the routines that actually operate on mutable types are defined
+ in <a
+ href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/typecheck/TcMType.lhs"><code>TcMType</code></a>;
+ this includes the zonking of type variables and type terms, routines to
+ create mutable structures and update them as well as routines that check
+ constraints, such as that type variables in function signatures have not
+ been instantiated during type checking. The actual type unification
+ routine is <code>uTys</code> in the module <a
+ href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/typecheck/TcUnify.lhs"><code>TcUnify</code></a>.
+ </p>
+ <p>
+ All type variables that may be instantiated (those in signatures
+ may not), but haven't been instantiated during type checking, are zonked
+ to <code>()</code>, so that after type checking all mutable variables
+ have been eliminated.
+ </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>
+
+ <h4>Type Checking Environment</h4>
+ <p>
+ During type checking, GHC maintains a <em>type environment</em> whose
+ type definitions are fixed in the module <a
+ href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/typecheck/TcRnTypes.lhs"><code>TcRnTypes</code></a> with the operations defined in
+<a
+ href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/typecheck/TcEnv.lhs"><code>TcEnv</code></a>.
+ Among other things, the environment contains all imported and local
+ instances as well as a list of <em>global</em> entities (imported and
+ local types and classes together with imported identifiers) and
+ <em>local</em> entities (locally defined identifiers). This environment
+ is threaded through the type checking monad, whose support functions
+ including initialisation can be found in the module <a
+ href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/typecheck/TcRnMonad.lhs"><code>TcRnMonad</code>.</a>
+
+ <h4>Expressions</h4>
+ <p>
+ Expressions are type checked by <a
+ href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/typecheck/TcExpr.lhs"><code>TcExpr</code>.</a>
+ <p>
+ Usage occurences of identifiers are processed by the function
+ <code>tcId</code> whose main purpose is to <a href="#inst">instantiate
+ overloaded identifiers.</a> It essentially calls
+ <code>TcInst.instOverloadedFun</code> once for each universally
+ quantified set of type constraints. It should be noted that overloaded
+ identifiers are replaced by new names that are first defined in the LIE
+ (Local Instance Environment?) and later promoted into top-level
+ bindings.
+
+ <h4><a name="inst">Handling of Dictionaries and Method Instances</a></h4>
+ <p>
+ GHC implements overloading using so-called <em>dictionaries.</em> A
+ dictionary is a tuple of functions -- one function for each method in
+ the class of which the dictionary implements an instance. During type
+ checking, GHC replaces each type constraint of a function with one
+ additional argument. At runtime, the extended function gets passed a
+ matching class dictionary by way of these additional arguments.
+ Whenever the function needs to call a method of such a class, it simply
+ extracts it from the dictionary.
+ <p>
+ This sounds simple enough; however, the actual implementation is a bit
+ more tricky as it wants to keep track of all the instances at which
+ overloaded functions are used in a module. This information is useful
+ to optimise the code. The implementation is the module <a
+ href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/typecheck/Inst.lhs"><code>Inst.lhs</code>.</a>
+ <p>
+ The function <code>instOverloadedFun</code> is invoked for each
+ overloaded usage occurence of an identifier, where overloaded means that
+ the type of the idendifier contains a non-trivial type constraint. It
+ proceeds in two steps: (1) Allocation of a method instance
+ (<code>newMethodWithGivenTy</code>) and (2) instantiation of functional
+ dependencies. The former implies allocating a new unique identifier,
+ which replaces the original (overloaded) identifier at the currently
+ type-checked usage occurrence.
+ <p>
+ The new identifier (after being threaded through the LIE) eventually
+ will be bound by a top-level binding whose rhs contains a partial
+ application of the original overloaded identifier. This papp applies
+ the overloaded function to the dictionaries needed for the current
+ instance. In GHC lingo, this is called a <em>method.</em> Before
+ becoming a top-level binding, the method is first represented as a value
+ of type <code>Inst.Inst</code>, which makes it easy to fold multiple
+ instances of the same identifier at the same types into one global
+ definition. (And probably other things, too, which I haven't
+ investigated yet.)
+
+ <p>
+ <strong>Note:</strong> As of 13 January 2001 (wrt. to the code in the
+ CVS HEAD), the above mechanism interferes badly with RULES pragmas
+ defined over overloaded functions. During instantiation, a new name is
+ created for an overloaded function partially applied to the dictionaries
+ needed in a usage position of that function. As the rewrite rule,
+ however, mentions the original overloaded name, it won't fire anymore
+ -- unless later phases remove the intermediate definition again. The
+ latest CVS version of GHC has an option
+ <code>-fno-method-sharing</code>, which avoids sharing instantiation
+ stubs. This is usually/often/sometimes sufficient to make the rules
+ fire again.
+
+ <p><small>
+<!-- hhmts start -->
+Last modified: Thu May 12 22:52:46 EST 2005
+<!-- hhmts end -->
+ </small>
+ </body>
+</html>
projects / ghc-hetmet.git / blobdiff