On Thu, Jul 16, 2009 at 2:34 PM, Andrew
Coppin
I've been working hard this week, and I'm stumbled upon something which is probably of absolutely no surprise to anybody but me.
Consider the following expression:
(foo True, foo 'x')
Is this expression well-typed?
Astonishingly, the answer depends on where "foo" is defined. If "foo" is a local variable, then the above expression is guaranteed to be ill-typed.
This isn't completely accurate: f0 _ = (foo True, foo 'x') where foo = id is well-typed. whereas f1 foo = (foo True, foo 'x') requires 'foo' to be polymorphic in its first argument. This does require a higher rank type, which can't be inferred: You could type f1 as f1 :: (forall a . a -> a) -> (Bool, Char) and apply it to 'id'. Or you could type it as something like: f1 :: (forall a . a -> ()) -> ((),()) and apply it to 'const ()'