Harden the ownership analysis for universal activation (value-types + HOF application) #56

New Issue

2026-06-01T14:52:33+02:00

Brummel commented

2026-06-01 14:52:33 +02:00

Blocks #55 (delete the ParamMode::Implicit ownership default, spec docs/specs/0062-eliminate-implicit-mode.md).

The discovery

Deleting Implicit makes every fn fully-moded, which turns the strict linearity check (consume-while-borrowed / use-after-consume, crates/ailang-check/src/linearity.rs) on universally for the first time. Today its activation gate (linearity.rs:339) skips any fn with a bare/Implicit param — i.e. all but ~45 of 258 fn-bearing modules. The strict ownership analysis, the core safety feature, currently almost never runs.

Evidence (measured 2026-06-01)

Temporarily materialising bare params as derived modes (consume_count==0 → Borrow, else Own) and batch-checking examples/: 38 of ~182 functional fixtures (~21%) newly break, all with use-after-consume. The real consume_count-derived rule breaks the SAME count as naive all-own, so the mode choice does not fix them. All are false positives, in two classes:

Value-type params (~25): n, i, depth, lo, x, d, sample — Int/Float read multiple times. Value types have no refcount and are never consumed; multi-read is always legal. e.g. sum.ail: (fn sum (params n) (body (if (eq n 0) 0 (+ n (sum (- n 1)))))).
Function params applied + passed in HOFs (~9): f in map_int, fold_left, apply_thrice. Applying a function is a borrow, not a consume.

None is real heap-data multi-consume needing clone.

Root cause

Spec 0062 handled the codegen side of value-types (trivial-own = no dec) but not the check side: the linearity analysis still tracks a value-type or function param as consumable. The Implicit gate has hidden these blind spots because the check almost never ran.

Scope

Harden the linearity analysis for universal activation:

Value types exempt from consume-tracking. Int/Bool/Float/Unit (and decide Str) are never consumed; multi-use is always legal.
Function application counted as borrow, not consume. A HOF that applies its function param and passes it on (recursion) must not trip use-after-consume.

This is independently valuable — it makes the core ownership analysis sharp across the whole codebase for the first time, not just under the #55 cutover.

Open design questions for the spec

Is Str a value type (immutable, but heap-allocated) for consume-tracking purposes?
When is a function value (closure with captures, heap-allocated, RC'd) consumed vs borrowed? Application = borrow; passing to an own param = consume; but the recursion-passing pattern needs precise rules.

depends on: nothing (precondition for #55)
context: discovered while de-risking #55; #55 cannot ship until this lands.

Blocks #55 (delete the `ParamMode::Implicit` ownership default, spec `docs/specs/0062-eliminate-implicit-mode.md`). ## The discovery Deleting `Implicit` makes every fn fully-moded, which turns the strict linearity check (`consume-while-borrowed` / `use-after-consume`, `crates/ailang-check/src/linearity.rs`) on **universally** for the first time. Today its activation gate (`linearity.rs:339`) skips any fn with a bare/`Implicit` param — i.e. all but ~45 of 258 fn-bearing modules. The strict ownership analysis, the core safety feature, currently almost never runs. ## Evidence (measured 2026-06-01) Temporarily materialising bare params as derived modes (`consume_count==0 → Borrow`, else `Own`) and batch-checking `examples/`: **38 of ~182 functional fixtures (~21%) newly break**, all with `use-after-consume`. The real consume_count-derived rule breaks the SAME count as naive all-own, so the mode choice does not fix them. **All are false positives**, in two classes: - **Value-type params** (~25): `n`, `i`, `depth`, `lo`, `x`, `d`, `sample` — `Int`/`Float` read multiple times. Value types have no refcount and are never consumed; multi-read is always legal. e.g. `sum.ail`: `(fn sum (params n) (body (if (eq n 0) 0 (+ n (sum (- n 1))))))`. - **Function params applied + passed in HOFs** (~9): `f` in `map_int`, `fold_left`, `apply_thrice`. Applying a function is a borrow, not a consume. None is real heap-data multi-consume needing `clone`. ## Root cause Spec 0062 handled the **codegen** side of value-types (trivial-own = no `dec`) but not the **check** side: the linearity analysis still tracks a value-type or function param as consumable. The `Implicit` gate has hidden these blind spots because the check almost never ran. ## Scope Harden the linearity analysis for universal activation: 1. **Value types exempt from consume-tracking.** `Int`/`Bool`/`Float`/`Unit` (and decide `Str`) are never consumed; multi-use is always legal. 2. **Function application counted as borrow, not consume.** A HOF that applies its function param and passes it on (recursion) must not trip `use-after-consume`. This is independently valuable — it makes the core ownership analysis sharp across the whole codebase for the first time, not just under the #55 cutover. ## Open design questions for the spec - Is `Str` a value type (immutable, but heap-allocated) for consume-tracking purposes? - When is a function value (closure with captures, heap-allocated, RC'd) consumed vs borrowed? Application = borrow; passing to an `own` param = consume; but the recursion-passing pattern needs precise rules. depends on: nothing (precondition for #55) context: discovered while de-risking #55; #55 cannot ship until this lands.

Brummel added the bug BLOCKER labels 2026-06-01 14:52:33 +02:00

Brummel referenced this issue

2026-06-01 14:53:08 +02:00

Eliminate the Implicit ownership default — totality minus borrow-returns #55

Brummel referenced this issue from a commit

2026-06-01 15:47:37 +02:00

spec: harden the ownership analysis for universal activation (0063)

Brummel referenced this issue from a commit

2026-06-01 15:47:37 +02:00

plan: harden ownership analysis — is_value_type + value exemption + app-borrow (0120)

Brummel referenced this issue from a commit

2026-06-01 15:47:37 +02:00