diff --git a/crates/ailang-check/tests/loop_recur_typecheck_pin.rs b/crates/ailang-check/tests/loop_recur_typecheck_pin.rs index 060806e..bed062c 100644 --- a/crates/ailang-check/tests/loop_recur_typecheck_pin.rs +++ b/crates/ailang-check/tests/loop_recur_typecheck_pin.rs @@ -66,3 +66,20 @@ fn infinite_loop_typechecks_clean_no_termination_claim() { let codes = check_fixture("loop_forever.ail"); assert!(codes.is_empty(), "infinite loop must typecheck (no totality claim), got {codes:?}"); } + +/// Property: a `Term::Lam` whose body captures a `Term::Loop` binder +/// must be rejected at `ail check` with a dedicated diagnostic, +/// symmetric to `mut-var-captured-by-lambda`. Loop binders are +/// alloca-resident and cannot escape their loop frame (iter-3 reuses +/// the `mut_var_allocas` registry, `std::mem::take`-emptied at the +/// lambda boundary), exactly the mut-var escape rule. Today the +/// escape guard inspects only `mut_scope_stack`; loop binders live +/// in `locals`, so check passes (exit 0) and codegen panics +/// `unreachable!()` at `crates/ailang-codegen/src/lambda.rs:102`. +/// This test pins the FIXED contract — RED until the guard also +/// rejects loop-binder captures. +#[test] +fn lambda_capturing_loop_binder_emits_loop_binder_captured_by_lambda() { + let codes = check_fixture("test_loop_binder_captured_by_lambda.ail.json"); + assert_eq!(codes, vec!["loop-binder-captured-by-lambda".to_string()]); +} diff --git a/examples/test_loop_binder_captured_by_lambda.ail.json b/examples/test_loop_binder_captured_by_lambda.ail.json new file mode 100644 index 0000000..1b8e296 --- /dev/null +++ b/examples/test_loop_binder_captured_by_lambda.ail.json @@ -0,0 +1,42 @@ +{ + "schema": "ailang/v0", + "name": "test_loop_binder_captured_by_lambda", + "imports": [], + "defs": [ + { + "kind": "fn", + "name": "main", + "type": { + "k": "fn", + "params": [], + "ret": { "k": "con", "name": "Int" }, + "effects": [] + }, + "params": [], + "doc": "loop-recur follow-on: a lambda inside a loop body that references the enclosing loop binder `acc` is rejected with loop-binder-captured-by-lambda. Loop binders are alloca-resident and lexically scoped (iter-3 reuses the mut_var_allocas registry, emptied at the lambda frame boundary); lifting them into a heap-closure env is the same deferred work as the mut-var case. Symmetric to mut-var-captured-by-lambda.", + "body": { + "t": "loop", + "binders": [ + { + "name": "acc", + "type": { "k": "con", "name": "Int" }, + "init": { "t": "lit", "lit": { "kind": "int", "value": 0 } } + } + ], + "body": { + "t": "let", + "name": "f", + "value": { + "t": "lam", + "params": [], + "paramTypes": [], + "retType": { "k": "con", "name": "Int" }, + "effects": [], + "body": { "t": "var", "name": "acc" } + }, + "body": { "t": "app", "fn": { "t": "var", "name": "f" }, "args": [] } + } + } + } + ] +}