Lint for functions that don't return, but aren't written as "-> !"

[ghost]

See rust-lang/rust#12836

[Manishearth]

Probably should be a pedantic lint.

[llogiq]

Also bail for trait impls. We have a lot of unreachable!() impls of std::ops traits in typenum for example.

[felix91gr]

I'm trying to imagine this lint existing. If it did, couldn't it be used to solve the Halting Problem?
I'm going to try to put this into words.

---

Let's try to prove that this lint cannot exist.

Let's say I have a Rust Function, and I run this lint on it.

• If the function never returns, the lint triggers.
• If the function sometimes returns, the lint does not trigger.

Let's say now that I make a compiler that translates a Turing Machine and its initial Tape into a Rust function. This is possible and not very hard, but the details of that compiler I will leave aside because they're not important.

An implementation detail, however, will be that the resulting function will return the bit that the Head of the TM points to after it halts.

Okay. Almost there.

Let's say we grab some Turing Machine M, and get its resulting Rust function, f. f will have the following signature:

fn f() -> bool

Now, we will run Clippy with this lint turned on.

• If the function never returns, the lint triggers.
• If the function sometimes returns, the lint does not trigger.

If, respectively, M eventually stops, the lint will not trigger. If M never stops, the lint will trigger.

Therefore, we have used this lint to solve the Halting Problem. Which we know to be impossible.

Therefore, this lint cannot possibly exist.

[felix91gr]

@llogiq who can I ping to proofread me? I think I've successfully proven that this lint is impossible 🤔

[Manishearth]

Rust already has a compiler-level understanding of divergence, which does not require solving the Halting Problem, because the Halting Problem is about proving whether a function does or doesn't terminate, whereas Rust's divergence is a subset of that: Rust has functions which definitely do not terminate and then "the rest". You can prove that a function definitely does not terminate if all of its branches are diverging (this means: calling diverging functions/panics, or using loop {} with no break). This will not work for stuff like x = 1; while (x > 0) {... x+=1 } which also does not terminate but it's harder to programmatically prove that.

[Manishearth]

Most such theoretical concerns are not super relevant in the practical world where you seldom need 100% perfection.

Dependency resolution is also NP-complete. Doesn't stop Cargo from trying anyway, it just bails in pathological cases. It's good enough!

[felix91gr]

That's good and all that, but we have to be clear on something: the lint, as proposed originally in this issue, is impossible. That much is true, unless there's a mistake in my proof.

The entire issue discusses a lint that absolutely decides whether or not a function diverges. That would be a nice lint to have, but it ultimately does not exist. What you propose is a different lint.

[felix91gr]

Rust already has a compiler-level understanding of divergence, which does not require solving the Halting Problem, because the Halting Problem is about proving whether a function does or doesn't terminate, whereas Rust's divergence is a subset of that: Rust has functions which definitely do not terminate and then "the rest". You can prove that a function definitely does not terminate if all of its branches are diverging (this means: calling diverging functions/panics, or using loop {} with no break). This will not work for stuff like x = 1; while (x > 0) {... x+=1 } which also does not terminate but it's harder to programmatically prove that.

Is that an useful enough subset of divergence for the users of !? If so, maybe that's a lint worth pursuing.

[felix91gr]

Dependency resolution is also NP-complete. Doesn't stop Cargo from trying anyway, it just bails in pathological cases. It's good enough!

NP-complete is not the same as Undecidable, Manish. One is possible, the other is not :)

Most such theoretical concerns are not super relevant in the practical world where you seldom need 100% perfection.

Fair enough. Let's propose a different lint to the one this post was about: one that is incomplete but exists. I think both of us agree on this. The perfect divergence lint, which is what was being proposed, doesn't exist. Let's make an imperfect one, if it can be useful enough.

[y21]

The way I understand this issue is that the lint would check for functions where the function block has a NeverToAny adjustment, so e.g. the block in fn foo() { panic!(); } has its type adjusted from ! to (). It's information the compiler already has and is easily accessible to clippy, so I don't think we need to reinvent anything for this.

I don't think this is proposing something stronger than that. It wouldn't really make sense either I don't think; even if we did have the perfect lint that could detect functions that don't return, telling the user to annotate their functions with ! in cases where the compiler's notion of divergence is not smart enough would result in the compiler rejecting the code and would thus just result in false positives.

There's actually a lint that's somewhat similar: infinite_loop. Though it seems to target a subset of this (infinite loops specifically), but the motivation of that lint seems to be the same as this one (I'd think the lint from this issue would actually end up potentially simpler implementation-wise, because the existing lint needs to do a bunch of checks on the loop expression such as that there are no breaks targetting the loop or an outer one). I suppose the lint here could deprecate/supersede that one.

[Manishearth]

That's good and all that, but we have to be clear on something: the lint, as proposed originally in this issue, is impossible. That much is true, unless there's a mistake in my proof.

Uh, it's absolutely possible.

T issue doesn't actually provide parameters for a lint, so arguing about "the lint proposed in the issue" is kinda moot. It's pretty clear to the multiple clippy team members in this thread that there is a possible lint that (a) handles the code in the original issue (b) is useful and (c) is implementable. If you've imagined a different lint specification that was not written anywhere, you're free to prove it's impossible all you like but it's kinda irrelevant to talk about it here.

The original issue was this code:

fn f() -> int {
  fail!("f")
}

fn main() {
  f();
}

translated to modern Rust:

fn f() -> isize {
  panic!("f")
}

fn main() {
  f();
}

Rust absolutely knows that f() diverges. How? Because Rust allows this to compile:

fn f() -> ! {
  panic!("f")
}

Rust does not know that main() diverges, sure, but that's kind of normal in the lint design space. We never design global analyses. However, iterated local analyses that have an compile-fix-compile cycle are absolutely on the table. Such a lint would get you to "fix" f() first, and then get you to "fix" main() on the second compile cycle.

telling the user to annotate their functions with ! in cases where the compiler's notion of divergence is not smart enough would result in the compiler rejecting the code and would thus just result in false positives.

@y21 is bang on the mark here, there is no other way this lint could work. it MUST restrict itself into being annoying about functions that rustc can prove diverge, because there's not much more you can do here to appease the lint beyond changing the return value of the function to -> !.

[felix91gr]

The issue doesn't actually provide parameters for a lint, so arguing about "the lint proposed in the issue" is kinda moot.

The parameters are right there in the title, see?

Lint for functions that don't return, but aren't written as "-> !"

That's a clear a functional requirement as any.

If you've imagined a different lint specification that was not written anywhere

Again, written right there in the title.

It's pretty clear (...) that there is a possible lint that (a) handles the code in the original issue

I see. I misunderstood the reference in the original post. It says "see X", where X is a closed issue in the rust repo, which I did not expect to mean "this would be a continuation of the work in X". Alright, my bad.

The title is still pretty misleading, though.

[Manishearth]

... that's just being pedantic. I'm not sure if you're being serious, but we do not typically expect issue titles to be exact specifications. Grice's maxim of quantity encourages brevity in the case of unambiguity.

I wouldn't think it's necessary, but if you really feel the need for this: feel free to imagine ".. within the scope that it is possible" on every issue title on the clippy repo. We have many lints that are "lint on X (within the scope that is possible)", it's implicitly assumed, more or less.