Parent: #508. Reference: #597.
Add a completeness check for union eliminations to hydra.validate.core: for every case-statement term, resolve the corresponding union type from the schema and fail validation if any variant of that union is not covered — either by an explicit case alternative or by virtue of a default branch.
Concretely, in checkTerm's _Term_cases arm (which today runs the T4–T6 rules: empty type name, empty cases, duplicate case fields):
- Resolve the case statement's
typeName to its schema type and extract the union's field list.
- If the case statement has a default branch, every variant is covered by definition — no finding.
- Otherwise, compute the set difference (union variants) − (alternative names); if nonempty, emit a new
InvalidTermError variant (e.g. MissingCaseBranchesError) carrying the location, the union type name, and the uncovered variant names.
- The inverse condition — an alternative naming a variant that does not exist in the union — is adjacent and cheap from the same data; include it if not already covered elsewhere.
Motivation (see #597): incomplete elimination of a union is exactly the defect class just found by hand in Rewriting.subtermsWithSteps, where present-but-stub arms hid missing behavior. A coverage validator makes the absent-branch half of that class machine-checkable everywhere, permanently — any future Term/Type variant addition immediately surfaces every case statement that fails to handle it, instead of relying on hosts' exhaustiveness warnings (which several target languages do not have).
Note: a default branch satisfies the checker but also silences it — kernel traversals that want per-variant exhaustiveness (the #597 concern) should prefer explicit alternatives over defaults, which is a style matter for #597's audit, not this validator.
Parent: #508. Reference: #597.
Add a completeness check for union eliminations to
hydra.validate.core: for every case-statement term, resolve the corresponding union type from the schema and fail validation if any variant of that union is not covered — either by an explicit case alternative or by virtue of a default branch.Concretely, in
checkTerm's_Term_casesarm (which today runs the T4–T6 rules: empty type name, empty cases, duplicate case fields):typeNameto its schema type and extract the union's field list.InvalidTermErrorvariant (e.g.MissingCaseBranchesError) carrying the location, the union type name, and the uncovered variant names.Motivation (see #597): incomplete elimination of a union is exactly the defect class just found by hand in
Rewriting.subtermsWithSteps, where present-but-stub arms hid missing behavior. A coverage validator makes the absent-branch half of that class machine-checkable everywhere, permanently — any futureTerm/Typevariant addition immediately surfaces every case statement that fails to handle it, instead of relying on hosts' exhaustiveness warnings (which several target languages do not have).Note: a default branch satisfies the checker but also silences it — kernel traversals that want per-variant exhaustiveness (the #597 concern) should prefer explicit alternatives over defaults, which is a style matter for #597's audit, not this validator.