Store binding phase in Ctx for per-variable stage checking

[iljakuklic]

Context

The reference 2LTT implementation (AndrasKovacs/staged) stores the stage/phase of each binding in the elaboration context and checks it against the current elaboration stage when a variable is looked up (guardStage). This prevents using a meta-phase variable directly in object-phase code (and vice versa) — you must go through splice/quote.

Currently, phase misuse is caught indirectly because meta-phase and object-phase types are distinct (e.g., u32(meta) vs u32(object)), so type mismatches surface eventually. However, this is less precise than the reference and could produce confusing error messages.

Proposed change

Add phases: Vec<Phase> to Ctx and thread the binding phase through:

• push_local(name, ty, phase) / push_local_val(name, ty_val, phase) / push_let_binding(name, ty_val, expr_val, phase)
• pop_local: also pop from phases
• lookup_local returns (Ix, &Value, Phase)
• infer Var arm: check that the variable's binding phase matches the current elaboration phase

Scope

~7 production call sites and ~40 test call sites need updating. The test changes are mechanical (pass the appropriate Phase::Meta or Phase::Object matching the type being pushed).

Why it was deferred

This was identified during the infer-returns-type refactor (3dd87b3) but deferred because the current phase-in-types approach catches most misuse and the change touches many call sites without affecting correctness of existing tests.

🤖 Generated with Claude Code