Tangential: How would the function `first :: &(Vec a) -> Option &a` (which, given a non-exclusive reference to a vector, returns a non-exclusive reference to th

Tangential: How would the function `first :: &(Vec a) -> Option &a` (which, given a non-exclusive reference to a vector, returns a non-exclusive reference to the first item of the vector, with the same lifetime) be typed using linear and / or dependent types? I'm certain that this can be modelled using dependent types (after all, anything can), but I can't think of a way to do it that's anywhere near as ergonomic as Rust.