Skip to content
BANG

ADR-0103 · ∀-generalization for bound-free self-recursive generics: a call-site-monomorphization pre-pass (the List-family door)

  • Status: Accepted

  • Summary: A bound-free self-recursive generic (length : List a -> Int, the whole List family: append/take/drop/zip/range/replicate) is realized by the SAME elaborate-to-mono move as every other generic (ADR-0075/0079/0080/0082): a pre-elabS pass discovers the FINITE set of concrete instantiations from the program's call sites, and emits ONE monomorphic let rec residue per instantiation — exactly the two-residues-by-hand program of witness w3, auto-generated. The kernel / Source.eval / HasCTy / soundness NEVER see a ∀, a tyvar, or a bound (invariant #4/#5 hold, census byte-identical). The fork's TWO surface doors — (a) "real top-level ∀ for let rec ascriptions" and (b) "a bound-FREE bounded-fn" — collapse to the same mechanism (one construct per problem): both need call-site-driven monomorphization of an ARGUMENT-position tyvar; door (b)'s reuse-the-bounded-fn-seam framing is REFUTED (witness w2 — ADR-0080's bfnWrapper requires the carrier in RESULT position, the fold shape … -> a; the List family's carrier is in ARGUMENT position, List a -> Int). The honest MINIMAL door (c) — monomorphic prelude entries per base type (lengthI/lengthB/…) — is priced and rejected (combinatorial blowup, no genericity). Verdict: adopt the monomorphization-pre-pass framing (door a ≡ door b); defer implementation to its own spike; the surface spelling is a bound-free let rec ascription (let rec length : List a -> Int), no new where syntax.

  • Depends-on: 0075, 0080, 0079, 0073, 0069

  • Relates-to: #120 (the machine-traced wall this resolves), #105 (the 9-10/10 List-family residue it gates), Q26 (the generic lawful stdlib), R6 / docs/notes/lambda-cube-ascent-survey.md (the finiteness gate this lives inside), #55 (annotation-driven generic CONSTRUCTION — the append/zip half's residual dependency)

  • Status: Accepted (kernel-engineer consult 2026-07-11; the OPERATOR ratifies — a type-power extension, invariant #4/#5 discipline; landed 2026-07-11: monomorphizeLetRec implemented as the expandBFns twin, Prelude.bang's take/drop shipped as the List-consumer payoff. length and a kernel-provided List deferred — see the Implementation note below for the residual findings this session established empirically)

  • Date: 2026-07-11

  • Layer: C + checker/elaborator (tested superset). Frontend LEAF (Frontend/TypeCheck, the elaborate-away seam); census byte-identical, kernel untouched. NO Spec.lean / Kernel change (a kernel change would be a REFUTATION finding — it is not needed; witnesses w0/w3 prove the residues already run).

Context — the #120 wall (machine-traced, refute-first)

Every List-family prelude entry is a self-recursive function generic over the element type with NO trait bound (length : List a -> Int, append : List a -> List a -> List a, …). The corpus has NO such entry today — only monomorphic List Int recursion (nqueens, Prelude's Str-typed folds) and NON-recursive generics (mapOption/bimap, which ride let-generalization). #120 traced two failure modes; both are reproduced against the real binary in witness-0103/:

witness   program                                    observed (bang run / check, 2026-07-11)
───────   ────────────────────────────────────────   ──────────────────────────────────────────────
w0        let rec length : List Int -> Int  (mono)    2          — the RESIDUE; certifies TOTAL
w1        let rec length : List a  -> Int  (free a)   error: unknown type name 'a'   — THE WALL
w2        fn length(xs):List a->Int where Monoid a    error: … result type must be 'a' (fold shape)
w3        two mono residues (Int + Unit+Unit) in one  3          — the monomorphization TARGET
w4        non-rec `id` at two types (generalizes)     5          — why let-general can't be reused

The wall is ONE line. w1 fails at resolveTy env.gen env.aliases t env.effects in the .letRecS elaboration arm (TypeCheck.lean:3033): resolveTyG's .tName "a" arm finds no σ-entry (no type params bind at top level) and no self? match, so resolveName fails loud "unknown type name 'a'". No construct introduces a free top-level ∀a. Everything downstream — structOK/Div certification, the buildLetRec μ-knot, the bidirectional checker — is INERT to the tyvar once it is closed to a concrete type: witnessed by w0 (length : List Int -> Int type-checks, certifies total, runs).

Why let rec can't ride the let-generalization that non-recursive generics already use (w4, the #120 "say precisely why" ask). ADR-0075 bite-0b generalizes a let-bound THUNK's value type (the ⑦b id example — w4 runs id at two types). The obstacle for let rec is NOT the ascription resolution alone; it is the SELF-KNOT. In the .letRecS arm the recursive name is bound in its own body at a SINGLE fixed monomorphic thunk type uT := .U botR (embC (ctyOf t')) (TypeCheck.lean:3034), and buildLetRec closes the μ-knot Rec = μX. Thunk(X → T) over a CONCRETE t'. Generalizing the ascription would require the recursive CALL to instantiate the scheme at a fresh type — i.e. polymorphic recursion, which is undecidable (the R6 §4 mono-instantiation wall: no finite instantiation set by construction). But the List family is UNIFORM: $length t calls length at the SAME a as the caller — monomorphic recursion, which monomorphization handles by construction. So the barrier is "the self-knot is monomorphic", and the fix is to close the tyvar BEFORE building the knot (once per call-site instantiation), never to generalize the knot itself.

The fork, refuted both ways

Door (a) — real top-level ∀ for let rec ascriptions. Generalize the ascription's free tyvars (close over the decl, HM-style). Falsifier outcomes:

  • The checker's self-recursion seeding: a SCHEMATIC seed breaks the fixpoint (polymorphic recursion, above). REFUTED as stated — a genuine ∀-scheme in the self-knot is undecidable.
  • BUT: if "generalize" means "instantiate the scheme per call site and monomorphize each" (the elaborate-to-mono reading, NOT a residual ∀ in the knot), it is decidable and sound — this is the same monomorphization ADR-0075/0080 already run, applied to an argument-position tyvar. This reading SURVIVES.

Door (b) — a bound-free bounded-fn (fn length(xs) : List a -> Int where a = …, or for a / bare where a). Falsifier outcomes:

  • The fold-shape wall (w2, DECISIVE). ADR-0080's carrier-fixing is annotation-driven off the RESULT type: bfnWrapper (TypeCheck.lean:2642) requires the declared result to BE the bound var (… -> a). The List family's tyvar is in ARGUMENT position (List a -> Int, result Int). Even with a vacuous bound, the bounded-fn path rejects it (w2, observed on the real binary). So "reuse the bounded-fn seam, minus the dictionary" does NOT work — the seam's whole carrier-discovery assumes result-position, and the ops-splicing step (env.rawImpls.find?) has nothing to splice for a bound-free fn anyway. The dictionary is not the only thing to drop; the entire carrier-from-result mechanism is wrong for this family. REFUTED as a bounded-fn variant.
  • The empty-dictionary question ("does the splice step become a no-op?"): moot — the splice step is reached only AFTER the fold-shape check passes, which it never does for List a -> Int.

Same mechanism (one construct per problem). Once door (b) is stripped of the bounded-fn framing, what BOTH doors need is identical: discover the finite instantiation set of an argument-position tyvar from call sites, monomorphize the let rec per element. Door (a) reaches it by "generalize-then-instantiate-per-use"; door (b) by "bound-free fn monomorphized per use". These are the same elaborate-to-mono pass with two surface spellings. Adopting BOTH surfaces would be two constructs for one problem. We adopt ONE: the existing let rec … : T = … ascription form, with resolveTy extended to admit free tyvars (closed by the monomorphization pre-pass), and NO new where/for/fn syntax. Rationale: let rec is already the generic-recursion surface (ADR-0073); the wall is purely that its ascription can't NAME a free tyvar. Fixing that one gap is minimal; adding a parallel bound-free fn form is a second door onto the same room.

Decision

  1. A call-site-monomorphization pre-pass (structurally the expandBFns twin, ADR-0080): a pure fuel-bounded Surf → Surf rewrite running BEFORE elabS. For each bound-free generic let rec, collect the concrete types at which it is applied (the instantiation set), emit one specialized let rec residue per instantiation (resolveTy's tyvar closed to that concrete type, then the existing buildLetRec μ-knot), and rewrite each call site to its residue. The kernel sees only the concrete residues (w0/w3 prove they run).
  2. Surface: the bound-free let rec ascription. let rec length : List a -> Int = … — a free tyvar in the declared type is admitted; NO new syntax. resolveTy/resolveTyG gain a "collect free tyvars as generalizable" reading at the .letRecS/top-level-decl entry (the ONLY sites that may introduce a top-level scheme — every other resolveTy caller stays fail-loud on an unknown name, preserving the typo-catch).
  3. Instantiation discovery is annotation-anchored, finiteness-gated (R6). v1 discovers the carrier from each call site's argument/annotation (the ADR-0079/0080 annotation discipline), computing a FINITE closed instantiation set. A call whose carrier is itself unresolved (a generic used inside another un-instantiated generic — polymorphic recursion / an unbounded set) is a LOUD error ("annotate the use" / "cannot monomorphize"), never a guess — the R6 finiteness gate as a fitness function, the type-system analog of Div.
  4. structOK/Div is inert (verified). Certification runs AFTER monomorphization on ground residues (w0: length : List Int -> Int certifies TOTAL with no Div marker). No change to structOK.
  5. Kernel/Spec.lean UNTOUCHED. No ∀ reaches the kernel; residues are ordinary monomorphic let recs. This is the fifth elaborate-away win (after ADR-0075/0079/0080/0082); the census (18→20 headline theorems) does not move.

Rejected / staged

  • Door (b) as a bounded-fn variant (where a / for a). REFUTED by the fold-shape wall (w2): ADR-0080's carrier lives in result position; the List family's is in argument position. Not a syntax tweak — a different discovery mechanism. Rejected in favor of extending let rec.
  • A residual ∀-scheme in the self-knot (naive door a). Polymorphic recursion, undecidable (R6 §4). The monomorphize-per-call-site reading is adopted instead.
  • (c) Monomorphic prelude entries per base type (lengthI : List Int -> Int, lengthB : List (Unit+Unit) -> Int, …). The "ugly-but-tomorrow" floor: it WORKS today (w0/w3 are literally this, by hand) but requires one hand-written entry per (function × base type) — a combinatorial blowup with no genericity, and it does not scale past Int to user data types. It is the fallback if the pre-pass slips, and the ground truth the pre-pass must reproduce — but not the ship target. Priced and rejected as the primary door.
  • A System F kernel (carry the ∀ in HasCTy/the LR/soundness/CalcVM). Spine work, unnecessary — elaborate-to-mono is the standing architecture (ADR-0075). Rejected (invariant #4/#8).

The sites-to-change map (for the implementing spike)

site                                            change
──────────────────────────────────────────     ─────────────────────────────────────────────────
TypeCheck.lean:3033 (.letRecS `resolveTy`)      the CHOKEPOINT: admit a free tyvar in the ascription
                                                (collect-as-generalizable), not fail-loud
resolveTyG/.tName arm (:1821-1828)              a new "free tyvar → generalizable marker" reading,
                                                gated to the top-level/`.letRecS` entry only
                                                (other callers unchanged — typo-catch preserved)
a new `monomorphizeLetRec` pre-pass             the `expandBFns` twin (:2698): discover the finite
                                                instantiation set from call sites, emit one
                                                `buildLetRec` residue per element, rewrite calls
elabProg wiring                                 run the pre-pass before `elabS` (as `expandBFns` runs)
genericPrelude / Prelude.bang (:3531)           the List family becomes expressible as bound-free
                                                `let rec` entries (the #105 payoff)
buildLetRec (:2347)                             UNCHANGED (each residue is a concrete `let rec`)
structOK / letRecRow (:2295)                    UNCHANGED (runs on ground residues, w0)
Kernel / Spec.lean / Core                       UNTOUCHED (no `∀`, invariant #4/#5)

R6-consistency argument (the finiteness gate)

This lives entirely inside the elaborate-to-mono rung the R6 survey already priced. length : List a -> Int is the F (∀) rung, which the survey records as SHIPPED via monomorphization (lambda-cube-ascent-survey.md §1, the "won five times" line). A bound-free generic is STRICTLY LESS demanding than a bounded one: no dictionary, no trait resolution, no impl lookup — just close a tyvar. The instantiation set is discovered from call sites exactly as bounded-fn carriers are (ADR-0080), and for the uniform (monomorphic-recursion) List family it is FINITE and CLOSED at elaboration time — the §4 gate holds. The one place it could fail the gate is polymorphic recursion (a self-call at a DIFFERENT type, growing the set unboundedly); that is caught loud by the finiteness check (decision item 3), never monomorphized silently. Kernel untouched, census stable — the survey's licence extends here conditional on the finiteness gate, exactly as it does for the bounded rung.

Implementation (2026-07-11) — the residue and residual findings, established empirically

monomorphizeLetRec (the expandBFns twin, Bang/Frontend/TypeCheck.lean) discovers a bound-free let rec's instantiation set from ANNOTATED call-site arguments ((($f) arg : T) — the argument- position twin of bfnWrapper's result-anchored discovery, w2's own decisive reason the two can't share a mechanism) and emits one monomorphic residue per distinct instantiation, wired into elabProg right before elabS. Four corpus #guards (Bang/Examples.lean §F) pin: the w3 two-residue shape now expressible as ONE bound-free let rec; lexical shadowing; the zero-call-site DROP (an unreferenced generic costs nothing, the expandBFns/env.bfns precedent); and polymorphic recursion REJECTED loud by the downstream type-checker (not a targeted diagnostic yet — a type mismatch, since every self-call inside one residue forces to that residue's own name regardless of its own annotation — safe, never silently wrong, but a coarser message than "annotate the use").

CONSTRUCTION REFUTES this ADR's own residual-dependency framing above. append/take/drop/ zip all CONSTRUCT (Cons(h, tail)) inside a monomorphized residue and run correctly WITHOUT any #55 annotation-free-inference work — because by the time elabS sees a residue, its tyvar is ALREADY closed to a concrete type by substTyVar; Cons(h, tail) is then ordinary MONOMORPHIC construction, not generic inference. Verified live: append/take both build + consume List Int correctly, chained through an intermediate let with no annotation on the DOWNSTREAM use (only the generic function's OWN call site needs the anchor). The REAL boundary is narrower and different in kind than "construction vs consumption": it is whether the call site that discovers the instantiation carries an explicit annotation — #55's annotation-free CONSTRUCTION wall is a SEPARATE, still-real gap for a DIFFERENT case (an un-annotated ctor intro with no enclosing type context at all), but it does not gate the List family's constructing half the way this ADR assumed.

Two residual gaps found, priced, and left open (not this session's scope):

  1. The auto-use alias indirection (ADR-0098): an unqualified prelude call ($take …) resolves through a let take = Prelude_take in … alias, not a direct reference to the qualified let rec's own name — invisible to monoCallSpine's discovery without a dedicated collapse pass (inlineVarAliases, added this session, narrow: only the ONE bare-.var-RHS shape the module system produces, not a general copy-propagation optimizer).
  2. A kernel-provided List is NOT shipped (deferred, not fixed): data List a referenced ONLY via a type ANNOTATION (never a bare .var) is invisible to injectPrelude's mention-filter (progUsesVar/surfUsesVar scan value positions only, never a .annotS's Ty slot) — so List can't ride Prelude.bang's mention-filtered injection the way take/drop do. Adding it to the UNCONDITIONAL genericPrelude bucket instead (alongside Option/Result) was tried and reverted: its natural ctor names Nil/Cons, made globally visible, collide with SEVERAL pre-existing corpus fixtures that independently chose the SAME bare names for their OWN differently-named list-shaped data decls (listProg's data IntList = Nil | Cons(…), confirmed live via ADR-0099 ambiguous-bare-ctor cascades). take/drop still work today against a program's OWN data List a declaration — only the zero-declaration convenience is deferred.

What the List family costs once the door opens

The 9-10/10-universal List family (#105's final residue) becomes expressible as bound-free let rec prelude entries. CONSUMING members (length/take/drop/sum) are unblocked immediately (w0/w3 prove the residues run + certify) — SHIPPED for take/drop; length itself is withheld (not a mechanism gap — its NAME collides with a pervasive corpus-local helper of the same name, taxing several tight-fuel #guards the moment it entered the mention-filtered prelude; a rename or a fuel-bump sweep would resolve it, out of this session's scope). CONSTRUCTING members (append/zip/range/replicate) do NOT carry the #55 dependency this ADR originally assumed — see the Implementation note above; they are blocked only by the SAME Prelude.bang mention-filter gap List itself hits (a construction call site needs List/Nil/Cons resolvable, which needs either a kernel-provided List or the caller's own data List a), not by annotation-free inference.

Revisit if

Polymorphic recursion is genuinely needed (a self-call at a different type) — that pressures the finiteness gate and is the R6 λ2/dependent frontier, its own K-ADR; OR annotation-free carrier inference (#55) is taken up, unblocking the constructing half; OR a bound-free fn surface is demanded independently of let rec (would reopen the one-construct-per-problem choice).

Amendment ① (2026-07-11, operator-ratified) — the List injection ships unconditionally

The Implementation note's residue 2 ("a kernel-provided List is NOT shipped… tried and reverted") is superseded: the design probe docs/notes/listdecl-injection-design.md (12 witnesses, run against the built binary) established that the revert's blocker is not a wall but a priced migration. With ADR-0099's B012 in force plus the D4 type-name shadow (witnessed arity-agnostic, w10 — a fact neither landing ADR recorded), unconditional injection is SOUND: a user's same-name List shadows silently; a differently-named list-shaped data with bare Nil/Cons gets a LOUD B012 ambiguity naming both candidates — a local, one-line qualification fix at each colliding corpus fixture, not a silent break. The operator ratified shipping data List a = Nil | Cons(a, List a) in the UNCONDITIONAL genericPrelude bucket (alongside Option/Result; zero fuel for non-users — data registration is not a letC step; sidesteps the mention-filter's .annotS Ty-blindness entirely) and accepted the corpus migration cost. Candidate (f) (type-scan the mention filter) stays the priced fallback; (g) (namespaced-only ctors) stays rejected.

length's residue is ruled: fuel-sweep (operator, over the note's cheaper rename) — the canonical name is worth the corpus touch; the sweep carries the same regression discipline as any contract change. Implementation rides the #105 first-slice lane.

Amendment ② (2026-07-12, operator-ratified) — result-position discovery closes #55's residual gap

This ADR's own "Revisit if" named the door: "annotation-free carrier inference (#55) is taken up, unblocking the constructing half." docs/notes/carrier-inference-design.md (design-first, live-witnessed against the built binary) traced the residual gap PRECISELY: a bound-free let rec's tyvar appearing ONLY in the declared RESULT (never in any argument — e.g. mapOpt : (a -> b) -> Option a -> Option b's b) was undiscoverable no matter how the call's arguments were annotated, because callSitesOf's .annotS e t arm discarded t (the annotation's own type) before this ADR's discovery mechanism (discoverAtCall) ever ran. The note also corrected #55's own framing: the SIMPLE case #55 named ("a generic combinator cannot construct generic data") was ALREADY CLOSED by ADR-0079's check-mode/synth-mode split (a bare Some(3) in synth position infers today) — only the bound-free-let rec-with-a-result-only- tyvar shape remained open, a narrower residue than #55's title suggested.

Decision: extend discoverAtCall's mechanism to a second input, discoverAtCallResult, matched against the call's own enclosing annotation when present — reusing matchTyVars UNCHANGED (no new inference power; the unifier already handles tArr/tProd/tSum/tApp/ tThunk structurally, it was simply never invoked on a result/annotation pair before). This is the SAME mechanism this ADR's own decision item 1 established for arguments, extended to a second discovery SITE, not a parallel inference system — the one-construct-per-problem discipline this ADR already committed to for the argument-position half.

Implementation (Bang/Frontend/TypeCheck.lean): callSitesOf/redirectCalls's WHOLE mutual groups gain a resultDom : Ty parameter (stripArrows tvs.length t, the ascription-side twin curriedDomains already is for arguments) threaded the SAME read-only way domains already is. The ONE structurally-interesting site is callSitesOf's .annotS inner t arm: when inner is EXACTLY name's call spine, t is matched against resultDom and MERGED into that spine's own binding (not a separate call site — completeInstantiation needs every tyvar's discovery unioned per call). redirectCalls re-derives the IDENTICAL merged binding at its own .annotS arm so the two passes agree on which residue a result-anchored call belongs to (by construction: same inputs, same discoverAtCall/discoverAtCallResult calls).

The fail-loud extension this door needed and the argument-only door never did. Before this Amendment, completeInstantiation's "last occurrence wins" convention silently collapsed repeated bindings for the same tyvar — SAFE when the only source was arguments (two List a arguments always agree on a by construction), but WRONG once a result annotation can also contribute a binding: an argument saying Int and a result saying Char for the same tyvar is a genuinely contradictory program, and silently preferring one is exactly the guess this whole discovery discipline refuses to make everywhere else. findConflict (checked BEFORE the silent collapse could hide it) detects a genuine disagreement (structurally different concrete types for the same tyvar within one call's binding) and refuses loud, naming the tyvar and both conflicting types (B017, Bang/Frontend/DiagCodes.lean) — never picking a winner.

Rejected (unchanged from this ADR's original door-refutation): HM-style let-generalization (a genuine top-level ∀ deferring monomorphization to every downstream use) — still REJECTED, still for the same reason (door (a)/(c) above: a residual ∀ in the self-knot is polymorphic recursion, undecidable, the R6 §4 finiteness wall). Amendment ② stays entirely within the FINITE, per-call-site discovery discipline this ADR already committed to; the kernel / Source. eval / HasCTy still never see a type variable (census byte-identical, invariant #4/#5 hold).

Witnessed (Bang/Frontend/TypeCheck.lean's compiled corpus, runTypedYieldsInt): a genuinely result-only tyvar (mkNone : a -> Option b) resolves from the call's OWN annotation alone; TWO independent instantiations of the same result-only tyvar in one program produce two distinct residues (the SAME distinct-instantiation-set discipline this ADR's decision item 1 already established for arguments); the disagreeing-annotation case fails loud with B017, never a guess.