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

[Brian Hulley]

Brian Hulley wrote:
> Thanks (also to Stefan) for clarifying that f's type is indeed legal.
> However I still think that there is a bit of confusion about what the
> syntax is supposed to mean, because:
>
>           f :: forall a. (forall b. Foo a b => a -> b) -> Int
>
> is effectively being used as a shorthand for (the illegal syntax):
>
>           f :: forall a. (forall c. Foo a c) => (forall b. Foo a b =>
> a->b)->Int
>
> whereas
>
>           g :: forall a. (Ord a => a->a)->Int
>
> is *not* being seen as a quick way of writing:
>
>          g :: forall a. Ord a => (Ord a => a->a)->Int
>
> (which would further reduce to g:: forall a. Ord a=> (a->a)->Int
> because there's no need for the constraint on 'a' to be written twice)
>
> In both cases, for the argument to be useable, 'a' needs to be
> constrained in the general case. The fact that all instances of Foo
> may happen to be polymorphic in the 'a' argument is surely just a
> special case, which would still be covered by the (forall c. Foo a c)
> constraint.
> I think a question for the syntax is: are we to understand
> quantifiers and class constraints in terms of logic, or are they
> supposed to only be understood in terms of some specific
> implementation eg passing a dictionary?
> If we are to understand them in terms of logic alone, I would suggest
> a general rule that all types could be (internally) converted into a
> normal form by propagating all constraints back to the relevant
> quantifier and eliminating any redundant constraints that are left,
> so that we would get the advantage of the existing "shorthand" while
> still allowing a simple way of understanding what's going on even in
> the presence of multi-param type classes.
>

Actually please ignore the above! :-)
I see now that all these things have useful meanings as they stand at the 
moment, and that there would never be any need for a constraint such as 
(forall c. Foo a c), because that actual 'c's used in the function body 
could all be explicitly enumerated by a series of constraints in the case 
where the relevant instances were not polymorphic in 'a' eg

         f :: forall a. (Foo a Char, Foo a Int) => (forall b. Foo a b => 
a->b) -> Int
         h :: forall a b c. (Foo a b, Foo a c) =>(forall d. Foo a d => 
a->d) -> a -> (b,c)
         h g x = (g x, g x)

Thanks to all who helped further my understanding of the interaction between 
constraints and arbitrary rank polymorphism! :-)

Brian.