Panic for else on exhaustive sealed when

[tjpalmer]

• Fix when expression with is-Type arms infers Void instead of arm type #427
• Panic when a sealed type is checked exhaustively rather than providing a void value
• For now, this exhaustiveness check relies on simple type checking conditions in the else-if chain, which should be the case for our current basic when-is block arms
• I didn't include the functional test from fix(IfTransform): when with is-Type arms now infers arm_types | Void #430, but I manually checked it, and the TypeStageTest case here shows that we can expect correct semantics

> temper test -b py
Tests passed: 3 of 3

[tjpalmer]

Look, Ma, no else!

[tjpalmer]

We can see the value assignments as well as the panic above. Maybe best even still to retain the panic in generated code for languages with exhaustiveness checking, especially for those that might be open in the runtime.

If we target some language later that disallows else in exhaustive cases, we'll have to deal with that when we come to it.

[tjpalmer]

This function is where the work happens.

[tjpalmer]

Here's the same removal from #430, but I didn't include the comment explaining the removal, given the extra context above. But based on tests, I believe Bobby is right that the other void (or now alternatively panic) is enough for our remaining handling.

[tjpalmer]

Comment above explains the strategy.

[tjpalmer]

This requires that all checks be for the same named value. If we want to be more flexible, we could track all checks for all named values, but when blocks should all be for the same, anyway.

And yes, this needs to be a named value, since that's much easier to check. Maybe our when handling already invents a named value when needed? I don't remember for sure.

[tjpalmer]

In a set, we can check just the sizes instead of the contents.

[mikesamuel]

I like the way this is done at the post-desugaring if step.

I wonder what we should do with a case like this:

classDiagram
    High <|-- Mid1
    High <|-- Mid2
    Mid1 <|-- Low1A
    Mid1 <|-- Low1B
    Mid2 <|-- Low2A
    Mid2 <|-- Low2B

Loading

By pure analysis of the following desugared when, it covers all Mid1 but does not cover Mid2.

sealed interface High {}

sealed interface Mid1 {}
sealed interface Mid2 {}

class Low1A extends Mid1 {}
class Low1B extends Mid1 {}
class Low2A extends Mid2 {}
class Low2B extends Mid2 {}

let f(x: High): String {
  when (x) {
    is Low1A -> "A";
    is Low1B -> "B";
  }
}

Could we detect that and issue an informative error message after we have type info?

[mikesamuel]

Approving. I think we can add some testcases and discuss ways to represent in the IR the expectation about when the inserted panic is unreachable, and how to undo that when the context really is void or issue a warning when it's not and explain the mismatched assumption.

[tjpalmer]

Could we detect that and issue an informative error message after we have type info?

Actually, looks like we could go simpler with just:

interface High {}

sealed interface Mid1 extends High {}
class Low1A extends Mid1 {}
class Low1B extends Mid1 {}

class Low2 extends High {}

Anyway, good catch. I guess I was just being genius. I'll check out some of the things you've recommended and make appropriate changes before merging this.

[tjpalmer]

And just to demo what type checks are and aren't allowed:

$ interface A {}; sealed interface B extends A {}; class C extends B {}; class D extends A {}
interactive#0: D__3
$ let d: A = new D();
interactive#1: void
$ d is C
interactive#2: false
$ d is D
interactive#3: true
$ new D() is C
1: new D() is C
   ┗━━━━━━━━━━┛
[interactive#4:1+0-12]@G: Runtime type check from D__3 to C__2 can never succeed
interactive#4: false

I just hadn't been thinking thoroughly when I originally coded this.

[tjpalmer]

Closed in favor of #452, which reuses some code from this branch.