Skip to content

lack of implied bounds for opaque types in binders is unsound #153596

@lcnr

Description

@lcnr
trait Trait {
    type Assoc;
}
impl<'a, 'b: 'a> Trait for Inv<'a, 'b> {
    type Assoc = ();
}

trait ReqWf {}
impl<T: Trait> ReqWf for T where T::Assoc: Sized {}
struct Inv<'a, 'b: 'a>(Option<*mut &'a &'b ()>);
fn mk_opaque<'a, 'b>(x: &'a &'b u32) -> impl ReqWf {
    Inv::<'a, 'b>(None)
}

trait Bound<T> {}
impl<T, F, R: ReqWf> Bound<T> for F where F: FnOnce(T) -> R {}
trait ImpossiblePredicates<F> {
    fn call_me(&self)
    where
        F: for<'a, 'b> Bound<&'a &'b u32>,
    {
        println!("method body");
    }
}
impl<F> ImpossiblePredicates<F> for () {}
fn mk_trait_object<F>(_: F) -> Box<dyn ImpossiblePredicates<F>> {
    Box::new(())
}
pub fn main() {
    let obj = mk_trait_object(mk_opaque);
    obj.call_me(); // segfault
}

A more general version of #152735 (comment). This is not limited to coroutine witnesses.

The quick summary:

We use item-bounds of opaque types during analysis and normalize them during codegen.

fn impossible_predicates is used when building trait objects to avoid creating vtable entries for uncallable methods. We rely on the trait solver to be complete during codegen for soundness: if we successfully proved something during analysis, then this has to also be true in an empty environment during codegen.

The way implied bounds on binders works breaks this property. impl ReqWf: ReqWf is assumed to trivially hold as this has been proven inside of mk_opaque. However, this proof relies on the implied bound 'b: 'a from the function signature.

When we now check impl ReqWf: ReqWf during codegen, we instantiate 'b and 'a with placeholders without tracking implied bounds. Normalizing <Inv<'a, 'b> as Trait>::Assoc now adds a 'b: 'a requirement which does not hold.

Metadata

Metadata

Assignees

No one assigned

    Labels

    A-higher-rankedArea: Higher-ranked things (e.g., lifetimes, types, trait bounds aka HRTBs)A-impl-traitArea: `impl Trait`. Universally / existentially quantified anonymous types with static dispatch.A-implied-boundsArea: Implied bounds / inferred outlives-boundsA-lifetimesArea: Lifetimes / regionsA-type-systemArea: Type systemC-bugCategory: This is a bug.I-unsoundIssue: A soundness hole (worst kind of bug), see: https://en.wikipedia.org/wiki/SoundnessP-highHigh priorityT-typesRelevant to the types team, which will review and decide on the PR/issue.

    Type

    No type
    No fields configured for issues without a type.

    Projects

    Status

    open/unblocked

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions