This is a great example, thanks for posting it. However, I feel like the real problem in this example is the lexically-scoped type variables declared with your function f. I am always surprised by the effects that lexically-scoped type variables can have on top-level declarations. Consider another example: f :: a -> a f = \x -> x Of course, f has type (forall a. a -> a). However, if we add another declaration g with lexically-scoped type variable a: g :: a -> a = \x -> 1 Then, suddenly, f has type Integer -> Integer If g is defined as: g :: a -> a = \x -> (1::Int) Then, f has type Int -> Int. If g is defined as: g :: a -> Int = \x -> 1 Then, f has type () -> () Personally, I would not mind if lexically-scoped type variables on top-level declarations were disallowed; or at least treated as "normal" top-level type annotations. --Paul On Nov 24, Lennart Augustsson wrote:
Here is a small puzzle.
-- The following generates a type error: f :: Char -> Char f c = let x = g c in h x
-- But this definition does not: f :: Char -> Char f c = let x :: Bool x = g c in h x
Furthermore, replacing Bool by any other type in the latter definition will always give a type error.
[...snip...]