prometeu-studio/docs/specs/pbs/4. Static Semantics Specification.md

# PBS Static Semantics Specification

Status: Draft v1 (Normative)  
Scope: binding, callable formation, type checking, and deterministic function application

## 1. Purpose

This document defines the static semantics of PBS core language.

It is intended to:

- give deterministic meaning to declarations accepted by the syntax specification,
- define callable identity and application rules,
- make type checking stable across implementations,
- preserve beginner-facing clarity without hidden callable behavior.

## 2. Core Semantic Model

### 2.1 Authority and precedence

Normative precedence:

1. Runtime authority (`docs/specs/hardware/topics/chapter-2.md`, `chapter-3.md`, `chapter-9.md`, `chapter-12.md`, `chapter-16.md`)
2. Bytecode authority (`docs/specs/bytecode/ISA_CORE.md`)
3. `3. Core Syntax Specification.md`
4. This document

If a rule here conflicts with higher authority, it is invalid.

### 2.2 Semantic namespaces

PBS distinguishes at least:

- type namespace,
- value namespace,
- callable namespace.
- host-owner namespace.

Rules:

- `declare struct`, `declare service`, `declare contract`, `declare error`, `declare enum`, and `declare callback` introduce names in the type namespace.
- `declare host` introduces names in the host-owner namespace.
- `let`, parameters, and `declare const` introduce names in the value namespace.
- `declare service Name` also introduces the canonical singleton value `Name` in the value namespace.
- Top-level `fn`, service methods, and host methods participate in the callable namespace.
- `fn` declarations are not first-class values in v1 core and therefore do not become ordinary value expressions.
- `bind(...)` is a callback-formation construct, not a general function-value construct.
- `declare host` declarations are reserved to SDK/toolchain-controlled modules and are not formable in ordinary user-authored PBS source.
- A host owner name is not an ordinary value expression in v1 core; it is used only as a qualified host-call owner.

### 2.3 Attribute metadata

Attributes are compile-time metadata attached to declaration surfaces.

Rules:

- An attribute has no value-level or type-level meaning by itself.
- Attributes are not first-class values and are not reflectable in v1 core.
- Attributes do not automatically survive into runtime or bytecode artifacts.
- An attribute affects runtime artifacts only when another specification defines an explicit lowering for its semantic effect.
- In v1 core, the only normative reserved attribute is `Host`.
- `Host` is valid only on a host method signature declared directly inside a reserved stdlib/interface-module `declare host` body.
- `Host` is invalid on ordinary user-authored modules, top-level `fn`, struct methods, service methods, callbacks, contracts, and constants.
- `Host` metadata is consumed by the compiler during host-binding lowering.
- The `Host` attribute syntax itself is not exported as runtime metadata; instead, its canonical identity participates in PBX host-binding emission as defined by the Host ABI Binding specification.

### 2.4 Tuple shapes

Static checking uses tuple shapes as semantic objects.

Definitions:

- Input tuple shape: ordered sequence of zero or more input slots.
- Output tuple shape: ordered sequence of zero or more output slots.
- Each slot has a type and a stable label.

Rules:

- Tuple shapes in PBS core are always named, except for unit `()`.
- Input slot labels come from parameter names and are local frame names.
- Output slot labels come from return annotations and are visible for multi-slot member projection.
- Tuple-shape identity for overload and resolution ignores labels.
- Tuple-shape compatibility requires matching arity and positional slot types.
- Labels must still be preserved as part of declaration surface and projection metadata.
- A single-slot tuple shape has a distinguished carrier value type equal to its slot type.
- In value positions, single-slot tuple values collapse to their carrier value type.
- Single-slot tuple shapes have no dedicated tuple-literal surface in v1 core.

## 3. Functions and `apply`

### 3.1 Canonical function model

Every callable `fn` in PBS is modeled statically as:

```text
Fn : InputTuple -> OutputTuple
```

Rules:

- `fn f(a: A, b: B)` has input tuple shape `(a: A, b: B)`.
- `fn f()` has empty input tuple shape `()`.
- `-> void`, `-> ()`, and omitted return annotation all denote empty output tuple shape `()`.
- `-> T` denotes a single-slot output tuple shape `(value: T)`.
- `-> (x: T)` denotes a single-slot output tuple shape `(x: T)`.
- `-> (x: T, y: U)` denotes a two-slot output tuple shape `(x: T, y: U)`.
- `-> T` and `-> (x: T)` are identical for overload identity and differ only in preserved label metadata.
- `optional T` is a regular value type and may appear in parameters, locals, fields, and plain returns.
- `optional T` with single-slot payload is internally normalized to `optional<(value: T)>`.
- `optional` and `optional void` are invalid type surfaces.
- `-> result<E> T` denotes a result return surface over payload shape `T` and error type `E`.
- `-> result<E> T` with single-slot payload is internally normalized to `result<E, (value: T)>`.
- `-> result<E>` is valid and denotes a result return surface with unit payload.
- A function return surface may be plain or `result<E>`.
- A function return surface must not combine `optional` and `result` in the same declaration.
- `result<E>` wraps the declared success payload; the payload itself may be scalar or a named tuple shape.

### 3.2 Callable categories

The following constructs are callable in v1 core:

- top-level `fn`,
- struct methods on concrete receivers,
- contract values,
- callback values,
- service methods,
- host methods on declared host owners.

Rules:

- All callable categories use the same input/output tuple model.
- A struct method is identified by `(struct type, method name, input tuple shape excluding the receiver slot, output tuple shape)`.
- A contract value is identified at the type level by its contract type and at runtime by an underlying concrete struct instance or service singleton value plus its selected implementation.
- A callback declaration defines a nominal callable type with exactly one input/output tuple shape.
- A service method is identified by `(service name, method name, input tuple shape, output tuple shape)`.
- A host method is identified by `(host owner name, method name, input tuple shape, output tuple shape)` within the PBS declaration surface.
- A top-level `fn` is identified by `(name, input tuple shape, output tuple shape)`.
- A callback value is identified at the type level by its declared callback type and signature.
- Contract signatures and barrel signatures must preserve the same callable shape.
- Canonical host primitive identity and binding are governed by the Host ABI Binding specification rather than by ordinary v1 core declaration identity alone.

### 3.3 Declaration validity

Rules:

- Parameter names in a single `ParamList` must be unique.
- Output labels in a named tuple return annotation must be unique.
- Error case labels in a single `declare error` body must be unique.
- Enum case labels in a single `declare enum` must be unique.
- Enum case integer identifiers in a single `declare enum` must be unique.
- Two declarations with the same callable name and the same input/output tuple shape are duplicates.
- Changing only parameter names does not create a new callable.
- Changing only input labels in `ParamList` does not create a new callable.
- Changing only output labels does not create a new callable.
- `mod.barrel` function entries are matched by callable identity, ignoring labels.
- Barrel labels may differ from implementation labels.
- Any return surface that combines `optional` and `result` is statically invalid.
- Any payload-less `optional` type surface is statically invalid.
- Any `optional void` type surface is statically invalid.
- A host method signature in a reserved stdlib/interface module MUST carry exactly one `Host` attribute.
- A `Host` attribute MUST declare exactly the named arguments `module`, `name`, and `version`.
- `Host.module` and `Host.name` MUST be non-empty string literals.
- `Host.version` MUST be a positive integer literal.
- Two host methods in the same resolved stdlib environment MUST NOT lower to the same canonical `(module, name, version)` unless they denote the same host method declaration after project/module resolution.
- A `declare const` declaration must include an explicit type annotation.
- A `declare const` initializer must be a constant expression.
- `declare const` dependency resolution is module-wide and must not depend on source-file processing order.
- `declare const` dependencies must form an acyclic graph.

### 3.4 Constant expressions

PBS core v1 restricts top-level constant evaluation to a deterministic compile-time subset.

Rules:

- A `declare const` initializer is evaluated at compile time.
- A `declare const` may depend only on previously resolved visible `declare const` declarations and enum case values.
- Cross-file constant resolution within a module is defined by dependency analysis, not source-file order.
- Constant evaluation fails if the dependency graph contains a cycle.
- The allowed constant-expression forms in v1 core are:
  - scalar literals: `IntLit`, `FloatLit`, `StringLit`, `BoolLit`,
  - enum case paths `EnumName.caseName`,
  - a reference to another visible `declare const`,
  - unary `-` applied to an integer or float constant expression,
  - unary `not` or `!` applied to a boolean constant expression,
  - binary arithmetic operators over numeric constant expressions,
  - binary comparison operators over compatible constant expressions,
  - binary boolean operators over boolean constant expressions.
- A `declare const` initializer must not use:
  - callable application or call sugar,
  - `new`,
  - `bind(...)`,
  - `some(...)` or `none`,
  - tuple expressions,
  - block expressions,
  - `if`, `switch`, `handle`, `else` extraction, or `!` result propagation,
  - method calls or member access except enum case paths.
- The initializer type must be compatible with the declared `const` type.
- A `pub const` may be imported from another module only through ordinary module import rules.
- A `declare const` does not introduce mutable runtime storage; implementations may inline, fold, or materialize it as an immutable constant as long as observable semantics remain unchanged.

### 3.5 Enum declarations and values

Rules:

- `declare enum Name(case1, case2, ...);` introduces a nominal enum type `Name`.
- `declare enum Name(case1 = n1, case2 = n2, ...);` introduces explicit integer identifiers for enum cases.
- If no enum case uses an explicit identifier, identifiers are assigned as `0..n-1` in declaration order.
- If any enum case uses an explicit identifier, then every enum case in that declaration must use an explicit identifier.
- `Name.case` is a valid enum value surface only when `Name` resolves to a declared enum type and `case` resolves to a declared case of that enum.
- The static type of `Name.case` is the enum type `Name`.
- Error labels are not enum cases and must not be used where enum case values are required.

### 3.6 Structs, services, methods, and contracts

Rules:

- Struct values are heap-backed reference values in v1 core.
- Service values are canonical module-owned singleton values in v1 core.
- `new Struct(args...)` allocates a new struct instance of the declared struct type.
- `new Struct.ctorName(args...)` invokes a named constructor declared in the enclosing struct body and produces a new struct instance of that type.
- Struct construction arguments are matched positionally to the declared struct field order.
- Assigning a struct value copies the reference, not the underlying field storage.
- Assigning a service value copies the same canonical singleton identity; it does not create a new instance.
- A struct field with no access modifier is readable and writable only from methods and `ctor` bodies of its enclosing struct.
- A `pub` struct field is externally readable but remains externally non-assignable.
- A `pub mut` struct field is externally readable and externally assignable.
- An assignment target `expr.name` to a struct field is valid only when the access site is permitted to write that field.
- Writes to a private struct field are valid only through `this.name` inside methods and `ctor` bodies of the enclosing struct.
- A struct method declared in a struct body has an implicit receiver binding `this` of type `Self`.
- A service method declared in a service body has an implicit receiver binding `this` of type `Self`.
- `this` is valid only inside struct method, service method, and `ctor` bodies.
- `Self` is valid only in struct method, service method, and `ctor` declarations and denotes the enclosing owner type.
- The enclosing struct name is in scope inside its own field declarations, enabling self-referential field types.
- A named `ctor` declared in a struct body is not a method, but it does introduce an implicit under-construction `this`.
- A `ctor` has no declared return annotation and is not a `fn`.
- A `ctor` completes by falling off the end of its body after initializing the enclosing struct instance.
- Every field of the enclosing struct must be definitely assigned on every completing `ctor` path.
- Named constructors participate in overload resolution by name plus parameter signature.
- `return;` and `return expr;` are both invalid inside `ctor` bodies.
- Methods declared in a struct body belong to the direct method namespace of that concrete struct type.
- Methods declared in a service body belong to the direct method namespace of that concrete service type.
- `receiver.method(...)` on a concrete struct receiver resolves only against methods declared directly in that struct body.
- `receiver.method(...)` on a service receiver resolves only against methods declared directly in that service body.
- `receiver.ctorName(...)` is never valid on a concrete struct value.
- Service values are ordinary value expressions and may be assigned, passed, and returned under their declared service type.
- Services do not have fields.
- Services do not declare named constructors and are never targets of `new`.
- Contract implementations do not inject their methods into the direct method namespace of the concrete struct or service.
- `implements Contract for Owner using s { ... }` is unique per `(Contract, Owner)` pair, where `Owner` is a declared struct or service.
- A contract for a struct or service may be implemented only in the module where that owner itself is declared.
- Contracts may be declared in other modules and implemented for the local struct or service in its owner module.
- An `implements` block has no independent visibility; its observability follows the visibility of the owner declaration, and the contract must also be nameable at the use site.
- Methods declared directly inside a struct or service follow the visibility of their enclosing owner declaration; they do not have independent visibility.
- A struct value or service singleton value may be coerced to a contract value when exactly one visible `implements Contract for Owner ...` applies.
- Contract coercion may happen by explicit `expr as ContractType` or by contextual typing in assignments, parameter passing, and returns.
- `as` in expression position is reserved for explicit contract coercion only; no other cast semantics exist in v1 core.
- The contract name in `expr as ContractName` must be a simple visible identifier resolved through ordinary scope and import rules.
- A contract value carries the underlying struct reference or service singleton value together with the selected contract implementation for runtime dispatch.
- Calling `contractValue.method(...)` uses dynamic dispatch through the contract value.
- Calling `structValue.contractMethod(...)` is not valid unless that method is also declared directly on the struct.
- Calling `serviceValue.contractMethod(...)` is not valid unless that method is also declared directly on the service.
- Structs do not have static methods in v1 core; named constructors are their only type-qualified callable members.
- Services are accessed through their canonical singleton value, not through `new` or static method declarations.

Example:

```pbs
declare contract StasisProcess {
  fn stasis() -> int;
}

declare struct Struct(pub a: int) {
  fn compute() -> int {
    return this.a;
  }

  ctor createWithSomethingSpecial(x: int) {
    this.a = x;
  }
}

implements StasisProcess for Struct using s {
  fn stasis() -> int {
    return s.compute();
  }
}

fn demo() -> int {
  let s = new Struct(1);
  let s2 = new Struct.createWithSomethingSpecial(2);
  let sp: StasisProcess = s;
  let sp2 = s as StasisProcess;
  let a = s.a;
  let _ = s2.compute();
  let b = sp.stasis();
  let c = sp2.stasis();
  return a + b + c;
}
```

### 3.7 Nominal callbacks

Rules:

- `declare callback Name(params...) -> R;` introduces a nominal callback type `Name`.
- A callback type is not a `fn`, and a `fn` declaration does not implicitly define a callback type.
- A value of callback type may be formed only from a compatible top-level `fn` in v1 core.
- A value of callback type may also be formed by `bind(context, fn_name)` when the surrounding static type context expects a callback type.
- Service methods are not assignable to callback values in v1 core.
- Host methods are not assignable to callback values in v1 core.
- Callback values do not capture local environment implicitly.
- Assignment of a top-level `fn` to a callback type succeeds only when exactly one visible overload matches the callback signature.
- `bind(context, fn_name)` succeeds only when exactly one visible top-level `fn` overload matches after consuming the first parameter with `context`.
- Valid expected callback contexts for `bind(context, fn_name)` include variable initialization with an explicit callback type, assignment to an explicitly typed callback location, argument passing to a callback-typed parameter, and return from a callback-typed function.
- The context expression in `bind(context, fn_name)` is evaluated once at bind time and stored explicitly in the resulting callback value.
- The stored context follows normal value semantics for its type.
- `bind(context, fn_name)` does not introduce general closures; it is explicit partial binding of the first parameter only.
- Callback compatibility ignores labels and compares ordered input/output slot types plus the return-surface kind.

Example:

```pbs
declare callback TickCb(dt: int) -> void;

fn on_tick(dt: int) -> void {
}

fn install_tick() -> void {
  let cb: TickCb = on_tick;
  let _ = cb;
}
```

Bound example:

```pbs
declare callback UpdateCb(dt: int) -> void;

declare struct Enemy(hp: int);

fn update_enemy(self: Enemy, dt: int) -> void {
}

fn install_update(enemy: Enemy) -> void {
  let cb: UpdateCb = bind(enemy, update_enemy);
  let _ = cb;
}
```

Ambiguous overload example:

```pbs
declare callback TickCb(dt: int) -> void;

fn tick(dt: int) -> void {
}

fn tick(time: int) -> void {
}

fn install_tick() -> void {
  let cb: TickCb = tick; // error: ambiguous overloaded fn assignment
}
```

### 3.8 Canonical application

The canonical surface form for function application is:

```pbs
callee apply arg
```

Rules:

- `apply` is an infix operator that is right-associative.
- `f1 apply f2 apply x` is defined as `f1 apply (f2 apply x)`.
- `f1 apply f2 apply f3 apply params` is defined as `f1 apply (f2 apply (f3 apply params))`.
- The left operand of `apply` must resolve to one of: a callable candidate set, a bound struct method target, a bound service method target, a contract-method target, or a callback value.
- The right operand of `apply` is an argument expression.
- If the callable input arity is `0`, the argument expression must be `()`.
- If the callable input arity is `1`, the argument expression is checked against the carrier type of the single input slot.
- If the callable input arity is `2..6`, the argument expression must have a named tuple shape with matching arity and positional types.
- Input labels are not used for compatibility.
- No single-slot tuple argument literal is required or recognized in surface syntax.
- There is no partial application in v1 core.
- There is no currying in v1 core.
- Chained `apply` is nested ordinary application, not callable composition as a first-class value.
- Callback values, service methods, host methods, struct methods, and contract-method targets use the same `apply` rules as top-level `fn`.

### 3.9 Call sugar

The surface form:

```pbs
callee(arg1, arg2, ..., argN)
```

desugars to the canonical `apply` surface according to arity.

Rules:

- The desugaring is purely syntactic.
- `f()` is exact sugar for `f apply ()`.
- `f(x)` is exact sugar for `f apply x`.
- `f(x1, x2, ..., xn)` for `n >= 2` is exact sugar for `f apply (x1, x2, ..., xn)`.
- No semantic distinction exists between direct call sugar and its canonical `apply` form.
- When `(arg1, ..., argN)` is used as positional tuple sugar, the callee input tuple shape supplies the effective labels.
- All overload resolution, diagnostics, and type checking are defined on the canonical `apply` form.

### 3.10 Result type of application

Rules:

- If the selected callable output arity is `0`, the result of `apply` is unit.
- If the selected callable output arity is `1`, the result of `apply` is the carrier type of the single output slot.
- If the selected callable output arity is `2..6`, the result of `apply` has the named output tuple shape of the selected callable.
- Multi-slot output tuple results expose their labels for member projection.
- If the selected callable is a callback value, the visible multi-slot output labels come from the callback type rather than from the original source `fn`.
- If the selected callable returns `()`, the application result is unit.

Example:

```pbs
fn func(a: int, b: int) -> (c: int, d: float) {
  return (c: a + b, d: 2.0);
}

fn demo_apply() -> int {
  let params: (a: int, b: int) = (1, 2);
  let r = func apply params;
  let c = r.c;
  let d = r.d;
  let _ = d;
  return c;
}
```

In the example above:

- `func` has input tuple shape `(a: int, b: int)`,
- `func` has output tuple shape `(c: int, d: float)`,
- `r` has named output tuple type `(c: int, d: float)`,
- `r.c` has type `int`,
- `r.d` has type `float`.

Single-slot example:

```pbs
fn plus_one(x: int) -> int {
  return x + 1;
}

fn demo_single() -> void {
  let r = plus_one apply 1;
  if r == 2 {
  }
}
```

In the example above:

- `plus_one` has input tuple shape `(x: int)`,
- the argument `1` is accepted directly as the carrier value for the single input slot,
- `plus_one` has output tuple shape `(value: int)`,
- the value produced by `plus_one apply 1` has carrier type `int`,
- `r.value` is not required and should not be used.

### 3.11 Overload resolution

Rules:

- Overload resolution starts from the visible callable candidates with the selected name.
- Candidate filtering first uses callable kind and input tuple arity.
- Remaining candidates are filtered by positional input type compatibility.
- If exactly one candidate remains, resolution succeeds.
- If multiple candidates remain, expected output types or expected multi-slot output tuple shapes may be used as a tie-breaker when statically available.
- If multiple candidates still remain, the `apply` is ambiguous and compilation fails.
- If no candidate remains, the `apply` is unresolved and compilation fails.
- Overloads that differ only by labels are duplicates and are forbidden.
- Overloads that differ only by output positional types are permitted, but uncontextualized `apply` sites may become ambiguous.

### 3.12 Member access and projection

Rules:

- `TypeName.case` is valid when `TypeName` resolves to a declared enum type and `case` resolves to one of its declared enum cases.
- `TypeName.case` has static type `TypeName`.
- `expr.name` is valid when the static type of `expr` is a declared `struct` containing field `name` and the access site is permitted to read that field.
- For `struct` field access, the projected member type is the declared field type.
- Reads of a private struct field are valid only through `this.name` inside methods and `ctor` bodies of the enclosing struct.
- `expr.method` is a valid method-call target when the static type of `expr` is a concrete struct type declaring method `method`.
- `expr.method` over a concrete struct receiver does not search visible contract implementations.
- `expr.method` is a valid method-call target when the static type of `expr` is a concrete service type declaring method `method`.
- `expr.method` over a concrete service receiver does not search visible contract implementations.
- `HostName.method` is a valid method-call target when `HostName` resolves to a visible declared host owner whose body declares method `method`.
- `TypeName.ctorName` is not a general member access surface; named constructors are entered only through `new TypeName.ctorName(...)`.
- `expr.method` is a valid method-call target when the static type of `expr` is a contract value whose contract declares method `method`.
- Bare extraction of a struct, service, host, or contract method as a value is invalid in v1 core because methods are not first-class.
- `expr.name` is valid when the static type of `expr` is a multi-slot named output tuple containing label `name`.
- For named output tuples, the projected member type is the type of the corresponding output slot.
- Projection is label-based, not position-based.
- `expr.hasSome()` and `expr.hasNone()` are valid intrinsic method-call surfaces when the static type of `expr` is `optional<P>`.
- `expr.hasSome()` and `expr.hasNone()` both have static type `bool`.
- `expr.name()` and `expr.key()` are valid intrinsic method-call surfaces when the static type of `expr` is an enum type.
- `expr.name()` has static type `str`.
- `expr.key()` has static type `int`.
- Access to a missing output label is a compile-time error.
- Access to a missing struct field is a compile-time error.
- Read access to an inaccessible private struct field is a compile-time error.
- Write access to an inaccessible or non-`pub mut` struct field is a compile-time error.
- Access to a missing struct method is a compile-time error.
- Access to a missing service method is a compile-time error.
- Access to a missing host method is a compile-time error.
- Access to a missing contract method is a compile-time error.
- Member projection is not defined for single-slot collapsed carrier values.

### 3.13 Block expressions and function fallthrough

Rules:

- A block expression with a `TailExpr` has the static type of that final expression.
- A block expression without a `TailExpr` has static type unit.
- Only the final unsemicoloned expression in a block contributes to the block result.
- A function body does not implicitly return its trailing `TailExpr`; explicit `return` and ordinary control-flow rules still apply.
- Reaching the end of a plain non-unit function is a compile-time error unless all control-flow paths are proven to return explicitly.
- Reaching the end of a `void` or `()` function is valid and yields unit.
- Reaching the end of an `optional P` function yields `none`.
- Reaching the end of a `result<E>` function is a compile-time error.

### 3.14 Loop forms

Rules:

- `while cond { ... }` requires `cond` to have static type `bool`.
- `for i: T from start until end { ... }` is the declarative counted loop form in v1 core.
- `for i: T from start until end step s { ... }` is the explicit-step counted loop form in v1 core.
- In `for`, the declared iteration variable `i` introduces a loop-local binding of type `T`.
- `start`, `end`, and `step` expressions in `for` must be type-compatible with the declared iteration type `T`.
- If `step` is omitted, the loop uses the integer value `1` of the iteration type domain.
- `for` iteration proceeds by evaluating `start`, `end`, and optional `step` once before loop entry.
- `for ... until ...` uses an exclusive upper bound.
- `continue` inside `while` transfers control to the next condition check.
- `continue` inside `for` transfers control to the step update and then to the next bound check.
- `break` exits the nearest enclosing loop.

### 3.15 `if` and `switch` conditional expressions

Rules:

- In `if cond { a } else { b }`, `cond` must have static type `bool`.
- Only the selected branch is evaluated at runtime.
- The branch expressions `a` and `b` must have the same static type, subject only to ordinary contextual typing already defined elsewhere in the language.
- The static result type of the `if` expression is that shared static type.
- In `switch selector { pattern: { ... }, ... }`, the selector expression is evaluated once.
- `switch` accepts enum selectors and literal-comparable scalar selectors; `error` selectors are invalid.
- Each non-wildcard `switch` arm pattern must be unique within the same `switch`.
- Each non-wildcard `switch` arm pattern must be type-compatible with the selector expression.
- Enum-case switch patterns must resolve to declared cases of the selector's enum type.
- Error labels are not valid switch patterns.
- `default` and `_` are equivalent wildcard spellings for `switch`.
- At most one wildcard arm may appear in a `switch`.
- A `switch` must not mix `default` and `_` in the same arm set.
- The blocks of all `switch` arms must have the same static type, subject only to ordinary contextual typing already defined elsewhere in the language.
- The static result type of the `switch` expression is that shared static type.
- A `switch` used as an `ExprStmt` is valid when the selected arm blocks evaluate to unit.
- A `switch` expression used in a value-required position must be exhaustive, either by a wildcard arm or by another statically proven exhaustive case set.

### 3.16 `optional` construction and extraction

Rules:

- `some(expr)` forms an `optional<P>` value where `P` is the static type of `expr`, unless an expected `optional<Q>` context is present and constrains `expr` to be compatible with `Q`.
- `some(expr)` is invalid when the payload normalizes to `void`.
- `none` is valid only when an expected `optional<P>` type is available from context.
- `opt else fallback` requires the left operand to have static type `optional<P>`.
- In `opt else fallback`, the `fallback` expression must be compatible with payload shape `P`.
- The static result type of `opt else fallback` is the carrier value type for single-slot payloads and the named tuple payload shape for multi-slot payloads.
- `opt else fallback` does not introduce implicit mutation or unwrapping side effects beyond normal expression evaluation.

### 3.17 `result<E>` return flow and handling

Rules:

- `return ok(expr);` is valid only inside a function whose declared return surface is `result<E> P`.
- In `return ok(expr);`, `expr` must be compatible with the declared success payload shape `P`.
- `return err(E.label);` is valid only inside a function whose declared return surface is `result<E> P`.
- In `return err(E.label);`, the error path must resolve to a declared case of the same error type `E`.
- `ok(...)` and `err(...)` do not denote ordinary value expressions in v1 core.
- `expr!` requires `expr` to have static type `result<E> P`.
- `expr!` is valid only when the enclosing function returns `result<E> Q` for the same error type `E`.
- The static result type of `expr!` is the extracted success payload shape `P`, collapsed to its carrier value when single-slot.
- `handle expr { ... }` requires `expr` to have static type `result<E1> P`.
- `handle expr { ... }` is valid only when the enclosing function returns `result<E2> Q` for some payload `Q`.
- Each non-wildcard `handle` arm must match a distinct declared case of `E1`.
- Each mapped error path on the right side of a `handle` arm must resolve to a declared case of `E2`.
- `handle` arms must be exhaustive over `E1`, either by naming all cases exactly once or by providing `_`.
- The static result type of `handle expr { ... }` is the extracted success payload shape `P`, collapsed to its carrier value when single-slot.
- On error, `handle` performs an immediate enclosing-function return with the mapped `err(...)`.

### 3.18 Required static diagnostics

At minimum, deterministic static diagnostics are required for:

- duplicate parameter names in `fn` declarations,
- duplicate output labels in named tuple returns,
- duplicate error case labels in `declare error`,
- duplicate enum case labels in `declare enum`,
- duplicate enum case identifiers in `declare enum`,
- invalid mixed implicit/explicit enum case identifiers,
- invalid `this` usage outside struct method, service method, or `ctor` body,
- invalid `Self` type usage outside struct method, service method, or `ctor` declarations,
- invalid struct method declaration shape,
- invalid service method declaration shape,
- invalid host declaration shape,
- invalid host method declaration shape,
- invalid attribute surface,
- invalid `Host` attribute target,
- duplicate `Host` attribute on one host method,
- missing required `Host` attribute on a reserved host method,
- malformed `Host(module=..., name=..., version=...)` argument set,
- invalid empty `Host.module` or `Host.name`,
- invalid non-positive `Host.version`,
- invalid `ctor` declaration shape,
- invalid `return` inside `ctor`,
- incomplete field initialization on a completing `ctor` path,
- duplicate `implements Contract for Owner` pair,
- `implements` declared outside the owner module of the struct or service,
- incompatible or missing contract method implementation,
- invalid contract coercion from concrete struct or service value,
- unresolved barrel function signature after label-insensitive matching,
- unresolved host barrel entry,
- unresolved callback barrel entry,
- invalid enum case path,
- invalid enum intrinsic member call,
- invalid named constructor target,
- unresolved named constructor overload,
- ambiguous named constructor overload,
- incompatible top-level `fn` assignment to callback type,
- ambiguous overloaded top-level `fn` assignment to callback type,
- attempted assignment of service method to callback type,
- attempted assignment of host method to callback type,
- use of `bind(...)` without an expected callback type,
- incompatible `bind(...)` context type for callback target,
- ambiguous overloaded top-level `fn` target in `bind(...)`,
- `apply` on a non-callable target,
- arity mismatch in `apply`,
- argument type mismatch in `apply`,
- `apply` chain with incompatible intermediate carrier/tuple shape,
- ambiguous overload resolution,
- unresolved callable application,
- possible fallthrough of plain non-unit function,
- non-boolean `while` condition,
- invalid `for` iteration type,
- incompatible `for` bound or step type,
- non-boolean `if` expression condition,
- incompatible `if` expression branch types,
- duplicate `switch` arm pattern,
- mixed `default` and `_` wildcard arms in `switch`,
- invalid `switch` selector type,
- selector-pattern type mismatch in `switch`,
- invalid enum case switch pattern,
- incompatible `switch` arm block types,
- non-exhaustive `switch` expression in value position,
- invalid mixed `optional`/`result` return surface,
- invalid payload-less `optional` type surface,
- invalid `optional void` type surface,
- missing explicit type annotation on `declare const`,
- non-constant `declare const` initializer,
- incompatible `declare const` initializer type,
- cyclic dependency among `declare const` declarations,
- unresolved referenced `declare const` in constant evaluation,
- invalid `none` usage without expected optional type,
- invalid `else` extraction over non-optional operand,
- fallback type mismatch in `else` extraction,
- invalid `some(...)` construction form,
- use of `ok(...)` or `err(...)` outside `return`,
- invalid `ok(...)` construction form,
- invalid `err(...)` construction form,
- invalid error label in `err(...)`,
- invalid `!` propagation on non-result expression,
- mismatched error type in `!` propagation,
- invalid `handle` on non-result expression,
- non-exhaustive `handle` mapping,
- duplicate `handle` mapping arm,
- invalid mapped error label in `handle`,
- attempted use of a single-slot tuple literal where no such surface form exists,
- member access on a missing struct field,
- read access to an inaccessible private struct field,
- write access to an inaccessible or non-`pub mut` struct field,
- member access on a missing struct method,
- member access on a missing service method,
- member access on a missing host method,
- member access on a missing contract method,
- bare method extraction from a struct, service, host, or contract value,
- member projection on a single-slot carrier value,
- invalid optional intrinsic member call,
- member projection on a missing named output label.