feat(check): resolve local function-typed binder modes (#57, 0064 iter 2)
Second iteration of spec 0064 (the #55-cutover hardening, #57). Closes false-positive class 1: applying a local function-typed binder -- a HOF predicate param like std_list.filter's `p` -- treated its arguments as Consume because callee_arg_modes resolved only the global symbol table (locals returned an empty mode vec). So `(app p h)` with `p` a local (borrow ...) predicate consumed the heap element `h`, and reusing `h` in the kept Cons false-fired use-after-consume. Fix: BinderState gains fn_param_modes: Option<Vec<ParamMode>>, seeded at all three function-typed binder introduction sites via a new fn_modes_of helper (strip_forall + Type::Fn { param_modes }, None for non-fn / empty-modes so the caller falls through to globals): params and lam-params from their signature type (param_tys), let-binders from the LetBinderTypes table built in iter 1. callee_arg_modes reads a local Var callee's fn_param_modes before the global lookup (a local binder shadows a global -- correct lexical scope); the existing App arg-walk maps a Borrow mode to a borrow walk unchanged, so the fix is confined to the seeding + the one local-precedence read. Scope call (orchestrator): all three seeding sites, not just the param path that unblocks filter -- the point of this hardening cycle is to leave no latent class (the #57-from-0063-deferral lesson), and the extraction is uniform with the table already built. RED-first: examples/c1_local_hof.ail added to harden_ownership_false_positives_are_clean (RED: use-after-consume on filter_box's h) before the fix; GREEN after. Two in-source unit tests pin both seeding paths (param via signature, let via a hand-built table). Verified: c1 RED->GREEN; 119 linearity unit tests green; harden_ownership_false_positives_are_clean green (now c1 + c3); the heap-double-consume must-stay-RED guard still fires; cargo test --workspace green; bench/check.py 34/34, compile_check.py 24/24 stable. Diagnostic-only; no schema/type/codegen change. The stale `// Locals never carry fn-types in 18c.2` comment in callee_arg_modes (and the fn's doc header) is rewritten to the accurate local-precedence behaviour -- it sat in the replaced lines and directly contradicted the new path. Classes 2 (let-alias redirect) and 4 (partition_eithers rewrite) remain for later iterations of spec 0064. refs #57
This commit is contained in:
@@ -0,0 +1,23 @@
|
||||
(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)))))))
|
||||
Reference in New Issue
Block a user