AILang/docs/plans/0123-harden-ownership-part2-class1.md

Harden ownership part 2 — iteration 2: local function-typed binder modes (class 1) — Implementation Plan

Parent spec: docs/specs/0064-harden-ownership-analysis-part-2.md

For agentic workers: REQUIRED SUB-SKILL: use the implement skill to run this plan. Steps use - [ ] checkboxes for tracking.

Goal: Resolve the parameter modes of a local function-typed binder so applying a borrow-mode HOF predicate (std_list.filter's p) borrows its argument instead of consuming it, closing false-positive class 1.

Architecture: BinderState gains fn_param_modes: Option<Vec<ParamMode>>, seeded at every function-typed binder introduction site — params and lam-params from their locally-available signature type, let-binders from the LetBinderTypes table built in iteration 1 (now on the Checker). callee_arg_modes, for a local Var callee, returns the binder's fn_param_modes before falling back to the global symbol table. The existing Term::App arg-walk already maps a Borrow mode to a borrow walk, so no App-arm change is needed. Diagnostic-only; no schema/type change.

Tech Stack: crates/ailang-check/src/linearity.rs (the whole fix), examples/ fixture, tests/workspace.rs assertion.

Scope: SECOND iteration of spec 0064 — class 1 only. Out of scope (later iterations): class 2 (alias-redirect map + contract 0008:340 update — callee_arg_modes resolves through aliases there, NOT here), class 4 (partition_eithers rewrite). Iteration 1 already shipped the table infrastructure + class 3. Do NOT add Checker.aliases or touch design/contracts/0008-memory-model.md / examples/std_either_list.ail here.

---

Files this plan creates or modifies:

• Create: examples/c1_local_hof.ail — class-1 RED→GREEN fixture (borrow-mode predicate param applied to a heap element reused in the kept Cons).
• Modify: crates/ailang-check/src/linearity.rs — fn_modes_of helper; BinderState.fn_param_modes field; seeding at the param loop (:394), let arm (:531), lam arm (:610); callee_arg_modes local-binder read (:776); a borrow-predicate test helper + two in-source unit tests.
• Test: crates/ailang-check/tests/workspace.rs:728 — add c1_local_hof to harden_ownership_false_positives_are_clean.

---

Task 1: RED — class-1 fixture and its failing workspace assertion

Files:

• Create: examples/c1_local_hof.ail

• Test: crates/ailang-check/tests/workspace.rs:728

• Step 1: Create the fixture

Create examples/c1_local_hof.ail with exactly:

(module c1_local_hof
  (data Box
    (doc "heap cell")
    (ctor Box (con Int)))
  (data List
    (doc "boxed list of boxes")
    (ctor Nil)
    (ctor Cons (con Box) (con List)))
  (fn filter_box
    (doc "borrow-mode predicate p applied to h; h reused in the kept Cons")
    (type
      (fn-type
        (params (borrow (fn-type (params (borrow (con Box))) (ret (own (con Bool)))))
                (own (con List)))
        (ret (own (con List)))))
    (params p xs)
    (body
      (match xs
        (case (pat-ctor Nil) (term-ctor List Nil))
        (case (pat-ctor Cons h t)
          (if (app p h)
            (term-ctor List Cons h (app filter_box p t))
            (app filter_box p t)))))))

• Step 2: Add the fixture to the false-positive list

In crates/ailang-check/tests/workspace.rs, the test harden_ownership_false_positives_are_clean iterates a literal array at line 728. Change exactly:

    for name in ["fp_value", "fp_hof", "fp_map", "c3_value_let"] {

to:

    for name in ["fp_value", "fp_hof", "fp_map", "c3_value_let", "c1_local_hof"] {

• Step 3: Run the test to verify it fails RED

Run: cargo test -p ailang-check --test workspace harden_ownership_false_positives_are_clean Expected: FAIL — panic c1_local_hof must be linearity-clean; got: [...] with a use-after-consume diagnostic on h in filter_box. The other four fixtures stay clean; only c1_local_hof fails.

---

Task 2: GREEN — fn_param_modes on BinderState, seeded at every introduction site, read by callee_arg_modes

Files:

• Modify: crates/ailang-check/src/linearity.rs:342-348 (add fn_modes_of after strip_forall), :199-216 (BinderState), :393-403 (param loop), :522-536 (Term::Let), :599-623 (Term::Lam), :776-820 (callee_arg_modes), plus the in-source test module.

• Step 1: Add the fn_modes_of helper

In crates/ailang-check/src/linearity.rs, immediately after the strip_forall fn (which ends at :348), add:

/// Pull a function-typed value's declared parameter modes out of its
/// type, unwrapping a leading `forall`. Returns `None` for any
/// non-function type and for a fn-type with no explicit modes (legacy
/// all-implicit), so a caller that gets `None` falls back to the
/// global symbol table exactly as before.
fn fn_modes_of(t: &Type) -> Option<Vec<ParamMode>> {
    match strip_forall(t) {
        Type::Fn { param_modes, .. } if !param_modes.is_empty() => Some(param_modes.clone()),
        _ => None,
    }
}

• Step 2: Add the fn_param_modes field to BinderState

In crates/ailang-check/src/linearity.rs, the struct BinderState (:200-216) ends with the is_value: bool field. Add after it:

    /// For a function-typed binder (a HOF predicate param, or a
    /// `let`/`lam`-bound function value), its declared parameter modes
    /// — so `callee_arg_modes` can resolve `(app p h)` where `p` is a
    /// local `(borrow …)` predicate and walk `h` as a borrow, not a
    /// consume. `None` for a non-function binder.
    fn_param_modes: Option<Vec<ParamMode>>,

(BinderState derives Default at :199; Option<…> defaults to None, so every ..BinderState::default() / BinderState::default() construction site auto-fills it. Only the explicit literal in the param loop, Step 3, must name the new field.)

• Step 3: Seed fn_param_modes at the param loop

In crates/ailang-check/src/linearity.rs, the param-seeding loop (:393-403) builds an explicit BinderState literal. Replace:

        let initial = BinderState {
            consumed: false,
            borrow_count: match mode {
                ParamMode::Borrow => 1,
                ParamMode::Own | ParamMode::Implicit => 0,
            },
            is_value: param_tys.get(i).map(type_is_value).unwrap_or(false),
        };

with (add the final field; the others are unchanged):

        let initial = BinderState {
            consumed: false,
            borrow_count: match mode {
                ParamMode::Borrow => 1,
                ParamMode::Own | ParamMode::Implicit => 0,
            },
            is_value: param_tys.get(i).map(type_is_value).unwrap_or(false),
            fn_param_modes: param_tys.get(i).and_then(|t| fn_modes_of(t)),
        };

• Step 4: Seed fn_param_modes at the Term::Let arm

In crates/ailang-check/src/linearity.rs, the Term::Let arm (:522-536) currently reads the table only for is_value. Replace:

            Term::Let { name, value, body } => {
                self.walk(value, Position::Consume);
                let is_value = self
                    .let_binder_types
                    .get(&(self.def_name.to_string(), name.clone()))
                    .map(type_is_value)
                    .unwrap_or(false);
                self.with_binder(
                    name,
                    BinderState { is_value, ..BinderState::default() },
                    |this| {
                        this.walk(body, pos);
                    },
                );
            }

with (read the teed type once, derive both flags from it):

            Term::Let { name, value, body } => {
                self.walk(value, Position::Consume);
                let teed = self
                    .let_binder_types
                    .get(&(self.def_name.to_string(), name.clone()));
                let is_value = teed.map(type_is_value).unwrap_or(false);
                let fn_param_modes = teed.and_then(|t| fn_modes_of(t));
                self.with_binder(
                    name,
                    BinderState { is_value, fn_param_modes, ..BinderState::default() },
                    |this| {
                        this.walk(body, pos);
                    },
                );
            }

• Step 5: Seed fn_param_modes at the Term::Lam arm

In crates/ailang-check/src/linearity.rs, the Term::Lam arm builds a per-param BinderState at :610-613. Replace:

                    let st = BinderState {
                        is_value: param_tys.get(i).map(type_is_value).unwrap_or(false),
                        ..BinderState::default()
                    };

with:

                    let st = BinderState {
                        is_value: param_tys.get(i).map(type_is_value).unwrap_or(false),
                        fn_param_modes: param_tys.get(i).and_then(|t| fn_modes_of(t)),
                        ..BinderState::default()
                    };

• Step 6: Read the local binder's modes in callee_arg_modes

In crates/ailang-check/src/linearity.rs, callee_arg_modes (:776-820) binds name from a Term::Var callee at :777-780, then goes straight to self.globals.get(name) at :783. Insert, between the name binding and the globals lookup (after the let name = match … block closes, before let ty = match self.globals.get(name)):

        // A local function-typed binder (HOF predicate param, or a
        // `let`/`lam`-bound function value) carries its declared arg
        // modes on its `BinderState`. Prefer those over the global
        // table so `(app p h)` with `p` a local `(borrow …)` predicate
        // borrows `h` instead of consuming it. A local binder shadows a
        // global of the same name, which is the correct lexical scope.
        if let Some(s) = self.binders.get(name) {
            if let Some(modes) = &s.fn_param_modes {
                return modes.clone();
            }
        }

• Step 7: Build the crate (compile gate)

Run: cargo build -p ailang-check Expected: 0 errors. (Adding the Option field broke only the explicit param-loop literal, fixed in Step 3; all other construction sites use ..BinderState::default(). The new field is read in Step 6, so no dead-code warning.)

• Step 8: Run the RED test from Task 1 — now GREEN

First rebuild the CLI is not needed for the test (the test calls check_workspace directly). Run: cargo test -p ailang-check --test workspace harden_ownership_false_positives_are_clean Expected: PASS — c1_local_hof is now linearity-clean ((app p h) borrows h via p's declared (borrow …) arg mode, so h is reusable in the kept Cons), and the other four fixtures stay clean.

• Step 9: Add the borrow-predicate test helper and two unit tests

In crates/ailang-check/src/linearity.rs, in the #[cfg(test)] mod tests block (alongside fn_with_fn_param at :1426 and own_fn_param_applied_twice_is_clean at :1455), add the helper and two tests. The first test exercises the param seeding path (modes from the signature, empty table); the second exercises the let seeding path (modes from a hand-built LetBinderTypes table):

    /// fn f(p0: (borrow (List -> Bool, inner arg Borrow)), h: (own List)).
    /// The inner predicate's arg is `Borrow`, so applying `p0` to `h`
    /// borrows `h` (it stays reusable). Used by the class-1 tests.
    fn fn_with_borrow_pred_and_heap(name: &str, body: Term) -> Def {
        let list = Type::Con { name: "List".into(), args: vec![] };
        Def::Fn(FnDef {
            name: name.into(),
            ty: Type::Fn {
                params: vec![
                    Type::Fn {
                        params: vec![list.clone()],
                        param_modes: vec![ParamMode::Borrow],
                        ret: Box::new(Type::bool_()),
                        ret_mode: ParamMode::Own,
                        effects: vec![],
                    },
                    list.clone(),
                ],
                param_modes: vec![ParamMode::Borrow, ParamMode::Own],
                ret: Box::new(Type::int()),
                ret_mode: ParamMode::Own,
                effects: vec![],
            },
            params: vec!["p0".into(), "h".into()],
            body,
            suppress: vec![],
            doc: None,
            export: None,
        })
    }

    /// Class 1 (param path): a local borrow-mode predicate param `p0`
    /// applied to a heap binder `h` (`(seq (app p0 h) h)`) does NOT
    /// consume `h` — `p0`'s declared `(borrow …)` arg mode makes the
    /// application a borrow, so `h` is reusable. RED until the
    /// local-fn-param-mode resolution lands.
    #[test]
    fn borrow_fn_param_applied_does_not_consume_heap_arg() {
        let body = Term::Seq {
            lhs: Box::new(Term::App {
                callee: Box::new(Term::Var { name: "p0".into() }),
                args: vec![Term::Var { name: "h".into() }],
                tail: false,
            }),
            rhs: Box::new(Term::Var { name: "h".into() }),
        };
        let m = Module {
            schema: ailang_core::SCHEMA.into(),
            name: "t".into(),
            kernel: false,
            imports: vec![],
            defs: vec![fn_with_borrow_pred_and_heap("f", body)],
        };
        let diags = check_module(&m);
        assert!(
            !diags.iter().any(|d| d.code == "use-after-consume"),
            "applying a borrow-mode predicate param borrows its arg; got {diags:?}"
        );
    }

    /// Class 1 (let path): a `let`-bound function value whose type is
    /// teed as a `(borrow …)` predicate resolves its modes from the
    /// LetBinderTypes table — applying it to heap binder `h` borrows
    /// `h`. The let-value term is a trivial literal; the hand-built
    /// table is the unit under test.
    #[test]
    fn borrow_fn_let_binder_applied_does_not_consume_heap_arg() {
        let body = Term::Let {
            name: "g".into(),
            value: Box::new(Term::Lit { lit: Literal::Int { value: 0 } }),
            body: Box::new(Term::Seq {
                lhs: Box::new(Term::App {
                    callee: Box::new(Term::Var { name: "g".into() }),
                    args: vec![Term::Var { name: "p0".into() }],
                    tail: false,
                }),
                rhs: Box::new(Term::Var { name: "p0".into() }),
            }),
        };
        let m = Module {
            schema: ailang_core::SCHEMA.into(),
            name: "t".into(),
            kernel: false,
            imports: vec![],
            defs: vec![fn_with_modes("f", vec![ParamMode::Own], body)],
        };
        let list = Type::Con { name: "List".into(), args: vec![] };
        let mut lbt = LetBinderTypes::new();
        lbt.insert(
            ("f".into(), "g".into()),
            Type::Fn {
                params: vec![list.clone()],
                param_modes: vec![ParamMode::Borrow],
                ret: Box::new(Type::bool_()),
                ret_mode: ParamMode::Own,
                effects: vec![],
            },
        );
        let diags = check_module_with_visible(&m, &[], &lbt);
        assert!(
            !diags.iter().any(|d| d.code == "use-after-consume"),
            "a let-bound borrow predicate borrows its arg via the teed modes; got {diags:?}"
        );
    }

(fn_with_modes at :1403 builds a fn with List-typed params — here p0 is the (own List) heap binder applied to g. Type::bool_() / Type::int() are the existing convenience constructors used elsewhere in this test module.)

• Step 10: Run the in-source linearity unit tests

Run: cargo test -p ailang-check --lib linearity::tests Expected: PASS — both new tests (borrow_fn_param_applied_does_not_consume_heap_arg, borrow_fn_let_binder_applied_does_not_consume_heap_arg) plus every pre-existing linearity unit test (own_fn_param_applied_twice_is_clean, value_let_binder_multi_read_is_clean, heap_let_binder_multi_read_still_errors, heap_param_multi_consume_still_errors, the implicit_fn_is_exempt family, …) stay green.

• Step 11: Full crate regression

Run: cargo test -p ailang-check Expected: PASS — the whole ailang-check suite green. The local-mode read only fires for a tracked function-typed binder (a HOF param / fn-valued let/lam); a global fn-ref callee is untracked and still falls through to self.globals, so no existing outcome changes except c1_local_hof flipping RED→GREEN.

• Step 12: Workspace suite + regression scripts

Run: cargo test --workspace Expected: PASS (per the typed-MIR re-synth strictness memory, run the whole workspace, not just e2e).

Run: python3 bench/check.py then python3 bench/compile_check.py Expected: both green — diagnostic-only change; no compile-baseline shift.