iter 22b.2.4: constraint-references-unbound-type-var diagnostic

crates/ail/src/main.rs

@@ -1068,6 +1068,25 @@ fn workspace_error_to_diagnostic(
                 "got_type": got_type,
             })),
         ),
+        W::UnboundConstraintTypeVar {
+            class,
+            method,
+            constraint_class,
+            var,
+        } => Some(
+            ailang_check::Diagnostic::error(
+                "constraint-references-unbound-type-var",
+                format!(
+                    "in class `{class}` method `{method}`: constraint `{constraint_class} {var}` references unbound type variable `{var}`"
+                ),
+            )
+            .with_ctx(serde_json::json!({
+                "class": class,
+                "method": method,
+                "constraint_class": constraint_class,
+                "var": var,
+            })),
+        ),
     }
 }
 

crates/ailang-core/src/workspace.rs

@@ -230,6 +230,20 @@ pub enum WorkspaceLoadError {
         expected_param: String,
         got_type: String,
     },
+
+    /// Iter 22b.2: class-schema validation. A class method's
+    /// signature contains a constraint referencing a type variable
+    /// that is neither bound by the method's `Forall.vars` nor equal
+    /// to the class's `param`.
+    #[error(
+        "in class `{class}` method `{method}`: constraint `{constraint_class} {var}` references unbound type variable `{var}`"
+    )]
+    UnboundConstraintTypeVar {
+        class: String,
+        method: String,
+        constraint_class: String,
+        var: String,
+    },
 }
 
 /// Hash over the canonical bytes of a complete module.
@@ -450,6 +464,25 @@ fn validate_classdefs(
                         });
                     }
                 }
+                for method in &c.methods {
+                    if let Type::Forall { vars, constraints, .. } = &method.ty {
+                        let mut bound: BTreeSet<&str> =
+                            vars.iter().map(String::as_str).collect();
+                        bound.insert(c.param.as_str());
+                        for constr in constraints {
+                            if let Type::Var { name } = &constr.type_ {
+                                if !bound.contains(name.as_str()) {
+                                    return Err(WorkspaceLoadError::UnboundConstraintTypeVar {
+                                        class: c.name.clone(),
+                                        method: method.name.clone(),
+                                        constraint_class: constr.class.clone(),
+                                        var: name.clone(),
+                                    });
+                                }
+                            }
+                        }
+                    }
+                }
             }
         }
     }
@@ -856,4 +889,30 @@ mod tests {
             other => panic!("expected InvalidSuperclassParam, got {other:?}"),
         }
     }
+
+    /// Iter 22b.2: a class method's `Type::Forall` whose `constraints`
+    /// reference a type variable that is neither bound by `Forall.vars`
+    /// nor equal to the class's `param` must fire
+    /// `UnboundConstraintTypeVar`. The fixture's `class Foo a` declares
+    /// method `foo` with `forall a. (Bar z) => a -> Unit`; `z` is
+    /// bound nowhere, so the constraint is unsatisfiable by
+    /// construction.
+    #[test]
+    fn constraint_with_unbound_var_fires_unbound_constraint_type_var() {
+        let entry = std::path::PathBuf::from(
+            "../../examples/test_22b2_unbound_constraint_var.ail.json",
+        );
+        let err = load_workspace(&entry)
+            .expect_err("must fire constraint-references-unbound-type-var");
+        match err {
+            WorkspaceLoadError::UnboundConstraintTypeVar {
+                class, method, var, ..
+            } => {
+                assert_eq!(class, "Foo");
+                assert_eq!(method, "foo");
+                assert_eq!(var, "z");
+            }
+            other => panic!("expected UnboundConstraintTypeVar, got {other:?}"),
+        }
+    }
 }

examples/test_22b2_unbound_constraint_var.ail.json

@@ -0,0 +1,30 @@
+{
+  "schema": "ailang/v0",
+  "name": "test_22b2_unbound_constraint_var",
+  "imports": [],
+  "defs": [
+    {
+      "kind": "class",
+      "name": "Foo",
+      "param": "a",
+      "methods": [
+        {
+          "name": "foo",
+          "type": {
+            "k": "forall",
+            "vars": ["a"],
+            "constraints": [
+              { "class": "Bar", "type": { "k": "var", "name": "z" } }
+            ],
+            "body": {
+              "k": "fn",
+              "params": [{ "k": "var", "name": "a" }],
+              "ret": { "k": "con", "name": "Unit" },
+              "effects": []
+            }
+          }
+        }
+      ]
+    }
+  ]
+}