Feature contract: match and match-with#

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

(match Family scrutinee (case Constructor binders... . body)...) and (match-with Family motive scrutinee (case Constructor binders... . body)...) are parenthesized prefix forms. A branch binder is an identifier or (ih name). case, ih, and match-with are structural only in these positions; ordinary applications with those names remain available when they do not have this shape.

2. Scope and binding rules, including generated names#

The checked family declaration supplies constructor order and field arity. Plain branch binders name constructor fields in declaration order. (ih name) may immediately follow a recursive field and exposes that field's induction result. An omitted induction result receives a hygienic inaccessible compiler name and cannot be referenced by source. Branch source order has no semantic effect.

3. Type and quantity requirements#

match needs an expected result type that is constant in the scrutinee. When no such expected type is available, or the result depends on the scrutinee, ALPHA-MATCH-NEEDS-MOTIVE requires match-with. The explicit motive of match-with has the same checked telescope as eliminate. Constructor fields and induction results retain their kernel-derived types and quantities.

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

Matching evaluates the scrutinee once. Branches are alternatives under the kernel's quantity accounting. The sugar adds no effects or partiality.

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

Both forms emit one ordinary exhaustive REliminate. The elaborator constructs the constant motive for match, derives branch binder layouts from the checked family, inserts inaccessible omitted induction binders, and emits branches in constructor declaration order. No trusted-core constructor is added.

6. Representation and target support, where relevant#

Erasure, checked interfaces, ALRI v4, and native lowering see only the existing eliminator and therefore require no representation revision.

7. Error codes and primary/secondary origins#

ALPHA-MATCH-NEEDS-MOTIVE, ALPHA-MATCH-MISSING-CASE, ALPHA-MATCH-DUPLICATE-CASE, ALPHA-MATCH-UNKNOWN-CASE, ALPHA-MATCH-BRANCH-ARITY, and ALPHA-MATCH-IH-POSITION are stable. Missing coverage points at the match; duplicate and unknown cases point at the offending case; an invalid IH marker points at that marker. Kernel type and quantity errors keep the originating branch body span.

8. Formatting and migration rules#

Canonical formatting preserves readable matching and comments. Expanded inspection renders the checked eliminate and validates closure-interface identity. alpha-2026 rejects both forms. No automatic eliminate-to-match migration exists because constant-motive and binder-intent recovery are not generally safe.

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

tests/language/matching/ owns SYN-004 fixtures for coverage, implicit and explicit motives over parameterized indexed families, recursive IH selection, branch order, source origins, core correspondence, formatting, quantity preservation, and native execution. The bootstrap surface suite independently exercises the same lowering and stable diagnostics.

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

The readable forms are introduced by alpha-2027. Their elaborated core remains valid in alpha-2026; the already-versioned edition cache key prevents a draft source parse from being reused under the stable edition.