Type checker doesn't understand divergent early-exit patterns #134

New issue

Closed

opened 2025-12-29 20:23:57 +00:00 by navicore · 1 comment

navicore commented

2025-12-29 20:23:57 +00:00

(Migrated from github.com)

Problem

The type checker rejects valid error-checking code in infinite loops because it doesn't understand divergent early-exit patterns.

Example

This pattern is rejected:

: store-loop ( Int Int Int Int -- )
  2 pick chan.receive             # ( parent my count pending msg success )
  not if drop store-loop then     # exit early if receive failed
  match
    ...
  end
;

Error:

Error: if/else branches have incompatible stack effects:
  then branch produces: ..rest
  else branch produces: (..rest Int Int Int Int T$5)

Analysis

The pattern not if drop X-loop then is an early-exit that:

Checks the success flag (not)
If failed: drops the placeholder value and tail-calls back to the loop (diverges)
If succeeded: continues to process the message

The type checker sees:

then branch: calls store-loop which never returns (divergent)
implicit else branch: continues with the message on stack

These should be compatible because the then branch diverges (never produces a value), so it's compatible with any continuation. In type theory, the bottom type (⊥) is a subtype of everything.

Proposed Solution

The type checker should recognize that when an if branch contains only a tail-call to a function with a compatible signature that never returns, it's a divergent branch and compatible with any else branch.

This pattern is common in:

Actor loops (CSP/message-passing)
Event loops
Any infinite loop with error handling

Workaround

Currently we must drop the success flag without checking (chan.receive drop), which triggers lint warnings and hides potential errors.

Issue #132 (error handling audit)
PR #133

## Problem The type checker rejects valid error-checking code in infinite loops because it doesn't understand divergent early-exit patterns. ## Example This pattern is rejected: ```seq : store-loop ( Int Int Int Int -- ) 2 pick chan.receive # ( parent my count pending msg success ) not if drop store-loop then # exit early if receive failed match ... end ; ``` Error: ``` Error: if/else branches have incompatible stack effects: then branch produces: ..rest else branch produces: (..rest Int Int Int Int T$5) ``` ## Analysis The pattern `not if drop X-loop then` is an early-exit that: 1. Checks the success flag (`not`) 2. If failed: drops the placeholder value and tail-calls back to the loop (diverges) 3. If succeeded: continues to process the message The type checker sees: - **then branch**: calls `store-loop` which never returns (divergent) - **implicit else branch**: continues with the message on stack These should be compatible because the `then` branch diverges (never produces a value), so it's compatible with any continuation. In type theory, the bottom type (⊥) is a subtype of everything. ## Proposed Solution The type checker should recognize that when an `if` branch contains only a tail-call to a function with a compatible signature that never returns, it's a divergent branch and compatible with any `else` branch. This pattern is common in: - Actor loops (CSP/message-passing) - Event loops - Any infinite loop with error handling ## Workaround Currently we must drop the success flag without checking (`chan.receive drop`), which triggers lint warnings and hides potential errors. ## Related - Issue #132 (error handling audit) - PR #133

navicore commented

2025-12-30 01:38:39 +00:00

(Migrated from github.com)

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