[project @ 2001-11-26 09:20:25 by simonpj]
----------------------
Implement Rank-N types
----------------------
This commit implements the full glory of Rank-N types, using
the Odersky/Laufer approach described in their paper
"Putting type annotations to work"
In fact, I've had to adapt their approach to deal with the
full glory of Haskell (including pattern matching, and the
scoped-type-variable extension). However, the result is:
* There is no restriction to rank-2 types. You can nest forall's
as deep as you like in a type. For example, you can write a type
like
p :: ((forall a. Eq a => a->a) -> Int) -> Int
This is a rank-3 type, illegal in GHC 5.02
* When matching types, GHC uses the cunning Odersky/Laufer coercion
rules. For example, suppose we have
q :: (forall c. Ord c => c->c) -> Int
Then, is this well typed?
x :: Int
x = p q
Yes, it is, but GHC has to generate the right coercion. Here's
what it looks like with all the big lambdas and dictionaries put in:
x = p (\ f :: (forall a. Eq a => a->a) ->
q (/\c \d::Ord c -> f c (eqFromOrd d)))
where eqFromOrd selects the Eq superclass dictionary from the Ord
dicationary: eqFromOrd :: Ord a -> Eq a
* You can use polymorphic types in pattern type signatures. For
example:
f (g :: forall a. a->a) = (g 'c', g True)
(Previously, pattern type signatures had to be monotypes.)
* The basic rule for using rank-N types is that you must specify
a type signature for every binder that you want to have a type
scheme (as opposed to a plain monotype) as its type.
However, you don't need to give the type signature on the
binder (as I did above in the defn for f). You can give it
in a separate type signature, thus:
f :: (forall a. a->a) -> (Char,Bool)
f g = (g 'c', g True)
GHC will push the external type signature inwards, and use
that information to decorate the binders as it comes across them.
I don't have a *precise* specification of this process, but I
think it is obvious enough in practice.
* In a type synonym you can use rank-N types too. For example,
you can write
type IdFun = forall a. a->a
f :: IdFun -> (Char,Bool)
f g = (g 'c', g True)
As always, type synonyms must always occur saturated; GHC
expands them before it does anything else. (Still, GHC goes
to some trouble to keep them unexpanded in error message.)
The main plan is as before. The main typechecker for expressions,
tcExpr, takes an "expected type" as its argument. This greatly
improves error messages. The new feature is that when this
"expected type" (going down) meets an "actual type" (coming up)
we use the new subsumption function
TcUnify.tcSub
which checks that the actual type can be coerced into the
expected type (and produces a coercion function to demonstrate).
The main new chunk of code is TcUnify.tcSub. The unifier itself
is unchanged, but it has moved from TcMType into TcUnify. Also
checkSigTyVars has moved from TcMonoType into TcUnify.
Result: the new module, TcUnify, contains all stuff relevant
to subsumption and unification.
Unfortunately, there is now an inevitable loop between TcUnify
and TcSimplify, but that's just too bad (a simple TcUnify.hi-boot
file).
All of this doesn't come entirely for free. Here's the typechecker
line count (INCLUDING comments)
Before 16,551
After 17,116
39 files changed: