Tracking issue for "eigentrust pitfall doc" PRs

[kumavis]

done

• #10 Bench migration — independent of pitfalls; reviewer just diffs old API → new API and runs raco make

hiero approved:

• #8 Eta-expansion with mw choice + deferred edge cases
• #13 New AST sentinel across 3 parser files
• #4 Single dispatch branch
• #15 4 library fns mirroring List
• #5 Single library fn

awaiting review:

• #6 Cosmetic + snapshots
• #11 18-line localized macro
• #12 Same dispatch site as parse-reader: splice multi-line spec continuations so -> stays top-level #4 (dedup)
• #16 Compact parser change + flagged latent bug

pending revisit after "elaboration refactor"

• #14 Pre-pass added to 3 processing paths + phase-ordering subtlety
• #17 Small surface (~12 LoC core), but the review hinges on a soundness claim about QTT

needs rethink

• #9 13 of 15 pipeline files (mechanical but exhaustive)

[hierophantos]

Quick cross-reference: while reviewing the pitfall PRs we noticed every spec signature uses explicit {A B C : Type} binders that, per our planned-but-unimplemented "improved implicit inference" work (docs/tracking/2026-02-22_IMPROVED_IMPLICIT_INFERENCE.org), would no longer be needed. Filed as #20 with help wanted — natural follow-up if you're interested.

Mirror of your tracking from our side:

• merged: Migrate bench-bsp-le-track2.rkt to current ATMS API (CI unblock) #10, parse-reader: splice multi-line spec continuations so -> stays top-level #4, Add pvec-zip-with library function (eigentrust pitfalls #13) #5, parser: disambiguate bare-token compound patterns in defn (eigentrust pitfall #7) #16
• approved, awaiting rebase against current main: parse-reader: splice multi-line def := continuations (eigentrust pitfall #15) #12
• next up: pvec: add Int-indexed helpers (eigentrust pitfall #12) #15, parser: preserve Rat-ness of slash-containing number literals (eigentrust pitfall #3) #13, Eta-expand primitive operators on bare reference (eigentrust pitfall #1) #8, pretty-print: emit type-applied forms with [T A] syntax (eigentrust pitfall #14) #6, Multi-line let body wrapping in expand-let (eigentrust pitfall #5) #11
• deferring per your note: Pre-register top-level defn types for mutual recursion (eigentrust pitfall #4) #14, unify: lenient {m0, mw} compatibility (eigentrust pitfall #2) #17, Add [force e] strict-normalization combinator (eigentrust pitfall #11) #9

Thanks for the great structure on this work.