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.