(I am not actually 100% sure if rfc 2000 meets the by-the-book definition of "dependent types", my copy of Pierce has been collecting dust. Really gotta study up more on this stuff.)
I believe in order to be dependent, a value needs to be able to affect the type somehow. So something like:
fn make_array(n: usize) -> [u8; n]
would do the trick.
I am guessing this isn't actually the feature though, and that it's not allowing dependence in this way, but rather promoting some const values and const functions to the type level (which is really useful, but not exactly dependent types)
Honestly I'm not totally sure either, however even if const-generics were technically dependant types enough to be called them with a straight face then I'm not sure if you get the benefits of them e.g. the textbook example seems to be static reasoning about the length of the result of appending two vectors of fixed but unknown lengths. The current proposal just seems like a convenient but theoretically shallow approximation of that due to the requirement of the const-parameter being known at compile time.
One roundabout way of doing this - which is very much possible in D but not worth doing because you can't really do useful work with it for the most part due to pain - is that if you extend (say) const-generics to work with basically anything evaluable at compile time, you can build up a data structure to represent and hold true some predicate about a runtime value in a type (as a template/generic parameter), then define how these combine under binary operations (trivial so far in D at least, impossible in C++, no idea about Rust - monomorphization differences aside), then use this datastructure for evil and profit (like giving invariants to the optimizer).
I would like to see how far the aforementioned idea can go, however it quickly becomes "write a compiler at compile time" or worse "write an SMT solver at compile time", both of which do not thrill me.
That's why the feature flag was "min_const_generics", we do plan on extending it more in the future, but you have to start somewhere, and even this tiny, tiny slice gives a lot of power.
I still want to try the ZZ language (https://github.com/zetzit/zz) someday. It compiles to C, and uses a SMT solver to prove that you don't index out-of-bounds at compile time. But I don't like how it lacks generics, uses C idioms, and compiles to C.
* https://github.com/rust-lang/rfcs/pull/1657
* https://github.com/rust-lang/rfcs/issues/1930
* https://github.com/rust-lang/rfcs/pull/2000 (the design that was accepted, in the end)
(I am not actually 100% sure if rfc 2000 meets the by-the-book definition of "dependent types", my copy of Pierce has been collecting dust. Really gotta study up more on this stuff.)