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