Skip to content

implied bounds from associated types may not actually get implied pt 2. #98543

Closed
@lcnr

Description

@lcnr

revives #91068 which has been fixed by only considering implied bounds from projections if they don't normalize while typechecking the function itself

// We only add implied bounds for the normalized type as the unnormalized
// type may not actually get checked by the caller.
//
// Can otherwise be unsound, see #91068.
let TypeOpOutput { output: norm_ty, constraints: constraints1, .. } = self
.param_env
.and(type_op::normalize::Normalize::new(ty))
.fully_perform(self.infcx)
.unwrap_or_else(|_| {
self.infcx
.tcx
.sess
.delay_span_bug(DUMMY_SP, &format!("failed to normalize {:?}", ty));
TypeOpOutput {
output: self.infcx.tcx.ty_error(),
constraints: None,
error_info: None,
}
});
// Note: we need this in examples like
// ```
// trait Foo {
// type Bar;
// fn foo(&self) -> &Self::Bar;
// }
// impl Foo for () {
// type Bar = ();
// fn foo(&self) ->&() {}
// }
// ```
// Both &Self::Bar and &() are WF
let constraints_implied = self.add_implied_bounds(norm_ty);
normalized_inputs_and_output.push(norm_ty);
constraints1.into_iter().chain(constraints_implied)

This does not mean that the projection won't normalize when getting called:

trait Trait {
    type Type;
}

impl<T> Trait for T {
    type Type = ();
}

fn f<'a, 'b>(s: &'b str, _: <&'a &'b () as Trait>::Type) -> &'a str
where
    &'a &'b (): Trait, // <- adding this bound is the change from #91068 
{
    s
}

fn main() {
    let x = String::from("Hello World!");
    let y = f(&x, ());
    drop(x);
    println!("{}", y);
}

The added bound prevents <&'a &'b () as Trait>::Type from getting normalized while borrowchecking f, as we prefer param candidates over impl candidates. When calling f, we don't have the &'a &'b (): Trait in our param_env, so we can now freely use the impl candidate to normalize the projection. The caller therefore doesn't have to prove that &'a &'b () is well formed, causing unsoundness.

I am a bit surprised that the caller doesn't have to prove that the &'a &'b (): Trait obligation is well formed, which would cause this example to not be unsound. It doesn't remove the general unsoundness here though. Here's an alternative test where that isn't enough:

trait Trait {
    type Type;
}

impl<T> Trait for T {
    type Type = ();
}

fn f<'a, 'b>(s: &'b str, _: <&'a &'b () as Trait>::Type) -> &'a str
where
    for<'what, 'ever> &'what &'ever (): Trait,
{
    s
}

fn main() {
    let x = String::from("Hello World!");
    let y = f(&x, ());
    drop(x);
    println!("{}", y);
}

Metadata

Metadata

Assignees

No one assigned

    Labels

    A-associated-itemsArea: Associated items (types, constants & functions)A-implied-boundsArea: Implied bounds / inferred outlives-boundsC-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

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions