Think a better definition of Idris would be Haskell with theorem proving and not forcing lazy everything.

It's compiled with C compiler or to JavaScript currently, no JVM implementation. You might be confused with Scala.