From what I gather, this happens at runtime, which makes me feel it's a bit unfortunate to call it dependent types, or at least my view of dependent types is of it being a compile-time guarantee.

Take for example Liquid Haskell[0] where you can, at compile time, make guarantees about your code. For example, here's a function that makes division safe, by never allowing the second value, y, to be 0,

    {-@ safeDiv :: Int -> {v:Int | v != 0} -> Int @-}
    safeDiv     :: Int -> Int -> Int
    safeDiv x y = x `div` y

The second annotation is plain Haskell meaning it takes 2 `Int`s and returns an `Int`, with the third line being the function body. The first {-@ .. -} annotation is the one Liquid Haskell reads, stating it takes an `Int` as the first argument, another `Int`, which we now refer to as v, that is not 0, and finally returns an `Int`.

Another practical language with dependent types is Idris[1], which supports full dependent types with dependent pattern matching.

Finally, for the "why would I use this", I recommend checking out Gabriel Gonsalez's keynote, from Haskell eXchange 2017, "Scrap your Bounds Checks with Liquid Haskell"[2]

[0] https://ucsd-progsys.github.io/liquidhaskell-blog/

[1] https://www.idris-lang.org

[2] https://skillsmatter.com/skillscasts/10690-keynote-scrap-you...