TAITs must not require fewer bounds than their defining scope

We consider the following pattern to be sound afaik:

mod prove_outlives {
    use std::marker::{PhantomData};
    #[derive(Copy, Clone, PartialEq, Eq)]
    pub struct OutlivesProof<'a, 'b>(PhantomData<*mut (&'a (), &'b ())>);
    impl<'a: 'b, 'b> OutlivesProof<'a, 'b> {
        pub const fn mk() -> Self {
            OutlivesProof(PhantomData)
        }
    }
    impl<'a, 'b> OutlivesProof<'a, 'b> {
        pub fn apply(self, x: &'a str) -> &'b str {
            // SAFETY: We've required `'a: 'b` when constructing the
            // proof object and both regions are invariant.
            unsafe { std::mem::transmute(x) }
        }
    }
}

now consider the following entirely safe code:

pub use prove_outlives::*;
// We're using const generics to move a `OutlivesProof` object into the type
// system so that we never have to actually call the defining function to use
// this proof.
struct ConstOutlives<'a, 'b, const PROOF: OutlivesProof<'a, 'b>>(Option<*mut (&'a (), &'b ())>);
trait Cast<'a, 'b> {
    fn cast(x: &'a str) -> &'b str;
}
impl<'a, 'b, const PROOF: OutlivesProof<'a, 'b>> Cast<'a, 'b> for ConstOutlives<'a, 'b, PROOF> {
    fn cast(x: &'a str) -> &'b str {
        PROOF.apply(x)
    }
}

const PROOF<'a: 'b, 'b>: OutlivesProof<'a, 'b> = OutlivesProof::mk();
type Opaque<'a, 'b> = impl Cast<'a, 'b>;
#[define_opaque(Opaque)]
fn mk<'a: 'b, 'b>() -> Option<Opaque<'a, 'b>> {
    None::<ConstOutlives<PROOF>>
}

fn transmute_static<'a>(x: &'a str) -> &'static str {
    Opaque::cast(x)
}

Ignore which unstable features would be required for this and the changes required for ConstOutlives to be a valid const parameter type. This would cause the above pattern to be unsound.

More generally: we currently support using values as proof of type system invariants. However, this relies on the assumption that if the invariants hold while computing the value, they will also hold when using it.

TAIT breaks this assumption. We only require the final returned value to be well-formed in case the TAIT is defined by a function which has stronger constraints than the TAIT itself. This means if the final value contains a const parameter of a type where the invariants are only checked by the constructor, TAIT allows using this value without proving them.

cc @rust-lang/types @RalfJung I've got 3 questions here:

• do we consider the prove_outlives module to be a safe abstraction (pretty sure yes)
• is there any principled reason why the above exploit via TAIT should error except by forbidding defining scopes with stronger requirements than the TAIT itself (i can't think of any)
• do we already have this issue with RPIT[IT] (i assume no, they don't allow weakening constraints)

I don't think keeping such types out of const generics is desirable, so IMO this issue is strongly on the TAIT side.

Start with the TAIT example in the issue, including the ConstOutlives const parameter and #[define_opaque(Opaque)], and determine how its stronger defining-scope bounds are checked. Compare the behavior with RPIT[IT] and const-generic invariant proofs; done means reaching a principled soundness decision and identifying the corresponding compiler handling or regression coverage.