Inferred type appears to detect an infinite loop, but what's really happening?

In Andrew Koenig’s An anecdote about ML type inference, the author uses implementation of merge sort as a learning exercise for ML and is pleased to find an “incorrect” type inference.

Much to my surprise, the compiler reported a type of

'a list -> int list

In other words, this sort function accepts a list of any type at all and returns a list of integers.

That is impossible. The output must be a permutation of the input; how can it possibly have a different type? The reader will surely find my first impulse familiar: I wondered if I had uncovered a bug in the compiler!

After thinking about it some more, I realized that there was another way in which the function could ignore its argument: perhaps it sometimes didn't return at all. Indeed, when I tried it, that is exactly what happened: sort(nil) did return nil, but sorting any non-empty list would go into an infinite recursion loop.

When translated to Haskell

split [] = ([], [])
split [x] = ([x], [])
split (x:y:xs) = (x:s1, y:s2)
  where (s1,s2) = split xs

merge xs [] = xs
merge [] ys = ys
merge xx@(x:xs) yy@(y:ys)
  | x < y     = x : merge xs yy
  | otherwise = y : merge xx ys

mergesort [] = []
mergesort xs = merge (mergesort p) (mergesort q)
  where (p,q) = split xs

GHC infers a similar type:

*Main> :t mergesort
mergesort :: (Ord a) => [t] -> [a]

How does the Damas–Hindley–Milner algorithm infer this type?