@@ -177,13 +177,21 @@ let parse_file (face : Affinescript.Face.face) path =
     CLI used the process CWD as [current_dir], so compiling `src/Main.affine`
     could not find a sibling `src/Helper.affine` even though the module
     loader already supported relative sibling paths (#642). *)
-let loader_config_for_file path =
+let loader_config_for_file ?prog path =
   let absolute_path =
     if Filename.is_relative path then Filename.concat (Sys.getcwd ()) path
     else path
   in
   let config = Affinescript.Module_loader.default_config () in
-  { config with current_dir = Filename.dirname absolute_path }
+  let mod_path =
+    Option.bind prog (fun (p : Affinescript.Ast.program) ->
+      Option.map (List.map (fun (id : Affinescript.Ast.ident) -> id.name))
+        p.prog_module)
+  in
+  { config with
+    current_dir =
+      Affinescript.Module_loader.module_root_dir
+        ~file_dir:(Filename.dirname absolute_path) mod_path }
 
 (** Type-check a file.  With [--json], emits a structured diagnostic
     report on stderr. *)
@@ -196,7 +204,7 @@ let check_file face json path =
     let resolve_refs = ref [] in
     begin try
       let prog = parse_with_face face path in
-      let loader_config = loader_config_for_file path in
+      let loader_config = loader_config_for_file ~prog path in
       let loader = Affinescript.Module_loader.create loader_config in
       (match Affinescript.Resolve.resolve_program_with_loader prog loader with
       | Error (e, span) ->
@@ -244,7 +252,7 @@ let check_file face json path =
   end else begin
     try
       let prog = parse_with_face face path in
-      let loader_config = loader_config_for_file path in
+      let loader_config = loader_config_for_file ~prog path in
       let loader = Affinescript.Module_loader.create loader_config in
       (match Affinescript.Resolve.resolve_program_with_loader prog loader with
       | Error (e, _span) ->
@@ -294,7 +302,7 @@ let eval_file face json path =
     let add d = diags := d :: !diags in
     begin try
       let prog = parse_with_face face path in
-      let loader_config = loader_config_for_file path in
+      let loader_config = loader_config_for_file ~prog path in
       let loader = Affinescript.Module_loader.create loader_config in
       (match Affinescript.Resolve.resolve_program_with_loader prog loader with
       | Error (e, span) ->
@@ -316,7 +324,8 @@ let eval_file face json path =
           | Error (err, span) ->
             add (Affinescript.Json_output.of_quantity_error (err, span))
           | Ok () ->
-            (match Affinescript.Interp.eval_program prog with
+            (match Affinescript.Interp.eval_program
+                     (Affinescript.Module_loader.flatten_imports loader prog) with
             | Ok env ->
               (* Auto-call main() if defined — entry point for TEA apps and scripts *)
               (match Affinescript.Value.lookup_env "main" env with
@@ -337,7 +346,7 @@ let eval_file face json path =
   end else begin
     try
       let prog = parse_with_face face path in
-      let loader_config = loader_config_for_file path in
+      let loader_config = loader_config_for_file ~prog path in
       let loader = Affinescript.Module_loader.create loader_config in
       (match Affinescript.Resolve.resolve_program_with_loader prog loader with
       | Error (e, _span) ->
@@ -365,7 +374,8 @@ let eval_file face json path =
               (Affinescript.Face.format_quantity_error face err);
             `Error (false, "Quantity error")
           | Ok () ->
-            (match Affinescript.Interp.eval_program prog with
+            (match Affinescript.Interp.eval_program
+                     (Affinescript.Module_loader.flatten_imports loader prog) with
             | Ok env ->
               (* Auto-call main() if defined — entry point for TEA apps and scripts *)
               (match Affinescript.Value.lookup_env "main" env with
@@ -519,7 +529,7 @@ let compile_file face json wasm_gc vscode_ext vscode_adapter vscode_no_lc
     let add d = diags := d :: !diags in
     begin try
       let prog = parse_with_face face path in
-      let loader_config = loader_config_for_file path in
+      let loader_config = loader_config_for_file ~prog path in
       let loader = Affinescript.Module_loader.create loader_config in
       (match Affinescript.Resolve.resolve_program_with_loader prog loader with
       | Error (e, span) ->
@@ -744,7 +754,7 @@ let compile_file face json wasm_gc vscode_ext vscode_adapter vscode_no_lc
   end else begin
     try
       let prog = parse_with_face face path in
-      let loader_config = loader_config_for_file path in
+      let loader_config = loader_config_for_file ~prog path in
       let loader = Affinescript.Module_loader.create loader_config in
       (match Affinescript.Resolve.resolve_program_with_loader prog loader with
       | Error (e, _span) ->
@@ -1037,7 +1047,7 @@ let lint_file face json path =
     let add d = diags := d :: !diags in
     begin try
       let prog = parse_with_face face path in
-      let loader_config = loader_config_for_file path in
+      let loader_config = loader_config_for_file ~prog path in
       let loader = Affinescript.Module_loader.create loader_config in
       (match Affinescript.Resolve.resolve_program_with_loader prog loader with
       | Error (e, span) ->
@@ -1057,7 +1067,7 @@ let lint_file face json path =
   end else begin
     try
       let prog = parse_with_face face path in
-      let loader_config = loader_config_for_file path in
+      let loader_config = loader_config_for_file ~prog path in
       let loader = Affinescript.Module_loader.create loader_config in
       (match Affinescript.Resolve.resolve_program_with_loader prog loader with
       | Error (e, _span) ->
@@ -1096,7 +1106,7 @@ let compile_to_wasm_module face path
   : (Affinescript.Wasm.wasm_module, string) Result.t =
   try
     let prog = parse_with_face face path in
-    let loader_config = loader_config_for_file path in
+    let loader_config = loader_config_for_file ~prog path in
     let loader = Affinescript.Module_loader.create loader_config in
     match Affinescript.Resolve.resolve_program_with_loader prog loader with
     | Error (e, _span) ->
@@ -1160,7 +1170,7 @@ let verify_file face path =
   let face = resolve_face face path in
   try
     let prog = parse_with_face face path in
-    let loader_config = loader_config_for_file path in
+    let loader_config = loader_config_for_file ~prog path in
     let loader = Affinescript.Module_loader.create loader_config in
     (match Affinescript.Resolve.resolve_program_with_loader prog loader with
     | Error (e, _span) ->
@@ -1688,7 +1698,7 @@ let preview_cafe_cmd =
 let run_pipeline_for_query face path =
   try
     let prog = parse_with_face face path in
-    let loader_config = loader_config_for_file path in
+    let loader_config = loader_config_for_file ~prog path in
     let loader = Affinescript.Module_loader.create loader_config in
     match Affinescript.Resolve.resolve_program_with_loader prog loader with
     | Error (e, _span) ->
 
@@ -87,7 +87,7 @@ Results were consistent, but they do not prove CI is green.
 | Memory reclamation. try/catch.
 
 | Bun-ESM (`lib/codegen_deno.ml`)
-| Basic programs are correct. A `return` inside a match arm returns 100 instead of 99 (IIFE at `:1575`). aLib conformance is 100 of 103 vectors.
+| Basic programs are correct. A `return` inside a match arm is correct in a `let` initializer, a function or lambda tail, and nested statement position; as an argument or operand it is refused at compile time rather than miscompiled (H2, 2026-11-09). aLib conformance is 100 of 103 vectors.
 | —
 | —
 
@@ -202,7 +202,7 @@ Results were consistent, but they do not prove CI is green.
 All were observed by RUN unless marked otherwise. The maps confirm that H1–H4 and H9 are absent from `docs/SOUNDNESS.adoc`. H5–H8, H10, H12 and H13 were not checked against the ledger. H11 already has a drafted issue (`issues-drafts/06`, referenced from the AFFIRMATION). H14, H15 and H19 belong to typed-wasm, not the AffineScript ledger.
 
 . H1. Interpreter early `return` has no non-local exit (`lib/interp.ml:262`).
-. H2. Bun-ESM `return` in expression position is lowered as an IIFE (`lib/codegen_deno.ml:1575`).
+. H2. Bun-ESM `return` in expression position is lowered as an IIFE (`lib/codegen_deno.ml:1575`). *Narrowed 2026-11-09:* `let` initializers and function and lambda tails are now lowered to statements, so the `return` leaves the function; a match used as an argument or operand with a `return` in an arm is refused loudly. Anchor: `test/test_module_root_flatten.ml`.
 . H3. The JS-text backend drops block returns (`lib/js_codegen.ml`). The Lua backend emits invalid code.
 . H4. Non-exhaustive match compiles to "return 0" on core WASM.
 . H5. Effect rows are not checked against performed operations or callee rows.
@@ -220,9 +220,9 @@ All were observed by RUN unless marked otherwise. The maps confirm that H1–H4
 . H17. The lexer accepts the bad escape `\q`, and an empty `match` parses (conformance invalid cases 010 and 011).
 . H18. The interpreter fails when dereferencing refs returned through calls ("Expected reference type"). The session lead reproduced this on two #554 fixtures.
 . H19 (typed-wasm). No L5 index guard: `get_player_hp(0,150)` reads an adjacent region. `where` constraints are discarded. Malformed `session` blocks are silently ignored.
-. H20. `Face.render_ty` is not injective, contrary to the F-5 model. On the Js face `List[Option[Int]]` and `Option[List[Int]]` both render as `List[Int] | null`; on Cafe both render as `List[Int]?`. The greedy `Option\[\(.*\)\]` regex in `lib/face.ml` causes it (RUN, by calling the built library).
-. H21. The Coq proof gate fails open on assertions outside the printed theorems' dependency cone. A planted `Admitted` false lemma and a planted `Axiom False` both passed a replica of `coq-proof-gate.yml` (RUN). The gate also never re-runs when the `lib/*.ml` files the models describe change.
-. H22. The staged Agda under `proposals/` (23 files) passes under the canonical flags, but nothing checks it: `tools/check-proofs.sh --agda` reports SKIP, not failure, when `AFFINESCRIPT_ECHO_TYPES_DIR` or `AGDA_STDLIB` is unset, and no workflow or dune rule calls it. No echo-types commit is pinned.
+. H20 (found and fixed 2026-11-09, checking and running metadatastician/kyq). A module file found for `A.B` that declares `module A;` was accepted as `A.B`, so `use A.Nonexistent::*` type-checked and imported `A`'s exports; it is now a `ModuleDeclMismatch` load error. Anchor: `test/test_module_root_flatten.ml`.
+. H21 (found and fixed 2026-11-09). `eval` ran the unflattened program, so no imported function was bound at run time; flattening also emitted a selected function before the private helpers it calls and carried no helpers for glob or plain imports. `eval` now flattens, every import kind carries its helpers, and they are emitted in the imported module's declaration order. Anchor: `test/test_module_root_flatten.ml`.
+. H22 (found and fixed 2026-11-09). The interpreter had no `++` on arrays and no `==`/`!=` beyond Int, Float, String and Bool, though the checker accepts them; it now uses the structural `Value.value_eq`. H7 (`let mut`) is unchanged. Anchor: `test/test_module_root_flatten.ml`.
 
 == 2. Target architecture
 
 
@@ -523,6 +523,15 @@ let rec expr_contains_return (e : expr) : bool =
   | ExprUnary (_, x) -> expr_contains_return x
   | ExprApp (f, args) ->
     expr_contains_return f || List.exists expr_contains_return args
+  (* A `return` in a match arm (`Err(e) => return Err(e)`) is the common
+     early-exit shape; without this arm it was invisible, and the Bun-ESM
+     backend compiled it into a `return` from the match's IIFE instead of
+     from the function. *)
+  | ExprMatch { em_scrutinee; em_arms } ->
+    expr_contains_return em_scrutinee
+    || List.exists (fun arm ->
+         (match arm.ma_guard with Some g -> expr_contains_return g | None -> false)
+         || expr_contains_return arm.ma_body) em_arms
   | _ -> false
 
 and block_contains_return (blk : block) : bool =
 
@@ -1434,6 +1434,15 @@ let enter_fn_scope ctx (params : param list) : codegen_ctx =
    call whose head is a known [extern fn] lowers via {!deno_builtins}.
    ============================================================================ *)
 
+(* Fresh temporaries for `let` initializers lowered to statements. *)
+let let_tmp_counter = ref 0
+
+(* Initializer shapes {!gen_assign_tail} can lower to statements. *)
+let rec lowers_to_statements = function
+  | ExprSpan (e, _) -> lowers_to_statements e
+  | ExprMatch _ | ExprIf _ | ExprBlock _ -> true
+  | _ -> false
+
 (** Render an expression as JavaScript using the names and host in [ctx].
     Lambdas are synchronous arrows; known qualified constructors refer to
     their emitted bindings. Nested statements can update integer tracking.
@@ -1587,8 +1596,15 @@ let rec gen_expr ctx (expr : expr) : string =
          the enclosing async context: inside a synthesised (async) method,
          `(x) => (await ...)` is a SyntaxError in browsers — Bun's parser
          happens to accept it, which hid the bug. *)
-      "((" ^ String.concat ", " ps ^ ") => "
-      ^ gen_expr { ctx with in_async = false } elam_body ^ ")"
+      let lctx = { ctx with in_async = false } in
+      if lowers_to_statements elam_body && expr_contains_return elam_body then
+        (* A `return` in the body returns from the lambda: emit a block
+           body so it is not swallowed by an IIFE (see {!gen_match}). *)
+        "((" ^ String.concat ", " ps ^ ") => { "
+        ^ gen_return_tail lctx elam_body ^ " })"
+      else
+        "((" ^ String.concat ", " ps ^ ") => "
+        ^ gen_expr lctx elam_body ^ ")"
   | ExprTry { et_body; et_catch; et_finally } ->
       gen_try ctx et_body et_catch et_finally
   | ExprVariant (ty, ctor) ->
@@ -1651,6 +1667,21 @@ and gen_pattern ctx (pat : pattern) : string =
   | PatOr (p, _)   -> gen_pattern ctx p
 
 and gen_match ctx scrutinee arms =
+  (* As an expression the match is an IIFE, so a `return` in an arm would
+     leave the IIFE, not the enclosing function, and the function would
+     carry on with the returned value as the match's result: silently wrong
+     output.  `let` initializers and tail/statement position are lowered to
+     statements and handled correctly; any other position (an argument, an
+     operand) is refused here rather than miscompiled. *)
+  if List.exists (fun arm ->
+       expr_contains_return arm.ma_body
+       || (match arm.ma_guard with
+           | Some g -> expr_contains_return g | None -> false)) arms
+  then
+    failwith
+      "a `return` inside a match arm is not supported when the match is \
+       used as a sub-expression (an argument or operand); bind the match \
+       to a `let` first";
   let scrutinee_str = gen_expr ctx scrutinee in
   let scrut_var = "__scrut" in
   let rec gen_arms = function
@@ -1844,6 +1875,58 @@ and gen_match_stmt ctx scrut arms =
   in
   "{ const " ^ sv ^ " = " ^ gen_expr ctx scrut ^ "; " ^ arms_js arms ^ " }"
 
+(* Statements that evaluate [e] and hand its value to [sink], which turns a
+   JS expression into a statement (`x = v;` or `return v;`).  A `return`
+   anywhere along a tail path stays a real function return, which the IIFE
+   expression form cannot express.  Used for `let` initializers and for
+   function and lambda bodies that contain an early return. *)
+and gen_tail_to ctx (sink : string -> string) e =
+  match e with
+  | ExprSpan (inner, _) -> gen_tail_to ctx sink inner
+  | ExprReturn _ -> gen_stmt_expr ctx e
+  | ExprBlock blk ->
+      let b = Buffer.create 64 in
+      List.iter (fun s ->
+        Buffer.add_string b (gen_stmt ctx s);
+        Buffer.add_char b ' ') blk.blk_stmts;
+      (match blk.blk_expr with
+       | Some tail -> Buffer.add_string b (gen_tail_to ctx sink tail)
+       | None -> Buffer.add_string b (sink "Unit"));
+      "{ " ^ Buffer.contents b ^ " }"
+  | ExprIf { ei_cond; ei_then; ei_else } ->
+      let elseb = match ei_else with
+        | Some el -> gen_tail_to ctx sink el
+        | None -> sink "Unit"
+      in
+      "if (" ^ gen_expr ctx ei_cond ^ ") { " ^ gen_tail_to ctx sink ei_then
+      ^ " } else { " ^ elseb ^ " }"
+  | ExprMatch { em_scrutinee; em_arms } ->
+      incr let_tmp_counter;
+      let sv = Printf.sprintf "__scrut_%d" !let_tmp_counter in
+      let rec arms_js = function
+        | [] -> "throw new Error(\"non-exhaustive match\");"
+        | arm :: rest ->
+            let cond = gen_pattern_test sv arm.ma_pat in
+            let binds = gen_pattern_bindings sv arm.ma_pat in
+            let guard = match arm.ma_guard with
+              | Some g -> " && (" ^ gen_expr ctx g ^ ")" | None -> "" in
+            "if (" ^ cond ^ guard ^ ") { " ^ binds
+            ^ gen_tail_to ctx sink arm.ma_body ^ " } else " ^ arms_js rest
+      in
+      "{ const " ^ sv ^ " = " ^ gen_expr ctx em_scrutinee ^ "; "
+      ^ arms_js em_arms ^ " }"
+  | other -> sink (gen_expr ctx other)
+
+and gen_assign_tail ctx target e =
+  gen_tail_to ctx (fun v -> target ^ " = " ^ v ^ ";") e
+
+(* A function or lambda body's tail: statements when it holds an early
+   return, else the plain `return <expr>;`. *)
+and gen_return_tail ctx e =
+  if lowers_to_statements e && expr_contains_return e then
+    gen_tail_to ctx (fun v -> "return " ^ v ^ ";") e
+  else "return " ^ gen_expr ctx e ^ ";"
+
 and gen_try_stmt ctx body catch finally =
   let b = gen_stmt_seq ctx body in
   let c = match catch with
@@ -1874,8 +1957,22 @@ and gen_stmt ctx (stmt : stmt) : string =
       gen_expr ctx sl_value ^ ";"
   | StmtLet { sl_pat; sl_value; sl_mut; sl_quantity = _; sl_ty = _ } ->
       let kw = if sl_mut then "let" else "const" in
-      let js = kw ^ " " ^ gen_pattern ctx sl_pat ^ " = "
-               ^ gen_expr ctx sl_value ^ ";" in
+      let js =
+        if lowers_to_statements sl_value && expr_contains_return sl_value then begin
+          (* `let x = match e { A(v) => v, B(err) => return f(err) };`
+             As an expression the match is an IIFE, and the arm's `return`
+             left the IIFE, not the function: the IIFE's result was then
+             bound to `x` and the function carried on.  Lower the
+             initializer to statements that assign a temporary, so the
+             `return` is a real function return. *)
+          incr let_tmp_counter;
+          let tmp = Printf.sprintf "__let_tmp_%d" !let_tmp_counter in
+          "let " ^ tmp ^ "; " ^ gen_assign_tail ctx tmp sl_value ^ " "
+          ^ kw ^ " " ^ gen_pattern ctx sl_pat ^ " = " ^ tmp ^ ";"
+        end else
+          kw ^ " " ^ gen_pattern ctx sl_pat ^ " = "
+          ^ gen_expr ctx sl_value ^ ";"
+      in
       (* Track an [Int]-bound name for the rest of this body (#478). A
          block statement's scope is the enclosing function, which
          {!enter_fn_scope} already bounds, so no restore is needed here. *)
@@ -1961,11 +2058,11 @@ let visibility_is_public = function
 let gen_body ctx (fb : fn_body) : unit =
   match fb with
   | FnExpr e ->
-      emit_line ctx ("return " ^ gen_expr ctx e ^ ";")
+      emit_line ctx (gen_return_tail ctx e)
   | FnBlock block ->
       List.iter (fun s -> emit_line ctx (gen_stmt ctx s)) block.blk_stmts;
       (match block.blk_expr with
-       | Some e -> emit_line ctx ("return " ^ gen_expr ctx e ^ ";")
+       | Some e -> emit_line ctx (gen_return_tail ctx e)
        | None   -> ())
   | FnExtern -> ()