Skip to content

Closures capturing heap-allocated values produce invalid WASM (nested-closure case is a narrow instance) #514

@aallan

Description

@aallan

Summary

Nested closures (a closure returned from inside another closure's body) fail WASM validation with a type-mismatch error, even when there is no variable capture across the nesting boundary.

Reproducer

public fn build_2d(@Unit -> @Int)
  requires(true) ensures(true) effects(pure)
{
  let @Array<Array<Int>> = array_map(
    array_range(0, 3),
    fn(@Int -> @Array<Int>) effects(pure) {
      array_map(
        array_range(0, 3),
        fn(@Int -> @Int) effects(pure) { @Int.0 * 2 }
      )
    }
  );
  nat_to_int(array_length(@Array<Array<Int>>.0))
}

vera check and vera compile succeed. vera run fails:

Caused by:
  0: WebAssembly translation error
  1: Invalid input WebAssembly code at offset 1529: type mismatch: expected i64, found i32

Variant: with capture

Same failure shape with an outer binding captured inside the nested closure:

let @Array<Array<Int>> = array_map(
  array_range(0, 3),
  fn(@Int -> @Array<Int>) effects(pure) {
    array_map(
      array_range(0, 3),
      fn(@Int -> @Int) effects(pure) { @Int.0 + @Int.1 }  -- @Int.1 captures outer row
    )
  }
);

Offset 1536 instead of 1529, but same type-mismatch class.

Workaround

Extract the inner closure into a named top-level helper and pass the captured values as explicit parameters. One level of nesting per array_map/array_fold/etc., never nest two closures directly.

private fn fill_row(@Int -> @Array<Int>)
  requires(true) ensures(true) effects(pure)
{
  array_map(
    array_range(0, 3),
    fn(@Int -> @Int) effects(pure) { @Int.0 + @Int.1 }   -- @Int.1 is now the fn param, not a capture
  )
}

public fn build_2d(@Unit -> @Int)
  requires(true) ensures(true) effects(pure)
{
  let @Array<Array<Int>> = array_map(array_range(0, 3), fill_row);
  nat_to_int(array_length(@Array<Array<Int>>.0))
}

Why this matters

Surfaced by an agent (the same agent whose Stage 11 feedback drove #463/#465/#466/#467/#470/#471/#366) while writing Conway's Game of Life. The natural shape — array_map(rows, fn(row) { array_map(cols, fn(col) { ... }) }) — hits this bug every time. The workaround works but loses the co-location that makes the combinator style readable.

Impacts v0.0.109's closure i32_pair fix (#359) class of work — nested-closure emission wasn't in the #359 repro set.

Initial investigation direction

Offset 1529/1536 in the emitted WASM is in the module's function section, past the imports. Suggests the (result) type descriptor for the outer closure's call_indirect is wrong — probably declaring an i64 return when the inner array_map returns an i32_pair (Array value). Check vera/wasm/closures.py _compile_lifted_closure and the type-descriptor emission in vera/wasm/calls_arrays.py _translate_array_map for how return types are inferred when the closure body is itself an array-returning expression.

Metadata

Metadata

Assignees

No one assigned

    Labels

    bugSomething isn't working

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions