I'm not sure if they will meet your standards, but Idris and ATS strive to be practical dependently typed languages:

http://www.ats-lang.org/Examples.html http://www.idris-lang.org/