[alkonaut]

I know idris (apart from improving some haskell warts) also adds dependent types. Are there any good simple examples of dependent type use, that isnot vectors-of-length-N?

[mej10]

The type safe printf implementation is pretty cool as another small example. https://github.com/mukeshtiwari/Idris/blob/master/Printf.idr

[nv-vn]

Yes. They're amazing for theorem proving (see Agda, Idris). They're also useful for refinement types, proving type class laws like for monads, etc.

[alkonaut]

Is there a hello world-y example of refinement types, similar to Vectors with length?