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

David Menendez zednenem at
Fri Feb 10 01:41:03 EST 2006

Brian Hulley writes:

> I've been puzzling over section 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


    (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


    Pi _:(Pi a:*. Pi _:a. a). Int
David Menendez <zednenem at> | "In this house, we obey the laws
<>      |        of thermodynamics!"

More information about the Glasgow-haskell-users mailing list