archives

Inference of Polymorphic Recursion

In the following (Haskell) example, the type annotation on f is required:

f :: a -> (Int, a)
f x = (g True, x)

g True = 0
g False = fst (f 'a') + fst (f 0)

main = do
    print (fst (f True))

I can understand why in general, but I wonder if we could just decide to generalize arbitrarily in the order that declarations appear so that in this case the type of f would be inferred but if you switched the definition order you'd get a type error. When f is generalized, g would be constrained Bool -> b where b would be unified after generalization. Is this something that might work (but isn't done because it's arbitrary and makes definition order matter) or are there hard cases I need to consider?

Thanks