I don't follow that. A human reader of the code has to obey the same rules and perform the same analyses as the compiler if s/he wants to end up with a conclusion consistent with the actual behavior of the compiled program.
Yes, definitely, but the human doesn't have to keep it all in mind at once if the compiler does its job. We don't have to keep in mind the entire control-flow of the Microsoft Excel code, because compilers and code analysers together with the human design help us with it.
Yes, but if for example it slows down compilation significantly, now you forced everyone to suffer because of a niche situation.
Hence this question --- "Could the logic ...?". If, as you say "for example" it turns out to slow down things too much, of course, the answer to my question is "no". But I would like to understand if it is so, more on that below.
Assuming you are referring to the aptly-named coverage-vs-complexity index, what's wrong with the refactoring that transforms nested matches and loops into a single match and a function call? Looks way more testable and easier to understand to me.
Sure, I am quite happy about that too, but please note that inside that function I still have dead code, imposed by the compiler upon me --- when it could be just a warning, in case it's not feasible to compute the non-exhaustiveness of matches.
See, we will never have the anecdotal "sufficiently smart" compiler. Turing and Gödel doesn't let it exist. I bet we can almost always find more and more special cases in the language that seem obviously valid yet it's not possible to prove them correct using the existing rules.
Yes, of course, but I am not convinced that analysing nested matches, at least for a single non-mutable variable is anything like the halting problem, but please feel free to prove me wrong.
[...] And it empirically turned out to be a terrible way to design a language.
I agree with all your other statements regarding too many features inside the design of the language etc., and I am not asking for crazy features here, these nested matches can arise naturally when there is common control flow like I suggest above. I am asking for something like: for 2-3 levels of nested matches on the same non-mutable variable, have checking ability, and throw errors if problems are detected. And for more, throw warnings, how about that? Rather than, again, forcing me to write unreachable code!