Andrew Coppin
So, after an entire day of boggling my mind over this, I have brought it down to one simple example:
(id 'J', id True) -- Works perfectly.
\f -> (f 'J', f True) -- Fails miserably.
Both expressions are obviously perfectly type-safe, and yet the type checker stubbornly rejects the second example. Clearly this is a flaw in the type checker.
So what is the type of that second expression? You would think that
(x -> x) -> (Char, Bool)
A bit late in the fray, but have you considered this simpler expression: \f -> f 'J' I think you'll agree this does not have type (x->x) -> Char but rather (Char -> a) -> a right? Yet you can use 'id' as an argument (for f), since it has type forall a . a -> a where you are free to substitute Char for a and get (Char -> Char). An expression like: \f -> (f 'J', f True) requires an f that is both (Char -> a) and (Bool -> a) *at the same time*. A type like (a -> a) -> (Char,Bool) means that the expression is polymorphic in its argument, but here you need to specify that the function argument must be polymorphic itself. E.g. (forall a. a -> a) -> (Char,Bool). (Disclaimer: I hope I got it right :-) -k -- If I haven't seen further, it is by standing in the footprints of giants