iter ct.1.2: validator extends to Term::Ctor.type_name

crates/ailang-core/src/workspace.rs

@@ -819,6 +819,11 @@ pub(crate) fn validate_canonical_type_names(
                 }
                 Ok(())
             })?;
+            walk_def_terms(def, &mut |type_name: &str| {
+                check_type_con_name(
+                    type_name, mod_name, &local_types, &import_names,
+                )
+            })?;
         }
     }
 
@@ -1028,6 +1033,119 @@ where
     }
 }
 
+/// ct.1: walk every `Term::Ctor.type_name` reachable from a single
+/// `Def`, calling `f` on the type_name strings. Used to enforce the
+/// canonical-form rule on term-side type references.
+fn walk_def_terms<F>(def: &Def, f: &mut F) -> Result<(), WorkspaceLoadError>
+where
+    F: FnMut(&str) -> Result<(), WorkspaceLoadError>,
+{
+    match def {
+        Def::Fn(fd) => walk_term(&fd.body, f),
+        Def::Const(cd) => walk_term(&cd.value, f),
+        Def::Type(_) => Ok(()),
+        Def::Class(cd) => {
+            for cm in &cd.methods {
+                if let Some(body) = &cm.default {
+                    walk_term(body, f)?;
+                }
+            }
+            Ok(())
+        }
+        Def::Instance(id) => {
+            for im in &id.methods {
+                walk_term(&im.body, f)?;
+            }
+            Ok(())
+        }
+    }
+}
+
+/// ct.1: recursive walk of a `Term`, calling `f` on every
+/// `Term::Ctor.type_name`. Embedded `Type` annotations (Lam param /
+/// return types, LetRec types) ride the `walk_def_types` /
+/// `walk_term_embedded_types` path — but `Term::Ctor.type_name` is
+/// a `String`, not a `Type`, so it lives here.
+fn walk_term<F>(t: &Term, f: &mut F) -> Result<(), WorkspaceLoadError>
+where
+    F: FnMut(&str) -> Result<(), WorkspaceLoadError>,
+{
+    match t {
+        Term::Lit { .. } | Term::Var { .. } => Ok(()),
+        Term::App { callee, args, .. } => {
+            walk_term(callee, f)?;
+            for a in args {
+                walk_term(a, f)?;
+            }
+            Ok(())
+        }
+        Term::Let { value, body, .. } => {
+            walk_term(value, f)?;
+            walk_term(body, f)
+        }
+        Term::LetRec { body, in_term, .. } => {
+            walk_term(body, f)?;
+            walk_term(in_term, f)
+        }
+        Term::If { cond, then, else_ } => {
+            walk_term(cond, f)?;
+            walk_term(then, f)?;
+            walk_term(else_, f)
+        }
+        Term::Do { args, .. } => {
+            for a in args {
+                walk_term(a, f)?;
+            }
+            Ok(())
+        }
+        Term::Ctor { type_name, args, .. } => {
+            f(type_name)?;
+            for a in args {
+                walk_term(a, f)?;
+            }
+            Ok(())
+        }
+        Term::Match { scrutinee, arms } => {
+            walk_term(scrutinee, f)?;
+            for arm in arms {
+                walk_pattern(&arm.pat, f)?;
+                walk_term(&arm.body, f)?;
+            }
+            Ok(())
+        }
+        Term::Lam { body, .. } => walk_term(body, f),
+        Term::Seq { lhs, rhs } => {
+            walk_term(lhs, f)?;
+            walk_term(rhs, f)
+        }
+        Term::Clone { value } => walk_term(value, f),
+        Term::ReuseAs { source, body } => {
+            walk_term(source, f)?;
+            walk_term(body, f)
+        }
+    }
+}
+
+/// ct.1: Pattern::Ctor carries a `ctor` name (matches against a
+/// scrutinee's TypeDef) but NOT a type_name field — the type is
+/// inferred from the scrutinee. So Pattern walking only recurses;
+/// no canonical-form check fires here.
+fn walk_pattern<F>(p: &crate::ast::Pattern, f: &mut F) -> Result<(), WorkspaceLoadError>
+where
+    F: FnMut(&str) -> Result<(), WorkspaceLoadError>,
+{
+    use crate::ast::Pattern;
+    match p {
+        Pattern::Wild | Pattern::Var { .. } | Pattern::Lit { .. } => Ok(()),
+        Pattern::Ctor { fields, .. } => {
+            for sub in fields {
+                walk_pattern(sub, f)?;
+            }
+            Ok(())
+        }
+    }
+}
+
 /// Iter 22b.1: extract the head-constructor name of a type, for the
 /// "where is this type defined" lookup and for diagnostic-message
 /// rendering.
@@ -1885,4 +2003,45 @@ mod tests {
             other => panic!("expected BareCrossModuleTypeRef, got {other:?}"),
         }
     }
+
+    /// ct.1: a `Term::Ctor` whose `type_name` is a bare cross-module ref
+    /// must fire `BareCrossModuleTypeRef`. Symmetric to the Type::Con
+    /// rule but the field lives on Term, not Type.
+    #[test]
+    fn ct1_validator_rejects_bare_term_ctor_type_name() {
+        let mut modules = BTreeMap::new();
+        modules.insert("prelude".to_string(),
+            module_with_type_def("prelude", "Ordering"));
+        // Module `m` has no imports, no local Ordering, but a Term::Ctor
+        // referencing bare `Ordering`.
+        let m: Module = serde_json::from_value(serde_json::json!({
+            "schema": crate::SCHEMA,
+            "name": "m",
+            "imports": [],
+            "defs": [{
+                "kind": "fn",
+                "name": "f",
+                "type": { "k": "fn", "params": [], "ret": { "k": "con", "name": "Unit" }, "effects": [] },
+                "params": [],
+                "body": {
+                    "t": "ctor",
+                    "type": "Ordering",
+                    "ctor": "LT",
+                    "args": []
+                }
+            }],
+        })).unwrap();
+        modules.insert("m".to_string(), m);
+        let err = validate_canonical_type_names(&modules)
+            .expect_err("bare Term::Ctor type must be rejected");
+        match err {
+            WorkspaceLoadError::BareCrossModuleTypeRef { module, name, candidates } => {
+                assert_eq!(module, "m");
+                assert_eq!(name, "Ordering");
+                assert_eq!(candidates, vec!["prelude.Ordering".to_string()],
+                    "prelude is implicit-fallback");
+            }
+            other => panic!("expected BareCrossModuleTypeRef, got {other:?}"),
+        }
+    }
 }