-
-
Notifications
You must be signed in to change notification settings - Fork 14.8k
Obligation caching allows for unsound coinductive matching #33344
Copy link
Copy link
Closed
Labels
I-unsoundIssue: A soundness hole (worst kind of bug), see: https://en.wikipedia.org/wiki/SoundnessIssue: A soundness hole (worst kind of bug), see: https://en.wikipedia.org/wiki/SoundnessP-highHigh priorityHigh priorityT-compilerRelevant to the compiler team, which will review and decide on the PR/issue.Relevant to the compiler team, which will review and decide on the PR/issue.
Metadata
Metadata
Assignees
Labels
I-unsoundIssue: A soundness hole (worst kind of bug), see: https://en.wikipedia.org/wiki/SoundnessIssue: A soundness hole (worst kind of bug), see: https://en.wikipedia.org/wiki/SoundnessP-highHigh priorityHigh priorityT-compilerRelevant to the compiler team, which will review and decide on the PR/issue.Relevant to the compiler team, which will review and decide on the PR/issue.
Type
Fields
Give feedbackNo fields configured for issues without a type.
STR
Expected Result
This should not compile, as adding
where T: Tweedledumtois_eedemonstrates.Actual Result
This typecks and fails on trans. A variant using
: 'staticcompiles but is unsound.Analysis
The current scheme for within-tree obligation caching checks in a very deliberate (and slow) way that obligations are not satisfied by their parents, but it allows sibling obligations to satisfy each-other.