fix(check): localize own-ADT type-args in free-fn mono; complete the lower_to_mir producer

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 `<module>.<T>`. 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<Int> minted
    ((std_list.List<Int>, Int) -> std_list.List<Int>,
     std_list.List<Int>, List<Int>) -> std_list.List<Int>
  — 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<Int>, got List<Int>`.

  Fix: localize_own_types (mono.rs) strips the `<defining_module>.`
  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 `<owner>.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

@@ -301,8 +301,42 @@ pub fn lower_module(module: &Module, env: &Env) -> Result<MirModule> {
         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<MirModule> {
             body,
         });
     }
-    Ok(MirModule { name: module.name.clone(), defs })
+    Ok(MirModule { name: module.name.clone(), ast: module.clone(), defs, consts })
 }

crates/ailang-check/src/mono.rs

@@ -1036,6 +1036,52 @@ pub fn synthesise_mono_fn(
     })
 }
 
+/// Rewrite every `<defining_module>.<T>` `Type::Con` whose `<T>` is one
+/// of `defining_module`'s own ADT names back to the bare `<T>` 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<String>) -> 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
+    // `<defining_module>.<T>` 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<Int>, got List<Int>`). 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<String> = source_module
+        .defs
+        .iter()
+        .filter_map(|d| match d {
+            Def::Type(td) => Some(td.name.clone()),
+            _ => None,
+        })
+        .collect();
     let mapping: BTreeMap<String, Type> = 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