Skip to content

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

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);
}

No activity

Activity on this issue will appear here.

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

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