If a compiler infers types at compile-time for a dynamically typed language, I still consider that "static typing" because it's statically inferring the types. If the term "static typing" is the problem, then I can rephrase: it only comes up when you try to determine all types before executing the program.
At this point I would like to remind both you and soc88 of a parable:
Patient: Doctor, it hurts when I do this.
Doctor: Well, don't do that.
(Soc88's response, in the context of this parable, is something along the lines of, "But anyone who doesn't do this is a moron.")
Inferring types at compile time is necessarily hard. It is a corollary of the halting problem that no static type inference can be perfect. Therefore you have the following choices:
1. A simple compiler that sometimes fails to identify type errors at compile time
2. A simple compiler that sometimes produces false positives (i.e. signals a type error in a program that is in fact correct)
3. A complicated compiler. (Note that even a complicated compiler will also do 1 or 2 or both, but potentially less often than a simple compiler.)
Those are your only options. Reasonable people can disagree over which is preferable.
I don't disagree with your points, but now that we've established that, that is why your original example does not solve the problem as presented in the post. The problem inherently has to do with statically inferring types.
That depends on what you consider to be "solving the problem." Do you want to "do this" or do you want to be free from pain? You can have one or the other, but not both.
OF COURSE static type inference is hard. That's a straightforward consequence of the halting problem. Pointing to defmethod is just an oblique way of making the point that perfect type inference is NOT NECESSARY for getting things done. You can choose to lament the complexity of Scala (and static type inferencing in general) or you can use Lisp or Python and trade certain compile-time guarantees for simplicity. Like I said, reasonable people can disagree over which is preferable.
What reasonable people cannot do is insist that there is a single perfect solution that is both simple and error-free. Anyone who believes that has not understood the implications of the halting problem.
Another thing reasonable people cannot do is frame the tradeoff as a binary choice: either you use static type inferencing, or you give up all compile-time guarantees. That is simply not true, as is amply demonstrated by e.g. the SBCL compiler. It's a complex, multi-dimensional space of tradeoffs in language design, compiler complexity, and different kinds of compile-time guarantees. It's INHERENTLY complicated. The best you can hope to do is find a reasonable point in the design space for your particular quality metric. For the OP, Scala isn't it.
Since the OP uses Scala to solve his problems, I have a feeling that Scala is, to him, a reasonable place in the design space. Scala allows a function much like your example. He used that example not say "This is a failing of Scala, and why I will not use it," but to say "This example demonstrates a complexity that is a natural consequence of the design of Scala." In other words, he said something quite similar to what you said.
> Scala is, to him, a reasonable place in the design space
Reasonable perhaps, but manifestly not ideal or he would not be complaining about how complex it is.
> he said something quite similar to what you said
Well, I didn't actually say much, I just posted a snippet of code and left people to draw their own conclusions. Why soc88 chose to start a fight I can only guess, but it seems to be not uncommon behavior among people trying to defend untenable positions.
> A simple compiler that sometimes requires a type annotation.
It is easy to show that that will not solve the problem. If your language is Turing-complete, then you can embed (say) a Lisp interpreter and arbitrary Lisp code within it. The only way your compiler can be complete and correct for your language is for it to be complete and correct for this embedded Lisp. This is a fundamental result. There is no way around it.