[RFC] Clarify (and improve) rules for projections and well-formedness

[nikomatsakis]

RFC has been accepted and merged.

Current text: https://github.com/rust-lang/rfcs/blob/master/text/1214-projections-lifetimes-and-wf.md
Tracking issue: rust-lang/rust#27579

---

Type system changes to address the outlives relation with respect to projections, and to better enforce that all types are well-formed (meaning that they respect their declared bounds). The current implementation can be both unsound (rust-lang/rust#24622), inconvenient (rust-lang/rust#23442), and surprising (rust-lang/rust#21748, rust-lang/rust#25692). The changes are as follows:

• Simplify the outlives relation to be syntactically based.
• Specify improved rules for the outlives relation and projections.
• Specify more specifically where WF bounds are enforced, covering several cases missing from the implementation.

The proposed changes here have been tested and found to cause only a modest number of regressions (about two dozen root regressions were previously found on crates.io; however, that run did not yet include all the provisions from this RFC; updated numbers coming soon). In order to minimize the impact on users, the plan is to first introduce the changes in two stages:

1. Initially, warnings will be issued for cases that violate the rules specified in this RFC. These warnings are not lints and cannot be silenced except by correcting the code such that it type-checks under the new rules.
2. After one release cycle, those warnings will become errors.

Note that although the changes do cause regressions, they also cause some code (like that in rust-lang/rust#23442) which currently gets errors to compile successfully.

cc @rust-lang/lang

Rendered

[nikomatsakis]

cc @arielb1

[Ryman]

@nikomatsakis I think the issue referenced for 'unsound' in your description should be rust-lang/rust#24622 which is mentioned in the RFC (also labelled wrong).

[nikomatsakis]

@Ryman thanks.

[Diggsey]

Should this be ∀i. R ⊢ Pi: 'a?

[Gankro]

It seems like T: 'a is redundant, since &'x T is WF only if T: 'x, no?

So T: 'x and 'x: 'a -> T: 'a by transitivity?

Maybe I'm missing a corner case.

[nikomatsakis]

@Gankro

Sorry, I'm not sure if I ever answered this.

It seems like T: 'a is redundant, since &'x T is WF only if T: 'x, no?

This seems true, if harmless.

[Gankro]

Similar as above

[arielb1]

Shouldn't this be ∀i R, i: 'a ⊢ Oi: 'a (otherwise for<'α> Fn(&'α ()) : 'a would be false).

[nikomatsakis]

@arielb1

Shouldn't this be ∀i R, i: 'a ⊢ Oi: 'a (otherwise for<'α> Fn(&'α ()) : 'a would be false).

No, because the binder is within the Oi.

[Gankro]

maybe add a "while" after the comma. Took me a second to parse this correctly.

[Gankro]

Note for those of us without a very strong type theory background:

⊢ == "proves"

So this is just saying that any set of bounds proves that a scalar outlives 'a, for any given 'a (Plain Old Data has no external lifetime constraints, so it lives for any lifetime).

(I think)

[arielb1]

Not exactly "proves". this is a sequent-style deduction rule, read "(implicitly) for every environment R, scalar s and lifetime 'a, s outlives 'a given R"

[Gankro]

Env being "the union of all in scope where clauses and implied bounds"? Unclear.

Also unclear what the significance of 'x not in R is? Are saying that R can only use facts from the environment to prove bounds for otherwise unbound lifetimes?

[Gankro]

Are these supposed to be the same 'a and 'x from the proceeding paragraph?

[Gankro]

It's seems interesting that trait definitions are not considered part of the environment when talking about a type that implements that trait.

[Gankro]

An example would be great. Is it simply any time you're working with a generic I: Iterator?

[nikomatsakis]

@Gankro

An example would be great. Is it simply any time you're working with a generic I: Iterator?

I added an example, but yes that's roughly right (and other analogous cases, of course).

[Gankro]

More generally:

Something can only fail to outlive 'x if its type refers to (non-'static) lifetime that doesn't outlive 'x, and the only lifetimes it can possibly refer to have to be declared in the impl declaration. So it's sufficient (though perhaps not always necessary?) to make sure everything referred to in the impl declaration outlives 'x.

[nikomatsakis]

@Gankro

Something can only fail to outlive 'x if its type refers to (non-'static) lifetime that doesn't outlive 'x, and the only lifetimes it can possibly refer to have to be declared in the impl declaration. So it's sufficient (though perhaps not always necessary?) to make sure everything referred to in the impl declaration outlives 'x.

Yes, with a bit of subtlety -- we have to be sure that it not only appears in the impl declaration, but does not appear as part of a projection (as specified below). But this rule already exists.

In other words:

impl<'a> Trait for <i32 as SomeTrait<'a>>::Bar { ... }

wouldn't be good enough for 'a because maybe <i32 as SomeTrait<'a>>::Bar normalized to u32 (and 'a doesn't appear in u32).

[Gankro]

Is that a problem though? We're trying to reason that it outlives 'a, and u32 is 'static.

[Gankro]

yesss nested asides

[Gankro]

X is a type parameter, I gather?

[Gankro]

Should this be P0: Trait<P1..Pn>?

[nikomatsakis]

@Gankro

Should this be P0: Trait<P1..Pn>?

Yeah, I guess. I alternate between those notations somewhat interchangeably. :)

[arielb1]

I think the [[T]] issue is a straight bug in rustc and shouldn't result in just a warning.

[arielb1]

There should also be a WfTuple - in fact in the form you use there should be a Wf rule for each type constructor.

[nikomatsakis]

@arielb1

There should also be a WfTuple - in fact in the form you use there should be a Wf rule for each type constructor.

Added.

[arielb1]

missing WF - should be

∀i. R, r.. ⊢ Ti WF
--------------------------------------------------
R ⊢ for<r..> fn(T1..Tn) -> T0 WF

[arielb1]

Is there a case where this is relevant? What's an object type vs. object fragment?

[nikomatsakis]

@arielb1

I think the [[T]] issue is a straight bug in rustc and shouldn't result in just a warning.

Perhaps, but the issue is really not whether it's a bug or not, the question is about whether code is affected by the change. That said, I haven't observed any.

[arielb1]

@nikomatsakis

[[T]] basically causes an ICE every time it is used, so it is relatively hard to abuse.

[arielb1]

Could you also clarify which of Box<Foo<'a>+'static>, Box<Foo<'static>+'a> and Box<Foo<'a>+'b> are well-formed (assuming 'a and `'b' are unrelated free regions)? AFAICT the rules say that only the second of these is valid, but an example would always be helpful.

[Zalastra]

Ran into this error using an associated const on a trait. On IRC it was suggested that this is likely a compiler bug.

pub trait IterableEnum<T> {
    const ENUM_VARIANTS: &'static [T];
}

[arielb1]

@Zalastra

Just add T: 'static. Not a bug.

[bluss]

It outputs two warnings (playpen)

• warning: the trait core::marker::Sized is not implemented for the type T
• warning: the parameter type T may not live long enough

The first one must be a bug.

[eddyb]

@bluss it's odd because it seems like it doesn't take actual bounds into account - see fixed version (the Sized bound is unnecessary, but it's there to show the issue).

[nikomatsakis]

I agree that the T: Sized message is a bug. Did anyone file an issue?

On Tue, Sep 22, 2015 at 8:14 AM, Eduard-Mihai Burtescu <
notifications@github.com> wrote:

@bluss https://github.com/bluss it's odd because it seems like it
doesn't take actual bounds into account - see fixed version
https://play.rust-lang.org/?gist=343add7244bd4b210961&version=nightly&run=1
(the Sized bound is unnecessary, but it's there to show the issue).

—
Reply to this email directly or view it on GitHub
#1214 (comment).