Hacker News Reader

Comment by pcwalton | Hacker News Reader

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.

View on HN

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 :)

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-...

> 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.

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.

The design problem has been fixed, as I noted above.

Reply on news.ycombinator.com