The big advantage to liquid types, a la liquid haskell, is that you get far more inference than you can get in full dependent typing.

I still think liquid haskell is too immature (Integer is not a good theory for Int, type classes aren't handled well, etc), but the promise is fascinating if the issues get worked out.