This isn't quite trivial, but well… it works.
a “transmute” in safe Rust:
```ru…st
fn main() {
let s: String = transmute(vec![65_u8, 66, 67]);
println!("{s}"); // ABC
}
```
```rust
fn transmute<L, R>(x: L) -> R {
transmute_inner_1::<L, R, RewriteReflRight<FakeRefl<L, R>>>(x)
}
fn transmute_inner_1<L, R, P: TyEq<LHS = L, RHS = R>>(x: L) -> R {
transmute_inner_2::<<P::ProofIsProofValue as TyEq>::ProofDef, L, R, P::ProofValue, P>(x)
}
fn transmute_inner_2<Rw, L, R, Actual, P: TyEq<LHS = L, RHS = R, ProofValue = Actual>>(x: L) -> R
where
<Rw as TypeIs<P::ProofValue>>::Is: TyEq<LHS = L, RHS = R>,
{
transmute_inner_3::<L, R, Actual>(x)
}
fn transmute_inner_3<L, R, P: TyEq<LHS = L, RHS = R>>(x: L) -> R {
transmute_inner_4::<R, P::ProofDef>(x)
}
fn transmute_inner_4<R, Rw>(x: <Rw as TypeIs<R>>::Is) -> R {
x
}
```
```rust
trait TypeIs<T> {
type Is;
}
impl<_Self, T> TypeIs<T> for _Self {
type Is = T;
}
trait TyEq: TyEqImpl {
type ProofDef: TypeIs<Self::RHS, Is = Self::LHS>;
}
trait TyEqImpl {
type LHS;
type RHS;
type Proof<_Dummy>: TyEq<LHS = Self::LHS, RHS = Self::RHS>;
type ProofValue;
type ProofIsProofValue: TyEq<LHS = Self::Proof<()>, RHS = Self::ProofValue>;
}
trait DeriveEqFromImpl {}
impl<P: TyEqImpl + DeriveEqFromImpl> TyEq for P {
type ProofDef = <P::Proof<()> as TyEq>::ProofDef;
}
struct Refl<T>(T);
impl<T> TyEqImpl for Refl<T> {
type LHS = T;
type RHS = T;
type Proof<_Dummy> = Refl<T>;
type ProofValue = Refl<T>;
type ProofIsProofValue = Refl<Refl<T>>;
}
impl<T> TyEq for Refl<T> {
type ProofDef = ();
}
struct FakeRefl<L, R>(L, R);
impl<L, R> DeriveEqFromImpl for FakeRefl<L, R> {}
impl<L, R> TyEqImpl for FakeRefl<L, R> {
type LHS = L;
type RHS = R;
type Proof<_Dummy> = FakeRefl<L, R>;
type ProofValue = FakeRefl<L, R>;
type ProofIsProofValue = Refl<FakeRefl<L, R>>;
}
struct RewriteReflRight<P>(P);
impl<P> DeriveEqFromImpl for RewriteReflRight<P> {}
impl<P, L, R> TyEqImpl for RewriteReflRight<P>
where
P: TyEq<LHS = L, RHS = R>,
{
type LHS = L;
type RHS = R;
type Proof<_Dummy: RewriteReflRightHelper> = _Dummy::RewriteRight<Refl<L>, R, P::ProofDef>;
type ProofValue = Refl<L>;
type ProofIsProofValue = Refl<Refl<L>>;
}
trait RewriteReflRightHelper {
type RewriteRight<P, R, Rw>: TyEq<LHS = P::LHS, RHS = R>
where
P: TyEq<RHS = <Rw as TypeIs<R>>::Is>;
}
impl<_Dummy> RewriteReflRightHelper for _Dummy {
type RewriteRight<P, R, Rw>
= P
where
P: TyEq<RHS = <Rw as TypeIs<R>>::Is>;
}
```
([playground](https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=4b187258e5a6e000417190f0f14a1ec0))
Besides this unsoundness, there are [also many ICEs](https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=304c247937ece5930ec548a5a479256e). This isn't surprising, since we're not *really* transmuting, but rather sort-of … convincing the type system that the 2 types were never different in the first place.
```rust
fn main() {
let s: u8 = transmute(());
println!("{s:?}");
}
```
Or interesting LLVM-errors
```rust
fn main() {
let s: &() = transmute("hi");
println!("{s:?}");
}
```
```
Compiling playground v0.0.1 (/playground)
Invalid bitcast
%7 = bitcast { ptr, i64 } %6 to ptr, !dbg !425
in function _ZN10playground17transmute_inner_317h363424402e6a7153E
rustc-LLVM ERROR: Broken function found, compilation aborted!
error: could not compile `playground` (bin "playground")
```
Oh… [that one on nightly has… the compiler itself execute a SIGILL](https://play.rust-lang.org/?version=nightly&mode=debug&edition=2021&gist=54c7da3065e4d042f121662122cd3ffd)? (Is that actual UB in the compiler!? Or UB in LLVM? Or can SIGILL be part of a *deliberate* crash condition?)
---
From a background of “this works a bit like Coq”, the relevant parts that make this work is how:
* `FakeRefl<L, R>` is a “proof” that `L` and `R` are the same types, which doesn't terminate (i.e. it is cyclically defined in terms of itself)
* unlike true proof assistants, Rust's trait system does allow some stuff to be defined in a somewhat cyclical manner, especially pre-monomorphization
* overflow during monomorphization is avoided anyways by:
* introducing the `Rewrite…` step which rewrites `Refl<L>` (a proof of `TyEq<LHS = L, RHS = R>`) using this `FakeRefl` proof
* at the same time *also* tracking that the proof term itself doesn't actually change with the rewrite
* using this tracked meta-information in order to eliminate the usage of `FakeRefl` before its (indirectly and cyclically defined) `ProofDef` type ever ends up being instantiated
Of course, this is just my intuitive description from a user perspective :-)
---
I have no idea which part of this code to blame exactly. Perhaps someone else with better knowledge of the theory behind Rust's typesystem and trait system could have a better clue here.
~~I'm not quite sure if~~ this can perhaps be "simplified" to remove the need for GATs
**Update**: It *can* be "simplified" to remove the need for GATs. ([playground](https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=48cfb42cae4b059efa1cccf7f991b337))
**Update2**: It's [even possible](https://github.com/rust-lang/rust/issues/135011#issuecomment-2569925948) to rework this into working since Rust 1.1
<details><summary><i>(this section has become somewhat outdated due to this update, click to expand anyway)</i></summary>
I'm not quite sure if this can perhaps be "simplified" to remove the need for GATs; however, I wasn't able to the `Rewrite…` stuff to work without this trick
```rust
type Proof<_Dummy: RewriteReflRightHelper> = _Dummy::RewriteRight<Refl<L>, R, P::ProofDef>;
```
where the (vacuous) `_Dummy: RewriteReflRightHelper` restriction prevents the compiler from already knowing the concrete `RewriteReflRightHelper` impl. (If you worry about the syntactical mismatch of
```rust
type Proof<_Dummy: RewriteReflRightHelper>
```
here vs
```rust
type Proof<_Dummy>: TyEq<LHS = Self::LHS, RHS = Self::RHS>;
```
without bounds on `_Dummy` in the trait definition: that's [actually avoidable](https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=a8257758d8535f11dc9553456f809be7) (<- see this playground on how the bound can be repeated everywhere and the `impl RewriteReflRightHelper for …` can even be for a concrete type only).
So for now, I would conjecture that this soundness hole *does* require GATs.
*Edit:* I completely forgot about the (generous) usage of GATs *inside* of `RewriteReflRightHelper` ~ so, yes, GATs seem fairly integral to this.
*Edit2:* Nevermind, those [can all be eliminated](https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=55294bcb7b83a8f934a4180cab390099) leaving only a single GAT.
*(end of somewhat outdated section)*
</details>
---
This is not a regression. It also isn't influenced by `-Znext-solver`.
---
This is a relatively clean typesystem hole, on stable Rust, without many of the other known-problematic features such as HRTBs, lifetimes, variance, trait objects, or implicitly defined trait impls for functions/closures/etc…
@rustbot label I-unsound, I-ICE, I-crash, T-types, A-type-system, A-trait-system, A-associated-items