Expose Obligations created during type inference. #119613

gavinleroy · 2024-01-05T10:49:40Z

This PR is a first pass at exposing the trait obligations generated and solved for during the type-check progress. Exposing these obligations allows for rustc plugins to use the public interface for proof trees (provided by the next gen trait solver).

The changes proposed track all obligations during the type-check process, this is desirable to not only look at the trees of failed obligations, but also those of successfully proved obligations. This feature is placed behind an unstable compiler option track-trait-obligations which should be used together with the next-solver option. I should note that the main interface is the function inspect_typeck made public in rustc_hir_typeck/src/lib.rs which allows the caller to provide a callback granting access to the FnCtxt.

r? @lcnr

rustbot · 2024-01-05T10:49:50Z

Some changes occurred to the core trait solver

cc @rust-lang/initiative-trait-system-refactor

lcnr · 2024-01-09T14:39:14Z

compiler/rustc_infer/src/infer/mod.rs

@@ -334,6 +334,8 @@ pub struct InferCtxt<'tcx> {
    pub intercrate: bool,

    next_trait_solver: bool,
+
+    pub fulfilled_obligations: Lrc<Lock<Vec<traits::FulfilledObligation<'tcx>>>>,


Please change this to only be a field of the fulfillment context (and a method on the Engine trait to get them. Do not add it to the inference context. That will miss some obligations checked while probing, but given that we also sometimes prove by just using evaluate, this shouldn't change

However, having it on the infcx stores obligations from probes, which can leak inference variables, which is bad:tm: and potentially results in ICE

Leaking inference variables is obviously not good. However, there is a motivation for catching obligations from within a probe. Take the following code:

#![feature(negative_impls)] use rayon::prelude::*; #[derive(Debug)] struct NotSend; impl !Send for NotSend {} impl !Sync for NotSend {} fn parallel_do(vs: Vec<NotSend>) { // Obligation `Vec<NotSend>: IntoParallelIterator` // happens inside a probe. (At least IIUC) vs.into_par_iter(); } fn main() {}

If my understanding of the trait solver is correct, when type-checking the expression vs.into_par_iter() the query Vec<NotSend>: IntoParallelIterator would happen inside of a probe. For the context of the "trait debugger" we're building, catching this obligation is important so that we can explain the call ambiguity to a user.

Is there a way to get this obligation without storing the obligations on the InferCtxt?

bors · 2024-01-14T09:33:28Z

☔ The latest upstream changes (presumably #119934) made this pull request unmergeable. Please resolve the merge conflicts.

gavinleroy · 2024-01-16T11:50:40Z

Following a suggestion on Zulip, the inference context is cloned and stored alongside the captured obligations. However, I'm not sure I'm satisfied with this approach.

The InferCtxt must now implement Clone, which I see as undesirable, as nowhere else in the compiler should you clone the context.
The obligations still need to be stored in the InferCtxt as opposed to the TyCtxt. My understanding is because rustc_middle cannot depend on rustc_infer.

Here's an alternative proposal. Instead of using the callback on inspect_typeck to inspect the FnCtxt, we could give the the callback to the InferCtxt. When obligation tracking is enabled this callback is invoked with the InferCtxt on all root obligations in the FulfillmentCtxt. Thus making the callback of type impl Fn(infcx: &InferCtxt<'tcx>, obligation: PredicateObligation<'tcx>). No cloning necessary, and external tools should be able to get all information necessary ™️. I can of course test this claim with our tool locally.

@lcnr do you have thoughts on this approach vs what was discussed the other day?

lcnr · 2024-01-16T12:05:15Z

The InferCtxt must now implement Clone, which I see as undesirable, as nowhere else in the compiler should you clone the context.

https://doc.rust-lang.org/nightly/nightly-rustc/rustc_infer/infer/struct.InferCtxt.html#method.fork exists and should be used instead

The obligations still need to be stored in the InferCtxt as opposed to the TyCtxt. My understanding is because rustc_middle cannot depend on rustc_infer.

the type could be erased on the TyCtxt, however, I think your suggested alternative is to never store the goals anywhere but eagerly call the supplied closure? This seems preferable to me

lcnr · 2024-01-18T08:11:33Z

compiler/rustc_trait_selection/src/solve/fulfill.rs

+            if let Some(inspector) = infcx.obligation_inspector.get() {
+                let result = match result {
+                    Ok((_, c, _)) => Ok(*c),
+                    Err(NoSolution) => Err(NoSolution),
+                };
+                (inspector)(infcx, &obligation, result);
+            }


isn't the Some(inspector) check enough 🤔 why did you add a separate flag here?

In it's current state, it's technically possible to have a Some when the track-trait-obligation flag isn't set. I'll change it to check the flag before setting the option.

my quesiton would be: why have the track-trait-obligation flag in the first place? It seems like always using an inspector, if one is provided, should be good enough 🤔 are you worried about accidentally relying on the behavior of an inspector in ordinary compilations?

Ah, I see. The motivation to have the unstable flag was to make the changes seem less intrusive :) especially because using the inspector relies on using the next trait solver, which is behind a flag. But functionally there's no reason to have the flag.

I removed the unstable flag and added a comment to inspect_typeck which states that it only has an effect when using the next trait solver. That should be clear enough for its use. I'm not particularly worried that someone will rely on its behavior during normal compilation.

lcnr

r=me after nits

lcnr · 2024-01-19T13:04:17Z

compiler/rustc_trait_selection/src/solve/fulfill.rs

-            .collect()
+            .collect();
+
+        errors


spurious change, please revert

lcnr · 2024-01-19T13:05:20Z

compiler/rustc_hir_typeck/src/lib.rs

 }

-#[instrument(level = "debug", skip(tcx, fallback), ret)]
+/// Same as `typeck` but `inspect` is invoked on evaluation of each root obligation.
+/// Inspecting obligations only works with the new trait solver.


please also state that:

only used by external tools

not cached as it's not a query

…tc_infer using callback. Pass each obligation to an fn callback with its respective inference context. This avoids needing to keep around copies of obligations or inference contexts. Specify usability of inspect_typeck in comment.

gavinleroy · 2024-01-19T14:47:52Z

@bors r=lcnr

bors · 2024-01-19T14:47:54Z

@gavinleroy: 🔑 Insufficient privileges: Not in reviewers

lcnr · 2024-01-19T15:20:43Z

@bors r+ rollup

bors · 2024-01-19T15:20:45Z

📌 Commit 130b7e7 has been approved by lcnr

It is now in the queue for this repository.

…iaskrgr Rollup of 10 pull requests Successful merges: - rust-lang#103730 (Added NonZeroXxx::from_mut(_unchecked)?) - rust-lang#113142 (optimize EscapeAscii's Display and CStr's Debug) - rust-lang#118799 (Stabilize single-field offset_of) - rust-lang#119613 (Expose Obligations created during type inference.) - rust-lang#119752 (Avoid ICEs in trait names without `dyn`) - rust-lang#120132 (Teach tidy about line/col information for malformed features) - rust-lang#120135 (SMIR: Make the remaining "private" fields actually private) - rust-lang#120148 (`single_use_lifetimes`: Don't suggest deleting lifetimes with bounds) - rust-lang#120150 (Stabilize `round_ties_even`) - rust-lang#120155 (Don't use `ReErased` to detect type test promotion failed) r? `@ghost` `@rustbot` modify labels: rollup

Rollup merge of rust-lang#119613 - gavinleroy:expose-obligations, r=lcnr Expose Obligations created during type inference. This PR is a first pass at exposing the trait obligations generated and solved for during the type-check progress. Exposing these obligations allows for rustc plugins to use the public interface for proof trees (provided by the next gen trait solver). The changes proposed track *all* obligations during the type-check process, this is desirable to not only look at the trees of failed obligations, but also those of successfully proved obligations. This feature is placed behind an unstable compiler option `track-trait-obligations` which should be used together with the `next-solver` option. I should note that the main interface is the function `inspect_typeck` made public in `rustc_hir_typeck/src/lib.rs` which allows the caller to provide a callback granting access to the `FnCtxt`. r? `@lcnr`

rustbot assigned lcnr Jan 5, 2024

rustbot added S-waiting-on-review Status: Awaiting review from the assignee but also interested parties. T-compiler Relevant to the compiler team, which will review and decide on the PR/issue. WG-trait-system-refactor The Rustc Trait System Refactor Initiative (-Znext-solver) labels Jan 5, 2024

This comment has been minimized.

Sign in to view

lcnr reviewed Jan 9, 2024

View reviewed changes

gavinleroy force-pushed the expose-obligations branch from 998644f to f9046e6 Compare January 17, 2024 23:42

lcnr reviewed Jan 18, 2024

View reviewed changes

gavinleroy force-pushed the expose-obligations branch from f9046e6 to 6352283 Compare January 18, 2024 10:25

lcnr reviewed Jan 19, 2024

View reviewed changes

gavinleroy force-pushed the expose-obligations branch from 2205c19 to e007f5a Compare January 19, 2024 14:34

gavinleroy force-pushed the expose-obligations branch from e007f5a to 130b7e7 Compare January 19, 2024 14:41

bors added S-waiting-on-bors Status: Waiting on bors to run and complete tests. Bors will change the label on completion. and removed S-waiting-on-review Status: Awaiting review from the assignee but also interested parties. labels Jan 19, 2024

matthiaskrgr mentioned this pull request Jan 20, 2024

Rollup of 10 pull requests #120157

Merged

bors merged commit 2de5ca2 into rust-lang:master Jan 20, 2024
11 checks passed

rustbot added this to the 1.77.0 milestone Jan 20, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Expose Obligations created during type inference. #119613

Expose Obligations created during type inference. #119613

gavinleroy commented Jan 5, 2024 •

edited

Loading

rustbot commented Jan 5, 2024

This comment has been minimized.

lcnr Jan 9, 2024

gavinleroy Jan 10, 2024 •

edited

Loading

bors commented Jan 14, 2024

gavinleroy commented Jan 16, 2024

lcnr commented Jan 16, 2024

lcnr Jan 18, 2024

gavinleroy Jan 18, 2024

lcnr Jan 18, 2024

gavinleroy Jan 18, 2024

gavinleroy Jan 19, 2024

lcnr left a comment

lcnr Jan 19, 2024

lcnr Jan 19, 2024

gavinleroy commented Jan 19, 2024

bors commented Jan 19, 2024

lcnr commented Jan 19, 2024

bors commented Jan 19, 2024

Expose Obligations created during type inference. #119613

Expose Obligations created during type inference. #119613

Conversation

gavinleroy commented Jan 5, 2024 • edited Loading

rustbot commented Jan 5, 2024

This comment has been minimized.

Choose a reason for hiding this comment

gavinleroy Jan 10, 2024 • edited Loading

Choose a reason for hiding this comment

bors commented Jan 14, 2024

gavinleroy commented Jan 16, 2024

lcnr commented Jan 16, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

lcnr left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

gavinleroy commented Jan 19, 2024

bors commented Jan 19, 2024

lcnr commented Jan 19, 2024

bors commented Jan 19, 2024

gavinleroy commented Jan 5, 2024 •

edited

Loading

gavinleroy Jan 10, 2024 •

edited

Loading