Brummel/AILang
1
0
Fork 0
Code Issues 29 Pull Requests Actions Packages Projects Releases Wiki Activity

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

New Issue
Closed
opened 2026-06-01 13:01:31 +02:00 by Brummel · 2 comments
Brummel commented 2026-06-01 13:01:31 +02:00
Owner
Copy Link
Copy Source

Supersedes #54, which patched the leak on the return position only. The
real problem is not the leak; it is that an ownership default
(ParamMode::Implicit) exists at all and is read two ways — the
typechecker treats Implicit == Own (mode_eq,
crates/ailang-core/src/ast.rs), while codegen omits the caller dec for
it (drop.rs ~476), so the same fn-type means two different things. See
design/models/0008-ownership-totality.md, sections 1-2.

Direction

Delete Implicit from ParamMode in a single cutover — ParamMode
becomes {Own, Borrow} — so no defaulted position survives anywhere.
This is the totality result of section 2, scoped to what is provably
shippable today by carving out exactly the one piece the 2026-06-01
design review found unsound.

What ships

  • ParamMode::Implicit deleted. One canonical-JSON hash reset, once,
    for the whole corpus (the hash-pin tests in
    ailang-core/tests/hash_pin.rs and
    ailang-surface/tests/prelude_module_hash_pin.rs reset together). This
    is the single irreversible step (section 6), signed off deliberately.
  • Parameters: total + verified, no new pass. Every parameter carries
    own/borrow. The existing uniqueness/consume analysis already
    verifies these (consume-while-borrowed, over-strict-mode, per-param
    consume_count) and can derive the correct mode for the migration.
    Value-type positions: trivial-own; (borrow (con Int)) is a check
    error (section 3.2).
  • Returns: total via own + a first-order return-provenance check.
    An own return must be a fresh allocation or an owned-binder transfer
    — not an alias of a non-owned binder. This rejects the
    fn f(x: (borrow T)) -> T { x } passthrough that is silently accepted
    today (no return check exists).
  • borrow returns are a check error in this cut, with a diagnostic
    naming the liveness/escape gap. Re-enabling them is separate later work
    behind the escape/liveness axis.

Why this is sound (addresses the 2026-06-01 review)

The review found full totality not atomically shippable because of
borrow-returns — they are refcount-invisible and can outlive their
source (sections 1, 8). This proposal forbids borrow-returns, so it
never enters that gap. And the first-order return-provenance check
suffices without the section-5.2 reachability pass, because
consume-while-borrowed already forbids a borrowed value from escaping
into a returned constructor (constructor args are Position::Consume,
linearity.rs:527): regime A (section 5.1) holds as a consequence of the
existing parameter checks, so a compound own return cannot carry a
borrowed field.

Why this is coherent (where #54 was not)

Implicit is removed entirely — no default remains on any position.
Forbidding borrow on the return position is not a surviving default; it
is a position-dependent mode restriction, exactly like the
already-accepted "value-type positions forbid borrow" rule
(section 3.2). Section 2 forbids defaults, not position restrictions.
#54 left a default standing (parameters = Implicit); this does not.

The cut, stated plainly

#54 took too little (returns only; the default stays on parameters; two
hash resets). Full totality takes too much (borrow-returns need the
unbuilt liveness axis). The right cut is everything except
borrow-returns.

Next step

Hard-gate: a brainstorm spec under docs/specs/ before any plan or code.
Questions to settle there: keyword form (own/borrow vs. adjectival
owned/borrowed, sections 3.4 / 7-Q3) and whether the shared type is
renamed off ParamMode (section 3.4) — both should land before the
cutover, since renaming after the hash reset would be a second
irreversible step. Multi-return (sections 5.3 / 7-Q4) stays out of scope.

Supersedes #54, which patched the leak on the return position only. The real problem is not the leak; it is that an ownership default (`ParamMode::Implicit`) exists at all and is read two ways — the typechecker treats `Implicit == Own` (`mode_eq`, crates/ailang-core/src/ast.rs), while codegen omits the caller `dec` for it (`drop.rs` ~476), so the same fn-type means two different things. See design/models/0008-ownership-totality.md, sections 1-2. ## Direction Delete `Implicit` from `ParamMode` in a single cutover — `ParamMode` becomes `{Own, Borrow}` — so no defaulted position survives anywhere. This is the totality result of section 2, scoped to what is provably shippable *today* by carving out exactly the one piece the 2026-06-01 design review found unsound. ### What ships - **`ParamMode::Implicit` deleted.** One canonical-JSON hash reset, once, for the whole corpus (the hash-pin tests in `ailang-core/tests/hash_pin.rs` and `ailang-surface/tests/prelude_module_hash_pin.rs` reset together). This is the single irreversible step (section 6), signed off deliberately. - **Parameters: total + verified, no new pass.** Every parameter carries `own`/`borrow`. The existing uniqueness/consume analysis already verifies these (`consume-while-borrowed`, `over-strict-mode`, per-param `consume_count`) and can *derive* the correct mode for the migration. Value-type positions: trivial-`own`; `(borrow (con Int))` is a check error (section 3.2). - **Returns: total via `own` + a first-order return-provenance check.** An `own` return must be a fresh allocation or an owned-binder transfer — *not* an alias of a non-owned binder. This rejects the `fn f(x: (borrow T)) -> T { x }` passthrough that is silently accepted today (no return check exists). - **`borrow` returns are a check error in this cut,** with a diagnostic naming the liveness/escape gap. Re-enabling them is separate later work behind the escape/liveness axis. ### Why this is sound (addresses the 2026-06-01 review) The review found full totality not atomically shippable *because of borrow-returns* — they are refcount-invisible and can outlive their source (sections 1, 8). This proposal **forbids** borrow-returns, so it never enters that gap. And the first-order return-provenance check suffices *without* the section-5.2 reachability pass, because `consume-while-borrowed` already forbids a borrowed value from escaping into a returned constructor (constructor args are `Position::Consume`, `linearity.rs:527`): regime A (section 5.1) holds as a consequence of the existing parameter checks, so a compound `own` return cannot carry a borrowed field. ### Why this is coherent (where #54 was not) `Implicit` is removed *entirely* — no default remains on any position. Forbidding `borrow` on the return position is not a surviving default; it is a position-dependent mode restriction, exactly like the already-accepted "value-type positions forbid `borrow`" rule (section 3.2). Section 2 forbids *defaults*, not *position restrictions*. #54 left a default standing (parameters = Implicit); this does not. ### The cut, stated plainly #54 took too little (returns only; the default stays on parameters; two hash resets). Full totality takes too much (borrow-returns need the unbuilt liveness axis). The right cut is everything **except** borrow-returns. ## Next step Hard-gate: a brainstorm spec under docs/specs/ before any plan or code. Questions to settle there: keyword form (`own`/`borrow` vs. adjectival `owned`/`borrowed`, sections 3.4 / 7-Q3) and whether the shared type is renamed off `ParamMode` (section 3.4) — both should land *before* the cutover, since renaming after the hash reset would be a second irreversible step. Multi-return (sections 5.3 / 7-Q4) stays out of scope.
Brummel added the feature label 2026-06-01 13:01:31 +02:00
Brummel commented 2026-06-01 14:53:08 +02:00
Author
Owner
Copy Link
Copy Source

Blocked on #56. De-risking the cutover revealed that deleting Implicit universal-activates the strict linearity check, which currently misfires on value-type and HOF params (~21% of fixtures, all false positives). The analysis must be hardened (value-types exempt from consume-tracking; function application = borrow) before this cutover can ship. Spec 0062 stands but is known-incomplete on that axis until #56 lands.

Blocked on #56. De-risking the cutover revealed that deleting `Implicit` universal-activates the strict linearity check, which currently misfires on value-type and HOF params (~21% of fixtures, all false positives). The analysis must be hardened (value-types exempt from consume-tracking; function application = borrow) before this cutover can ship. Spec 0062 stands but is known-incomplete on that axis until #56 lands.
Brummel commented 2026-06-01 16:54:54 +02:00
Author
Owner
Copy Link
Copy Source

Blocked: executing the cutover (plan 0121, Task 4) revealed that universal linearity activation is NOT clean after #56 — at least three more false-positive classes plus one genuine corpus over-consume surface (full diagnosis in #57). The irreversible variant deletion was correctly stopped before it ran; main is untouched. Tasks 1 (borrow-return reject, e1c9089) and 3 (throwaway migration tool, 39b674c) landed and are green. #55 is blocked on #57 (the #56 part 2 hardening) before the cutover can proceed.

Blocked: executing the cutover (plan 0121, Task 4) revealed that universal linearity activation is NOT clean after #56 — at least three more false-positive classes plus one genuine corpus over-consume surface (full diagnosis in #57). The irreversible variant deletion was correctly stopped before it ran; main is untouched. Tasks 1 (borrow-return reject, e1c9089) and 3 (throwaway migration tool, 39b674c) landed and are green. #55 is blocked on #57 (the #56 part 2 hardening) before the cutover can proceed.
Brummel reopened this issue 2026-06-01 20:46:07 +02:00
Sign in to join this conversation.
No Branch/Tag Specified
Branches Tags
Labels
Clear labels
BLOCKER
Core functionality broken — takes precedence over everything else in the queue. /boss preempts current work to handle it
 bug
Observable misbehaviour — surface inconsistency, false positive, wrong output
 feature
Smaller addition inside a milestone, no full spec
 idea
Not yet decision-ready, no commitment
No Label feature
Milestone
No items
No Milestone
Projects
Clear projects
No project
Assignees
Clear assignees
claude (Claude) Brummel
No Assignees
1 Participants
Notifications
Due Date
No due date set.
Dependencies

No dependencies set.

Reference: Brummel/AILang#55
Delete Branch "%!s()"

Deleting a branch is permanent. Although the deleted branch may continue to exist for a short time before it actually gets removed, it CANNOT be undone in most cases. Continue?