Let's say we're creating an array of strings separated by newlines obtained from reading a file. Call this arr[n] where n is determined at runtime.
Now let's have String index(arr:int[], i:(Fin(arr):int)), where FinInt(arr) is a dependent type that is an integer between zero and the length of the array. As the code is compiling, we have this
int i = 24951;
String str = index(f, i);
The file exists in the future after the compilation. If the future file has at least 24951+1 lines, then the compiler can verify that i < n and that i is correctly typed. But if the file is short, then the type of i is incorrect. So at compile-type the type of i is indeterminate.
you get a compile time error saying f isn't known to have enough entries, and you resolve it by adding a decidable check that produces a proof that it does. (the check at runtime is just >)
Now let's have String index(arr:int[], i:(Fin(arr):int)), where FinInt(arr) is a dependent type that is an integer between zero and the length of the array. As the code is compiling, we have this
int i = 24951; String str = index(f, i);
The file exists in the future after the compilation. If the future file has at least 24951+1 lines, then the compiler can verify that i < n and that i is correctly typed. But if the file is short, then the type of i is incorrect. So at compile-type the type of i is indeterminate.