Uncheckable bugs

Here's a bug that's hard to find automatically:

fib :: Num a => a -> a
fib 1 = 1
fib n = n * fib (n - 1)

See the bug? No typechecker can. More precisely, no checker (whether of type or anything else) can detect the problem without further information about what the function is supposed to do, because it does something reasonable. It's the wrong reasonable thing, but an uninformed checker has no way of knowing that.

This is why tests are useful: they provide constraints specific to the program. There are other kinds of checkable declarations (e.g. invariants, reference implementations) that are even more powerful. I suspect they're not used much only because they're harder to implement and harder to use.

Edit: fixed type declaration. That wasn't the intended bug.