Comment by rq1

Imagine you read a value from stdin and parse it as:

Maybe Int

So your program splits into two branches:

1. Nothing branch: you failed to obtain an Int.

There is no integer to use as an index, so you can’t even attempt a safe lookup into something like Vect n a.

2. Just i branch: you do have an Int called i.

But an Int is not automatically a valid index for Vect n a, because vectors are indexed by Fin n (a proof carrying “bounded natural”).

So inside the Just i branch, you refine further:

3. Try to turn the runtime integer i into a value of type Fin n.

There are two typical shapes of this step:

* Checked conversion returning Maybe (Fin n)

If the integer is in range, you get Just (fin : Fin n). Otherwise Nothing.

Checked conversion returning evidence (proof) that it’s in range

For example: produce k : Nat plus a proof like k < n (or LTE (S k) n), and then you can construct Fin n from that evidence.

(But it’s the same basically, you end up with a “Maybe LTE…”

Now if you also have a vector: xs : Vect n a

… the n in Fin n and the n in Vect n a are the same n (that’s what “unifies” means here: the types line up), so you can do: index fin xs : a

And crucially:

there is no branch in which you can call index without having constructed the Fin n first, so out-of-bounds access is unrepresentable (it’s not “checked later”, it’s “cannot be expressed”).

And within _that_ branch of the program, you have a proof of Fin n.

Said differently: you don’t get “compile-time knowledge of i”; you get a compile-time guarantee that whatever value you ended up with satisfies a predicate.

Concretely: you run a runtime check i < n. _ONCE_

If it fails, you’re in a branch where you do not have Fin n.

If it succeeds, you construct fin : Fin n at runtime (it’s a value, you can’t get around that), but its type encodes the invariant “in bounds”/check was done somewhere in this branch.