docs/comm/the-beast/typecheck.html

   1 <!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
   2 <html>
   3   <head>
   4     <META HTTP-EQUIV="Content-Type" CONTENT="text/html; charset=ISO-8859-1">
   5     <title>The GHC Commentary - Checking Types</title>
   6   </head>
   7
   8   <body BGCOLOR="FFFFFF">
   9     <h1>The GHC Commentary - Checking Types</h1>
  10     <p>
  11       Probably the most important phase in the frontend is the type checker,
  12       which is located at <a
  13         href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/typecheck/"><code>fptools/ghc/compiler/typecheck/</code>.</a>
  14       GHC type checks programs in their original Haskell form before the
  15       desugarer converts them into Core code.  This complicates the type
  16       checker as it has to handle the much more verbose Haskell AST, but it
  17       improves error messages, as those message are based on the same
  18       structure that the user sees.
  19     </p>
  20     <p>
  21       GHC defines the abstract syntax of Haskell programs in <a
  22       href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/hsSyn/HsSyn.lhs"><code>HsSyn</code></a>
  23       using a structure that abstracts over the concrete representation of
  24       bound occurences of identifiers and patterns.  The module <a
  25       href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/typecheck/TcHsSyn.lhs"><code>TcHsSyn</code></a>
  26       defines a number of helper function required by the type checker.  Note
  27       that the type <a
  28       href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/typecheck/TcRnTypes.lhs"><code>TcRnTypes</code></a>.<code>TcId</code>
  29       used to represent identifiers in some signatures during type checking
  30       is, in fact, nothing but a synonym for a <a href="vars.html">plain
  31       <code>Id</code>.</a>
  32     </p>
  33     <p>
  34       It is also noteworthy, that the representations of types changes during
  35       type checking from <code>HsType</code> to <code>TypeRep.Type</code>.
  36       The latter is a <a href="types.html">hybrid type representation</a> that
  37       is used to type Core, but still contains sufficient information to
  38       recover source types.  In particular, the type checker maintains and
  39       compares types in their <code>Type</code> form.
  40     </p>
  41
  42     <h2>The Overall Flow of Things</h2>
  43
  44     <h4>Entry Points Into the Type Checker</h4>
  45     <p>
  46       The interface of the type checker (and <a
  47       href="renamer.html">renamer</a>) to the rest of the compiler is provided
  48       by <a
  49       href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/typecheck/TcRnDriver.lhs"><code>TcRnDriver</code></a>.
  50       Entire modules are processed by calling <code>tcRnModule</code> and GHCi
  51       uses <code>tcRnStmt</code>, <code>tcRnExpr</code>, and
  52       <code>tcRnType</code> to typecheck statements and expressions, and to
  53       kind check types, respectively.  Moreover, <code>tcRnExtCore</code> is
  54       provided to typecheck external Core code.  Moreover,
  55       <code>tcTopSrcDecls</code> is used by Template Haskell - more
  56       specifically by <code>TcSplice.tc_bracket</code>
  57       - to type check the contents of declaration brackets.
  58     </p>
  59
  60     <h4>Renaming and Type Checking a Module</h4>
  61     <p>
  62       The function <code>tcRnModule</code> controls the complete static
  63       analysis of a Haskell module.  It sets up the combined renamer and type
  64       checker monad, resolves all import statements, initiates the actual
  65       renaming and type checking process, and finally, wraps off by processing
  66       the export list.
  67     </p>
  68     <p>
  69       The actual type checking and renaming process is initiated via
  70       <code>TcRnDriver.tcRnSrcDecls</code>, which uses a helper called
  71       <code>tc_rn_src_decls</code> to implement the iterative renaming and
  72       type checking process required by <a href="../exts/th.html">Template
  73       Haskell</a>.  However, before it invokes <code>tc_rn_src_decls</code>,
  74       it takes care of hi-boot files; afterwards, it simplifies type
  75       constraints and zonking (see below regarding the later).
  76     </p>
  77     <p>
  78       The function <code>tc_rn_src_decls</code> partitions static analysis of
  79       a whole module into multiple rounds, where the initial round is followed
  80       by an additional one for each toplevel splice.  It collects all
  81       declarations up to the next splice into an <code>HsDecl.HsGroup</code>
  82       to rename and type check that <em>declaration group</em> by calling
  83       <code>TcRnDriver.tcRnGroup</code>.  Afterwards, it executes the
  84       splice (if there are any left) and proceeds to the next group, which
  85       includes the declarations produced by the splice.
  86     </p>
  87     <p>
  88       The function <code>tcRnGroup</code>, finally, gets down to invoke the
  89       actual renaming and type checking via
  90       <code>TcRnDriver.rnTopSrcDecls</code> and
  91       <code>TcRnDriver.tcTopSrcDecls</code>, respectively.  The renamer, apart
  92       from renaming, computes the global type checking environment, of type
  93       <code>TcRnTypes.TcGblEnv</code>, which is stored in the type checking
  94       monad before type checking commences.
  95     </p>
  96
  97     <h2>Type Checking a Declaration Group</h2>
  98     <p>
  99       The type checking of a declaration group, performed by
 100       <code>tcTopSrcDecls</code> starts by processing of the type and class
 101       declarations of the current module, using the function
 102       <code>TcTyClsDecls.tcTyAndClassDecls</code>.  This is followed by a
 103       first round over instance declarations using
 104       <code>TcInstDcls.tcInstDecls1</code>, which in particular generates all
 105       additional bindings due to the deriving process.  Then come foreign
 106       import declarations (<code>TcForeign.tcForeignImports</code>) and
 107       default declarations (<code>TcDefaults.tcDefaults</code>).
 108     </p>
 109     <p>
 110       Now, finally, toplevel value declarations (including derived ones) are
 111       type checked using <code>TcBinds.tcTopBinds</code>.  Afterwards,
 112       <code>TcInstDcls.tcInstDecls2</code> traverses instances for the second
 113       time.  Type checking concludes with processing foreign exports
 114       (<code>TcForeign.tcForeignExports</code>) and rewrite rules
 115       (<code>TcRules.tcRules</code>).  Finally, the global environment is
 116       extended with the new bindings.
 117     </p>
 118
 119     <h2>Type checking Type and Class Declarations</h2>
 120     <p>
 121       Type and class declarations are type checked in a couple of phases that
 122       contain recursive dependencies - aka <em>knots.</em> The first knot
 123       encompasses almost the whole type checking of these declarations and
 124       forms the main piece of <code>TcTyClsDecls.tcTyAndClassDecls</code>.
 125     </p>
 126     <p>
 127       Inside this big knot, the first main operation is kind checking, which
 128       again involves a knot.  It is implemented by <code>kcTyClDecls</code>,
 129       which performs kind checking of potentially recursively-dependent type
 130       and class declarations using kind variables for initially unknown kinds.
 131       During processing the individual declarations some of these variables
 132       will be instantiated depending on the context; the rest gets by default
 133       kind <code>*</code> (during <em>zonking</em> of the kind signatures).
 134       Type synonyms are treated specially in this process, because they can
 135       have an unboxed type, but they cannot be recursive.  Hence, their kinds
 136       are inferred in dependency order.  Moreover, in contrast to class
 137       declarations and other type declarations, synonyms are not entered into
 138       the global environment as a global <code>TyThing</code>.
 139       (<code>TypeRep.TyThing</code> is a sum type that combines the various
 140       flavours of typish entities, such that they can be stuck into type
 141       environments and similar.)
 142     </p>
 143
 144     <h2>More Details</h2>
 145
 146     <h4>Types Variables and Zonking</h4>
 147     <p>
 148       During type checking type variables are represented by mutable variables
 149       - cf. the <a href="vars.html#TyVar">variable story.</a>  Consequently,
 150       unification can instantiate type variables by updating those mutable
 151       variables.  This process of instantiation is (for reasons that elude me)
 152       called <a
 153       href="http://www.dictionary.com/cgi-bin/dict.pl?term=zonk&db=*">zonking</a>
 154       in GHC's sources.  The zonking routines for the various forms of Haskell
 155       constructs are responsible for most of the code in the module <a
 156       href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/typecheck/TcHsSyn.lhs"><code>TcHsSyn</code>,</a>
 157       whereas the routines that actually operate on mutable types are defined
 158       in <a
 159       href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/typecheck/TcMType.lhs"><code>TcMType</code></a>;
 160       this includes the zonking of type variables and type terms, routines to
 161       create mutable structures and update them as well as routines that check
 162       constraints, such as that type variables in function signatures have not
 163       been instantiated during type checking.  The actual type unification
 164       routine is <code>uTys</code> in the module <a
 165       href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/typecheck/TcUnify.lhs"><code>TcUnify</code></a>.
 166     </p>
 167     <p>
 168       All type variables that may be instantiated (those in signatures
 169       may not), but haven't been instantiated during type checking, are zonked
 170       to <code>()</code>, so that after type checking all mutable variables
 171       have been eliminated.
 172     </p>
 173
 174     <h4>Type Representation</h4>
 175     <p>
 176       The representation of types is fixed in the module <a
 177       href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/typecheck/TcRep.lhs"><code>TcRep</code></a>
 178       and exported as the data type <code>Type</code>.  As explained in <a
 179       href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/typecheck/TcType.lhs"><code>TcType</code></a>,
 180       GHC supports rank-N types, but, in the type checker, maintains the
 181       restriction that type variables cannot be instantiated to quantified
 182       types (i.e., the type system is predicative).  The type checker floats
 183       universal quantifiers outside and maintains types in prenex form.
 184       (However, quantifiers can, of course, not float out of negative
 185       positions.)  Overall, we have
 186     </p>
 187     <blockquote>
 188       <pre>
 189 sigma -> forall tyvars. phi
 190 phi   -> theta => rho
 191 rho   -> sigma -> rho
 192        | tau
 193 tau   -> tyvar
 194        | tycon tau_1 .. tau_n
 195        | tau_1 tau_2
 196        | tau_1 -> tau_2</pre>
 197     </blockquote>
 198     <p>
 199       where <code>sigma</code> is in prenex form; i.e., there is never a
 200       forall to the right of an arrow in a <code>phi</code> type.  Moreover, a
 201       type of the form <code>tau</code> never contains a quantifier (which
 202       includes arguments to type constructors).
 203     </p>
 204     <p>
 205       Of particular interest are the variants <code>SourceTy</code> and
 206       <code>NoteTy</code> of <a
 207       href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/typecheck/TypeRep.lhs"><code>TypeRep</code></a>.<code>Type</code>.
 208       The constructor <code>SourceTy :: SourceType -> Type</code> represents a
 209       type constraint; that is, a predicate over types represented by a
 210       dictionary.  The type checker treats a <code>SourceTy</code> as opaque,
 211       but during the translation to core it will be expanded into its concrete
 212       representation (i.e., a dictionary type) by the function <a
 213       href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/types/Type.lhs"><code>Type</code></a>.<code>sourceTypeRep</code>.
 214       Note that newtypes are not covered by <code>SourceType</code>s anymore,
 215       even if some comments in GHC still suggest this.  Instead, all newtype
 216       applications are initially represented as a <code>NewTcApp</code>, until
 217       they are eliminated by calls to <a
 218       href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/types/Type.lhs"><code>Type</code></a>.<code>newTypeRep</code>.
 219     </p>
 220     <p>
 221       The <code>NoteTy</code> constructor is used to add non-essential
 222       information to a type term.  Such information has the type
 223       <code>TypeRep.TyNote</code> and is either the set of free type variables
 224       of the annotated expression or the unexpanded version of a type synonym.
 225       Free variables sets are cached as notes to save the overhead of
 226       repeatedly computing the same set for a given term.  Unexpanded type
 227       synonyms are useful for generating comprehensible error messages, but
 228       have no influence on the process of type checking.
 229     </p>
 230
 231     <h4>Type Checking Environment</h4>
 232     <p>
 233       During type checking, GHC maintains a <em>type environment</em> whose
 234       type definitions are fixed in the module <a
 235       href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/typecheck/TcRnTypes.lhs"><code>TcRnTypes</code></a> with the operations defined in
 236 <a
 237       href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/typecheck/TcEnv.lhs"><code>TcEnv</code></a>.
 238       Among other things, the environment contains all imported and local
 239       instances as well as a list of <em>global</em> entities (imported and
 240       local types and classes together with imported identifiers) and
 241       <em>local</em> entities (locally defined identifiers).  This environment
 242       is threaded through the type checking monad, whose support functions
 243       including initialisation can be found in the module <a
 244       href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/typecheck/TcRnMonad.lhs"><code>TcRnMonad</code>.</a>
 245
 246     <h4>Expressions</h4>
 247     <p>
 248       Expressions are type checked by <a
 249       href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/typecheck/TcExpr.lhs"><code>TcExpr</code>.</a>
 250     <p>
 251       Usage occurences of identifiers are processed by the function
 252       <code>tcId</code> whose main purpose is to <a href="#inst">instantiate
 253       overloaded identifiers.</a> It essentially calls
 254       <code>TcInst.instOverloadedFun</code> once for each universally
 255       quantified set of type constraints.  It should be noted that overloaded
 256       identifiers are replaced by new names that are first defined in the LIE
 257       (Local Instance Environment?) and later promoted into top-level
 258       bindings.
 259
 260     <h4><a name="inst">Handling of Dictionaries and Method Instances</a></h4>
 261     <p>
 262       GHC implements overloading using so-called <em>dictionaries.</em> A
 263       dictionary is a tuple of functions -- one function for each method in
 264       the class of which the dictionary implements an instance.  During type
 265       checking, GHC replaces each type constraint of a function with one
 266       additional argument.  At runtime, the extended function gets passed a
 267       matching class dictionary by way of these additional arguments.
 268       Whenever the function needs to call a method of such a class, it simply
 269       extracts it from the dictionary.
 270     <p>
 271       This sounds simple enough; however, the actual implementation is a bit
 272       more tricky as it wants to keep track of all the instances at which
 273       overloaded functions are used in a module.  This information is useful
 274       to optimise the code.  The implementation is the module <a
 275       href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/typecheck/Inst.lhs"><code>Inst.lhs</code>.</a>
 276     <p>
 277       The function <code>instOverloadedFun</code> is invoked for each
 278       overloaded usage occurence of an identifier, where overloaded means that
 279       the type of the idendifier contains a non-trivial type constraint.  It
 280       proceeds in two steps: (1) Allocation of a method instance
 281       (<code>newMethodWithGivenTy</code>) and (2) instantiation of functional
 282       dependencies.  The former implies allocating a new unique identifier,
 283       which replaces the original (overloaded) identifier at the currently
 284       type-checked usage occurrence.
 285     <p>
 286       The new identifier (after being threaded through the LIE) eventually
 287       will be bound by a top-level binding whose rhs contains a partial
 288       application of the original overloaded identifier.  This papp applies
 289       the overloaded function to the dictionaries needed for the current
 290       instance.  In GHC lingo, this is called a <em>method.</em>  Before
 291       becoming a top-level binding, the method is first represented as a value
 292       of type <code>Inst.Inst</code>, which makes it easy to fold multiple
 293       instances of the same identifier at the same types into one global
 294       definition.  (And probably other things, too, which I haven't
 295       investigated yet.)
 296
 297     <p>
 298       <strong>Note:</strong> As of 13 January 2001 (wrt. to the code in the
 299       CVS HEAD), the above mechanism interferes badly with RULES pragmas
 300       defined over overloaded functions.  During instantiation, a new name is
 301       created for an overloaded function partially applied to the dictionaries
 302       needed in a usage position of that function.  As the rewrite rule,
 303       however, mentions the original overloaded name, it won't fire anymore
 304       -- unless later phases remove the intermediate definition again.  The
 305       latest CVS version of GHC has an option
 306       <code>-fno-method-sharing</code>, which avoids sharing instantiation
 307       stubs.  This is usually/often/sometimes sufficient to make the rules
 308       fire again.
 309
 310     <p><small>
 311 <!-- hhmts start -->
 312 Last modified: Thu May 12 22:52:46 EST 2005
 313 <!-- hhmts end -->
 314     </small>
 315   </body>
 316 </html>