Type Production Closure

Type production closure is the rule that production runtime and lowering

entrypoints must pass through the checked type/effect boundary before execution

or artifact creation.

The type production closure gate records the production typed boundary in a

source-owned matrix and rejects false production claims.

Run the bounded gate:

make type-production-closure-check

This gate does not run release, self-host, browser, network-cluster, emulator,

or physical hardware jobs.

Production Boundary

Production user-facing entrypoints are:

• tools/runtime-cli.py run;
• tools/runtime-cli.py run-vm;
• tools/runtime-cli.py build;
• tools/runtime-cli.py serve;
• tools/unified-lowering.py emit-ir;
• tools/unified-lowering.py run-vm;
• tools/unified-lowering.py build-native;
• tools/unified-lowering.py build-wasm;
• tools/unified-lowering.py run-wasm;
• tools/unified-lowering.py diff.

Each of those paths uses tools/type-effect-system-check.py directly or uses a

unified IR envelope produced by that checker. Runtime reports and build

metadata record typed IR or unified IR SHA-256 values.

zero-native build, zero-native asm, zero-native build-obj, zero-ar, and

zero-link are compatibility or backend-parity entrypoints. They remain tested

and useful, but they are not allowed to be the production semantic owner for

type production closure. Backend coverage parity owns their full production

alignment.

Explicit Any

Any is valid only when source writes it explicitly. The production

type/effect checker rejects untyped parameters that would otherwise become

implicit Any.

(ƒ bad
  (value)
  value)

That source fails with TE_ANY_IMPLICIT. Use an explicit function annotation

or typed parameter syntax:

(ƒ good
  (∷ (→ I64 I64))
  (value)
  value)

(ƒ also-good
  ((value I64))
  value)

List accessors also require a checked list shape unless the source explicitly

uses Any at the boundary.

Evidence

type-system/production-backends.tsv is the source-owned inventory of

production entrypoints, compatibility entrypoints, typed boundaries, gates, and

evidence paths.

tools/type-production-closure.py validates that matrix, checks the runtime CLI

and unified lowering code paths for typed preflight, and verifies the

type/effect checker owns the required diagnostics.

tests/type-production-closure.sh runs a typed source file through VM, native

runtime, native build, loopback serve, unified IR, native lowering, WASM-shaped

lowering, WASM-shaped execution, and parity comparison. It also proves

implicit Any, non-list access, and false direct-compiler production claims

fail closed.