diff --git a/crates/ailang-check/src/mono.rs b/crates/ailang-check/src/mono.rs
index e98f99e..2349e64 100644
--- a/crates/ailang-check/src/mono.rs
+++ b/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 —