diff --git a/.gitignore b/.gitignore
index 623ef91..b2eaf88 100644
--- a/.gitignore
+++ b/.gitignore
@@ -4,3 +4,4 @@ scratch/
 posts/
 .claude/settings.local.json
 .claude/worktrees/
+.opencode/package-lock.json
diff --git a/cli/src/main.rs b/cli/src/main.rs
index 6e4d324..565a674 100644
--- a/cli/src/main.rs
+++ b/cli/src/main.rs
@@ -35,24 +35,28 @@ fn stage(file: &PathBuf) -> Result<()> {
     let source = std::fs::read_to_string(file)
         .with_context(|| format!("failed to read file: {}", file.display()))?;
 
+    // Names arena: owns all identifier strings for the lifetime of the pipeline.
+    let names_arena = bumpalo::Bump::new();
+
     // Parse into src_arena; the arena lives until elaboration finishes
     // consuming the AST, then is dropped.
-    let src_arena = bumpalo::Bump::new();
-    let lexer = lexer::Lexer::new(&source);
-    let mut parser = parser::Parser::new(lexer, &src_arena);
+    let ast_arena = bumpalo::Bump::new();
+    let lexer = lexer::Lexer::new(&source, &names_arena);
+    let mut parser = parser::Parser::new(lexer, &ast_arena);
     let program = parser.parse_program().context("failed to parse program")?;
+    drop(source);
 
     // Elaborate/typecheck into core_arena; the arena lives until staging
     // finishes consuming the core IR, then is dropped.
     let core_arena = bumpalo::Bump::new();
     let core_program =
         checker::elaborate_program(&core_arena, &program).context("failed to elaborate program")?;
-    drop(src_arena);
+    drop(ast_arena);
 
     // Unstage into out_arena; core_arena is no longer needed after this.
-    let out_arena = bumpalo::Bump::new();
-    let staged =
-        staging::unstage_program(&out_arena, &core_program).context("failed to stage program")?;
+    let staged_arena = bumpalo::Bump::new();
+    let staged = staging::unstage_program(&staged_arena, &core_program)
+        .context("failed to stage program")?;
     drop(core_arena);
 
     // Print the staged result, then out_arena is dropped at end of scope.
diff --git a/compiler/src/checker/ctx.rs b/compiler/src/checker/ctx.rs
index 760e2d0..eb91ec1 100644
--- a/compiler/src/checker/ctx.rs
+++ b/compiler/src/checker/ctx.rs
@@ -12,31 +12,31 @@ use crate::core::{self, value};
 /// Phase is not stored here — it is threaded as an argument to `infer`/`check`
 /// since it shifts locally when entering `Quote`, `Splice`, or `Lift`.
 #[derive(Debug)]
-pub struct Ctx<'core, 'globals> {
+pub struct Ctx<'names, 'core, 'globals> {
     /// Arena for allocating core terms
     pub arena: &'core bumpalo::Bump,
 
     /// Local variable names (oldest first), for error messages.
-    pub names: Vec<&'core core::Name>,
+    pub names: Vec<&'names core::Name>,
 
     /// Evaluation environment (oldest first): values of locals.
     /// `env[env.len() - 1 - ix]` = value of `Var(Ix(ix))`.
-    pub env: value::Env<'core>,
+    pub env: value::Env<'names, 'core>,
 
     /// Types of locals as semantic values (oldest first).
     /// `types[types.len() - 1 - ix]` = type of `Var(Ix(ix))`.
-    pub types: Vec<value::Value<'core>>,
+    pub types: Vec<value::Value<'names, 'core>>,
 
     /// Global function types: name -> Pi term.
     /// Storing `&Term` (always a Pi) unifies type lookup for globals and locals.
     /// Borrowed independently of the arena so the map can live on the stack.
-    pub globals: &'globals HashMap<&'core core::Name, &'core core::Pi<'core>>,
+    pub globals: &'globals HashMap<&'names core::Name, &'core core::Pi<'names, 'core>>,
 }
 
-impl<'core, 'globals> Ctx<'core, 'globals> {
+impl<'names, 'core, 'globals> Ctx<'names, 'core, 'globals> {
     pub const fn new(
         arena: &'core bumpalo::Bump,
-        globals: &'globals HashMap<&'core core::Name, &'core core::Pi<'core>>,
+        globals: &'globals HashMap<&'names core::Name, &'core core::Pi<'names, 'core>>,
     ) -> Self {
         Ctx {
             arena,
@@ -48,7 +48,7 @@ impl<'core, 'globals> Ctx<'core, 'globals> {
     }
 
     /// Allocate a term in the core arena
-    pub fn alloc(&self, term: core::Term<'core>) -> &'core core::Term<'core> {
+    pub fn alloc(&self, term: core::Term<'names, 'core>) -> &'core core::Term<'names, 'core> {
         self.arena.alloc(term)
     }
 
@@ -67,14 +67,18 @@ impl<'core, 'globals> Ctx<'core, 'globals> {
 
     /// Push a local variable onto the context, given its type as a term.
     /// Evaluates the type term in the current environment.
-    pub fn push_local(&mut self, name: &'core core::Name, ty: &'core core::Term<'core>) {
+    pub fn push_local(&mut self, name: &'names core::Name, ty: &'core core::Term<'names, 'core>) {
         let ty_val = value::eval(self.arena, &self.env, ty);
         self.push_local_val(name, ty_val);
     }
 
     /// Push a local variable onto the context, given its type as a Value.
     /// The variable itself is a fresh rigid (neutral) variable — use for lambda/pi params.
-    pub fn push_local_val(&mut self, name: &'core core::Name, ty_val: value::Value<'core>) {
+    pub fn push_local_val(
+        &mut self,
+        name: &'names core::Name,
+        ty_val: value::Value<'names, 'core>,
+    ) {
         self.env.push(value::Value::Rigid(self.depth().as_lvl()));
         self.types.push(ty_val);
         self.names.push(name);
@@ -84,9 +88,9 @@ impl<'core, 'globals> Ctx<'core, 'globals> {
     /// Use for `let x = e` bindings so that dependent references to `x` evaluate correctly.
     pub fn push_let_binding(
         &mut self,
-        name: &'core core::Name,
-        ty_val: value::Value<'core>,
-        expr_val: value::Value<'core>,
+        name: &'names core::Name,
+        ty_val: value::Value<'names, 'core>,
+        expr_val: value::Value<'names, 'core>,
     ) {
         self.env.push(expr_val);
         self.types.push(ty_val);
@@ -104,8 +108,8 @@ impl<'core, 'globals> Ctx<'core, 'globals> {
     /// Searches from the most recently pushed variable inward to handle shadowing.
     pub fn lookup_local(
         &self,
-        name: &'_ core::Name,
-    ) -> Option<(de_bruijn::Ix, &value::Value<'core>)> {
+        name: &core::Name,
+    ) -> Option<(de_bruijn::Ix, &value::Value<'names, 'core>)> {
         for (i, local_name) in self.names.iter().enumerate().rev() {
             if *local_name == name {
                 let ix = de_bruijn::Lvl::new(i).ix_at(self.depth());
@@ -120,17 +124,20 @@ impl<'core, 'globals> Ctx<'core, 'globals> {
     }
 
     /// Helper to create a lifted type [[T]]
-    pub fn lift_ty(&self, inner: &'core core::Term<'core>) -> &'core core::Term<'core> {
+    pub fn lift_ty(
+        &self,
+        inner: &'core core::Term<'names, 'core>,
+    ) -> &'core core::Term<'names, 'core> {
         self.arena.alloc(core::Term::Lift(inner))
     }
 
     /// Evaluate a term in the current environment.
-    pub fn eval(&self, term: &'core core::Term<'core>) -> value::Value<'core> {
+    pub fn eval(&self, term: &'core core::Term<'names, 'core>) -> value::Value<'names, 'core> {
         value::eval(self.arena, &self.env, term)
     }
 
     /// Quote a value back to a term at the current depth.
-    pub fn quote_val(&self, val: &value::Value<'core>) -> &'core core::Term<'core> {
+    pub fn quote_val(&self, val: &value::Value<'names, 'core>) -> &'core core::Term<'names, 'core> {
         value::quote(self.arena, self.depth(), val)
     }
 }
diff --git a/compiler/src/checker/elaborate.rs b/compiler/src/checker/elaborate.rs
index 66dfd54..55507f1 100644
--- a/compiler/src/checker/elaborate.rs
+++ b/compiler/src/checker/elaborate.rs
@@ -9,19 +9,18 @@ use super::Ctx;
 use super::infer;
 
 /// Elaborate one function's signature into a `Pi` (the globals table entry).
-fn elaborate_sig<'src, 'core>(
+fn elaborate_sig<'names, 'ast, 'core>(
     arena: &'core bumpalo::Bump,
-    func: &ast::Function<'src>,
-) -> Result<&'core core::Pi<'core>> {
-    let empty_globals = HashMap::new();
+    func: &ast::Function<'names, 'ast>,
+) -> Result<&'core core::Pi<'names, 'core>> {
+    let empty_globals: HashMap<&'names core::Name, &'core core::Pi<'names, 'core>> = HashMap::new();
     let mut ctx = Ctx::new(arena, &empty_globals);
 
-    let params: &'core [(&'core core::Name, &'core core::Term<'core>)] = arena
+    let params: &'core [(&'names core::Name, &'core core::Term<'names, 'core>)] = arena
         .alloc_slice_try_fill_iter(func.params.iter().map(|p| -> Result<_> {
-            let param_name = core::Name::new(arena.alloc_str(p.name.as_str()));
             let (param_ty, _) = infer::infer(&mut ctx, func.phase, p.ty)?;
-            ctx.push_local(param_name, param_ty);
-            Ok((param_name, param_ty))
+            ctx.push_local(p.name, param_ty);
+            Ok((p.name, param_ty))
         }))?;
 
     let body_ty = infer::check(
@@ -39,14 +38,14 @@ fn elaborate_sig<'src, 'core>(
 }
 
 /// Pass 1: collect all top-level function signatures into a globals table.
-pub fn collect_signatures<'src, 'core>(
+pub fn collect_signatures<'names, 'ast, 'core>(
     arena: &'core bumpalo::Bump,
-    program: &ast::Program<'src>,
-) -> Result<HashMap<&'core core::Name, &'core core::Pi<'core>>> {
-    let mut globals: HashMap<&'core core::Name, &'core core::Pi<'core>> = HashMap::new();
+    program: &ast::Program<'names, 'ast>,
+) -> Result<HashMap<&'names core::Name, &'core core::Pi<'names, 'core>>> {
+    let mut globals: HashMap<&'names core::Name, &'core core::Pi<'names, 'core>> = HashMap::new();
 
     for func in program.functions {
-        let name = core::Name::new(arena.alloc_str(func.name.as_str()));
+        let name = func.name;
 
         ensure!(
             !globals.contains_key(&name),
@@ -62,14 +61,14 @@ pub fn collect_signatures<'src, 'core>(
 }
 
 /// Pass 2: elaborate all function bodies with the full globals table available.
-fn elaborate_bodies<'src, 'core>(
+fn elaborate_bodies<'names, 'ast, 'core>(
     arena: &'core bumpalo::Bump,
-    program: &ast::Program<'src>,
-    globals: &HashMap<&'core core::Name, &'core core::Pi<'core>>,
-) -> Result<core::Program<'core>> {
-    let functions: &'core [core::Function<'core>] =
+    program: &ast::Program<'names, 'ast>,
+    globals: &HashMap<&'names core::Name, &'core core::Pi<'names, 'core>>,
+) -> Result<core::Program<'names, 'core>> {
+    let functions: &'core [core::Function<'names, 'core>] =
         arena.alloc_slice_try_fill_iter(program.functions.iter().map(|func| -> Result<_> {
-            let name = core::Name::new(arena.alloc_str(func.name.as_str()));
+            let name = func.name;
             let pi = *globals.get(&name).expect("signature missing from pass 1");
 
             // Build a fresh context borrowing the stack-owned globals map.
@@ -93,10 +92,10 @@ fn elaborate_bodies<'src, 'core>(
 }
 
 /// Elaborate the entire program in two passes
-pub fn elaborate_program<'core>(
+pub fn elaborate_program<'names, 'core>(
     arena: &'core bumpalo::Bump,
-    program: &ast::Program<'_>,
-) -> Result<core::Program<'core>> {
+    program: &ast::Program<'names, '_>,
+) -> Result<core::Program<'names, 'core>> {
     let globals = collect_signatures(arena, program)?;
     elaborate_bodies(arena, program, &globals)
 }
diff --git a/compiler/src/checker/infer.rs b/compiler/src/checker/infer.rs
index f5ad85f..53264e2 100644
--- a/compiler/src/checker/infer.rs
+++ b/compiler/src/checker/infer.rs
@@ -12,11 +12,14 @@ use super::{Ctx, builtin_prim_ty};
     clippy::too_many_lines,
     reason = "large match over all surface term variants"
 )]
-pub fn infer<'src, 'core>(
-    ctx: &mut Ctx<'core, '_>,
+pub fn infer<'names, 'ast, 'core>(
+    ctx: &mut Ctx<'names, 'core, '_>,
     phase: Phase,
-    term: &'src ast::Term<'src>,
-) -> Result<(&'core core::Term<'core>, value::Value<'core>)> {
+    term: &'ast ast::Term<'names, 'ast>,
+) -> Result<(
+    &'core core::Term<'names, 'core>,
+    value::Value<'names, 'core>,
+)> {
     match term {
         // ------------------------------------------------------------------ Var
         ast::Term::Var(name) => {
@@ -44,7 +47,6 @@ pub fn infer<'src, 'core>(
             }
             // Globals — bare reference without call
             if let Some(pi) = ctx.globals.get(name).copied() {
-                let name = core::Name::new(ctx.arena.alloc_str(name.as_str()));
                 let ty = value::eval_pi(ctx.arena, &[], pi);
                 return Ok((ctx.alloc(core::Term::Global(name)), ty));
             }
@@ -90,8 +92,9 @@ pub fn infer<'src, 'core>(
             );
 
             // Check each arg against its domain (evaluated with prior arg values).
-            let mut arg_vals: Vec<value::Value<'core>> = Vec::with_capacity(args.len());
-            let mut core_args: Vec<&'core core::Term<'core>> = Vec::with_capacity(args.len());
+            let mut arg_vals: Vec<value::Value<'names, 'core>> = Vec::with_capacity(args.len());
+            let mut core_args: Vec<&'core core::Term<'names, 'core>> =
+                Vec::with_capacity(args.len());
             for (i, (arg, (_, domain_cl))) in args.iter().zip(vpi.params.iter()).enumerate() {
                 let domain_val = value::inst_n(ctx.arena, domain_cl, &arg_vals);
                 let core_arg = check_val(ctx, phase, arg, domain_val)
@@ -178,13 +181,12 @@ pub fn infer<'src, 'core>(
             );
             let depth_before = ctx.depth();
 
-            let mut elaborated_params: Vec<(&'core core::Name, &'core core::Term<'core>)> =
+            let mut elaborated_params: Vec<(&'names core::Name, &'core core::Term<'names, 'core>)> =
                 Vec::new();
             for p in *params {
-                let param_name = core::Name::new(ctx.arena.alloc_str(p.name.as_str()));
                 let param_ty = check_universe(ctx, Phase::Meta, p.ty)?;
-                elaborated_params.push((param_name, param_ty));
-                ctx.push_local(param_name, param_ty);
+                elaborated_params.push((p.name, param_ty));
+                ctx.push_local(p.name, param_ty);
             }
 
             let core_ret_ty = check_universe(ctx, Phase::Meta, ret_ty)?;
@@ -212,14 +214,13 @@ pub fn infer<'src, 'core>(
             );
 
             let depth_before = ctx.depth();
-            let mut elaborated_params: Vec<(&'core core::Name, &'core core::Term<'core>)> =
+            let mut elaborated_params: Vec<(&'names core::Name, &'core core::Term<'names, 'core>)> =
                 Vec::new();
 
             for p in *params {
-                let param_name = core::Name::new(ctx.arena.alloc_str(p.name.as_str()));
                 let (param_ty, _) = infer(ctx, Phase::Meta, p.ty)?;
-                elaborated_params.push((param_name, param_ty));
-                ctx.push_local(param_name, param_ty);
+                elaborated_params.push((p.name, param_ty));
+                ctx.push_local(p.name, param_ty);
             }
 
             let (core_body, body_ty) = infer(ctx, phase, body)?;
@@ -325,7 +326,10 @@ pub fn infer<'src, 'core>(
 }
 
 /// Check exhaustiveness of `arms` given the scrutinee type `scrut_ty`.
-fn check_exhaustiveness(scrut_ty: &value::Value<'_>, arms: &[ast::MatchArm<'_>]) -> Result<()> {
+fn check_exhaustiveness(
+    scrut_ty: &value::Value<'_, '_>,
+    arms: &[ast::MatchArm<'_, '_>],
+) -> Result<()> {
     let mut covered_lits: Option<Vec<bool>> = match scrut_ty {
         value::Value::Prim(Prim::IntTy(ty)) => match ty.width {
             IntWidth::U0 => Some(vec![false; 1]),
@@ -362,32 +366,29 @@ fn check_exhaustiveness(scrut_ty: &value::Value<'_>, arms: &[ast::MatchArm<'_>])
 }
 
 /// Elaborate a match pattern into a core pattern.
-fn elaborate_pat<'core>(ctx: &Ctx<'core, '_>, pat: &ast::Pat<'_>) -> core::Pat<'core> {
+fn elaborate_pat<'names>(pat: &ast::Pat<'names>) -> core::Pat<'names> {
     match pat {
         ast::Pat::Lit(n) => core::Pat::Lit(*n),
         ast::Pat::Name(name) => match name.as_str() {
             "_" => core::Pat::Wildcard,
-            s => {
-                let bound = core::Name::new(ctx.arena.alloc_str(s));
-                core::Pat::Bind(bound)
-            }
+            _ => core::Pat::Bind(name),
         },
     }
 }
 
 /// Elaborate a single `let` binding.
-fn elaborate_let<'src, 'core, T, F, G, W>(
-    ctx: &mut Ctx<'core, '_>,
+fn elaborate_let<'names, 'ast, 'core, T, F, G, W>(
+    ctx: &mut Ctx<'names, 'core, '_>,
     phase: Phase,
-    stmt: &'src ast::Let<'src>,
+    stmt: &'ast ast::Let<'names, 'ast>,
     cont: F,
     body_of: G,
     wrap: W,
 ) -> Result<T>
 where
-    F: FnOnce(&mut Ctx<'core, '_>) -> Result<T>,
-    G: FnOnce(&T) -> &'core core::Term<'core>,
-    W: FnOnce(&'core core::Term<'core>, T) -> T,
+    F: FnOnce(&mut Ctx<'names, 'core, '_>) -> Result<T>,
+    G: FnOnce(&T) -> &'core core::Term<'names, 'core>,
+    W: FnOnce(&'core core::Term<'names, 'core>, T) -> T,
 {
     let (core_expr, bind_ty_val) = if let Some(ann) = stmt.ty {
         let (ty, _) = infer(ctx, phase, ann)?;
@@ -404,7 +405,7 @@ where
     let bind_ty_term = ctx.quote_val(&bind_ty_val);
     // Evaluate the bound expression so dependent references to this binding work correctly.
     let expr_val = ctx.eval(core_expr);
-    let bind_name = core::Name::new(ctx.arena.alloc_str(stmt.name.as_str()));
+    let bind_name = stmt.name;
     ctx.push_let_binding(bind_name, bind_ty_val, expr_val);
     let cont_result = cont(ctx);
     ctx.pop_local();
@@ -421,12 +422,15 @@ where
 }
 
 /// Elaborate a sequence of `let` bindings followed by a trailing expression (infer mode).
-fn infer_block<'src, 'core>(
-    ctx: &mut Ctx<'core, '_>,
+fn infer_block<'names, 'ast, 'core>(
+    ctx: &mut Ctx<'names, 'core, '_>,
     phase: Phase,
-    stmts: &'src [ast::Let<'src>],
-    expr: &'src ast::Term<'src>,
-) -> Result<(&'core core::Term<'core>, value::Value<'core>)> {
+    stmts: &'ast [ast::Let<'names, 'ast>],
+    expr: &'ast ast::Term<'names, 'ast>,
+) -> Result<(
+    &'core core::Term<'names, 'core>,
+    value::Value<'names, 'core>,
+)> {
     match stmts {
         [] => infer(ctx, phase, expr),
         [first, rest @ ..] => elaborate_let(
@@ -441,14 +445,14 @@ fn infer_block<'src, 'core>(
 }
 
 /// Elaborate a sequence of `let` bindings followed by a trailing expression (check mode).
-fn check_block_val<'src, 'core>(
-    ctx: &mut Ctx<'core, '_>,
+fn check_block_val<'names, 'ast, 'core>(
+    ctx: &mut Ctx<'names, 'core, '_>,
     phase: Phase,
-    stmts: &'src [ast::Let<'src>],
-    expr: &'src ast::Term<'src>,
-    expected: value::Value<'core>,
-    expected_term: Option<&'core core::Term<'core>>,
-) -> Result<&'core core::Term<'core>> {
+    stmts: &'ast [ast::Let<'names, 'ast>],
+    expr: &'ast ast::Term<'names, 'ast>,
+    expected: value::Value<'names, 'core>,
+    expected_term: Option<&'core core::Term<'names, 'core>>,
+) -> Result<&'core core::Term<'names, 'core>> {
     match stmts {
         [] => check_val_impl(ctx, phase, expr, expected, expected_term),
         [first, rest @ ..] => elaborate_let(
@@ -466,11 +470,11 @@ fn check_block_val<'src, 'core>(
 ///
 /// Equivalent to `check(ctx, phase, term, Type)` for meta phase or
 /// `check(ctx, phase, term, VmType)` for object phase.
-fn check_universe<'src, 'core>(
-    ctx: &mut Ctx<'core, '_>,
+fn check_universe<'names, 'ast, 'core>(
+    ctx: &mut Ctx<'names, 'core, '_>,
     phase: Phase,
-    term: &'src ast::Term<'src>,
-) -> Result<&'core core::Term<'core>> {
+    term: &'ast ast::Term<'names, 'ast>,
+) -> Result<&'core core::Term<'names, 'core>> {
     let universe: &core::Term = match phase {
         Phase::Meta => &core::Term::TYPE,
         Phase::Object => &core::Term::VM_TYPE,
@@ -482,23 +486,23 @@ fn check_universe<'src, 'core>(
 ///
 /// This is a convenience wrapper for callers that have an expected type as a `&Term`.
 /// It also threads the expected term through for dependent-type arm refinement.
-pub fn check<'src, 'core>(
-    ctx: &mut Ctx<'core, '_>,
+pub fn check<'names, 'ast, 'core>(
+    ctx: &mut Ctx<'names, 'core, '_>,
     phase: Phase,
-    term: &'src ast::Term<'src>,
-    expected: &'core core::Term<'core>,
-) -> Result<&'core core::Term<'core>> {
+    term: &'ast ast::Term<'names, 'ast>,
+    expected: &'core core::Term<'names, 'core>,
+) -> Result<&'core core::Term<'names, 'core>> {
     let expected_val = ctx.eval(expected);
     check_val_impl(ctx, phase, term, expected_val, Some(expected))
 }
 
 /// Check `term` against `expected` (as a semantic Value), returning the elaborated core term.
-pub fn check_val<'src, 'core>(
-    ctx: &mut Ctx<'core, '_>,
+pub fn check_val<'names, 'ast, 'core>(
+    ctx: &mut Ctx<'names, 'core, '_>,
     phase: Phase,
-    term: &'src ast::Term<'src>,
-    expected: value::Value<'core>,
-) -> Result<&'core core::Term<'core>> {
+    term: &'ast ast::Term<'names, 'ast>,
+    expected: value::Value<'names, 'core>,
+) -> Result<&'core core::Term<'names, 'core>> {
     check_val_impl(ctx, phase, term, expected, None)
 }
 
@@ -508,13 +512,13 @@ pub fn check_val<'src, 'core>(
     clippy::too_many_lines,
     reason = "large match over all surface term variants"
 )]
-fn check_val_impl<'src, 'core>(
-    ctx: &mut Ctx<'core, '_>,
+fn check_val_impl<'names, 'ast, 'core>(
+    ctx: &mut Ctx<'names, 'core, '_>,
     phase: Phase,
-    term: &'src ast::Term<'src>,
-    expected: value::Value<'core>,
-    expected_term: Option<&'core core::Term<'core>>,
-) -> Result<&'core core::Term<'core>> {
+    term: &'ast ast::Term<'names, 'ast>,
+    expected: value::Value<'names, 'core>,
+    expected_term: Option<&'core core::Term<'names, 'core>>,
+) -> Result<&'core core::Term<'names, 'core>> {
     match term {
         // ------------------------------------------------------------------ Lit
         ast::Term::Lit(n) => match &expected {
@@ -666,12 +670,12 @@ fn check_val_impl<'src, 'core>(
                 vpi.params.len()
             );
 
-            let mut elaborated_params: Vec<(&'core core::Name, &'core core::Term<'core>)> =
+            let mut elaborated_params: Vec<(&'names core::Name, &'core core::Term<'names, 'core>)> =
                 Vec::new();
-            let mut arg_vals: Vec<value::Value<'core>> = Vec::new();
+            let mut arg_vals: Vec<value::Value<'names, 'core>> = Vec::new();
 
             for (p, (_, domain_cl)) in params.iter().zip(vpi.params.iter()) {
-                let param_name = core::Name::new(ctx.arena.alloc_str(p.name.as_str()));
+                let param_name = p.name;
                 let (annotated_ty, _) = infer(ctx, Phase::Meta, p.ty)?;
                 let annotated_ty_val = ctx.eval(annotated_ty);
                 let expected_domain = value::inst_n(ctx.arena, domain_cl, &arg_vals);
@@ -720,38 +724,38 @@ fn check_val_impl<'src, 'core>(
                 _ => None,
             };
 
-            let core_arms: &'core [core::Arm<'core>] =
-                ctx.arena
-                    .alloc_slice_try_fill_iter(arms.iter().map(|arm| -> Result<_> {
-                        let core_pat = elaborate_pat(ctx, &arm.pat);
-
-                        let arm_expected = match (&scrut_refine, &core_pat, expected_term) {
-                            (Some((lvl, int_ty)), core::Pat::Lit(n), Some(ety)) => {
-                                let mut env = ctx.env.clone();
-                                *env.get_mut(lvl.as_usize())
-                                    .expect("scrutinee level must be in scope") =
-                                    value::Value::Lit(*n, *int_ty);
-                                value::eval(ctx.arena, &env, ety)
-                            }
-                            _ => expected.clone(),
-                        };
-
-                        if let Some(bname) = core_pat.bound_name() {
-                            ctx.push_local(bname, scrut_ty_term);
+            let core_arms: &'core [core::Arm<'names, 'core>] = ctx
+                .arena
+                .alloc_slice_try_fill_iter(arms.iter().map(|arm| -> Result<_> {
+                    let core_pat = elaborate_pat(&arm.pat);
+
+                    let arm_expected = match (&scrut_refine, &core_pat, expected_term) {
+                        (Some((lvl, int_ty)), core::Pat::Lit(n), Some(ety)) => {
+                            let mut env = ctx.env.clone();
+                            *env.get_mut(lvl.as_usize())
+                                .expect("scrutinee level must be in scope") =
+                                value::Value::Lit(*n, *int_ty);
+                            value::eval(ctx.arena, &env, ety)
                         }
+                        _ => expected.clone(),
+                    };
 
-                        let arm_result = check_val(ctx, phase, arm.body, arm_expected);
+                    if let Some(bname) = core_pat.bound_name() {
+                        ctx.push_local(bname, scrut_ty_term);
+                    }
 
-                        if core_pat.bound_name().is_some() {
-                            ctx.pop_local();
-                        }
+                    let arm_result = check_val(ctx, phase, arm.body, arm_expected);
+
+                    if core_pat.bound_name().is_some() {
+                        ctx.pop_local();
+                    }
 
-                        let core_body = arm_result?;
-                        Ok(core::Arm {
-                            pat: core_pat,
-                            body: core_body,
-                        })
-                    }))?;
+                    let core_body = arm_result?;
+                    Ok(core::Arm {
+                        pat: core_pat,
+                        body: core_body,
+                    })
+                }))?;
 
             Ok(ctx.alloc(core::Term::new_match(core_scrutinee, core_arms)))
         }
diff --git a/compiler/src/checker/mod.rs b/compiler/src/checker/mod.rs
index 6741adf..2f556d3 100644
--- a/compiler/src/checker/mod.rs
+++ b/compiler/src/checker/mod.rs
@@ -14,7 +14,7 @@ mod infer;
 pub(crate) fn builtin_prim_ty(
     name: &'_ core::Name,
     phase: Phase,
-) -> Option<&'static core::Term<'static>> {
+) -> Option<&'static core::Term<'static, 'static>> {
     Some(match name.as_str() {
         "u0" => core::Term::int_ty(IntWidth::U0, phase),
         "u1" => core::Term::int_ty(IntWidth::U1, phase),
diff --git a/compiler/src/checker/test/helpers.rs b/compiler/src/checker/test/helpers.rs
index 893eda7..cf35500 100644
--- a/compiler/src/checker/test/helpers.rs
+++ b/compiler/src/checker/test/helpers.rs
@@ -3,8 +3,8 @@
 use super::*;
 
 /// Helper to create a test context with empty globals
-pub fn test_ctx(arena: &bumpalo::Bump) -> Ctx<'_, '_> {
-    static EMPTY: std::sync::OnceLock<HashMap<&'static Name, &'static core::Pi<'static>>> =
+pub fn test_ctx(arena: &bumpalo::Bump) -> Ctx<'_, '_, '_> {
+    static EMPTY: std::sync::OnceLock<HashMap<&'static Name, &'static core::Pi<'static, 'static>>> =
         std::sync::OnceLock::new();
     let globals = EMPTY.get_or_init(HashMap::new);
     Ctx::new(arena, globals)
@@ -13,15 +13,15 @@ pub fn test_ctx(arena: &bumpalo::Bump) -> Ctx<'_, '_> {
 /// Helper to create a test context with a given globals table.
 ///
 /// The caller must ensure `globals` outlives the returned `Ctx`.
-pub fn test_ctx_with_globals<'core, 'globals>(
+pub fn test_ctx_with_globals<'names, 'core, 'globals>(
     arena: &'core bumpalo::Bump,
-    globals: &'globals HashMap<&'core Name, &'core core::Pi<'core>>,
-) -> Ctx<'core, 'globals> {
+    globals: &'globals HashMap<&'names Name, &'core core::Pi<'names, 'core>>,
+) -> Ctx<'names, 'core, 'globals> {
     Ctx::new(arena, globals)
 }
 
 /// Helper: build a Pi for a function `fn f() -> u64` (no params, meta phase).
-pub fn sig_no_params_returns_u64(arena: &bumpalo::Bump) -> &core::Pi<'_> {
+pub fn sig_no_params_returns_u64(arena: &bumpalo::Bump) -> &core::Pi<'_, '_> {
     arena.alloc(Pi {
         params: &[],
         body_ty: &core::Term::U64_META,
@@ -30,7 +30,7 @@ pub fn sig_no_params_returns_u64(arena: &bumpalo::Bump) -> &core::Pi<'_> {
 }
 
 /// Helper: build a Pi for `fn f(x: u32) -> u64`.
-pub fn sig_one_param_returns_u64(arena: &bumpalo::Bump) -> &core::Pi<'_> {
+pub fn sig_one_param_returns_u64(arena: &bumpalo::Bump) -> &core::Pi<'_, '_> {
     let params =
         arena.alloc_slice_fill_iter([(core::Name::new("x"), &core::Term::U32_META as &core::Term)]);
     arena.alloc(Pi {
diff --git a/compiler/src/core/alpha_eq.rs b/compiler/src/core/alpha_eq.rs
index 5bf3fb6..c632391 100644
--- a/compiler/src/core/alpha_eq.rs
+++ b/compiler/src/core/alpha_eq.rs
@@ -1,7 +1,7 @@
 use super::Term;
 
 /// Alpha-equality: structural equality ignoring `param_name` fields in Pi/Lam.
-pub fn alpha_eq(a: &Term<'_>, b: &Term<'_>) -> bool {
+pub fn alpha_eq(a: &Term<'_, '_>, b: &Term<'_, '_>) -> bool {
     // Fast path: pointer equality
     if std::ptr::eq(a, b) {
         return true;
diff --git a/compiler/src/core/mod.rs b/compiler/src/core/mod.rs
index ed807c4..f7757e7 100644
--- a/compiler/src/core/mod.rs
+++ b/compiler/src/core/mod.rs
@@ -9,15 +9,15 @@ pub use prim::{IntType, IntWidth, Prim};
 
 /// Match pattern in the core IR
 #[derive(Debug, Clone, PartialEq, Eq)]
-pub enum Pat<'a> {
+pub enum Pat<'names> {
     Lit(u64),
-    Bind(&'a Name), // named binding
-    Wildcard,       // _ pattern
+    Bind(&'names Name), // named binding
+    Wildcard,           // _ pattern
 }
 
-impl<'a> Pat<'a> {
+impl<'names> Pat<'names> {
     /// Return the name bound by this pattern, if any.
-    pub const fn bound_name(&self) -> Option<&'a Name> {
+    pub const fn bound_name(&self) -> Option<&'names Name> {
         match self {
             Pat::Bind(name) => Some(*name),
             Pat::Lit(_) | Pat::Wildcard => None,
@@ -27,31 +27,31 @@ impl<'a> Pat<'a> {
 
 /// Match arm
 #[derive(Clone, Debug, PartialEq, Eq)]
-pub struct Arm<'a> {
-    pub pat: Pat<'a>,
-    pub body: &'a Term<'a>,
+pub struct Arm<'names, 'a> {
+    pub pat: Pat<'names>,
+    pub body: &'a Term<'names, 'a>,
 }
 
 /// Elaborated top-level function definition.
 #[derive(Debug)]
-pub struct Function<'a> {
-    pub name: &'a Name,
+pub struct Function<'names, 'a> {
+    pub name: &'names Name,
     /// Function type: phase, params, and return type.
-    pub ty: &'a Pi<'a>,
-    pub body: &'a Term<'a>,
+    pub ty: &'a Pi<'names, 'a>,
+    pub body: &'a Term<'names, 'a>,
 }
 
-impl<'a> Function<'a> {
+impl<'names, 'a> Function<'names, 'a> {
     /// Return the function's Pi type.
-    pub const fn pi(&self) -> &Pi<'a> {
+    pub const fn pi(&self) -> &Pi<'names, 'a> {
         self.ty
     }
 }
 
 /// Elaborated program: a sequence of top-level function definitions
 #[derive(Debug)]
-pub struct Program<'a> {
-    pub functions: &'a [Function<'a>],
+pub struct Program<'names, 'a> {
+    pub functions: &'a [Function<'names, 'a>],
 }
 
 /// Function or primitive application: `func(args...)`
@@ -64,9 +64,9 @@ pub struct Program<'a> {
 /// An empty `args` slice represents a zero-argument call and is distinct from
 /// a bare reference to `func`.
 #[derive(Debug, PartialEq, Eq)]
-pub struct App<'a> {
-    pub func: &'a Term<'a>,
-    pub args: &'a [&'a Term<'a>],
+pub struct App<'names, 'a> {
+    pub func: &'a Term<'names, 'a>,
+    pub args: &'a [&'a Term<'names, 'a>],
 }
 
 /// Dependent function type: `fn(params...) -> body_ty`
@@ -75,38 +75,38 @@ pub struct App<'a> {
 /// This allows the globals table to store `&Term` directly, unifying type lookup
 /// for globals and locals.
 #[derive(Debug, PartialEq, Eq)]
-pub struct Pi<'a> {
-    pub params: &'a [(&'a Name, &'a Term<'a>)], // (name, type) pairs
-    pub body_ty: &'a Term<'a>,
+pub struct Pi<'names, 'a> {
+    pub params: &'a [(&'names Name, &'a Term<'names, 'a>)], // (name, type) pairs
+    pub body_ty: &'a Term<'names, 'a>,
     pub phase: Phase,
 }
 
 /// Lambda abstraction: |params...| body
 #[derive(Debug, PartialEq, Eq)]
-pub struct Lam<'a> {
-    pub params: &'a [(&'a Name, &'a Term<'a>)], // (name, type) pairs
-    pub body: &'a Term<'a>,
+pub struct Lam<'names, 'a> {
+    pub params: &'a [(&'names Name, &'a Term<'names, 'a>)], // (name, type) pairs
+    pub body: &'a Term<'names, 'a>,
 }
 
 /// Let binding with explicit type annotation and a body.
 #[derive(Debug, PartialEq, Eq)]
-pub struct Let<'a> {
-    pub name: &'a Name,
-    pub ty: &'a Term<'a>,
-    pub expr: &'a Term<'a>,
-    pub body: &'a Term<'a>,
+pub struct Let<'names, 'a> {
+    pub name: &'names Name,
+    pub ty: &'a Term<'names, 'a>,
+    pub expr: &'a Term<'names, 'a>,
+    pub body: &'a Term<'names, 'a>,
 }
 
 /// Pattern match.
 #[derive(Debug, PartialEq, Eq)]
-pub struct Match<'a> {
-    pub scrutinee: &'a Term<'a>,
-    pub arms: &'a [Arm<'a>],
+pub struct Match<'names, 'a> {
+    pub scrutinee: &'a Term<'names, 'a>,
+    pub arms: &'a [Arm<'names, 'a>],
 }
 
 /// Core term / type (terms and types are unified)
 #[derive(Debug, PartialEq, Eq, derive_more::From)]
-pub enum Term<'a> {
+pub enum Term<'names, 'a> {
     /// Local variable, identified by De Bruijn index (0 = innermost binder)
     Var(de_bruijn::Ix),
     /// Built-in type or operation (not applied)
@@ -115,16 +115,16 @@ pub enum Term<'a> {
     /// Numeric literal with its integer type
     Lit(u64, IntType),
     /// Global function reference
-    Global(&'a Name),
+    Global(&'names Name),
     /// Function or primitive application: func(args...)
     #[from]
-    App(App<'a>),
+    App(App<'names, 'a>),
     /// Dependent function type: fn(x: A) -> B
     #[from]
-    Pi(Pi<'a>),
+    Pi(Pi<'names, 'a>),
     /// Lambda abstraction: |x: A| body
     #[from]
-    Lam(Lam<'a>),
+    Lam(Lam<'names, 'a>),
     /// Lift: [[T]] — meta type representing object-level code of type T
     Lift(&'a Self),
     /// Quotation: #(t) — produce object-level code from a meta expression
@@ -133,13 +133,13 @@ pub enum Term<'a> {
     Splice(&'a Self),
     /// Let binding with explicit type annotation and a body
     #[from]
-    Let(Let<'a>),
+    Let(Let<'names, 'a>),
     /// Pattern match
     #[from]
-    Match(Match<'a>),
+    Match(Match<'names, 'a>),
 }
 
-impl Term<'static> {
+impl Term<'static, 'static> {
     // Integer types at meta phase
     pub const U0_META: Self = Self::Prim(Prim::IntTy(IntType::U0_META));
     pub const U1_META: Self = Self::Prim(Prim::IntTy(IntType::U1_META));
@@ -195,12 +195,12 @@ impl Term<'static> {
     }
 }
 
-impl<'a> Term<'a> {
+impl<'names, 'a> Term<'names, 'a> {
     pub const fn new_app(func: &'a Self, args: &'a [&'a Self]) -> Self {
         Self::App(App { func, args })
     }
 
-    pub const fn new_let(name: &'a Name, ty: &'a Self, expr: &'a Self, body: &'a Self) -> Self {
+    pub const fn new_let(name: &'names Name, ty: &'a Self, expr: &'a Self, body: &'a Self) -> Self {
         Self::Let(Let {
             name,
             ty,
@@ -209,7 +209,7 @@ impl<'a> Term<'a> {
         })
     }
 
-    pub const fn new_match(scrutinee: &'a Self, arms: &'a [Arm<'a>]) -> Self {
+    pub const fn new_match(scrutinee: &'a Self, arms: &'a [Arm<'names, 'a>]) -> Self {
         Self::Match(Match { scrutinee, arms })
     }
 }
diff --git a/compiler/src/core/pretty.rs b/compiler/src/core/pretty.rs
index 340ebea..17546a9 100644
--- a/compiler/src/core/pretty.rs
+++ b/compiler/src/core/pretty.rs
@@ -13,13 +13,13 @@ fn write_indent(f: &mut fmt::Formatter<'_>, depth: usize) -> fmt::Result {
 
 // ── Core formatting ───────────────────────────────────────────────────────────
 
-impl<'a> Term<'a> {
+impl<'names> Term<'names, '_> {
     /// Print `self` in **statement position**: emits leading indentation, then
     /// the term content. `Let` and `Match` are printed without an enclosing `{ }`
     /// (the caller is responsible for any surrounding braces).
     fn fmt_term(
         &self,
-        env: &mut Vec<&'a Name>,
+        env: &mut Vec<&'names Name>,
         indent: usize,
         f: &mut fmt::Formatter<'_>,
     ) -> fmt::Result {
@@ -41,7 +41,7 @@ impl<'a> Term<'a> {
     /// a new indented block (e.g. `Let` / `Match`).
     fn fmt_term_inline(
         &self,
-        env: &mut Vec<&'a Name>,
+        env: &mut Vec<&'names Name>,
         indent: usize,
         f: &mut fmt::Formatter<'_>,
     ) -> fmt::Result {
@@ -171,7 +171,7 @@ impl<'a> Term<'a> {
     /// syntactically valid as sub-expressions.
     fn fmt_expr(
         &self,
-        env: &mut Vec<&'a Name>,
+        env: &mut Vec<&'names Name>,
         indent: usize,
         f: &mut fmt::Formatter<'_>,
     ) -> fmt::Result {
@@ -197,11 +197,11 @@ impl<'a> Term<'a> {
     }
 }
 
-impl<'a> Arm<'a> {
+impl<'names> Arm<'names, '_> {
     /// Print a single match arm.
     fn fmt_arm(
         &self,
-        env: &mut Vec<&'a Name>,
+        env: &mut Vec<&'names Name>,
         indent: usize,
         f: &mut fmt::Formatter<'_>,
     ) -> fmt::Result {
@@ -225,7 +225,7 @@ impl<'a> Arm<'a> {
 
 // ── Display impls ─────────────────────────────────────────────────────────────
 
-impl fmt::Display for Program<'_> {
+impl fmt::Display for Program<'_, '_> {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
         for (i, func) in self.functions.iter().enumerate() {
             if i > 0 {
@@ -237,7 +237,7 @@ impl fmt::Display for Program<'_> {
     }
 }
 
-impl fmt::Display for Function<'_> {
+impl fmt::Display for Function<'_, '_> {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
         let pi = self.pi();
 
diff --git a/compiler/src/core/value.rs b/compiler/src/core/value.rs
index 87d5d55..98c845e 100644
--- a/compiler/src/core/value.rs
+++ b/compiler/src/core/value.rs
@@ -12,15 +12,15 @@ use crate::common::{Phase, de_bruijn};
 
 /// Working evaluation environment: index 0 = outermost binding, last = innermost.
 /// `Var(Ix(i))` maps to `env[env.len() - 1 - i]`.
-pub type Env<'a> = Vec<Value<'a>>;
+pub type Env<'names, 'a> = Vec<Value<'names, 'a>>;
 
 /// Semantic value — result of evaluating a term or type.
 #[derive(Clone, Debug)]
-pub enum Value<'a> {
+pub enum Value<'names, 'a> {
     /// Neutral: stuck on a local variable (identified by De Bruijn level)
     Rigid(de_bruijn::Lvl),
     /// Neutral: global function reference (not inlined during type-checking)
-    Global(&'a Name),
+    Global(&'names Name),
     /// Neutral: unapplied or partially applied primitive
     Prim(Prim),
     /// Neutral: stuck application (callee cannot reduce further)
@@ -28,9 +28,9 @@ pub enum Value<'a> {
     /// Canonical: integer literal value
     Lit(u64, IntType),
     /// Canonical: lambda abstraction
-    Lam(VLam<'a>),
+    Lam(VLam<'names, 'a>),
     /// Canonical: dependent function type
-    Pi(VPi<'a>),
+    Pi(VPi<'names, 'a>),
     /// Canonical: lifted object type `[[T]]`
     Lift(&'a Self),
     /// Canonical: quoted object code `#(t)`
@@ -46,9 +46,9 @@ pub enum Value<'a> {
 /// type of the i-th parameter (supporting dependent telescopes).
 /// `closure` takes all `params.len()` arguments.
 #[derive(Clone, Debug)]
-pub struct VLam<'a> {
-    pub params: &'a [(&'a Name, Closure<'a>)],
-    pub closure: Closure<'a>,
+pub struct VLam<'names, 'a> {
+    pub params: &'a [(&'names Name, Closure<'names, 'a>)],
+    pub closure: Closure<'names, 'a>,
 }
 
 /// Pi (dependent function type) value.
@@ -56,25 +56,29 @@ pub struct VLam<'a> {
 /// Same telescope layout as `VLam`: `params[i].1` is instantiated with `args[0..i]`
 /// to yield the domain of the i-th parameter. `ret_closure` takes all `params.len()` args.
 #[derive(Clone, Debug)]
-pub struct VPi<'a> {
-    pub params: &'a [(&'a Name, Closure<'a>)],
-    pub ret_closure: Closure<'a>,
+pub struct VPi<'names, 'a> {
+    pub params: &'a [(&'names Name, Closure<'names, 'a>)],
+    pub ret_closure: Closure<'names, 'a>,
     pub phase: Phase,
 }
 
 /// A closure: snapshot of the environment at creation time, plus an unevaluated body.
 #[derive(Clone, Debug)]
-pub struct Closure<'a> {
+pub struct Closure<'names, 'a> {
     /// Arena-allocated environment snapshot (index 0 = outermost).
-    pub env: &'a [Value<'a>],
+    pub env: &'a [Value<'names, 'a>],
     /// Unevaluated body term.
-    pub body: &'a Term<'a>,
+    pub body: &'a Term<'names, 'a>,
 }
 
 /// Evaluate a term in an environment, producing a semantic value.
 ///
 /// `env[env.len() - 1 - ix]` gives the value for `Var(Ix(ix))`.
-pub fn eval<'a>(arena: &'a Bump, env: &[Value<'a>], term: &'a Term<'a>) -> Value<'a> {
+pub fn eval<'names, 'a>(
+    arena: &'a Bump,
+    env: &[Value<'names, 'a>],
+    term: &'a Term<'names, 'a>,
+) -> Value<'names, 'a> {
     match term {
         Term::Var(ix) => {
             let lvl = ix.lvl_at(de_bruijn::Depth::new(env.len()));
@@ -93,7 +97,8 @@ pub fn eval<'a>(arena: &'a Bump, env: &[Value<'a>], term: &'a Term<'a>) -> Value
 
         Term::App(app) => {
             let func_val = eval(arena, env, app.func);
-            let arg_vals: Vec<Value<'a>> = app.args.iter().map(|a| eval(arena, env, a)).collect();
+            let arg_vals: Vec<Value<'names, 'a>> =
+                app.args.iter().map(|a| eval(arena, env, a)).collect();
             apply_many(arena, func_val, &arg_vals)
         }
 
@@ -120,7 +125,7 @@ pub fn eval<'a>(arena: &'a Bump, env: &[Value<'a>], term: &'a Term<'a>) -> Value
 
         Term::Let(let_) => {
             let val = eval(arena, env, let_.expr);
-            let mut env2: Vec<Value<'a>> = env.to_vec();
+            let mut env2: Vec<Value<'names, 'a>> = env.to_vec();
             env2.push(val);
             eval(arena, &env2, let_.body)
         }
@@ -165,9 +170,13 @@ pub fn eval<'a>(arena: &'a Bump, env: &[Value<'a>], term: &'a Term<'a>) -> Value
 /// All parameter domain closures share the same base environment snapshot.
 /// Each domain closure's body uses De Bruijn indices to reference preceding
 /// parameters, so they are correctly differentiated despite sharing the base env.
-pub fn eval_pi<'a>(arena: &'a Bump, env: &[Value<'a>], pi: &'a Pi<'a>) -> Value<'a> {
+pub fn eval_pi<'names, 'a>(
+    arena: &'a Bump,
+    env: &[Value<'names, 'a>],
+    pi: &'a Pi<'names, 'a>,
+) -> Value<'names, 'a> {
     let env_snapshot = arena.alloc_slice_fill_iter(env.iter().cloned());
-    let params: Vec<(&'a Name, Closure<'a>)> = pi
+    let params: Vec<(&'names Name, Closure<'names, 'a>)> = pi
         .params
         .iter()
         .map(|&(name, ty_term)| {
@@ -191,9 +200,13 @@ pub fn eval_pi<'a>(arena: &'a Bump, env: &[Value<'a>], pi: &'a Pi<'a>) -> Value<
 }
 
 /// Evaluate a multi-param Lam into a multi-param `Value::Lam` (no currying).
-fn eval_lam<'a>(arena: &'a Bump, env: &[Value<'a>], lam: &'a Lam<'a>) -> Value<'a> {
+fn eval_lam<'names, 'a>(
+    arena: &'a Bump,
+    env: &[Value<'names, 'a>],
+    lam: &'a Lam<'names, 'a>,
+) -> Value<'names, 'a> {
     let env_snapshot = arena.alloc_slice_fill_iter(env.iter().cloned());
-    let params: Vec<(&'a Name, Closure<'a>)> = lam
+    let params: Vec<(&'names Name, Closure<'names, 'a>)> = lam
         .params
         .iter()
         .map(|&(name, ty_term)| {
@@ -220,7 +233,11 @@ fn eval_lam<'a>(arena: &'a Bump, env: &[Value<'a>], lam: &'a Lam<'a>) -> Value<'
 /// For `Value::Lam` and `Value::Pi`, all args are pushed into the closure env at once.
 /// For neutrals, a stuck `App` node is produced. Each call site is its own `App` node;
 /// args are NOT flattened into existing `App` nodes to preserve call-site identity.
-pub fn apply_many<'a>(arena: &'a Bump, func: Value<'a>, args: &[Value<'a>]) -> Value<'a> {
+pub fn apply_many<'names, 'a>(
+    arena: &'a Bump,
+    func: Value<'names, 'a>,
+    args: &[Value<'names, 'a>],
+) -> Value<'names, 'a> {
     match func {
         Value::Lam(vlam) => inst_n(arena, &vlam.closure, args),
         Value::Pi(vpi) => inst_n(arena, &vpi.ret_closure, args),
@@ -249,7 +266,11 @@ pub fn apply_many<'a>(arena: &'a Bump, func: Value<'a>, args: &[Value<'a>]) -> V
 }
 
 /// Instantiate a closure with N arguments: extend env with all args, eval body.
-pub fn inst_n<'a>(arena: &'a Bump, closure: &Closure<'a>, args: &[Value<'a>]) -> Value<'a> {
+pub fn inst_n<'names, 'a>(
+    arena: &'a Bump,
+    closure: &Closure<'names, 'a>,
+    args: &[Value<'names, 'a>],
+) -> Value<'names, 'a> {
     let mut env = closure.env.to_vec();
     env.extend_from_slice(args);
     eval(arena, &env, closure.body)
@@ -257,14 +278,14 @@ pub fn inst_n<'a>(arena: &'a Bump, closure: &Closure<'a>, args: &[Value<'a>]) ->
 
 /// Quote a telescope (sequence of named parameters with closures).
 /// Returns the quoted parameters, final depth, and the rigid values built during the process.
-fn quote_telescope<'a>(
+fn quote_telescope<'names, 'a>(
     arena: &'a Bump,
     initial_depth: de_bruijn::Depth,
-    params: &[(&'a Name, Closure<'a>)],
+    params: &[(&'names Name, Closure<'names, 'a>)],
 ) -> (
-    Vec<(&'a Name, &'a Term<'a>)>,
+    Vec<(&'names Name, &'a Term<'names, 'a>)>,
     de_bruijn::Depth,
-    Vec<Value<'a>>,
+    Vec<Value<'names, 'a>>,
 ) {
     let mut rigid_vals = Vec::new();
     let mut quoted_params = Vec::new();
@@ -284,7 +305,11 @@ fn quote_telescope<'a>(
 /// Convert a value back to a term (for error reporting and definitional equality).
 ///
 /// `depth` is the current De Bruijn depth (number of locally-bound variables in scope).
-pub fn quote<'a>(arena: &'a Bump, depth: de_bruijn::Depth, val: &Value<'a>) -> &'a Term<'a> {
+pub fn quote<'names, 'a>(
+    arena: &'a Bump,
+    depth: de_bruijn::Depth,
+    val: &Value<'names, 'a>,
+) -> &'a Term<'names, 'a> {
     match val {
         Value::Rigid(lvl) => {
             let ix = lvl.ix_at(depth);
@@ -295,7 +320,7 @@ pub fn quote<'a>(arena: &'a Bump, depth: de_bruijn::Depth, val: &Value<'a>) -> &
         Value::Lit(n, it) => arena.alloc(Term::Lit(*n, *it)),
         Value::App(f, args) => {
             let qf = quote(arena, depth, f);
-            let qargs: Vec<&'a Term<'a>> = args
+            let qargs: Vec<&'a Term<'names, 'a>> = args
                 .iter()
                 .map(|a| quote(arena, depth, a) as &'a _)
                 .collect();
@@ -338,20 +363,25 @@ pub fn quote<'a>(arena: &'a Bump, depth: de_bruijn::Depth, val: &Value<'a>) -> &
 }
 
 /// Definitional equality: quote both values and compare structurally.
-pub fn val_eq<'a>(arena: &'a Bump, depth: de_bruijn::Depth, a: &Value<'a>, b: &Value<'a>) -> bool {
+pub fn val_eq<'names, 'a>(
+    arena: &'a Bump,
+    depth: de_bruijn::Depth,
+    a: &Value<'names, 'a>,
+    b: &Value<'names, 'a>,
+) -> bool {
     let ta = quote(arena, depth, a);
     let tb = quote(arena, depth, b);
     super::alpha_eq::alpha_eq(ta, tb)
 }
 
 /// Evaluate a term in the empty environment.
-pub fn eval_closed<'a>(arena: &'a Bump, term: &'a Term<'a>) -> Value<'a> {
+pub fn eval_closed<'names, 'a>(arena: &'a Bump, term: &'a Term<'names, 'a>) -> Value<'names, 'a> {
     eval(arena, &[], term)
 }
 
 /// Extract the Phase from a Value that represents a universe (Type or `VmType`),
 /// if it is indeed a type universe.
-pub const fn value_phase(val: &Value<'_>) -> Option<Phase> {
+pub const fn value_phase(val: &Value<'_, '_>) -> Option<Phase> {
     match val {
         Value::Prim(Prim::IntTy(it)) => Some(it.phase),
         Value::Prim(Prim::U(_)) | Value::Lift(_) | Value::Pi(_) => Some(Phase::Meta),
diff --git a/compiler/src/lexer/mod.rs b/compiler/src/lexer/mod.rs
index 79197d2..eea709d 100644
--- a/compiler/src/lexer/mod.rs
+++ b/compiler/src/lexer/mod.rs
@@ -7,13 +7,14 @@ pub use token::Token;
 pub mod testutils;
 mod token;
 
-pub struct Lexer<'a> {
-    input: &'a str,
+pub struct Lexer<'src, 'names> {
+    input: &'src str,
+    names: &'names bumpalo::Bump,
 }
 
-impl<'a> Lexer<'a> {
-    pub const fn new(input: &'a str) -> Self {
-        Self { input }
+impl<'src, 'names> Lexer<'src, 'names> {
+    pub const fn new(input: &'src str, names: &'names bumpalo::Bump) -> Self {
+        Self { input, names }
     }
 
     #[inline]
@@ -33,7 +34,7 @@ impl<'a> Lexer<'a> {
         }
     }
 
-    fn split_pred<F: Fn(char) -> bool>(&mut self, pred: F) -> &'a str {
+    fn split_pred<F: Fn(char) -> bool>(&mut self, pred: F) -> &'src str {
         let len = self.input.find(pred).unwrap_or(self.input.len());
         let (token, rest) = self.input.split_at(len);
         self.input = rest;
@@ -44,21 +45,21 @@ impl<'a> Lexer<'a> {
         c.is_ascii_alphanumeric() || c == '_'
     }
 
-    fn read_number(&mut self) -> Result<Token<'a>> {
+    fn read_number(&mut self) -> Result<Token<'names>> {
         let num_str = self.split_pred(|c| !c.is_ascii_digit());
         Ok(Token::Num(num_str.parse()?))
     }
 
-    fn read_ident(&mut self) -> Token<'a> {
+    fn read_ident(&mut self) -> Token<'names> {
         let ident = self.split_pred(|c| !Self::is_ident_char(c));
-        Token::KEYWORDS
-            .iter()
-            .find(|(kw, _)| *kw == ident)
-            .map_or(Token::Ident(Name::new(ident)), |(_, tok)| *tok)
+        Token::KEYWORDS.iter().find(|(kw, _)| *kw == ident).map_or(
+            Token::Ident(Name::new(self.names.alloc_str(ident))),
+            |(_, tok)| *tok,
+        )
     }
 
     #[inline]
-    fn read_token_impl(&mut self) -> Option<Result<Token<'a>>> {
+    fn read_token_impl(&mut self) -> Option<Result<Token<'names>>> {
         let c = self.input.chars().next()?;
 
         // Try matching symbols (longer first due to table order)
@@ -83,7 +84,7 @@ impl<'a> Lexer<'a> {
     }
 
     #[inline]
-    fn read_token(&mut self) -> Option<Result<Token<'a>>> {
+    fn read_token(&mut self) -> Option<Result<Token<'names>>> {
         let orig_len = self.input.len();
         let result = self.read_token_impl();
         assert!(
@@ -94,16 +95,16 @@ impl<'a> Lexer<'a> {
     }
 
     #[inline]
-    fn next(&mut self) -> Option<Result<Token<'a>>> {
+    fn next(&mut self) -> Option<Result<Token<'names>>> {
         self.skip_whitespace();
         self.read_token()
     }
 }
 
-impl<'a> Iterator for Lexer<'a> {
-    type Item = Result<Token<'a>>;
+impl<'names> Iterator for Lexer<'_, 'names> {
+    type Item = Result<Token<'names>>;
 
-    fn next(&mut self) -> Option<Result<Token<'a>>> {
+    fn next(&mut self) -> Option<Result<Token<'names>>> {
         self.next()
     }
 }
diff --git a/compiler/src/lexer/test/fuzz.rs b/compiler/src/lexer/test/fuzz.rs
index cecffc5..a41700e 100644
--- a/compiler/src/lexer/test/fuzz.rs
+++ b/compiler/src/lexer/test/fuzz.rs
@@ -1,10 +1,13 @@
+use bumpalo::Bump;
+
 use crate::lexer::Lexer;
 use bolero::check;
 
 #[test]
 fn lexer() {
     check!().with_type::<String>().for_each(|input: &String| {
-        let lexer = Lexer::new(input);
+        let names = Bump::new();
+        let lexer = Lexer::new(input, &names);
         let tokens = lexer.collect::<Vec<_>>();
         if tokens.iter().any(Result::is_ok) {
             eprintln!("[len={:3}] {input:?} {tokens:?}", input.len());
@@ -15,7 +18,8 @@ fn lexer() {
 #[test]
 fn token() {
     check!().with_type::<String>().for_each(|input: &String| {
-        let token = Lexer::new(input).next();
+        let names = Bump::new();
+        let token = Lexer::new(input, &names).next();
         if let Some(Ok(token)) = token {
             let len = input.len();
             eprintln!("[len={len:03}] {input:?}: {token:?}");
diff --git a/compiler/src/lexer/token.rs b/compiler/src/lexer/token.rs
index 33492ac..3081863 100644
--- a/compiler/src/lexer/token.rs
+++ b/compiler/src/lexer/token.rs
@@ -1,7 +1,7 @@
 use crate::common::Name;
 
 #[derive(Clone, Copy, Debug, PartialEq, Eq)]
-pub enum Token<'a> {
+pub enum Token<'names> {
     Fn,
     Code,
     Let,
@@ -38,7 +38,7 @@ pub enum Token<'a> {
     DoubleRBracket,
     DArrow,
     Num(u64),
-    Ident(&'a Name),
+    Ident(&'names Name),
 }
 
 impl Token<'static> {
diff --git a/compiler/src/parser/ast.rs b/compiler/src/parser/ast.rs
index dc85299..0e07656 100644
--- a/compiler/src/parser/ast.rs
+++ b/compiler/src/parser/ast.rs
@@ -2,9 +2,9 @@ pub use crate::common::{Assoc, BinOp, Name, Phase, UnOp};
 
 /// Function or operator reference
 #[derive(Clone, Copy, derive_more::Debug)]
-pub enum FunName<'a> {
+pub enum FunName<'names, 'ast> {
     #[debug("{_0:?}")]
-    Term(&'a Term<'a>),
+    Term(&'ast Term<'names, 'ast>),
     #[debug("{_0:?}")]
     BinOp(BinOp),
     #[debug("{_0:?}")]
@@ -12,84 +12,84 @@ pub enum FunName<'a> {
 }
 
 #[derive(derive_more::Debug)]
-pub enum Pat<'a> {
+pub enum Pat<'names> {
     #[debug("{_0:?}")]
-    Name(&'a Name),
+    Name(&'names Name),
     #[debug("{_0:?}")]
     Lit(u64),
 }
 
 #[derive(Debug)]
-pub struct MatchArm<'a> {
-    pub pat: Pat<'a>,
-    pub body: &'a Term<'a>,
+pub struct MatchArm<'names, 'ast> {
+    pub pat: Pat<'names>,
+    pub body: &'ast Term<'names, 'ast>,
 }
 
 #[derive(Debug)]
-pub struct Let<'a> {
-    pub name: &'a Name,
-    pub ty: Option<&'a Term<'a>>,
-    pub expr: &'a Term<'a>,
+pub struct Let<'names, 'ast> {
+    pub name: &'names Name,
+    pub ty: Option<&'ast Term<'names, 'ast>>,
+    pub expr: &'ast Term<'names, 'ast>,
 }
 
 #[derive(Debug)]
-pub struct Param<'a> {
-    pub name: &'a Name,
-    pub ty: &'a Term<'a>,
+pub struct Param<'names, 'ast> {
+    pub name: &'names Name,
+    pub ty: &'ast Term<'names, 'ast>,
 }
 
 #[derive(Debug)]
-pub struct Function<'a> {
+pub struct Function<'names, 'ast> {
     pub phase: Phase,
-    pub name: &'a Name,
-    pub params: &'a [Param<'a>],
-    pub ret_ty: &'a Term<'a>,
-    pub body: &'a Term<'a>,
+    pub name: &'names Name,
+    pub params: &'ast [Param<'names, 'ast>],
+    pub ret_ty: &'ast Term<'names, 'ast>,
+    pub body: &'ast Term<'names, 'ast>,
 }
 
 #[derive(Debug)]
-pub struct Program<'a> {
-    pub functions: &'a [Function<'a>],
+pub struct Program<'names, 'ast> {
+    pub functions: &'ast [Function<'names, 'ast>],
 }
 
 #[derive(derive_more::Debug)]
-pub enum Term<'a> {
+pub enum Term<'names, 'ast> {
     #[debug("{_0:?}")]
     Lit(u64),
 
     #[debug("{_0:?}")]
-    Var(&'a Name),
+    Var(&'names Name),
 
     App {
-        func: FunName<'a>,
-        args: &'a [&'a Self],
+        func: FunName<'names, 'ast>,
+        args: &'ast [&'ast Self],
     },
 
     /// Function type: `fn(name: ty, ...) -> ret_ty`
     Pi {
-        params: &'a [Param<'a>],
-        ret_ty: &'a Self,
+        params: &'ast [Param<'names, 'ast>],
+        ret_ty: &'ast Self,
     },
 
     /// Lambda: `|params| body`
     Lam {
-        params: &'a [Param<'a>],
-        body: &'a Self,
+        params: &'ast [Param<'names, 'ast>],
+        body: &'ast Self,
     },
 
-    Quote(&'a Self),
+    Quote(&'ast Self),
 
-    Splice(&'a Self),
+    Splice(&'ast Self),
 
-    Lift(&'a Self),
+    Lift(&'ast Self),
 
     Match {
-        scrutinee: &'a Self,
-        arms: &'a [MatchArm<'a>],
+        scrutinee: &'ast Self,
+        arms: &'ast [MatchArm<'names, 'ast>],
     },
 
     Block {
-        stmts: &'a [Let<'a>],
-        expr: &'a Self,
+        stmts: &'ast [Let<'names, 'ast>],
+        expr: &'ast Self,
     },
 }
diff --git a/compiler/src/parser/mod.rs b/compiler/src/parser/mod.rs
index f751848..5690a1e 100644
--- a/compiler/src/parser/mod.rs
+++ b/compiler/src/parser/mod.rs
@@ -10,35 +10,35 @@ use crate::parser::ast::{
 
 pub mod ast;
 
-pub struct Parser<'a, I>
+pub struct Parser<'names, 'ast, I>
 where
-    I: Iterator<Item = Result<Token<'a>>>,
+    I: Iterator<Item = Result<Token<'names>>>,
 {
     tokens: Peekable<I>,
-    arena: &'a bumpalo::Bump,
+    arena: &'ast bumpalo::Bump,
 }
 
-impl<'a, I> Parser<'a, I>
+impl<'names, 'ast, I> Parser<'names, 'ast, I>
 where
-    I: Iterator<Item = Result<Token<'a>>>,
+    I: Iterator<Item = Result<Token<'names>>>,
 {
-    pub fn new(tokens: I, arena: &'a bumpalo::Bump) -> Self {
+    pub fn new(tokens: I, arena: &'ast bumpalo::Bump) -> Self {
         let tokens = tokens.peekable();
         Self { tokens, arena }
     }
 
-    fn peek(&mut self) -> Option<Token<'a>> {
+    fn peek(&mut self) -> Option<Token<'names>> {
         self.tokens.peek().and_then(|r| r.as_ref().ok().copied())
     }
 
-    fn next(&mut self) -> Option<Result<Token<'a>>> {
+    fn next(&mut self) -> Option<Result<Token<'names>>> {
         self.tokens.next()
     }
 
     /// Helper for extracting a token with a custom validation closure
     fn expect_token<T, F>(&mut self, description: &str, f: F) -> Result<T>
     where
-        F: FnOnce(Token<'a>) -> Option<T>,
+        F: FnOnce(Token<'names>) -> Option<T>,
     {
         match self.next() {
             Some(Ok(token)) => {
@@ -49,13 +49,13 @@ where
         }
     }
 
-    fn take(&mut self, expected: Token<'a>) -> Result<Token<'a>> {
+    fn take(&mut self, expected: Token<'names>) -> Result<Token<'names>> {
         self.expect_token(&format!("{expected:?}"), |token| {
             (token == expected).then_some(token)
         })
     }
 
-    fn take_ident(&mut self) -> Result<&'a Name> {
+    fn take_ident(&mut self) -> Result<&'names Name> {
         self.expect_token("identifier", |token| {
             if let Token::Ident(name) = token {
                 Some(name)
@@ -66,7 +66,7 @@ where
     }
 
     /// Consume a token if it matches the expected token
-    fn consume_if(&mut self, token: Token<'a>) -> bool {
+    fn consume_if(&mut self, token: Token<'names>) -> bool {
         if matches!(self.peek(), Some(t) if t == token) {
             self.next();
             true
@@ -76,12 +76,12 @@ where
     }
 
     /// Allocate a term and return a reference to it
-    fn alloc(&self, term: Term<'a>) -> &'a Term<'a> {
+    fn alloc(&self, term: Term<'names, 'ast>) -> &'ast Term<'names, 'ast> {
         &*self.arena.alloc(term)
     }
 
     /// Parse a quoted expression: #(...)
-    fn parse_quoted_expr(&mut self) -> Result<Term<'a>> {
+    fn parse_quoted_expr(&mut self) -> Result<Term<'names, 'ast>> {
         let expr = self.parse_expr().context("parsing quoted expression")?;
         self.take(Token::RParen)
             .context("expected ')' after quotation")?;
@@ -89,13 +89,13 @@ where
     }
 
     /// Parse a quoted block: #{...}
-    fn parse_quoted_block(&mut self) -> Result<Term<'a>> {
+    fn parse_quoted_block(&mut self) -> Result<Term<'names, 'ast>> {
         let (stmts, expr) = self.parse_block_inner()?;
         Ok(Term::Quote(self.alloc(Term::Block { stmts, expr })))
     }
 
     /// Parse a spliced expression: $(...)
-    fn parse_spliced_expr(&mut self) -> Result<Term<'a>> {
+    fn parse_spliced_expr(&mut self) -> Result<Term<'names, 'ast>> {
         let expr = self.parse_expr().context("parsing spliced expression")?;
         self.take(Token::RParen)
             .context("expected ')' after splice")?;
@@ -103,13 +103,13 @@ where
     }
 
     /// Parse a spliced block: ${...}
-    fn parse_spliced_block(&mut self) -> Result<Term<'a>> {
+    fn parse_spliced_block(&mut self) -> Result<Term<'names, 'ast>> {
         let (stmts, expr) = self.parse_block_inner()?;
         Ok(Term::Splice(self.alloc(Term::Block { stmts, expr })))
     }
 
     /// Parse a lifted expression: [[...]]
-    fn parse_lifted_expr(&mut self) -> Result<Term<'a>> {
+    fn parse_lifted_expr(&mut self) -> Result<Term<'names, 'ast>> {
         let expr = self.parse_expr().context("parsing lifted expression")?;
         self.take(Token::DoubleRBracket)
             .context("expected ']]' after lifted expression")?;
@@ -117,7 +117,11 @@ where
     }
 
     /// Parse a comma-separated list of items bounded by a terminator token
-    fn parse_separated_list<T, F>(&mut self, terminator: Token<'a>, mut parser: F) -> Result<Vec<T>>
+    fn parse_separated_list<T, F>(
+        &mut self,
+        terminator: Token<'names>,
+        mut parser: F,
+    ) -> Result<Vec<T>>
     where
         F: FnMut(&mut Self) -> Result<T>,
     {
@@ -134,7 +138,7 @@ where
         Ok(items)
     }
 
-    pub fn parse_program(&mut self) -> Result<Program<'a>> {
+    pub fn parse_program(&mut self) -> Result<Program<'names, 'ast>> {
         let mut functions = Vec::new();
         while self.peek().is_some() {
             let fun = self.parse_fn_def()?;
@@ -144,7 +148,7 @@ where
         Ok(Program { functions })
     }
 
-    fn parse_fn_def(&mut self) -> Result<Function<'a>> {
+    fn parse_fn_def(&mut self) -> Result<Function<'names, 'ast>> {
         let phase = if self.consume_if(Token::Code) {
             Phase::Object
         } else {
@@ -158,7 +162,11 @@ where
             .with_context(|| format!("in function `{name}`"))
     }
 
-    fn parse_fn_def_after_name(&mut self, phase: Phase, name: &'a Name) -> Result<Function<'a>> {
+    fn parse_fn_def_after_name(
+        &mut self,
+        phase: Phase,
+        name: &'names Name,
+    ) -> Result<Function<'names, 'ast>> {
         self.take(Token::LParen).context("expected '('")?;
         let params = self.parse_params()?;
         self.take(Token::RParen).context("expected ')'")?;
@@ -180,7 +188,7 @@ where
         })
     }
 
-    fn parse_params(&mut self) -> Result<&'a [Param<'a>]> {
+    fn parse_params(&mut self) -> Result<&'ast [Param<'names, 'ast>]> {
         let params = self.parse_separated_list(Token::RParen, |parser| {
             let name = parser.take_ident().context("expected parameter name")?;
             parser
@@ -193,13 +201,15 @@ where
         Ok(self.arena.alloc_slice_fill_iter(params))
     }
 
-    fn parse_block(&mut self) -> Result<&'a Term<'a>> {
+    fn parse_block(&mut self) -> Result<&'ast Term<'names, 'ast>> {
         self.take(Token::LBrace).context("expected '{'")?;
         let (stmts, expr) = self.parse_block_inner()?;
         Ok(self.alloc(Term::Block { stmts, expr }))
     }
 
-    fn parse_block_inner(&mut self) -> Result<(&'a [Let<'a>], &'a Term<'a>)> {
+    fn parse_block_inner(
+        &mut self,
+    ) -> Result<(&'ast [Let<'names, 'ast>], &'ast Term<'names, 'ast>)> {
         let mut stmts = Vec::new();
 
         while self.peek() == Some(Token::Let) {
@@ -214,7 +224,7 @@ where
         Ok((stmts, expr))
     }
 
-    fn parse_let_stmt(&mut self) -> Result<Let<'a>> {
+    fn parse_let_stmt(&mut self) -> Result<Let<'names, 'ast>> {
         self.take(Token::Let).context("expected 'let'")?;
         let name = self.take_ident().context("expected variable name")?;
         let ty = if self.consume_if(Token::Colon) {
@@ -232,15 +242,15 @@ where
         Ok(Let { name, ty, expr })
     }
 
-    fn parse_expr(&mut self) -> Result<&'a Term<'a>> {
+    fn parse_expr(&mut self) -> Result<&'ast Term<'names, 'ast>> {
         Ok(self.arena.alloc(self.parse_expr_owned()?))
     }
 
-    fn parse_expr_owned(&mut self) -> Result<Term<'a>> {
+    fn parse_expr_owned(&mut self) -> Result<Term<'names, 'ast>> {
         self.parse_expr_prec(Precedence::MIN)
     }
 
-    fn parse_expr_prec(&mut self, min_prec: Precedence) -> Result<Term<'a>> {
+    fn parse_expr_prec(&mut self, min_prec: Precedence) -> Result<Term<'names, 'ast>> {
         let mut lhs = if let Some(op) = self.match_unop() {
             self.next();
             let expr = self
@@ -333,7 +343,7 @@ where
     }
 
     /// Parse a function call with arguments
-    fn parse_function_call(&mut self, name: &'a Name) -> Result<Term<'a>> {
+    fn parse_function_call(&mut self, name: &'names Name) -> Result<Term<'names, 'ast>> {
         let args = self.parse_separated_list(Token::RParen, |parser| {
             parser.parse_expr().context("parsing function argument")
         })?;
@@ -347,7 +357,7 @@ where
     }
 
     /// Parse a parenthesized expression
-    fn parse_paren_expr(&mut self) -> Result<Term<'a>> {
+    fn parse_paren_expr(&mut self) -> Result<Term<'names, 'ast>> {
         let expr = self
             .parse_expr_owned()
             .context("parsing expression in parentheses")?;
@@ -357,7 +367,7 @@ where
     }
 
     /// Parse a match expression
-    fn parse_match_expr(&mut self) -> Result<Term<'a>> {
+    fn parse_match_expr(&mut self) -> Result<Term<'names, 'ast>> {
         let scrutinee = self.parse_expr().context("parsing match scrutinee")?;
         self.take(Token::LBrace)
             .context("expected '{' after match expression")?;
@@ -371,7 +381,7 @@ where
     /// Parse a function type: `fn(params) -> ret_ty`
     ///
     /// Called after consuming the `fn` token. Each param is `name: type`.
-    fn parse_fn_type(&mut self) -> Result<Term<'a>> {
+    fn parse_fn_type(&mut self) -> Result<Term<'names, 'ast>> {
         self.take(Token::LParen)
             .context("expected '(' in function type")?;
         let params = self.parse_params()?;
@@ -388,7 +398,7 @@ where
     /// Parse a lambda expression: `|params| body`
     ///
     /// Called after consuming the `|` token. Each param is `name: type`.
-    fn parse_lambda(&mut self) -> Result<Term<'a>> {
+    fn parse_lambda(&mut self) -> Result<Term<'names, 'ast>> {
         let params_vec = self.parse_separated_list(Token::Bar, |parser| {
             let name = parser
                 .take_ident()
@@ -415,7 +425,7 @@ where
         clippy::wildcard_enum_match_arm,
         reason = "unrecognised tokens are intentionally caught by the wildcard arm"
     )]
-    fn parse_atom_owned(&mut self) -> Result<Term<'a>> {
+    fn parse_atom_owned(&mut self) -> Result<Term<'names, 'ast>> {
         let token = self.next().context("expected expression")??;
         match token {
             Token::Num(n) => Ok(Term::Lit(n)),
@@ -445,7 +455,7 @@ where
         }
     }
 
-    fn parse_match_arms(&mut self) -> Result<Vec<MatchArm<'a>>> {
+    fn parse_match_arms(&mut self) -> Result<Vec<MatchArm<'names, 'ast>>> {
         let mut arms = Vec::new();
         while self.peek().is_some() && !matches!(self.peek(), Some(Token::RBrace)) {
             let pat = self.parse_pattern().context("parsing match pattern")?;
@@ -465,7 +475,7 @@ where
         clippy::wildcard_enum_match_arm,
         reason = "unrecognised tokens are intentionally caught by the wildcard arm"
     )]
-    fn parse_pattern(&mut self) -> Result<Pat<'a>> {
+    fn parse_pattern(&mut self) -> Result<Pat<'names>> {
         let token = self.next().context("expected pattern")??;
         match token {
             Token::Num(n) => Ok(Pat::Lit(n)),
diff --git a/compiler/src/parser/test/mod.rs b/compiler/src/parser/test/mod.rs
index 4ae36b6..bf1e66a 100644
--- a/compiler/src/parser/test/mod.rs
+++ b/compiler/src/parser/test/mod.rs
@@ -18,7 +18,7 @@ use crate::parser::ast::{BinOp, FunName};
 
 fn parse_expr(input: &str) -> String {
     let arena = bumpalo::Bump::new();
-    let lexer = Lexer::new(input);
+    let lexer = Lexer::new(input, &arena);
     let mut parser = Parser::new(lexer, &arena);
     let expr = parser.parse_expr().unwrap();
     format!("{expr:#?}\n")
@@ -36,7 +36,7 @@ fn expr(#[files("src/parser/test/expr/*.input.txt")] path: PathBuf) {
 #[test]
 fn parse_trivial_block() {
     let arena = bumpalo::Bump::new();
-    let lexer = Lexer::new("{ 0 + 1 }");
+    let lexer = Lexer::new("{ 0 + 1 }", &arena);
     let mut parser = Parser::new(lexer, &arena);
     let expr = parser.parse_expr().unwrap();
     match expr {
@@ -48,7 +48,7 @@ fn parse_trivial_block() {
 #[test]
 fn parse_simple_fn() {
     let arena = bumpalo::Bump::new();
-    let lexer = Lexer::new("fn add(x: u32, y: u32) -> u32 { x + y }");
+    let lexer = Lexer::new("fn add(x: u32, y: u32) -> u32 { x + y }", &arena);
     let mut parser = Parser::new(lexer, &arena);
     let program = parser.parse_program().unwrap();
     assert_eq!(program.functions.len(), 1);
@@ -60,7 +60,7 @@ fn parse_simple_fn() {
 #[test]
 fn parse_simple_fn_and_junk() {
     let arena = bumpalo::Bump::new();
-    let lexer = Lexer::new("fn foo() -> u32 { 0 } wat");
+    let lexer = Lexer::new("fn foo() -> u32 { 0 } wat", &arena);
     let mut parser = Parser::new(lexer, &arena);
     let program = parser.parse_program();
     assert!(program.is_err());
@@ -69,7 +69,7 @@ fn parse_simple_fn_and_junk() {
 #[test]
 fn parse_expr_prec() {
     let arena = bumpalo::Bump::new();
-    let lexer = Lexer::new("1 + 2 * 3");
+    let lexer = Lexer::new("1 + 2 * 3", &arena);
     let mut parser = Parser::new(lexer, &arena);
     let expr = parser.parse_expr().unwrap();
     match expr {
@@ -84,7 +84,7 @@ fn parse_expr_prec() {
 #[test]
 fn parse_expr_prec2() {
     let arena = bumpalo::Bump::new();
-    let lexer = Lexer::new("1 * 2 + 3");
+    let lexer = Lexer::new("1 * 2 + 3", &arena);
     let mut parser = Parser::new(lexer, &arena);
     let expr = parser.parse_expr().unwrap();
     match expr {
@@ -99,7 +99,7 @@ fn parse_expr_prec2() {
 #[test]
 fn parse_expr_paren() {
     let arena = bumpalo::Bump::new();
-    let lexer = Lexer::new("1 * (2 + 3)");
+    let lexer = Lexer::new("1 * (2 + 3)", &arena);
     let mut parser = Parser::new(lexer, &arena);
     let expr = parser.parse_expr().unwrap();
     match expr {
diff --git a/compiler/src/staging/mod.rs b/compiler/src/staging/mod.rs
index db64c87..cd4376b 100644
--- a/compiler/src/staging/mod.rs
+++ b/compiler/src/staging/mod.rs
@@ -19,7 +19,7 @@ use crate::parser::ast::Phase;
 /// forbidden in Splic (the type-checker enforces this); `eval_obj` eagerly
 /// evaluates under binders by extending the environment with fresh level variables.
 #[derive(Clone, Debug)]
-enum ObjVal<'a> {
+enum ObjVal<'names, 'eval> {
     /// Local variable identified by De Bruijn level (absolute, context-independent).
     Var(de_bruijn::Lvl),
     /// Integer literal.
@@ -27,27 +27,27 @@ enum ObjVal<'a> {
     /// Unapplied primitive.
     Prim(Prim),
     /// Global function reference.
-    Global(&'a Name),
+    Global(&'names Name),
     /// Application.
-    App(&'a Self, &'a [Self]),
+    App(&'eval Self, &'eval [Self]),
     /// Let binding.
     Let {
-        name: &'a Name,
-        ty: &'a Self,
-        expr: &'a Self,
-        body: &'a Self,
+        name: &'names Name,
+        ty: &'eval Self,
+        expr: &'eval Self,
+        body: &'eval Self,
     },
     /// Pattern match.
     Match {
-        scrutinee: &'a Self,
-        arms: &'a [ObjArm<'a>],
+        scrutinee: &'eval Self,
+        arms: &'eval [ObjArm<'names, 'eval>],
     },
 }
 
 #[derive(Clone, Debug)]
-struct ObjArm<'a> {
-    pat: Pat<'a>,
-    body: &'a ObjVal<'a>,
+struct ObjArm<'names, 'eval> {
+    pat: Pat<'names>,
+    body: &'eval ObjVal<'names, 'eval>,
 }
 
 // ── Meta-level values ─────────────────────────────────────────────────────────
@@ -62,22 +62,22 @@ struct ObjArm<'a> {
 /// they are automatically discarded after staging; only the final `Term` output
 /// from `quote_obj` survives in the output arena.
 #[derive(Clone, Debug)]
-enum MetaVal<'eval> {
+enum MetaVal<'names, 'eval> {
     /// A concrete integer value computed at meta (compile) time.
     Lit(u64),
     /// Quoted object-level code as a semantic value.
     ///
     /// Uses De Bruijn levels internally, so it can be spliced into any depth
     /// without adjustment.  Allocated in the eval arena.
-    Quote(&'eval ObjVal<'eval>),
+    Quote(&'eval ObjVal<'names, 'eval>),
     /// A type term passed as a type argument (dependent types: types are values).
     /// The type term itself is not inspected during evaluation.
     Ty,
     /// A closure: a lambda body captured with its environment.
     Closure {
-        body: &'eval Term<'eval>,
+        body: &'eval Term<'names, 'eval>,
         arity: usize,
-        env: Vec<Binding<'eval>>,
+        env: Vec<Binding<'names, 'eval>>,
         obj_depth: de_bruijn::Depth,
     },
 }
@@ -86,9 +86,9 @@ enum MetaVal<'eval> {
 
 /// A binding stored in the evaluation environment, indexed by De Bruijn level.
 #[derive(Clone, Debug)]
-enum Binding<'eval> {
+enum Binding<'names, 'eval> {
     /// A meta-level variable bound to a concrete `MetaVal`.
-    Meta(MetaVal<'eval>),
+    Meta(MetaVal<'names, 'eval>),
     /// An object-level variable.
     Obj(de_bruijn::Lvl),
 }
@@ -98,12 +98,12 @@ enum Binding<'eval> {
 /// Bindings are stored oldest-first. `Var(Ix(i))` refers to
 /// `bindings[bindings.len() - 1 - i]` — the `i`-th binding from the end.
 #[derive(Debug)]
-struct Env<'eval> {
-    bindings: Vec<Binding<'eval>>,
+struct Env<'names, 'eval> {
+    bindings: Vec<Binding<'names, 'eval>>,
     obj_depth: de_bruijn::Depth,
 }
 
-impl<'eval> Env<'eval> {
+impl<'names, 'eval> Env<'names, 'eval> {
     const fn new(obj_depth: de_bruijn::Depth) -> Self {
         Env {
             bindings: Vec::new(),
@@ -112,7 +112,7 @@ impl<'eval> Env<'eval> {
     }
 
     /// Look up the binding for `Var(Ix(ix))`.
-    fn get_ix(&self, ix: de_bruijn::Ix) -> &Binding<'eval> {
+    fn get_ix(&self, ix: de_bruijn::Ix) -> &Binding<'names, 'eval> {
         let depth = de_bruijn::Depth::new(self.bindings.len());
         let lvl = ix.lvl_at(depth);
         let i = lvl.as_usize();
@@ -129,7 +129,7 @@ impl<'eval> Env<'eval> {
     }
 
     /// Push a meta-level binding bound to the given value.
-    fn push_meta(&mut self, val: MetaVal<'eval>) {
+    fn push_meta(&mut self, val: MetaVal<'names, 'eval>) {
         self.bindings.push(Binding::Meta(val));
     }
 
@@ -147,22 +147,22 @@ impl<'eval> Env<'eval> {
 // ── Globals table ─────────────────────────────────────────────────────────────
 
 /// Everything the evaluator needs to know about a top-level function.
-struct GlobalDef<'a> {
-    ty: &'a Pi<'a>,
-    body: &'a Term<'a>,
+struct GlobalDef<'names, 'a> {
+    ty: &'a Pi<'names, 'a>,
+    body: &'a Term<'names, 'a>,
 }
 
-type Globals<'a> = HashMap<&'a Name, GlobalDef<'a>>;
+type Globals<'names, 'a> = HashMap<&'names Name, GlobalDef<'names, 'a>>;
 
 // ── Meta-level evaluator ──────────────────────────────────────────────────────
 
 /// Evaluate a meta-level `term` to a `MetaVal`.
-fn eval_meta<'eval>(
+fn eval_meta<'names, 'eval>(
     eval_arena: &'eval Bump,
-    globals: &Globals<'eval>,
-    env: &mut Env<'eval>,
-    term: &'eval Term<'eval>,
-) -> Result<MetaVal<'eval>> {
+    globals: &Globals<'names, 'eval>,
+    env: &mut Env<'names, 'eval>,
+    term: &'eval Term<'names, 'eval>,
+) -> Result<MetaVal<'names, 'eval>> {
     match term {
         // ── Variable ─────────────────────────────────────────────────────────
         Term::Var(ix) => match env.get_ix(*ix) {
@@ -197,7 +197,7 @@ fn eval_meta<'eval>(
             Term::Prim(prim) => eval_meta_prim(eval_arena, globals, env, *prim, app.args),
             _ => {
                 let func_val = eval_meta(eval_arena, globals, env, app.func)?;
-                let arg_vals: Vec<MetaVal<'eval>> = app
+                let arg_vals: Vec<MetaVal<'names, 'eval>> = app
                     .args
                     .iter()
                     .map(|a| eval_meta(eval_arena, globals, env, a))
@@ -242,10 +242,10 @@ fn eval_meta<'eval>(
 }
 
 /// Convert a global function definition into a closure value.
-const fn global_to_closure<'eval>(
-    def: &GlobalDef<'eval>,
+const fn global_to_closure<'names, 'eval>(
+    def: &GlobalDef<'names, 'eval>,
     obj_depth: de_bruijn::Depth,
-) -> MetaVal<'eval> {
+) -> MetaVal<'names, 'eval> {
     MetaVal::Closure {
         body: def.body,
         arity: def.ty.params.len(),
@@ -255,12 +255,12 @@ const fn global_to_closure<'eval>(
 }
 
 /// Apply a closure value to N arguments simultaneously.
-fn apply_closure_n<'eval>(
+fn apply_closure_n<'names, 'eval>(
     eval_arena: &'eval Bump,
-    globals: &Globals<'eval>,
-    func_val: MetaVal<'eval>,
-    args: &[MetaVal<'eval>],
-) -> Result<MetaVal<'eval>> {
+    globals: &Globals<'names, 'eval>,
+    func_val: MetaVal<'names, 'eval>,
+    args: &[MetaVal<'names, 'eval>],
+) -> Result<MetaVal<'names, 'eval>> {
     match func_val {
         MetaVal::Closure {
             body,
@@ -284,11 +284,11 @@ fn apply_closure_n<'eval>(
     }
 }
 
-fn eval_lit<'eval>(
+fn eval_lit<'names, 'eval>(
     eval_arena: &'eval Bump,
-    globals: &Globals<'eval>,
-    env: &mut Env<'eval>,
-    arg: &'eval Term<'eval>,
+    globals: &Globals<'names, 'eval>,
+    env: &mut Env<'names, 'eval>,
+    arg: &'eval Term<'names, 'eval>,
 ) -> Result<u64> {
     eval_meta(eval_arena, globals, env, arg).map(|v| match v {
         MetaVal::Lit(n) => n,
@@ -298,11 +298,11 @@ fn eval_lit<'eval>(
     })
 }
 
-fn eval_bin_args<'eval>(
+fn eval_bin_args<'names, 'eval>(
     eval_arena: &'eval Bump,
-    globals: &Globals<'eval>,
-    env: &mut Env<'eval>,
-    args: &'eval [&'eval Term<'eval>],
+    globals: &Globals<'names, 'eval>,
+    env: &mut Env<'names, 'eval>,
+    args: &'eval [&'eval Term<'names, 'eval>],
 ) -> Result<(u64, u64)> {
     let [lhs, rhs] = args else {
         panic!("binary primitive requires exactly 2 arguments (typechecker invariant)")
@@ -313,13 +313,13 @@ fn eval_bin_args<'eval>(
 }
 
 /// Evaluate a primitive operation at meta level.
-fn eval_meta_prim<'eval>(
+fn eval_meta_prim<'names, 'eval>(
     eval_arena: &'eval Bump,
-    globals: &Globals<'eval>,
-    env: &mut Env<'eval>,
+    globals: &Globals<'names, 'eval>,
+    env: &mut Env<'names, 'eval>,
     prim: Prim,
-    args: &'eval [&'eval Term<'eval>],
-) -> Result<MetaVal<'eval>> {
+    args: &'eval [&'eval Term<'names, 'eval>],
+) -> Result<MetaVal<'names, 'eval>> {
     match prim {
         // ── Arithmetic ────────────────────────────────────────────────────────
         Prim::Add(IntType { width, .. }) => {
@@ -442,13 +442,13 @@ const fn mask_to_width(width: IntWidth, val: u64) -> u64 {
 }
 
 /// Evaluate a meta-level `match` expression.
-fn eval_meta_match<'eval>(
+fn eval_meta_match<'names, 'eval>(
     eval_arena: &'eval Bump,
-    globals: &Globals<'eval>,
-    env: &mut Env<'eval>,
+    globals: &Globals<'names, 'eval>,
+    env: &mut Env<'names, 'eval>,
     n: u64,
-    arms: &'eval [Arm<'eval>],
-) -> Result<MetaVal<'eval>> {
+    arms: &'eval [Arm<'names, 'eval>],
+) -> Result<MetaVal<'names, 'eval>> {
     for arm in arms {
         match &arm.pat {
             Pat::Lit(m) => {
@@ -478,12 +478,12 @@ fn eval_meta_match<'eval>(
 ///
 /// All `ObjVal` nodes are allocated in `eval_arena` (a temporary arena); they are
 /// discarded once `quote_obj` has converted them to output `Term` nodes.
-fn eval_obj<'eval>(
+fn eval_obj<'names, 'eval>(
     eval_arena: &'eval Bump,
-    globals: &Globals<'eval>,
-    env: &mut Env<'eval>,
-    term: &'eval Term<'eval>,
-) -> Result<&'eval ObjVal<'eval>> {
+    globals: &Globals<'names, 'eval>,
+    env: &mut Env<'names, 'eval>,
+    term: &'eval Term<'names, 'eval>,
+) -> Result<&'eval ObjVal<'names, 'eval>> {
     match term {
         // ── Variable ─────────────────────────────────────────────────────────
         Term::Var(ix) => match env.get_ix(*ix) {
@@ -520,7 +520,7 @@ fn eval_obj<'eval>(
         // ── App ───────────────────────────────────────────────────────────────
         Term::App(app) => {
             let func_val = eval_obj(eval_arena, globals, env, app.func)?;
-            let arg_vals: &'eval [ObjVal<'eval>] = eval_arena.alloc_slice_try_fill_iter(
+            let arg_vals: &'eval [ObjVal<'names, 'eval>] = eval_arena.alloc_slice_try_fill_iter(
                 app.args
                     .iter()
                     .map(|arg| eval_obj(eval_arena, globals, env, arg).cloned()),
@@ -558,7 +558,7 @@ fn eval_obj<'eval>(
         // ── Match ────────────────────────────────────────────────────────────
         Term::Match(match_) => {
             let scrutinee_val = eval_obj(eval_arena, globals, env, match_.scrutinee)?;
-            let arm_vals: &'eval [ObjArm<'eval>] = eval_arena.alloc_slice_try_fill_iter(
+            let arm_vals: &'eval [ObjArm<'_, 'eval>] = eval_arena.alloc_slice_try_fill_iter(
                 match_.arms.iter().map(|arm| -> Result<_> {
                     let has_binding = arm.pat.bound_name().is_some();
                     if has_binding {
@@ -593,20 +593,16 @@ fn eval_obj<'eval>(
 /// Convert an `ObjVal` back to a `Term` by translating De Bruijn levels to indices.
 ///
 /// `depth` is the number of object-level variables currently in scope.
-/// Names are copied into the output arena here — `eval_obj` stores bare references
-/// into the (temporary) eval arena; this is the single place they migrate to `'out`.
-fn quote_obj<'out>(
+fn quote_obj<'names, 'out>(
     out_arena: &'out Bump,
     depth: de_bruijn::Depth,
-    val: &ObjVal<'_>,
-) -> &'out Term<'out> {
+    val: &ObjVal<'names, '_>,
+) -> &'out Term<'names, 'out> {
     match val {
         ObjVal::Var(lvl) => out_arena.alloc(Term::Var(lvl.ix_at(depth))),
         ObjVal::Lit(n, it) => out_arena.alloc(Term::Lit(*n, *it)),
         ObjVal::Prim(p) => out_arena.alloc(Term::Prim(*p)),
-        ObjVal::Global(name) => {
-            out_arena.alloc(Term::Global(Name::new(out_arena.alloc_str(name.as_str()))))
-        }
+        ObjVal::Global(name) => out_arena.alloc(Term::Global(name)),
         ObjVal::App(func, args) => {
             let qfunc = quote_obj(out_arena, depth, func);
             let qargs = out_arena
@@ -622,8 +618,7 @@ fn quote_obj<'out>(
             let qty = quote_obj(out_arena, depth, ty);
             let qexpr = quote_obj(out_arena, depth, expr);
             let qbody = quote_obj(out_arena, depth.succ(), body);
-            let out_name = Name::new(out_arena.alloc_str(name.as_str()));
-            out_arena.alloc(Term::new_let(out_name, qty, qexpr, qbody))
+            out_arena.alloc(Term::new_let(name, qty, qexpr, qbody))
         }
         ObjVal::Match { scrutinee, arms } => {
             let qscrutinee = quote_obj(out_arena, depth, scrutinee);
@@ -635,7 +630,7 @@ fn quote_obj<'out>(
                 };
                 let out_pat = match &arm.pat {
                     Pat::Lit(n) => Pat::Lit(*n),
-                    Pat::Bind(name) => Pat::Bind(Name::new(out_arena.alloc_str(name.as_str()))),
+                    Pat::Bind(name) => Pat::Bind(name),
                     Pat::Wildcard => Pat::Wildcard,
                 };
                 Arm {
@@ -652,13 +647,13 @@ fn quote_obj<'out>(
 
 /// Unstage an elaborated program.
 ///
-/// - `out_arena`: output arena; the returned `Program<'out>` is allocated here.
+/// - `out_arena`: output arena; the returned `Program` is allocated here.
 /// - `program`: input core program; may be dropped once this function returns.
-pub fn unstage_program<'out, 'core>(
+pub fn unstage_program<'names, 'out, 'core>(
     out_arena: &'out Bump,
-    program: &'core Program<'core>,
-) -> Result<Program<'out>> {
-    let globals: Globals<'_> = program
+    program: &'core Program<'names, 'core>,
+) -> Result<Program<'names, 'out>> {
+    let globals: Globals<'names, '_> = program
         .functions
         .iter()
         .map(|f| {
@@ -672,7 +667,7 @@ pub fn unstage_program<'out, 'core>(
         })
         .collect();
 
-    let staged_fns: Vec<Function<'out>> = program
+    let staged_fns: Vec<Function<'names, 'out>> = program
         .functions
         .iter()
         .filter(|f| f.pi().phase.is_object())
@@ -685,11 +680,11 @@ pub fn unstage_program<'out, 'core>(
             let mut env = Env::new(de_bruijn::Depth::ZERO);
 
             let staged_params = out_arena.alloc_slice_try_fill_iter(pi.params.iter().map(
-                |(n, ty)| -> Result<(&'out Name, &'out Term<'out>)> {
+                |(n, ty)| -> Result<(&'names Name, &'out Term<'names, 'out>)> {
                     let ty_val = eval_obj(&eval_arena, &globals, &mut env, ty)?;
                     let staged_ty = quote_obj(out_arena, env.obj_depth, ty_val);
                     env.push_obj();
-                    Ok((Name::new(out_arena.alloc_str(n.as_str())), staged_ty))
+                    Ok((n, staged_ty))
                 },
             ))?;
 
@@ -700,7 +695,7 @@ pub fn unstage_program<'out, 'core>(
             let staged_body = quote_obj(out_arena, env.obj_depth, body_val);
 
             Ok(Function {
-                name: Name::new(out_arena.alloc_str(f.name.as_str())),
+                name: f.name,
                 ty: out_arena.alloc(Pi {
                     params: staged_params,
                     body_ty: staged_ret_ty,
diff --git a/compiler/tests/snap.rs b/compiler/tests/snap.rs
index a4726fa..f12b15f 100644
--- a/compiler/tests/snap.rs
+++ b/compiler/tests/snap.rs
@@ -24,7 +24,7 @@ fn snap(#[files("tests/snap/*/*/0_input.splic")] path: PathBuf) {
     let arena = Bump::new();
 
     // ── Phase 1: Lex ────────────────────────────────────────────────────────
-    let lex_result: Result<Vec<_>, _> = Lexer::new(&input).collect();
+    let lex_result: Result<Vec<_>, _> = Lexer::new(&input, &arena).collect();
     let lex_snap = match &lex_result {
         Ok(tokens) => {
             use std::fmt::Write as _;