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.