1 <!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
4 <META HTTP-EQUIV="Content-Type" CONTENT="text/html; charset=ISO-8859-1">
5 <title>The GHC Commentary - Checking Types</title>
8 <body BGCOLOR="FFFFFF">
9 <h1>The GHC Commentary - Checking Types</h1>
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.
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
33 <h4>Entry Points Into the Type Checker</h4>
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.
45 <h4>Types Variables and Zonking</h4>
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)
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
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>.
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
73 <h4>Type Representation</h4>
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
88 sigma -> forall tyvars. phi
93 | tycon tau_1 .. tau_n
95 | tau_1 -> tau_2</pre>
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).
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>.
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.
130 <h4>Type Checking Environment</h4>
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
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>
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>
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
159 <h4><a name="inst">Handling of Dictionaries and Method Instances</a></h4>
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.
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>
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.
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
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
211 Last modified: Sat Sep 13 23:35:24 BST 2003