Basically when you take some value the user gives you and cast it to the dependent type, you can then cover the case where you got some result because the cast was successful or you got none. You can't have dependent types at compile time, at least not completely so, though you could use something like fslint to catch any data being entered in code.

https://news.ycombinator.com/item?id=7567310

it would seem that in practice you can go even further, essentially writing exhaustive proofs. However F* already supports this and compiles to F#, so I would say if you want that level of correctness you should probably use a language which is better at describing the totality of a function.

I'm pretty sure there are vector libraries available to F#. Dig around and you will find them. Then just apply dependent type to a type in that library. I don't work with them myself.

I'm not asking specifically about vectors, that's just a common example of a dependent type. To take another example from the documentation, can you express a type like

    type digits = RegexString (Regex "^[0-9]+$")

where all values of type digits are strings containing only digits? Then

    let s1 : digits = "1234"

would typecheck but

    let s2 : digits = "abc"

would not? That would be very surprising given the F# type system.