The obvious solution is that the standard library would provide both options wherever appropriate, just like Rust has `borrow` and `borrow_mut`, `raw_entry` and `raw_entry_mut`, etc. You might be able to save some of this pain with some polymorphism, as some people suggest[0] for `&` and `&mut`, too.

It might also be a good idea to look at the standard library of Idris 2[1] — it has linear types and garbage collection, so it has many of the same issues you describe, and it also seems to solve them with duplication where necessary[2], at least sometimes.

[0]: https://github.com/rust-lang/rfcs/issues/414

[1]: https://github.com/idris-lang/Idris2/tree/master/libs/base

[2]: https://github.com/idris-lang/Idris2/blob/master/libs/base/D...