I think I maybe-sorta get what problem we are actually trying to address here now (w.r.t. partially initialized product types), which is new. I don’t really mind the proposed solution - at least it’d work in the way I would “naively” expect in most cases - though I don’t feel entirely convinced that the added complexity is justified…
Couldn’t/shouldn’t this, rather than being tied to uninhabited types specifically, be a general feature of pattern matching which lets you assert “and there are no more cases” any time you have previously covered all the possible ones? E.g. match my_bool { true => thing, false => other_thing, ! } would also be legal. Which feels really redundant, but not more so than when the number of other possible cases was zero, so. (Is this the same thing @canndrew was proposing in the comment @Centril linked?)