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