diff --git a/crates/ail/src/main.rs b/crates/ail/src/main.rs index 180877f..4d44f12 100644 --- a/crates/ail/src/main.rs +++ b/crates/ail/src/main.rs @@ -1029,6 +1029,26 @@ fn workspace_error_to_diagnostic( "method": method, })), ), + W::KindMismatch { + class, + param, + method, + defining_module, + } => Some( + ailang_check::Diagnostic::error( + "kind-mismatch", + format!( + "kind mismatch in class `{class}`: parameter `{param}` is used in applied position \ + inside method `{method}` (Decision 11 axis 5: class params are kind `*` only)" + ), + ) + .with_ctx(serde_json::json!({ + "class": class, + "param": param, + "method": method, + "defining_module": defining_module, + })), + ), } } diff --git a/crates/ailang-core/src/workspace.rs b/crates/ailang-core/src/workspace.rs index d284eda..98cd5dc 100644 --- a/crates/ailang-core/src/workspace.rs +++ b/crates/ailang-core/src/workspace.rs @@ -199,6 +199,22 @@ pub enum WorkspaceLoadError { type_repr: String, method: String, }, + + /// Iter 22b.2: class-schema validation. The class parameter + /// appears in applied position (e.g. as the head of a + /// `Type::Con { name == param, args.len() > 0 }`) inside a method + /// signature. Decision 11 axis 5 forbids HKTs — class params are + /// kind `*` only. + #[error( + "kind mismatch in class `{class}`: parameter `{param}` is used in applied position \ + inside method `{method}` (Decision 11 axis 5: class params are kind `*` only)" + )] + KindMismatch { + class: String, + param: String, + method: String, + defining_module: String, + }, } /// Hash over the canonical bytes of a complete module. @@ -250,6 +266,11 @@ pub fn load_workspace(entry_path: &Path) -> Result, +) -> Result<(), WorkspaceLoadError> { + for (mod_name, m) in modules { + for def in &m.defs { + if let Def::Class(c) = def { + for method in &c.methods { + walk_kind_mismatch(&method.ty, &c.param) + .map_err(|()| WorkspaceLoadError::KindMismatch { + class: c.name.clone(), + param: c.param.clone(), + method: method.name.clone(), + defining_module: mod_name.clone(), + })?; + } + } + } + } + Ok(()) +} + +/// Walks a `Type` looking for any `Type::Con { name == param, args +/// non-empty }`. The class param is kind `*`; appearing as a +/// constructor with arguments is a kind-mismatch. +fn walk_kind_mismatch(t: &Type, param: &str) -> Result<(), ()> { + match t { + Type::Con { name, args } => { + if name == param && !args.is_empty() { + return Err(()); + } + for a in args { + walk_kind_mismatch(a, param)?; + } + Ok(()) + } + Type::Fn { params, ret, .. } => { + for p in params { + walk_kind_mismatch(p, param)?; + } + walk_kind_mismatch(ret, param) + } + Type::Forall { body, .. } => walk_kind_mismatch(body, param), + Type::Var { .. } => 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. @@ -714,4 +784,26 @@ mod tests { other => panic!("expected MissingMethod, got {other:?}"), } } + + /// Iter 22b.2: a class whose parameter `f` appears in applied + /// position (`Type::Con { name == "f", args.len() > 0 }`) inside + /// a method signature must fire `KindMismatch`. Decision 11 axis + /// 5 forbids HKTs — class params are kind `*` only, never + /// constructors. + #[test] + fn class_param_in_applied_position_fires_kind_mismatch() { + let entry = std::path::PathBuf::from( + "../../examples/test_22b2_kind_mismatch.ail.json", + ); + let err = load_workspace(&entry) + .expect_err("must fire kind-mismatch"); + match err { + WorkspaceLoadError::KindMismatch { class, param, method, .. } => { + assert_eq!(class, "Functor"); + assert_eq!(param, "f"); + assert_eq!(method, "fmap"); + } + other => panic!("expected KindMismatch, got {other:?}"), + } + } } diff --git a/crates/ailang-surface/tests/round_trip.rs b/crates/ailang-surface/tests/round_trip.rs index b211abe..91922d9 100644 --- a/crates/ailang-surface/tests/round_trip.rs +++ b/crates/ailang-surface/tests/round_trip.rs @@ -32,14 +32,17 @@ fn list_json_fixtures() -> Vec { p.file_name() .and_then(|n| n.to_str()) .map(|n| { - // Iter 22b.1: the `test_22b1_*` fixtures exercise - // class/instance defs at the workspace-load level, - // but the surface (Form-B) parser/printer arms for - // those nodes are deferred to 22b.4. Until that - // ships, including these fixtures in the round-trip - // gate would block 22b.1 close on a property the - // schema floor does not yet promise. Skip them. - n.ends_with(".ail.json") && !n.starts_with("test_22b1_") + // Iter 22b.1 / 22b.2: the `test_22b1_*` and + // `test_22b2_*` fixtures exercise class/instance + // defs at the workspace-load level, but the surface + // (Form-B) parser/printer arms for those nodes are + // deferred to 22b.4. Until that ships, including + // these fixtures in the round-trip gate would block + // 22b on a property the schema floor does not yet + // promise. Skip them. + n.ends_with(".ail.json") + && !n.starts_with("test_22b1_") + && !n.starts_with("test_22b2_") }) .unwrap_or(false) }) diff --git a/examples/test_22b2_kind_mismatch.ail.json b/examples/test_22b2_kind_mismatch.ail.json new file mode 100644 index 0000000..0328761 --- /dev/null +++ b/examples/test_22b2_kind_mismatch.ail.json @@ -0,0 +1,29 @@ +{ + "schema": "ailang/v0", + "name": "test_22b2_kind_mismatch", + "imports": [], + "defs": [ + { + "kind": "class", + "name": "Functor", + "param": "f", + "methods": [ + { + "name": "fmap", + "type": { + "k": "fn", + "params": [ + { "k": "fn", "params": [{ "k": "var", "name": "a" }], + "ret": { "k": "var", "name": "b" }, "effects": [] }, + { "k": "con", "name": "f", + "args": [{ "k": "var", "name": "a" }] } + ], + "ret": { "k": "con", "name": "f", + "args": [{ "k": "var", "name": "b" }] }, + "effects": [] + } + } + ] + } + ] +}