I propose to let the compiler recognize exhaustive...

# language-proposals

[uli]

I propose to let the compiler recognize exhaustiveness on when expressions without parameter.
Currently, the following definition gives 1 error + 1 warning

1: fun verificationText(verified: Boolean) : String {
2:     return when {
3:         verified -> "Verified"
4:         verified.not() -> "Not verified"
5:     } 
6: }

1. Error: ‘when’ expression must be exhaustive, add necessary ‘else’ branch (Line 2)
2. Warning: Value of ‘verified’ is always false (Line 4)
I disagree with the compiler. For me (2) means “yes, we have a catch all case. No need for exhaustive error, no need for warning.

In my everyday work, I use when expressions to exhaustively map combinations of boolean flags and feel that adding an else branch to the when above, just to shut up the compiler is big pain.

[dmitriy.novozhilov]

Compiler can't track such information at the moment
The warning (2) is not actually a warning but an IDE inspection

[uli]

Compiler can’t track such information at the moment

That’s why this is a proposal 😉
Or do you mean, the compiler can not reasonably made to track such information?

The warning (2) is not actually a warning but an IDE inspection

Ah, yes. Thanks for pointing out.

[dmitriy.novozhilov]

Or do you mean, the compiler can not reasonably made to track such information?

Theoretically it may be implemented, but there are no plans for it in the nearest future
Also your example is more or less meaningless, as it can be rewritten in much cleaner way which is understandable by the compiler and more readable for user, but there is a real case for integer values for progressions check

val x: Int = ...
when {
    x > 0 -> ...
    x == 0 -> ...
    x < 0 -> ...
    // else required but never executed
}

[uli]

> as it can be rewritten in much cleaner way which is understandable by the compiler
Do you mean by using when(verified) ? Or if/else?
Yes, in real life, it would be more then one boolean:

1: fun verificationText(a: Boolean, b: Boolean) : String {
2:     return when {
3:         a && b.not() -> "Yes, you have a"
4:         a && b -> "Yes, you have a and b"
5:         a.not() -> "Sorry, you don't have a"
6:     } 
7: }

[uli]

And one more

Compiler can’t track such information at the moment

The IDE already knows that the last case will always match (see warning). So I think the tracking is already in place

[uli]

Well, interestingly, the ide does not warn in my latest example above

[uli]

but there is a real case for integer values for progressions check

Yes, good one but I would think sure harder to track

[dmitriy.novozhilov]

The IDE already knows that the last case will always match (see warning). So I think the tracking is already in place

It is implemented in IDE infrastructure
So yes, the algorithm is known, but it's unknown if it acceptable for the compiler/how hard to port it

[ephemient]

https://youtrack.jetbrains.com/issue/KT-20943

[uli]

thanks @ephemient

[uli]

Final comment by @abreslav from 2018:
> Wouldn’t this require the compiler to solve SAT?
Interesting question. And if Andrey is right, would it really be an issue with the number of cases a regualar developer can reasonably write in a when statement? We only need to prove, that the ‘when’ is non exhaustive. I.e. is an exhaustive when with a large number of variables something a developer can even write?

[ephemient]

I see the compiler and IDE being under different limitations. it's somewhat OK if the IDE analysis changes or gives up sometimes. but the compiler must do the same thing every time.