Brummel/AILang
1
0
Fork 0
Code Issues 29 Pull Requests Actions Packages Projects Releases Wiki Activity

iter mq.1: class-ref canonical-form extension + workspace-internal class-name qualification

Browse Source 
Three schema fields move bare → canonical (bare for same-module,
<module>.<Class> for cross-module): InstanceDef.class,
Constraint.class, SuperclassRef.class. Symmetric to ct.1's
Type::Con.name rule. ClassDef.name stays bare.

validate_canonical_type_names gains three field-walks via new
check_class_ref helper + two sibling diagnostics
BareCrossModuleClassRef / BadCrossModuleClassRef.
check_class_name_fields narrowed to ClassDef.name-only.

Workspace-internal class-name keys all qualified:
class_def_module, class_by_name, registry entries.0,
ClassMethodEntry.class_name, class_superclasses, mono's
class_index, Origin::Class.class_name. New qualify_class_ref
helper at workspace.rs scope plus sibling
qualify_class_ref_in_check in ailang-check.

Two new positive on-disk fixtures (mq1_xmod_constraint_class{,_dep})
exercise the qualified Constraint.class shape.

Recon claim that all existing fixtures' class-refs are intra-module
was empirically wrong — 10 fixtures required minimal canonical-form
migration. Duplicate-instance test architecturally restructured:
post-mq.1 orphan-freedom makes two-modules-on-same-(class,type)
structurally impossible; new test_22b1_dup_same_module fixture
lands both instances in the class's module.

Plan defects fixed inline: Origin::Class.class_name single
construction site (plan recon off-by-one); build_class_index in
mono.rs needed qualifying; build_module_globals needed Def::Instance
carve-out; check_fn declared-constraint matching needed inline
canonical-form lifting; NoInstance Float-aware message arm needed
prelude.Eq/prelude.Ord match; coherence type-leg needed qualified-
head split-and-lookup. Tasks 3-6 ran as one coherent fix.

7/7 tasks, 520 tests green. bench/compile_check.py + cross_lang.py
exit 0; bench/check.py exit 1 (4 improvements-beyond-tolerance,
audit-ratifiable, not a regression).

MethodNameCollision + dispatch path unchanged; iters mq.2 + mq.3
land them.
This commit is contained in:
Brummel
2026-05-13 01:11:56 +02:00
parent 1a5f8289b7
commit 0eb33235eb
28 changed files with 1159 additions and 234 deletions
Download Patch File Download Diff File Expand all files Collapse all files
crates/ailang-check/src/lib.rs
+66 -6
View File
@@ -716,7 +716,9 @@ impl CheckError {
// (`ne` / `lt` / `le` / `gt` / `ge` / direct `eq` / `compare`)
// are the natural surface where the LLM hits this.
if let CheckError::NoInstance { class, at_type, .. } = self.inner() {
if (class == "Eq" || class == "Ord") && at_type == "Float" {
// mq.1: `class` carries the qualified workspace-key shape
// (`prelude.Eq` / `prelude.Ord`), not the bare name.
if (class == "prelude.Eq" || class == "prelude.Ord") && at_type == "Float" {
d.message = format!(
"{} — Float has no Eq/Ord instance by design (partial \
orderability per IEEE-754); see DESIGN.md §\"Float semantics\".",
@@ -1107,6 +1109,11 @@ impl ModuleGlobals {
#[derive(Debug, Clone)]
pub struct ClassMethodEntry {
/// The class that declared the method (e.g. `Show` for `show`).
///
/// mq.1: carries the qualified form `<defining_module>.<Class>`;
/// flows downstream into `ResidualConstraint.class` and
/// `MonoTarget::ClassMethod.class` unchanged. Match the registry
/// key shape so discharge / mono lookups land on the right entry.
pub class_name: String,
/// The class's single type parameter name (e.g. `a` in
/// `class Show a`). The class param appears at this name inside
@@ -1141,7 +1148,13 @@ pub fn build_module_globals(
let mut globals = ModuleGlobals::default();
for def in &m.defs {
let def_name = def.name();
if def_name.contains('.') {
// mq.1: for `Def::Instance`, `def.name()` returns
// `inst.class` which carries the canonical-form value
// (qualified for cross-module). The dot-in-def-name check
// is meant for `Fn`/`Const`/`Type` whose names are author-
// chosen identifiers — instances have no author-chosen
// name and are excluded.
if !matches!(def, Def::Instance(_)) && def_name.contains('.') {
return Err(CheckError::Def(
def_name.to_string(),
Box::new(CheckError::InvalidDefName {
@@ -1198,11 +1211,17 @@ pub fn build_module_globals(
// with enough metadata for the typecheck arms in
// Tasks 9 / 10 to build a residual constraint at
// the call site.
//
// mq.1: store the qualified class name
// (`<defining_module>.<Class>`) so the residual
// emitted at the call site matches the workspace
// registry's qualified key.
let qualified_class = format!("{mname}.{}", cd.name);
for meth in &cd.methods {
globals.class_methods.insert(
meth.name.clone(),
ClassMethodEntry {
class_name: cd.name.clone(),
class_name: qualified_class.clone(),
class_param: cd.param.clone(),
method_ty: meth.ty.clone(),
defining_module: mname.clone(),
@@ -1301,11 +1320,25 @@ pub fn build_check_env(ws: &Workspace) -> Env {
}
// env.class_superclasses — walk every module's Def::Class.
for m in ws.modules.values() {
//
// mq.1: key + value both carry the qualified class name. The map
// is queried by `expand_declared_constraints` with `c.class`
// (a `Constraint.class` value, which is canonical-form on the
// residual side post-mq.1), so both halves of the map must match
// the same workspace-key shape. A bare `SuperclassRef.class`
// (same-module superclass) is lifted via `qualify_class_ref` —
// mirrored inline below to avoid pulling in the workspace helper.
for (mod_name, m) in &ws.modules {
for d in &m.defs {
if let Def::Class(cd) = d {
if let Some(sc) = &cd.superclass {
env.class_superclasses.insert(cd.name.clone(), sc.class.clone());
let class_qualified = format!("{mod_name}.{}", cd.name);
let sc_qualified = if sc.class.contains('.') {
sc.class.clone()
} else {
format!("{mod_name}.{}", sc.class)
};
env.class_superclasses.insert(class_qualified, sc_qualified);
}
}
}
@@ -1604,8 +1637,21 @@ fn check_fn(f: &FnDef, env: &Env) -> Result<()> {
// Decision 11) and compare against residuals. Var-shaped residuals
// not covered by the expanded set fire `MissingConstraint`. Concrete
// residuals are deferred to Task 10's `no-instance` arm.
//
// mq.1: declared constraints carry the canonical-form `class`
// value (bare for same-module, qualified for cross-module). Lift
// to the workspace-key shape (always qualified) before comparing
// against residuals — residuals always carry qualified `class`
// because they come from `ClassMethodEntry.class_name` which is
// qualified post-mq.1.
let declared_constraints: Vec<Constraint> = match &f.ty {
Type::Forall { constraints, .. } => constraints.clone(),
Type::Forall { constraints, .. } => constraints
.iter()
.map(|c| Constraint {
class: qualify_class_ref_in_check(&c.class, &env.current_module),
type_: c.type_.clone(),
})
.collect(),
_ => Vec::new(),
};
let expanded = expand_declared_constraints(&declared_constraints, &env.class_superclasses);
@@ -1733,6 +1779,20 @@ pub struct FreeFnCall {
pub metas: Vec<Type>,
}
/// mq.1: lift a canonical-form class-ref value to the qualified
/// workspace-key shape. Bare ⇒ prepend `caller_module` (the bare
/// form names the caller-module-local class under the canonical-form
/// rule); qualified ⇒ as-is. Sibling of `workspace::qualify_class_ref`
/// for the check-side; duplicated to keep `ailang-check` from
/// reaching across crates for one private helper.
pub(crate) fn qualify_class_ref_in_check(class_ref: &str, caller_module: &str) -> String {
if class_ref.contains('.') {
class_ref.to_string()
} else {
format!("{caller_module}.{class_ref}")
}
}
/// Iter 22b.2 (Task 9): expand a list of declared class constraints
/// with their one-step superclass closure (Decision 11). For every
/// declared `(C, t)`, append `(S, t)` if class `C` has a superclass
crates/ailang-check/src/mono.rs
+8 -2
View File
@@ -341,12 +341,18 @@ fn poly_free_fn_names_for_module(
/// Iter 22b.3: workspace-wide `class-name -> ClassDef` index.
/// Used by the fixpoint to look up the matching class definition
/// when synthesising a fn.
///
/// mq.1: keys carry the qualified class name
/// (`<defining_module>.<Class>`) to match the post-mq.1 residual /
/// `MonoTarget::ClassMethod.class` field and the registry's
/// qualified entries key.
fn build_class_index(ws: &Workspace) -> BTreeMap<String, ClassDef> {
let mut idx = BTreeMap::new();
for m in ws.modules.values() {
for (mod_name, m) in &ws.modules {
for d in &m.defs {
if let Def::Class(c) = d {
idx.insert(c.name.clone(), c.clone());
let qualified = format!("{mod_name}.{}", c.name);
idx.insert(qualified, c.clone());
}
}
}