Fin, Vect and restrict in idris

It seems like a bit of a trap that restrict yields Fin (S n) for a Vect (S n) but it’s giving a type level protection from trying to access a member of a Vect with zero elements (as mod used under the hood is not total for 0 anway). It’s fair enough when you’re putting a function at the top level, as you can capture one less than the Vect’s length in an implicit param like this:

prepend_to_group : {tsm1 : Nat} -> (rsize : Nat) -> Nat -> Vect rsize x -> Vect (S tsm1) x -> Vect (S rsize) x

tsm1 is captured structurally as one less than the length of the vect, so restrict can use this value.

But what if you’re implementing a typeclass method like this?

interface ContainsBytes a where
  get_byte : a -> Nat -> Nat

Vect (S l) Nat is a natural fit for this:

implementation ContainsBytes (Vect (S l) Nat) where
 get_byte a n = ?get_byte_of_vect_impl

But there’s a problem: we don’t actually have an implicit available for the length of the Vect. Structurally, we’ve guaranteed that the problem can be solved, but some proof machinery is needed, otherwise:

Can’t solve constraint between: pred (length a) and l

I needed two proofs, and admittedly I tend not to be an exhaustive reader, so it’s possible the analog of at least the first of these is waiting in the standard library and I wasn’t able to locate it:

vectLengthIsL : {ll : Nat} -> (v : Vect ll x) -> length v = ll
vectLengthIsL Vect.Nil = Refl
vectLengthIsL (Vect.(::) _ rest) =
 rewrite vectLengthIsL rest in
 Refl

Fairly straightforward proof that l = length (Vect l v) … that allows us to recover what would have been the implicit argument and swap (length v) for it.

The other proof target we need is to allow us to replace ll with S (pred ll). Since it’s greater than one we know that’s possible:

ifVectLenIsSLThenPredVectLenIsL : {ll : Nat} -> (v : Vect (S ll) x) -> pred (length v) = ll
ifVectLenIsSLThenPredVectLenIsL v =
 rewrite vectLengthIsL v in
 Refl

Since the type is recoverable, we can use vectLengthIsL to rewrite (length v) as (S ll) in context and rewrite ll as pred (length v), giving the resulting Fin a type describing the number we have.

The result was type rewriting that got us where we wanted to be:

implementation ContainsBytes (Vect (S l) Nat) where
 get_byte a n =
 let
   lastElementOf : Nat
   lastElementOf = pred (length a)
   indexIntoVect : Fin (S l)
   indexIntoVect =
     rewrite sym (ifVectLenIsSLThenPredVectLenIsL a) in
     restrict lastElementOf (cast n) -- Fin (S (pred (length a)))
 in
 index indexIntoVect a

A small inconvenience but also a chance to look at how rewriting can allow us to construct a Fin that idris doesn’t initially 100% know belongs to the bounds of the Vect it has.