How can SML infer types like this?

Wikipedia says:

fun factorial n = 
    if n = 0 then 1 else n * factorial (n-1)

A Standard ML compiler is required to infer the static type int -> int of this function
without user-supplied type annotations. I.e., it has to deduce that n
is only used with integer expressions, and must therefore itself be an
integer, and that all value-producing expressions within the function
return integers.

I don't understand how a compiler could infer this. It sounds like SML is essentially solving the halting problem for the factorial function, and showing that it only halts on positive integer inputs.

Am I missing something?

The classic Hindley-Milner type inference algorithm requires each literal value to be unambiguously inferable to a type: 0 is an int, while 0.0 is a real. Haskell's type system has been enhanced to include a certain kind of bounded polymorphism, so that 0 can have any type that is a number (more precisely, of any type that is an instance of the Num type class: 0 is of type Num a => a).

See the wikipedia article on Hindley-Milner for further details on the algorithm (the article explanations are much better than anything I could write on that topic).

StackExchange Computer Science Q#9407, answer score: 8