Skip to content

Panic for else on exhaustive sealed when #439

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
tjpalmer wants to merge 3 commits into from
+199 −7
Closed

Panic for else on exhaustive sealed when #439

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
0a1bb70
Panic for else on exhaustive sealed when
tjpalmer Jun 13, 2026
02adbc7
Put extra void back in; test void case nearby
tjpalmer Jun 13, 2026
5dfe27d
Improve comment
tjpalmer Jun 13, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
132 changes: 132 additions & 0 deletions frontend/src/commonTest/kotlin/lang/temper/frontend/TypeStageTest.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2394,6 +2394,138 @@ class TypeStageTest {
|}
""".trimMargin().stripDoubleHashCommentLinesToPutCommentsInlineBelow(),
)

@Test
fun sealedWhen() = assertModuleAtStage(
stage = Stage.Type,
pseudoCodeDetail = PseudoCodeDetail.default.copy(showInferredTypes = true),
input = """
|export sealed interface Shape {}
|export class Circle() extends Shape {}
|export class Square() extends Shape {}
|export let describe(s: Shape): String {
| when (s) {
| is Circle -> "circle";
| is Square -> "square";
| // defaults to panic here because above is exhaustive
| }
|}

@tjpalmer tjpalmer Jun 13, 2026

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Look, Ma, no else!

""".trimMargin(),
want = """
|{
| type: {
| body:
| ```
| @typeDecl(Shape) @stay @sealedType let `test//`.Shape ⦂ Type;
| `test//`.Shape = type (Shape);
| @typeDecl(Circle) @stay let `test//`.Circle ⦂ Type;
| `test//`.Circle = type (Circle);
| @typeDecl(Square) @stay let `test//`.Square ⦂ Type;
| `test//`.Square = type (Square);
| @fn let `test//`.describe ⦂(fn (Shape): String), @typePlaceholder(Shape) typePlaceholder#0: Empty;
| typePlaceholder#0 = {class: Empty__0};
| @fn @visibility(\public) @stay @fromType(Circle) let constructor__0 ⦂(fn (Circle): Void);
| constructor__0 = (@stay fn constructor(@impliedThis(Circle) this__0: Circle) /* return__0 */: Void {
| return__0 = void
| });
| @fn @visibility(\public) @stay @fromType(Square) let constructor__1 ⦂(fn (Square): Void);
| constructor__1 = (@stay fn constructor(@impliedThis(Square) this__1: Square) /* return__1 */: Void {
| return__1 = void
| });
| `test//`.describe = (@stay fn describe(s__0 /* aka s */: Shape) /* return__2 */: String {
| var t#0 ⦂ Boolean, t#1 ⦂ Boolean;
| void;
| fn__0: do {
| if (!false) {
| t#0 = is(s__0, Circle)
| } else {
| t#0 = false
| };
| if (t#0) {
| return__2 = "circle"
| } else {
| if (!false) {
| t#1 = is(s__0, Square)
| } else {
| t#1 = false
| };
| if (t#1) {
| return__2 = "square"
| } else {
| return__2 = panic ⋖ String ⋗()
| }

@tjpalmer tjpalmer Jun 13, 2026

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

| };
| }
| })
|
| ```
| }
|}
""".trimMargin().stripDoubleHashCommentLinesToPutCommentsInlineBelow(),
)

@Test
fun unsealedWhen() = assertModuleAtStage(
stage = Stage.Type,
pseudoCodeDetail = PseudoCodeDetail.default.copy(showInferredTypes = true),
input = """
|export /* totally not sealed */ interface Shape {}
|export class Circle() extends Shape {}
|export class Square() extends Shape {}
|export let describe(s: Shape): String {
| when (s) {
| is Circle -> "circle";
| is Square -> "square";
| // defaults to void here
| }
|}
""".trimMargin(),
want = """
|{
| type: {
| body:
| ```
| @typeDecl(Shape) @stay let `test//`.Shape ⦂ Type;
| `test//`.Shape = type (Shape);
| @typeDecl(Circle) @stay let `test//`.Circle ⦂ Type;
| `test//`.Circle = type (Circle);
| @typeDecl(Square) @stay let `test//`.Square ⦂ Type;
| `test//`.Square = type (Square);
| @fn let `test//`.describe ⦂(fn (Shape): String), @typePlaceholder(Shape) typePlaceholder#0: Empty;
| typePlaceholder#0 = {class: Empty__0};
| @fn @visibility(\public) @stay @fromType(Circle) let constructor__0 ⦂(fn (Circle): Void);
| constructor__0 = (@stay fn constructor(@impliedThis(Circle) this__0: Circle) /* return__0 */: Void {
| return__0 = void
| });
| @fn @visibility(\public) @stay @fromType(Square) let constructor__1 ⦂(fn (Square): Void);
| constructor__1 = (@stay fn constructor(@impliedThis(Square) this__1: Square) /* return__1 */: Void {
| return__1 = void
| });
| `test//`.describe = (@stay fn describe(s__0 /* aka s */: Shape) /* return__2 */: String {
| var t#0 ⦂ Boolean, t#1 ⦂ Boolean;
| fn__0: do {
| if (!false) {
| t#0 = is(s__0, Circle)
| } else {
| t#0 = false
| };
| if (!t#0) {
| if (!false) {
| t#1 = is(s__0, Square)
| } else {
| t#1 = false
| };
| if (t#1) {}
| };
| return__2 = void
| }
| })
|
| ```
| }
|}
""".trimMargin().stripDoubleHashCommentLinesToPutCommentsInlineBelow(),
)
}

private object ImpureIgnoreFn : NamedBuiltinFun, CallableValue {
Expand Down
74 changes: 67 additions & 7 deletions interp/src/commonMain/kotlin/lang/temper/interp/IfTransform.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,21 +1,29 @@
package lang.temper.interp

import lang.temper.builtin.BuiltinFuns
import lang.temper.env.InterpMode
import lang.temper.log.spanningPosition
import lang.temper.name.TemperName
import lang.temper.type.TypeDefinition
import lang.temper.type.TypeShape
import lang.temper.type2.Signature2
import lang.temper.value.ActualValues
import lang.temper.value.CallTree
import lang.temper.value.ControlFlow
import lang.temper.value.Fail
import lang.temper.value.MacroEnvironment
import lang.temper.value.NamedBuiltinFun
import lang.temper.value.NotYet
import lang.temper.value.PartialResult
import lang.temper.value.ReifiedType
import lang.temper.value.Result
import lang.temper.value.SpecialFunction
import lang.temper.value.TEdge
import lang.temper.value.Value
import lang.temper.value.elseIfSymbol
import lang.temper.value.elseSymbol
import lang.temper.value.nameContained
import lang.temper.value.valueContained
import lang.temper.value.void

/**
Expand Down Expand Up @@ -183,16 +191,27 @@ internal object IfTransform : ControlFlowTransform("if") {
}
// Build branching subsystems from `else` backwards to `if`.
val hasFinalElse = branches.last().first == null
val exhaustiveAutoFinalElse = !hasFinalElse && anySealedTypesExhaustive(branches)
var branchIndex = branches.size
var controlFlow: ControlFlow? =
if (hasFinalElse) {
null
} else {
// Having a `void` here makes sure that static checks like UseBeforeInit
// get a diagnostic position for error logging.
ControlFlow.Stmt(
macroCursor.referenceToVoid(macroCursor.macroEnvironment.pos.rightEdge),
)
when {
// If someone has checked all subtypes for some supertype, panic instead of void.
exhaustiveAutoFinalElse -> {
val pos = macroCursor.macroEnvironment.pos
val panicCall = macroCursor.macroEnvironment.document.treeFarm.grow(pos) {
Block {
Call { V(BuiltinFuns.vPanic) }
}
}.edge(0)
macroCursor.referenceTo(panicCall)
}
// Otherwise, having a `void` here makes sure that static checks like UseBeforeInit
// get a diagnostic position for error logging.
else -> macroCursor.referenceToVoid(macroCursor.macroEnvironment.pos.rightEdge)
}.let { ControlFlow.Stmt(it) }
}
while (branchIndex != 0) {
branchIndex -= 1
Expand All @@ -218,11 +237,13 @@ internal object IfTransform : ControlFlowTransform("if") {
}
}

// `if` chains that don't end in an `else` should be typed as Void.
// Non-exhaustive `if` chains that don't end in `else` should be typed as Void.
// See LoopTransform comments on typing as for the problems with control-flow
// constructs that start with a condition and which don't reliably follow it
// with a typeable tree.
if (controlFlow != null && !hasFinalElse) {
if (controlFlow != null && !hasFinalElse && !exhaustiveAutoFinalElse) {
// TODO Record metadata on the added voids for better messages in case of errors later?
// TODO Maybe: "Use final `else` to provide a default value when not checking all sealed subtypes"?
controlFlow = ControlFlow.StmtBlock(
controlFlow.pos,
listOf(
Expand All @@ -239,3 +260,42 @@ internal object IfTransform : ControlFlowTransform("if") {
}
}
}

/**
* Check for simple sealed exhaustiveness. This requires that a single name be
* checked against each sealed subtype of some sealed supertype. If so, default
* to panic instead of void, which allows for type inference without an else.
*
* Rely on checks elsewhere for valid downcasts. And if the above holds and we
* could downcast, the check would be exhaustive in any case.

@tjpalmer tjpalmer Jun 13, 2026

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Comment above explains the strategy.

*
* TODO Fancy flowtyping check for exhaustiveness.
*/
private fun anySealedTypesExhaustive(branches: MutableList<Pair<TEdge?, TEdge>>): Boolean {
val allFoundSealedSubs = mutableMapOf<TypeShape, MutableSet<TypeDefinition>>()
var checkedName: TemperName? = null
branches@ for (branch in branches) {
val condition = branch.first?.target as? CallTree ?: continue@branches
condition.childOrNull(0)?.valueContained?.stateVector == BuiltinFuns.isFn || continue@branches
val nextCheckedName = condition.childOrNull(1)?.nameContained ?: continue@branches
when (checkedName) {
null -> checkedName = nextCheckedName
else if checkedName != nextCheckedName -> break@branches
else -> {}
}

@tjpalmer tjpalmer Jun 13, 2026

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

val subtype = condition.childOrNull(2)?.valueContained?.stateVector as? ReifiedType ?: continue@branches
val subdef = subtype.type2.definition
supertypes@ for (supertype in subdef.superTypes) {
val supershape = supertype.definition as? TypeShape
val sealedSubs = supershape?.sealedSubTypes ?: continue@supertypes
if (subdef in sealedSubs) {
val foundSealedSubs = allFoundSealedSubs.getOrPut(supershape) { mutableSetOf() }
foundSealedSubs.add(subdef)
if (foundSealedSubs.size == sealedSubs.size) {

@tjpalmer tjpalmer Jun 13, 2026

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

return true
}
}
}
}
return false
}
Loading