Feature contract: update — functional record update#

1. Lexical and grammar rules, including precedence and termination#

(update Family value (field = replacement)+) contains a family identifier, one scrutinee, and one or more grouped assignments. A zero-field update has no semantic purpose and remains an ordinary application spelling for compatibility. The form terminates at the outer close and shares ALPHA-PARSE-RECORD assignment diagnostics with construction.

2. Scope and binding rules, including generated names#

Assignments bind no names. Elaboration creates one motive and a constructor branch; expanded inspection alpha-renames all generated binders away from globals before emitting parseable source.

3. Type and quantity requirements#

The scrutinee must inhabit the named single-constructor family. Supplied fields must be unique, declared, and well typed in the progressively reconstructed telescope. Unspecified fields are retained. If an updated field occurs free in a later field's type, that dependent field must also be supplied; otherwise the old value is stale and the update is rejected.

4. Effects, totality, and evaluation-order rules#

The scrutinee is eliminated once and the constructor is rebuilt once. Supplied values follow declaration order. Update adds no effect; replacing a linear field while discarding its old value is rejected by quantity checking.

5. Elaboration into existing core or a specifically versioned new core extension#

Update becomes one REliminate; its sole branch emits the existing constructor with supplied replacements and branch variables for retained fields. Parameters come from the checked scrutinee family application.

6. Representation and target support, where relevant#

Only existing eliminator and constructor representation reaches erasure and native lowering. There is no mutation and no record-specific runtime layout.

7. Error codes and primary/secondary origins#

Duplicate and unknown assignments use ALPHA-RECORD-DUPLICATE-FIELD and ALPHA-RECORD-UNKNOWN-FIELD at the assignment. A stale dependency uses ALPHA-RECORD-STALE-DEPENDENT-FIELD at the changed field. Family mismatch uses ALPHA-RECORD-UPDATE-FAMILY; ordinary type and quantity codes retain the value origin which caused the kernel failure.

8. Formatting and migration rules#

Normal formatting keeps readable named updates and comments. Expanded inspection emits the checked eliminate/reconstruct form and accepts it only after a semantic-interface-identical overlay re-check.

9. Positive, negative, execution, and edge-case tests#

tests/language/records/Update.alpha covers exact core, retained values, duplicate/unknown/ill-typed fields, stale dependencies, and coordinated dependent updates. Bootstrap tests cover the same paths and linear replacement; the product diagnostic fixtures live under source-negative/.

10. Compatibility with the old edition, serialized forms, and cache keys#

The source form is draft alpha-2027; its expansion uses existing core and serialization. Cache identity already includes edition, and no format version is changed.