Squash some spelling issues
[ghc.git] / 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 occurrences 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 occurrences 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 occurrence 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>