ITADN

let bindings of pair-represented Future payloads (let @Future<String>) are check-green but E602-skip

#1039Openaallan 创建于 2026-07-16
bug
A
aallancommented
## Summary `let @Future<String> = async("hello");` — and by extension any `Future<T>` whose payload is pair-represented (String/Array) bound via `let` — is check+verify green but E602-skips the enclosing function ("let binding type 'Future<String>' has no WASM representation"). The direct (non-alias) spelling; unrelated to the #1031/#1037 alias canonicalization (verified: identical with and without that fix). Found by PR #1038's family mapping: it blocks the `await(Future<String>)` match-scrutinee shape upstream, with no match required to reproduce. ## Root cause direction `Future<T>` is representation-transparent (#841), so `Future<String>` is an `i32_pair` — but the let-binding translator's pair handling appears keyed to the known pair type names rather than the canonical WASM type, so the transparent wrapper falls to the no-representation skip. Same check-green→E602 family as the fixed #1006/#1031/#1037/#1038. ## Repro ```vera public fn go(@Unit -> @Int) requires(true) ensures(true) effects(<Async>) { let @Future<String> = async("hello"); let @String = await(@Future<String>.0); string_length(@String.0) } ``` `vera check`/`verify` green; `vera run` → E602 skip → unknown func.
0 条评论