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

Cyclic traits allow arbitrary traits to be synthesized #29859

Closed
nikomatsakis opened this Issue Nov 16, 2015 · 32 comments

Comments

Projects
None yet
@nikomatsakis
Copy link
Contributor

nikomatsakis commented Nov 16, 2015

This issue is partially fixed through the introduction of the "obligation jungle" but we still want to impose a limitation that auto traits cannot have supertraits (for now, no supertraits at all seems easiest). This would close the remaining soundness hole described here.

This is, I believe, an unintended outcome of some caching I put in. The problem is that this test compiles fine -- I believe the expected outcome was an internal stack overflow. My preferred fix is to refactor the fulfillment context to track trees in more detail, which is something that we've started but the branch has since bitrotted. This makes me want to get back to that more urgently.

@nikomatsakis

This comment has been minimized.

Copy link
Contributor Author

nikomatsakis commented Nov 16, 2015

triage: P-high

@nikomatsakis nikomatsakis self-assigned this Nov 16, 2015

@nikomatsakis

This comment has been minimized.

Copy link
Contributor Author

nikomatsakis commented Nov 16, 2015

(Probably) related: http://is.gd/2qIl3k (you'd want to extend this in a similar fashion to the original code snippet)

Update: weaponized form from eddyb http://is.gd/xks7Td

Update: unrelated, my mistake. This is #29861.

@eddyb

This comment has been minimized.

Copy link
Member

eddyb commented Nov 16, 2015

cc @james-darkfox (who tripped on this and #29861 in his lense crate)

@james-darkfox

This comment has been minimized.

Copy link
Contributor

james-darkfox commented Nov 16, 2015

Another simple example as follows: Magic treats anything as Copy, but this could 'imply' any traits like Send + Sync to send *mut ClearlyUnSendableThings.

trait Magic: Copy {}
impl<T: Magic> Magic for T {}

fn copy<T: Magic>(x: T) -> (T, T) { (x, x) }

#[derive(Debug)]
struct NoClone;

fn main() {
    let (a, b) = copy(NoClone);
    println!("{:?} {:?}", a, b);
}
@james-darkfox

This comment has been minimized.

Copy link
Contributor

james-darkfox commented Nov 18, 2015

@nikomatsakis Earlier I decided to create a "safe" hexdump using this concept. :-)

https://play.rust-lang.org/?gist=0832c0210daba58942c0&version=nightly

@jnicholls

This comment has been minimized.

Copy link

jnicholls commented Nov 18, 2015

This is a big issue. I think a fix needs to be put out for 1.4.0+ as soon as possible.

@bstrie

This comment has been minimized.

Copy link
Contributor

bstrie commented Nov 18, 2015

Related, what's our policy on nominating soundness fixes for backporting to beta?

@arielb1

This comment has been minimized.

Copy link
Contributor

arielb1 commented Nov 18, 2015

@nikomatsakis

In my understanding of the system, the impl was supposed to cause a WF error (why do we think that Self: Trait?) but in general this kind of code was intentionally supposed to actually work (I feel like we intentionally discussed it during the associated types RFC). What is going wrong exactly?

@arielb1

This comment has been minimized.

Copy link
Contributor

arielb1 commented Nov 18, 2015

The supertrait version looks more dangerous.

@arielb1

This comment has been minimized.

Copy link
Contributor

arielb1 commented Nov 18, 2015

Eh I got it - wfcheck checks Self::Out: Trait rather than expansion-of(Self::Out): Sized. We don't have to worry about "infinite" associated types because they are not supported - they cause a stack overflow, but we do have to worry about supertraits.

@arielb1

This comment has been minimized.

Copy link
Contributor

arielb1 commented Nov 18, 2015

As a fix, maybe not elaborate supertraits when checking WF? That would have an ugly annotation burden, but I am not sure how bad would it be.

@erickt

This comment has been minimized.

Copy link
Contributor

erickt commented Nov 19, 2015

This seems like a great candidate for a stable version bug fix release. According to play, hexdump works in 1.4. Is it in any older versions? If so, should we backport a fix to them?

@arielb1

This comment has been minimized.

Copy link
Contributor

arielb1 commented Nov 19, 2015

@erickt

The "supertrait" variant exists at least since multidispatch. The "associated type" variant is a problem with wf checking, but wf checking didn't really work before 1.5.

@aturon

This comment has been minimized.

Copy link
Member

aturon commented Nov 19, 2015

@bstrie We mark with beta-nominated for backports to beta. We don't currently have a way to mark for backporting beyond the current beta.

@erickt I suspect this goes all the way back to 1.0; it's not just an implementation issue, but may point to some deeper conceptual issues with how the trait system works. Before we talk about backporting in too much detail, we need to figure out how we want to address the problem (and see the code impact for doing so).

@nikomatsakis

This comment has been minimized.

Copy link
Contributor Author

nikomatsakis commented Nov 19, 2015

Let's first decide on what we want the fix to be before we discuss whether
to backport. I am not (personally) persuaded that this particular bug is
any worse than other soundness bugs, but it seems like a rather abstraction
discussion until we know what fix we plan to make.

@arielb1 I am not sure yet where I think the error should occur. My first
thought, like yours, was that the impl was in error, but I am now not so
sure. My second thought was that I would expect an infinite recursion
error, and I still do, but I'm not quite sure at what point. I think this
comes down to whether impl matching should be inductive not, and I think
the answer varies somewhat depending on the case, actually:

  1. Structural (nee OIBIT) traits definitely need to support this sort of
    recursion, in order to handle recursive types. For example, if you say that
    Foo is Send and it contains a Foo, you're relying on this sort of
    reasoning.
  2. For most other traits, though, I think an inductive model is perhaps
    correct. Do you think this is wrong?

I don't particularly like this division though. But I think that just
making the impl be unable to reason about facts that are present in the
trait definition doesn't feel like a very proper fix (and I'm not persuaded
it would suffice). Interestingly, most variations on this example that I've
tried to create produce infinite recursion, even ones that I expect to
work. I've been wanting to step through the compiler to see why that is,
and what goes differently here.

On Thu, Nov 19, 2015 at 10:22 AM, arielb1 notifications@github.com wrote:

@erickt https://github.com/erickt

The "supertrait" variant exists at least since multidispatch. The
"associated type" bug is a problem with wf checking, but wf checking didn't
really work before 1.5.


Reply to this email directly or view it on GitHub
#29859 (comment).

@nikomatsakis

This comment has been minimized.

Copy link
Contributor Author

nikomatsakis commented Nov 19, 2015

I wrote this:

But I think that just making the impl be unable to reason about facts that are present in the trait definition doesn't feel like a very proper fix (and I'm not persuaded it would suffice).

in response to @arielb1's comment here:

As a fix, maybe not elaborate supertraits when checking WF?

But I realize now I'm not 100% sure what he meant, so I potentially take it back. 😄

In any case, I'm stepping out the door just now (leaving on a trip for the next few days), but I'll definitely be pondering this. It may be that we can change something about how wfcheck is checking, but I'm not sure. One thing I would like to do is just to document precisely what the reasoning is for this test case that makes the trait checker accept it, in contrast to other similar-looking examples like this one. (*)

(*) A caveat, that example just happens to be one representative tab I have lying around open, it may have some small flaw that is orthogonal to this bug that's making it not work for all I know. But the main point is, it'd be interesting to try and pin down precisely why so many similar examples seem to not work, and make sure we have a fix that applies universally.

@james-darkfox

This comment has been minimized.

@nikomatsakis

This comment has been minimized.

Copy link
Contributor Author

nikomatsakis commented Dec 3, 2015

triage: P-high

I think the best fix for this in short term is to make non-structural-traits be inductive. I have a patch underway for this. But I'd like to think more about the longer term fix.

@arielb1

This comment has been minimized.

Copy link
Contributor

arielb1 commented Dec 3, 2015

I don't have serious objections to making non-structural-trait matching inductive, except that it would be a big scary breaking-change.

@angelsl

This comment has been minimized.

Copy link
Contributor

angelsl commented Dec 7, 2015

Obligatory segfault.

trait Magic: Copy {} impl<T: Magic> Magic for T {}
fn copy<T: Magic>(x: T) -> (T, T) { (x, x) }

#[derive(Debug)]
struct NoClone(String);

fn main() { println!("{:?}", copy(NoClone(String::from("cow")))); }
@jnicholls

This comment has been minimized.

Copy link

jnicholls commented Dec 7, 2015

lol.

Such recursive trait impl. are an illogical paradox and should not be
allowed. The generic type parameter should be used within the broader
definition of another type, not be the type. Is there really a use case
for such a definition?

On Sunday, December 6, 2015, angelsl notifications@github.com wrote:

Obligatory segfault. http://is.gd/QaGzmy

trait Magic: Copy {} impl<T: Magic> Magic for T {}
fn copy<T: Magic>(x: T) -> (T, T) { (x, x) }

#[derive(Debug)]
struct NoClone(String);

fn main() { println!("{:?}", copy(NoClone(String::from("cow")))); }


Reply to this email directly or view it on GitHub
#29859 (comment).

Sent from Gmail Mobile

@nikomatsakis

This comment has been minimized.

Copy link
Contributor Author

nikomatsakis commented Jul 1, 2016

@brson We've narrowed down this problem significantly but as far as I know not closed it completely. @arielb1 I recall at the dev sprint you proposed a set of rules concerning cycles that seemed reasonable -- I think it was to allow full coinductive reasoning for auto traits, but disallow an auto trait from supertraits or other similar side conditions?

@nikomatsakis

This comment has been minimized.

Copy link
Contributor Author

nikomatsakis commented Jul 1, 2016

@brson but I'm not sure what you mean when you say "still P-high". I guess you mean "would this warrant dropping everything and fixing this second"... if that's the question, the answer is clearly no. I guess what I'm saying is that I still feel like we never rejiggered our triage system to my satisfaction so I'm not entirely sure what the set of labels are :)

@brson

This comment has been minimized.

Copy link
Contributor

brson commented Jul 1, 2016

@nikomatsakis I am trying to steer P-high to mean "stuff people are working on this cycle".

@aturon

This comment has been minimized.

Copy link
Member

aturon commented Jul 1, 2016

@brson And P-medium is periodically re-triaged, right? So it offers a way to make sure we eventually get back to something? (We sometimes called this P-on-the-radar.)

@brson

This comment has been minimized.

Copy link
Contributor

brson commented Jul 1, 2016

@aturon That's the intent yeah. We should probably discuss more offline about our goals for process tracking though.

@pnkfelix

This comment has been minimized.

Copy link
Member

pnkfelix commented Jul 7, 2016

@arielb1 says he is planning to discuss this with @nikomatsakis . I-unsound already expresses the unsoundness aspect of the bug. We're going to demote this to P-medium, but if ariel or niko plan to address this in this cycle, they can promote it back to P-high.

@pnkfelix

This comment has been minimized.

Copy link
Member

pnkfelix commented Jul 7, 2016

triage: P-medium

jroesch added a commit that referenced this issue Aug 17, 2016

jroesch added a commit to jroesch/rust that referenced this issue Aug 17, 2016

jroesch added a commit to jroesch/rust that referenced this issue Aug 18, 2016

jroesch added a commit to jroesch/rust that referenced this issue Aug 18, 2016

bors added a commit that referenced this issue Aug 22, 2016

Auto merge of #35745 - jroesch:soundness-fix-29859, r=nikomatsakis
Fix soundness bug described in #29859

This is an attempt at fixing the problems described in #29859 based on an IRC conversation between @nikomatsakis and I today. I'm waiting on a full build to come back, otherwise both tests trigger the correct error.

bors added a commit that referenced this issue Aug 29, 2016

Auto merge of #35745 - jroesch:soundness-fix-29859, r=nikomatsakis
Fix soundness bug described in #29859

This is an attempt at fixing the problems described in #29859 based on an IRC conversation between @nikomatsakis and I today. I'm waiting on a full build to come back, otherwise both tests trigger the correct error.

jroesch added a commit to jroesch/rust that referenced this issue Aug 29, 2016

jroesch added a commit to jroesch/rust that referenced this issue Aug 29, 2016

bors added a commit that referenced this issue Aug 29, 2016

Auto merge of #35745 - jroesch:soundness-fix-29859, r=nikomatsakis
Fix soundness bug described in #29859

This is an attempt at fixing the problems described in #29859 based on an IRC conversation between @nikomatsakis and I today. I'm waiting on a full build to come back, otherwise both tests trigger the correct error.

bors added a commit that referenced this issue Aug 29, 2016

Auto merge of #35745 - jroesch:soundness-fix-29859, r=nikomatsakis
Fix soundness bug described in #29859

This is an attempt at fixing the problems described in #29859 based on an IRC conversation between @nikomatsakis and I today. I'm waiting on a full build to come back, otherwise both tests trigger the correct error.

bors added a commit that referenced this issue Sep 1, 2016

Auto merge of #35745 - jroesch:soundness-fix-29859, r=nikomatsakis
Fix soundness bug described in #29859

This is an attempt at fixing the problems described in #29859 based on an IRC conversation between @nikomatsakis and I today. I'm waiting on a full build to come back, otherwise both tests trigger the correct error.

jroesch added a commit to jroesch/rust that referenced this issue Sep 2, 2016

bors added a commit that referenced this issue Sep 8, 2016

Auto merge of #35745 - jroesch:soundness-fix-29859, r=nikomatsakis
Fix soundness bug described in #29859

This is an attempt at fixing the problems described in #29859 based on an IRC conversation between @nikomatsakis and I today. I'm waiting on a full build to come back, otherwise both tests trigger the correct error.

bors added a commit that referenced this issue Sep 8, 2016

Auto merge of #35745 - jroesch:soundness-fix-29859, r=nikomatsakis
Fix soundness bug described in #29859

This is an attempt at fixing the problems described in #29859 based on an IRC conversation between @nikomatsakis and I today. I'm waiting on a full build to come back, otherwise both tests trigger the correct error.

@bors bors closed this in 352fac9 Sep 8, 2016

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.