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

[Ben Rudiak-Gould]

David Menendez wrote:
> Ben Rudiak-Gould writes:
> |      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.

This works:

     f :: forall a. (forall b. Foo a b => a -> b) -> Int
     f _ = 3

I interpret this type as meaning that you can call the argument provided you 
can come up with an appropriate b. If you can't come up with one then you 
can't call the argument, but you can still ignore it and type check.

If you had, for example,

     instance Foo a Char
     instance Foo a Int

then you would be able to use the argument polymorphically at b=Char and b=Int.

f = undefined also works if you have "instance Foo a b" (which is only 
allowed with -fallow-undecidable-instances). I think it's because of 
predicativity that it fails without it.

Presumably forall a. (Ord a => a-> a) -> Int could be allowed as well, but 
if you're called with a = IO () then you can't call your argument, therefore 
you can never call your argument, therefore it's not a useful type in practice.

-- Ben