Probably the most important phase in the frontend is the type checker,
which is located at fptools/ghc/compiler/typecheck/
.
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 the those message are based on the same
structure that the user sees.
GHC defines the abstract syntax of Haskell programs in HsSyn
using a structure that abstracts over the concrete representation of
bound occurences of identifiers and patterns. The module TcHsSyn
instantiates this structure for the type checker using TcRnTypes
.TcId
to represent identifiers - in fact, a TcId
is currently
nothing but just a synonym for a plain
Id
.
The interface of the type checker (and renamer) to the rest of the
compiler is provided by TcRnDriver
.
Entire modules are processed by calling tcRnModule
and GHCi
uses tcRnStmt
and tcRnExpr
to typecheck
statements and expressions, respectively. Moreover,
tcRnIface
and tcRnExtCore
are provided to
typecheck interface files and external Core code.
During type checking type variables are represented by mutable variables
- cf. the variable story. Consequently,
unification can instantiate type variables by updating those mutable
variables. This process of instantiation is (for reasons that elude me)
called zonking
in GHC's sources. The zonking routines for the various forms of Haskell
constructs are responsible for most of the code in the module TcHsSyn
,
whereas the routines that actually operate on mutable types are defined
in TcMType
;
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 uTys
in the module TcUnify
.
All type variables that may be instantiated (those in signatures
may not), but haven't been instantiated during type checking, are zonked
to ()
, so that after type checking all mutable variables
have been eliminated.
The representation of types is fixed in the module TcRep
and exported as the data type Type
. As explained in TcType
,
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
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
where sigma
is in prenex form; i.e., there is never a
forall to the right of an arrow in a phi
type. Moreover, a
type of the form tau
never contains a quantifier (which
includes arguments to type constructors).
Of particular interest are the variants SourceTy
and
NoteTy
of TypeRep
.Type
.
The constructor SourceTy :: SourceType -> Type
represents a
type constraint; that is, a predicate over types represented by a
dictionary. The type checker treats a SourceTy
as opaque,
but during the translation to core it will be expanded into its concrete
representation (i.e., a dictionary type) by the function Type
.sourceTypeRep
.
Note that newtypes are not covered by SourceType
s anymore,
even if some comments in GHC still suggest this. Instead, all newtype
applications are initially represented as a NewTcApp
, until
they are eliminated by calls to Type
.newTypeRep
.
The NoteTy
constructor is used to add non-essential
information to a type term. Such information has the type
TypeRep.TyNote
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.
During type checking, GHC maintains a type environment whose
type definitions are fixed in the module TcRnTypes
with the operations defined in
TcEnv
.
Among other things, the environment contains all imported and local
instances as well as a list of global entities (imported and
local types and classes together with imported identifiers) and
local entities (locally defined identifiers). This environment
is threaded through the type checking monad, whose support functions
including initialisation can be found in the module TcRnMonad
.
Expressions are type checked by TcExpr
.
Usage occurences of identifiers are processed by the function
tcId
whose main purpose is to instantiate
overloaded identifiers. It essentially calls
TcInst.instOverloadedFun
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.
GHC implements overloading using so-called dictionaries. 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.
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 Inst.lhs
.
The function instOverloadedFun
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
(newMethodWithGivenTy
) 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.
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 method. Before
becoming a top-level binding, the method is first represented as a value
of type Inst.Inst
, 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.)
Note: 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
-fno-method-sharing
, which avoids sharing instantiation
stubs. This is usually/often/sometimes sufficient to make the rules
fire again.
Last modified: Sat Sep 13 23:35:24 BST 2003