spec: implement Direction 1 + 2 implicit binder auto-introduction (#20)

[kumavis]

Fixes #20

Closes the planned-but-unimplemented work from
docs/tracking/2026-02-22_IMPROVED_IMPLICIT_INFERENCE.org.

Direction 1. Bare capitalized identifiers in a spec are auto-
introduced as kind-Type implicit binders. {A : Type} is no longer
needed.

Direction 2. Higher-kinded variables get their kind inferred from
:where and inline trait constraints. {C : Type -> Type} is no longer
needed when a Seqable C / Buildable C constraint pins the kind.

Three changes in macros.rkt:

1. The keyword-headed-children merge in process-spec flattens single-
   element :where (Foo A) into the bare constraint (Foo A) and crashes
   expand-bundle-constraints at (car 'Foo). Fixed by keeping known
   list-valued keys (:where, :properties, :laws, :includes,
   :examples, :see-also, :implicits) as lists.

2. After propagate-kinds-from-constraints, the auto-detected portion of
   the binder list is now sorted by kind (kind-Type first, then higher-
   kinded). This matches the convention {A B : Type} {C : Type -> Type}
   that explicit-binder users have written for years and keeps the
   inserted-implicit-arg order stable when callers omit explicit binders.
   Explicit and :over binders keep their declared order.

3. New kind-rank / implicit-binder-kind-ranks-before? helpers; new
   auto-detected-names accumulator threaded through the refinement
   pipeline.

Stdlib refactor: redundant {A : Type}, {A B : Type}, {K V : Type},
and {C : Type -> Type} binders dropped from spec lines across 17 files
in core/ + book/ + data/. The two specs map-merge-with and
map-lattice-leq retain explicit {K V : Type} because the Map-K-V
Lattice impl bodies pass K V as explicit type args; source-walk-order
auto-detection (which sees V first in [V V -> V]) would silently flip
the call-site argument order. Inline comments document the caveat.

Tests: 3 new cases in test-extended-spec.rkt covering the issue's
target form (spec gmap [A -> B] -> [C A] -> [C B] :where (Seqable C) (Buildable C)), bare-vs-explicit idempotence, and the single-constraint
inline :where regression. All 15 affected test files (296 tests) and
all 19 spec/elaborator/HKT/trait test files (389 tests) pass.

Docs: docs/spec/grammar.org and .claude/rules/prologos-syntax.md
updated to document the canonical bare form; design doc flipped
PLANNED → DONE; Master Roadmap entry added.

https://claude.ai/code/session_01UEKqhSHN5y9XEg88BkFnsW

[Copilot]

Pull request overview

Implements the remaining work from docs/tracking/2026-02-22_IMPROVED_IMPLICIT_INFERENCE.org (Issue #20) by making spec signatures auto-introduce implicit binders for free capitalized identifiers (Direction 1) and refine higher-kinded binder kinds based on :where / inline trait constraints (Direction 2), plus updates stdlib specs and documentation to use the canonical “bare” form.

Changes:

• Update process-spec to preserve list-valued WS metadata entries (e.g. (:where (Foo A))) and to canonicalize auto-detected implicit binder ordering by kind after kind propagation.
• Refactor many stdlib/book .prologos specs to drop redundant explicit {A : Type} / {C : Type -> Type} binders.
• Add regression + idempotence tests and update tracking/docs to reflect the completed design.

Reviewed changes

Copilot reviewed 25 out of 26 changed files in this pull request and generated 2 comments.

Show a summary per file

File	Description
racket/prologos/macros.rkt	Fix WS metadata merge shape for list-valued keys; add kind-ranking + post-propagation canonical ordering of auto-detected binders.
racket/prologos/tests/test-extended-spec.rkt	Adds new tests covering D1+D2 combined behavior, bare-vs-explicit idempotence, and single-inline-:where regression.
racket/prologos/lib/prologos/data/transducer.prologos	Removes redundant explicit Type binders from transducer specs to rely on auto-introduction.
racket/prologos/lib/prologos/data/map-entry.prologos	Removes redundant {K V : Type} spec binders.
racket/prologos/lib/prologos/core/string-ops.prologos	Removes redundant {A : Type} from string fold specs.
racket/prologos/lib/prologos/core/set.prologos	Removes redundant {A ... : Type} from set helper specs.
racket/prologos/lib/prologos/core/pvec.prologos	Removes redundant {A ... : Type} from persistent vector helper specs.
racket/prologos/lib/prologos/core/map.prologos	Removes redundant {K V : Type} from map helper specs.
racket/prologos/lib/prologos/core/lattice.prologos	Keeps explicit {K V : Type} for order-sensitive call sites; adds explanatory comments.
racket/prologos/lib/prologos/core/generic-ops.prologos	Removes redundant {A B : Type} {C : Type -> Type} from generic ops specs.
racket/prologos/lib/prologos/core/fio.prologos	Removes redundant {A : Type} from fio-with-file spec.
racket/prologos/lib/prologos/core/collections.prologos	Refactors collection API specs to canonical bare implicit style.
racket/prologos/lib/prologos/book/sets.prologos	Mirrors core set spec refactor in book chapter.
racket/prologos/lib/prologos/book/persistent-vectors.prologos	Mirrors core pvec spec refactor in book chapter.
racket/prologos/lib/prologos/book/maps.prologos	Mirrors core map/map-entry spec refactor in book chapter.
racket/prologos/lib/prologos/book/lattices.prologos	Mirrors lattice set-subset? spec change in book chapter.
racket/prologos/lib/prologos/book/generic-operations.prologos	Mirrors core generic ops spec refactor in book chapter.
racket/prologos/lib/prologos/book/datum-and-homoiconicity.prologos	Mirrors transducer spec refactor in book chapter.
racket/prologos/lib/prologos/book/collection-functions.prologos	Mirrors core collections spec refactor in book chapter.
racket/prologos/lib/prologos/book/characters-and-strings.prologos	Mirrors core string-ops spec refactor in book chapter.
racket/prologos/data/cache/pnet/prologos/data/nat.pnet	Updates a generated .pnet cache snapshot (likely unintended to commit).
racket/prologos/data/benchmarks/failures/test-reducible.rkt.log	Removes benchmark failure log content.
racket/prologos/data/benchmarks/failures/test-pipe-compose-e2e-02.rkt.log	Removes benchmark failure log content.
racket/prologos/data/benchmarks/failures/test-lang-errors-02-ws.rkt.log	Removes benchmark failure log content.
racket/prologos/data/benchmarks/failures/test-lang-errors-01-sexp.rkt.log	Removes benchmark failure log content.
racket/prologos/data/benchmarks/failures/test-lang-04-repl.rkt.log	Removes benchmark failure log content.
racket/prologos/data/benchmarks/failures/test-lang-03-macros.rkt.log	Removes benchmark failure log content.
racket/prologos/data/benchmarks/failures/test-lang-02-ws.rkt.log	Removes benchmark failure log content.
racket/prologos/data/benchmarks/failures/test-lang-01-sexp.rkt.log	Removes benchmark failure log content.
racket/prologos/data/benchmarks/failures/test-functor-ws.rkt.log	Removes benchmark failure log content.
docs/tracking/MASTER_ROADMAP.org	Adds roadmap entry for Improved Implicit Inference (#20) completion.
docs/tracking/2026-02-22_IMPROVED_IMPLICIT_INFERENCE.org	Marks design as DONE and documents implementation details + follow-ups.
docs/spec/grammar.org	Updates spec grammar documentation to present the bare implicit form as canonical.
.claude/rules/prologos-syntax.md	Updates contributor guidance to prefer bare implicit variables in spec.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.