iter ctt.3: KindMismatch retire

This commit is contained in:
2026-05-12 22:31:57 +02:00
parent 0e556f085c
commit 0d3f44bee1
6 changed files with 97 additions and 83 deletions
+6 -62
View File
@@ -253,22 +253,6 @@ pub enum WorkspaceLoadError {
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,
},
/// Iter 22b.2: class-schema validation. A class's `superclass.type`
/// does not equal its own `param`. Decision 11 single-superclass
/// model requires the superclass to be applied to the same param
@@ -789,23 +773,17 @@ fn build_registry(
}
/// 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`.
/// Two diagnostics fire from here: `invalid-superclass-param`,
/// `constraint-references-unbound-type-var`. The `kind-mismatch`
/// diagnostic was retired at ctt.3 — the malformed shape now
/// fires `BareCrossModuleTypeRef` from the canonical-form
/// validator before `validate_classdefs` runs.
fn validate_classdefs(
modules: &BTreeMap<String, Module>,
) -> Result<(), WorkspaceLoadError> {
for (mod_name, m) in modules {
for m in modules.values() {
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(),
})?;
}
if let Some(sc) = &c.superclass {
if sc.type_ != c.param {
return Err(WorkspaceLoadError::InvalidSuperclassParam {
@@ -841,31 +819,6 @@ fn validate_classdefs(
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(()),
}
}
/// ct.1: the five primitive type names that are always bare under
/// the canonical-form rule. Kept in sync with `Type::int`,
/// `Type::bool_`, `Type::str_`, `Type::unit`, `Type::float` in
@@ -1876,15 +1829,6 @@ mod tests {
}
}
/// ct.1: a class whose parameter `f` appears as a `Type::Con`
/// name (the malformed-but-historically-test-fixture shape used
/// to trigger `KindMismatch` pre-ct.1) is now caught earlier by
/// the canonical-type-names validator: `f` is bare,
/// non-primitive, and not a TypeDef in the owning module, so
/// `BareCrossModuleTypeRef` fires before `validate_classdefs`
/// gets a chance to run. The `KindMismatch` path stays in the
/// codebase as dead-but-defensive code; a future tidy may
/// retire it.
#[test]
fn class_param_in_applied_position_fires_canonical_form_rejection() {
let entry = std::path::PathBuf::from(