Repository: rust
Issue: Typesystem soundness hole involving cyclically-defined ATIT, and normalization in trait bounds
Labels: A-type-system,I-crash,I-ICE,A-trait-system,P-medium,A-associated-items,I-unsound,C-bug,T-types

This isn't quite trivial, but well… it works.

a “transmute” in safe Rust:
```rust
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