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

evaluation cache, freshen each predicate by itself #102713

Closed
wants to merge 1 commit into from

Conversation

lcnr
Copy link
Contributor

@lcnr lcnr commented Oct 5, 2022

I think this change is correct. Here's my understanding of this:

This previously wasn't done was so that we don't consider Foo<?0>: Trait requiring Foo<?0>: Trait (which is trivially a cycle), the same as Foo<?0>: Trait requiring Foo<?1>: Trait, which is an infinite chain instead.

For inductive obligations, cycles and infinite chains should both result in ambiguity, so for these this doesn't matter.

For coinductive obligations, cycles result in success and I believe that infinitely diverging chains should also be a success. That's my understanding given my limited experience with coq and the general intuition of "coinduction means stuff is true unless proven otherwise, induction means stuff is wrong unless proven otherwise".

r? @nikomatsakis cc @rust-lang/types

@lcnr

This comment was marked as outdated.

@@ -2253,7 +2245,8 @@ impl<'cx, 'tcx> SelectionContext<'cx, 'tcx> {
previous_stack: TraitObligationStackList<'o, 'tcx>,
obligation: &'o TraitObligation<'tcx>,
) -> TraitObligationStack<'o, 'tcx> {
let fresh_trait_pred = obligation.predicate.fold_with(&mut self.freshener);
let fresh_trait_pred =
obligation.predicate.fold_with(&mut self.infcx.freshener_keep_static());
Copy link
Contributor Author

@lcnr lcnr Oct 5, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

keeping 'static here is wrong. I am changing this separately in #102472 which is blocked on #102635

@nikomatsakis nikomatsakis self-assigned this Oct 5, 2022
@lcnr

This comment was marked as outdated.

@lcnr lcnr closed this Oct 5, 2022
@lcnr lcnr reopened this Oct 5, 2022
@lcnr
Copy link
Contributor Author

lcnr commented Oct 5, 2022

@bors try @rust-timer queue

@lcnr lcnr force-pushed the freshen-no-unique-vars branch from 14584fb to da92870 Compare October 5, 2022 15:54
@rust-highfive rust-highfive added the S-waiting-on-review Status: Awaiting review from the assignee but also interested parties. label Oct 5, 2022
@rustbot rustbot added the T-compiler Relevant to the compiler team, which will review and decide on the PR/issue. label Oct 5, 2022
@rust-timer
Copy link
Collaborator

Awaiting bors try build completion.

@rustbot label: +S-waiting-on-perf

@bors
Copy link
Contributor

bors commented Oct 5, 2022

⌛ Trying commit da928700181422639a4c06f0ac832f3a87e65180 with merge 79e77056cd5cd1e6cd8cb883026e53a7f1ff0659...

@rust-timer
Copy link
Collaborator

Awaiting bors try build completion.

@rustbot label: +S-waiting-on-perf

1 similar comment
@rust-timer
Copy link
Collaborator

Awaiting bors try build completion.

@rustbot label: +S-waiting-on-perf

@bors
Copy link
Contributor

bors commented Oct 5, 2022

⌛ Trying commit da928700181422639a4c06f0ac832f3a87e65180 with merge f30cafb00d844ad0086efc9765084f4e994286f5...

@rust-timer
Copy link
Collaborator

Awaiting bors try build completion.

@rustbot label: +S-waiting-on-perf

1 similar comment
@rust-timer
Copy link
Collaborator

Awaiting bors try build completion.

@rustbot label: +S-waiting-on-perf

@bors
Copy link
Contributor

bors commented Oct 5, 2022

⌛ Trying commit da928700181422639a4c06f0ac832f3a87e65180 with merge 0cb6fd9f0ff8333a6cdc3b11e06197e42a2c8da5...

@rustbot rustbot added the S-waiting-on-perf Status: Waiting on a perf run to be completed. label Oct 5, 2022
@bors
Copy link
Contributor

bors commented Oct 5, 2022

☀️ Try build successful - checks-actions
Build commit: 0cb6fd9f0ff8333a6cdc3b11e06197e42a2c8da5 (0cb6fd9f0ff8333a6cdc3b11e06197e42a2c8da5)

@rust-timer
Copy link
Collaborator

Queued 0cb6fd9f0ff8333a6cdc3b11e06197e42a2c8da5 with parent 8c71b67, future comparison URL.

@rust-timer
Copy link
Collaborator

Finished benchmarking commit (0cb6fd9f0ff8333a6cdc3b11e06197e42a2c8da5): comparison URL.

Overall result: ❌✅ regressions and improvements - ACTION NEEDED

Benchmarking this pull request likely means that it is perf-sensitive, so we're automatically marking it as not fit for rolling up. While you can manually mark this PR as fit for rollup, we strongly recommend not doing so since this PR may lead to changes in compiler perf.

Next Steps: If you can justify the regressions found in this try perf run, please indicate this with @rustbot label: +perf-regression-triaged along with sufficient written justification. If you cannot justify the regressions please fix the regressions and do another perf run. If the next run shows neutral or positive results, the label will be automatically removed.

@bors rollup=never
@rustbot label: +S-waiting-on-review -S-waiting-on-perf +perf-regression

Instruction count

This is a highly reliable metric that was used to determine the overall result at the top of this comment.

mean1 range count2
Regressions ❌
(primary)
0.8% [0.8%, 0.8%] 1
Regressions ❌
(secondary)
1.1% [1.1%, 1.1%] 1
Improvements ✅
(primary)
-0.2% [-0.2%, -0.2%] 1
Improvements ✅
(secondary)
-0.3% [-0.4%, -0.2%] 9
All ❌✅ (primary) 0.3% [-0.2%, 0.8%] 2

Max RSS (memory usage)

This benchmark run did not return any relevant results for this metric.

Cycles

This benchmark run did not return any relevant results for this metric.

Footnotes

  1. the arithmetic mean of the percent change

  2. number of relevant changes

@rustbot rustbot added perf-regression Performance regression. and removed S-waiting-on-perf Status: Waiting on a perf run to be completed. labels Oct 6, 2022
@lcnr
Copy link
Contributor Author

lcnr commented Oct 6, 2022

@bors try

@nikomatsakis
Copy link
Contributor

r=me but I think we should do a crater run

@bors
Copy link
Contributor

bors commented Oct 6, 2022

⌛ Trying commit da928700181422639a4c06f0ac832f3a87e65180 with merge 7f168b18704203996d3698515c88a036a9300946...

@bors
Copy link
Contributor

bors commented Oct 6, 2022

☀️ Try build successful - checks-actions
Build commit: 7f168b18704203996d3698515c88a036a9300946 (7f168b18704203996d3698515c88a036a9300946)

@lcnr
Copy link
Contributor Author

lcnr commented Oct 7, 2022

@craterbot check

@craterbot
Copy link
Collaborator

👌 Experiment pr-102713 created and queued.
🤖 Automatically detected try build 7f168b18704203996d3698515c88a036a9300946
🔍 You can check out the queue and this experiment's details.

ℹ️ Crater is a tool to run experiments across parts of the Rust ecosystem. Learn more

@craterbot craterbot added S-waiting-on-crater Status: Waiting on a crater run to be completed. and removed S-waiting-on-review Status: Awaiting review from the assignee but also interested parties. labels Oct 7, 2022
@craterbot
Copy link
Collaborator

🚧 Experiment pr-102713 is now running

ℹ️ Crater is a tool to run experiments across parts of the Rust ecosystem. Learn more

@craterbot
Copy link
Collaborator

🎉 Experiment pr-102713 is completed!
📊 64 regressed and 6 fixed (244993 total)
📰 Open the full report.

⚠️ If you notice any spurious failure please add them to the blacklist!
ℹ️ Crater is a tool to run experiments across parts of the Rust ecosystem. Learn more

@craterbot craterbot added S-waiting-on-review Status: Awaiting review from the assignee but also interested parties. and removed S-waiting-on-crater Status: Waiting on a crater run to be completed. labels Oct 9, 2022
@lcnr lcnr force-pushed the freshen-no-unique-vars branch from da92870 to b28b235 Compare October 17, 2022 09:51
@lcnr
Copy link
Contributor Author

lcnr commented Oct 17, 2022

this changes some recursive paths from EvaluatedToUnknown to EvaluatedToRecur with EvaluatedToRecur getting treated differently, breaking existing crates.

Comparing the trait ref using structural eq, this previously failed as we had different fresh vars, now it succeeds:

if let Some(cycle_depth) = stack
.iter()
.skip(1) // Skip top-most frame.
.find(|prev| {
stack.obligation.param_env == prev.obligation.param_env
&& stack.fresh_trait_pred == prev.fresh_trait_pred
})
.map(|stack| stack.depth)

This succeeds even for different fresh vars:

if unbound_input_types
&& stack.iter().skip(1).any(|prev| {
stack.obligation.param_env == prev.obligation.param_env
&& self.match_fresh_trait_refs(
stack.fresh_trait_pred,
prev.fresh_trait_pred,
prev.obligation.param_env,
)
})
{
debug!("evaluate_stack --> unbound argument, recursive --> giving up",);
return Ok(EvaluatedToUnknown);
}

@jyn514 previously looked into changing EvaluatedToRecur. Reached out to him to figure out how to best make progress here.

@lcnr lcnr added S-blocked Status: Blocked on something else such as an RFC or other implementation work. and removed S-waiting-on-review Status: Awaiting review from the assignee but also interested parties. labels Oct 17, 2022
@jyn514
Copy link
Member

jyn514 commented Oct 19, 2022

wip code here: https://github.com/jyn514/rust/pull/new/normalize-docs
but it doesn't work

@bors
Copy link
Contributor

bors commented Nov 19, 2022

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

@lcnr
Copy link
Contributor Author

lcnr commented Dec 4, 2022

when freshening each obligation by itself we have to correctly deal with inference constraints from the cyclic call. Otherwise we get the following issue:

trait Foo {} // assume `Foo` is coinductive here
struct Wrapper<T>(T);

impl<T> Foo for Wrapper<Wrapper<T>>
where
    Wrapper<T>: Foo
{} 

query: does Wrapper<?0>: Foo hold?

  • candidate: impl<T> Foo for Wrapper<Wrapper<T>> -> ?0 -> Wrapper<?1>
    • nested: Wrapper<?1>: Foo COINDUCTIVE CYCLE OK
  • query returns OK: ?0 = Wrapper<?1>

To deal with this evaluate has to return inference results which will only be added in the implementation of the trait system refactor initiative.

@lcnr lcnr closed this Dec 4, 2022
compiler-errors added a commit to compiler-errors/rust that referenced this pull request Jan 9, 2023
update test for inductive canonical cycles

the previous test always resulted in a cycle 😅 cc rust-lang/chalk#787.

I checked with rust-lang#102713 and this is the only test which fails with that PR.

r? `@jackh726`
JohnTitor pushed a commit to JohnTitor/rust that referenced this pull request Jan 9, 2023
update test for inductive canonical cycles

the previous test always resulted in a cycle 😅 cc rust-lang/chalk#787.

I checked with rust-lang#102713 and this is the only test which fails with that PR.

r? ``@jackh726``
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
perf-regression Performance regression. S-blocked Status: Blocked on something else such as an RFC or other implementation work. T-compiler Relevant to the compiler team, which will review and decide on the PR/issue.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

8 participants