fix(resolve): remove b895374 seed band-aid; recursive cross-module resolution (#138)

lib/resolve.ml

@@ -88,9 +88,14 @@ let seed_builtins (symbols : Symbol.t) : unit =
   let defc name =
     let _ = Symbol.define symbols name SKConstructor Span.dummy Public in ()
   in
-  defc "Some"; defc "None"; defc "Ok"; defc "Err";
+  (* #138: Some/None/Ok/Err are no longer seeded as flat builtins — the
+     stdlib now reaches them through the proper prelude/module path
+     (`use prelude::{Some, None, Ok, Err}`; prelude.affine itself
+     defines `Option`/`Result`). Removing the b895374 band-aid keeps it
+     from becoming load-bearing. *)
   (* Interpreter builtin exception variant, pattern-matched in try/catch
-     arms by the honest stdlib (testing.affine, result.affine). *)
+     arms by the honest stdlib (testing.affine, result.affine). It has
+     no module home by design, so it remains a genuine builtin. *)
   defc "RuntimeError"
 
 (** Create a new resolution context, pre-seeded with builtins. *)
@@ -554,41 +559,9 @@ let resolve_program (program : program) : (context, resolve_error * Span.t) Resu
   | Ok () -> Ok ctx
   | Error e -> Error e
 
-(** Resolve and type-check a loaded module's symbols *)
-let resolve_and_typecheck_module (loaded_mod : Module_loader.loaded_module)
-    : (Symbol.t * Typecheck.context) result =
-  let prog = Module_loader.get_program loaded_mod in
-  let symbols = Symbol.create () in
-  seed_builtins symbols;
-  let mod_ctx = { symbols; current_module = []; imports = []; references = [] } in
-
-  (* Pass 1: forward-declare every top-level name (#135 slice 11). *)
-  pre_register_program mod_ctx prog;
-  (* Pass 2: resolve all declaration bodies. *)
-  let* () = List.fold_left (fun acc decl ->
-    match acc with
-    | Error e -> Error e
-    | Ok () -> resolve_decl mod_ctx decl
-  ) (Ok ()) prog.prog_decls in
-
-  (* Type-check all declarations. Seed builtin schemes (len, arithmetic,
-     Some/None/…) exactly as Typecheck.check_program does for the top-level
-     program — the manual check_decl fold below otherwise leaves an imported
-     module's use of builtins as "Unbound variable". *)
-  let type_ctx = Typecheck.create_context symbols in
-  Typecheck.register_builtins type_ctx;
-  let type_result = List.fold_left (fun acc decl ->
-    match acc with
-    | Error e -> Error e
-    | Ok () -> Typecheck.check_decl type_ctx decl
-  ) (Ok ()) prog.prog_decls in
-
-  match type_result with
-  | Ok () -> Ok (symbols, type_ctx)
-  | Error type_err ->
-    (* Convert type error to resolve error *)
-    let msg = Typecheck.show_type_error type_err in
-    Error (ImportError ("Type checking failed: " ^ msg), Span.dummy)
+(* [resolve_and_typecheck_module] is defined below, mutually recursive
+   with [resolve_imports_with_loader], so that an imported module's own
+   `use` imports are resolved through the loader (no flat builtin seed). *)
 
 (** Look up a scheme for [sym] in [source_types] (sym_id-keyed) first, then
     fall back to [source_name_types] (name-keyed). The fallback is needed
@@ -664,7 +637,52 @@ let import_specific_items
   ) (Ok ()) items
 
 (** Resolve imports in a program using module loader *)
-let resolve_imports_with_loader
+let rec resolve_and_typecheck_module
+    (loader : Module_loader.t)
+    (loaded_mod : Module_loader.loaded_module)
+    : (Symbol.t * Typecheck.context) result =
+  let prog = Module_loader.get_program loaded_mod in
+  let symbols = Symbol.create () in
+  seed_builtins symbols;
+  let mod_ctx = { symbols; current_module = []; imports = []; references = [] } in
+  (* Type-check context, created up front so this module's own imports
+     can populate its scheme maps before its decls are checked. *)
+  let type_ctx = Typecheck.create_context symbols in
+  Typecheck.register_builtins type_ctx;
+
+  (* Resolve THIS module's own `use` imports first (#138 / #128
+     coherence). A dependency module reaches Some/None/Ok/Err and its
+     sibling modules through its own `use prelude::{...}` /
+     `use string::{...}`, not a flat builtin seed. Mutually recursive
+     with the loader; the stdlib import graph is an acyclic DAG
+     (max depth io -> string -> prelude). *)
+  let* () =
+    resolve_imports_with_loader mod_ctx type_ctx loader prog.prog_imports
+  in
+
+  (* Pass 1: forward-declare every top-level name (#135 slice 11). *)
+  pre_register_program mod_ctx prog;
+  (* Pass 2: resolve all declaration bodies. *)
+  let* () = List.fold_left (fun acc decl ->
+    match acc with
+    | Error e -> Error e
+    | Ok () -> resolve_decl mod_ctx decl
+  ) (Ok ()) prog.prog_decls in
+
+  (* Type-check all declarations. *)
+  let type_result = List.fold_left (fun acc decl ->
+    match acc with
+    | Error e -> Error e
+    | Ok () -> Typecheck.check_decl type_ctx decl
+  ) (Ok ()) prog.prog_decls in
+
+  match type_result with
+  | Ok () -> Ok (symbols, type_ctx)
+  | Error type_err ->
+    let msg = Typecheck.show_type_error type_err in
+    Error (ImportError ("Type checking failed: " ^ msg), Span.dummy)
+
+and resolve_imports_with_loader
     (ctx : context)
     (type_ctx : Typecheck.context)
     (loader : Module_loader.t)
@@ -678,7 +696,7 @@ let resolve_imports_with_loader
       begin match Module_loader.load_module loader path_strs with
         | Ok loaded_mod ->
           (* Resolve and type-check the module *)
-          begin match resolve_and_typecheck_module loaded_mod with
+          begin match resolve_and_typecheck_module loader loaded_mod with
             | Ok (mod_symbols, mod_type_ctx) ->
               let alias_str = Option.map (fun id -> id.name) alias in
               import_resolved_symbols ctx.symbols
@@ -704,7 +722,7 @@ let resolve_imports_with_loader
       begin match Module_loader.load_module loader path_strs with
         | Ok loaded_mod ->
           (* Resolve and type-check the module *)
-          begin match resolve_and_typecheck_module loaded_mod with
+          begin match resolve_and_typecheck_module loader loaded_mod with
             | Ok (mod_symbols, mod_type_ctx) ->
               import_specific_items ctx.symbols
                 type_ctx.Typecheck.var_types
@@ -728,7 +746,7 @@ let resolve_imports_with_loader
       begin match Module_loader.load_module loader path_strs with
         | Ok loaded_mod ->
           (* Resolve and type-check the module *)
-          begin match resolve_and_typecheck_module loaded_mod with
+          begin match resolve_and_typecheck_module loader loaded_mod with
             | Ok (mod_symbols, mod_type_ctx) ->
               (* Import all public symbols *)
               Hashtbl.iter (fun _id sym ->

lib/typecheck.ml

@@ -639,13 +639,6 @@ let rec synth (ctx : context) (expr : expr) : ty result =
         let* () = unify_or_err then_ty else_ty in
         Ok then_ty
       | None ->
-        let () =
-          if ty_to_string then_ty <> ty_to_string ty_unit then
-            Format.eprintf "If without else returns %s; then=%s cond=%s\n%!"
-              (ty_to_string then_ty) (expr_summary ei_then) (expr_summary ei_cond)
-          else
-            ()
-        in
         (* No else branch: result is Unit *)
         let* () = unify_or_err then_ty ty_unit in
         Ok ty_unit
@@ -1284,46 +1277,25 @@ let register_builtins (ctx : context) : unit =
      (issue #122 v2.5). Concrete String/Char types; the Deno-ESM backend
      lowers each to a JS intrinsic. char ::= TCon "Char". *)
   let ty_char = TCon "Char" in
+  (* Option/Result type constructors, used only to spell the *types* of
+     builtin signatures (parse_int, read_file, …) — not the value
+     constructors. *)
   let opt t = TApp (TCon "Option", [t]) in
-  (* Option / Result value constructors — seeded as polymorphic builtin
-     schemes so the honest stdlib resolves without the legacy prelude
-     (mirrors the Resolve.create_context constructor seeding). Codegen
-     (codegen_deno.ml:111-114) already provides the Some/None/Ok/Err
-     runtime; this is purely the front-end type side. A user/prelude
-     `type Option`/`type Result` decl shadows these. Issue #122. *)
   let res a b = TApp (TCon "Result", [a; b]) in
+  (* #138: Some/None/Ok/Err are no longer seeded as polymorphic builtin
+     schemes. The stdlib now resolves them through the proper module
+     path — prelude.affine declares `type Option`/`type Result` and
+     every consumer does `use prelude::{Some, None, Ok, Err}`. Removing
+     the b895374 / #122 front-end band-aid keeps it from becoming
+     load-bearing now that real resolution + the module model have
+     landed (stdlib 19/19). Codegen still provides the runtime. *)
   let fresh_named () =
     let tv = fresh_tyvar 0 in
     let v = (match tv with
       | TVar r -> (match !r with Unbound (v, _) -> v | _ -> assert false)
       | _ -> assert false) in
     (v, tv)
   in
-  let (v_none, t_none) = fresh_named () in
-  bind_scheme ctx "None"
-    { sc_tyvars = [(v_none, Types.KType)]; sc_effvars = []; sc_rowvars = [];
-      sc_body = opt t_none };
-  Hashtbl.replace ctx.constructor_env "None" (opt t_none);
-  let (v_some, t_some) = fresh_named () in
-  let some_ty = TArrow (t_some, QOmega, opt t_some, EPure) in
-  bind_scheme ctx "Some"
-    { sc_tyvars = [(v_some, Types.KType)]; sc_effvars = []; sc_rowvars = [];
-      sc_body = some_ty };
-  Hashtbl.replace ctx.constructor_env "Some" some_ty;
-  let (v_oka, t_oka) = fresh_named () in
-  let (v_okb, t_okb) = fresh_named () in
-  let ok_ty = TArrow (t_oka, QOmega, res t_oka t_okb, EPure) in
-  bind_scheme ctx "Ok"
-    { sc_tyvars = [(v_oka, Types.KType); (v_okb, Types.KType)];
-      sc_effvars = []; sc_rowvars = []; sc_body = ok_ty };
-  Hashtbl.replace ctx.constructor_env "Ok" ok_ty;
-  let (v_erra, t_erra) = fresh_named () in
-  let (v_errb, t_errb) = fresh_named () in
-  let err_ty = TArrow (t_errb, QOmega, res t_erra t_errb, EPure) in
-  bind_scheme ctx "Err"
-    { sc_tyvars = [(v_erra, Types.KType); (v_errb, Types.KType)];
-      sc_effvars = []; sc_rowvars = []; sc_body = err_ty };
-  Hashtbl.replace ctx.constructor_env "Err" err_ty;
   (* [RuntimeError(String)] is the interpreter's builtin exception variant
      (see [Interp]: panics surface as [VVariant ("RuntimeError", VString
      msg)]). The honest stdlib pattern-matches it in [try/catch] arms

stdlib/io.affine

@@ -20,7 +20,8 @@
 //   show(value)             -> String
 //   time_now()              -> Float              (CPU time in seconds)
 
-// Cross-module import (ADR-011: explicit `use module::{...}`)
+// Cross-module imports (ADR-011: explicit `use module::{...}`)
+use prelude::{ Option, Result, Some, None, Ok, Err };
 use string::{ split, join };
 
 // ============================================================================

stdlib/string.affine

@@ -18,6 +18,9 @@
 //   int_to_char(n)        -> Char          (ASCII code point to character)
 //   show(v)               -> String        (any value to debug string)
 
+// Cross-module import (ADR-011: explicit `use module::{...}`)
+use prelude::{ Option, Some, None };
+
 // ============================================================================
 // String inspection
 // ============================================================================

stdlib/testing.affine

@@ -8,6 +8,9 @@
 //
 // Depends on builtins: show, panic, time_now
 
+// Cross-module import (ADR-011: explicit `use module::{...}`)
+use prelude::{ Option, Result, Some, None, Ok, Err };
+
 // ============================================================================
 // Assertions
 // ============================================================================

test/test_e2e.ml

@@ -3426,9 +3426,13 @@ let test_angle_nested_gtgtgt () =
        {|fn f(o: Option<Option<Result<Int, String>>>) -> Int { return 0; }|})
 
 let test_angle_nested_return_pos () =
+  (* Exercises the nested generic *in return position* (the point of this
+     test) without constructing Ok/None — those live in prelude and are
+     reached via `use prelude::{...}`, not a flat builtin seed (#138).
+     Mirrors the param-position sibling tests above. *)
   Alcotest.(check bool) "-> Result<Option<T>, E> nested in return position" true
     (parse_check_passes
-       {|fn f() -> Result<Option<Int>, String> { return Ok(None); }|})
+       {|fn f(r: Result<Option<Int>, String>) -> Result<Option<Int>, String> { return r; }|})
 
 (* Non-regression: a real right-shift expression must still be one GTGT,
    not split, since GTGT is grammatical there. *)