ghc/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 the 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       instantiates this structure for the type checker using <a
  27       href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/typecheck/TcRnTypes.lhs"><code>TcRnTypes</code></a>.<code>TcId</code>
  28       to represent identifiers - in fact, a <code>TcId</code> is currently
  29       nothing but just a synonym for a <a href="vars.html">plain
  30       <code>Id</code>.</a>
  31     </p>
  32
  33     <h4>Entry Points Into the Type Checker</h4>
  34     <p>
  35       The interface of the type checker (and renamer) to the rest of the
  36       compiler is provided by <a
  37       href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/typecheck/TcRnDriver.lhs"><code>TcRnDriver</code></a>.
  38       Entire modules are processed by calling <code>tcRnModule</code> and GHCi
  39       uses <code>tcRnStmt</code> and <code>tcRnExpr</code> to typecheck
  40       statements and expressions, respectively.  Moreover,
  41       <code>tcRnIface</code> and <code>tcRnExtCore</code> are provided to
  42       typecheck interface files and external Core code.
  43     </p>
  44
  45     <h4>Types Variables and Zonking</h4>
  46     <p>
  47       During type checking type variables are represented by mutable variables
  48       - cf. the <a href="vars.html#TyVar">variable story.</a>  Consequently,
  49       unification can instantiate type variables by updating those mutable
  50       variables.  This process of instantiation is (for reasons that elude me)
  51       called <a
  52       href="http://www.dictionary.com/cgi-bin/dict.pl?term=zonk&db=*">zonking</a>
  53       in GHC's sources.  The zonking routines for the various forms of Haskell
  54       constructs are responsible for most of the code in the module <a
  55       href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/typecheck/TcHsSyn.lhs"><code>TcHsSyn</code>,</a>
  56       whereas the routines that actually operate on mutable types are defined
  57       in <a
  58       href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/typecheck/TcMType.lhs"><code>TcMType</code></a>;
  59       this includes the zonking of type variables and type terms, routines to
  60       create mutable structures and update them as well as routines that check
  61       constraints, such as that type variables in function signatures have not
  62       been instantiated during type checking.  The actual type unification
  63       routine is <code>uTys</code> in the module <a
  64       href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/typecheck/TcUnify.lhs"><code>TcUnify</code></a>.
  65     </p>
  66     <p>
  67       All type variables that may be instantiated (those in signatures
  68       may not), but haven't been instantiated during type checking, are zonked
  69       to <code>()</code>, so that after type checking all mutable variables
  70       have been eliminated.
  71     </p>
  72
  73     <h4>Type Representation</h4>
  74     <p>
  75       The representation of types is fixed in the module <a
  76       href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/typecheck/TcRep.lhs"><code>TcRep</code></a>
  77       and exported as the data type <code>Type</code>.  As explained in <a
  78       href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/typecheck/TcType.lhs"><code>TcType</code></a>,
  79       GHC supports rank-N types, but, in the type checker, maintains the
  80       restriction that type variables cannot be instantiated to quantified
  81       types (i.e., the type system is predicative).  The type checker floats
  82       universal quantifiers outside and maintains types in prenex form.
  83       (However, quantifiers can, of course, not float out of negative
  84       positions.)  Overall, we have
  85     </p>
  86     <blockquote>
  87       <pre>
  88 sigma -> forall tyvars. phi
  89 phi   -> theta => rho
  90 rho   -> sigma -> rho
  91        | tau
  92 tau   -> tyvar
  93        | tycon tau_1 .. tau_n
  94        | tau_1 tau_2
  95        | tau_1 -> tau_2</pre>
  96     </blockquote>
  97     <p>
  98       where <code>sigma</code> is in prenex form; i.e., there is never a
  99       forall to the right of an arrow in a <code>phi</code> type.  Moreover, a
 100       type of the form <code>tau</code> never contains a quantifier (which
 101       includes arguments to type constructors).
 102     </p>
 103     <p>
 104       Of particular interest are the variants <code>SourceTy</code> and
 105       <code>NoteTy</code> of <a
 106       href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/typecheck/TypeRep.lhs"><code>TypeRep</code></a>.<code>Type</code>.
 107       The constructor <code>SourceTy :: SourceType -> Type</code> represents a
 108       type constraint; that is, a predicate over types represented by a
 109       dictionary.  The type checker treats a <code>SourceTy</code> as opaque,
 110       but during the translation to core it will be expanded into its concrete
 111       representation (i.e., a dictionary type) by the function <a
 112       href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/types/Type.lhs"><code>Type</code></a>.<code>sourceTypeRep</code>.
 113       Note that newtypes are not covered by <code>SourceType</code>s anymore,
 114       even if some comments in GHC still suggest this.  Instead, all newtype
 115       applications are initially represented as a <code>NewTcApp</code>, until
 116       they are eliminated by calls to <a
 117       href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/types/Type.lhs"><code>Type</code></a>.<code>newTypeRep</code>.
 118     </p>
 119     <p>
 120       The <code>NoteTy</code> constructor is used to add non-essential
 121       information to a type term.  Such information has the type
 122       <code>TypeRep.TyNote</code> and is either the set of free type variables
 123       of the annotated expression or the unexpanded version of a type synonym.
 124       Free variables sets are cached as notes to save the overhead of
 125       repeatedly computing the same set for a given term.  Unexpanded type
 126       synonyms are useful for generating comprehensible error messages, but
 127       have no influence on the process of type checking.
 128     </p>
 129
 130     <h4>Type Checking Environment</h4>
 131     <p>
 132       During type checking, GHC maintains a <em>type environment</em> whose
 133       type definitions are fixed in the module <a
 134       href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/typecheck/TcRnTypes.lhs"><code>TcRnTypes</code></a> with the operations defined in
 135 <a
 136       href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/typecheck/TcEnv.lhs"><code>TcEnv</code></a>.
 137       Among other things, the environment contains all imported and local
 138       instances as well as a list of <em>global</em> entities (imported and
 139       local types and classes together with imported identifiers) and
 140       <em>local</em> entities (locally defined identifiers).  This environment
 141       is threaded through the type checking monad, whose support functions
 142       including initialisation can be found in the module <a
 143       href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/typecheck/TcRnMonad.lhs"><code>TcRnMonad</code>.</a>
 144
 145     <h4>Expressions</h4>
 146     <p>
 147       Expressions are type checked by <a
 148       href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/typecheck/TcExpr.lhs"><code>TcExpr</code>.</a>
 149     <p>
 150       Usage occurences of identifiers are processed by the function
 151       <code>tcId</code> whose main purpose is to <a href="#inst">instantiate
 152       overloaded identifiers.</a> It essentially calls
 153       <code>TcInst.instOverloadedFun</code> once for each universally
 154       quantified set of type constraints.  It should be noted that overloaded
 155       identifiers are replaced by new names that are first defined in the LIE
 156       (Local Instance Environment?) and later promoted into top-level
 157       bindings.
 158
 159     <h4><a name="inst">Handling of Dictionaries and Method Instances</a></h4>
 160     <p>
 161       GHC implements overloading using so-called <em>dictionaries.</em> A
 162       dictionary is a tuple of functions -- one function for each method in
 163       the class of which the dictionary implements an instance.  During type
 164       checking, GHC replaces each type constraint of a function with one
 165       additional argument.  At runtime, the extended function gets passed a
 166       matching class dictionary by way of these additional arguments.
 167       Whenever the function needs to call a method of such a class, it simply
 168       extracts it from the dictionary.
 169     <p>
 170       This sounds simple enough; however, the actual implementation is a bit
 171       more tricky as it wants to keep track of all the instances at which
 172       overloaded functions are used in a module.  This information is useful
 173       to optimise the code.  The implementation is the module <a
 174       href="http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/ghc/compiler/typecheck/Inst.lhs"><code>Inst.lhs</code>.</a>
 175     <p>
 176       The function <code>instOverloadedFun</code> is invoked for each
 177       overloaded usage occurence of an identifier, where overloaded means that
 178       the type of the idendifier contains a non-trivial type constraint.  It
 179       proceeds in two steps: (1) Allocation of a method instance
 180       (<code>newMethodWithGivenTy</code>) and (2) instantiation of functional
 181       dependencies.  The former implies allocating a new unique identifier,
 182       which replaces the original (overloaded) identifier at the currently
 183       type-checked usage occurrence.
 184     <p>
 185       The new identifier (after being threaded through the LIE) eventually
 186       will be bound by a top-level binding whose rhs contains a partial
 187       application of the original overloaded identifier.  This papp applies
 188       the overloaded function to the dictionaries needed for the current
 189       instance.  In GHC lingo, this is called a <em>method.</em>  Before
 190       becoming a top-level binding, the method is first represented as a value
 191       of type <code>Inst.Inst</code>, which makes it easy to fold multiple
 192       instances of the same identifier at the same types into one global
 193       definition.  (And probably other things, too, which I haven't
 194       investigated yet.)
 195
 196     <p>
 197       <strong>Note:</strong> As of 13 January 2001 (wrt. to the code in the
 198       CVS HEAD), the above mechanism interferes badly with RULES pragmas
 199       defined over overloaded functions.  During instantiation, a new name is
 200       created for an overloaded function partially applied to the dictionaries
 201       needed in a usage position of that function.  As the rewrite rule,
 202       however, mentions the original overloaded name, it won't fire anymore
 203       -- unless later phases remove the intermediate definition again.  The
 204       latest CVS version of GHC has an option
 205       <code>-fno-method-sharing</code>, which avoids sharing instantiation
 206       stubs.  This is usually/often/sometimes sufficient to make the rules
 207       fire again.
 208
 209     <p><small>
 210 <!-- hhmts start -->
 211 Last modified: Sat Sep 13 23:35:24 BST 2003
 212 <!-- hhmts end -->
 213     </small>
 214   </body>
 215 </html>