[sanxiyn]

Yes, but the rule is still complete. What is going on is "place" is currently defined to be local x, or field x.f, or index x[i], but all x[i] are merged to x[*]. Rust's so-called NLL changed definition of "live". The point is, the rule is simple, formal, and complete. It is neither an ad hoc rule nor a best effort prover.

[ajross]

> What is going on is "place" is currently defined to be

Not to belabor this growing thread, but here's the disconnect. I complained the rules were ad hoc and complicated, you replied that they were simple, and when challenged on an edge case your treatment is to add another clause to re-define a term you used in isolation earlier.

That's what "ad hoc and complicated" means.

[sanxiyn]

"place" and "live" have their respective intuitive definitions. To clarify, "place" is a set of bytes in the memory. "live" means it is used again. But both are runtime concepts, so Rust compiler needs to compute static approximation of these runtime concepts. This static approximation is what is complex and changing. But the principle is simple.

Actually, my elaboration of "place", local/field/index, is nearly complete. The only thing missing is upvar, which is local captured in closure. Pre-NLL "live" is simple: expression is live from the definition to the end of the containing statement, and declaration is live from the definition to the end of the containing block. Post-NLL "live" is connected region of control flow graph from the definition to potentially multiple last uses. Really, that is the whole story.

There are two changes currently in development. One changes definition of "place" to include field captured in closure, in addition to local captured in closure. The other is more drastic, changing definition of "live": a loan is live where the loan is origin of a variable and the variable is live. This is great, because current approximation is equivalent to union of all origins.