Tracking issue for unsupported rust features

[Nadrieril]

This issue tracks language features we don't support yet.

• [x] dyn Trait: https://github.com/AeneasVerif/charon/issues/123
• [x] for<'a> bounds: https://github.com/AeneasVerif/charon/issues/67
• [x] String constants: https://github.com/AeneasVerif/charon/issues/72
• [x] enum as isize casting: https://github.com/AeneasVerif/charon/issues/91
• [x] Retain type aliases: https://github.com/AeneasVerif/charon/issues/134
• [x] Associated type equalities: https://github.com/AeneasVerif/charon/issues/127
• [x] Mutually recursive traits: https://github.com/AeneasVerif/charon/issues/94
• [x] Defaulted trait method implementations: https://github.com/AeneasVerif/aeneas/issues/70
• [ ] Correct Drop semantics: https://github.com/AeneasVerif/charon/issues/152
• [x] vec![...] macro: https://github.com/AeneasVerif/charon/issues/165
• [x] Unsafe code: https://github.com/AeneasVerif/charon/issues/280
• [x] Generalized associated types (GATs): https://github.com/AeneasVerif/charon/issues/477
• [ ] Return-position impl trait in trait (RPITIT): https://github.com/AeneasVerif/charon/issues/478
• [ ] Thread-local variables #560
• [ ] Contract annotations https://github.com/AeneasVerif/charon/issues/646