[Haskell-beginners] A type level programming question

[Levi Stephen]

Hi,

I was looking at Data.Param.FSVec from parameterized-data [1].

The method to retrieve an element from a FSVec has the following type:

(!) :: (Pos s, Nat i, i :<: s) => FSVec s a -> i -> a

I was wondering if it was possible to write a function of type:

elementAt :: FSVec s a -> Int -> a

that called the above function, throwing an error if the index was out
of bounds. e.g.,

elementAt v idx | idx < 0 || idx > length v = error "Out of bounds"
                | otherwise = ....

But, I can't figure out how to implement the otherwise part. In
particular I can't work out how to call the (!) function with the i
:<: s class constraint satisfied.

Thanks,
Levi