Note that I am not even talking about determining whether a type is inhabited. I am talking about defining the term “inhabited”.
Care to elaborate?
Literally the only reason why I care about inhabitedness is for insta-UB. So I am pretty sure that this is exactly the definition we need for discussing match and UB. There might be other situations where other definitions are relevant, but this is a very specific discussion we are having here.
Well actually, it’s probably not even so relevant. We are drifting off into “basic layout invariants” again. Which is closely related but not the same thing…
If unsafe code does this, then we either have to quickly go ahead and change all that unsafe code (it probably does this for a reason, so we would have to provide some better way of doing things), or we better do not make it UB.
There is no space for “this is UB but code does it anyway”.
I assume you mean x: !? How can it be a NOP? Imagine this function:
fn foo(x: !) -> i32 { match x {} }
We have to generate some code. So a NOP is not an option.
And a compiler error… well that is possible, but the thing is: We do want a way to express in safe code that “this is an impossible situation we are in, so I do not need to write any more code here”. The function I wrote above looks funny because it is impossible to call, but that’s just because I am writing concrete code. (Also this is all to some extend counterfactual reasoning, so intuition can get a bit wonky here if you haven’t seen it in its “pure form”, e.g. in type theory.) This is in fact very similar to the () type – many other languages do not have it (void in C, C# or Java is not a type, you cannot use it for arguments). And indeed it is totally useless to write a function that takes an argument x: (). However, once you get to generic code, you can see the price that C# is paying: Abstracting over function types has to always handle both the case "f returns some type T", and "f returns void". By making () a proper type, Rust has avoided this situation, making generic code so much easier to write – now “there is no data here” is just a special case of “there is some data of type T here” with T = (). Now we just have to also make ! a proper type so that “this is impossible” is also just a special case of “there is some data of type T here” with T = !. Then it’ll be beautiful. 
For example, say you have plenty of code that works with a generic Result<T, E>, but then you have some specific code that knows that a certain action cannot go wrong, so it uses Result<T, !>. Now you want to get the data out there, i.e., turn the Result<T, !> into a T. You know there cannot be an error, so this should be possible in safe code without writing panics or so, and without run-time checks. Here is how:
fn bar<T>(x: Result<T, !>) -> T {
match x { Ok(t) => t, Err(!) }
}
And then many people think that having to write the impossible cases is not very ergonomic, so they want to be able to write
fn bar<T>(x: Result<T, !>) -> T {
match x { Ok(t) => t }
}
This is particularly useful when combined with irrefutable patterns in let:
fn bar<T>(x: Result<T, !>) -> T {
let Ok(t) = x;
// Now go on using `t`
t
}
The “completely empty” match x {} is then again just the case that falls out of generalizing ! to be a type that is usable anywhere. It is an edge case, and it is very useful for discussing properties of types like ! but not very useful to motivate them.
