[Rusky]

The point of dependent types is to check these uses of N and M at compile time symbolically, for all possible values, without having to "lift" their actual concrete values to compile time.

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.