bug: conversion never δ-unfolds meta globals — type-level definitions are unusable

[iljakuklic]

Problem

Value::Global is a permanent neutral: globals are "not inlined during type-checking" and apply_many leaves global applications stuck. Meta-level conversion therefore has no δ-reduction, so a definition can never be used transparently in types:

def sel(b: u1) -> Type = match b { 0 => u32, 1 => u64 };
def j() -> sel(0) = 5;   -- sel(0) is never convertible to u32

(Today this fails even earlier with "unbound variable sel" because signatures are elaborated with an empty globals table — that's #72. But fixing #72 alone is not enough: with the global visible, sel(0) still evaluates to a stuck App(Global, [0]) and val_eq compares it syntactically, so sel(0) vs u32 still fails.)

Why it matters

In the 2LTT reference design, meta-level definitional equality includes δ (the reference implementation evaluates let-bound and top-level definitions via the environment). Type families defined as meta functions — the flagship staged-programming pattern (Vec : Nat1 → ⇑U0 → ⇑U0, EvalTy : Ty → ⇑U0, …) — are unusable without it. Splic local lets already unfold correctly (values stored in the context); only globals are opaque.

Fix directions

• Store the elaborated body (or its evaluated value) in GlobalEntry::Meta and unfold in eval — simplest.
• Or glued/lazy unfolding (keep both the neutral and the unfolded value) for better error messages and performance, as in elaboration-zoo's glued evaluator — more work, better long-term.

Related: #72 (globals in signatures), #48 (type-level normalization), #91 (globals stuck during NbE noted as an open question).