Ask HN: A well-typed program won't go wrong?

I've read a few times here on HN the saying "a well-typed program won't go wrong" or some slight variation. I don't think that can be correct, so I'm going to state my objection, and see if I'm right, or if someone can educate me.

Let's say I'm writing a recursive factorial function in Haskell. But, because it's early morning and the caffeine hasn't kicked in yet, I mess up the recursive call. I say "+ 1" instead of "- 1".

What is Haskell's type system going to say about this mistake? I believe it will say nothing at all, because the problem isn't the type of the value, it's the value of the value. But what's the program going to do? It's going to run until it exhausts memory, and then it's going to die in disgrace.

It seems to me that there are only four possibilities here:

1. Haskell's type system can in fact catch this error at compile time.

2. Despite its celebrated type system, Haskell is not a sufficient base for building a well-typed program, but some other language would be. (Coq? Agda? Some not-yet-existent language?)

3. Dying in disgrace rather than returning the correct value does not count as "going wrong".

4. The statement "a well-typed program won't go wrong" is false.

Of those options, I believe that number 4 is correct, but I am willing to listen to reasoned arguments to the contrary.