Reject a product with no fields instead of answering Unit

[dpmills]

materialize_record answered Unit for an empty field map, which is the silent arrival docs/chl-spec.md, "6.6 The empty product is unit" exists to rule out. Unit is a base type precisely so that a product reaches it only through an operation that says so: an empty field set is a subset of every field set, so a zero-field product would be a type every product flows into with every field dropped and nothing marking the loss.

A positive merge intersects field sets, so two products sharing no field merge to the empty map — and the answer was Unit, a type neither operand is a subtype of (Record([("a", Int)]) <: Unit is rejected, as it should be). Reachable from source and silent: (a=1) if c else (b=2) inferred as Unit. It now has no type, which is the honest answer — the only type above two such records would be the product that does not exist.

That rejection is CoalesceError::IncompatibleBounds, the error the same conflict one level up already raises: bounds with no common shape. The empty product is that read one level down, so it needs no error of its own. details names the empty field set rather than the operands, which the merge has already consumed by the time the position materializes.

Both polarities reject. One site serves both, and the invariant is not polarity-dependent — there is no zero-field product to require either.

Nothing in the suite depended on the old behaviour: instrumenting the branch showed no compiled program reaching it, so materialize_record's claim that it was reached by "a record variable that accumulated no field demands" described a case no test exercises.

type-inference.md's coalesce section said "no keys at all become Unit" and now says what the position is instead; the product constructor's empty-case collapse is unchanged, because a constructed empty product is an operation that says so.

products_sharing_no_field_are_incompatible_bounds pins the rejection and products_sharing_a_field_join_on_it pins its companion — a non-empty intersection still joins fieldwise, so this is about the empty case and not about products at a join.

[dpmills]

This change is part of the following stack:

• Scope inference variables with telescopes, and identify binder references by position #108
  • Hold a refined type's refinements in one unordered set instead of nested layers #77
    • Derive a Cast's refinements from its term instead of overwriting the target #78
      • Give CompactType's refinement slot the None sentinel its shape slots carry #115
        • Apply a function slot's domain rule once its kind is resolved, not at each merge #116
          • Give a function slot's domain alternatives an order-insensitive set #117
            • Reject a product with no fields instead of answering Unit #118 ◀
              • Model the type system in Lean, and check the solver's subtyping and bound merge against it #109

_{Change managed by git-spice.}