+++ /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