Safer backpermute

[mniip]

Currently there are two versions of backpermute:

backpermute :: Vector m a -> Vector n Int -> Vector n a
unsafeBackpermute :: Vector m a -> Vector n Int -> Vector n a

The former does bounds checking to validate that the Int is a valid index for Vector m, the latter does not.

Seems like a missed opportunity to use a datatype that already did the bounds checking:

safeBackpermute :: Vector m a -> Vector n (Finite m) -> Vector n a

Possible implementation:

safeBackpermute xs is = Sized.unsafeBackpermute xs
  -- safe by construction of Finite m
  $ Sized.map (fromInteger . getFinite) is
  -- unsafeBackpermute already goes through Bundle, so this map should fuse