REPL infers lambda-lifted closures standalone, losing captured values' nat arguments #53

New issue

Closed

opened 2026-07-27 11:29:31 +02:00 by st · 0 comments

st commented

2026-07-27 11:29:31 +02:00

Owner

Summary. A function containing an inner let-bound function that captures a value whose type carries a nat argument (i.e. an Array[T, N]) compiles and runs correctly through the library/AOT path, but is mis-compiled by the REPL. The captured array's type is not known while the lifted closure is inferred, so the nat is left symbolic and never reconciled.

Not a nat-inference bug in the ordinary sense: the enclosing function's own nat param is threaded correctly (reading N inside the closure yields 3). And it isn't specific to generics or to module … end — a fully concrete Array[i64, 3] in a bare top-level REPL fn reproduces it.

Root cause. Frontend.run_decls (lib/frontend.ml:96-125) lifts a decl, then calls register_lifted (lib/frontend.ml:73-82), which runs Infer.infer_decl_pre on each lifted lambda independently, before the parent decl is inferred. There is no dependency analysis, so the lambda and its parent are never inferred as one group, and each captured parameter gets a fresh, unconstrained type variable.

The library path does not do this: compile_package (lib/driver/loader.ml:441-455) pools all resolved decls, runs Dependency.analyze_resolved_global_graph, and infers by SCC through Infer.infer_package — so the lifted lambda and its parent land in the same SCC and the capture's type unifies.

Ordinary captures survive the REPL path because their type variables get resolved later, when the parent's go(0) call unifies against the lambda's scheme — plain i64 captures, arithmetic on captures, and captures needing a Show dictionary all work. Nats do not get that second chance: a Core.array_* call inside the lifted body commits its nat argument to an Ir.nat_value during the standalone inference, via nat_value_of (lib/infer.ml:2443-2447), and nothing revisits it once the capture's type is known.

The two branches of nat_value_of produce the two hard failure modes:

| Types.NatVar { nat_hint = Some h; _ } -> Ir.NatWitness h
| Types.NatVar { nat_hint = None; _ } -> Ir.NatLit 0 (* unreachable *)

- NatWitness h assumes the nat is aion, loaded from evidence. The liftedclosure has no such slot, so compilgen.ml:1086) hits failwith "codegen:unknown nat witness N".- The NatLit 0 arm is commented (* le via this path. The array's lengthcompiles as 0, every bounds check frray index out of bounds — nocompile-time signal at all.

Three observed symptoms, all one root:

  ┌──────────────────────────────────┬─────────────────────────────────────────────────────────────┐
  │         Capture used as          │                           Result                            │
  ├──────────────────────────────────┼─────────────────────────────────────────────────────────────┤
  │ Core.array_get(arr, i) /         │ error: codegen: unknown nat witness N                       │
  │ Core.array_len(arr)              │                                                             │
  ├──────────────────────────────────┼─────────────────────────────────────────────────────────────┤
  │ arr[i] := arr[i] * k             │ compiles, then error: array index out of bounds at runtime  │
  ├──────────────────────────────────┼─────────────────────────────────────────────────────────────┤
  │ acc + arr[i]                     │ ambiguous (?, usize): ? needs a Index instance but is       │
  │                                  │ undetermined — the ? is the unresolved capture              │
  ├──────────────────────────────────┼─────────────────────────────────────────────────────────────┤
  │ arr[0] alone                     │ cannot unify Option[?] with i64 — dispatches to the wrong   │
  │                                  │ Index instance                                              │
  └──────────────────────────────────┴─────────────────────────────────────────────────────────────┘

  Minimal repro (no generics, no module wrapper):

  fn f(arr: Array[i64, 3]): usize =
    let go(i: usize): usize = if i >= 1 then Core.array_len(arr) else go(i + 1) end
    in
    go(0)

  f(Array(1, 2, 3))
  → error: codegen: unknown nat witness N. The identical source in a file built with amelie build
  prints the right answer. examples/arrays.aml exercises this exact pattern and passes in
  test_jit_examples, which is why it was never caught — nothing tests the pattern through the REPL.

``` Summary. A function containing an inner let-bound function that captures a value whose type carries a nat argument (i.e. an Array[T, N]) compiles and runs correctly through the library/AOT path, but is mis-compiled by the REPL. The captured array's type is not known while the lifted closure is inferred, so the nat is left symbolic and never reconciled. Not a nat-inference bug in the ordinary sense: the enclosing function's own nat param is threaded correctly (reading N inside the closure yields 3). And it isn't specific to generics or to module … end — a fully concrete Array[i64, 3] in a bare top-level REPL fn reproduces it. Root cause. Frontend.run_decls (lib/frontend.ml:96-125) lifts a decl, then calls register_lifted (lib/frontend.ml:73-82), which runs Infer.infer_decl_pre on each lifted lambda independently, before the parent decl is inferred. There is no dependency analysis, so the lambda and its parent are never inferred as one group, and each captured parameter gets a fresh, unconstrained type variable. The library path does not do this: compile_package (lib/driver/loader.ml:441-455) pools all resolved decls, runs Dependency.analyze_resolved_global_graph, and infers by SCC through Infer.infer_package — so the lifted lambda and its parent land in the same SCC and the capture's type unifies. Ordinary captures survive the REPL path because their type variables get resolved later, when the parent's go(0) call unifies against the lambda's scheme — plain i64 captures, arithmetic on captures, and captures needing a Show dictionary all work. Nats do not get that second chance: a Core.array_* call inside the lifted body commits its nat argument to an Ir.nat_value during the standalone inference, via nat_value_of (lib/infer.ml:2443-2447), and nothing revisits it once the capture's type is known. The two branches of nat_value_of produce the two hard failure modes: | Types.NatVar { nat_hint = Some h; _ } -> Ir.NatWitness h | Types.NatVar { nat_hint = None; _ } -> Ir.NatLit 0 (* unreachable *) - NatWitness h assumes the nat is aion, loaded from evidence. The liftedclosure has no such slot, so compilgen.ml:1086) hits failwith "codegen:unknown nat witness N".- The NatLit 0 arm is commented (* le via this path. The array's lengthcompiles as 0, every bounds check frray index out of bounds — nocompile-time signal at all. Three observed symptoms, all one root: ┌──────────────────────────────────┬─────────────────────────────────────────────────────────────┐ │ Capture used as │ Result │ ├──────────────────────────────────┼─────────────────────────────────────────────────────────────┤ │ Core.array_get(arr, i) / │ error: codegen: unknown nat witness N │ │ Core.array_len(arr) │ │ ├──────────────────────────────────┼─────────────────────────────────────────────────────────────┤ │ arr[i] := arr[i] * k │ compiles, then error: array index out of bounds at runtime │ ├──────────────────────────────────┼─────────────────────────────────────────────────────────────┤ │ acc + arr[i] │ ambiguous (?, usize): ? needs a Index instance but is │ │ │ undetermined — the ? is the unresolved capture │ ├──────────────────────────────────┼─────────────────────────────────────────────────────────────┤ │ arr[0] alone │ cannot unify Option[?] with i64 — dispatches to the wrong │ │ │ Index instance │ └──────────────────────────────────┴─────────────────────────────────────────────────────────────┘ Minimal repro (no generics, no module wrapper): fn f(arr: Array[i64, 3]): usize = let go(i: usize): usize = if i >= 1 then Core.array_len(arr) else go(i + 1) end in go(0) f(Array(1, 2, 3)) → error: codegen: unknown nat witness N. The identical source in a file built with amelie build prints the right answer. examples/arrays.aml exercises this exact pattern and passes in test_jit_examples, which is why it was never caught — nothing tests the pattern through the REPL. ```