Summary

Postcheck currently loses provenance for empty tag unions: an unconstrained type slot with no evidence and an explicit source-level empty tag union ([]) can both materialize to the same final Type.Store representation, an ordinary tag_union with an empty tag span.

That makes later stages unable to distinguish "this is a proven uninhabited type" from "this slot had no evidence yet when it was materialized." Some later code then treats the empty span as if it may still yield to later evidence, which is the design debt.

This came up during review of #10025 and was intentionally left unchanged there because it is separate from the nominal representation split.

Evidence

Relevant design points:

• design.md notes that unconstrained checked variables lower to an empty tag union.
• The forward design also treats the output Monotype IR as a completed snapshot that later stages should consume, not reinterpret or widen.

Relevant implementation points:

• src/postcheck/monotype/solve.zig has a distinct solving-time empty_tag_union state.
• During materialization, that state is written as an ordinary tag_union with an empty tag span.
• Importing an already-finished Monotype can reopen a zero-tag tag_union as unresolved row evidence.
• src/postcheck/lambda_solved/solve.zig has similar yielding behavior for empty tag unions, linking them to concrete peers instead of treating them as exact finished types.

Tests and observed consequences touch areas such as:

• recursive reverse inference/regression coverage (test/cli/Issue9885UnannotatedRecursiveReverse.roc)
• Str.inspect behavior around uninhabited values
• eval and CLI regression tests that exercise helper generation and specialization paths

Problem

The issue is not that [] is uninhabited; that is valid Roc semantics. The issue is that the compiler currently encodes two different meanings with the same final representation:

1. explicit/proven source-level empty tag union ([])
2. unresolved or unconstrained slot that had no evidence at materialization time

After that collapse, later stages recover intent from the incidental empty tag span. That conflicts with the compiler direction that post-check stages should consume explicit data produced by earlier stages rather than recovering, guessing, or widening missing information.

Impact

This can affect specialization, Lambda Solved type unification, function-template deduplication, Str.inspect, parser/encoder generation, and layout decisions for containers that involve uninhabited element types.

A visible failure mode would be either a postcheck invariant/panic or generated unreachable helper code such as uninhabited value reached Str.inspect when a reachable value path was incorrectly typed as containing [].

Suggested direction

Preserve provenance through Monotype so later stages can distinguish:

• explicit/proven uninhabited empty tag unions
• unresolved or unconstrained slots whose lack of evidence currently defaults to an empty tag union shape

Once the relevant specialization evidence has been applied explicitly, remove the later-stage reopen/yield behavior. Any attempted late widening of a finished explicit [] should become an invariant violation with a producer-side fix.