diff --git a/crates/ailang-core/src/workspace.rs b/crates/ailang-core/src/workspace.rs index 27cc41f..af08860 100644 --- a/crates/ailang-core/src/workspace.rs +++ b/crates/ailang-core/src/workspace.rs @@ -2231,4 +2231,50 @@ mod tests { other => panic!("expected QualifiedClassName, got {other:?}"), } } + + /// ct.1: a qualified `Constraint.class` nested inside a + /// `ClassDef.methods[].ty.Forall.constraints` must fire + /// `QualifiedClassName`. Distinct from the `Def::Fn` site: the + /// `Def::Class` branch of `check_class_name_fields` has its own + /// per-method Forall walk that needs independent coverage. + #[test] + fn ct1_validator_rejects_qualified_constraint_class_in_classdef_method() { + let m: Module = serde_json::from_value(serde_json::json!({ + "schema": crate::SCHEMA, + "name": "m", + "imports": [], + "defs": [{ + "kind": "class", + "name": "Foo", + "param": "a", + "methods": [{ + "name": "m", + "type": { + "k": "forall", + "vars": ["b"], + "constraints": [ + { "class": "other.MyEq", "type": { "k": "var", "name": "b" } } + ], + "body": { + "k": "fn", + "params": [{ "k": "var", "name": "b" }], + "ret": { "k": "con", "name": "Unit" }, + "effects": [] + } + } + }] + }], + })).unwrap(); + let mut modules = BTreeMap::new(); + modules.insert("m".to_string(), m); + let err = validate_canonical_type_names(&modules) + .expect_err("qualified Constraint.class in ClassDef-method Forall must be rejected"); + match err { + WorkspaceLoadError::QualifiedClassName { name, field, .. } => { + assert_eq!(name, "other.MyEq"); + assert_eq!(field, "Constraint.class"); + } + other => panic!("expected QualifiedClassName, got {other:?}"), + } + } }