Adding examples, with dependent types we can write the type-safe printf in Idris:

https://github.com/chrisdone/sandbox/blob/master/dependently...

Meanwhile with Liquid Haskell (refinement types), it was really easy for me to define a date data type that can only construct valid year-month-day combinations:

https://github.com/chrisdone/sandbox/blob/master/liquid-hask...

The `if ..` tests are all required, otherwise Liquid Haskell rejects the program.

So I see value in both directions, if you extrapolate from these examples to harder problems.