Typechecker normalization of type-level expressions

[iljakuklic]

Background

The typechecker currently performs NbE evaluation only for type-level computation (comparing types in val_eq, instantiating dependent Pi closures). It does not normalize arithmetic expressions in terms — those remain as App(Prim::Add, ...) nodes in the core IR and are only reduced by the staging evaluator.

This is fine for the current prototype, but will become load-bearing once dependent types are in use. Consider a type like:

Vec(u32, n + 1)

The typechecker needs to be able to normalize n + 1 (and reason about its relationship to other size expressions) in order to typecheck programs that use Vec.

The wrapping semantics question

The meta-evaluator now uses wrapping arithmetic (matching Wasm's i32/i64) for phase coherence between fn and code fn. However, wrapping semantics are a poor fit for size indices: Vec(u32, 255 + 1) silently producing a 0-element vector would be surprising and unsafe.

This suggests that size indices may want a separate integer type — perhaps an unbounded Nat, or a large fixed-width type treated as a proof-irrelevant index — with distinct (non-wrapping, or checked) arithmetic semantics. This is a common pattern in dependently-typed languages (Agda's ℕ, Idris's Nat).

Open questions

• Should size indices use a dedicated Nat-like type, or a fixed-width integer with non-wrapping semantics?
• If a separate type, how does it relate to object-level integer types? (Lifting, coercions, bounded proofs?)
• How does normalization interact with the existing NbE evaluator — does size arithmetic share the same evaluator, or get a separate reduction strategy?
• What normal forms are needed for the typechecker to decide type equality of expressions like Vec(A, m + n) vs Vec(A, n + m)?

Relationship to phase polymorphism

With phase polymorphism, a function quantifying over a size n : ??? and returning Vec(A, n) needs the size type to be well-behaved at both meta and object phase. This further constrains the design.

[iljakuklic]

Design clarification

The intended design is:

• u32, u64, etc. — phase-polymorphic integers with wrapping semantics, available at both meta and object level. A single function body can be instantiated at either phase.
• nat (or similar name) — meta-only unbounded natural number, used for size indices, loop counts, proofs, etc. Not available at object level. No wrapping.

The motivation for keeping u32 etc. phase-polymorphic: a function like a cryptographic hash can be written once and used at both phases. For example, in a sparse Merkle tree, the empty-subtree hashes at every level are constants — they can be generated at compile time by staging the hash function with known inputs. But as real data arrives, the same hash function needs to operate on runtime values. Phase polymorphism lets you write it once.

So the phase structure is roughly:

              meta only     meta + object
unbounded:      nat           —
fixed-width:     —           u8, u16, u32, u64

nat is the right type for Vec sizes and proof-relevant indices. u32/u64 are the right type for data that needs to exist at runtime (hashes, field elements, etc.) but may also be computed at compile time.

This also means the normalization question splits cleanly: size arithmetic on nat needs to be decidable (for type equality of Vec(A, m + n) vs Vec(A, n + m)), while arithmetic on u32 etc. just needs to be evaluable (wrapping, for staging).