Issue #1123: Decision: how the generic `proofs::in_function` moves into Nikaia

ready · opened 2026-11-01 · updated 2026-11-03 · 1 comment

The question

The thread-local accessors of the proof engine move into Nikaia as explicit host parameters (ADR-281 D32 and ADR-289 refuse global and thread-local state). Most of them are plain values. One is not:

// crates/nikaia/src/proofs.rs:131
pub fn in_function<R>(name: &str, at: usize, run: impl FnOnce() -> R) -> R

It sets THREAD.function / function_at, runs run, and restores the old values. with_book<R> works the same way. It is generic in the result: the callers need two result types.

fold_bound.rs:159 collects into a Vec (out.extend(...)).
bounds.rs:303 and :356 hand back walked, of two different types.

A host parameter in_function: fn(String, i64, fn() -> R) -> R needs a function value that is itself generic (rank-2). Nikaia has no such thing, and neither has Rust: a closure is not generic.

Options

A. One host parameter per result type (in_function_proven, in_function_vec, …), each written by hand.

For: it can be built today, with nothing new in the language.
Against: the same thing is written once per type, and every new caller with a new type adds a row. That is debt by the “no technical debt” rule.

B. Generic function values (rank-2) in the language.

For: the accessor stays as it is.
Against: this is a large type-system change. It does not lower to Rust closures (Rust would need a trait with a generic method, which is C anyway). Nothing else needs it now.

C. A host trait with a generic method, statically dispatched.

trait ProofsHost { fn in_function[R](self, name: String, at: i64, run: fn() -> R sync) -> R sync }
fn walk[H: ProofsHost](host: H, ...) { ... host.in_function(name, at, fn() { ... }) ... }

For: idiomatic, and it lowers one to one to fn in_function<R>(&self, ...) with H: ProofsHost. It is monomorphised, so no allocation and no dyn. One place for every proof accessor.
Against: generic methods do not work today. NK1245 fires on a struct method and NK1103 through a bound (#1122, a defect with probes, ready). C waits for #1122.

D. Remove the hidden state: the context becomes data. (name, at) is a value Scope { function: String, at: i64 } that is passed down to the places that read it (ask and the messages). No closure and no in_function remain; in_function(name, at, || body) becomes body with scope passed in. The move rewrites the pattern by hand at each call site.

For: the cleanest by Nikaia’s principles (explicit data instead of a swapped global). No generics needed, nothing waits on #1122, and it does no work at run time.
Against: every function between the setter and the reader gets a parameter (how many: to be counted before building). The move is no longer one-to-one against the Rust, so the differential test compares outputs, not structure.

Recommendation

D, with C as the fallback.

D removes the reason for the generic accessor instead of finding a way to say it. It matches ADR-281 D32 and needs nothing new.
If counting shows the scope has to go through too many layers, C, once #1122 is fixed. #1122 has to be fixed anyway; it is a defect.
A is refused (duplicated, debt). B is not worth it for this one case.

Needs from the owner

D, C or A?
With D: may the move rewrite in_function/with_book into a passed scope (a structural change, compared by output)?

Context: self-hosting (ADR-294, #125).

Generated by Claude Code

Comments

keywan-ghadami, 2026-11-03

Owner, 2026-11-03: the target architecture collects the facts first, and every later phase runs on those facts (#761).

Decision: D. (function, at) becomes a plain value, Scope, that is passed down to its readers. No swapped global and no generic accessor. Scope is shaped as a fact that #761’s phase A will produce, so the later phases read it rather than set it. with_book follows the same pattern.

The move may restructure the call sites. The differential test compares outputs, not structure. C (#1122) stays a defect to fix on its own merits, but it no longer blocks this move.