Plan: plans/implementations/evaluator-recursion-and-eq-rec-followup.md (Part 3, Fix A). A def with two or more EXPLICIT params where a later param's type references an earlier one (e.g. `def f (A : Type) (a : A) : A := a`) previously failed to type-check with `type mismatch: <unknown> vs. <unknown>`, independent of Eq/match/GADTs entirely -- confirmed via a minimal repro (`def a3 (A:Type)(a:A):I64 := 5`, fails even though the body doesn't use `a`). Implicit `{A}` params (Forall) already worked; only explicit Pi telescopes were broken. This blocked any hand-written dependently-typed function, not just Eq.rec. Root cause and fix, three parts: 1. parser.rs's def-param-list desugaring built each param's Pi via pi_with_mult, which always set arg_name: None (Term::Pi's own binder-name field) -- unlike Term::Forall, which always carries a real name. lower_core.rs's Pi-lowering pushes arg_name into scope before lowering ret; with no name to push, a later domain's reference to an earlier param's name fell through to ordinary global-name resolution instead of a Bound reference, independently (and inconsistently) between the type-lowering pass and the body's own Term::Lam chain (which DOES carry real names). Fixed with a new pi_named_with_mult (term.rs), threading each param's real name through at the one call site that builds a def's own Pi-typed signature from its param list. 2. That alone only fixed DECLARING such a function. APPLYING one (e.g. `myid I64 5`) surfaced a second, independent gap: an ordinary inductive's own bare name (`I64`, `Bool`) used as a VALUE (not just a type annotation) had no `ctx` kind entry -- core_check_module.rs's inductive registration only ever gave constructors a type, never the inductive itself (a documented, previously-deliberate omission, "never needed before"). Fixed by registering each ordinary inductive's own declared kind (`ind.typ()`) into ctx too. 3. Comparing a concrete type's freshly-registered kind (a raw Sort{level:1} literal) against "Type"-as-surface-syntax (which resolves to Free(the "Type" keyword atom) via ordinary name resolution, not directly to CoreTerm::Sort, unlike explicit "Sort N") still failed structural unification. Fixed with a narrow special case in core_unify.rs's unify: treat Free(atom) as interchangeable with the Sort it stands for when atom is one of the three well-known "Type"/"Prop"/"Pred" keyword atoms (core_check_module.rs's own pre-existing "E7" registration), applying the same cumulativity rule already used for Sort-vs-Sort. 4. Applying such a function successfully then hit a THIRD gap at evaluation time: lower_core_ir.rs's global-slot assembly had no runtime representation for an ordinary inductive's bare name used as a value either (only "Type"/"Prop"/"Pred" had this, via builtin_sort_level) -- "eval error: unresolved global: I64". Fixed by extending the same fallback to any registered inductive, defaulting to Sort(1) (correct for ordinary data types; a narrow, accepted gap for a bare, unapplied `: Prop` inductive's own name used as a value, not exercised by anything this fixes). Verified end-to-end, not just type-checked: `myid I64 5` and a GADT case (`dep (n:Nat)(v:Vec n I64)`, applied to `Vec.nil`) both type-check AND evaluate to the correct result. Still blocked, a separate and larger gap: Eq.rec's own full 6-explicit- param signature hits a THIRD, distinct issue beyond this fix -- core_ unify.rs's unify never reduces (WHNF/beta/delta) a type-level application before structurally comparing it, so a param whose declared type is itself a function application (e.g. `h : P a`, P a type-level function) can't be checked against an already-evaluated concrete type. Reproduced minimally, Eq-free: `foo3 Bool foo identity_type foo` (P := identity_type, a plain `Bool -> Type` function) fails with `type mismatch: Bool vs. (identity_type foo)` even though identity_type always returns Bool. This is a real, separate, and substantially larger piece of work (definitional- equality/conversion checking in the unifier) -- not attempted here; flagged for a dedicated follow-up. Also fixes 7 pre-existing parser test fixtures (declarations.rs, do_notation.rs, docstrings.rs) whose hardcoded expected ASTs asserted the old, incorrect arg_name: None for a def's own multi-param signature -- updated to the new, correct arg_name: Some(param_name). New tests (core_check_module.rs): 3 permanent regressions, confirmed to fail on the pre-fix code via a partial git-stash revert -- test_dependent_explicit_pi_telescope_definition_checks, ..._application_checks, ..._over_gadt_index_checks. Verification: - cargo test: 679/679 (676 + 3 new), 0 failed - cargo run --release -- test init std lang examples: 1287/1287, byte-identical - cargo run --release -- check init std lang examples: byte-identical (101 files, 2 errors, 62 warnings) - cargo run --release -- test slow_tests: same 29 pre-existing test_typecheck_* failures, not a new regression Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>