assoc types in binders can pass wf check but error when trying to normalize via impl

[carlini]

I've been using LLMs to find soundness issues in various programs, including rust. This bug was discussed on zulip (t-types thread) where @lcnr diagnosed the root cause and believes it affects stable (and also identified the regressing PR). Filing the bug here.

I tried this code:

#![forbid(unsafe_code)]
use std::any::type_name;

trait Overlap {
    type Out;
}

impl<T: ?Sized + Gated> Overlap for T
where
    for<'a> <T as Gated>::Assoc<'a>: Copy,
{
    type Out = usize;
}

impl Overlap for str {
    type Out = &'static u64;
}

trait Gated {
    type Assoc<'a>: Copy
    where
        Self: Sized;
}
impl Gated for str {}

fn cast<T: ?Sized + Gated>() -> <T as Overlap>::Out {
    println!("cast: Out = {}", type_name::<<T as Overlap>::Out>()); // usize
    8
}

fn main() {
    let r = cast::<str>();
    println!("main: Out = {} = {r:p}", type_name::<<str as Overlap>::Out>()); // &u64 = 0x8
    println!("{}", *r); // SIGSEGV
}

compiled with -Znext-solver.

I expected to see this happen: the program is rejected

Instead, this happened: -Znext-solver accepts it and the program prints

cast: Out = usize
main: Out = &u64 = 0x8
Segmentation fault

From @lcnr's analysis, the underlying issue also affects stable, : https://rust.godbolt.org/z/7scG3Pqjh (and a second demonstration in impossible_predicates: https://rust.godbolt.org/z/fG6v7K6fP). Also found the regression to be #144064 (comment) (https://rust.godbolt.org/z/Mb4ExdjeG).

Meta

nightly: rustc 1.100.0-nightly (8fa1c96cf 2026-08-17)
stable (old solver rejects the program above; stable godbolt link above shows the underlying issue): rustc 1.97.1 (8bab26f4f 2026-07-14)

Root cause (analysis by lcnr)

<T as Gated>::Assoc<'a>: Copy does not make sense because the associated type is only well-formed if T is Sized — now clearly, this should not be allowed. This error is ignored in WF check. This error is not ignored when actually normalizing, because we've instantiated the binder at this point.

What exactly is going on:

• we have a type which implements a trait, with a GAT where-clause that may not hold
• trying to normalize that where-clause for this type always errors as normalization rechecks GAT item bounds
• we don't check GAT where-clauses in well-formedness checking of the impl if they reference bound variables
• using an item bound does not need to prove GAT where-bounds
• this means using an impl with that where-clause must use an item bound instead of actually the impl itself, causing the impl to be applicable
• when normalizing via a concrete impl [it] does check GAT where-clauses, so the impl no longer applies

A stupid fix would be to not check GAT where-clauses in coherence when using impls — [but that is] insufficient, [it] also causes problems in impossible_predicates (godbolt link above). The proper fix is the higher-ranked region rework.

[lcnr]

marking as P-medium as while this is an unsoundness, it's very hard to hit by accident, you need:

• a higher-ranked where-bound that can be proven via an item bound of the self type
• this where-bound has a WF requirement which does not hold, but gets ignored because it references a bound variable
• actually exploit this setup

[lcnr]

this is an incompleteness without involving inference variables, so it affects coherence (as in the issue text) and impossible_predicates, e.g.

trait NotImplemented {}
trait GatBound {
    type Assoc<T>: Copy
    where
        T: NotImplemented;
}
impl<T> GatBound for T {
    type Assoc<U> = u32
    where
        U: NotImplemented;
}

trait TraitMethod<T: GatBound> {
    fn sadness(&self)
    where
        for<'a> <T as GatBound>::Assoc<&'a u32>: Copy
    {
        println!("hi there");
    }
}
impl<T: GatBound, U> TraitMethod<T> for U {}



fn foo<T: GatBound>(x: &dyn TraitMethod<T>) { x.sadness() }

fn main() {
    foo::<u32>(&1);
}