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

[David Menendez]

Ben Rudiak-Gould writes:

| Also, the rule would not be quite as simple as you make it out to be,
| since
| 
|      forall a. (forall b. Foo a b => a -> b) -> Int
| 
| is a legal type, for example.

Is it? GHCi gives me an error if I try typing a function like that.

> {-# OPTIONS -fglasgow-exts #-}
> class Foo a b
> 
> f :: forall a. (forall b. Foo a b => a -> b) -> Int
> f = undefined

    No instance for (Foo a b)
      arising from instantiating a type signature at x.hs:5:4-12
    Probable fix: add (Foo a b) to the type signature(s) for `f'
      Expected type: (forall b1. (Foo a b1) => a -> b1) -> Int
      Inferred type: (a -> b) -> Int
    In the definition of `f': f = undefined

I think there would need to be a top-level constraint on |a| to
guarantee that an instance of |Foo a b| exists, like

    forall a. (exists c. Foo a c) =>
        (forall b. Foo a b => a -> b) -> Int
-- 
David Menendez <zednenem at psualum.com> | "In this house, we obey the laws
<http://www.eyrie.org/~zednenem>      |        of thermodynamics!"