There are plenty of optimizations that are only available when you know the types of the objects you're dealing with (mostly relating to aliasing). See:
Virtually every optimization even dynamic languages make are about narrowing down exactly what the type something is and which method that is called at runtime. At that point you can do things like inlining and other high powered optimizations.
Of course it does, and I never said it didn't. I just said that my impression is that the primary motivation of language people is correctness. However, I have published several in the area of software verification, so perhaps I am biased.
