Skip to content

WF is no longer coinductive? #169

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.

Sign up for GitHub

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

Jump to bottom
Closed
compiler-errors opened this issue Mar 21, 2025 · 4 comments · Fixed by rust-lang/rust#140208
Closed

WF is no longer coinductive? #169

compiler-errors opened this issue Mar 21, 2025 · 4 comments · Fixed by rust-lang/rust#140208
Assignees
@compiler-errors
Labels
A-coinduction S-breaking-change

Comments

@compiler-errors
Copy link
Member

Trivial WF cycles from where clauses seem to have broken in rust-lang/rust#136824.

struct Foo where Foo:;
@compiler-errors
Copy link
Member Author

Found from issue-64855-2.rs in the suite.

@lcnr
Copy link
Contributor

lcnr commented Mar 22, 2025

I am not sure whether it should be 😅 let's wait until we encounter this in the wild.

@compiler-errors
Copy link
Member Author

💀

@lcnr lcnr mentioned this issue Mar 23, 2025
Merged
@lcnr lcnr moved this from unknown to potentially irrelevant in -Znext-solver=globally Apr 4, 2025
@compiler-errors compiler-errors mentioned this issue May 5, 2025
Merged
@compiler-errors compiler-errors self-assigned this May 5, 2025
rust-timer added a commit to rust-lang-ci/rust that referenced this issue May 17, 2025
@rust-timer
Unrolled build for rust-lang#140208
28e1a5c 
Rollup merge of rust-lang#140208 - compiler-errors:wf-coinductive, r=lcnr

Make well-formedness predicates no longer coinductive

This PR makes well-formedness no longer coinductive. It was made coinductive in rust-lang#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 rust-lang#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 #109764 (not sure if this behavior is emulatable w/o coinductive WF?)

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

r? lcnr
@lcnr lcnr moved this from potentially irrelevant to done in -Znext-solver=globally May 18, 2025
@lcnr
Copy link
Contributor

lcnr commented May 18, 2025

fixed by making it not coinductive in the old solver as well in rust-lang/rust#140208

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@compiler-errors compiler-errors

Labels
A-coinduction S-breaking-change
Projects
-Znext-solver=globally
Status: done
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Make well-formedness predicates no longer coinductive compiler-errors/rust
2 participants
@compiler-errors @lcnr