GHC/Haskell is edging towards what could be called weak dependent typing or type-level programming, look at Weirich deck and phantom types:

http://www.cis.upenn.edu/~sweirich/plmw12/Slides/plmw12-Pier...

http://www.haskell.org/haskellwiki/Phantom_type

http://stackoverflow.com/questions/8600692/datatype-promotio...

For scala:

http://groups.google.com/group/scala-internals/browse_frm/th...

http://www.chuusai.com/2012/01/27/type-level-sorting-in-shap...

-------------

SAT and SMT solvers, e.g. in OCaml

http://caml.inria.fr/cgi-bin/hump.cgi?contrib=706

-----------------

I could give a few dozen more examples in these 3 languages, incluindg Coq which is written in C and OCaml, and agda and idris and others, which are written in C and haskell, or compile down to some stage of haskell compilation.