[Haskell-beginners] A type level programming question

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