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

.claude/rules/prologos-syntax.md

@@ -42,7 +42,7 @@
 
 - **Prefer type inference** where unambiguous -- `def x := 42` over `def x : Int := 42`. We work hard on inference; lean on it. Use explicit annotations when the type is genuinely ambiguous (union types, polymorphic contexts) or for documentation in specs.
 - **Angle brackets for complex types** -- `<Int | String>`, `<(x : A) -> B>`.
-- **`{A B : Type}` for implicit erased binders** in `spec`.
+- **Skip `{A : Type}` and `{C : Type -> Type}` in `spec`** -- bare capitalized identifiers are auto-introduced as implicit binders. Kind-`Type` vars (D1) come from any free occurrence; higher-kinded vars (D2) get their kind inferred from `:where` / inline trait constraints. Explicit binders remain useful for pedagogic examples, for the rare spec with no constraining position (`spec empty {A : Type} [List A]`), and when the body passes type args explicitly in a specific order.
 
 ## Lists and literals
 

docs/spec/grammar.org

@@ -811,16 +811,60 @@ def- internal-state : Nat zero
 ;; Simple function type
 spec factorial Nat -> Nat
 
-;; With implicit type parameters
-spec map {A B : Type} [A -> B] [List A] -> List B
+;; Bare type variables — auto-introduced
+;; (kind-`Type` vars and higher-kinded vars constrained by `:where`)
+spec map [A -> B] [List A] -> List B
 
-;; With trait constraints
-spec elem {A : Type} [Eq A] A [List A] -> Bool
+;; With trait constraints — the implicit binder is also auto-introduced
+spec elem [Eq A] A [List A] -> Bool
+
+;; Higher-kinded — `C` is inferred to have kind `Type -> Type`
+;; from the `Seqable C` / `Buildable C` constraints.
+spec gmap [A -> B] -> [C A] -> [C B]
+  :where (Seqable C) (Buildable C)
 
 ;; With varargs
 spec sum-all Nat ... -> Nat
+#+end_src
 
-;; With multiple implicits and constraints
+*** Auto-Introduced Implicit Binders
+
+A capitalized identifier that appears free in a =spec= signature (and is not a
+known type or trait name) is auto-introduced as an implicit binder.  Two
+directions of inference cooperate:
+
+- *Direction 1.* Free type variables are auto-introduced with kind =Type=.
+  ={A : Type}= almost never needs to be written.
+- *Direction 2.* Higher-kinded variables (e.g. =C : Type -> Type=) are
+  inferred from =:where= clauses and from inline trait constraints.  When
+  =Seqable= is declared over ={C : Type -> Type}=, a free =C= used at
+  =[Seqable C]= or =:where (Seqable C)= is auto-introduced with the trait's
+  declared kind.
+
+#+begin_src prologos
+;; Equivalent — the bare form is the canonical style:
+spec gmap {A B : Type} {C : Type -> Type} [A -> B] -> [C A] -> [C B]
+  :where (Seqable C) (Buildable C)
+
+spec gmap [A -> B] -> [C A] -> [C B]
+  :where (Seqable C) (Buildable C)
+#+end_src
+
+Auto-detected binders are placed after explicit binders and sorted by kind
+(=Type= first, then higher-kinded), matching the convention users have
+written by hand.
+
+Explicit binders remain useful for:
+
+- *Pedagogic clarity* — when documenting a teaching example.
+- *Disambiguation* — when no constraining position pins the kind, e.g.
+  =spec empty {A : Type} [List A]=.
+- *Order-sensitive call sites* — when a body explicitly passes type
+  arguments in a particular order, declaring the binders explicitly fixes
+  the order against the source-walk-order auto-introduction would produce.
+
+#+begin_src prologos
+;; Multiple implicits and constraints (still works):
 spec sort-on {A B : Type} [B -> B -> Bool] [A -> B] [List A] -> List A
 #+end_src
 

docs/tracking/2026-02-22_IMPROVED_IMPLICIT_INFERENCE.org

@@ -1,6 +1,8 @@
 #+TITLE: Improved Implicit Binder Inference
 #+DATE: 2026-02-22
-#+PROPERTY: Status PLANNED
+#+PROPERTY: Status DONE
+#+PROPERTY: Closed 2026-04-30
+#+PROPERTY: Issue #20
 
 * Summary
 
@@ -75,3 +77,82 @@ Should be implemented before or alongside Phase 1 of the extended spec.
 - ~propagate-kinds-from-constraints~ (macros.rkt)
 - Trait store for kind lookups
 - ~process-spec~ pipeline
+
+* Implementation (Issue #20, 2026-04-30)
+
+** What landed
+
+- *Direction 1.* The auto-introduction logic in =process-spec=
+  (=auto-detected-binders= at ~macros.rkt:3424~) walks the type tokens and
+  constraint argument lists for free capitalized identifiers, filters out
+  known type names / locally-bound Pi binder names / explicit binders, and
+  registers each survivor as an implicit binder with default kind =(Type 0)=.
+  This was already wired but not documented as canonical and not exploited by
+  the stdlib.
+
+- *Direction 2.* =propagate-kinds-from-constraints= refines an
+  auto-introduced binder's kind whenever a constraint pins it (e.g. a free
+  =C= with =:where (Seqable C)= picks up =Seqable='s declared kind
+  =Type -> Type=).  Inline trait constraints participate via
+  =extract-inline-constraints=.
+
+- *Canonical-order sort.*  After kind refinement, the auto-detected portion
+  of the binder list is sorted by =kind-rank= (kind-=Type= before
+  higher-kinded) so the inserted-implicit-arg order matches the convention
+  ={A B : Type} {C : Type -> Type}= that explicit-binder users have written
+  for years.  Explicit (and =:over=) binders keep their declared order.
+  Source-walk-order auto-introduction otherwise put inline-constraint vars
+  (e.g. =C= in =[Reducible C]=) ahead of value-position vars (=A=) and
+  silently flipped the inserted argument order.
+
+- *Single-constraint inline =:where= bug fix.*  The keyword-headed-children
+  merge in =process-spec= used to flatten a single =(:where (Foo A))= entry
+  into the bare constraint =(Foo A)=, which then crashed
+  =expand-bundle-constraints= at =(car 'Foo)=.  The merge now keeps known
+  list-valued keys (=:where=, =:properties=, =:laws=, =:includes=,
+  =:examples=, =:see-also=, =:implicits=) as lists.
+
+** Stdlib refactor
+
+Redundant ={A : Type}=, ={A B : Type}=, ={K V : Type}=, and
+={C : Type -> Type}= binders were removed from spec lines across the
+stdlib:
+
+- =racket/prologos/lib/prologos/core/= — =collections.prologos=,
+  =generic-ops.prologos=, =fio.prologos=, =map.prologos=, =pvec.prologos=,
+  =set.prologos=, =string-ops.prologos=
+- =racket/prologos/lib/prologos/data/= — =transducer.prologos=,
+  =map-entry.prologos=
+- =racket/prologos/lib/prologos/book/= — =collection-functions.prologos=,
+  =generic-operations.prologos=, =datum-and-homoiconicity.prologos=,
+  =persistent-vectors.prologos=, =sets.prologos=,
+  =characters-and-strings.prologos=, =maps.prologos=, =lattices.prologos=
+
+The =map-merge-with= and =map-lattice-leq= specs in =core/lattice.prologos=
+and =book/lattices.prologos= retain the explicit ={K V : Type}= because the
+=Map-K-V--Lattice= impl bodies pass =K V= as explicit type arguments to
+those functions.  Source-walk-order auto-detection (which sees =V= first in
+=[V V -> V]=) would silently flip the argument order at the call site;
+explicit binders pin it.  Documented in inline comments.
+
+** Tests
+
+Three new test cases in =tests/test-extended-spec.rkt=:
+
+- ="spec: D1+D2 combined — kind-Type and HKT both auto-introduced"= —
+  asserts the issue's target form produces =A=, =B= at kind =(Type 0)= and
+  =C= at kind =(-> (Type 0) (Type 0))=.
+- ="spec: bare form equals explicit form (D1+D2 idempotence)"= — asserts
+  =spec g-bare= and =spec g-explicit= produce identical implicit binders.
+- ="spec: D2 single-constraint metadata =:where= preserves list shape"= —
+  regression test for the WS-mode child-form merge bug.
+
+** Open follow-ups
+
+- The =Map K V= call-site argument-order subtlety hints at a deeper want:
+  let users opt into "auto-detect, ordered as I'd write them" without
+  spelling out kinds.  Possibly a sibling syntax (e.g. ={K V}= with no
+  kind) or a per-spec annotation (=:binder-order (K V)=).  Not pursued in
+  this pass.
+- Curried (=[A -> B -> C]=) vs uncurried (=[A B -> C]=) function-type style
+  is tracked separately; #20 explicitly leaves it out of scope.

docs/tracking/MASTER_ROADMAP.org

@@ -573,6 +573,7 @@ any Series.
 | PUnify Parts 1–2 | 2026-03-19 | [[file:2026-03-19_PUNIFY_STRUCTURAL_UNIFICATION_PROPAGATORS.org][P1 Design]], [[file:2026-03-19_PUNIFY_PART2_CELL_TREE_ARCHITECTURE.md][P2 Design]] | [[file:2026-03-19_PUNIFY_PARTS1_2_PIR.md][PIR]] | Cell-tree unification, descriptor registry, polymorphic solver dispatch. Breakout from Track 8 first half. |
 | BSP-LE Track 0 | 2026-03-21 | [[file:2026-03-21_BSP_LE_TRACK0_ALLOCATION_EFFICIENCY_DESIGN.md][Design]] | [[file:2026-03-21_BSP_LE_TRACK0_PIR.md][PIR]] | hot/warm/cold struct split, mutable worklist, batch API. GC eliminated on hot path; wall-time neutral. |
 | CHAMP Performance | 2026-03-21 | [[file:2026-03-21_CHAMP_PERFORMANCE_DESIGN.md][Design]] | [[file:2026-03-21_CHAMP_PERFORMANCE_PIR.md][PIR]] | Owner-ID transients (16× faster at N=2), eq?-first, value-only fast path. Track 0 Phase 5 rehabilitated. |
+| Improved Implicit Inference (#20) | 2026-04-30 | [[file:2026-02-22_IMPROVED_IMPLICIT_INFERENCE.org][Design]] | — | Direction 1 + 2 finalized: bare `A`/`B`/`C` auto-introduced; `:where`/inline trait constraints refine higher kinds; canonical kind-`Type`-first sort; stdlib refactor across 17 files. |
 
 * Standalone Design Documents (Not Yet Implemented / Future Scope)
 

racket/prologos/lib/prologos/book/characters-and-strings.prologos

@@ -365,13 +365,13 @@ defn pad-end [n c s]
 ;; ── Folding ──────────────────────────────────────
 
 ;; str-foldl : (A -> Char -> A) -> A -> String -> A
-spec str-foldl-loop {A : Type} [-> A [-> Char A]] -> A -> String -> Int -> Int -> A
+spec str-foldl-loop [-> A [-> Char A]] -> A -> String -> Int -> Int -> A
 defn str-foldl-loop [f acc s len i]
   if [int-eq i len]
     acc
     [str-foldl-loop f [f acc [str::ref s i]] s len [int+ i 1]]
 
-spec str-foldl {A : Type} [-> A [-> Char A]] -> A -> String -> A
+spec str-foldl [-> A [-> Char A]] -> A -> String -> A
 defn str-foldl [f z s]
   str-foldl-loop f z s [str::length s] 0
 

racket/prologos/lib/prologos/book/collection-functions.prologos

@@ -57,49 +57,49 @@ module prologos::core::collections :no-prelude
 ;; ── Transforming ops (Seqable + Buildable) ──────────
 
 ;; map : (A -> B) -> C A -> C B
-(spec map {A B : Type} {C : Type -> Type} (Seqable C) -> (Buildable C) -> (-> A B) -> (C A) -> (C B))
+(spec map (Seqable C) -> (Buildable C) -> (-> A B) -> (C A) -> (C B))
 (defn map [$seq $build f xs]
   (Buildable-from-seq $build B (lseq-map A B f ($seq A xs))))
 
 ;; filter : (A -> Bool) -> C A -> C A
-(spec filter {A : Type} {C : Type -> Type} (Seqable C) -> (Buildable C) -> (-> A Bool) -> (C A) -> (C A))
+(spec filter (Seqable C) -> (Buildable C) -> (-> A Bool) -> (C A) -> (C A))
 (defn filter [$seq $build pred xs]
   (Buildable-from-seq $build A (lseq-filter A pred ($seq A xs))))
 
 ;; concat : C A -> C A -> C A
-(spec concat {A : Type} {C : Type -> Type} (Seqable C) -> (Buildable C) -> (C A) -> (C A) -> (C A))
+(spec concat (Seqable C) -> (Buildable C) -> (C A) -> (C A) -> (C A))
 (defn concat [$seq $build xs ys]
   (Buildable-from-seq $build A (lseq-append A ($seq A xs) ($seq A ys))))
 
 ;; ── Reducing ops (Reducible — native left fold) ─────
 
 ;; reduce : (B -> A -> B) -> B -> C A -> B   [left fold, accumulator first]
 ;; Folds natively over the collection via Reducible — no LSeq intermediary.
-(spec reduce {A B : Type} {C : Type -> Type} (Reducible C) -> (-> B (-> A B)) -> B -> (C A) -> B)
+(spec reduce (Reducible C) -> (-> B (-> A B)) -> B -> (C A) -> B)
 (defn reduce [$red f z xs]
   ($red A B f z xs))
 
 ;; length : C A -> Nat
 ;; Counts elements via native left fold.
-(spec length {A : Type} {C : Type -> Type} (Reducible C) -> (C A) -> Nat)
+(spec length (Reducible C) -> (C A) -> Nat)
 (defn length [$red xs]
   ($red A Nat (fn (n : Nat) (fn (_ : A) (suc n))) zero xs))
 
 ;; any? : (A -> Bool) -> C A -> Bool
 ;; Note: does NOT short-circuit (processes all elements via fold).
-(spec any? {A : Type} {C : Type -> Type} (Reducible C) -> (-> A Bool) -> (C A) -> Bool)
+(spec any? (Reducible C) -> (-> A Bool) -> (C A) -> Bool)
 (defn any? [$red pred xs]
   ($red A Bool (fn (acc : Bool) (fn (a : A) (if (pred a) true acc))) false xs))
 
 ;; all? : (A -> Bool) -> C A -> Bool
 ;; Note: does NOT short-circuit (processes all elements via fold).
-(spec all? {A : Type} {C : Type -> Type} (Reducible C) -> (-> A Bool) -> (C A) -> Bool)
+(spec all? (Reducible C) -> (-> A Bool) -> (C A) -> Bool)
 (defn all? [$red pred xs]
   ($red A Bool (fn (acc : Bool) (fn (a : A) (if (pred a) acc false))) true xs))
 
 ;; find : (A -> Bool) -> C A -> Option A
 ;; Note: does NOT short-circuit (processes all elements via fold).
-(spec find {A : Type} {C : Type -> Type} (Reducible C) -> (-> A Bool) -> (C A) -> (Option A))
+(spec find (Reducible C) -> (-> A Bool) -> (C A) -> (Option A))
 (defn find [$red pred xs]
   ($red A (Option A)
     (fn (acc : (Option A)) (fn (a : A)
@@ -110,7 +110,7 @@ module prologos::core::collections :no-prelude
 
 ;; to-list : C A -> List A
 ;; Materialize any Seqable collection into a List.
-(spec to-list {A : Type} {C : Type -> Type} (Seqable C) -> (C A) -> (List A))
+(spec to-list (Seqable C) -> (C A) -> (List A))
 (defn to-list [$seq xs]
   (lseq-to-list ($seq A xs)))
 
@@ -120,19 +120,19 @@ module prologos::core::collections :no-prelude
 ;; Like Clojure's (reduce f coll): uses first element as accumulator.
 ;; Returns none for empty collections, some result for non-empty.
 ;; Stays on Seqable because it needs head access to extract the first element.
-(spec reduce1 {A : Type} {C : Type -> Type} (Seqable C) -> (-> A (-> A A)) -> (C A) -> (Option A))
+(spec reduce1 (Seqable C) -> (-> A (-> A A)) -> (C A) -> (Option A))
 (defn reduce1 [$seq f xs]
   (match ($seq A xs)
     (lseq-nil -> (none A))
     (lseq-cell a t -> (some A (lseq-fold A A f a (t unit))))))
 
 ;; take : Nat -> C A -> C A
-(spec take {A : Type} {C : Type -> Type} (Seqable C) -> (Buildable C) -> Nat -> (C A) -> (C A))
+(spec take (Seqable C) -> (Buildable C) -> Nat -> (C A) -> (C A))
 (defn take [$seq $build n xs]
   (Buildable-from-seq $build A (lseq-take A n ($seq A xs))))
 
 ;; drop : Nat -> C A -> C A
-(spec drop {A : Type} {C : Type -> Type} (Seqable C) -> (Buildable C) -> Nat -> (C A) -> (C A))
+(spec drop (Seqable C) -> (Buildable C) -> Nat -> (C A) -> (C A))
 (defn drop [$seq $build n xs]
   (Buildable-from-seq $build A (lseq-drop A n ($seq A xs))))
 
@@ -142,7 +142,7 @@ module prologos::core::collections :no-prelude
 ;; Usage: (into @[] '[1 2 3]) → @[1 2 3]
 ;;        (into #{} @[1 2 3]) → #{1 2 3}
 ;;        |> '[1 2 3] (into @[])   ;; in pipe context
-(spec into {A : Type} {S : Type -> Type} {T : Type -> Type} (Seqable S) -> (Buildable T) -> (T A) -> (S A) -> (T A))
+(spec into (Seqable S) -> (Buildable T) -> (T A) -> (S A) -> (T A))
 (defn into [$seq $build _target source]
   (Buildable-from-seq $build A ($seq A source)))
 
@@ -151,21 +151,21 @@ module prologos::core::collections :no-prelude
 ;; Converts to LSeq via Seqable, then extracts the head.
 ;; Note: named `head` not `first` because `first` is a parser keyword
 ;; (Sigma pair projection).
-(spec head {A : Type} {C : Type -> Type} (Seqable C) -> (C A) -> (Option A))
+(spec head (Seqable C) -> (C A) -> (Option A))
 (defn head [$seq xs]
   (lseq-head A ($seq A xs)))
 
 ;; empty? : C A -> Bool
 ;; Check if a collection is empty.
-(spec empty? {A : Type} {C : Type -> Type} (Seqable C) -> (C A) -> Bool)
+(spec empty? (Seqable C) -> (C A) -> Bool)
 (defn empty? [$seq xs]
   (lseq-empty? A ($seq A xs)))
 
 ;; rest-seq : C A -> LSeq A
 ;; Get the remaining elements as a lazy sequence.
 ;; The return type is always LSeq (not the original collection type)
 ;; since this streams the tail without materializing a new collection.
-(spec rest-seq {A : Type} {C : Type -> Type} (Seqable C) -> (C A) -> (LSeq A))
+(spec rest-seq (Seqable C) -> (C A) -> (LSeq A))
 (defn rest-seq [$seq xs]
   (lseq-rest A ($seq A xs)))
 
@@ -175,22 +175,22 @@ module prologos::core::collections :no-prelude
 ;; Demonstrates Seq-centric architecture with explicit List specialization.
 
 ;; coll-map : (A -> B) -> List A -> List B
-spec coll-map {A B : Type} [A -> B] -> [List A] -> [List B]
+spec coll-map [A -> B] -> [List A] -> [List B]
 defn coll-map [f xs]
   List--Buildable--from-seq B [lseq-map A B f [List--Seqable--dict A xs]]
 
 ;; coll-filter : (A -> Bool) -> List A -> List A
-spec coll-filter {A : Type} [A -> Bool] -> [List A] -> [List A]
+spec coll-filter [A -> Bool] -> [List A] -> [List A]
 defn coll-filter [pred xs]
   List--Buildable--from-seq A [lseq-filter A pred [List--Seqable--dict A xs]]
 
 ;; coll-length : List A -> Nat
-spec coll-length {A : Type} [List A] -> Nat
+spec coll-length [List A] -> Nat
 defn coll-length [xs]
   lseq-length A [List--Seqable--dict A xs]
 
 ;; coll-to-list : List A -> List A
-spec coll-to-list {A : Type} [List A] -> [List A]
+spec coll-to-list [List A] -> [List A]
 defn coll-to-list [xs]
   lseq-to-list A [List--Seqable--dict A xs]
 
@@ -203,42 +203,42 @@ defn coll-to-list [xs]
 ;; ── List → PVec ──────────
 
 ;; vec : List A -> PVec A
-spec vec {A : Type} [List A] -> [PVec A]
+spec vec [List A] -> [PVec A]
 defn vec [xs]
   pvec-from-list xs
 
 ;; ── Any → LSeq (lazy sequence) ──────────
 
 ;; list-to-seq : List A -> LSeq A
-spec list-to-seq {A : Type} [List A] -> [LSeq A]
+spec list-to-seq [List A] -> [LSeq A]
 defn list-to-seq [xs]
   list-to-lseq A xs
 
 ;; pvec-to-seq : PVec A -> LSeq A
-spec pvec-to-seq {A : Type} [PVec A] -> [LSeq A]
+spec pvec-to-seq [PVec A] -> [LSeq A]
 defn pvec-to-seq [v]
   list-to-lseq A [pvec-to-list v]
 
 ;; set-to-seq : Set A -> LSeq A
-spec set-to-seq {A : Type} [Set A] -> [LSeq A]
+spec set-to-seq [Set A] -> [LSeq A]
 defn set-to-seq [s]
   list-to-lseq A [set-to-list s]
 
 ;; ── LSeq → specific collections (into-*) ──────────
 
 ;; into-list : LSeq A -> List A
-spec into-list {A : Type} [LSeq A] -> [List A]
+spec into-list [LSeq A] -> [List A]
 defn into-list [xs]
   lseq-to-list A xs
 
 ;; into-vec : LSeq A -> PVec A
-spec into-vec {A : Type} [LSeq A] -> [PVec A]
+spec into-vec [LSeq A] -> [PVec A]
 defn into-vec [xs]
   pvec-from-list [lseq-to-list A xs]
 
 ;; into-set : LSeq A -> Set A
 ;; Folds the lazy sequence into a Set via set-insert.
 ;; (Can't call set-from-list due to :w/:0 multiplicity mismatch.)
-spec into-set {A : Type} [LSeq A] -> [Set A]
+spec into-set [LSeq A] -> [Set A]
 defn into-set [xs]
   foldr A [Set A] [fn a acc [set-insert acc a]] [set-empty A] [lseq-to-list A xs]