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

update inductive_canonical_cycle test #787

Merged
merged 1 commit into from
Jan 9, 2023

Conversation

lcnr
Copy link
Contributor

@lcnr lcnr commented Jan 9, 2023

my concern was already known 😅

## What happens if we treat inductive cycles as errors?
So, what do we do when we hit an inductive cycle? Given that we told you that an
inductive proof cannot contain cycles, you might imagine that we can just treat
such a cycle as an error. But this won't give us the correct result.
Consider our previous example. If we just treat that cycle as an error, then we
will conclude that the impl for `Vec<T>` doesn't apply to `?X: A`, and we'll
proceed to try the impl for `u32`. This will let us reason that `?X: A` is
provable if `?X = u32`. This is, in fact, correct: `?X = u32` *is* a possible
answer. The problem is, it's not the only one!
In fact, `Implemented(?X: A)` has an **infinite** number of answers. It is true
for `?X = u32`. It is true for `?X = Vec<u32>`. It is also true for
`Vec<Vec<u32>>` and `Vec<Vec<Vec<u32>>>` and so on.
Given this, the correct result for our query is actually "ambiguous" -- in
particular, there is no unique substitution that we can give that would make the
query provable.

r? @jackh726

@jackh726
Copy link
Member

jackh726 commented Jan 9, 2023

@bors r+

@bors
Copy link
Contributor

bors commented Jan 9, 2023

📌 Commit 0ffedf2 has been approved by jackh726

It is now in the queue for this repository.

@bors
Copy link
Contributor

bors commented Jan 9, 2023

⌛ Testing commit 0ffedf2 with merge 808257c...

@bors
Copy link
Contributor

bors commented Jan 9, 2023

☀️ Test successful - checks-actions
Approved by: jackh726
Pushing 808257c to master...

@bors bors merged commit 808257c into rust-lang:master Jan 9, 2023
@lcnr lcnr deleted the update-inductive-canonical-cycle-test branch January 9, 2023 17:26
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``
RalfJung pushed a commit to RalfJung/miri that referenced this pull request Jan 13, 2023
update test for inductive canonical cycles

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

I checked with #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
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants