diff --git a/crates/ailang-check/src/linearity.rs b/crates/ailang-check/src/linearity.rs index 064d98b..4795510 100644 --- a/crates/ailang-check/src/linearity.rs +++ b/crates/ailang-check/src/linearity.rs @@ -205,11 +205,19 @@ pub(crate) fn check_module(m: &Module) -> Vec { ctors.insert(name.clone(), fields.clone()); } } - // Iter 22b.1: class/instance defs are skipped here. Once - // 22b.3 monomorphisation materialises class methods as - // ordinary `FnDef`s, the lift's globals map will pick - // them up automatically. - Def::Class(_) | Def::Instance(_) => {} + // Iter 23.4-prep: class methods register their types into + // the globals map so `callee_arg_modes` can see their + // `param_modes`. Without this, a borrow-mode fn that + // forwards its borrow params into a class-method call + // fires `consume-while-borrowed` false positives. + // Instance defs stay a no-op: instance method bodies are + // walked separately via `Def::Fn` after monomorphisation. + Def::Class(c) => { + for m in &c.methods { + globals.insert(m.name.clone(), strip_forall(&m.ty).clone()); + } + } + Def::Instance(_) => {} } } @@ -1426,4 +1434,76 @@ mod tests { }) ); } + + /// Iter 23.4-prep Task 1: a borrow-mode fn that forwards its borrow + /// params into a class-method call must not fire + /// `consume-while-borrowed` false positives. The pre-fix behaviour + /// is two diagnostics (one per param) because + /// `linearity::check_module`'s globals-construction loop skips + /// `Def::Class`, so `callee_arg_modes` cannot see the method's + /// `param_modes` and defaults each call argument to `Consume`. + #[test] + fn class_method_borrow_call_does_not_fire_consume_while_borrowed() { + use ailang_core::ast::{ClassDef, ClassMethod}; + + let class_eq = Def::Class(ClassDef { + name: "TestEq".into(), + param: "a".into(), + superclass: None, + methods: vec![ClassMethod { + name: "teq".into(), + ty: Type::Fn { + params: vec![ + Type::Var { name: "a".into() }, + Type::Var { name: "a".into() }, + ], + param_modes: vec![ParamMode::Borrow, ParamMode::Borrow], + ret: Box::new(Type::bool_()), + ret_mode: ParamMode::Implicit, + effects: vec![], + }, + default: None, + }], + doc: None, + }); + + let ne = Def::Fn(FnDef { + name: "tne".into(), + ty: Type::Fn { + params: vec![ + Type::Var { name: "a".into() }, + Type::Var { name: "a".into() }, + ], + param_modes: vec![ParamMode::Borrow, ParamMode::Borrow], + ret: Box::new(Type::bool_()), + ret_mode: ParamMode::Implicit, + effects: vec![], + }, + params: vec!["x".into(), "y".into()], + body: Term::App { + callee: Box::new(Term::Var { name: "teq".into() }), + args: vec![ + Term::Var { name: "x".into() }, + Term::Var { name: "y".into() }, + ], + tail: false, + }, + suppress: vec![], + doc: None, + }); + + let m = Module { + schema: ailang_core::SCHEMA.into(), + name: "m".into(), + imports: vec![], + defs: vec![class_eq, ne], + }; + + let diags = check_module(&m); + assert!( + diags.is_empty(), + "expected no diagnostics but got {:#?}", + diags + ); + } }