Well, I can't be bothered to edit wikipedia, but it's a confusing claim. Dependent typing does not require runtime information, results can be produced at compile time. The dependent type depends on a value, but the interesting property of the value is independently tracked in the type system, it's not retrieved from runtime information.

The gist of how it works is so:

    createEmptyIntList() => List<size=0, content=int> {...}
    push(List<size=a, content=b>) => List<size=a+1, content=b> {...}
    firstElement(List<size=a, content=b> | a > 0) => b {...}

In this example, you don't need to know runtime values, you need to know that you can safely get the first element. For that, you just need to know that something has been pushed at least once in the list.

Since push returns a type that is different from createEmptyList, your typesystem has this information.

> The value does not exist during compilation.

    type Z = []["length"]
    type One = [0]["length"]
    type Two = [0,0]["length"]

The "value" in this case is symbolic, sort of like defining an array with variable length arr[x] and having the compiler verify that arr[x+5] is always out of bounds before knowing the actual value of x. If the type system is not powerful to prove correctness of some expression, you will need to insert a runtime check that lets the compiler to trust the value at compile time.