10 Jun
2008
10 Jun
'08
2:28 p.m.
On 6/10/08, Derek Elkins
This is the lack of impredicativity.
W :: a -> W a To get the result type W (forall a. t a), W must instantiate the a in W's type to (forall a. t a). Further we then pass it to (.) which has type (b -> c) -> (a -> b) -> a -> c and thus require instantiating both a and b to higher-rank types. A predicative type system does not allow instantiating type variables to quantified types.
Although if I am reading the literature correctly, that definition will likely typecheck in the next GHC... http://research.microsoft.com/~simonpj/papers/boxy/ -- ryan