Better support for unsized types #608
Description
Currently the translation of unsized types requires the user to figure out metadata manipulation themselves: e.g. a cast from Box<[T; N]> to Box<[T]> makes a fat pointer but nothing in charon makes that clear.
Ideally charon would tell you exactly what metadata to use whenever creating a pointer that happens to be fat.
- Make explicit which metadata is used on a given unsizing coercion;
- Make pointer metadata tracking explicit;
- Support unsizing behind non-builtin pointers;