In what situations do you specifically prefer a dynamically typed language and why?

Like you, I am a big fan of type inference. Scala is my primary language these days, but I really came to appreciate the power of type inference when I did some stuff with SML years ago. The ability to almost never specify a type but know that you always have complete type safety is really nice.

I have mixed feelings about gradual typing. I’d love to see a language with “gradual proving”. Have an IDE or another tool that works with an interactive theorem prover and lets you prove chunks of code are completely correct one method/function at a time. Probably would be most useful in functional languages, but it is still something I would love to see.