-
Simon Peyton Jones authored
---------------------- 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
5e3f005d