Blog post: never patterns, exhaustive matching, and uninhabited types

(This is my last reply in this off-topic part of the discussion.)

Oh, great, another undefined term. :wink: Now what is "valid"?

No I am not. Undefined behavior is an abstract concept defined as part of the language semantics, it is not defined by whatever the compiler does currently.

(You had another sentence here that just disappeared. Good, then I will not respond to it.^^)

Ah, finally something where I can see the relation to this discussion. :smiley: So you are essentially saying one of these two things:

  • ! as a pattern should apply more generally to uninhabited types, not just specifically to empty enums and ! (which is nothing but a built-in empty enum). I disagree, because empty enums are a very simple concept that is easy to explain; uninhabitedness is much more subtle. Pattern matching is already very complicated, I'd like to avoid stuffing more complication into it.
  • Auto-never should generate the pattern Foo { a: _, b: ! }, letting you leave away match arms. That is a possible extension of auto-never, I do not have a strong opinion here.

I am not sure which of these positions you are arguing for though.

And maybe you are also arguing that self-referential structs like your earlier example should let you leave away match arms. While that has some appeal to it, it's also really complicated with (from what I have seen so far) no benefit. Having an analysis to detect this case, and having to explain this to everyone learning Rust, is a cost only worth paying if we get something out of this.

Pattern matching is, to a large extend, about enum, so I feel pretty good about restricting its reasoning about uninhabitedness to enums. When teaching this, we should then probably avoid talking about uninhabitedness in general and related the ! pattern directly to empty enums specifically, not uninhabited types in general. I think that makes everything much simpler while getting us almost all of the benefits and staying coherent.

These docs are written extremely conservatively because we do not know the exact rules yet.

But I appreciate that it can be hard to see what is a conservative approximation, and what is definite. The sad part is that almost nothing is definite.