We can, theoretically. We just haven't yet developed algorithms that are clever enough to make the correct optimizations to code in enough of the cases where such optimizations are possible. There are patterns in our code that we humans can write out when we write our code in C++, but that we haven't yet formalized and implemented for the computer to do.
There really has. D 1.0 has 20 days of life left, and D 2.0 is really amazing. It has the C++ idea of "it's only there if you want it" but taken to an amazing degree. Yes, it's a little more verbose than most FP languages, but honestly, if you're interested in verbosity, go use J or Coke.
The thing I like about D is that there's no surprises, everything works the way you'd expect it to. You can guess at what code should look like, and chances are it'll work.
Can you detail, or point to background info? There've been type system debates between proponents of Haskell, ocaml, SML, scala, and F#, i've never seen a D to Haskell comparison, and I've never seen D mentioned as a "free theorems" language. Maybe in this vid: