while body quotation allows stack pollution #233

New issue

Closed

opened 2026-01-11 00:17:14 +00:00 by navicore · 1 comment

navicore commented

2026-01-11 00:17:14 +00:00

(Migrated from github.com)

Summary

The while combinator does not properly verify that its body quotation is stack-neutral. A quotation like [1] that pushes a value should be rejected at compile time, but currently passes type checking.

Expected Behavior

: bad-while ( -- ) true [ 1 ] while ;  // Should fail: body pushes Int

Should produce a compile-time error like:

Type error: while body must be stack-neutral, but pushes Int

Actual Behavior

The code compiles without error. Each loop iteration pushes an extra value onto the stack.

Root Cause

The row variable unification is too permissive. When unifying the body quotation's effect ( ..a -- ..a Int ) against the expected ( ..a -- ..a ), the row variable absorbs the extra Int instead of rejecting it.

Discovered while testing #231 (Quotation effect verification)
Test: test_while_body_stack_neutral_gap in typechecker.rs documents this gap

## Summary The `while` combinator does not properly verify that its body quotation is stack-neutral. A quotation like `[1]` that pushes a value should be rejected at compile time, but currently passes type checking. ## Expected Behavior ```seq : bad-while ( -- ) true [ 1 ] while ; // Should fail: body pushes Int ``` Should produce a compile-time error like: ``` Type error: while body must be stack-neutral, but pushes Int ``` ## Actual Behavior The code compiles without error. Each loop iteration pushes an extra value onto the stack. ## Root Cause The row variable unification is too permissive. When unifying the body quotation's effect `( ..a -- ..a Int )` against the expected `( ..a -- ..a )`, the row variable absorbs the extra `Int` instead of rejecting it. ## Related - Discovered while testing #231 (Quotation effect verification) - Test: `test_while_body_stack_neutral_gap` in typechecker.rs documents this gap

navicore commented

2026-01-11 00:42:19 +00:00

(Migrated from github.com)

https://github.com/navicore/patch-seq/pull/236