[nicklecompte]

Perhaps I should have said "hole in the type theory" to clarify what I meant.

To be clear I wasn't trying to imply the rustc maintainers were ignorant of the difference. I meant that Rust programmers seem to treat fundamental design flaws in the language as if they are temporary bugs in the compiler. (e.g. the comment I was responding to) There's a big difference between "this buggy program should not have compiled but somehow rustc missed it" and "this buggy program will compile because the Rust language has a design flaw."

[pcwalton]

But it's not a fundamental design flaw in the language, nor is it a "hole in the type theory". It's a compiler bug. The compiler isn't checking function contravariance properly. Miri catches the problem, while rustc doesn't.

[comex]

You mean that Miri catches it at runtime, right? If so, that hardly demonstrates anything about the difficulty or lack thereof of fixing rustc’s type checker, since Miri is not a type checker and doesn’t know anything about “lifetimes” in the usual sense.

I agree that this isn’t a “fundamental design flaw in the language”, but Miri is irrelevant to proving that.

[pcwalton]

Yes. I'm not saying that Miri demonstrates anything other than that it's not a language issue.

[comex]

I’m not sure it even demonstrates that. For comparison, C’s inability to prevent undefined behavior at compile time definitely is a fundamental weakness of the language. Yet C has its own tools that, like Miri, can detect most undefined behavior at runtime in exchange for a drastic performance cost. (tis-interpreter is probably the closest analogy, though of course you also have ASan and Valgrind.)

Or to put it another way, the reason that Rust’s implied bounds issue is not a fundamental language issue is that it almost certainly can be fixed without massive backwards compatibility breakage or language alterations, whereas making C safe would require such breakage and alterations. But Miri tells us nothing about that.

[nicklecompte]

I believe it really is a flaw in the language, it's impossible for any compiler to check contravariance properly in this edge case. I don't think anything in this link is incorrect: https://counterexamples.org/nearly-universal.html?highlight=... (and it seems the rustc types team endorses this analysis)

I am not at all familiar with Miri. Does Miri consider a slightly different dialect of Rust where implicit constraints like this become explicit but inferred? Sort of like this proposal from the GH issue: https://github.com/rust-lang/rust/issues/25860#issuecomment-... but the "where" clause is inferred at compile time. If so I wouldn't call that a "fix" so much as a partial mitigation, useful for static analysis but not actually a solution to the problem in rustc. I believe that inference problem is undecidable in general and that rustc would need to do something else.

[pcwalton]

I think you're misinterpreting what "the implicit constraint 'b: 'a has been lost" in that link means. What it means is that the compiler loses track of the constraint. It doesn't mean that the language semantics as everyone understands them allows this constraint to be dropped. That sentence is describing a Rust compiler bug, not a language problem.

[nicklecompte]

I think you're misinterpreting what "implicit" means here. It doesn't mean "a constraint rustc carries around implicitly but sometimes loses due to a programming bug." It means "a constraint Rust programmers use to reason about their code but which rustc itself does not actually keep track of." "The implicit constraint 'b: 'a has been lost" should more precisely read "the implicit constraint 'b: 'a no longer holds."

Look closely at what happens:

  fn foo<'a, 'b, T> (_: &'a &'b (), v: &'b T) -> &'a T

There is an implicit "where 'b : 'a" clause at the end of this declaration - this clause would be explicit if Rust was more like OCaml. The reason this clause is there implicitly is that in correct Rust code you can't get &'a &'b if 'b : 'a doesn't hold. So when a human programmer reasons about this code they implicitly assume 'b: 'a even though there's nothing telling rustc that this must be the case.

This runs into a problem with the requirements of contravariance, which let us replace any instance of 'b in foo with any type 'd such that 'd : 'b, in particular 'static:

  fn foo<'a, 'b, T> (_: &'a &'static (), v: &'b T) -> &'a T

Since contravariance allows us to replace the &'a &'b with &'a &'static without changing the second &'b, the completely implicit constraint 'b : 'a is no longer actually being enforced, and there's no way for it to be enforced. This is not a compiler bug! It's a flaw in the design.

In particular I don't think there's anything especially magical about 'static here except that it works for any type 'a[1]. If you had a specific type 'd such that 'd : 'a then I think you could trigger a similar bug, converting references to 'b into references to 'd.

[1] Actually maybe "static UNIT: &'static &'static () = &&();" is more critical here since I don't think &'d &'d will work. Perhaps there's a more convoluted way to trigger it. This stuff hurts my head :)

[pcwalton]

Because Rust doesn't have a specification, we can argue back and forth forever about whether something is part of the "language design". The point is that the design problem has been fixed by desugaring to bounds on "for" since 2016 [1]. The only thing that remains is to implement the solution in the compiler, which is an engineering problem. It's not going to break a significant amount of code: even the bigger sledgehammer of banning contravariance on function types was measured to not have much of an impact.

As far as I can tell, the main reason to argue "language design" vs. "compiler bug" is to imply that language design issues threaten to bring down the entire foundation of the language. It doesn't work like that. Rust's type system isn't like a mathematical proof, where either the theorem is true or it's false and one mistake in the proof could invalidate the whole thing. It's a tool to help programmers avoid memory safety issues, and it's proven to be extremely good at that in practice. If there are problems with Rust's type system, they're identified and patched.

[1]: https://github.com/rust-lang/rust/issues/25860#issuecomment-...

[littlestymaar]

> Rust's type system isn't like a mathematical proof, where either the theorem is true or it's false and one mistake in the proof could invalidate the whole thing

Interestingly enough, in practice even mathematical proofs aren't like that either: flaws are routinely found when papers are submitted but most of the time the proof as a whole can be fixed.

Wiles first submission for his proof of Fermat's last theorem in 1993 is the best known example, but it's in fact pretty frequent.

[mjburgess]

His point seems to be that there are reasons in principle you cannot do this (holding the design fixed).

It's a little like making a type system turing-complete then saying, "we can fix the halting problem in a patch".

If you change the design, then you can fix it. This is what I interpret "design flaw" to mean.

[anderskaseorg]

In the language,

    fn foo<'a, 'b, T>(_: &'a &'b (), v: &'b T) -> &'a T { v }

should be equivalent to

    fn foo<'a, 'b, T>(_: &'a &'b (), v: &'b T) -> &'a T where 'b: 'a { v }

because the type &'a &'b is only well-formed if 'b: 'a. However, in the implementation, only the first form where the constraint is left implicit is subject to the bug: the implicit constraint is incorrectly lost when 'static is substituted for 'b. This is clearly an implementation bug, not a language bug (insofar as there is a distinction at all—ideally there would be a written formal specification that we could point to, but I don’t think there’s any disagreement in principle about what it should say about this issue).

[nicklecompte]

See my other comment above: https://news.ycombinator.com/item?id=39448909

The point is that rustc does not even implicitly have the "where 'b: 'a { v }" clause. The programmer knows "where 'b: 'a { v }" is true because otherwise &'a &'b would be self-contradictory, and in most cases that's more than enough. But in certain edge cases this runs into problems with the contravariance requirement since we can substitute either one of the 'bs with a type that outlives 'b (i.e. 'static), and the design of contravariance lets us do this pretty arbitrarily.

[anderskaseorg]

We could choose to design the language as I wrote where the constraint is implicitly present and variance consequently ought to preserve it, or as you wrote where it is not present at all and variance is unsound. But we want Rust to be sound, so we should choose the former design. We would need a very compelling reason to prefer the latter—for example, some evidence that “it would break too much code” or “it’s impossible to implement”—but I don’t see anyone claiming to actually have such evidence. The only reason the implementation has not been updated to align with the sound design is that it takes work and that work is still ongoing.

[withoutboats3]

The issue isn't contravariance but that higher ranked lifetimes can't have subtyping relations between them in rustc's implementation, so the fn pointer type is treated as a more general type than it is. This user is still wrong, the problem with rustc just isn't how it handles contravariance.

[nialv7]

Why is this distinction important? It's still something you fix by changing what programs the compiler accepts or rejects. Or were you trying to imply this is unfixable?

[nicklecompte]

Probably better to be maximally pedantic here:

- Assume our language has a specification, even if it's entirely in your head

- a "correct" program is a program that is 100% conformant to the specification

- an "incorrect" program is a program which violates the specification in some way

Let's say we have a compiler that compiles correct programs with 100% accuracy, but occasionally compiles incorrect programs instead of erroring out. If the language specification is fine but the compiler implementation has a bug, then fixing the compiler does not affect the compilation behavior of correct programs. (Unless of course you introduce a new implementation-level bug.) But if the language specification has a bug, then this does not hold: the specification has to change to fix the bug, and it is likely that at least some formerly correct programs would no longer obey this new specification.

So this is true:

> It's still something you fix by changing what programs the compiler accepts or rejects

But in one case you are only changing what incorrect programs the compiler accepts, and in the other you are also changing the correct programs the compiler accepts. It's much more serious.

[nextaccountic]

> - Assume our language has a specification, even if it's entirely in your head

It does not, and at the current pace, it might never have a spec.

The reason there is no spec - not even an hypothetical spec in my head - is that the exact semantics of Rust has not been settled.

With the constraints the Rust project are operating with, the only way forward I can think of is following the ideas laid out in post

https://faultlore.com/blah/tower-of-weakenings/

With the understanding that you can have multiple specs if one is entirely more permissive than the other (and as such, programmers must conform to the least permissive spec, that is, the spec that allows the smallest number of things)

But the problem is, Rust doesn't even have this least permissive spec. Or any other.

[lmm]

> Or were you trying to imply this is unfixable?

If it's been known since 2015 and not fixed, that's pretty suggestive.

[pcwalton]

It's been backed up behind a giant rewrite of more or less the entire trait system. This has been an enormous, many-year project that's been years late in shipping. The issue isn't so much the difficulty of the problem as the development hell that Chalk (and traits-next) has been stuck in for years.

[mwcampbell]

Is there anything we users can do to help get that project out of development hell? Besides not constantly getting the developers down, and even burning them out, with uninformed complaints and criticisms, which is something I try not to do.

[LoganDark]

> If it's been known since 2015 and not fixed, that's pretty suggestive.

That means nothing. In Rust, "everyone is a volunteer" and you're not allowed to expect things to be fixed unless you do it yourself - so the fact that this hasn't been fixed is simply an artifact of the culture, not necessarily the difficulty of the problem.

[chatmasta]

The distinction matters because any existing code that breaks with the compiler fix was either relying on "undefined behavior" (in the case of a compiler bug incorrectly implementing the spec), so you can blame the user, or it was relying on "defined behavior" (in the case of a compiler bug correctly implementing a badly designed spec), so you can't blame the user.

I suppose the end result is the same, but it might impact any justification around whether the fix should be a minor security patch or a major version bump and breaking update.

[estebank]

Rust's backwards compatibility assurances explicitly mention that breaking changes to fix unsoundness are allowed. In practice the project would be careful to avoid breaking more than strictly necessary for a fix.

In the case of user code that isn't unsound but breaks with the changes to the compiler/language, that would be breaking backwards compatibility, in which case there might be a need to relegate the change to a new edition.

[nialv7]

Well first of all, Rust doesn't even have a spec. And I would also advocate for not blaming anyone, let's just fix this bug ;)