[Haskell-cafe] Why does Haskell not infer most general type?

Is haskell supposed to always infer the most general type (barring extensions)? I found a simple case where this is not true: f _ = undefined where _ = y :: Int -> Int y x = undefined where _ = f x Haskell infers the types of 'y' and 'f' as: f :: Int -> a y :: Int -> Int This confused me at first, but after thinking about it a while it seemed to make sense. But then my friend John pointed out that you can add type sigs for 'f' and 'y': f :: a -> b y :: a -> b and have it still typecheck! This thoroughly confused me. Why does haskell not infer the most general type for these functions? Is it a limitation of the algorithm? a limitation of the recursive let binding? Any insight would be appreciated :) - Job