The code example will work even if `u` is only known at runtime. That's because the inner switch is not matching on `u`, it's matching on `ab`, which is known at compile time due to the use of `inline`.

That may be confusing, but basically `inline` is generating different code for the branches .a and .b, so in those cases the value of `ab` is known at compile time. So, the inner switch is running at compile time too. In the .a branch it just turns into a call to handle_a(), and in the .b branch it turns into a call to handle_b().

The problem this is meant to solve is that sometimes a human thinking about the logic of the program can see it is impossible to reach some code (ie it is statically certain) but the language syntax and type system alone would not see the impossibility. So you can help the compiler along.

It is not meant for asserting dynamic “unreachability” (which is more like an assertion than a proof).