iter 22b.2.2: kind-mismatch class-schema diagnostic
This commit is contained in:
@@ -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,
|
||||
})),
|
||||
),
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
@@ -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<Workspace, WorkspaceLoadError
|
||||
&mut visiting_set,
|
||||
)?;
|
||||
|
||||
// Iter 22b.2: class-schema validation runs before registry
|
||||
// construction so that ill-kinded class definitions are rejected
|
||||
// before any instance against them is registered.
|
||||
validate_classdefs(&modules)?;
|
||||
|
||||
// Iter 22b.1: build the workspace-global instance registry. Three
|
||||
// coherence checks fire here (Orphan / Duplicate / Missing-method);
|
||||
// any violation is surfaced as a `WorkspaceLoadError`, not as a
|
||||
@@ -386,6 +407,55 @@ fn build_registry(
|
||||
Ok(Registry { entries })
|
||||
}
|
||||
|
||||
/// Iter 22b.2: class-schema validation. Runs before `build_registry`.
|
||||
/// Three diagnostics fire from here: `kind-mismatch`,
|
||||
/// `invalid-superclass-param`, `constraint-references-unbound-type-var`.
|
||||
fn validate_classdefs(
|
||||
modules: &BTreeMap<String, Module>,
|
||||
) -> 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:?}"),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
@@ -32,14 +32,17 @@ fn list_json_fixtures() -> Vec<PathBuf> {
|
||||
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)
|
||||
})
|
||||
|
||||
@@ -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": []
|
||||
}
|
||||
}
|
||||
]
|
||||
}
|
||||
]
|
||||
}
|
||||
Reference in New Issue
Block a user