Do note however that the "proof" part of dependent types requires being able to evaluate arbitrary parts of the program at "compile time". (As a fact of the matter, there isn't even a clean phase separation between compile time and run time in dependently-typed languages; the distinction can only be reintroduced after-the-fact via "program extraction".) So, in a sense, types may depend on values in a dependently-typed language but this is merely an elaborate form of meta-programming, it need not establish a true dependence from runtime values. Whether Ada qualifies as a 'true' dependently-typed language, in this view, would depend on how strong its forms of guaranteed compile-time evaluation and meta-programming are.
It does look like the "discriminant" system of Ada shares key similarities with what dependently-typed languages call a "dependent sum", a generalized record type where "later" elements of the record can depend on "earlier" ones.
"Dependent products", on the other hand, can be viewed as an extended version
of generic functions, although they may also suffice to account for e.g. the examples given by OP of Ada's runtime range types and runtime-sized arrays. The key here being that the representation of a type is indeed given as a "function" of the value parameters that are "depended" on.
It does look like the "discriminant" system of Ada shares key similarities with what dependently-typed languages call a "dependent sum", a generalized record type where "later" elements of the record can depend on "earlier" ones.
"Dependent products", on the other hand, can be viewed as an extended version of generic functions, although they may also suffice to account for e.g. the examples given by OP of Ada's runtime range types and runtime-sized arrays. The key here being that the representation of a type is indeed given as a "function" of the value parameters that are "depended" on.