Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

NLL should identify and respect the lifetime annotations that the user wrote #47184

Closed
22 of 27 tasks
shepmaster opened this issue Jan 4, 2018 · 38 comments
Closed
22 of 27 tasks
Assignees
Labels
A-NLL Area: Non-lexical lifetimes (NLL) C-enhancement Category: An issue proposing an enhancement or a PR with one. E-hard Call for participation: Hard difficulty. Experience needed to fix: A lot. metabug Issues about issues themselves ("bugs about bugs") NLL-sound Working towards the "invalid code does not compile" goal T-compiler Relevant to the compiler team, which will review and decide on the PR/issue.

Comments

@shepmaster
Copy link
Member

shepmaster commented Jan 4, 2018

We have made some progress on this issue.

Here's a list of everywhere within function bodies where we annotate types, with check boxes on the ones that are currently getting checked by the MIR-borrowck / NLL.

(We should update this list as we think of more.)

Original bug report follows:


This code compiles with 1.24.0-nightly (2018-01-03 0a3761e):

#![feature(nll)]

fn main() {
    let vec: Vec<&'static String> = vec![&String::new()];

    // fn only_static(_: Vec<&'static String>) {}
    // only_static(vec);
}

This is confusing as the Vec almost certainly cannot contain a reference of a 'static lifetime. If you uncomment the call to only_static, you get the expected error that the String does not live long enough.

@nikomatsakis said:

NLL currently ignores hand-written type annotations, in particular, those that appear in local variables.

@shepmaster shepmaster added A-NLL Area: Non-lexical lifetimes (NLL) T-compiler Relevant to the compiler team, which will review and decide on the PR/issue. WG-compiler-nll labels Jan 4, 2018
@nikomatsakis nikomatsakis added this to the NLL Future Compat Warnings milestone Jan 4, 2018
@nikomatsakis nikomatsakis added the E-hard Call for participation: Hard difficulty. Experience needed to fix: A lot. label Jan 10, 2018
@nikomatsakis
Copy link
Contributor

I'm tagging this with E-hard because @pnkfelix and I established that as the "have to figure out how to do this" convention. That said, I don't know that it's that hard. My rough plan was something like this:

  • Extend HAIR/MIR with some sort of extra operations, that assert equality between types.
    • The region renumbering code would know that the types in such operations come from the user, and should not be renumbered.
    • Example: ASSERT_HAS_TY<T>(_1) would assert that the variable _1 has the given type T
    • We also have to handle foo::<T>() style annotations though
  • The HIR -> HAIR lowering would insert these operations when there are explicit Ty nodes
  • The HAIR -> MIR would produce ASSERT.
  • Similar strategy could be used for casts and things.

However, it might also be best to have some other way to indicate which types are from user -- for example, maybe instead of a Ty, MIR could embed a newtype that also carries a boolean whether it was inferred or explicit.

But I sort of prefer to have the "explicit annotations" come from somewhere else, seems easier overall to me.

@nikomatsakis nikomatsakis modified the milestones: NLL run-pass without ICEs, NLL soundness violations Jan 19, 2018
@nikomatsakis
Copy link
Contributor

cc @Aaron1011 -- btw, since you're on a roll lately, this would be a good one to get done at some point. It'll require a bit of experimentation though. =) Happy to discuss it sometime.

@davidtwco davidtwco self-assigned this Feb 8, 2018
@davidtwco
Copy link
Member

I'll tackle this one.

@nikomatsakis
Copy link
Contributor

nikomatsakis commented Feb 21, 2018

@davidtwco ok, so I think my prior directions were the right path still. It probably makes sense to tackle different kinds of annotations independently. Let's start with the most basic sort of annotation, that placed on local variables:

let x: T = ...

To handle this, I think we want to add a new form of MIR statement, a type assertion. That would be done by editing the StorageKind enum:

pub enum StatementKind<'tcx> {

I would call it something like UserAssertTy. It might look like:

/// Encodes a user's type assertion. These need to be preserved
/// intact so that NLL can respect them. For example:
///
///     let (a, b): (T, U) = y;
///
/// Here, we would insert a `UserAssertTy<(T, U)>(y)` instruction to check
/// that the type of `y` is the right thing.
UserAssertTy(Ty<'tcx>, Local),

We would then want to special-case these statements in the renumberer, so that it skips the embedded type within:

fn visit_statement(
&mut self,
block: BasicBlock,
statement: &mut Statement<'tcx>,
location: Location,
) {
if let StatementKind::EndRegion(_) = statement.kind {
statement.kind = StatementKind::Nop;
}
self.super_statement(block, statement, location);
}

But actually I realize there is a bit more complexity here than I initially considered. For example:

let x: &u32 = ...;

needs to be distinguished from

let x: &'static u32 = ...;

The current code doesn't have give you a good way to do that. But let's ignore that complication for a moment -- I have some ideas there for later =). For now, let's just test it with &'static u32 =)

Anyway, once we have this MIR, we also need to generate it. This could presumably mean instrumenting the HAIR, which is the intermediate IR that we use to transition from HIR to MIR.

I think we would want to extend the Let variant in HAIR to include the type annotation (if any):

Let {
/// scope for variables bound in this let; covers this and
/// remaining statements in block
remainder_scope: region::Scope,
/// scope for the initialization itself; might be used as
/// lifetime of temporaries
init_scope: region::Scope,
/// let <PAT> = ...
pattern: Pattern<'tcx>,
/// let pat = <INIT> ...
initializer: Option<ExprRef<'tcx>>,
/// the lint level for this let-statement
lint_level: LintLevel,
},

These are converted to MIR here:

StmtKind::Let {
remainder_scope,
init_scope,
pattern,
initializer,
lint_level
} => {

Hmm. As you can see from the comment, I initially thought we would apply the type to the initializer -- this would probably mean threading the user's type to expr_into_pattern here:

this.expr_into_pattern(block, pattern, init)

So it can add the appropriate assertions. But I guess that wouldn't cover a case like

let (a, b): (T, U);

Maybe we want to do things slightly differently. Mostly I wanted to avoid having the need to "match up" the patterns on the LHS (e.g., the (_, _) pattern) with the type on the RHS, which sounds annoying.

@nikomatsakis
Copy link
Contributor

Oh, I neglected to add that we will want to kill those new statements, presumably through a pass roughly like clean_end_regions. In fact, I think I would want to generalize that existing pass to something like cleanup_post_borrowck.

@davidtwco
Copy link
Member

@nikomatsakis I've submitted a PR with what I've got so far: #48482.

@davidtwco
Copy link
Member

davidtwco commented Mar 13, 2018

After chatting with @nikomatsakis on Gitter, here's a list of everywhere within function bodies where we annotate types:

(Update: @pnkfelix moved the list to the issue description to increase its visibility and make it easier to update it consistently.)

@nikomatsakis
Copy link
Contributor

@davidtwco so the problem in #48482 is (I think) precisely that sometimes user-given types may still include inference variables. The example I gave on gitter is a case of that:

fn foo() {
  let x = 22;
  let y: &u32 = &x;
  ...
}

Specifically, the lifetime in the type of y will be an inference variable. That will ultimately get inferred by the lexical region resolver to some specific lifetime, and that is what is recorded in the HIR -- and hence what gets propagated as part of the UserAssertTy. The problem is that this region is (a) going to be some scope, which makes no sense in NLL and (b) not coming from the user, but from inference! We only want to get the things the user gave us. The problem is that these types the user is giving are not complete types, we we can't just use a Ty<'tcx> to represent them.

However, what we can use is a Canonical<'_, Ty<'tcx>>. The canonicalization code was added recently in #48411. The high-level idea is covered in the rustc-guide, but in short canonicalization lets us take a type that includes inference variables and "extract them".

So, I think that the thing we want to be keeping in all of these cases (but let's just keep concentrating on the types in let x: T) is a Canonical<'_, Ty<'tcx>>. We can produce one of those readily enough by invoking canonicalize_query:

pub fn canonicalize_query<V>(&self, value: &V) -> (V::Canonicalized, CanonicalVarValues<'tcx>)
where
V: Canonicalize<'gcx, 'tcx>,

Though we may need to add a Canonicalize impl, like so:

pub type CanonicalTy<'gcx> = Canonical<'gcx, Ty<'tcx>>;

impl<'gcx: 'tcx, 'tcx> Canonicalize<'gcx, 'tcx> for Ty<'tcx> {
    type Canonicalized = CanonicalTy<'gcx>;

    fn intern(
        _gcx: TyCtxt<'_, 'gcx, 'gcx>,
        value: Canonical<'gcx, Self::Lifted>,
    ) -> Self::Canonicalized {
        value
    }
}

Anyway, the next challenge is that the "typeck tables" don't have a suitable table:

#[derive(RustcEncodable, RustcDecodable, Debug)]
pub struct TypeckTables<'tcx> {

We'll have to add a field like this one:

/// Stores the types for various nodes in the AST. Note that this table
/// is not guaranteed to be populated until after typeck. See
/// typeck::check::fn_ctxt for details.
node_types: ItemLocalMap<Ty<'tcx>>,

but it should be called user_provided_tys and have the type ItemLocalMap<CanonicalTy<'tcx>>.

Finally, we have to populate that field. We first convert the user-provided types here:

let o_ty = match local.ty {
Some(ref ty) => Some(self.fcx.to_ty(&ty)),
None => None
};

If we canonicalize the type right there, before we go and do anything else it, that should give us the value we want for the table. We can do the store into the table with local.id, sort of like here:

self.assign(local.span, local.id, o_ty);

@nikomatsakis nikomatsakis added the NLL-sound Working towards the "invalid code does not compile" goal label Mar 14, 2018
davidtwco added a commit to davidtwco/rust that referenced this issue Mar 22, 2018
alexcrichton added a commit to alexcrichton/rust that referenced this issue Mar 23, 2018
NLL should identify and respect the lifetime annotations that the user wrote

Part of rust-lang#47184.

r? @nikomatsakis
bors added a commit that referenced this issue Mar 24, 2018
NLL should identify and respect the lifetime annotations that the user wrote

Part of #47184.

r? @nikomatsakis
@davidtwco
Copy link
Member

With #48482 merged, there are some things that were not covered in that PR.

// FIXME(#47184): We currently only insert `UserAssertTy` statements for
// patterns that are bindings, this is as we do not want to deconstruct
// the type being assertion to match the pattern.
if let PatternKind::Binding { var, .. } = *pattern.kind {
if let Some(ty) = ty {
this.user_assert_ty(block, ty, var, span);
}
}

  • The current implementation does not handle patterns that are not bindings, such as let (a, b): (u32, u32) = (84, 29);.

//[nll]compile-flags: -Z disable-nll-user-type-assert

  • There is a temporary flag to disable this functionality for the case where a lifetime was defined but not used, this currently only occurs in the yield-subtype.rs test but that will also need resolved.

Further, this PR also only implements the check for type annotations in the let x: T = ...; case, see this comment for the remaining cases.

@jkordish jkordish added the C-enhancement Category: An issue proposing an enhancement or a PR with one. label Mar 29, 2018
@davidtwco davidtwco removed their assignment Apr 4, 2018
bors added a commit that referenced this issue Sep 11, 2018
…n-ascription, r=pnkfelix

support ascription for patterns in NLL

This implements the strategy outlined in [this comment](#47184 (comment)):

- We first extend the NLL subtyping code so it can handle inference variables and subtyping.
- Then we extend HAIR patterns with type ascription.
- Then we treat the type `T` in `let pat: T = ...` as an ascription.

Before landing, a few things:

- [x] Fix the WF rule bug (filed a FIXME #54105)
- [x] Fix an ICE I encountered locally around bound regions, or else file a follow-up
- [x] More tests probably =)

r? @pnkfelix
@nikomatsakis
Copy link
Contributor

Spun out to sub-issues.

@pnkfelix pnkfelix added metabug Issues about issues themselves ("bugs about bugs") C-tracking-issue Category: A tracking issue for an RFC or an unstable feature. and removed C-tracking-issue Category: A tracking issue for an RFC or an unstable feature. labels Oct 2, 2018
@pnkfelix pnkfelix self-assigned this Oct 2, 2018
@nikomatsakis
Copy link
Contributor

Demoting to Rust 2018 release. However, we should go ahead and convert all remaining items to sub-issues, I think, and close this

bors added a commit that referenced this issue Oct 27, 2018
…type-take-2, r=nikomatsakis

Handle bindings in substructure of patterns with type ascriptions

This attempts to follow the outline described by @nikomatsakis [here](#47184 (comment)). Its a bit more complicated than expected for two reasons:

 1. In general it handles sets of type ascriptions, because such ascriptions can be nested within patterns
 2.  It has a separate types in the HAIR, `PatternTypeProjections` and `PatternTypeProjection`, which are analogues to the corresponding types in the MIR.

The main reason I added the new HAIR types was because I am worried that the current implementation is inefficent, and asymptotically so: It makes copies of vectors as it descends the patterns, even when those accumulated vectors are never used.

Longer term, I would like to used a linked tree structure for the `PatternTypeProjections` and `PatternTypeProjection`, and save the construction of standalone vectors for the MIR types. I didn't want to block landing this on that hypoethetical revision; but I figured I could at least make the future change easier by differentiating between the two types now.

Oh, one more thing: This doesn't attempt to handle `ref x` (in terms of ensuring that any necessary types are ascribed to `x` in that scenario as well). We should open an issue to investigate supporting that as well. But I didn't want to block this PR on that future work.

Fix #54570
@nikomatsakis
Copy link
Contributor

I'm going to close this bug now -- we're down to just a handful of "subbullets", each of which has their own tracking issues.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
A-NLL Area: Non-lexical lifetimes (NLL) C-enhancement Category: An issue proposing an enhancement or a PR with one. E-hard Call for participation: Hard difficulty. Experience needed to fix: A lot. metabug Issues about issues themselves ("bugs about bugs") NLL-sound Working towards the "invalid code does not compile" goal T-compiler Relevant to the compiler team, which will review and decide on the PR/issue.
Projects
None yet
Development

No branches or pull requests

9 participants