From 600565d356ccc8d20c73b390913e1e03ac894829 Mon Sep 17 00:00:00 2001 From: Brummel Date: Sun, 31 May 2026 17:41:05 +0200 Subject: [PATCH] fix(check): localize own-ADT type-args in free-fn mono; complete the lower_to_mir producer MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Additive producer-side work for the typed-MIR milestone (spec docs/specs/0060-typed-mir.md), surfaced while building the mir.1b codegen-consumption switch. Nothing here consumes MIR — codegen is untouched; the whole existing suite stays green and one new RED pin goes green. The mir.1b codegen switch itself stays in the working tree. Headline fix — own-ADT type-arg localization in free-fn mono: monomorphise_workspace's free-fn arm normalises every observed type-arg through Registry::normalize_type_for_lookup. That normalisation is load-bearing for cross-module dedup and a stable specialisation symbol name, but it qualifies a *defining-module-own* ADT to `.`. synthesise_mono_fn_for_free_fn then substitutes those qualified type-args into the polymorphic source signature and body, which are in the module's own *bare* convention (the qualify pre-pass deliberately leaves own-module type-cons bare — lib.rs:4358, "the current module sees its own types bare"). The result is a self-inconsistent specialisation: e.g. fold_left specialised with accumulator b := List minted ((std_list.List, Int) -> std_list.List, std_list.List, List) -> std_list.List — a qualified accumulator parameter against a bare list argument and a bare Lam body. check_workspace never hits this (it synths the pre-mono bodies, bare throughout); the old codegen tolerated it via the now-deleted synth_arg_type's loose type-tracking. The post-mono synth re-entry in lower_to_mir does full unification and correctly rejects it: `expected std_list.List, got List`. Fix: localize_own_types (mono.rs) strips the `.` prefix back to bare for the module's own ADTs, applied to the type-args before they are substituted, so the synthesised signature and body stay uniformly bare-own. The *stored* type_args remain normalised, so the symbol name and the Phase-3 rewrite-cursor key on the same canonical form — the byte-identity invariant between synthesis and rewrite is untouched. The ClassMethod arm needs no analogue: it already substitutes the un-normalised target.type_ (mono.rs:841). Alternatives rejected: (a) drop the normalisation in the shared apply_subst_and_normalize helper — breaks cross-module dedup, mints duplicate specialisations under divergent names. (b) Make lower_to_mir's synth treat `.T` and bare `T` as equal during unification — papers over the producer inconsistency in the consumer and contradicts the established own-types-stay-bare invariant the rest of check relies on. (c) Qualify the whole synthesised def own->qualified — fights lib.rs:4358 and would require the lower path to also flip, cascading the convention change through synth. Producer completeness (additive, mirrors existing guards): - lower_module skips Type::Forall defs (lower_to_mir.rs), mirroring emit_module's guard. Polymorphic defs are stale source kept for round-trip; their bodies carry mono-rewritten call names for specialisations that were never synthesised, so a synth re-entry would hit UnknownIdentifier. - lower_module lowers non-literal const bodies to typed MTerm, carried in MirModule.consts (+ MirConst in ailang-mir). A non-literal const (e.g. a List ctor expression) needs a typed body once the consumer walk takes &MTerm; literal consts emit a global and need no body. - MirModule gains `ast: Module`, populated by lower_module — forward scaffolding the mir.1b codegen consumption reads for module structure. Populated here, consumed by the in-tree switch. Verification: full `cargo test --workspace` green (697 passed, 0 failed) with the codegen-consumption switch stashed out, including the new pin crates/ailang-check/tests/lower_to_mir_ty.rs::poly_free_fn_accumulating_into_own_adt_elaborates (RED before the localize fix with the exact mismatch above, GREEN after) and the full e2e corpus (the own-ADT-poly demos elaborate clean and run through the old codegen). This proves the producer fix is regression-free and the remaining 22 e2e reds in the working tree are codegen-consumption defects, not producer defects. --- crates/ailang-check/src/lower_to_mir.rs | 36 ++++++++- crates/ailang-check/src/mono.rs | 82 +++++++++++++++++++- crates/ailang-check/tests/lower_to_mir_ty.rs | 21 +++++ crates/ailang-mir/src/lib.rs | 25 +++++- 4 files changed, 161 insertions(+), 3 deletions(-) diff --git a/crates/ailang-check/src/lower_to_mir.rs b/crates/ailang-check/src/lower_to_mir.rs index 76c2ae4..3cc81d5 100644 --- a/crates/ailang-check/src/lower_to_mir.rs +++ b/crates/ailang-check/src/lower_to_mir.rs @@ -301,8 +301,42 @@ pub fn lower_module(module: &Module, env: &Env) -> Result { env.imports = im; } let mut defs = Vec::new(); + let mut consts = Vec::new(); for def in &module.defs { + // Non-literal consts are inlined by codegen at each reference + // site; lower their bodies to typed MTerm so codegen re-derives + // no type. Literal consts emit a global and need no MIR body. + if let ailang_core::ast::Def::Const(c) = def { + if !matches!(c.value, Term::Lit { .. }) { + let mut ctx = Ctx { + env: &env, + in_def: &c.name, + locals: IndexMap::new(), + loop_stack: Vec::new(), + }; + let body = lower_term(&mut ctx, &c.value)?; + consts.push(ailang_mir::MirConst { + name: c.name.clone(), + ty: c.ty.clone(), + body, + }); + } + continue; + } let ailang_core::ast::Def::Fn(f) = def else { continue }; + // Polymorphic (`Type::Forall`) defs are stale source defs kept + // for round-trip / `ail diff`; the mono pass synthesised their + // monomorphic counterparts as separate defs. Codegen skips them + // (`emit_module`'s `Type::Forall` guard), so producing a MirDef + // would be dead work — and worse, their bodies may carry + // mono-rewritten call names (e.g. `fold_left__Unit__Int`) whose + // specialisations were never synthesised because the poly def + // itself is never instantiated at those types. The synth + // re-entry on such a body would hit `UnknownIdentifier`. Skip, + // mirroring `emit_module`. + if matches!(&f.ty, Type::Forall { .. }) { + continue; + } // An `(intrinsic)` body is signature-only — codegen supplies it // via the intercept registry, never walking a body. Skip the // lower (which would hit synth's `Term::Intrinsic` unreachable @@ -331,5 +365,5 @@ pub fn lower_module(module: &Module, env: &Env) -> Result { body, }); } - Ok(MirModule { name: module.name.clone(), defs }) + Ok(MirModule { name: module.name.clone(), ast: module.clone(), defs, consts }) } diff --git a/crates/ailang-check/src/mono.rs b/crates/ailang-check/src/mono.rs index 2087bc6..2679797 100644 --- a/crates/ailang-check/src/mono.rs +++ b/crates/ailang-check/src/mono.rs @@ -1036,6 +1036,52 @@ pub fn synthesise_mono_fn( }) } +/// Rewrite every `.` `Type::Con` whose `` is one +/// of `defining_module`'s own ADT names back to the bare `` form, +/// recursing structurally. This is the inverse of +/// [`Registry::normalize_type_for_lookup`](ailang_core::workspace::Registry::normalize_type_for_lookup) +/// restricted to the owning module: cross-module qualified names, +/// primitives, and type variables are left intact. Used to localise a +/// registry-canonical monomorphisation type-arg into the defining +/// module's own bare convention before it is substituted into a +/// polymorphic free-fn signature/body (which carry own-module type-cons +/// bare). See the call site in [`synthesise_mono_fn_for_free_fn`]. +fn localize_own_types(t: &Type, defining_module: &str, own_type_names: &BTreeSet) -> Type { + match t { + Type::Con { name, args } => { + let local = name + .strip_prefix(defining_module) + .and_then(|rest| rest.strip_prefix('.')) + .filter(|bare| own_type_names.contains(*bare)) + .map(|bare| bare.to_string()) + .unwrap_or_else(|| name.clone()); + Type::Con { + name: local, + args: args + .iter() + .map(|a| localize_own_types(a, defining_module, own_type_names)) + .collect(), + } + } + Type::Fn { params, ret, effects, param_modes, ret_mode } => Type::Fn { + params: params + .iter() + .map(|p| localize_own_types(p, defining_module, own_type_names)) + .collect(), + ret: Box::new(localize_own_types(ret, defining_module, own_type_names)), + effects: effects.clone(), + param_modes: param_modes.clone(), + ret_mode: ret_mode.clone(), + }, + Type::Forall { vars, constraints, body } => Type::Forall { + vars: vars.clone(), + constraints: constraints.clone(), + body: Box::new(localize_own_types(body, defining_module, own_type_names)), + }, + Type::Var { .. } => t.clone(), + } +} + /// synthesise a monomorphic `FnDef` for a polymorphic /// free-fn target. The source body comes directly from the /// polymorphic `Def::Fn`'s `body` (NOT from `Registry::entries`); @@ -1103,10 +1149,44 @@ pub fn synthesise_mono_fn_for_free_fn( type_args.len() ))); } + // The observed `type_args` are registry-canonical: a forall var + // bound to the *defining module's own* ADT carries the qualified + // `.` spelling, because mono normalises every + // observed type-arg through `Registry::normalize_type_for_lookup` + // (see `apply_subst_and_normalize`) so that cross-module call sites + // dedup to one specialisation and mint a stable symbol name. The + // polymorphic source signature and body, by contrast, are in the + // module's own *bare* convention — the qualify pre-pass deliberately + // leaves own-module type-cons bare (lib.rs:4358). Substituting a + // qualified type-arg into that bare signature mints a + // self-inconsistent specialisation: a qualified `std_list.List` + // accumulator parameter against a bare `List` list argument and Lam + // body. The post-mono `synth` re-entry (`lower_to_mir`) re-derives + // own-module type-cons in bare form and rejects the clash + // (`expected std_list.List, got List`). Localise each + // type-arg back to the defining module's bare convention before + // substitution so the synthesised signature + body stay uniformly + // bare-own. The stored `type_args` are left normalised — the symbol + // name (line below) and the Phase-3 rewrite cursor both key on the + // canonical form, preserving their byte-identity invariant. (The + // ClassMethod arm needs no analogue: it already substitutes the + // un-normalised `target.type_`.) + let own_type_names: BTreeSet = source_module + .defs + .iter() + .filter_map(|d| match d { + Def::Type(td) => Some(td.name.clone()), + _ => None, + }) + .collect(); let mapping: BTreeMap = forall_vars .iter() .cloned() - .zip(type_args.iter().cloned()) + .zip( + type_args + .iter() + .map(|t| localize_own_types(t, defining_module, &own_type_names)), + ) .collect(); // Apply rigid-var substitution on the function type AND on the diff --git a/crates/ailang-check/tests/lower_to_mir_ty.rs b/crates/ailang-check/tests/lower_to_mir_ty.rs index 1f60831..b8e576d 100644 --- a/crates/ailang-check/tests/lower_to_mir_ty.rs +++ b/crates/ailang-check/tests/lower_to_mir_ty.rs @@ -81,6 +81,27 @@ fn rawbuf_size_only_elaborates() { assert!(mir.modules.contains_key("new_rawbuf_size_only")); } +#[test] +fn poly_free_fn_accumulating_into_own_adt_elaborates() { + // Producer pin (mono ↔ lower_to_mir boundary): a polymorphic free + // fn whose accumulator type-arg instantiates to the *defining + // module's own* ADT must elaborate. `std_list.fold_left` is + // `forall a b. ((b, a) -> b, b, List) -> b`; `List_reverse` + // calls it with `b := List` — the accumulator is std_list's + // OWN `List`. mono normalises the observed type-arg to the + // registry-canonical qualified form (`std_list.List`) for dedup + + // symbol naming, but that qualified form must be localised back to + // the module's bare convention before it is substituted into the + // (own-bare) polymorphic signature and body. Without the + // localisation the synthesised specialisation is self-inconsistent + // — a qualified-`std_list.List` accumulator parameter against a + // bare-`List` list argument and Lam body — and the post-mono + // `synth` re-entry in `lower_to_mir` rejects it with + // `expected std_list.List, got List`. + let mir = elaborate_fixture("std_list_demo"); + assert!(mir.modules.contains_key("std_list")); +} + /// Recursively search for a `MTerm::Str { rep: Static }` reachable /// from a loop binder init (the seed). fn find_static_str_seed(t: &MTerm) -> bool { diff --git a/crates/ailang-mir/src/lib.rs b/crates/ailang-mir/src/lib.rs index 807e311..d1be9e2 100644 --- a/crates/ailang-mir/src/lib.rs +++ b/crates/ailang-mir/src/lib.rs @@ -8,7 +8,7 @@ //! (`StrRep`, filled mir.4). MIR is never authored, never hashed, //! never round-tripped — it is a compiler-internal derived form. -use ailang_core::ast::{Literal, Pattern, Type}; +use ailang_core::ast::{Literal, Module, Pattern, Type}; use std::collections::BTreeMap; /// A whole monomorphised program, lowered to MIR. @@ -21,7 +21,30 @@ pub struct MirWorkspace { #[derive(Debug, Clone)] pub struct MirModule { pub name: String, + /// The post-mono AST module. codegen reads structural data + /// (Def::Type / Def::Const / ctor layouts / intrinsic-fn markers / + /// imports) from here; the typed fn bodies come from `defs`. This + /// keeps `MirWorkspace` the single artefact codegen consumes — + /// structural reads were never a re-derivation, so carrying the AST + /// alongside the typed bodies does not reintroduce one. + pub ast: Module, pub defs: Vec, + /// Typed bodies of the module's non-literal `Def::Const`s. A const + /// is inlined at every `Var` reference site (codegen reads the + /// body from here, keyed by name); literal consts emit a global + /// instead and are not carried. Same role as `defs` for fns — the + /// body is the checker-typed `MTerm` so codegen re-derives no + /// type to lower it. + pub consts: Vec, +} + +/// One lowered non-literal const. `body` is the typed `MTerm` codegen +/// inlines at each reference site. +#[derive(Debug, Clone)] +pub struct MirConst { + pub name: String, + pub ty: Type, + pub body: MTerm, } /// One lowered top-level fn. `sig` is the declared signature; `body`