forall a (Ord a => a-> a) -> Int is an illegal type???

[David Menendez]

Brian Hulley writes:

> I've been puzzling over section 7.4.9.3 of the ghc users manual for
> the past few months (!) and still can't understand why the following
> is an illegal type:
> 
> forall a. ((Ord a => a-> a) -> Int)
> 
> whereas
> 
> (forall a. Ord a => a->a) -> Int
> 
> is legal. I can understand why the second one *is* legal but I can't
> seem to understand why the first syntax is not just exactly the same
> thing even though the parse tree is different.

I see you already clarified this, but I'd like to point out that

    forall a. (a -> a) -> Int

and

    (forall a. a -> a) -> Int

are very different. The first essentially takes two arguments, a type
|a| and a value of type |a -> a|. The second takes a single argument of
type |forall a. a -> a|.
 
There are some type systems (like JHC core, IIRC) which treat "forall"
and "->" as special cases of the dependent product. That is, "T -> U" is
short for "Pi _:T. U" and "forall a. T" is short for "Pi a:*. T". Using
that syntax, the types above become:

    Pi a:*. Pi _:(Pi _:a. a). Int

and

    Pi _:(Pi a:*. Pi _:a. a). Int
-- 
David Menendez <zednenem at psualum.com> | "In this house, we obey the laws
<http://www.eyrie.org/~zednenem>      |        of thermodynamics!"