Roberto Zunino:
Yes, you are right, I didn't want to involve type classes and assumed 3::Int. A better example would be:
polyf :: Int -> a -> Int polyf x y = if x==0 then 0 else if x==1 then polyf (x-1) (\z->z) else polyf (x-2) ()
Here, passing both () and (\z->z) _does_ make inference fail.
Alternatively, type inference succeeds in rejecting an illegal program [1,2]. :-) So I think we need to be a little more precise about exactly what is undecideable in this example. Yes, the explicit type signature you've given is valid, and the Hindley-Milner type inference algorithm is not able to assign that type without an explicit signature. But that doesn't make Hindley-Milner type inference undecideable. On the contrary, Hindley-Milner type inference is deliberately designed to be decideable. To achieve that, it assumes monomorphic types in certain identifiable contexts, and therefore rejects some functions for which valid types exist. So I think the point you were making is that the problem of inferring the types of all functions for which valid types exist is, in general, undecideable. Hindley-Milner inference ensures decideability by choosing a somewhat less general (but still useful) problem. For what it's worth (not much), it might be possible to invent a decideable type inference which could infer types for a slightly larger set of functions (including polyf), by automatically generalising the types of arguments which are not inspected. Of course, doing so would presuppose the decideability of the subproblem of identifying unused arguments, and achieving that would undoubtedly require certain restrictions on the subproblem definition, analogous to the ones employed by Hindley-Milner. [1] http://haskell.org/onlinereport/decls.html#sect4.1.4 [2] http://haskell.org/onlinereport/decls.html#sect4.5