← Spec review

D — VibeLang has a serious runtime design, but its language rules make evaluation strategy depend on types and spelling, contradict their own preservation guarantees, and admit demonstrable requirement unsoundness.

Reviewer: astra. Reviewed 2026-10-27. Scope: all 33 files in `spec/design/src/`, including both appendix files, and all of `spec/design/DECISIONS.md`. Implementation checks used only the supplied probe harness and this reviewer's probe directory. No other panel reports were consulted.

The central diagnosis is architectural: the document specifies a continuation machine more carefully than it specifies the source language that feeds that machine. A correct continuation kernel cannot repair an elaboration that changes binding, evaluation, or completion semantics.

The grade is for the specification, not a count of compiler bugs. Chapter 13 already requires left-to-right, once-only evaluation and short-circuiting; a compiler that evaluates an operand twice or tests an Effect object instead of its success value violates that requirement. Conversely, ignoring a shadowing pattern binding and copying inline-module exports are specified behavior. They require language changes, not merely implementation repairs.

## The call-semantics inventory and proposed minimal design

### Inventory

“Today” below means the written specification, including amendments in DECISIONS.md. Several rows overlap: that overlap is itself the design problem. There are not twenty independent machine instructions; there are twenty routes by which the checker chooses an evaluation strategy.

| Semantics | How it is dispatched today | How it should be dispatched | Programs that change |
| --- | --- | --- | --- |
| Vibe function invocation | Callee provenance, inferred control class, annotation, and availability of a direct implementation; Chapter 13/D10/D67 | One computational call operation in a computational region; direct code is an implementation of that operation | Adding or removing a plain return annotation no longer changes public ABI |
| Foreign function returning Effect | Instantiated result type must be Effect itself, D24 | Explicit foreign-Effect adapter at the import/boundary; thereafter the uniform computational call | Raw foreign imports need one adapter; widening a result type no longer changes execution |
| Foreign call returning Config, Exit, key, or TaggedError | A structured subtype of Effect is returned as data, despite being executable; D24 | Native call or a value-returning computational adapter; execution requires explicit `run` | Code relying on the exact-Effect/subtype distinction must state whether to execute |
| Calling an Effect value, `p()` | The callee's type is noncallable Effect/yieldable data | Explicit `run p` | `p()` becomes `run p`; a data object is no longer made callable by its type |
| Service lookup, `S()` | Callee resolves to a service key; some namespace names acquire that meaning through D311 | Explicit `use S`; method shorthand may desugar to this syntax after symbol resolution | Bare service calls change spelling; requirements still infer |
| Service member call, `S.m(a)` | Resolved key, member type, and whether member is a function or an Effect value; plain members are trusted | Explicit `(use S).m(a)` followed by the uniform call; Effect-valued members use explicit `run` | `S.m(a)` becomes `(use S).m(a)`; Effect-valued members need explicit execution |
| Control operation | Resolved operation type; nearest handler on current fiber | A control declaration emits a callable with the single computational ABI; its body performs handler lookup | No need to remove direct-style handling; aliases must retain operation identity |
| Trusted native call | Built-in/package provenance or `@vibelang trusted`; listed exception classes change E | Explicit native adapter carrying its exception policy; trust is a property of that adapter | Untagged aliases and declaration packaging no longer change call behavior |
| Untrusted native call inside a plain-annotated function | Explicit/contextual plain contract bypasses the trust boundary; D282 | Native region selected syntactically | Merely adding `: A` cannot enable arbitrary foreign calls |
| By-name argument, array element, record field | Expected declared parameter/field type, before instantiation; D147/D265; entire expression repeats per run | Explicit `defer { ... }`, including collection elements | `retry(work(), p)` becomes `retry(defer { work() }, p)` |
| Held program initializer | A declared Effect-typed `const` or field suppresses running its outer initializer; D262/D269 | Explicit program construction; an annotation only checks it | Removing a type annotation cannot turn stored work into immediate work |
| Eager Effect factory | Explicit Effect contract plus a returned program not assignable to A; D269 | Explicit native factory/adaptor or explicit program construction | Widening A to `unknown` cannot change factory/body staging |
| Inline callback / named callback type | An inline function type gains E/R polymorphism; an equivalent named alias stays plain; D12 | Explicit computational versus native function kind, preserved through aliases | Factoring a type into an alias has no runtime or acceptance effect |
| Lambda converted into Effect function, plain function, or program | Expected type of an overload candidate; no-parameter lambdas may become programs; D7/D44/D56 | Function literals remain functions; explicit `defer` creates programs; native lambda syntax creates native callbacks | Overload order cannot turn the same literal into a different runtime representation |
| Function-or-Effect union and overload competition | Eligibility, candidate order, and D257 preference for by-name programs | Overload resolution checks already elaborated argument forms | Some ambiguous calls need explicit adapters or `defer` |
| `sync`, `try`, `callback` | First argument is a native-language region, other arguments Vibe; result type/declaration chooses Promise handling; D148/D229–232 | Explicit native boundary with explicit sync/async/callback mode and fixed argument positions | Promise-like return inference and optional parameter types no longer decide signal injection |
| A hatch used through an alias or from TypeScript | Runtime inspects values/function declaration; cannot reproduce direct-hatch type tests; D231/D232 | First-class adapter with the same ABI and policy as direct syntax | Direct and aliased hatches become equivalent |
| `trusted` and trusted contracts | Declaration/body category plus exception metadata | Explicit adapter construction once; ordinary calls subsequently uniform | No per-call recognition by spelling |
| Topic pipe | Expected type of every `%` determines eager value versus deferred left expression; mixed uses rejected; D155 | Pipe evaluates left once; explicitly pipe a `defer` value to operate on a program | Retry pipes need explicit quotation |
| `pipe(...)`, `.pipe(...)`, curried pipe stages | Recognized pipe helper, first-stage signature, actual member, and D272 syntactic fast-path restrictions | Ordinary native/value pipe operation; syntax desugaring preserves the same strict evaluation | Refactoring the left operand or stage cannot change what gets executed |
| Extension methods on Effect data | Receiver type's module, absence of real member, export name, first parameter named `self`/`*OrOptions` or D295 table | Explicit extension metadata on resolved exports, or explicit module call | Renaming a library parameter cannot remove a language feature |
| Block after a call | Append-last ordinarily; Effect dual data-first/data-last candidates take priority; D188 | Fixed syntactic argument position, with explicit adapters for dual APIs | Some `Layer.effect(S) { ... }`/dual forms require a documented fixed expansion |
| Methods and constructors | Methods become Effect based on body/context; some plain annotations remain plain; `new` never executes an Effect | Method invocation uses the chosen region's uniform call; `new` retains a distinct native construction operation | Methods cannot change ABI merely because their body begins suspending |
| Tagged templates | D267 applies call classification to the tag, with native template identity and receiver obligations | Region's call operation; fixed template evaluation rule | Type context cannot silently quote or execute tag results |
| Producers and JS generators | Unannotated/Stream-annotated `function*` is a producer; explicit iterator annotation preserves JS generator, D271; direct/Stream consumption differs | Distinct producer syntax and native generator syntax; explicit Stream adapter | Changing only a return annotation cannot replace the iterator protocol |
| Runners and generated entry calls | Resolved runners check R; D135 also suppresses entry on any top-level function named `runSync`, etc. | Explicit entry declaration and resolved runner symbols | Unrelated same-named functions cannot disable main |
| TypeScript calling Vibe/generated wrapper | Effect ABI except plain annotations/factories; direct metadata absent across declarations | One stable exported computational ABI, explicit native exports | Source-based and declaration-based consumers share behavior; optimization availability differs only in cost |

### Minimal design: two invocation modes, with explicit program construction

Keep the useful goal: inside computational code, `const user = find(id)` reads directly and runs on the current fiber. Keep Effect as the external representation. Remove the rule that a type annotation selects an evaluation strategy.

1. **Computational invocation C.** Every callable admitted into a computational region has one language ABI: invoke it with strictly evaluated arguments and obtain its success value on the current fiber. It may suspend, fail, or request services. Pure functions use the same abstract operation; a direct implementation must preserve its observations. A foreign function becomes such a callable through a declared adapter, not through the inferred type of an individual call.
2. **Native invocation N.** Calls inside explicitly native syntax use ECMAScript invocation and return their JavaScript value, including an inert Effect object. Existing hatches can provide this syntax. Sync, Promise, and callback adapters state their exception/cancellation policy explicitly; they do not inspect overloads to decide it.

These are two call semantics, not one call semantic per return type. Native constructors remain ECMAScript `new`. A function/operation's resolved binding identifies what is invoked; it does not make the compiler choose between evaluation strategies.

Two explicit operations separate values from computations: `defer { statements; result }` creates a cold program; `run p` executes a program value. `use S` projects a service. These spellings are proposed syntax, not claims about the current parser. A lambda stays a function. An Effect annotation checks a value; it never inserts `defer`, `run`, or a new function representation.

At the TypeScript boundary, an exported computational function returns `Effect<A,E,R>`. Calling this factory captures the supplied receiver and raw argument values; executing its Effect initializes the source activation and runs its body. A separate explicitly native export is an ordinary TypeScript function. No body inference changes that ABI.

There is an unavoidable choice: syntax-directed call semantics and unrestricted automatic raw-TypeScript interoperation cannot both survive unchanged. A small explicit adapter layer is the cost of keeping direct style without making the checker a staging interpreter. Prelude adapters can be supplied by the language. This is a **LANGUAGE CHANGE**, including migrations listed above; pretending otherwise would repeat the specification's current problem.

## Findings, ranked

### 1. BLOCKER — Optional service brands do not preserve requirement identity

**Location and rule.** Chapter 4, “Declaring a service,” D45:

> “The optional brand keeps two services with the same methods distinct in R.”

The emitted interface contains:

> `readonly "~vibelang/service"?: "@acme/app/src/users#Users"`

**Falsifiable claim.** An ordinary structural intermediate type erases that identity and allows an Alpha requirement to be retyped as Beta without a cast or `any`. Providing Beta then type-checks while Alpha is missing.

**Confirmed probe.** [service_brand/src/main.vibe](probes/service_brand/src/main.vibe), [result](probes/service_brand/result.log):

```ts
service Alpha { get(): number!! }
service Beta  { get(): number!! }
type Shape = { get(): number!! }

function useAlpha() { return Alpha.get() }
const erased: Effect.Effect<number, never, Shape> = () => useAlpha()
const claimed: Effect.Effect<number, never, Beta> = erased

export function main() {
  provide Beta = { get(): number!! { return 7 } } {
    Console.log(claimed())
  }
}
```

Compilation exits 0, with spelling warnings only. Execution exits 1: `Service not found: service_brand/src/main#Alpha`. The emitted code provides Beta and executes an Effect that looks up Alpha.

**First principles and prior art.** Nominality requires an unforgeable required identity in the requirement type. A discriminator that can be omitted distinguishes some pairs of already-branded values, but does not prevent structural widening and reassignment. TypeScript explicitly uses structural compatibility; the language must introduce stronger identity where it promises stronger guarantees. [TypeScript compatibility](https://www.typescriptlang.org/docs/handbook/type-compatibility.html). Effect's separation between service identifier and implementation shape is precisely the separation D45 discards; Chapter 4's “service of any shape” form already retains it.

**Exact replacement rule.**

> A service declaration creates a nominal identifier type and a separate structural implementation type. Only the nominal identifier occurs in R, Layer outputs, and provider subtraction. It contains a required compiler-private unique identity that survives declaration emit and cannot be satisfied by the implementation shape. `Service.Shape<typeof S>` denotes the implementation shape. `implements S`, if retained as sugar, checks that shape and does not make the implementation an identifier. Assignments through a structural type cannot establish a service requirement identity.

**LANGUAGE CHANGE: YES.** Structural service-interface types can no longer substitute for requirement identifiers. Ordinary object implementations remain accepted through the shape check. Confidence: certain, reproduced.

### 2. BLOCKER — Contextual typing selects when work happens and what a value is

**Location and rule.** Chapter 13, “One syntax, several meanings” and “How program values are spelled”:

> “A call is always written `f(x)`; what it compiles to depends on what `f` is, decided from the types:”

> “A call runs where it stands, except where the expected type is `Effect`:”

D269 further selects eager factories when a returned program would not be assignable to A. Chapter 16, “A callback type without a contract accepts any contract”:

> “only a function type written in place gains a contract, so a named one keeps TypeScript's meaning and takes plain functions.”

**Falsifiable claim.** Adding an annotation, widening a success type, changing an overload order, or factoring a callback type into an alias can change evaluation time, repeat count, runtime representation, or whether a callback may suspend. This is not erased typing. It is an implicit, nonlocal staging language.

A by-name `retry(work(), policy)` repeats the receiver lookup and argument expression as well as the operation. A declared Effect-typed `const p = factory(input)` captures one factory result. An unannotated binding can execute it immediately. These are three distinct evaluation strategies behind ordinary-looking declarations/calls. The spec states them; the compiler did not invent them.

**First principles and prior art.** Type-directed elaboration is not inherently invalid. It needs a coherent target term and an explicit account of when distinct derivations may differ. Here the document treats these changes as familiar TypeScript contextual typing. TypeScript's checker selects signatures and contextual types; it does not thereby turn a function literal into a computation object or defer an argument's side effects. Its actual overload machinery also reorders specialized candidates, so “declaration order” is not an adequate complete model. [TypeScript checker, reorderCandidates/chooseOverload](https://raw.githubusercontent.com/microsoft/TypeScript/v5.9.3/src/compiler/checker.ts).

Eff separates expressions, computations, and handlers in its core calculus even where its surface syntax makes them convenient to mix. That is the missing semantic boundary here. [Bauer and Pretnar, §§1–3](https://math.andrej.com/wp-content/uploads/2012/03/eff.pdf).

**Exact replacement rule.**

> Elaboration inserts computation construction and execution only for explicit language syntax. The call operation is determined by the enclosing syntactic region. Expected types and overload selection check the already selected operation; they cannot change whether an operand is evaluated, deferred, repeated, or converted from a function to an Effect. Type aliases preserve function kind. Return annotations do not change a function's execution phase or public ABI.

Apply the C/N design and explicit `defer`/`run` above. If the project refuses this change, it must instead specify a complete contextual-elaboration calculus, including a single overload priority relation and all staging boundaries. The present prose is not such a calculus.

**LANGUAGE CHANGE: YES.** This is the largest migration and the largest reduction in compiler complexity. Confidence: certain from normative rules.

### 3. BLOCKER — Pattern semantics deliberately ignore lexical binding

**Location and rule.** Chapter 1, prelude:

> “An import or local declaration with the same name shadows a prelude name, as it shadows any global.”

Chapter 29, D208:

> “a shadowing local is not consulted”

Chapter 13's extension-method rule also examines whether a parameter is named `self`, ends in `OrOptions`, or appears in D295's table. D135 suppresses entry generation for:

> “any call of a function named `runMain`, `runPromise`, `runFork`, `runSync`, or `runCallback`”

**Confirmed probe.** [pattern_shadow](probes/pattern_shadow/src/main.vibe) defines identical predicates named `Number` and `StringMatcher`, both testing for a string. For `"text"`, `[x is Number, x is StringMatcher]` prints `[ false, true ]`. [Result](probes/pattern_shadow/result.log). Renaming the local predicate changes the answer.

**First principles and prior art.** This violates alpha-equivalence: consistently renaming a bound variable changes the program's meaning. A built-in pattern can be reserved syntax, or a distinguished resolved binding. It cannot simultaneously promise ordinary shadowing and ignore the shadow. Scheme's hygienic transformation rules distinguish identifiers by their binding context and protect inserted free references. [R7RS §4.3](https://small.r7rs.org/attachment/r7rs.pdf).

D311's same-named-export convenience is also explicitly restricted to modules reached under their own names. Therefore aliases need a specified policy; a textual local name cannot identify the original module export. D313, by contrast, correctly says a local `Experimental` shadows the prelude namespace. Implementations that ignore that shadow violate D313; the spec does not authorize that bug.

**Exact replacement rule.**

> All identifier-based language facilities are recognized from resolved symbol identity. Prelude bindings obey ordinary lexical shadowing and retain their identity through aliases and re-exports. A built-in matcher is selected only when its identifier resolves to that matcher. An unrelated same-spelled declaration has no built-in behavior. Runner recognition uses a resolved runner identity. Extension-method eligibility is declared metadata on the resolved export, never a parameter's spelling. Same-named-export shorthand uses the module's original export identity after resolution and behaves identically through aliases.

**LANGUAGE CHANGE: YES.** Shadowing built-in matcher names begins working; unrelated runner names cease suppressing entry; parameter renaming ceases affecting extension availability. Confidence: certain; pattern case reproduced.

### 4. BLOCKER — Plain `finally` has a different completion algebra

**Location and rule.** Chapter 15, “Regions inside a plain function”:

> “they compile to JavaScript's own statements. Nothing inside can pause or be interrupted, so JavaScript's semantics match the machine's.”

Chapter 17, rules:

> “A failure during cleanup is never dropped. It is added to the cause being reported”

**Confirmed probe.** [plain_finally](probes/plain_finally/src/main.vibe) catches the result of `try { throw "body" } finally { throw "cleanup" }` in a plain function and returns `"cleanup"`. [frame_finally](probes/frame_finally/src/main.vibe), with an Effect sleep in the protected body, returns `"body"` to the outer catch. Both compile and run successfully. This is the expected distinction between replacing an abrupt completion and combining Causes.

**First principles and prior art.** Suspension is irrelevant to this counterexample. ECMAScript's `finally` evaluation replaces the prior completion when the finalizer completes abruptly. Effect finalization composes failure information. Proving “cannot suspend” does not prove equality of these completion algebras. [ECMAScript TryStatement evaluation](https://tc39.es/ecma262/multipage/ecmascript-language-statements-and-declarations.html#sec-try-statement-runtime-semantics-evaluation), [Effect Cause combination](https://effect.website/docs/v4/data-types/cause).

**Exact replacement rule.**

> Every VibeLang try/finally, including one in a function eligible for direct execution, uses the same completion-combination operation. If cleanup succeeds, preserve the incoming completion. If cleanup fails and the incoming completion is successful or a nonfailure transfer, propagate cleanup's cause. If both fail, retain both causes in body-then-cleanup order and apply the pinned defect-precedence rule. An optimization may use JavaScript finally only if it proves cleanup cannot complete abruptly or explicitly implements this combination. Typed catch subsequently applies Chapter 17's recovery rule to that combined cause.

Keep ECMAScript replacement behavior only inside explicit native hatches.

**LANGUAGE CHANGE: YES relative to Chapter 15; restoration of Chapter 17's intended guarantee.** Confidence: certain, reproduced. This is a compiler-101 counterexample to the stated optimization proof.

### 5. BLOCKER — Inline modules export snapshots while promising TypeScript modules

**Location and rule.** Chapter 10, “Code that is not Effect,” D283/D303. D303 specifies:

> “An import from the module becomes constants destructured from the object”

and admits:

> “a later assignment to an exported `let` is not seen”

It also evaluates the inline module after all ordinary imports rather than in import order, and treats module names differing only in case as the same name.

**Confirmed probe.** [module_live](probes/module_live/src/main.vibe) declares an inline module exporting `count = 0`, `bump()`, and `read()`. After `bump()`, logging the imported count and `read()` produces `[ 0, 1 ]`. [Result](probes/module_live/result.log). A live import produces `[ 1, 1 ]`.

**First principles and prior art.** A module import denotes a binding, not a sampled value. A frozen object is not an ECMAScript module namespace. Destructuring destroys indirection; moving imports changes initialization and failure order. Loader inconvenience is not a semantic justification. [ECMAScript Module Environment Records / CreateImportBinding](https://tc39.es/ecma262/multipage/executable-code-and-execution-contexts.html#sec-module-environment-records).

**Exact replacement rule.**

> A source module declaration has module binding semantics. Every import and re-export reads the current target binding; assignment to an exported mutable binding is visible to all importers. Initialization, temporal dead zones, cycles, and dependency evaluation order follow the module dependency graph. Inlining may represent bindings by cells or namespace accessors, but may not snapshot them. Source module names are case-sensitive regardless of temporary-file naming. Unsupported module graphs are diagnosed rather than assigned different semantics.

**LANGUAGE CHANGE: YES.** Programs depending on snapshots or reordered initialization change. Ordinary external imports already have the intended rule; extend it consistently. Confidence: certain, reproduced.

### 6. BLOCKER — The specification explicitly permits a continuation to return outside its type

**Location and rule.** Chapter 9, “The full API,” in the `handle(program,...)` discussion, D97; Chapter 28, EK2119:

> “a `resume` still waiting can receive a value outside its type”

Chapter 9 explains:

> “a clause's return computed from it stays out of its type”

The diagnostic is only a warning because inference would require a fixpoint.

**Falsifiable claim.** If the stated rule is implemented literally, a well-typed resumption can return a value not inhabiting its assigned answer type. That directly violates type preservation; a warning does not repair it. The runtime needs the answer type of the entire deep handler, including later clauses and return transformation.

**Evidence boundary.** The specification itself states the unsound outcome. My attempted simpler numerical-resume probe was rejected with TS2322 because its answer was correctly inferred as `string | number`; see [resume_result](probes/resume_result/result.log). I do not claim that this attempted counterexample demonstrates an implementation hole. The normative permission remains unacceptable independently.

**First principles and prior art.** A deep resumption returns the handler's answer, not necessarily the performed operation's result or the original program's result. Eff gives handlers an input-to-output computation type; OCaml gives a continuation separate argument and answer parameters. [Eff §3](https://math.andrej.com/wp-content/uploads/2012/03/eff.pdf), [OCaml effect handlers](https://ocaml.org/manual/5.3/effects.html).

**Exact replacement rule.**

> A handler has one answer type H. Every normal body return after onReturn, every clause return, and every resumed continuation result must be compatible with H. A continuation for an operation returning V has resumption type V -> H. Infer a sound H from all those constraints. If recursive constraints cannot be resolved, require an explicit H and check every branch against it. A clause that can produce a value outside H is an error; no warning or inference omission licenses it.

**LANGUAGE CHANGE: YES.** Programs accepted only under EK2119 must add a sound answer annotation or fail checking. Confidence: certain about the specification defect; runtime reproduction not obtained.

### 7. BLOCKER — `using` specifies double disposal and leaves an acquisition leak open

**Location and rule.** Chapter 6, “`using`”:

> “If its Effect release already disposes it, this disposes it twice (D94).”

For AsyncDisposable, the implicit disposal is instead omitted if acquisition registered its own release. DECISIONS.md D25:

> “the value never reaches `using`, so a Disposable made there is not released”

The decision ends:

> “Open.”

**Falsifiable claim.** A legal acquisition can be disposed twice; another can escape disposal when pending interruption is delivered between acquisition and implicit registration. Whether an acquisition registered some finalizer does not establish which value that finalizer owns. Sync and async disposables have different ownership policies.

**First principles and prior art.** Resource safety requires one explicit owner and atomic transfer from successful acquisition to registered release. “There is a finalizer” is not proof of ownership of this result. Effect's acquisition/release abstraction makes registration part of the acquisition protocol. [Effect resource management](https://effect.website/docs/v4/resource-management/introduction). A blanket uninterruptible acquisition is not an adequate fix: it can make a cancellable network wait uncancellable, which D25 correctly notices.

**Exact replacement rule.**

> Resource ownership is explicit. A scoped Effect acquisition owns its registered release; using supplies the lexical Scope and does not add a second disposal action. A plain Disposable/AsyncDisposable initializer is acquired and registered atomically by the language's disposal acquisition primitive. An Effect returning an unregistered Disposable must use an explicit disposal-acquisition adapter, with its masking/interruptibility contract stated; using does not infer ownership from the result's shape or from the number of finalizers registered. Each ownership token releases exactly once. A failed or interrupted acquisition must either transfer ownership to a registered release or release what it acquired before exiting.

**LANGUAGE CHANGE: YES.** Double-disposed acquisitions release once; unregistered Effect-produced disposables require an explicit ownership adapter. Confidence: certain from explicit rules; no new interruption-race probe claimed.

### 8. BLOCKER — Open error families silently weaken exhaustive matching into a defect

**Location and rule.** Chapter 3, “Matching errors and outcomes,” D209:

> “A match without `default` over a finite union must cover every case”

DECISIONS.md D209:

> “Over any other type, an unmatched value throws the proposal's `TypeError`”

D304 makes an extensible error family's tag `string`, not a closed union.

**Confirmed probe.** [open_error](probes/open_error/src/main.vibe) declares abstract `Family`, subclasses `First` and `Second`, and matches a `Family` with only `when First`. It compiles successfully. Passing `new Second()` produces an Exit with a Die reason. [Result](probes/open_error/result.log).

**First principles and prior art.** A finite union and an open class family are different domains. Adding a family abstraction should not turn an exhaustiveness obligation into permission for an implicit runtime crash. This is not, by itself, a proof that E is unsound: E deliberately excludes defects. It is a recovery-coverage hole that converts an omitted domain case into a bug. Rust requires a wildcard for external non-exhaustive enums; Kotlin's exhaustive sealed matching depends on a closed subclass boundary. [Rust non_exhaustive](https://doc.rust-lang.org/reference/attributes/type_system.html#the-non_exhaustive-attribute), [Kotlin sealed classes](https://kotlinlang.org/docs/sealed-classes.html).

**Exact replacement rule.**

> A match without default must be proven exhaustive. For a closed data declaration or explicit finite union, coverage is computed over its variants. An open error family, unknown/any subject, unbounded structural domain, or arbitrary predicate requires a default unless a total arm is proven to cover the whole domain. Known subclasses do not close an open family. Guarded arms do not subtract their pattern's entire type. Explicit partial matching, if provided, must have separate syntax and a documented MatchError outcome.

**LANGUAGE CHANGE: YES.** Previously accepted partial matches over open domains become errors or explicit partial matches. Confidence: certain, reproduced.


### 9. BLOCKER — A first-class hatch does not mean what the direct hatch means

**Location and rule.** Chapter 10, “Code that is not Effect”; DECISIONS.md D231/D232. D231 says:

> “The runtime's `try`, which TypeScript callers and a hatch passed as a value reach, sees only values, so there a function in second place is always the mapper.”

D232 says of a direct hatch's optional parameter:

> “Called as a value, `sync` and `try` still give that parameter the signal: they see no types”

**Confirmed probe.** [hatch_alias](probes/hatch_alias/src/main.vibe) exports this native helper from an inline module:

```ts
export async function f(a: number, b?: number) { return typeof b }
```

Then `sync(f, 1)` returns `"undefined"`, while `const h = sync; h(f, 1)` returns `"object"`. Both compile successfully. [Result](probes/hatch_alias/result.log). The second call receives an AbortSignal in a parameter declared numeric.

**First principles and prior art.** An ordinary alias must preserve a function's behavior. If syntax is intrinsic, expose it as syntax rather than pretending the runtime value is equivalent. Parameter `length`, `async` declaration syntax, and erased TypeScript parameter types cannot jointly define one ABI. ECMAScript invocation passes the chosen argument list; a Promise result does not authorize inventing a signal argument. [ECMAScript EvaluateCall](https://tc39.es/ecma262/multipage/ecmascript-language-expressions.html#sec-evaluatecall).

**Exact replacement rule.**

> A hatch's native adapter has an explicit mode and argument layout. The signal occupies a separately declared slot, never a slot inferred from function length or parameter type. The try mapper occupies a named option or otherwise unambiguous syntactic slot. Direct syntax and its first-class adapter invoke the same operation with the same arguments, exception conversion, awaiting, and cancellation behavior. If a hatch has no first-class equivalent, taking it as a value is an error.

**LANGUAGE CHANGE: YES.** Ambiguous function-input/mapper cases and implicit signal injection require explicit adapters/options. Confidence: certain, reproduced.

### 10. MAJOR — Evaluation order is stated, but staging lacks a complete binding-time contract

**Location and rule.** Chapter 13, “Evaluation order”:

> “Generated code keeps JavaScript's evaluation order. Arguments are evaluated left to right, each once. A receiver is evaluated once and keeps its `this`.”

Chapter 20, “Objects”:

> “A cold, reusable description of a computation. Constructing it runs nothing. Each run creates a new execution with fresh frames.”

Chapter 13/D269 separately specifies eager factory snapshots and held initializers.

**Falsifiable claim.** The first quote correctly determines ordinary strict JavaScript expression order. It does not define which source operations belong to construction, invocation, or execution after contextual quotation, factory recognition, service projection, and wrappers. Two implementers can preserve left-to-right order within each phase and still put a getter/default/factory call in different phases.

The unresolved obligations are concrete:

| Form | Already specified | Missing or insufficiently integrated rule |
| --- | --- | --- |
| Ordinary operators and calls | Left-to-right, once; short-circuit; receiver; getters | Formal lowering must preserve References, not only values, when an operand suspends. This is an implementation obligation under the existing rule, not permission to reorder |
| By-name expression | Entire expression repeats each run, D147 | One authoritative account of nested quotation, held initializers, unions/overloads, and the D269 eager-factory exception |
| Exported function wrapper | Body is cold; EK1001 forbids running Effects in defaults; D274 keeps defaults/destructuring on the generator path | Time of default-parameter evaluation, destructuring/getters, rest/arguments creation, and exceptions during parameter binding; whether they repeat on rerun |
| Service call | Lookup followed by method call in the example | A normative rule placing service lookup/member getter before argument effects, including missing-service failure and optional/computed access |
| `provide` and `wire` | Providers are composed by Layer dependencies | Preserve the already-required expression order/count while sorting the build graph; specify independent-build concurrency; repeated layer identity and memoization in the generated composition |
| `await.*` records/arrays | By-name branches and operator policy | Construction/enumeration with computed keys/spreads and integer keys; “keys keep the order written” versus ECMAScript own-key order; failure during collection construction |
| `for concurrent` | Bounded execution policy | Relative evaluation of bound and iterable, bound validation, iterator acquisition/closing on start failure, and how nonliteral bounds are sampled |
| Patterns | Subject evaluated once; ordered arms; some extractor rules | One algorithm fixing getter/extractor/guard calls and extraction reuse across composite patterns and optimized last arms |
| Tagged templates | D267 preserves site identity and native order | This rule needs incorporation into Chapter 13's core semantics, including suspension between substitutions |
| Native asynchronous inputs | Input expressions are eager, D232 | Separate cold adapter registration from an already-hot Promise; define whether rerunning re-invokes the producer or merely re-awaits the same promise |

An arbitrary value typed Effect is not proof of cold construction or fresh outside-world inputs. It may capture a hot Promise, a memoized result, a mutable object, or an already acquired resource. “Reusable” must mean a new execution is permitted, not that the same external work or resource acquisition repeats. One-shot continuations are a separate category and correctly remain non-reusable.

**First principles and prior art.** Operational semantics needs evaluation contexts and an explicit store/environment. ECMAScript's call algorithm obtains the callable Reference before arguments and preserves its receiver; laziness is a separate operation. [ECMAScript expressions](https://tc39.es/ecma262/multipage/ecmascript-language-expressions.html#sec-evaluatecall).

**Exact replacement rules.**

> Ordinary syntax inherits ECMAScript's evaluation order, evaluation count, Reference behavior, short-circuiting, and abrupt-completion rules except for explicitly enumerated VibeLang operations. Suspending during evaluation preserves the saved Reference and prior operand values; it does not re-evaluate them.

> Creating a computational function's exported Effect captures the provided receiver and raw argument values only. Each execution creates a fresh source activation, initializes its parameters including defaults/destructuring, and evaluates its body. A default requiring computation is evaluated in that execution. Argument expressions in the external caller remain external work and are not repeated. A defer expression captures lexical bindings and evaluates its entire body anew per execution; const-bound values inside an outer activation remain that activation's values.

> A service projection resolves the key, obtains the implementation, and reads the member before evaluating call arguments. Provider expressions are evaluated once left-to-right before composition; dependency-driven layer acquisition is a separate phase using the pinned Layer memoization and concurrency rules. Each additional language form shall have an ordered evaluation algorithm that specifies its failure and iterator-closing edges.

> Coldness means that constructing a language program executes none of its program body. It does not describe arbitrary foreign construction, captured hot values, or idempotence. Fresh frames do not imply fresh external resources.

**LANGUAGE CHANGE: PARTLY.** Preserving ordinary operand order is already mandatory. The chosen parameter/run-time staging and removal of contextual quotation are explicit new rules; programs observing defaults or factory timing can change. Confidence: high about the gaps; no claim that every listed edge is currently miscompiled.

### 11. MAJOR — Hygiene is a collection of patches, not a language invariant

**Location and rule.** Chapter 27, “Declarations and metadata”; Chapter 29 D123; DECISIONS.md D104/D303:

> “A `.d.ts` that already binds a prelude name imports the prelude type under a free alias such as `Effect_1`.”

D104 says:

> “Compiled generators are named after their function, variable, or property”

D303 adds a special rule preventing a module's generated imports from colliding with the outer file's generated names.

**Falsifiable claim.** These local rules do not require capture avoidance for every introduced binder and free intrinsic reference. A compiler can follow them and still capture a user's `runtime`, `Effect_1`, `arguments_1`, `$direct`, catch binding, temporary, or source-function self-reference in another lowering.

**First principles and prior art.** Hygiene has two directions: inserted binders must not capture source references, and inserted free references must not resolve to source bindings. Picking a rare prefix solves neither in an open identifier namespace. Scheme makes both requirements explicit. [R7RS §4.3](https://small.r7rs.org/attachment/r7rs.pdf).

**Exact replacement rule.**

> Every lowering is hygienic. A source identifier retains its resolved binding through transformation. Each introduced binding has a fresh compiler identity distinct from every source and generated binding in the affected scopes. Each runtime intrinsic reference is bound to the compiler-selected import, independently of source shadowing. Printed names are assigned after binding and avoid all collisions. Moving code preserves free-variable binding identities. These requirements apply to JavaScript and declaration emit, all module forms, wrappers, debug names, helpers, pattern bindings, and recovery regions.

Also require alpha-renaming conformance: rename every user local to names used by emitter helpers and compare behavior. Reserved public generated names, such as a data declaration's explicitly documented companion name, may produce a diagnostic; they must never capture silently.

**LANGUAGE CHANGE: NO for intended lexical behavior.** This makes a general obligation explicit instead of requiring the compiler author to infer it from individual bug fixes. Confidence: high; no new generated-name collision probe asserted.

### 12. MAJOR — Preserving `this` is not enough to preserve a function activation

**Location and rule.** Chapter 13, “Evaluation order,” promises the same receiver. D92's amendment says:

> “The function that binds them in the source now declares `const super_1 = (key) => super[key]` and `const arguments_1 = arguments`”

D104 names generators for debugging; D274 discusses arrow capture. The source chapters contain no corresponding general rule for `new.target`.

**Falsifiable claim.** A function body moved into a generator or region closure can have correct values and frame ownership while still changing its lexical/dynamic environment. The rules cover selected `super`/`arguments` rewrites but do not define preservation for all nested arrows, parameters, regions, computed super accesses, assignments, and named function expressions.

The required distinctions are: ordinary-function dynamic `this` versus arrow lexical `this`; source `arguments` versus generator `arguments`; source `new.target` versus generated activation `new.target`; super's home object and original receiver; and the private immutable self-binding of a named function expression versus an outer variable or generated generator name. Saving a super getter is insufficient to define compound assignments and updates, which must preserve Reference evaluation and getter/setter counts.

**Evidence boundary.** [method_arguments](probes/method_arguments/src/main.vibe) correctly returned 73 after suspension. That particular implementation case is fixed. The finding is the absence of a universal specification obligation, not a claim that every generator loses arguments.

**First principles and prior art.** ECMAScript models function environments and their `[[ThisBindingStatus]]`, `[[NewTarget]]`, and super resolution explicitly. A closure conversion must preserve the source environment, not merely make the generated code syntactically valid. [ECMAScript Function Environment Records](https://tc39.es/ecma262/multipage/executable-code-and-execution-contexts.html#sec-function-environment-records).

**Exact replacement rule.**

> A generated closure or generator is not a source activation. Every occurrence of this, arguments, new.target, super, private class names, and a named function expression's self-binding resolves as in its source activation and source lexical nesting. Transformations preserve receiver identity, home-object super lookup, computed-key order, accessor/update counts, and self-binding identity through suspension and rerun. Where VibeLang intentionally delays activation initialization, Chapter 13 defines that phase; delay does not change binding identity. Unsupported uses are diagnosed before emit. Debug names have no binding effect.

**LANGUAGE CHANGE: NO for the promised JavaScript lexical meaning; timing follows the explicit rule in finding 10.** Confidence: high.

### 13. MAJOR — Cleanup preservation is qualified in the decision log but absolute in the language chapter

**Location and rule.** Chapter 17, rules:

> “A failure during cleanup is never dropped.”

DECISIONS.md D256:

> “This does not extend to failures an Effect operator discards by design, including `timeout`/`race` dropping a loser's cleanup failure.”

D305 explicitly says this limitation remains on Effect 4.0.6.

**Confirmed probe.** [timeout_cleanup](probes/timeout_cleanup/src/main.vibe) prints `cleanup-ran`, then throws `Cleanup` in a finalizer of timed-out work. Its printed Exit contains TimeoutError alone, not Cleanup. [Result](probes/timeout_cleanup/result.log).

**First principles and prior art.** “Cleanup executes” and “cleanup's failure is observable in the parent's Cause” are different properties. The latter requires an explicit join/aggregation policy at a concurrency boundary. Effect 4 Cause stores multiple Fail/Die/Interrupt reasons in a flat array; this review does not import Effect 3's sequential/parallel tree into version 4. [Effect 4 Cause](https://effect.website/docs/v4/data-types/cause). The measured 4.0.6 operator behavior and the spec's D256 determine the timeout claim.

Chapter 17 also intentionally lets typed catch consume a whole multi-failure Cause by selecting its first failure, and D306 permits recovery beside interruption. Those are stated policies, not accidental algebra errors. They need to remain distinct from unintentional loss during finalization.

**Exact replacement rule, preserving the chosen Effect compatibility policy.**

> VibeLang's cleanup combiner preserves every reason until an explicitly specified recovery or concurrency operator consumes it. Source finally, using, scope close, and continuation abandonment use that combiner. This guarantee is local to the exit they produce. Effect 4.0.6 timeout/race may discard a losing fiber's final exit, including cleanup failures; observing the parent's exit therefore does not observe those reasons. Typed catch consumes the selected failure's entire recoverable cause as specified below. Applications requiring every child cleanup failure must use an explicit join/aggregation operation with that guarantee.

Put this qualification beside the opening timeout example, not solely in D256 or an evidence appendix. Pin the behavior in conformance tests. A stronger language-level race could be designed, but must not silently claim to be Effect's race.

**LANGUAGE CHANGE: NO for this compatibility-preserving rewrite.** The alternative “never lose any child cleanup failure” requires a different operator and is a language change. Confidence: certain, reproduced.

### 14. MAJOR — Style and optimization rules lack a common observation model

**Location and rule.** Chapter 29 D96:

> “`() => fork(p)`, an arrow function with an expression body, is `Effect.forkScoped` and keeps `Scope` in R”

Chapter 28 EK4823 recommends:

> “Write the value as the body”

for an arrow block that only returns a value. Chapter 15 promises:

> “No point where another fiber could run disappears.”

DECISIONS.md D294 justifies dropping proven final match tests partly because otherwise branch coverage cannot reach 100%; D274 chooses shorter execution paths using run-loop budgets.

**Falsifiable claim.** Replacing `() => { return fork(p) }` with `() => fork(p)` can change ownership and cancellation lifetime: the first has an owning function-body block, the second uses the caller's Scope. “No new diagnostic” is not a proof of preserved behavior. A code action or optimizer must account for lifetime, Cause, binding, and scheduling observations, not just A/E/R.

D294's amended class/custom-matcher preservation is a real improvement: it keeps a runtime assertion rather than trusting structural class types. The earlier rationale still incorrectly equates this with TypeScript deleting the last switch test. TypeScript's exhaustiveness checking does not generally erase JavaScript case tests. More generally, even a successful getter-based test can be observable; proving coverage does not prove purity of testing.

**First principles and prior art.** An optimization proves observational equivalence under a declared observation model. Exhaustiveness proves absence of unmatched inhabitants; it does not prove absence of test effects. Ownership is dynamic behavior. Rust's coverage algorithm analyzes pattern usefulness under Rust's own value and pattern rules, not arbitrary JavaScript getter behavior. [Rust pattern checking](https://rustc-dev-guide.rust-lang.org/pat-exhaustive-checking.html), [ECMAScript expression evaluation](https://tc39.es/ecma262/multipage/ecmascript-language-expressions.html).

**Exact replacement rule.**

> Every source refactoring and optimization preserves returned values, failure Causes up to explicitly permitted recovery, observable side-effect order/count, lexical bindings, resource/fiber ownership, and language-defined suspension points. A code action that changes any of these is labeled a semantic change and is not an automatic style fix. Arrow block-to-expression conversion is unavailable when it changes an owning scope. A match test may be omitted only when it is both exhaustive and observationally inert. Coverage goals never establish that proof.

> The specification defines permitted scheduling variation independently of emitter instruction counts. If an Effect operation is a required suspension opportunity, an optimization preserves it; otherwise the language must explicitly say the opportunity is not guaranteed.

**LANGUAGE CHANGE: NO for the conservative code-action/optimization restriction.** Making all expression-bodied functions implicit owning blocks would be an additional language change; use explicit forkIn for escaped lifetimes if adopting it. Confidence: high on the specified lifetime conflict; EK4823 was not probed.

### 15. MAJOR — Declaration emit needs a semantic ABI, not merely readable types

**Location and rule.** Chapter 27, “Declarations and metadata”:

> “TypeScript consumers need only the `.js`, `.d.ts`, `effect`, and runtime packages.”

> “Chapter 15's control-class and `$direct` JSDoc metadata is a design target; the compiler neither emits nor reads it.”

Chapter 14, “What the compiler infers”:

> “Precisely, E is the type of every expected failure a cause can hold.”

**Falsifiable claim.** A declaration consumer needs stable function kind, service identifier identity, callback E/R polymorphism, and handler/control restrictions, not only a syntactically valid success type. If source provenance is used for semantic decisions, then separate compilation can select a different interpretation unless that information is either irrelevant by construction or carried by the ABI.

The missing direct-call metadata alone is not a soundness bug: the document correctly chooses the slower Effect path. But the optional-brand counterexample crosses precisely the type boundary advertised as safe. D269 factory phase selection, native/plain callback kinds, control-operation identity, and D311 namespace shorthand likewise need explicit declaration-roundtrip obligations.

Typed E is intentionally not “all ways the program can go wrong.” Defects and interruption are outside E, and trust declarations, casts, any, and native callbacks can invalidate broader claims. TypeScript already admits unsound assignments; VibeLang must state which stronger guarantees it adds and actually enforces. [TypeScript's soundness note](https://www.typescriptlang.org/docs/handbook/type-compatibility.html). Koka is useful contrast: its stated absence-of-exception theorem is a semantic property of a defined effect system, not an inference convention. [Leijen, Koka](https://www.microsoft.com/en-us/research/publication/koka-programming-with-row-polymorphic-effect-types/).

**Exact replacement rule.**

> For every exported declaration, a consumer compiled from its emitted .d.ts has the same public runtime operation, success/error/requirement contract, service identity, and legal callback/handler uses as a consumer compiled from source. Optional optimization metadata may affect cost only. Semantic metadata has a versioned, specified representation or is eliminated from call dispatch. Declaration emit uses standard TypeScript syntax and hygienic imports, and never exposes private generated entry points as public exports.

> The E guarantee bounds Fail reasons, not Die or Interrupt reasons. Its assumptions are checked VibeLang code, truthful foreign contracts, and absence of explicitly unsafe escapes. Unsafe escapes are identified in the specification. Native failures not promised by an adapter become defects; adapters cannot manufacture a claim that their behavior was statically proved.

> Provider checking distinguishes layer-build E/R from service-call E/R; wire composes nominal identifiers and rejects unknown output identity. The declaration roundtrip must preserve that distinction and any defaults/reference-key behavior.

Require a roundtrip suite with a stock TypeScript consumer and a fresh VibeLang consumer that sees only emitted declarations. It must include aliases/re-exports, recursive E/R inference, generic callbacks, services, providers, data variants, and open error families.

**LANGUAGE CHANGE: NO for the claimed ABI guarantee; YES where existing conventions violate it, notably finding 1.** Confidence: high on the missing normative contract; no claim that every listed declaration form currently fails.

### 16. MAJOR — The normative documents disagree and provide no precedence rule

**Location and rules.** The introduction says:

> “Every rule in this specification is decided.”

Chapter 13 says:

> “With overloads, the first candidate that accepts the lambda in the form it expects wins”

DECISIONS.md D257 instead says:

> “a candidate whose parameter expects an `Effect` and passes a program argument by name outranks one that would run that same argument.”

Chapter 4, “Providers that hold resources”:

> “`using pool = …` would close it when the provider function returned, before any query ran.”

D222 says:

> “a `using` in the setup is released when the layer's scope closes”

**Falsifiable claim.** Two conforming readers cannot infer one behavior for all these cases. Some differences are genuine amendments, but the chapter text has not been made authoritative and consistent with them. Candidate order and resource lifetime cannot be left to document archaeology.

Additional specific drift:

- Chapter 12's matching answer says the proposal “is not used”; Appendix B says “Not adopted.” Chapter 3 and D206–215 define and implement it. Appendix C's effectful-matching guidance still points only to switch/if.
- Chapter 10 sends generator-style code to TypeScript; D271 explicitly admits iterator-annotated native generators, including async generators, in VibeLang.
- The introduction names D1–D60 and a 2026-10-16 status while D310–313 are provisional amendments pending review on 2026-10-27; D25 still ends “Open.”
- Chapter 29 repeats the D13 row six more times where a reader expects other decisions.
- Chapter 3's defect discussion still motivates a difference from Effect.catch that D305 removes for the pinned 4.0.6 runtime.
- Chapter 27's block explicitly marked `dts` contains `User!UserNotFound!`, which is not standard TypeScript declaration syntax, contrary to Chapter 14.
- D294 retains the false blanket analogy to TypeScript switch erasure, even though its later correction properly acknowledges structural class-pattern problems.

**First principles and prior art.** A specification must assign a unique meaning or explicitly reject a program. ECMAScript separates normative algorithms from explanatory notes; a revision updates the algorithm rather than appending a contradictory anecdote. [ECMAScript specification](https://tc39.es/ecma262/).

**Exact replacement rule.**

> Chapters 13–17 and the source-to-core rules are normative. Runtime dependencies and their versions are identified explicitly. The decision log is historical and cannot override published normative text. Every adopted decision updates all affected rules, examples, diagnostics, and declaration examples in the same revision. Provisional proposals are labeled non-normative and are excluded from conformance claims. Every semantic rule has a stable identifier and a corresponding conformance assertion.

Resolve the concrete conflicts before calling the document a decided specification. The compilation-eligible callback order and the by-name preference must become one algorithm even if the larger redesign is deferred.

**LANGUAGE CHANGE: NOT INHERENTLY.** Choosing between contradictory published behaviors may require migration; the editorial repair must name which rule wins. Confidence: certain from quoted contradictions.

### 17. MAJOR — Compiler convenience is allowed to overrule language semantics

**Location and rule.** Chapter 30, G19, failure condition for the single-pass experiment:

> “A construct that needs a check outside its own component; its rule changes so that one pass decides it”

Chapter 29 D210 justifies forbidding bindings in some composite patterns because:

> “Inline boolean lowering has nowhere to declare it”

D303 chooses snapshot exports to fit one-file loader output; D294 chooses match emission partly to satisfy coverage; D307 caps generic data parameters because the current WithGenerics encoding cannot pass more.

**Falsifiable claim.** These are implementation constraints being promoted into language rules without an independent semantic rationale. A one-pass checker, a chosen AST lowering, a loader interface, and a coverage tool are replaceable implementation details. When they determine binding or evaluation semantics, each implementation repair can become another language exception.

The frame machine in Part III does not settle this problem. It gives transitions for programs already lowered into frames; it does not determine how a source expression becomes a program, function, native call, factory, or deferred argument. The compiler architecture's hooks are not typing judgments.

**First principles and prior art.** Specify a small language and prove/elicit its implementation, rather than defining the language as whatever a checker hook can decide today. Eff supplies a computation/handler semantics; Koka specifies an effect-inference system and states what its inferred effects guarantee. These are the appropriate precedents for the core language, while Effect's run loop is the appropriate implementation substrate. [Eff](https://math.andrej.com/wp-content/uploads/2012/03/eff.pdf), [Koka](https://www.microsoft.com/en-us/research/publication/koka-programming-with-row-polymorphic-effect-types/).

**Exact replacement rule.**

> The normative language is defined by grammar, binding rules, typing/effect judgments, and an elaboration into a small core with explicit invocation, suspension, execution, handlers, ownership, and completion. Compiler pass count and lowering representation are non-normative. If the implementation cannot establish a required judgment, it reports a documented restriction or requests an annotation; it does not silently assign another meaning. Restrictions chosen for implementation cost are labeled as such and reviewed separately from semantic guarantees.

**LANGUAGE CHANGE: NO by itself.** It changes the design process and specification boundary; individual restrictions may later be lifted compatibly. Confidence: high.

### 18. MINOR — “Every function is an Effect” is no longer an accurate user model

**Location and rule.** Introduction:

> “VibeLang is TypeScript syntax in which every function is an Effect.”

Chapter 15 explicitly retains plain annotated functions and plain callback contracts. D269 adds eager factories; D271 adds native generators.

**Falsifiable claim.** The opening sentence is false for accepted programs. It encourages readers to infer coldness and uniform call behavior that later chapters revoke.

**First principles and prior art.** A user model may omit implementation details, but it must not state a universal claim with observable exceptions. Effect distinguishes a function producing a description from executing that description; the distinction is central here, not pedagogical clutter. [Effect type and execution model](https://effect.website/docs/v4/getting-started/the-effect-type).

**Exact replacement text for the current design.**

> VibeLang adds computational functions to TypeScript. Computational calls run on the current Effect fiber; their exported TypeScript interface returns an Effect. Explicit native regions and certain plain function declarations retain JavaScript behavior. This document specifies which forms belong to each category and when they execute.

Under the proposed minimal design, replace “certain plain function declarations” with “explicit native function declarations.”

**LANGUAGE CHANGE: NO.** Confidence: certain.


## What the specification gets right

- **It treats continuations as owned, one-shot resources.** Chapters 20–23 distinguish continuation capture from ordinary program reuse; require consumption on the capturing fiber; restore Context and interruption state; and unwind abandoned segments. This addresses real resource hazards. OCaml's documented restrictions on one-shot continuations are useful corroboration, though VibeLang goes further in specifying abandonment cleanup. [OCaml effects, linear continuations](https://ocaml.org/manual/5.3/effects.html).
- **The frame invariant is a sound organizing principle.** Chapters 18 and 26 require the runtime to see every activation/region through which suspension or capture can pass. They reject a second scheduler and explain why opaque JavaScript try/finally cannot delimit a captured computation. The mistake is extending “no suspension” into a proof of all other preservation properties.
- **Control class is separate from E/R.** Chapter 15 correctly observes that sleep has empty error and requirement channels while still suspending. A trusted function is at most sync, not automatically pure. Its prohibition on deleting, merging, or reordering calls merely because they are classified pure is appropriately conservative.
- **Provider construction and service invocation are distinguished.** Chapter 4 correctly explains that capturing a dependency while building a layer creates a build requirement, whereas looking it up in a method creates a call-time requirement. Its main resource example correctly avoids using for a pool meant to live for the layer's Scope.
- **The intended evaluation and failure invariants are useful.** Chapter 13 explicitly says left-to-right/once-only and receiver preservation. Chapter 17 distinguishes typed failure, defect, interruption, and abandonment, and pins the 4.0.6 mixed-cause policy. These are enforceable rules once their exceptions and contradictions are repaired.
- **The document records falsifiable runtime claims.** Chapter 25 says, “Passing tests in both is therefore not evidence of agreement,” and identifies a specific prompt-context disagreement between implementations. That is the right standard. Apply it equally to source elaboration, native/direct paths, and declaration-only consumers.
- **Data declarations reuse an existing runtime representation.** Chapter 11/D307 uses Effect Data tagged constructors and tag-based variant matching rather than inventing another equality/serialization world. Distinguishing these closed tagged alternatives from open error families would make the matching story substantially stronger.

## Probe evidence and limits

All probes used the supplied current-build harness, sequentially, with the installed runtime confirmed as effect 4.0.6. Paths are relative to this report. The source, generated output, and captured harness result remain under this reviewer's directory.

| Probe | Compilation / execution | Observation |
| --- | --- | --- |
| [service_brand](probes/service_brand/result.log) | 0 / 1 | Cast-free requirement relabeling passes; missing Alpha at runtime |
| [pattern_shadow](probes/pattern_shadow/result.log) | 0 / 0 | Same predicate under different local names produces false versus true |
| [plain_finally](probes/plain_finally/result.log) | 0 / 0 | Outer catch receives cleanup |
| [frame_finally](probes/frame_finally/result.log) | 0 / 0 | Outer catch receives body |
| [module_live](probes/module_live/result.log) | 0 / 0 | Imported count is 0 while module's current count is 1 |
| [open_error](probes/open_error/result.log) | 0 / 0 | Partial open-family match yields a Die exit |
| [timeout_cleanup](probes/timeout_cleanup/result.log) | 0 / 0 | Cleanup visibly runs; parent Cause contains only TimeoutError |
| [hatch_alias](probes/hatch_alias/result.log) | 0 / 0 | Direct call sees undefined; alias sees an injected object |
| [method_arguments](probes/method_arguments/result.log) | 0 / 0 | Source arguments survive this suspended method; negative evidence against a blanket bug claim |
| [resume_result](probes/resume_result/result.log) | 1 / not run | Candidate counterexample rejected as string-or-number; no runtime unsoundness claimed from it |

Seven findings have positive runtime witnesses; the plain/frame comparison uses two probes. This is a specification review with targeted counterexamples, not an independent replication of the morning compiler audit. Kernel race and ownership conclusions above rest on the written rules, not a claim to have rerun the kernel conformance suite.

## Reading list: the three changes that would remove the most compiler bugs

1. **Replace contextual call staging with a small explicit core.** Write down strict computational invocation, native invocation, explicit program construction/execution, and a phase table before touching more call fast paths. Include a single callback kind/ABI and alias-invariant adapters. Read ECMAScript EvaluateCall and Eff's expression/computation distinction together. This removes whole families of overload-dependent laziness, double evaluation, Effect-object conditionals, and callback conversions. [ECMAScript calls](https://tc39.es/ecma262/multipage/ecmascript-language-expressions.html#sec-evaluatecall), [Eff](https://math.andrej.com/wp-content/uploads/2012/03/eff.pdf).

2. **Make binding preservation a universal compiler contract.** Require resolved-symbol recognition, hygienic generated binders/intrinsics, preservation of source activation context, and live module bindings. Give service identifiers required nominal identity separate from implementation shapes. Read Scheme hygiene alongside ECMAScript environments and TypeScript structural compatibility. Test alpha-renaming, aliasing, module mutation, and declaration roundtrips. This addresses capture, spelling-based features, lost lexical context, service erasure, and export snapshots. [R7RS](https://small.r7rs.org/attachment/r7rs.pdf), [ECMAScript environments](https://tc39.es/ecma262/multipage/executable-code-and-execution-contexts.html), [TypeScript compatibility](https://www.typescriptlang.org/docs/handbook/type-compatibility.html).

3. **Specify one completion/ownership algebra and check every lowering against it.** Plain and framed paths must agree on Cause combination; acquisition must transfer one release obligation atomically; handler answer types must be checked, not warned about; open families require total recovery. Declare concurrency operators' intentional information loss. Differential conformance must compare values, side effects, Causes, and lifetimes, not just emitted text or coverage percentages. Read Effect's Cause/finalization model with OCaml's one-shot discipline and Rust/Kotlin's closed-world exhaustiveness boundary. [Effect Cause](https://effect.website/docs/v4/data-types/cause), [Effect finalization](https://effect.website/docs/v4/resource-management/introduction), [OCaml](https://ocaml.org/manual/5.3/effects.html), [Rust](https://doc.rust-lang.org/reference/attributes/type_system.html#the-non_exhaustive-attribute), [Kotlin](https://kotlinlang.org/docs/sealed-classes.html).