Obligation caching allows for unsound coinductive matching #33344
Labels
I-unsound
Issue: A soundness hole (worst kind of bug), see: https://en.wikipedia.org/wiki/Soundness
P-high
High priority
T-compiler
Relevant to the compiler team, which will review and decide on the PR/issue.
STR
Expected Result
This should not compile, as adding
where T: Tweedledum
tois_ee
demonstrates.Actual Result
This typecks and fails on trans. A variant using
: 'static
compiles 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.
The text was updated successfully, but these errors were encountered: