[solved, see thread] I just found a funny edge case in the "when expression must be exhaustive" check:

fun foo(a: Boolean, b: Boolean) = when { // "when expression must be exhaustive" error
    a == b -> "same"
    a -> "first"
    b -> "second"
    // this actually IS exhaustive:
    //  a | b | result
    // ---+---+--------
    //  0 | 0 | same
    //  1 | 0 | first
    //  0 | 1 | second
    //  1 | 1 | same
}

Do you guys think this is an issue that should be reported? 🙂 edit: I am not sure because surely this is just one example of a whole bunch of those cases and I personally would not want to implement thousands of corner cases into a language feature. (After all, this is a language, not platformer physics 😄)

its exhaustive to you, but your when expression doesn't know that. Your when doesn't know about a and b, or that it should check anything about a and b.

Yeah, logical exhaustiveness is not the same as exhaustiveness of an expression. You just kinda assume that

false, false

is equal to

true, true

Ah, so

when

does not care what

a

and

b

are... In this case they are final fields, but they could have been custom properties with getters that change their return value every time...

you haven't told when about anything right, so yeah there is a and b, but maybe theres a bunch of other variables in scope right? When by itself will only ever be exhaustive with an else. When using it the way you have here, it usually looks more like a switch .... when(someVariable) { // do stuff }

nice. another thing learned. thank you ❤️

What are you guys talking about? This is clearly exhaustive, and it's certainly possible to make

when

smarter for cases like this. I'd be happy if they did, but in the end it's a choice they made.

Doesn't this require the compiler to solve SAT?

In theory yes, but it would still be nice if it could solve some simpler cases. I understand that that would be a slippery slope and that they don't want to go that way.

There you go. https://youtrack.jetbrains.com/issue/KT-20943

@karelpeeters as things stand in this case, how would when know though? Without the context of what it means to be exhaustive? certainly it COULD be done if they decided to add it to the language, but as i said before it would generally be something like when(a, b) { // stuff } not when { } ... right?

class Bar(val a: Boolean) {
  fun foo(b: Boolean, c: Boolean) = when {
    a -> "a!"
    b == c -> "same"
    b -> "first"
    c -> "second"
  }
}

Yeah sure, for what I proposed the context would matter. Better pattern matching like in some other languages would work too:

when((a, b)) {
    (x, x) -> "same"
    (true, _) -> "first"
    (_, true) -> "second"
}

That solves the context problem but there's still SAT.

who knows, my brain isn't working well today which is why i'm hanging out here to begin with 😄 I suppose all branches of his original when expression are covered, but there's still other possibilities that could be added.. which I think means its not exhaustive even if it logically is.

You can add redundant branches but the original is definitely exhaustive.

its not entirely redundant, 'a' is not a path that ever could have happened in the original case. but also else would never be reached so... i could see both sides

(true, false)

would match the second one but not the first one.

no i mean in the one i posted.

Yours isn't redundant and it's exhaustive too!

i guess the question is what do they mean by exhaustive 😄 ... again you can't get to else. so on one hand yeah exhaustive. On the other there are infinite path possibilities beyond what is there that aren't redundant. due to the lack of context.

For yours there's enough context, there is always exactly one branch taken, no more no less.

yeah but at any given time i could add more and more branches. depending on your POV for "exhaustive" ... if i can add more possible paths that aren't redundant then I am not exhaustive

I don't get what you're saying, of course you can add more braches to the front but that doesn't matter right? It'll stay exhaustive.