• simonpj's avatar
    [project @ 2001-11-26 09:20:25 by simonpj] · 5e3f005d
    simonpj 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
TcSimplify.lhs 61.4 KB