Andrew Coppin wrote:
(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.
When you type some expression such as \x -> x you have to choose among an infinite number of valid types for it: Int -> Int Char -> Char forall a . a -> a forall a b . (a,b) -> (a,b) ... Yet the type inference is smart enough to choose the "best" one: forall a. a -> a because this is the "most general" type. Alas, for code like yours: foo = \f -> (f 'J', f True) there are infinite valid types too: (forall a. a -> Int) -> (Int, Int) (forall a. a -> Char)-> (Char, Char) (forall a. a -> (a,a)) -> ((Char,Char),(Bool,Bool)) ... and it is much less clear if a "best", most general type exists at all. You might have a preference to type it so that foo :: (forall a . a->a) -> (Char,Bool) foo id ==> ('J',True) :: (Char,Bool) but one could also require the following, similarly reasonable code to work: foo :: (forall a. a -> (a,a)) -> ((Char,Char),(Bool,Bool)) foo (\y -> (y,y)) ==> (('J','J'),(True,True)) :: ((Char,Char),(Bool,Bool)) And devising a type inference system allowing both seems to be quite hard. Requiring a type annotation for these not-so-common code snippets seems to be a fair compromise, at least to me. Regards, Zun.