I've mentioned Common Lisp and Dylan as languages which allow a programmer to add type constraints to your program. What I haven't discussed is the idea of having tools that can put the types in for you, or show you (as part of the IDE, what it thinks the types should be). This is just a different way to use type inference. I think that we can have dynamically typed languages with tools that can show us static constraints like types, so when we read programs we can benefit from that information, and when we write we still have the ability to change the program quickly and easily. Check out the work that the PLT Scheme folks are doing, in particular, MrSpidey and MrFlow.

I think that we can have both. We're not there yet, but we're getting closer.