Final variable initialization problem with exhaustive switch

[Dimitris Paltatzidis]

Consider the case:

enum Parity {ODD, EVEN}
Parity p = ...
final int a;
switch (p) {
    case Parity.ODD -> a = 1;
    case Parity.EVEN -> a = 0;
}
int b = a + 1; //Compile time error: variable a might not have been
initialized

The switch is exhaustive, yet we need to add a default case to compile. The
same behaviour is observed with instance final fields too.
Without changing the semantics, the code below compiles:

final int a = switch (p) {
    case Parity.ODD -> 1;
    case Parity.EVEN -> 0;
};
int b = a + 1; //Compiles

How can the compiler prove that the final variable will be initialized only
in the second case and not in the first too?

Thanks for your time.