diff --git a/docs/plans/0121-eliminate-implicit-mode.md b/docs/plans/0121-eliminate-implicit-mode.md index 68525a1..37409b0 100644 --- a/docs/plans/0121-eliminate-implicit-mode.md +++ b/docs/plans/0121-eliminate-implicit-mode.md @@ -68,7 +68,8 @@ figures the plan executes against (verified by `plan-recon`, ## Files this plan creates or modifies - Create: `examples/borrow_return_reject.ail` — RED fixture, borrow-return reject (Task 1) -- Create: `examples/borrow_value_reject.ail` — RED fixture, borrow-over-value reject (Task 2) +- Create: `examples/borrow_value_reject.ail` — RED fixture, borrow-over-value reject (Task 4 Step B2) +- Modify: `crates/ailang-codegen/src/subst.rs:165` — mono-coercion `(borrow value-type)→(own value-type)` (Task 4 Step B1) - Create: `examples/bare_slot_reject.ail` — RED fixture, parser bare-slot reject (Task 4) - Create: `examples/own_return_provenance_reject.ail` (+ `_let`, `_ctor` variants) — already-green `consume-while-borrowed` regression pins (Task 4) - Create: `examples/ownership_total.ail` — post-cutover authoring-surface GREEN fixture (Task 4) @@ -198,14 +199,15 @@ destructured at `:2240`: } ``` -Change the pattern to bind the modes, and after the existing -`check_type_well_formed(&ret_ty, &env)?;` line (`:2275`) add the -reject. First, widen the destructure: +Change the pattern to also bind `ret_mode` (leave `param_modes` under +`..` — Task 1 does not read it; Task 4 Step B2 widens further), and +after the existing `check_type_well_formed(&ret_ty, &env)?;` line +(`:2275`) add the reject. First, widen the destructure: ```rust - let (param_tys, param_modes, ret_ty, ret_mode, declared_effs) = match &inner_ty { - Type::Fn { params, param_modes, ret, ret_mode, effects } => { - (params.clone(), param_modes.clone(), (**ret).clone(), *ret_mode, effects.clone()) + let (param_tys, ret_ty, ret_mode, declared_effs) = match &inner_ty { + Type::Fn { params, ret, ret_mode, effects, .. } => { + (params.clone(), (**ret).clone(), *ret_mode, effects.clone()) } other => { return Err(CheckError::FnTypeRequired( @@ -227,9 +229,10 @@ Then immediately after `check_type_well_formed(&ret_ty, &env)?;`: ``` > Ensure `ParamMode` is in scope in `lib.rs` (it is — `param_modes` -> are already referenced elsewhere in the file). If the widened -> destructure makes `param_modes`/`ret_mode` unused warnings appear -> before Task 2 lands, prefix with `_` and unprefix in Task 2 Step 4. +> are already referenced elsewhere in the file). Task 1 binds only +> `ret_mode`, leaving `param_modes` under `..`, so there is no unused +> binding. **Task 4 Step B2** widens this same destructure to also bind +> `param_modes` (its borrow-over-value loop is the first reader). - [ ] **Step 7: Run the test to verify it passes** @@ -245,111 +248,37 @@ rejects the body shapes that would force one). --- -## Task 2: New signature reject — borrow-over-value +## Task 2: New signature reject — borrow-over-value — FOLDED INTO TASK 4 -`(borrow value-type)` becomes a check error, fired on the signature. -Independent of `Implicit`; tree stays green; independently committable. - -**Files:** -- Create: `examples/borrow_value_reject.ail` -- Modify: `crates/ailang-check/src/lib.rs` (`CheckError` enum, `code()`, signature check) -- Test: `crates/ail/tests/mode_signature_rejects.rs` (extend) - -- [ ] **Step 1: Confirm the corpus has no borrow-over-value today** - -Run: `git grep -nE '\(borrow \(con (Int|Bool|Float|Unit)\)' examples crates/ailang-kernel` -Expected: no matches (if any match, that fixture must be re-moded to -`(own …)` as part of this task before the check can land green — note -it in the implement report). - -- [ ] **Step 2: Write the RED fixture** - -Create `examples/borrow_value_reject.ail`: - -```ail -(module borrow_value_reject - - (fn ignore - (doc "MUST FAIL post-cutover: borrow over a value type is meaningless.") - (type - (fn-type - (params (borrow (con Int))) - (ret (own (con Int))))) - (params n) - (body 0))) -``` - -- [ ] **Step 3: Extend the test** - -Append to `crates/ail/tests/mode_signature_rejects.rs`: - -```rust -/// `(borrow value-type)` is rejected with code `borrow-over-value`. -#[test] -fn borrow_over_value_is_rejected() { - check_rejects_with("borrow_value_reject.ail", "borrow-over-value"); -} -``` - -- [ ] **Step 4: Run the test to verify it fails** - -Run: `cargo test -p ail --test mode_signature_rejects borrow_over_value_is_rejected` -Expected: FAIL — today the fixture checks clean. - -- [ ] **Step 5: Add the `CheckError` variant + code** - -In `pub enum CheckError`, add: - -```rust - /// A fn-type slot is `(borrow V)` where `V` is an unboxed value - /// type (`Int`/`Bool`/`Float`/`Unit`). Borrow is meaningless over - /// a value type — it has no refcount and is copied by value - /// (model §3.2). Code: `borrow-over-value`. - #[error("borrow over value type in `{def}`: `{ty}` is an unboxed value type and cannot be borrowed; use `(own {ty})`")] - BorrowOverValueType { def: String, ty: String }, -``` - -In `fn code(&self)`, add before `CheckError::Internal(_)`: - -```rust - CheckError::BorrowOverValueType { .. } => "borrow-over-value", -``` - -- [ ] **Step 6: Fire the check at the fn signature** - -In `check_def`, immediately after the borrow-return check added in -Task 1 Step 6, add (this uses the `param_modes`/`param_tys` bound in -Task 1; unprefix them if Task 1 prefixed with `_`): - -```rust - // spec 0062: borrow over an unboxed value type is meaningless. - // Fired on the signature, before body dataflow. - for (ty, mode) in param_tys.iter().zip(param_modes.iter()) { - if matches!(mode, ParamMode::Borrow) { - if let Type::Con { name, args } = ty { - if args.is_empty() && ailang_core::primitives::is_value_type(name) { - return Err(CheckError::BorrowOverValueType { - def: f.name.clone(), - ty: name.clone(), - }); - } - } - } - } - // ret slot: a borrow ret is already rejected above, so a - // borrow-over-value ret cannot reach here. -``` - -- [ ] **Step 7: Run the test to verify it passes** - -Run: `cargo build -p ail && cargo test -p ail --test mode_signature_rejects` -Expected: PASS (both tests). - -- [ ] **Step 8: Full check-suite gate** - -Run: `cargo build -p ail && python3 bench/check.py && python3 bench/compile_check.py` -Expected: 0 regressions. (Confirms no corpus fixture borrows a value -type today — the Step 1 grep already proved this.) +> **Finding during implementation (2026-06-01), re-staged.** The +> borrow-over-value reject CANNOT land green in isolation before the +> cutover. The prelude's polymorphic comparison builtins are declared +> `(fn-type (params (borrow a) (borrow a)) (ret …))` (`eq`, `compare`, +> `lt`/`le`/`gt`/`ge`, …). When the mono pass specialises `a := Int` +> (or `Bool`/`Float`), `apply_subst_to_type` (`subst.rs:165`) produces +> `compare__Int(borrow Int, borrow Int)` — i.e. the language's OWN +> generated code is in the forbidden `(borrow value-type)` shape. The +> standalone check broke `compare_{int,bool}_mono_symbol_emits_branch_ladder` +> (`ailang-codegen` lib tests) with `borrow over value type in +> compare__Int`. +> +> **The spec's rule is universal ("value types always own", model +> §3.2), so the language's generated code must honour it too** — the +> principled fix is that the mono pass coerces `(borrow value-type) → +> (own value-type)` when specialising a polymorphic borrow param onto +> a value type (semantically a no-op: value types are never +> refcounted, so own vs borrow emits no inc/dec and the branch-ladder +> IR is unchanged). The check and the coercion are therefore a matched +> pair and land together in Task 4 (which touches the mono/codegen +> path anyway), not as a standalone pre-cutover task. +> +> Spec gap to record at the next brainstorm touch of 0062: the +> borrow-over-value rule needs the mono-coercion clause spelled out; +> the spec tested only the authored case. +> +> The borrow-over-value variant + check + fixture + the +> `borrow_over_value_is_rejected` test + the mono-coercion now live in +> **Task 4 Phase B Steps B1–B2** below. --- @@ -571,6 +500,13 @@ modes (consumed ⇒ own, read-only-heap ⇒ borrow, value ⇒ own). ### Phase B — delete the variant (compiler-driven site set) +> Phase B order: Steps 4–8 (schema + compiler-driven migration + parser +> + printer + drift tag) first, THEN Steps B1–B2 (mono-coercion + +> borrow-over-value), because B1 relies on Step 4's length invariant +> (`param_modes.len() == params.len()`, the elision gone) and B2's check +> must not fire until B1 has coerced the generated value-type-borrow +> instances. Final Phase-B gate is at B2. + - [ ] **Step 4: Edit `ParamMode` and `Type::Fn` serde in `ast.rs`** In `crates/ailang-core/src/ast.rs`: @@ -727,6 +663,151 @@ post-cutover). `"implicit"` exemplar row and the `match` arm that asserts it serialises and is doc-anchored. +- [ ] **Step B1: Mono-coercion — `(borrow value-type) → (own value-type)`** + +The prelude's polymorphic comparison builtins are `(params (borrow a) …)` +(`eq`/`compare`/`lt`/…); specialising `a` to a value type would emit +`compare__Int(borrow Int, …)`, which Step B2's check forbids. Coerce at +the mono specialisation site so the language's generated code honours +"value types always own". In `crates/ailang-codegen/src/subst.rs`, +`apply_subst_to_type`'s `Type::Fn` arm (`:165`), recompute the modes +after substituting the slot types: + +```rust + Type::Fn { params, ret, effects, param_modes, ret_mode } => { + let new_params: Vec = params.iter().map(|p| apply_subst_to_type(p, subst)).collect(); + let new_ret = apply_subst_to_type(ret, subst); + // spec 0062: a polymorphic (borrow a) specialised onto a + // value type becomes (own value-type) — borrow-over-value is + // forbidden and is a no-op for unboxed types (no RC). + let coerce = |ty: &Type, m: &ParamMode| -> ParamMode { + if matches!(m, ParamMode::Borrow) { + if let Type::Con { name, args } = ty { + if args.is_empty() && ailang_core::primitives::is_value_type(name) { + return ParamMode::Own; + } + } + } + *m + }; + let new_param_modes: Vec = new_params.iter().zip(param_modes.iter()) + .map(|(t, m)| coerce(t, m)).collect(); + let new_ret_mode = coerce(&new_ret, ret_mode); + Type::Fn { + params: new_params, + ret: Box::new(new_ret), + effects: effects.clone(), + param_modes: new_param_modes, + ret_mode: new_ret_mode, + } + } +``` + +> Runs after Step 4, so the length invariant `param_modes.len() == +> params.len()` is in force (the elision is gone) and the `.zip` is +> total. `ParamMode` is already in scope in `subst.rs` (the arm binds +> `param_modes`/`ret_mode`). + +- [ ] **Step B2: borrow-over-value reject (corpus re-mode + check + fixture + test)** + +First re-mode any authored `(borrow value-type)` left in the corpus +(the migration tool left explicit `Borrow` untouched in Phase A, so e.g. +`examples/mq3_class_eq_vs_fn_eq_fnmod.ail`'s `(params (borrow (con Int)) +(borrow (con Int)))` is still present): + +Run: `git grep -lE '\(borrow \(con (Int|Bool|Float|Unit)\)' examples crates/ailang-kernel` +For each hit, replace `(borrow (con ))` with `(own (con ))`. +Re-run the grep until empty. + +Add the `CheckError` variant to `pub enum CheckError` +(`crates/ailang-check/src/lib.rs`): + +```rust + /// A fn-type slot is `(borrow V)` where `V` is an unboxed value + /// type (`Int`/`Bool`/`Float`/`Unit`). Borrow is meaningless over + /// a value type — it has no refcount and is copied by value + /// (model §3.2). Code: `borrow-over-value`. + #[error("borrow over value type in `{def}`: `{ty}` is an unboxed value type and cannot be borrowed; use `(own {ty})`")] + BorrowOverValueType { def: String, ty: String }, +``` + +Register the code in `fn code(&self)` before `CheckError::Internal(_)`: + +```rust + CheckError::BorrowOverValueType { .. } => "borrow-over-value", +``` + +In `check_def`, first widen Task 1's destructure to also bind +`param_modes` (it was left under `..` in Task 1 Step 6): + +```rust + let (param_tys, param_modes, ret_ty, ret_mode, declared_effs) = match &inner_ty { + Type::Fn { params, param_modes, ret, ret_mode, effects } => ( + params.clone(), param_modes.clone(), (**ret).clone(), *ret_mode, effects.clone(), + ), + other => { + return Err(CheckError::FnTypeRequired( + f.name.clone(), + ailang_core::pretty::type_to_string(other), + )); + } + }; +``` + +Then, after the borrow-return check, add the borrow-over-value loop: + +```rust + // spec 0062: borrow over an unboxed value type is meaningless. + // Fired on the signature, before body dataflow. The mono-coercion + // (subst.rs, Step B1) guarantees no generated value-type-borrow + // instance reaches here. + for (ty, mode) in param_tys.iter().zip(param_modes.iter()) { + if matches!(mode, ParamMode::Borrow) { + if let Type::Con { name, args } = ty { + if args.is_empty() && ailang_core::primitives::is_value_type(name) { + return Err(CheckError::BorrowOverValueType { + def: f.name.clone(), + ty: name.clone(), + }); + } + } + } + } +``` + +Create `examples/borrow_value_reject.ail`: + +```ail +(module borrow_value_reject + + (fn ignore + (doc "MUST FAIL post-cutover: borrow over a value type is meaningless.") + (type + (fn-type + (params (borrow (con Int))) + (ret (own (con Int))))) + (params n) + (body 0))) +``` + +Add to `crates/ail/tests/mode_signature_rejects.rs` (the +`check_rejects_with` helper is created in Task 1 Step 2): + +```rust +/// `(borrow value-type)` is rejected with code `borrow-over-value`. +#[test] +fn borrow_over_value_is_rejected() { + check_rejects_with("borrow_value_reject.ail", "borrow-over-value"); +} +``` + +Gate: `cargo test -p ailang-codegen --lib compare` — the +`compare_{int,bool}_mono_symbol_emits_branch_ladder` tests PASS (the +mono-coercion makes their value-type params `own`; branch-ladder IR is +unchanged — value types emit no RC ops). And `cargo test -p ail --test +mode_signature_rejects` PASS (all three: borrow-return, borrow-over-value, +provenance pins). + ### Phase C — pins, fixtures, contracts - [ ] **Step 9: Reset all five hash pins** @@ -960,11 +1041,15 @@ fixture, and is exercised by `cargo test -p ail --test migrate_modes`. ## Commit shape (orchestrator note, not an implement step) -Tasks 1, 2, and 3 each leave a green, independent tree and may be -committed separately before the cutover (`feat(check): borrow-return -reject`, `feat(check): borrow-over-value reject`, `chore: throwaway -mode-migration tool`). Task 4 is the single irreversible cutover commit -(`feat: delete ParamMode::Implicit — binary ownership modes (#55)`) -carrying the one-time hash reset. main only ever advances on a green -tree; nothing half-migrated is committed. +Task 1 (borrow-return reject) and Task 3 (throwaway migration tool) +each leave a green, independent tree and may be committed separately +before the cutover (`feat(check): borrow-return reject`, `chore: +throwaway mode-migration tool`). The borrow-over-value reject is NOT a +standalone pre-cutover task — it is folded into Task 4 (Steps B1–B2) +because it is entangled with the mono pass (see the Task 2 finding +note). Task 4 is the single irreversible cutover commit (`feat: delete +ParamMode::Implicit — binary ownership modes (#55)`) carrying the +one-time hash reset and the borrow-over-value reject + mono-coercion. +main only ever advances on a green tree; nothing half-migrated is +committed. ```