This is true even for expressions that are only evaluated in a compile-time context, since dependently-typed languages do "everything" at compile time anyway, they don't have a phase distinction where you can talk about "runtime" being separate.
This is true even for expressions that are only evaluated in a compile-time context, since dependently-typed languages do "everything" at compile time anyway, they don't have a phase distinction where you can talk about "runtime" being separate.
A truly dependently typed language performs these checks before instantiation time, by evaluating those expressions abstractly. Code that is polymorphic over values is checked for all possible instantiations, and thus its types can actually depend on values that will not be known until runtime.
The classic example is a dynamic array whose type includes its size- you can write something like `concat(vector<int, N>, vector<int, M>) -> vector<int, N + M>` and call this on e.g. arrays you have read from a file or over the network. The compiler doesn't care what N and M are, exactly- it only cares that `concat` always produces a result with the length `N + M`.
To be clear this distinction is not unique to dependent types, either. Most languages with some form of generics or polymorphism check the definition of the generic function/type/etc against the constraints, so the compiler can report errors before it ever sees any instantiations. This just also happens to be a prerequisite to consider something "dependently typed."
Notably Rust type-based generics do this, a key difference wrt. C++ templates. (You can use macros if you want checks after instantiation, of course.)
Rust already does have some level of const generic expressions, but they are indeed only possible to instantiate with values known at compile time, like C++.
The difficulty of type checking them symbolically still applies regardless of how they're instantiated, but OTOH it doesn't look like Rust is really trying to go that direction.
Typical implementations of dependent types do not generate a separate copy of a function for every instantiation, the way C++ does, so they simply do not need the concrete values in the same way.