Replace the ATF result cache with evaluation from instance equations

[nanavati]

Staged here for the upstream PR to B-Lang-org/bsc (the integration cannot open PRs there; open it from B-Lang-org/bsc@main...nanavati:bsc:claude/itype-rnf-type-var-cache-sddtz9).

Summary

This PR replaces the ATF result cache with direct evaluation from the instance declarations — the rewrite rules the cache was memoizing all along. The cache captured point observations of instance equations at whatever types the typechecker happened to discharge them, serialized them into .bo files, and unioned them across the import closure at elaboration; a miss fell back to expandSynN, a full runTI (the constraint solver) invoked from the middle of elaboration. After this PR, a fully applied ATF application at ground arguments is reduced by a pure evaluator (ATFRules) over the instance equations in the symbol table, and nothing is captured, merged, or serialized.

The deeper invariant this enforces: permanent construction (IConv / ISimplify / IExpand) never consults the typechecker. Reduction at ground types is evaluation — matching is decisive, instance contexts resolve recursively at ground types, no judgment is involved — so the constraint solver's machinery (fresh variables, unification, improvement, deferral, incoherence decisions) is not needed and not reachable from the evaluator. Applications over type variables stay dormant in ISyntax exactly as before: whether and how they reduce is scope-dependent (rigid variables act as atoms) and remains the typechecker's business, settled before ISyntax exists.

Commits

1. Evaluate type functions from instance equations, not the ATF cache — adds src/comp/ATFRules.hs and rewires the consumers. fullTypeNormalizer reduces armed (ground) applications via the evaluator; a ground application that does not reduce is an internal error naming the application, never a solver call. The IATFCache parameter threading disappears from iExpand/genModule/runG (rules are a pure view of the symtab each phase already holds), and elaboration-time cache growth (cExprToIExpr's mergeATFCache) is deleted. The cache's pin tests become rules pin tests (ATFElabReduce, ATFElabImportDef/Use).

2. Retire the ATF cache — removes the production pipeline end to end: recordATFResult / sat's recordATFs, CATFCache / tiATFCache, the ipkg_atf_cache field, its conversion in iConvPackage, and its serialization in GenBin. A .bo now carries declarations and code, never memoized inferences; every consumer can re-derive every reduction from the instance declarations it already reads.

3. IConv: reduce ground ATFs from instance equations, not via runTI — iConvT ran expandSynN (a typechecker instantiation) on every converted type. Conversion is now pure (expandSyn + atfReduceInType); the typechecker round trip survives only for a type still carrying a variable-dependent ATF application, which normalized typechecker output should never produce (kept until enforced by an assertion).

Why the evaluator commits to the same instances the typechecker does

reducePred walks candidates most-specific-first and commits at the first match. On ground arguments, matching is plain structural pattern matching — no substitution into the argument can change which equations match — so "first match in most-specific-first order" is exactly "the unique most-specific matching instance", which is what the evaluator computes directly (with a pairwise generalization test). For a coherent class the overlap check has already guaranteed that any two instances matching the same ground type are comparable; if the evaluator ever finds an ambiguous ground match, that is an unsealed / incoherent family leaking into permanent construction, and it fails loudly rather than guessing.

Instance contexts are consulted only to bind variables the result mentions, by running their fundeps recursively at ground types (e.g. TupleSize'-style helper classes, or a Bits a sa context whose sa appears in the result). Dictionary satisfiability was the typechecker's obligation at the original use site and is not re-verified — the same stance the old cache-hit path took.

Behavior preservation

• The cache was consulted only under canNorm (ground keys), so the polymorphic/open-keyed entries recorded by the typechecker were never readable by any consumer — deleting the capture loses nothing that was reachable.
• normTFun already internalErrored on any ground application the symbol table could not reduce; the evaluator enforces the same contract directly, with a better message.
• The incoherent-match record refusal (previously a careful comment in sat) becomes moot: nothing is recorded at all.
• Full ATF test battery passes (107 tests), including new pins: same-package elaboration-time reduction (with -trace-atf-rules and a check that no ATF application survives into the expanded module) and reduction of a family defined entirely in an imported package. bsc.lib/Prelude (79 tests, including TupleSize) and bsc.binary pass.
• A clean world rebuild (all libraries) succeeds with the new .bo format; existing .bo files are invalidated by the version hash as with any format change.

Performance notes

• IConv no longer pays a runTI per converted type (every type in every package went through expandSynN).
• Elaboration no longer pays a runTI per cache miss; an armed reduction costs a walk of the family's (small) instance equations.
• .bo files shrink by their cache section.

Known restrictions / follow-ups

• Instance heads are matched structurally; a family whose selection requires solving numeric equations in the head (mgu's deferred numeric equalities) is outside the evaluator's domain and fails loudly. No ATF-carrying family in the current libraries does this.
• PrimTypeOf's iToCT/iConvT round trip in IExpand (for synonym-expansion-implemented operators like SizeOf) is orthogonal to the ATF cache and unchanged.
• iConvT's expandSynN fallback for dormant applications is believed unreachable and should become an assertion in a follow-up.
• This is groundwork for the IType interning work: the evaluator is IType-native (matching binds shared subtrees by reference, so reduction cost is proportional to the rule, not the argument), which is what interning needs to keep reductions DAG-bounded — and it makes ATF reduction at construction time possible in principle, since the rules are a monotone, load-time-complete view of the instance declarations rather than solver state.

🤖 Generated with Claude Code

https://claude.ai/code/session_01A6uLp1FBmGTXMVRjWc9byU

---

Generated by Claude Code