Make well-formedness predicates no longer coinductive

[compiler-errors]

This PR makes well-formedness no longer coinductive. It was made coinductive in #98542, but AFAICT this was only to fix UI tests since we stopped lowering where Ty: to an empty-region outlives predicate but to a WF predicate instead.

Arguably it should lower to something completely different, something like a "type mentioned no-op predicate", but well-formedness serves this purpose fine today, and since no code (according to crater) relies on this coinductive behavior, we'd like to avoid having to emulate it in the new solver.

Fixes #123456 (I didn't want to add a test since it seems low-value to have a ICE test for a fuzzer minimization that is basically garbage code.)

Fixes rust-lang/trait-system-refactor-initiative#209 (not sure if this behavior is emulatable w/o coinductive WF?)

Fixes rust-lang/trait-system-refactor-initiative#169

r? lcnr

[compiler-errors]

@bors try @rust-timer queue

[bors]

⌛ Trying commit 3f4d6c9 with merge 099e089...

[bors]

☀️ Try build successful - checks-actions
Build commit: 099e089 (099e089ab723e6ee96175f3496051098c60a4cd4)

[compiler-errors]

@craterbot check

[craterbot]

👌 Experiment pr-140208 created and queued.
🤖 Automatically detected try build 099e089
🔍 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

[rust-timer]

Finished benchmarking commit (099e089): comparison URL.

Overall result: no relevant changes - no 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.

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

Instruction count

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

Max RSS (memory usage)

Results (primary -0.3%)

This is a less reliable metric that may be of interest but was not used to determine the overall result at the top of this comment.

	mean	range	count
Regressions ❌ (primary)	0.5%	[0.5%, 0.5%]	1
Regressions ❌ (secondary)	-	-	0
Improvements ✅ (primary)	-0.7%	[-0.9%, -0.6%]	2
Improvements ✅ (secondary)	-	-	0
All ❌✅ (primary)	-0.3%	[-0.9%, 0.5%]	3

Cycles

Results (primary 0.1%)

This is a less reliable metric that may be of interest but was not used to determine the overall result at the top of this comment.

	mean	range	count
Regressions ❌ (primary)	1.3%	[1.0%, 1.7%]	3
Regressions ❌ (secondary)	-	-	0
Improvements ✅ (primary)	-1.1%	[-1.9%, -0.7%]	3
Improvements ✅ (secondary)	-	-	0
All ❌✅ (primary)	0.1%	[-1.9%, 1.7%]	6

Binary size

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

Bootstrap: 775.475s -> 776.132s (0.08%)
Artifact size: 365.04 MiB -> 365.04 MiB (-0.00%)

[craterbot]

🚧 Experiment pr-140208 is now running

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

[craterbot]

🎉 Experiment pr-140208 is completed!
📊 66 regressed and 4 fixed (619632 total)
📰 Open the full report.

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

[compiler-errors]

@bors try

[bors]

⌛ Trying commit 8b2295f with merge aa39591...

[bors]

☀️ Try build successful - checks-actions
Build commit: aa39591 (aa39591f8789657c0627c7890f58b20d7a4c4b51)

[compiler-errors]

@craterbot check

[rustbot]

This PR changes a file inside tests/crashes. If a crash was fixed, please move into the corresponding ui subdir and add 'Fixes #' to the PR description to autoclose the issue upon merge.

[lcnr]

I would like to stop treating well-formed goals as coinductive, even if the reasoning for why it will be problematic is a bit far fetched.

---

We may want to elaborate WellFormed(Ty) where-clauses, e.g. allow a &'a T: where-bound to imply T: 'a.

We currently only elaborate where-bounds by eagerly extending the ParamEnv. we may want to generalize elaboration to simply consider sub-traits when proving super traits, e.g.

trait Trait: Sup {}
fn is_sup<T: Sup>() {}
fn foo<T: Trait>() {
    is_sup::<T>();
}

This currently elaborates the env to [T: Trait, T: Sup] and then proves T: Sup using that environment directly.

Alternatively, we could not elaborate the env and instead have the following proof tree:

• T: Sup prove via "super trait of Trait"
  • T: Trait via where-bound.

When doing this, we need to be careful that this doesn't allow for cyclic reasoning:

trait Trait: Sup {}
impl<T> Trait for T {}
fn is_trait<T: Trait>() {}
fn foo<T>() {
    is_trait::<T>();
}

If we simply check T: Sup when checking that he impl is well-formed:

• T: Sup prove via "super trait of Trait"
  • T: Trait prove via impl

We therefore need to prove T: Sup non-productively whenever we want to prove T: Trait

• T: Sup prove via "super trait of Trait"
  • T: Trait prove via impl, requires provnig super trait bounds
    • T: Sup non-productive cycle

With this, let's look at the following example:

struct WfImpliesOutlives<'a, T> {
    field: &'a T,
}
where
    T: 'a,
    Wf<'a, T>:;

Now, one could imagine that elaborating WellFormed clauses can also go backwards, i.e. proving T: 'a by checking wf(WfImpliesOutlives<'a, T>)

• T: 'a via "implied by well-formedness"
  • wf(WfImpliesOutlives<'a, T>)
    • T: 'a cycle
    • wf(WfImpliesOutlives<'a, T>) cycle

This means these cycles would have to be non-productive. With the current setup this is only achievable by making nested goals of WellFormed goals to be non-productive. I don't see a clean design where wf -> wf cycles are productive but wf -> other-predicate -> wf are not.

While I don't know whether we'll ever lazily elaborate WellFormed goals, I would prefer to not have to worry about this at all.

---

This PR causes the following snippet to no longer compile

struct Foo
where
    Foo:;

struct Bar
where
   Vec<Bar>:;

We do not break crates which have feature(generic_const_exprs) enabled as this feature relies on [whatever; CONST]: where bounds at add ConstEvaluatable clauses into the environment. The feature is very much incomplete and will need to get significantly reworked before landing, and any stabilization should use a better syntax.

It's generally difficult to support feature(generic_const_exprs) with the new solver and we currently want it to get replaced by a better approach before we're stabilizing the new solver.

This is why I believe that keeping WellFormed goals coinductive only when GCE is enabled is fine for now. Removing this special case for GCE later on should not require an FCP.

There is no crater breakage.

@rfcbot fcp merge

[rfcbot]

Team member @lcnr has proposed to merge this. The next step is review by the rest of the tagged team members:

• @BoxyUwU
• @compiler-errors
• @jackh726
• @lcnr
• @nikomatsakis
• @oli-obk
• @spastorino

No concerns currently listed.

Once a majority of reviewers approve (and at most 2 approvals are outstanding), this will enter its final comment period. If you spot a major issue that hasn't been raised at any point in this process, please speak up!

See this document for info about what commands tagged team members can give me.

[jackh726]

I'm okay with walking this back if we avoid actual breakage, even if the reasoning is "this is a bit weird and may block us in the future". I don't like the special-casing for GCE, but we're not walking through a door that we can't step back through if its actually always going to be required there, and its unstable.

[BoxyUwU]

I expect this special casing will not be necessary with mgca (or a potential full gca which would subsume gce), so with my const generics hat on I'm not too worried about this special case 🤔 It kind of sucks that we seem to be accumulating lists of hacks just to avoid breaking too much (unstable) gce code, but it is a relatively pragmatic choice and hopefully won't be necessary for too much longer...

[rfcbot]

🔔 This is now entering its final comment period, as per the review above. 🔔

[rfcbot]

The final comment period, with a disposition to merge, as per the review above, is now complete.

As the automated representative of the governance process, I would like to thank the author for their work and everyone else who contributed.

This will be merged soon.

[lcnr]

@bors r+ rollup

[bors]

📌 Commit 38c05a6 has been approved by lcnr

It is now in the queue for this repository.