Optional stack-effect checking and basic type discipline

[tetsuo-cpp]

Summary

Add optional verification that stack depth (and, where known, int vs float bit-interpretation) is consistent at control-flow merges and word boundaries.

Motivation

The stack is intentionally untyped (!forth.stack as i64 cells; floats are bit patterns). The programmer ensures type safety. That is flexible but makes mistakes silent: using + instead of F+, or unbalanced IF branches that leave different depths, often produce wrong results rather than compile errors.

Control-flow structure is already validated (#21). Stack effects are not.

Proposed levels

Level 1 — Depth checking (high value, do first)

• Annotate or infer stack depth delta per word/op
• Require matching depths on IF/ELSE arms, loop back-edges, and word exit points
• Error: IF branches leave different stack depths (then=2, else=1)

Level 2 — Optional sort tracking

• Track a coarse tag per slot: int / float / addr / unknown
• Warn or error on F+ consuming int, + consuming float, etc.
• Escape hatch: explicit bitcast words or UNSAFE regions

Level 3 — Effect comments as checked contracts (optional)

: dot  ( addr addr n -- f )  ... ;

Parse stack comments and verify against inferred effects (Forth tradition).

Acceptance criteria

• Depth checker behind a flag or on-by-default for obvious imbalances
• LIT tests for unbalanced IF/loop/word effects
• Document inference rules and false-positive policy
• (Stretch) coarse int/float warnings

Non-goals

• Full dependent types or MLIR type redesign of !forth.stack in v1
• Runtime type tags on the GPU stack

Related

• Control-flow validation (Add validation for mismatched control flow words #21 closed)
• Stack flattening (depth analysis is shared machinery)
• Debug-mode runtime checks (separate issue)