If "prover" just means "has dependent types" then that's a much larger class than it sounds like. I write a lot of Scala, which has dependent types, but most of the code I write is just ordinary web services.
I don't understand the distinction you're drawing. Idris' type level functions are easier to write than Scala's but they don't seem to be able to do anything that Scala ones can't.
