Skip to content

fix(types): check no longer stack-overflows on functions returning T[k] - #74

Open
JonathanTurnock wants to merge 2 commits into
mainfrom
lean-v1
Open

JonathanTurnock wants to merge 2 commits into
mainfrom
lean-v1

Conversation

@JonathanTurnock

Copy link
Copy Markdown
Contributor

Problem

luabox check aborted the whole run with a stack overflow on ordinary Lua. Seen on Penlight (pl/data.lua) and lazy.nvim (lua/lazy/core/plugin.lua, lua/lazy/manage/semver.lua). Minimal repro:

local S = {}
function S.f(key)
  return S[key]
end

S[key] widens to every value of S, and f is one of them, so f's inferred returns contain f itself. reify_func had no cycle guard (unlike reify_shape), so turning f into a Ty recursed forever.

Fix

  • d43e2bf: added a cycle guard to reify_func.
  • fd0703e: the guard alone left the acyclic case factorial. With n sibling functions that each return S[k], check took 5.2 s at n=8. Replaced the stack with a depth counter (MAX_NESTED_FUNC_RETURNS = 1): a function's returns are spelled out only at the outermost level.
siblings before after
8 5.2 s 0.08 s
30 — 0.12 s
100 — 2.7 s (unavoidable size of 100 unions of 100 members each)

Trade-off

A returned closure's own returns reify as unknown. A factory now hovers as fun(): fun() instead of fun(): fun(): integer. Same-file call checking walks the inference graph and is unaffected. A cross-file consumer calling M.make()() now sees unknown for the inner result. The fd0703e commit message says call checking is unaffected; that holds only for same-file calls. The cap is one constant if we'd rather pay the cost.

Verification

  • 3 new tests in luabox-types: the self-reference, 12 siblings (would never finish under factorial cost), and the pinned depth-cap display.
  • cargo test --workspace: 3078 passed, 0 failed. clippy -D warnings and fmt --check are clean.
  • Real code with the release build: Penlight finishes (strict: 492 errors, almost all from strict mode's handling of untyped values; non-strict: 0 errors, 58 warnings). lazy.nvim finishes with 0 errors and 355 warnings. All 7 examples/ still check clean.

🤖 Generated with Claude Code

JonathanTurnock and others added 2 commits September 23, 2026 19:39
…ial returns

A function stored in a table that returns a dynamic index into that table
(`function S.f(k) return S[k] end`) has itself among its returns: `S[k]`
widens to every value of `S`, `f` included. `reify_func` had no cycle guard
(unlike `reify_shape`), so reifying `f` recursed until the stack overflowed
and aborted the whole `luabox check` run. Seen on real code: Penlight
`pl/data.lua`, lazy.nvim `core/plugin.lua` and `manage/semver.lua`.

A function reached again through its own returns now reifies with no
returns, the way a shape cycle cuts off at the catch-all table.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
The cycle guard alone left the acyclic case exponential: n sibling
functions that each return `S[k]` reach one another in every order, so
`check` took 5.2 s at 8 siblings and grew factorially. A depth counter
replaces the stack and bounds both cases: a function's returns are spelled
out only at the outermost level (n=30: 1.2 s -> 0.12 s; n=100: 2.7 s).

Trade-off: a returned closure's own returns reify as unknown, so a factory
hovers as `fun(): fun()` rather than `fun(): fun(): integer`. Call checking
walks the inference graph, not reified types, and is unaffected.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant