Have you ever used anything in the ML family of languages (e.g OCaml/Standard ML/Haskell)? You barely ever have to write types in these as long as your program makes sense..
Right on. I'm not sure I'd go so far as wanting the language to be as strict/typesafe as those (also calling Haskell an ML derivative is kind of funny, but I know what you mean)
Perhaps? It's unclear that a JIT with type inference will give you better performance than compiling (especially if you were to do profile guided optimization) (sidethought: not sure if llvm has support for PGO).
Also, if most of your types are static anyway (which in my middling amount of experience, they tend to be), I personally would rather get compile time errors rather than runtime errors. But maybe thats just me.