iter 23.4-prep.1: linearity — register Def::Class method types in globals

crates/ailang-check/src/linearity.rs

@@ -205,11 +205,19 @@ pub(crate) fn check_module(m: &Module) -> Vec<Diagnostic> {
                     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
+        );
+    }
 }