iter ct.1.3-followup: test for Constraint.class in ClassDef-method Forall

2026-05-11 01:11:47 +02:00
parent 9e2e84332f
commit 219908ed54
1 changed files with 46 additions and 0 deletions
@@ -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:?}"),
+        }
+    }
 }