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

Iter 15b: std_list ships, three more compiler gaps closed

Browse Source 
Second stdlib module. Tester wrote std_list.ailx (10 combinators,
164 LOC) and a consumer demo. std_list typechecked standalone;
demo did not, surfacing three compiler bugs:

1. Check-side: Iter 14h's qualify_local_types was applied to
   Term::Var cross-module lookup but not to ctor-field types in
   Term::Ctor synth or Pattern::Ctor resolution. First recursive
   cross-module ADT (List has Cons a (List a) — recursive Con
   self-ref) triggers the bug. std_maybe slipped through because
   Maybe's ctors have no recursive Con field.
2. Codegen-side: same gap mirrored across 4 sites in codegen
   (Term::Ctor synth, lower_ctor, lower_match) plus a tweak to
   unify_for_subst (recurse on re-bind instead of strict equality
   so sibling-derived List<Int> accepts nullary-ctor's List<$u>
   wildcard).
3. Const codegen: emit_const rejected non-literal const bodies.
   The demo's xs : List<Int> = Cons 1 (...) requires it. Fix:
   per-module const table, Term::Var resolution loads literal
   consts from global, inlines non-literal bodies. Bare and
   qualified refs both supported.

All three fixes carry an "Iter 15b" code comment at their site.
~349/25 LOC across ailang-check, ailang-codegen, e2e.rs.

Tests 85 -> 87. New e2e std_list_demo asserts 11-line stdout:
length 5, is_empty false/true, head via from_maybe, tail length,
append length, reverse head, map double head, filter is_even
length, fold_left sum, fold_right sum. New ailang-check unit
test cross_module_recursive_adt_term_and_pat_ctor covers both
the original bug and the symmetric pat-ctor latent twin.

Hash invariance: all pre-15b fixtures + std_maybe defs
bit-identical. 14a / 14e / 14h regressions all green.

Cumulative state: 2 stdlib modules (std_maybe, std_list), 14
combinators, cross-module recursive ADT working end-to-end.
Three compiler bugs surfaced + fixed in dogfood since 14a (each
dogfood iter has surfaced ≥1).

Authoring observation: form (A) at 10 combinators is fine; main
friction is paren-counting in nested seq chains, not the form
itself. n-ary seq would help but is sugar.

Plan 15c: 1000-element list stress test for fold_left (tail-call-
marked) vs fold_right (constructor-blocked).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This commit is contained in:
Brummel
2026-05-07 18:34:49 +02:00
parent 12e9a9c0cc
commit 92f4b4f8c7
8 changed files with 694 additions and 25 deletions
Download Patch File Download Diff File Expand all files Collapse all files
crates/ailang-check/src/lib.rs
+170 -8
View File
@@ -1229,6 +1229,16 @@ fn synth(
// through the import map; the ctor name stays bare and is
// looked up inside the resolved TypeDef. The bare-name path
// is the original Iter 13 behaviour.
//
// Iter 15b: when the type is cross-module, `cdef.fields` is
// written in the owning module's local namespace. A recursive
// self-reference like `Cons a (List a)` carries `Con
// { name: "List" }` even though, from the consumer's view,
// the type is `std_list.List`. Apply `qualify_local_types`
// with the owning module so that recursive ctor field types
// (and any other locally-named cross-module type-cons) are
// qualified before substitution / unification.
let owning_module: Option<String>;
let td = if type_name.matches('.').count() == 1 {
let (prefix, suffix) = type_name.split_once('.').expect("checked");
let target_module = match env.imports.get(prefix) {
@@ -1239,12 +1249,15 @@ fn synth(
});
}
};
env.module_types
let td = env.module_types
.get(&target_module)
.and_then(|tys| tys.get(suffix))
.cloned()
.ok_or_else(|| CheckError::UnknownType(type_name.clone()))?
.ok_or_else(|| CheckError::UnknownType(type_name.clone()))?;
owning_module = Some(target_module);
td
} else {
owning_module = None;
env.types
.get(type_name)
.ok_or_else(|| CheckError::UnknownType(type_name.clone()))?
@@ -1267,6 +1280,23 @@ fn synth(
got: args.len(),
});
}
// Iter 15b: qualify local type-cons in the field types when
// the ctor's owning type is cross-module. No-op when the
// type is local (owning_module is None).
let qualified_fields: Vec<Type> = match &owning_module {
Some(m) => {
let owner_types = env
.module_types
.get(m)
.cloned()
.unwrap_or_default();
cdef.fields
.iter()
.map(|f| qualify_local_types(f, m, &owner_types))
.collect()
}
None => cdef.fields.clone(),
};
// Iter 13a: parameterised ADT — instantiate the type's vars
// with fresh metavars, substitute them through every ctor
// field type, and let the field types' metavars be solved by
@@ -1280,7 +1310,7 @@ fn synth(
mapping.insert(v.clone(), m.clone());
type_args.push(m);
}
for (a, exp) in args.iter().zip(cdef.fields.iter()) {
for (a, exp) in args.iter().zip(qualified_fields.iter()) {
let exp_inst = substitute_rigids(exp, &mapping);
let actual = synth(a, env, locals, effects, in_def, subst, counter)?;
unify(&exp_inst, &actual, subst)?;
@@ -1516,18 +1546,30 @@ fn type_check_pattern(
// produces for qualified `Term::Ctor`s. Multiple imported
// candidates → `ambiguous-ctor` (local always wins on
// conflict, hence the "imported only if local missing" order).
//
// Iter 15b: track whether the resolved ctor lives in an
// imported module. If so, the cdef's recursive self-references
// need `qualify_local_types` (symmetric to the term-ctor fix);
// otherwise their bare names will not unify against the
// qualified scrutinee args.
let resolved_type_name: String;
let resolved_td: TypeDef;
let resolved_owning_module: Option<String>;
if let Some(cref) = env.ctor_index.get(ctor) {
resolved_type_name = cref.type_name.clone();
resolved_td = env.types[&cref.type_name].clone();
resolved_owning_module = None;
} else {
let mut hits: Vec<(String, TypeDef)> = Vec::new();
let mut hits: Vec<(String, String, TypeDef)> = Vec::new();
for imp in env.imports.values() {
if let Some(tys) = env.module_types.get(imp) {
for (tname, td) in tys {
if td.ctors.iter().any(|c| &c.name == ctor) {
hits.push((format!("{imp}.{tname}"), td.clone()));
hits.push((
format!("{imp}.{tname}"),
imp.clone(),
td.clone(),
));
}
}
}
@@ -1535,14 +1577,16 @@ fn type_check_pattern(
match hits.len() {
0 => return Err(CheckError::UnknownCtorInPattern(ctor.clone())),
1 => {
let (qname, td) = hits.into_iter().next().expect("len == 1");
let (qname, owner, td) =
hits.into_iter().next().expect("len == 1");
resolved_type_name = qname;
resolved_td = td;
resolved_owning_module = Some(owner);
}
_ => {
return Err(CheckError::AmbiguousCtor {
ctor: ctor.clone(),
candidates: hits.into_iter().map(|(q, _)| q).collect(),
candidates: hits.into_iter().map(|(q, _, _)| q).collect(),
});
}
}
@@ -1577,6 +1621,24 @@ fn type_check_pattern(
// into each cdef field type (e.g. `Cons(a, List a)` checked
// against a `List Int` scrutinee yields field types
// `Int, List Int`).
//
// Iter 15b: when the resolved ctor lives in an imported
// module, qualify any bare local type-cons in the field
// types first — symmetric to the term-ctor fix.
let qualified_fields: Vec<Type> = match &resolved_owning_module {
Some(m) => {
let owner_types = env
.module_types
.get(m)
.cloned()
.unwrap_or_default();
cdef.fields
.iter()
.map(|f| qualify_local_types(f, m, &owner_types))
.collect()
}
None => cdef.fields.clone(),
};
let mapping: BTreeMap<String, Type> = td
.vars
.iter()
@@ -1584,7 +1646,7 @@ fn type_check_pattern(
.zip(scrutinee_args)
.collect();
let mut out = Vec::new();
for (sub, sub_ty) in fields.iter().zip(cdef.fields.iter()) {
for (sub, sub_ty) in fields.iter().zip(qualified_fields.iter()) {
let sub_ty_inst = substitute_rigids(sub_ty, &mapping);
out.extend(type_check_pattern(sub, &sub_ty_inst, env)?);
}
@@ -2595,6 +2657,106 @@ mod tests {
);
}
/// Iter 15b: a recursive cross-module ADT (`std_list.List a` with a
/// `Cons a (List a)` ctor) round-trips through both `Term::Ctor` synth
/// and pattern-ctor binding without unqualified-field-name unification
/// failures. The bug fixed in 15b: `cdef.fields` on the imported side
/// carries `Con("List", _)` (unqualified, owner's local namespace),
/// while the consumer-visible scrutinee/result type is
/// `Con("std_list.List", _)`. Without `qualify_local_types` applied
/// to the fields at use sites, `unify` rejected the mismatch.
#[test]
fn cross_module_recursive_adt_term_and_pat_ctor() {
// Library: `data List a = Nil | Cons a (List a)`. The `Cons`
// field types reference the local-namespace `List`, exactly
// mirroring the std_list shape that tripped the gap.
let lib = Module {
schema: SCHEMA.into(),
name: "lst".into(),
imports: vec![],
defs: vec![Def::Type(TypeDef {
name: "List".into(),
vars: vec!["a".into()],
ctors: vec![
Ctor { name: "Nil".into(), fields: vec![] },
Ctor {
name: "Cons".into(),
fields: vec![
Type::Var { name: "a".into() },
Type::Con {
name: "List".into(),
args: vec![Type::Var { name: "a".into() }],
},
],
},
],
doc: None,
})],
};
// Consumer: builds `Cons 1 (Cons 2 (Nil))` via qualified
// `lst.List/Cons` and pattern-matches it back out. The match
// arm exercises the symmetric pat-ctor fix.
let cons = |head: i64, tail: Term| Term::Ctor {
type_name: "lst.List".into(),
ctor: "Cons".into(),
args: vec![
Term::Lit { lit: Literal::Int { value: head } },
tail,
],
};
let nil = Term::Ctor {
type_name: "lst.List".into(),
ctor: "Nil".into(),
args: vec![],
};
let consumer = Module {
schema: SCHEMA.into(),
name: "uses_lst".into(),
imports: vec![Import { module: "lst".into(), alias: None }],
defs: vec![fn_def(
"head_or_zero",
Type::Fn {
params: vec![],
ret: Box::new(Type::int()),
effects: vec![],
},
vec![],
Term::Match {
scrutinee: Box::new(cons(1, cons(2, nil.clone()))),
arms: vec![
Arm {
pat: Pattern::Ctor {
ctor: "Cons".into(),
fields: vec![
Pattern::Var { name: "h".into() },
Pattern::Wild,
],
},
body: Term::Var { name: "h".into() },
},
Arm {
pat: Pattern::Ctor {
ctor: "Nil".into(),
fields: vec![],
},
body: Term::Lit { lit: Literal::Int { value: 0 } },
},
],
},
)],
};
let mut modules = BTreeMap::new();
modules.insert("lst".into(), lib);
modules.insert("uses_lst".into(), consumer);
let ws = Workspace {
entry: "uses_lst".into(),
modules,
root_dir: std::path::PathBuf::from("."),
};
let diags = check_workspace(&ws);
assert!(diags.is_empty(), "expected green; got {diags:?}");
}
/// Iter 14e: a `Term::App { tail: true, .. }` that genuinely sits
/// in tail position (as the rhs of a `Seq` that is the body of a
/// `Match` arm that is the body of the fn) must pass.