Skip to content

Obligation caching allows for unsound coinductive matching #33344

Closed
@arielb1

Description

STR

trait Tweedledum: IntoIterator {}
trait Tweedledee: IntoIterator {}

impl<T: Tweedledum> Tweedledee for T {}
impl<T: Tweedledee> Tweedledum for T {}

trait Combo: IntoIterator {}
impl<T: Tweedledee + Tweedledum> Combo for T {}

fn is_ee<T: Combo>(t: T) {
    t.into_iter();
}

fn main() {
    is_ee(4);
}

Expected Result

This should not compile, as adding where T: Tweedledum to is_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.

Activity

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

Metadata

Assignees

Labels

I-unsoundIssue: A soundness hole (worst kind of bug), see: https://en.wikipedia.org/wiki/SoundnessP-highHigh priorityT-compilerRelevant to the compiler team, which will review and decide on the PR/issue.

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions