There are some deficiencies, most prominently that the “role” system is aggressively monomorphic, so you can’t always prove that two things are coercible—the compiler must conservatively assume that type parameters with unknown roles cannot be coerced—but overall it’s much better than what we had before, and I expect it’ll continue to improve.
It cites the Haskell work: https://github.com/jswrenn/rfcs/blob/safer-transmute/text/00...
I’m thinking about a similar sort of coercion system for a language project, and it’s good to have a slightly broader view of the design space. This area hasn’t been very well explored yet, not just in terms of semantics, but also developer ergonomics: most of the time you want to hide representations for convenience, but when considering safe coercions, you really want to make it possible to talk about them explicitly & precisely.
This feature is also very subtle, and right at the very edge of the type system, so it’s extremely easy to break soundness here, usually by failing to consider things like variance. The reason “roles” were added to GHC in the first place isn’t just because of the issue with type families / associated types mentioned in that RFC; it’s also because anything that provides a safe API atop unsafe internals could also be used to violate soundness, especially in conjunction with mutation. The classic examples are: 1. coercing “container of A” to “container of B” using the coercion from A to B, then inserting a B that is not a valid A, either in its value or just because A and B have incompatible trait instances (like ordering or hashing). You need to be able to disallow conversions between things even if they have identical representations.
I’m pretty sure that declaring both `Item` and `SecureVec` as `#[repr(transparent)]` would cover that last 0.0001% chance: it protects against the extra fields becoming non-zero-size by accident and forces the binary representation to be identical to the first field.
At that point, he’s transmuting between things with the same representation; all that’s left to verify is semantics.
Admittedly the SecureVec example is more understandable: because the generic is passed through to Item as well, you’ll need to convert the Vec<Item<T, ItemLevel>> to a Vec<Item<T, MaxLevel<ItemLevel, VecLevel>>>, which… well, it can be done readily enough without unsafe code, by consuming the Vec, mapping each item and collecting to a new vec, but short of a kind of specialisation magic that I don’t think will kick in in this case, that’s going to entail allocating a new vector, so that I would be inclined to use unsafe code here for efficiency; but care should still be taken that it doesn’t invoke undefined behaviour.
But one more word in defence of the transmutes: it makes it obvious that it’s either zero-cost or just a copy, whereas more involved things can become subject to compiler optimisations, so that you don’t know that the whole supposedly-noop transformation will be being optimised out of existence. That confidence and clearly-stated intent is valuable.