feat: add names arena and thread 'names lifetime through IR

.gitignore

@@ -4,3 +4,4 @@ scratch/
 posts/
 .claude/settings.local.json
 .claude/worktrees/
+.opencode/package-lock.json

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.

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)
     }
 }

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)
 }