2023-05-01 planning meeting

--- tags: weekly-meeting --- # 2023-05-01 planning meeting ## Updates ### RPITIT refactoring We currently have 5 or so failing test cases https://hackmd.io/h_1WrqUkTt6vHPXGFUyI0g (maybe there are more as we rebase). The main one is that we need to make the GAT well-formed. The copied lifetime generated for the GAT would need to have a where clause that makes the copy equal to the original lifetime. I didn't try this out but I think this [#103449](https://github.com/rust-lang/rust/pull/103449) also makes the problem go away as we don't duplicate the lifetime anymore. ### AFIT/RPITIT stabilization * [RPITIT RFC authored](https://github.com/rust-lang/rfcs/pull/3425) * [Associated return types RFC drafted](https://hackmd.io/@wg-async/H1qTVUMgn) * [Draft blog post regarding roadmap](https://github.com/rust-lang/blog.rust-lang.org/pull/1102) * Need to do a survey of bugs to categorize blockers etc ### TAITs nikomatsakis: I'd like to synchronize on this. I'd like to see this moving forward in some form. ### GATs We had a deep dive (https://rust-lang.zulipchat.com/#narrow/stream/326132-t-types.2Fmeetings/topic/2024-04-10). nikomatsakis: can we summarize some of the takeaways? I had one, which was that we ought to establish a "staleness" policy on RFCs and also target RFC text to the work we expect to do in "short term". ### a-mir-formality Work has stalled due to other priorities. The new style engine and port to Rust has been successful so far and contains a model of negative impls to demonstrate viability. Fuzzing support is code complete but untested. Next step is to schedule a design meeting for May with goal of reading the RFC and some summary of the overall approach. Question for group: I would like to move the repository from nikomatsakis to rust-lang. What is the criteria we want for this? Overall goals and next steps: * Codebase: * complete and test fuzzing support, use to fuzz negative impls implementation * develop testing engine to parse Rust tests and convert to a-mir-formality tests, eventually based on stable MIR * model MIR and borrow checker * RFC draft: * describe role and capabilities of a-mir-formality: * complete model of Rust type system + borrow checker; operational semantics for *safe Rust only* * required integration before new features are stabilized (or types team signoff if infeasible) * support for fuzz testing and ability to run against rust codebase ### Subtyping refactor ### Implied bounds ### Trait solver refactor * https://github.com/rust-lang/trait-system-refactor-initiative for tracking trait solver work and concerns * lcnr did work on unsoundness in new solver from alias bounds * lcnr is planning on doing implementation for handling opaques in new solver * compiler-errors has done some implementation work (polarity, fixing overflow. bugs, handling lazy norm in hir typeck) ### Trait object upcasting * Oh !@#!$! is this not stabilized yet? I totally forgot about this. What are next steps? --nikomatsakis * [RFC #3324](https://github.com/rust-lang/rfcs/pull/3324) was merged. ### Negative impls [RFC draft](https://hackmd.io/ZmpF0ITPRWKx6jYxgCWS7g) is nearing completion. a-mir-formality contains a draft implementation. The basic idea is that, for every trait `Bar`, you can either prove `T: Bar` based on positive impls or prove `T: !Bar` based on negative impls. By default (i.e., with no impls), neither is provable. Effectively, `Bar` and `!Bar` become (almost) independent traits. To prove disjointness, each positive `T: Bar` impl is required to prove that no negative impl `T: !Bar` exists. Negative impls must follow the orphan rules like any other impl. Coherence is then extended so that, given two impls (of any trait), if the two impls overlap but require `T: Bar`, and `T: !Bar` is provable, then the impls are considered disjoint (see RFC draft for more details). The full version of this check has been implementation in a-mir-formality and we are working to prepare a fuzzing setup to validate its soundness. However, we encountered a complication when implementing this in rustc, because the fully general implementation would require the ability to add `ParamEnv` entries that include inference variables. However, if we limit negative impls to "always applicable" impls, this sidesteps the problem. We are therefore pursuing an initial implementation that is more limited. We already wanted to limit negative impls for auto traits to "always applicable" cases, so this is a more consistent and simplified design, and still satisfies known use cases. **Example.** Consider this program ```rust struct Foo<T> { } trait Bar { } // (Negative) impl A impl<T> !Bar for Foo<T> where T: Display, {} // (Positive) impl B impl Bar for Foo<Vec> where U: Debug, {} ``` The way the a-mir-formality model works, for each positive impl, we have to prove that no negative impls exist that overlap. In other words, the (positive) impl B here has the job of proving * for all `U`... * assuming `U: Debug`... * it is not possible to prove `Foo<Vec>: !Bar` * (note the "double negative" -- proving `T: !Bar` means finding a negative impl for `Bar` that is satisfied) This is equivalent to proving: * not: * exists `U` where `U: Debug` such that `Foo<Vec>: !Bar` In other words, if we run a query `exists { if (U: Debug) { Foo<Vec>: !Bar } }` and we get back no results, that is good, but this will require having a param env that `?U: Debug`, which is not currently supported. **Alternative.** The alternative approach is to limit negative impls to "always applicable" impls which do not have any where-clauses beyond those required for well-formedness of the input type(s). This is a mild generalization of the existing "always applicable" check for `Drop` impls. Based on this rule, we can simply search to see if a negative impl exists that unifies with the types, and we don't have to consider the where-clauses, since we know they are satisfied so long as the input types are WF (and impls already have to prove their input types are WF). ### Polonius Series of goals have been established. We are looking for a skilled contributor to drive one of the required refactorings (contact lqd). The plan is to begin my reworking the formulation of current borrow checker to be closer to polonius's structure, without making it more expressive, and then to add in location sensitivity. Milestones: ```mermaid flowchart TD HR[" Factoring out higher-ranked errors from the main path (June) Looking for help! 🔎 "] IN[" Invert data structure and error reporting (June) lqd "] LI[" Location insensitive pass on nightly (end of June?) "] VF[" Verify full test suite passes with location insensitive Compilers in P2.0 mode accepts same programs as with NLL (Aug) "] P2["Location sensitive pass on nightly (Nov 15)"] IN --> LI HR --> LI LI --> VF VF --> P2 ``` ### chalk-ty Related work done by @nnethercote for perf reasons. Also led to [a bit of cleanup](https://github.com/rust-lang/rust/pull/110036). nikomatsakis: This would be useful for a-mir-formailty. ## Nominated issues Do we want to postpone a week to discuss in more detail? ### [A Pin unsoundness involving an impl DerefMut for Pin<&dyn LocalTrait>](https://github.com/rust-lang/rust/issues/85099) ### [PhantomData: fix documentation wrt interaction with dropck](https://github.com/rust-lang/rust/pull/103413) ### [Account for late-bound lifetimes in generics](https://github.com/rust-lang/rust/pull/103448) ### [Allow impl on projection](https://github.com/rust-lang/rust/pull/107263) ### [Erase late bound regions for dropped instances](https://github.com/rust-lang/rust/pull/107936) ### [Make late_bound_lifetime_arguments a hard error](https://github.com/rust-lang/rust/pull/108782) ### [Normalize obligations before matching them against a candidate](https://github.com/rust-lang/rust/pull/109115) ### [stop adding outlives requirements to dropck for [T; 0]](https://github.com/rust-lang/rust/issues/110288) ## Types FCPs 6 open: https://github.com/rust-lang/rust/issues?q=is%3Aopen+label%3AT-types+label%3Aproposed-final-comment-period ## Deep dive planning 12 open proposals: https://github.com/rust-lang/types-team/issues?q=is%3Aissue+is%3Aopen+label%3Adeep-dive-proposal *Note from Jack*: I'd really love to see a meeting on polonius and the direction there. I know @lqd has been interested, and it would be nice to have full-team buy-in and have a sense of direction here. *Response from Niko:* :+1: let's tag lqd, but also see the update for our general plans.