fix(mono): thread declared return type into mono synth re-entry

GREEN for the series-step-1 base-tier RED (e035eff). A polymorphic fn
that allocates `(new RawBuf n)` with no explicit type-arg — element var
solved purely from the enclosing ctor-field type `(con RawBuf a)` —
checked clean but failed `ail build --alloc=rc` with the unregistered
`RawBuf_new__Unit`.

Root cause (verified, and it diverges from the handoff's diagnosis
pointer): the no-type-arg `(new RawBuf n)` desugars to an ordinary
`(app RawBuf.new n)` free-fn call, NOT a surviving `Term::New` — so the
`lower_to_mir.rs:501 elem: None` site the pointer named is never reached
for this case. The real gap is in mono's synth re-entry.
`RawBuf.new : forall a. (Int) -> RawBuf a` has a result-only forall var
`a` that no argument pins. `collect_mono_targets` and
`collect_residuals_ordered` re-`synth` the body but never unified the
synthesised body type against the declared return type, so `a`'s metavar
stayed unbound through the walk and the free-fn arm Unit-defaulted it.
This is the typed-MIR re-synth strictness family again: a mono synth
re-entry that did not replicate a step `check_fn` performs.

Fix (one file, mono.rs): both re-entries now call a shared
`unify_body_against_declared_ret` that mirrors `check_fn`'s closing
`unify(&ret_ty, &body_ty, …)` (lib.rs:2498), threading the return-type
solution into the same `subst` the FreeFnCall metas read. For
`mk : (Int) -> Box Float` this pins `a := Float` from the ctor-field
context `(con RawBuf a)`, so the buffer specialises to the registered
`RawBuf_new__Float`. Safe by construction: mono runs on already-checked
code, so this unify can only re-derive the solution check already
proved — it cannot introduce a new failure. The shared helper keeps the
two passes resolving identical `type_args`, so the minted symbol matches
the Phase-3 rewrite target.

Verification: full `cargo test --workspace` green (0 failed across all
suites); new pin green; `intercepts_bijection_with_intrinsic_markers`
green (no intercept/marker change — `RawBuf_new__Float` already
registered); `pre_desugar_validation.rs` untouched. Both CLAUDE.md
lockstep pairs intact. End-to-end: a polymorphic `Series a` over RawBuf
now builds and runs with the model-0007 `(new Series (con Float) n)`
caller surface — the precondition for Series as a pure library
extension.

refs #61

crates/ailang-check/src/mono.rs

@@ -762,6 +762,27 @@ fn apply_subst_and_normalize(
     }
 }
 
+/// Unify a freshly-synthesised function body type against the function's
+/// declared return type, threading the solution into `subst`. Mirrors
+/// `check_fn`'s closing `unify(&ret_ty, &body_ty, …)` (lib.rs:2498) and
+/// is the single site both mono synth re-entries
+/// ([`collect_mono_targets`] and [`collect_residuals_ordered`]) call, so
+/// they cannot drift on how a result-only callee forall var (whose only
+/// pin is the declared return type — e.g. `RawBuf.new`'s element type)
+/// gets resolved before the free-fn arm reads it. A non-`Type::Fn`
+/// `inner_ty` is a no-op (both callers early-return on it before reaching
+/// the synth, so this is unreachable in practice; kept total for safety).
+fn unify_body_against_declared_ret(
+    inner_ty: &Type,
+    body_ty: &Type,
+    subst: &mut crate::Subst,
+) -> Result<()> {
+    if let Type::Fn { ret, .. } = inner_ty {
+        crate::unify(ret, body_ty, subst)?;
+    }
+    Ok(())
+}
+
 pub fn collect_mono_targets(
     f: &AstFnDef,
     module_name: &str,
@@ -834,7 +855,7 @@ pub fn collect_mono_targets(
     // empty loop-stack (any `Term::Loop` pushes its own frame as the
     // walk descends).
     let mut loop_stack: Vec<Vec<(String, crate::Type)>> = Vec::new();
-    crate::synth(
+    let body_ty = crate::synth(
         &f.body,
         &env,
         &mut locals,
@@ -848,6 +869,24 @@ pub fn collect_mono_targets(
         &mut warnings_discarded,
         &mut crate::linearity::LetBinderTypes::new(),
     )?;
+    // Unify the synthesised body type against the declared return type,
+    // mirroring `check_fn`'s final `unify(&ret_ty, &body_ty, …)`
+    // (lib.rs:2498). synth is bottom-up and only equates a result-only
+    // forall var of a callee with the function's declared return type at
+    // this boundary: e.g. `mk : (Int) -> Box Float` whose body allocates
+    // `(new RawBuf n)` (desugared to `(app RawBuf.new n)`) where
+    // `RawBuf.new : forall a. (Int) -> RawBuf a` — `a` is never pinned
+    // by an argument, so the free-fn-call meta for `RawBuf.new` stays
+    // unbound through the body walk and the free-fn arm below would
+    // Unit-default it (minting the unregistered `RawBuf_new__Unit`).
+    // Threading the return type into the same `subst` the FreeFnCall
+    // metas are read from pins `a := Float` from the ctor-field context
+    // `(con RawBuf a)` of the result `Box Float`. The pre-mono typecheck
+    // already proved this unifies; here we only need its solution to flow
+    // into the mono substitution. `collect_residuals_ordered` applies the
+    // identical unification so both passes resolve the same `type_args`
+    // and the minted symbol matches the Phase-3 rewrite target.
+    unify_body_against_declared_ret(&inner_ty, &body_ty, &mut subst)?;
 
     // Filter residuals to fully-concrete ones; look up
     // defining_module via the registry.
@@ -1617,7 +1656,7 @@ pub(crate) fn collect_residuals_ordered(
     // empty loop-stack (any `Term::Loop` pushes its own frame as the
     // walk descends).
     let mut loop_stack: Vec<Vec<(String, crate::Type)>> = Vec::new();
-    crate::synth(
+    let body_ty = crate::synth(
         &f.body,
         &env,
         &mut locals,
@@ -1631,6 +1670,13 @@ pub(crate) fn collect_residuals_ordered(
         &mut warnings_discarded,
         &mut crate::linearity::LetBinderTypes::new(),
     )?;
+    // Mirror `collect_mono_targets`'s body-against-declared-ret
+    // unification (see the comment there). Both passes must thread the
+    // return type into `subst` identically so a result-only callee
+    // forall var (e.g. `RawBuf.new`'s element) resolves to the same
+    // concrete type in both — otherwise this pass's rewrite target would
+    // disagree with the symbol `collect_mono_targets` minted.
+    unify_body_against_declared_ret(&inner_ty, &body_ty, &mut subst)?;
 
     // Build two per-channel slot lists — one for class-method
     // residuals, one for poly-free-fn observations —