Unsoundness due to where clauses not checked for well-formedness

[aliemjay]

This code does pass: (playground)

trait Outlives<'a>: 'a {} // without `: 'a`, it fails as expected.

fn t_is_static<T>()
where
    &'static T: Outlives<'static>,
{
}

But according to RFC 1214 functions are responsible for checking the well-formedness of their own where clauses. So this should fail and require an explicit bound T: 'static.

Here is an exploit of this unsoundness: (playground)

trait Outlives<'a>: 'a {}
impl<'a, T> Outlives<'a> for &'a T {}

fn step2<T>(t: T) -> &'static str
where
    &'static T: Outlives<'static>,
    T: AsRef<str>,
{
    AsRef::as_ref(Box::leak(Box::new(t) as Box<dyn AsRef<str> + 'static>))
}

fn step1<T>(t: T) -> &'static str
where
    for<'a> &'a T: Outlives<'a>,
    T: AsRef<str>,
{
    step2(t)
}

fn main() {
    let s: &'static str = step1(&String::from("blah blah blah"));
    println!("{s}");
}

@rustbot label C-bug T-compiler T-types A-lifetimes I-unsound

[steffahn]

This works, too

use std::fmt::Display;

trait Static: 'static {}
impl<T> Static for &'static T {}

fn foo<T: Display>(x: T) -> Box<dyn Display>
where
    &'static T: Static,
{
    Box::new(x)
}

fn main() {
    let s = foo(&String::from("blah blah blah"));
    println!("{s}");
}

(playground)

[steffahn]

Seems to compile since 1.14 (obviously without the dyn keyword, and without the naked "{s}").

[compiler-errors]

@steffahn's minimized example is much easier to work with:

use std::fmt::Display;

trait Static: 'static {}
impl<T> Static for &'static T {}

fn foo<S: Display>(x: S) -> Box<dyn Display>
where
    &'static S: Static,
{
    Box::new(x)
}

fn main() {
    let s = foo(&String::from("blah blah blah"));
    println!("{}", s);
}

Somewhere we're throwing bounds on the floor that we should be checking. Which function is responsible for ultimately checking that T: 'static is really is a mess to keep track of, honestly.

I guess it's worthwhile nominating this for T-types discussion.

[Dylan-DPC]

Marking this as p-high based on the discussion here

[jackh726]

Discussed in t-types meeting.

We think this will fall out of the ongoing work towards a-mir-formality. Namely here it's probably introducing WellFormed predicates for everything that is being proven. @lcnr is steadily making progress on this.

[jackh726]

Discussed in t-types meeting.

This link points to the prioritization discussion @jackh726

Thanks, fixed.

[lcnr]

@rustbot claim

already working in the area and want to take a closer look at this specific issue

[lcnr]

Summarizing what's going wrong in the minimized example:

use std::fmt::Display;

trait Static: 'static {}
impl<T> Static for &'static T {}

fn foo<S: Display>(x: S) -> Box<dyn Display>
where
    &'static S: Static,
{
    Box::new(x)
}

fn main() {
    let s = foo(&String::from("blah blah blah"));
    println!("{}", s);
}

We check that where-clauses of items when wfchecking that item, we do not recheck the where-clauses when using it. We assume this to be sound as instantiating a binder should not remove WF.

We check that &'static S: Static is WF in the param_env of the function. After elaborating super trait bounds this environment contains a &'static S: 'static bound, which gets destructures to result in a S: 'static clause. When now checking whether &'static S is well-formed, we are able to use that bound.

When calling that function we never check that &'static &'a String is well-formed. When applying the impl we also assume that the trait_ref is well-formed, as that should have been checked by wfcheck of the function. However, wfcheck of the function relied on the elaborated S: 'static bound which never gets proven here.

I think this should generally be fixed by also proving super trait bounds when using an impl (which is already part of our coinduction approach).

[lcnr]

actually: we can already elaborate any region constraints on traits when applying an impl. We can't check super traits because that requires coinduction, but adding a TypeOutlives constraint should already be possible.