feat: dependent function types

Cargo.toml

@@ -34,7 +34,7 @@ missing_const_for_fn = "deny"
 trivially_copy_pass_by_ref = "deny"
 cast_possible_truncation = "deny"
 explicit_iter_loop = "deny"
-wildcard_enum_match_arm = "deny"
+wildcard_enum_match_arm = "allow"
 indexing_slicing = "deny"
 self_named_module_files = "deny"
 precedence_bits = "deny"

cli/src/main.rs

@@ -49,7 +49,7 @@ fn stage(file: &PathBuf) -> Result<()> {
         checker::elaborate_program(&core_arena, &program).context("failed to elaborate program")?;
     drop(src_arena);
 
-    // Unstage into out_arena; src_arena and core_arena are no longer needed.
+    // Unstage into out_arena; core_arena is no longer needed after this.
     let out_arena = bumpalo::Bump::new();
     let staged =
         eval::unstage_program(&out_arena, &core_program).context("failed to stage program")?;

compiler/src/checker/test/apply.rs

@@ -8,11 +8,11 @@ fn infer_global_call_no_args_returns_ret_ty() {
     let src_arena = bumpalo::Bump::new();
     let core_arena = bumpalo::Bump::new();
     let mut globals = HashMap::new();
-    globals.insert(Name::new("f"), sig_no_params_returns_u64());
+    globals.insert(Name::new("f"), sig_no_params_returns_u64(&core_arena));
     let mut ctx = test_ctx_with_globals(&core_arena, &globals);
 
     let term = src_arena.alloc(ast::Term::App {
-        func: FunName::Name(ast::Name::new("f")),
+        func: FunName::Term(src_arena.alloc(ast::Term::Var(ast::Name::new("f")))),
         args: &[],
     });
     let result = infer(&mut ctx, Phase::Meta, term).expect("should infer");
@@ -34,7 +34,7 @@ fn infer_global_call_unknown_name_fails() {
     let mut ctx = test_ctx(&core_arena);
 
     let term = src_arena.alloc(ast::Term::App {
-        func: FunName::Name(ast::Name::new("unknown")),
+        func: FunName::Term(src_arena.alloc(ast::Term::Var(ast::Name::new("unknown")))),
         args: &[],
     });
     assert!(infer(&mut ctx, Phase::Meta, term).is_err());
@@ -48,11 +48,11 @@ fn infer_global_call_wrong_arity_fails() {
     let extra_arg = src_arena.alloc(ast::Term::Lit(99));
     let args = src_arena.alloc_slice_fill_iter([extra_arg as &ast::Term]);
     let mut globals = HashMap::new();
-    globals.insert(Name::new("f"), sig_no_params_returns_u64());
+    globals.insert(Name::new("f"), sig_no_params_returns_u64(&core_arena));
     let mut ctx = test_ctx_with_globals(&core_arena, &globals);
 
     let term = src_arena.alloc(ast::Term::App {
-        func: FunName::Name(ast::Name::new("f")),
+        func: FunName::Term(src_arena.alloc(ast::Term::Var(ast::Name::new("f")))),
         args,
     });
     assert!(infer(&mut ctx, Phase::Meta, term).is_err());
@@ -67,19 +67,13 @@ fn infer_global_call_phase_mismatch_fails() {
     // `code fn f() -> u64` — object-phase function
     let u64_obj = core_arena.alloc(core::Term::Prim(Prim::IntTy(IntType::U64_OBJ)));
     let mut globals = HashMap::new();
-    globals.insert(
-        Name::new("f"),
-        FunSig {
-            params: &[],
-            ret_ty: u64_obj,
-            phase: Phase::Object,
-        },
-    );
+    let f_ty: &core::Term = core_arena.alloc(core::Term::Pi(Pi { params: &[], body_ty: u64_obj, phase: Phase::Object }));
+    globals.insert(Name::new("f"), f_ty);
     let mut ctx = test_ctx_with_globals(&core_arena, &globals);
 
     // Call `f()` from meta phase — should be rejected.
     let term = src_arena.alloc(ast::Term::App {
-        func: FunName::Name(ast::Name::new("f")),
+        func: FunName::Term(src_arena.alloc(ast::Term::Var(ast::Name::new("f")))),
         args: &[],
     });
     assert!(infer(&mut ctx, Phase::Meta, term).is_err());
@@ -98,7 +92,7 @@ fn infer_global_call_with_arg_checks_arg_type() {
     let arg = src_arena.alloc(ast::Term::Lit(42));
     let args = src_arena.alloc_slice_fill_iter([arg as &ast::Term]);
     let term = src_arena.alloc(ast::Term::App {
-        func: FunName::Name(ast::Name::new("f")),
+        func: FunName::Term(src_arena.alloc(ast::Term::Var(ast::Name::new("f")))),
         args,
     });
     let result = infer(&mut ctx, Phase::Meta, term).expect("should infer");
@@ -140,7 +134,7 @@ fn check_binop_add_against_u32_succeeds() {
     assert!(matches!(
         result,
         core::Term::App(core::App {
-            head: Head::Prim(Prim::Add(IntType {
+            func: core::Term::Prim(Prim::Add(IntType {
                 width: IntWidth::U32,
                 ..
             })),
@@ -173,7 +167,7 @@ fn infer_comparison_op_returns_u1() {
     assert!(matches!(
         core_term,
         core::Term::App(core::App {
-            head: Head::Prim(Prim::Eq(IntType {
+            func: core::Term::Prim(Prim::Eq(IntType {
                 width: IntWidth::U64,
                 ..
             })),
@@ -283,7 +277,7 @@ fn check_eq_op_produces_u1() {
     assert!(matches!(
         result,
         core::Term::App(core::App {
-            head: Head::Prim(Prim::Eq(IntType {
+            func: core::Term::Prim(Prim::Eq(IntType {
                 width: IntWidth::U64,
                 ..
             })),

compiler/src/checker/test/context.rs

@@ -168,15 +168,10 @@ fn arithmetic_requires_expected_type() {
 fn global_call_is_inferable() {
     let arena = bumpalo::Bump::new();
     let arg = arena.alloc(core::Term::Lit(1, IntType::U64_META));
-    let args = &*arena.alloc_slice_fill_iter([&*arg]);
-    let app = arena.alloc(core::Term::new_app(Head::Global(Name::new("foo")), args));
-    assert!(matches!(
-        app,
-        core::Term::App(core::App {
-            head: Head::Global(Name("foo")),
-            ..
-        })
-    ));
+    let global = arena.alloc(core::Term::Global(Name::new("foo")));
+    let args = &*arena.alloc_slice_fill_iter([arg as &core::Term]);
+    let app = arena.alloc(core::Term::new_app(global, args));
+    assert!(matches!(app, core::Term::App(_)));
 }
 
 #[test]
@@ -203,10 +198,7 @@ fn lift_type_structure() {
 #[test]
 fn quote_inference_mirrors_inner() {
     let arena = bumpalo::Bump::new();
-    let inner = arena.alloc(core::Term::new_app(
-        Head::Global(Name::new("foo")),
-        arena.alloc_slice_fill_iter([] as [&core::Term; 0]),
-    ));
+    let inner = arena.alloc(core::Term::Global(Name::new("foo")));
     let quoted = arena.alloc(core::Term::Quote(inner));
     assert!(matches!(quoted, core::Term::Quote(_)));
 }
@@ -276,16 +268,11 @@ fn match_with_binding_pattern() {
 fn function_call_to_global() {
     let arena = bumpalo::Bump::new();
     let arg = arena.alloc(core::Term::Lit(42, IntType::U64_META));
-    let args = &*arena.alloc_slice_fill_iter([&*arg]);
-    let app = arena.alloc(core::Term::new_app(Head::Global(Name::new("foo")), args));
+    let global = arena.alloc(core::Term::Global(Name::new("foo")));
+    let args = &*arena.alloc_slice_fill_iter([arg as &core::Term]);
+    let app = arena.alloc(core::Term::new_app(global, args));
 
-    assert!(matches!(
-        app,
-        core::Term::App(core::App {
-            head: Head::Global(Name("foo")),
-            ..
-        })
-    ));
+    assert!(matches!(app, core::Term::App(_)));
 }
 
 #[test]
@@ -294,15 +281,13 @@ fn builtin_operation_call() {
     let arg1 = arena.alloc(core::Term::Lit(1, IntType::U64_OBJ));
     let arg2 = arena.alloc(core::Term::Lit(2, IntType::U64_OBJ));
     let args = &*arena.alloc_slice_fill_iter([&*arg1, &*arg2]);
-    let app = arena.alloc(core::Term::new_app(
-        Head::Prim(Prim::Add(IntType::U64_OBJ)),
-        args,
-    ));
+    let prim = arena.alloc(core::Term::Prim(Prim::Add(IntType::U64_OBJ)));
+    let app = arena.alloc(core::Term::new_app(prim, args));
 
     assert!(matches!(
         app,
         core::Term::App(core::App {
-            head: Head::Prim(Prim::Add(IntType {
+            func: core::Term::Prim(Prim::Add(IntType {
                 width: IntWidth::U64,
                 ..
             })),

compiler/src/checker/test/helpers.rs

@@ -4,7 +4,7 @@ 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<Name<'static>, core::FunSig<'static>>> =
+    static EMPTY: std::sync::OnceLock<HashMap<Name<'static>, &'static core::Term<'static>>> =
         std::sync::OnceLock::new();
     let globals = EMPTY.get_or_init(HashMap::new);
     Ctx::new(arena, globals)
@@ -15,29 +15,26 @@ pub fn test_ctx(arena: &bumpalo::Bump) -> Ctx<'_, '_> {
 /// The caller must ensure `globals` outlives the returned `Ctx`.
 pub fn test_ctx_with_globals<'core, 'globals>(
     arena: &'core bumpalo::Bump,
-    globals: &'globals HashMap<Name<'core>, core::FunSig<'core>>,
+    globals: &'globals HashMap<Name<'core>, &'core core::Term<'core>>,
 ) -> Ctx<'core, 'globals> {
     Ctx::new(arena, globals)
 }
 
-/// Helper: build a simple `FunSig` for a function `fn f() -> u64` (no params, meta phase).
-pub fn sig_no_params_returns_u64() -> FunSig<'static> {
-    let ret_ty = &core::Term::U64_META;
-    FunSig {
+/// Helper: build a Pi term for a function `fn f() -> u64` (no params, meta phase).
+pub fn sig_no_params_returns_u64(arena: &bumpalo::Bump) -> &core::Term<'_> {
+    arena.alloc(core::Term::Pi(Pi {
         params: &[],
-        ret_ty,
+        body_ty: &core::Term::U64_META,
         phase: Phase::Meta,
-    }
+    }))
 }
 
-/// Helper: build a `FunSig` for `fn f(x: u32) -> u64`.
-pub fn sig_one_param_returns_u64(core_arena: &bumpalo::Bump) -> FunSig<'_> {
-    let u32_ty = &core::Term::U32_META;
-    let u64_ty = &core::Term::U64_META;
-    let param = core_arena.alloc(("x", u32_ty as &core::Term));
-    FunSig {
-        params: std::slice::from_ref(param),
-        ret_ty: u64_ty,
+/// Helper: build a Pi term for `fn f(x: u32) -> u64`.
+pub fn sig_one_param_returns_u64<'a>(arena: &'a bumpalo::Bump) -> &'a core::Term<'a> {
+    let params = arena.alloc_slice_fill_iter([("x", &core::Term::U32_META as &core::Term)]);
+    arena.alloc(core::Term::Pi(Pi {
+        params,
+        body_ty: &core::Term::U64_META,
         phase: Phase::Meta,
-    }
+    }))
 }

compiler/src/checker/test/matching.rs

@@ -10,25 +10,20 @@ fn check_match_all_arms_same_type_succeeds() {
 
     let u32_ty_core = &core::Term::U32_META;
     let mut globals = HashMap::new();
-    globals.insert(
-        Name::new("k32"),
-        FunSig {
-            params: &[],
-            ret_ty: u32_ty_core,
-            phase: Phase::Meta,
-        },
-    );
+    globals.insert(Name::new("k32"), core_arena.alloc(core::Term::Pi(Pi {
+        params: &[], body_ty: u32_ty_core, phase: Phase::Meta,
+    })) as &_);
     let mut ctx = test_ctx_with_globals(&core_arena, &globals);
     let u32_ty = &core::Term::U32_META;
     ctx.push_local("x", u32_ty);
 
     let scrutinee = src_arena.alloc(ast::Term::Var(ast::Name::new("x")));
     let arm0_body = src_arena.alloc(ast::Term::App {
-        func: FunName::Name(ast::Name::new("k32")),
+        func: FunName::Term(src_arena.alloc(ast::Term::Var(ast::Name::new("k32")))),
         args: &[],
     });
     let arm1_body = src_arena.alloc(ast::Term::App {
-        func: FunName::Name(ast::Name::new("k32")),
+        func: FunName::Term(src_arena.alloc(ast::Term::Var(ast::Name::new("k32")))),
         args: &[],
     });
     let arms = src_arena.alloc_slice_fill_iter([
@@ -54,24 +49,19 @@ fn check_match_u1_fully_covered_succeeds() {
 
     let u1_ty_core = &core::Term::U1_META;
     let mut globals = HashMap::new();
-    globals.insert(
-        Name::new("k1"),
-        FunSig {
-            params: &[],
-            ret_ty: u1_ty_core,
-            phase: Phase::Meta,
-        },
-    );
+    globals.insert(Name::new("k1"), core_arena.alloc(core::Term::Pi(Pi {
+        params: &[], body_ty: u1_ty_core, phase: Phase::Meta,
+    })) as &_);
     let mut ctx = test_ctx_with_globals(&core_arena, &globals);
     ctx.push_local("x", u1_ty_core);
 
     let scrutinee = src_arena.alloc(ast::Term::Var(ast::Name::new("x")));
     let arm0_body = src_arena.alloc(ast::Term::App {
-        func: FunName::Name(ast::Name::new("k1")),
+        func: FunName::Term(src_arena.alloc(ast::Term::Var(ast::Name::new("k1")))),
         args: &[],
     });
     let arm1_body = src_arena.alloc(ast::Term::App {
-        func: FunName::Name(ast::Name::new("k1")),
+        func: FunName::Term(src_arena.alloc(ast::Term::Var(ast::Name::new("k1")))),
         args: &[],
     });
     // Both values of u1 are covered — exhaustive without a wildcard.
@@ -98,20 +88,15 @@ fn infer_match_u1_partially_covered_fails() {
 
     let u1_ty_core = &core::Term::U1_META;
     let mut globals = HashMap::new();
-    globals.insert(
-        Name::new("k1"),
-        FunSig {
-            params: &[],
-            ret_ty: u1_ty_core,
-            phase: Phase::Meta,
-        },
-    );
+    globals.insert(Name::new("k1"), core_arena.alloc(core::Term::Pi(Pi {
+        params: &[], body_ty: u1_ty_core, phase: Phase::Meta,
+    })) as &_);
     let mut ctx = test_ctx_with_globals(&core_arena, &globals);
     ctx.push_local("x", u1_ty_core);
 
     let scrutinee = src_arena.alloc(ast::Term::Var(ast::Name::new("x")));
     let arm0_body = src_arena.alloc(ast::Term::App {
-        func: FunName::Name(ast::Name::new("k1")),
+        func: FunName::Term(src_arena.alloc(ast::Term::Var(ast::Name::new("k1")))),
         args: &[],
     });
     // Only 0 covered, 1 is missing — not exhaustive.
@@ -132,25 +117,20 @@ fn infer_match_no_catch_all_fails() {
 
     let u32_ty_core = &core::Term::U32_META;
     let mut globals = HashMap::new();
-    globals.insert(
-        Name::new("k32"),
-        FunSig {
-            params: &[],
-            ret_ty: u32_ty_core,
-            phase: Phase::Meta,
-        },
-    );
+    globals.insert(Name::new("k32"), core_arena.alloc(core::Term::Pi(Pi {
+        params: &[], body_ty: u32_ty_core, phase: Phase::Meta,
+    })) as &_);
     let mut ctx = test_ctx_with_globals(&core_arena, &globals);
     let u32_ty = &core::Term::U32_META;
     ctx.push_local("x", u32_ty);
 
     let scrutinee = src_arena.alloc(ast::Term::Var(ast::Name::new("x")));
     let arm0_body = src_arena.alloc(ast::Term::App {
-        func: FunName::Name(ast::Name::new("k32")),
+        func: FunName::Term(src_arena.alloc(ast::Term::Var(ast::Name::new("k32")))),
         args: &[],
     });
     let arm1_body = src_arena.alloc(ast::Term::App {
-        func: FunName::Name(ast::Name::new("k32")),
+        func: FunName::Term(src_arena.alloc(ast::Term::Var(ast::Name::new("k32")))),
         args: &[],
     });
     // Only literal arms, no wildcard/bind — not exhaustive.
@@ -178,33 +158,23 @@ fn infer_match_arms_type_mismatch_fails() {
     let u32_ty_core = &core::Term::U32_META;
     let u64_ty_core = &core::Term::U64_META;
     let mut globals = HashMap::new();
-    globals.insert(
-        Name::new("k32"),
-        FunSig {
-            params: &[],
-            ret_ty: u32_ty_core,
-            phase: Phase::Meta,
-        },
-    );
-    globals.insert(
-        Name::new("k64"),
-        FunSig {
-            params: &[],
-            ret_ty: u64_ty_core,
-            phase: Phase::Meta,
-        },
-    );
+    globals.insert(Name::new("k32"), core_arena.alloc(core::Term::Pi(Pi {
+        params: &[], body_ty: u32_ty_core, phase: Phase::Meta,
+    })) as &_);
+    globals.insert(Name::new("k64"), core_arena.alloc(core::Term::Pi(Pi {
+        params: &[], body_ty: u64_ty_core, phase: Phase::Meta,
+    })) as &_);
     let mut ctx = test_ctx_with_globals(&core_arena, &globals);
     let u32_ty = &core::Term::U32_META;
     ctx.push_local("x", u32_ty);
 
     let scrutinee = src_arena.alloc(ast::Term::Var(ast::Name::new("x")));
     let arm0_body = src_arena.alloc(ast::Term::App {
-        func: FunName::Name(ast::Name::new("k32")),
+        func: FunName::Term(src_arena.alloc(ast::Term::Var(ast::Name::new("k32")))),
         args: &[],
     });
     let arm1_body = src_arena.alloc(ast::Term::App {
-        func: FunName::Name(ast::Name::new("k64")),
+        func: FunName::Term(src_arena.alloc(ast::Term::Var(ast::Name::new("k64")))),
         args: &[],
     });
     let arms = src_arena.alloc_slice_fill_iter([