Here's the story * GHC understands only rank-2 types; your type is rank 3 * The reason for this is that type inference for higher-rank types is tricky. GHC just squeezes through the door with rank-2 types by using a neat hack, but the hack just doesn't cope with higher ranks at all. * GHC 4.08 didn't *check* that the type is rank-2, whereas ghc 5.02 does. So all versions of your program will be rejected by GHC now, before it ever gets to type checking. * It's true that your test' *does* typecheck in GHC 4.08, but it's a coincidence! Certain very special programs will work even with higher rank types, but its jolly hard to explain which, so GHC 5 chucks them all out. * Nevertheless your program makes perfect sense. I believe that the Right Thing to do is to adopt Odersky/Laufer's idea of "Putting Type Annotations To Work" (POPL 96). They show how to typecheck arbitrarily high rank type provided there are enough type annotations, and Mark Shields has recently explained it all to me. But implementing this would be real work. So I'm interested to know: if GHC allowed arbitrarily-ranked types, who would use them? Simon | -----Original Message----- | From: Janis Voigtlaender [mailto:voigt@orchid.inf.tu-dresden.de] | Sent: 24 October 2001 08:00 | To: haskell@haskell.org | Subject: Re: rank 2-polymorphism and type checking | | | Iavor S. Diatchki writes: | | > > > test :: (forall t . (forall a . t a) -> t b) -> b -> b | > i am not an expert on this, but isnt this rank 3? | | Might be. Does this mean I cannot write it in Haskell? But, with | | data T a = C | | I can write: | | test' :: (forall t . (forall a . t a) -> t b) -> b -> b | test' g x = case g C of C -> x | | Here, the type checker finds out on its own that t is | instantiated to T. Still, | why are the annotations in the following code not enough to | let it also accept | the definition of "test" (see my earlier message), | respectively how can I tell | it that t should be instantiated to t c = forall d . (c->d) | -> d -> d ? | | test :: (forall t . (forall a . t a) -> t b) -> b -> b | test g x = (g :: (forall a . (forall d . (a->d) -> | d -> d)) -> | (forall e . (b->e) -> e -> e)) | ((\f y -> y) :: (forall a . (forall d . (a->d) -> | d -> d))) | (id :: (b -> b)) | (x :: b) | | | -- | Janis Voigtlaender | http://wwwtcs.inf.tu-dresden.de/~voigt/ | mailto:voigt@tcs.inf.tu-dresden.de | | | _______________________________________________ | Haskell mailing list | Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell |