From 4dccebe11cb1aa12c283fb6ce9cdedea79dc8771 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Fri, 1 May 2026 02:44:35 +0000
Subject: [PATCH] spec: implement Direction 1 + 2 implicit binder
 auto-introduction (#20)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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

data: refresh test timings + propagator-cache + failure logs

Build artifacts from the issue #20 verification runs.  The failure logs
are all pre-existing infrastructure issues (`prologos/propagator` and
`rackcheck` collection imports unresolvable in this sandbox without the
`prologos` package installed and rackcheck wired in) — none are caused
by the spec / auto-introduction changes.

https://claude.ai/code/session_01UEKqhSHN5y9XEg88BkFnsW

data: drop stale + environment-only failure logs

The previous commit (a254cda) committed 17 failure logs that were a mix
of stale and resolvable:

- 9 logs referenced `/Users/avanti/dev/projects/prologos/...` paths
  (the user's local Mac tree), for tests that don't even exist in this
  repo — purely stale.
- 6 logs (test-attribute-record, test-facet-tag-dispatch,
  test-meta-feedback, test-ppn-track4, test-propagator-patterns,
  test-sre-coverage) failed with "collection not found: prologos/
  propagator" because the `prologos` collection wasn't linked in this
  sandbox. Fixed by `raco link --user --name prologos racket/prologos`;
  all 6 now pass (91 tests total).
- 2 logs (test-generators, test-properties) genuinely require the
  external `rackcheck` package, which can't be installed here because
  the package catalog (download.racket-lang.org/releases/9.0/catalog)
  returns 403 and github.com clones are blocked from this sandbox.
  These are not real failures of the codebase — only of the sandbox's
  network reachability — and they're orthogonal to issue #20.

Net change: drop all 17 stale logs.  The 2 rackcheck-blocked tests will
fail again on any machine without rackcheck installed; they're a known
external-dep gap, not introduced or affected by this branch.

https://claude.ai/code/session_01UEKqhSHN5y9XEg88BkFnsW

data: revert all benchmark/failures/ diffs to match main

Restore the 9 stale failure logs that were on main before this branch.
The previous two commits (a254cda, dbd42c9) churned this directory
unnecessarily; this commit makes the branch's net diff for
racket/prologos/data/benchmarks/failures/ empty against main.

https://claude.ai/code/session_01UEKqhSHN5y9XEg88BkFnsW

spec: address PR #43 review comments

1. kind-rank: rank ANY (Type n) as 0, not just (Type 0).  Forward-
   defensive against universe-level inference producing (Type 1+) for
   auto-introduced binders — those would previously have fallen to the
   "elaborate" rank and sorted after higher-kinded arrows.

2. Drop the racket/prologos/data/cache/pnet/prologos/data/nat.pnet diff.
   The file embeds an absolute build path + timestamp; the cache directory
   is already in .gitignore (the file is tracked from before the ignore
   rule).  The diff was pure path/timestamp churn with no semantic change.

https://claude.ai/code/session_01UEKqhSHN5y9XEg88BkFnsW
---
 .claude/rules/prologos-syntax.md              |  2 +-
 docs/spec/grammar.org                         | 54 ++++++++++--
 ...2026-02-22_IMPROVED_IMPLICIT_INFERENCE.org | 83 ++++++++++++++++++-
 docs/tracking/MASTER_ROADMAP.org              |  1 +
 .../book/characters-and-strings.prologos      |  4 +-
 .../book/collection-functions.prologos        | 54 ++++++------
 .../book/datum-and-homoiconicity.prologos     | 16 ++--
 .../prologos/book/generic-operations.prologos | 16 ++--
 .../lib/prologos/book/lattices.prologos       |  2 +-
 .../prologos/lib/prologos/book/maps.prologos  | 12 +--
 .../prologos/book/persistent-vectors.prologos |  8 +-
 .../prologos/lib/prologos/book/sets.prologos  | 10 +--
 .../lib/prologos/core/collections.prologos    | 60 +++++++-------
 .../prologos/lib/prologos/core/fio.prologos   |  2 +-
 .../lib/prologos/core/generic-ops.prologos    | 16 ++--
 .../lib/prologos/core/lattice.prologos        |  7 +-
 .../prologos/lib/prologos/core/map.prologos   |  8 +-
 .../prologos/lib/prologos/core/pvec.prologos  | 10 +--
 .../prologos/lib/prologos/core/set.prologos   | 10 +--
 .../lib/prologos/core/string-ops.prologos     |  4 +-
 .../lib/prologos/data/map-entry.prologos      |  4 +-
 .../lib/prologos/data/transducer.prologos     | 16 ++--
 racket/prologos/macros.rkt                    | 54 +++++++++++-
 racket/prologos/tests/test-extended-spec.rkt  | 72 ++++++++++++++++
 24 files changed, 390 insertions(+), 135 deletions(-)

diff --git a/.claude/rules/prologos-syntax.md b/.claude/rules/prologos-syntax.md
index c81adfa88..363646f73 100644
--- a/.claude/rules/prologos-syntax.md
+++ b/.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
 
diff --git a/docs/spec/grammar.org b/docs/spec/grammar.org
index 6b5c1b6fd..641213553 100644
--- a/docs/spec/grammar.org
+++ b/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
 
diff --git a/docs/tracking/2026-02-22_IMPROVED_IMPLICIT_INFERENCE.org b/docs/tracking/2026-02-22_IMPROVED_IMPLICIT_INFERENCE.org
index a2c61f9bb..5bbd9a7e4 100644
--- a/docs/tracking/2026-02-22_IMPROVED_IMPLICIT_INFERENCE.org
+++ b/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.
diff --git a/docs/tracking/MASTER_ROADMAP.org b/docs/tracking/MASTER_ROADMAP.org
index 6ee219b14..6932affa3 100644
--- a/docs/tracking/MASTER_ROADMAP.org
+++ b/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)
 
diff --git a/racket/prologos/lib/prologos/book/characters-and-strings.prologos b/racket/prologos/lib/prologos/book/characters-and-strings.prologos
index 5183765c1..cc9ffb231 100644
--- a/racket/prologos/lib/prologos/book/characters-and-strings.prologos
+++ b/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
 
diff --git a/racket/prologos/lib/prologos/book/collection-functions.prologos b/racket/prologos/lib/prologos/book/collection-functions.prologos
index 5176d5730..555fecdf5 100644
--- a/racket/prologos/lib/prologos/book/collection-functions.prologos
+++ b/racket/prologos/lib/prologos/book/collection-functions.prologos
@@ -57,17 +57,17 @@ 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))))
 
@@ -75,31 +75,31 @@ module prologos::core::collections :no-prelude
 
 ;; 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,13 +151,13 @@ 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)))
 
@@ -165,7 +165,7 @@ module prologos::core::collections :no-prelude
 ;; 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]
diff --git a/racket/prologos/lib/prologos/book/datum-and-homoiconicity.prologos b/racket/prologos/lib/prologos/book/datum-and-homoiconicity.prologos
index 4f0057e48..bb9598c68 100644
--- a/racket/prologos/lib/prologos/book/datum-and-homoiconicity.prologos
+++ b/racket/prologos/lib/prologos/book/datum-and-homoiconicity.prologos
@@ -187,19 +187,19 @@ require [prologos::data::lseq     :refer [LSeq lseq-nil lseq-cell lseq-head lseq
 ;; ── Transducer Constructors ────────────────────────
 
 ;; map-xf : transform each element through f before passing to reducer.
-spec map-xf {A B : Type} [A -> B] -> <(R :0 Type) -> [R -> B -> R] -> R -> A -> R>
+spec map-xf [A -> B] -> <(R :0 Type) -> [R -> B -> R] -> R -> A -> R>
 defn map-xf [f]
   fn [R :0 <Type>] [rf : <R -> B -> R>] [acc : <R>] [x : <A>]
     rf acc [f x]
 
 ;; filter-xf : only pass elements satisfying pred to the reducer.
-spec filter-xf {A : Type} [A -> Bool] -> <(R :0 Type) -> [R -> A -> R] -> R -> A -> R>
+spec filter-xf [A -> Bool] -> <(R :0 Type) -> [R -> A -> R] -> R -> A -> R>
 defn filter-xf [pred]
   fn [R :0 <Type>] [rf : <R -> A -> R>] [acc : <R>] [x : <A>]
     if [pred x] [rf acc x] acc
 
 ;; remove-xf : opposite of filter — remove elements satisfying pred.
-spec remove-xf {A : Type} [A -> Bool] -> <(R :0 Type) -> [R -> A -> R] -> R -> A -> R>
+spec remove-xf [A -> Bool] -> <(R :0 Type) -> [R -> A -> R] -> R -> A -> R>
 defn remove-xf [pred]
   fn [R :0 <Type>] [rf : <R -> A -> R>] [acc : <R>] [x : <A>]
     if [pred x] acc [rf acc x]
@@ -211,7 +211,7 @@ defn remove-xf [pred]
 ;;
 ;; In transducer algebra, composition is reversed from function composition:
 ;; xf1 transforms the input first, xf2 transforms the reducer wrapping.
-spec xf-compose {A B C : Type} <(S :0 Type) -> [S -> B -> S] -> S -> A -> S> <(S :0 Type) -> [S -> C -> S] -> S -> B -> S> -> <(S :0 Type) -> [S -> C -> S] -> S -> A -> S>
+spec xf-compose <(S :0 Type) -> [S -> B -> S] -> S -> A -> S> <(S :0 Type) -> [S -> C -> S] -> S -> B -> S> -> <(S :0 Type) -> [S -> C -> S] -> S -> A -> S>
 defn xf-compose [xf1 xf2]
   fn [R :0 <Type>] [rf : <R -> C -> R>]
     xf1 R [xf2 R rf]
@@ -220,7 +220,7 @@ defn xf-compose [xf1 xf2]
 
 ;; list-conj : a cons-to-front reducer for building lists.
 ;; Result is reversed since we fold left.
-spec list-conj {A : Type} [List A] -> A -> [List A]
+spec list-conj [List A] -> A -> [List A]
 defn list-conj [acc x]
   cons A x acc
 
@@ -229,14 +229,14 @@ defn list-conj [acc x]
 ;; transduce : apply a polymorphic transducer xf to list xs,
 ;; using reducer rf and initial accumulator init.
 ;; The xf is polymorphic in R — transduce specializes it internally.
-spec transduce {A B R : Type} <(S :0 Type) -> [S -> B -> S] -> S -> A -> S> [R -> B -> R] R [List A] -> R
+spec transduce <(S :0 Type) -> [S -> B -> S] -> S -> A -> S> [R -> B -> R] R [List A] -> R
 defn transduce [xf rf init xs]
   lseq-fold R A [xf R rf] init [list-to-lseq A xs]
 
 ;; xf-into-list-rev : transduce into a reversed list (fold-left with cons).
 ;; The xf is polymorphic in R — xf-into-list-rev specializes it to (List B).
 ;; Renamed from into-list-rev to avoid collision with prologos::core::collections::into-list.
-spec xf-into-list-rev {A B : Type} <(S :0 Type) -> [S -> B -> S] -> S -> A -> S> [List A] -> [List B]
+spec xf-into-list-rev <(S :0 Type) -> [S -> B -> S] -> S -> A -> S> [List A] -> [List B]
 defn xf-into-list-rev [xf xs]
   lseq-fold [List B] A [xf [List B] [list-conj B]] [nil B] [list-to-lseq A xs]
 
@@ -244,6 +244,6 @@ defn xf-into-list-rev [xf xs]
 ;; Uses xf-into-list-rev then reverses for correct element order.
 ;; One extra O(n) reverse, but fusion saves N-1 intermediate list allocations.
 ;; Renamed from into-list to avoid collision with prologos::core::collections::into-list.
-spec xf-into-list {A B : Type} <(S :0 Type) -> [S -> B -> S] -> S -> A -> S> [List A] -> [List B]
+spec xf-into-list <(S :0 Type) -> [S -> B -> S] -> S -> A -> S> [List A] -> [List B]
 defn xf-into-list [xf xs]
   reverse B [xf-into-list-rev xf xs]
diff --git a/racket/prologos/lib/prologos/book/generic-operations.prologos b/racket/prologos/lib/prologos/book/generic-operations.prologos
index c91212b8d..56ca4549d 100644
--- a/racket/prologos/lib/prologos/book/generic-operations.prologos
+++ b/racket/prologos/lib/prologos/book/generic-operations.prologos
@@ -50,42 +50,42 @@ require [prologos::data::option           :refer [Option some none some? unwrap-
 ;; since it comes after the dict param (not a leading m0 position).
 
 ;; gmap : (A -> B) -> C A -> C B
-spec gmap {A B : Type} {C : Type -> Type} [Seqable C] -> [Buildable C] -> [A -> B] -> [C A] -> [C B]
+spec gmap [Seqable C] -> [Buildable C] -> [A -> B] -> [C A] -> [C B]
 defn gmap [$seq $build f xs]
   Buildable-from-seq $build B [lseq-map A B f [$seq A xs]]
 
 ;; gfilter : (A -> Bool) -> C A -> C A
-spec gfilter {A : Type} {C : Type -> Type} [Seqable C] -> [Buildable C] -> [A -> Bool] -> [C A] -> [C A]
+spec gfilter [Seqable C] -> [Buildable C] -> [A -> Bool] -> [C A] -> [C A]
 defn gfilter [$seq $build pred xs]
   Buildable-from-seq $build A [lseq-filter A pred [$seq A xs]]
 
 ;; gfold : (A -> B -> B) -> B -> C A -> B
-spec gfold {A B : Type} {C : Type -> Type} [Foldable C] -> [A -> B -> B] -> B -> [C A] -> B
+spec gfold [Foldable C] -> [A -> B -> B] -> B -> [C A] -> B
 defn gfold [$foldable f z xs]
   $foldable A B f z xs
 
 ;; glength : C A -> Nat
-spec glength {A : Type} {C : Type -> Type} [Seqable C] -> [C A] -> Nat
+spec glength [Seqable C] -> [C A] -> Nat
 defn glength [$seq xs]
   lseq-length [$seq A xs]
 
 ;; gconcat : C A -> C A -> C A
-spec gconcat {A : Type} {C : Type -> Type} [Seqable C] -> [Buildable C] -> [C A] -> [C A] -> [C A]
+spec gconcat [Seqable C] -> [Buildable C] -> [C A] -> [C A] -> [C A]
 defn gconcat [$seq $build xs ys]
   Buildable-from-seq $build A [lseq-append A [$seq A xs] [$seq A ys]]
 
 ;; gany? : (A -> Bool) -> C A -> Bool
-spec gany? {A : Type} {C : Type -> Type} [Foldable C] -> [A -> Bool] -> [C A] -> Bool
+spec gany? [Foldable C] -> [A -> Bool] -> [C A] -> Bool
 defn gany? [$foldable pred xs]
   $foldable A Bool (fn [a] [acc] (if [pred a] true acc)) false xs
 
 ;; gall? : (A -> Bool) -> C A -> Bool
-spec gall? {A : Type} {C : Type -> Type} [Foldable C] -> [A -> Bool] -> [C A] -> Bool
+spec gall? [Foldable C] -> [A -> Bool] -> [C A] -> Bool
 defn gall? [$foldable pred xs]
   $foldable A Bool (fn [a] [acc] (if [pred a] acc false)) true xs
 
 ;; gto-list : C A -> List A
-spec gto-list {A : Type} {C : Type -> Type} [Seqable C] -> [C A] -> [List A]
+spec gto-list [Seqable C] -> [C A] -> [List A]
 defn gto-list [$seq xs]
   lseq-to-list [$seq A xs]
 
diff --git a/racket/prologos/lib/prologos/book/lattices.prologos b/racket/prologos/lib/prologos/book/lattices.prologos
index b664f52fe..f858ccbb0 100644
--- a/racket/prologos/lib/prologos/book/lattices.prologos
+++ b/racket/prologos/lib/prologos/book/lattices.prologos
@@ -153,7 +153,7 @@ defn rat-min [a b]
 
 ;; --- Set helpers ---
 
-spec set-subset? {A : Type} [Set A] [Set A] -> Bool
+spec set-subset? [Set A] [Set A] -> Bool
 defn set-subset? [a b]
   set-fold [fn acc x [and acc [set-member? b x]]] true a
 
diff --git a/racket/prologos/lib/prologos/book/maps.prologos b/racket/prologos/lib/prologos/book/maps.prologos
index d22fd7d3e..586121127 100644
--- a/racket/prologos/lib/prologos/book/maps.prologos
+++ b/racket/prologos/lib/prologos/book/maps.prologos
@@ -55,13 +55,13 @@ data MapEntry {K V}
   mk-entry : K -> V
 
 ;; Extract the key from a MapEntry.
-spec entry-key {K V : Type} [MapEntry K V] -> K
+spec entry-key [MapEntry K V] -> K
 defn entry-key [e]
   match e
     | mk-entry k _ -> k
 
 ;; Extract the value from a MapEntry.
-spec entry-val {K V : Type} [MapEntry K V] -> V
+spec entry-val [MapEntry K V] -> V
 defn entry-val [e]
   match e
     | mk-entry _ v -> v
@@ -119,24 +119,24 @@ require [prologos::data::lseq-ops    :refer [list-to-lseq lseq-to-list]]
 ;; map-filter-vals : (V -> Bool) -> Map K V -> Map K V
 ;; Keeps only entries whose value satisfies pred.
 ;; Uses native map-filter-entries with a key-ignoring predicate.
-spec map-filter-vals {K V : Type} [-> V Bool] -> [Map K V] -> [Map K V]
+spec map-filter-vals [-> V Bool] -> [Map K V] -> [Map K V]
 defn map-filter-vals [pred m]
   map-filter-entries [fn k v [pred v]] m
 
 ;; map-keys-list : Map K V -> List K  (wraps AST map-keys as a function)
-spec map-keys-list {K V : Type} [Map K V] -> [List K]
+spec map-keys-list [Map K V] -> [List K]
 defn map-keys-list [m]
   map-keys m
 
 ;; map-vals-list : Map K V -> List V  (wraps AST map-vals as a function)
-spec map-vals-list {K V : Type} [Map K V] -> [List V]
+spec map-vals-list [Map K V] -> [List V]
 defn map-vals-list [m]
   map-vals m
 
 ;; map-merge : Map K V -> Map K V -> Map K V
 ;; Merge two maps. Right map wins on key collision.
 ;; Uses native map-fold-entries to fold over m2's entries.
-spec map-merge {K V : Type} [Map K V] -> [Map K V] -> [Map K V]
+spec map-merge [Map K V] -> [Map K V] -> [Map K V]
 defn map-merge [m1 m2]
   map-fold-entries [fn acc k v [map-assoc acc k v]] m1 m2
 
diff --git a/racket/prologos/lib/prologos/book/persistent-vectors.prologos b/racket/prologos/lib/prologos/book/persistent-vectors.prologos
index 73c10abc4..5b6590e05 100644
--- a/racket/prologos/lib/prologos/book/persistent-vectors.prologos
+++ b/racket/prologos/lib/prologos/book/persistent-vectors.prologos
@@ -140,21 +140,21 @@ require [prologos::data::nat            :refer [lt?]]
 ;; pvec-any? and pvec-all? use native pvec-fold.
 
 ;; pvec-any? : (A -> Bool) -> PVec A -> Bool
-spec pvec-any? {A : Type} [-> A Bool] -> [PVec A] -> Bool
+spec pvec-any? [-> A Bool] -> [PVec A] -> Bool
 defn pvec-any? [pred v]
   pvec-fold [fn acc x [if [pred x] true acc]] false v
 
 ;; pvec-all? : (A -> Bool) -> PVec A -> Bool
-spec pvec-all? {A : Type} [-> A Bool] -> [PVec A] -> Bool
+spec pvec-all? [-> A Bool] -> [PVec A] -> Bool
 defn pvec-all? [pred v]
   pvec-fold [fn acc x [if [pred x] acc false]] true v
 
 ;; pvec-from-list-fn : List A -> PVec A  (wraps AST pvec-from-list as a function)
-spec pvec-from-list-fn {A : Type} [List A] -> [PVec A]
+spec pvec-from-list-fn [List A] -> [PVec A]
 defn pvec-from-list-fn [xs]
   pvec-from-list xs
 
 ;; pvec-to-list-fn : PVec A -> List A  (wraps AST pvec-to-list as a function)
-spec pvec-to-list-fn {A : Type} [PVec A] -> [List A]
+spec pvec-to-list-fn [PVec A] -> [List A]
 defn pvec-to-list-fn [v]
   pvec-to-list v
diff --git a/racket/prologos/lib/prologos/book/sets.prologos b/racket/prologos/lib/prologos/book/sets.prologos
index 218ef466e..6f591ee01 100644
--- a/racket/prologos/lib/prologos/book/sets.prologos
+++ b/racket/prologos/lib/prologos/book/sets.prologos
@@ -174,28 +174,28 @@ require [prologos::data::list             :refer [List nil cons foldr]]
 ;; set-map : (A -> B) -> Set A -> Set B
 ;; Applies f to every element, collecting results into a new set.
 ;; Uses native set-fold to avoid List conversion.
-spec set-map {A B : Type} [-> A B] -> [Set A] -> [Set B]
+spec set-map [-> A B] -> [Set A] -> [Set B]
 defn set-map [f s]
   set-fold [fn acc x [set-insert acc [f x]]] [set-empty B] s
 
 ;; set-any? : (A -> Bool) -> Set A -> Bool
-spec set-any? {A : Type} [-> A Bool] -> [Set A] -> Bool
+spec set-any? [-> A Bool] -> [Set A] -> Bool
 defn set-any? [pred s]
   set-fold [fn acc x [if [pred x] true acc]] false s
 
 ;; set-all? : (A -> Bool) -> Set A -> Bool
-spec set-all? {A : Type} [-> A Bool] -> [Set A] -> Bool
+spec set-all? [-> A Bool] -> [Set A] -> Bool
 defn set-all? [pred s]
   set-fold [fn acc x [if [pred x] acc false]] true s
 
 ;; set-to-list-fn : Set A -> List A  (wraps AST set-to-list as a function)
-spec set-to-list-fn {A : Type} [Set A] -> [List A]
+spec set-to-list-fn [Set A] -> [List A]
 defn set-to-list-fn [s]
   set-to-list s
 
 ;; set-from-list-fn : List A -> Set A  (wraps via fold, erased type arg)
 ;; Note: We avoid calling set-from-list directly because it declares A :w,
 ;; but spec/defn generates A :0 (erased). Instead we fold with set-insert.
-spec set-from-list-fn {A : Type} [List A] -> [Set A]
+spec set-from-list-fn [List A] -> [Set A]
 defn set-from-list-fn [xs]
   foldr A [Set A] [fn a acc [set-insert acc a]] [set-empty A] xs
diff --git a/racket/prologos/lib/prologos/core/collections.prologos b/racket/prologos/lib/prologos/core/collections.prologos
index 2a52fb50b..05dc8c468 100644
--- a/racket/prologos/lib/prologos/core/collections.prologos
+++ b/racket/prologos/lib/prologos/core/collections.prologos
@@ -30,17 +30,17 @@
 ;; ── 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))))
 
@@ -48,31 +48,31 @@
 
 ;; 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)
@@ -83,7 +83,7 @@
 
 ;; 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)))
 
@@ -93,19 +93,19 @@
 ;; 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))))
 
@@ -115,7 +115,7 @@
 ;; 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)))
 
@@ -123,13 +123,13 @@
 ;; Get the first element of any collection, or none if empty.
 ;; Converts to LSeq via Seqable, then extracts the head.
 ;; Alias: `first` (identical behavior).
-(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)))
 
@@ -137,7 +137,7 @@
 ;; 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)))
 
@@ -146,13 +146,13 @@
 ;; first : C A -> Option A
 ;; Get the first element of any Seqable collection, or none if empty.
 ;; Identical to `head` — exists for ergonomic naming alongside `second`/`rest`.
-(spec first {A : Type} {C : Type -> Type} (Seqable C) -> (C A) -> (Option A))
+(spec first (Seqable C) -> (C A) -> (Option A))
 (defn first [$seq xs]
   (lseq-head A ($seq A xs)))
 
 ;; second : C A -> Option A
 ;; Get the second element of any Seqable collection, or none if fewer than 2.
-(spec second {A : Type} {C : Type -> Type} (Seqable C) -> (C A) -> (Option A))
+(spec second (Seqable C) -> (C A) -> (Option A))
 (defn second [$seq xs]
   (match ($seq A xs)
     (lseq-nil -> (none A))
@@ -161,7 +161,7 @@
 ;; rest : C A -> C A
 ;; All elements after the first, preserving the collection type.
 ;; Returns empty for empty collections.
-(spec rest {A : Type} {C : Type -> Type} (Seqable C) -> (Buildable C) -> (C A) -> (C A))
+(spec rest (Seqable C) -> (Buildable C) -> (C A) -> (C A))
 (defn rest [$seq $build xs]
   (Buildable-from-seq $build A (lseq-rest A ($seq A xs))))
 
@@ -171,22 +171,22 @@
 ;; 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]
 
@@ -199,42 +199,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]
diff --git a/racket/prologos/lib/prologos/core/fio.prologos b/racket/prologos/lib/prologos/core/fio.prologos
index d7388f8a7..a7db90827 100644
--- a/racket/prologos/lib/prologos/core/fio.prologos
+++ b/racket/prologos/lib/prologos/core/fio.prologos
@@ -73,7 +73,7 @@ defn fio-close [h]
 ;;
 ;; Not linear (-1>) because it doesn't take a linear param — it creates
 ;; and manages the handle internally.
-spec fio-with-file {A : Type} String -> String -> <Handle -> <Handle * A>> -> A
+spec fio-with-file String -> String -> <Handle -> <Handle * A>> -> A
 defn fio-with-file [path mode body]
   let p := [body [fio-open path mode]]
     match [fio-close [fst p]] (unit -> [snd p])
diff --git a/racket/prologos/lib/prologos/core/generic-ops.prologos b/racket/prologos/lib/prologos/core/generic-ops.prologos
index d7955be04..aeabed5ec 100644
--- a/racket/prologos/lib/prologos/core/generic-ops.prologos
+++ b/racket/prologos/lib/prologos/core/generic-ops.prologos
@@ -28,42 +28,42 @@ require [prologos::data::option           :refer [Option some none some? unwrap-
 ;; since it comes after the dict param (not a leading m0 position).
 
 ;; gmap : (A -> B) -> C A -> C B
-spec gmap {A B : Type} {C : Type -> Type} [Seqable C] -> [Buildable C] -> [A -> B] -> [C A] -> [C B]
+spec gmap [Seqable C] -> [Buildable C] -> [A -> B] -> [C A] -> [C B]
 defn gmap [$seq $build f xs]
   Buildable-from-seq $build B [lseq-map A B f [$seq A xs]]
 
 ;; gfilter : (A -> Bool) -> C A -> C A
-spec gfilter {A : Type} {C : Type -> Type} [Seqable C] -> [Buildable C] -> [A -> Bool] -> [C A] -> [C A]
+spec gfilter [Seqable C] -> [Buildable C] -> [A -> Bool] -> [C A] -> [C A]
 defn gfilter [$seq $build pred xs]
   Buildable-from-seq $build A [lseq-filter A pred [$seq A xs]]
 
 ;; gfold : (A -> B -> B) -> B -> C A -> B
-spec gfold {A B : Type} {C : Type -> Type} [Foldable C] -> [A -> B -> B] -> B -> [C A] -> B
+spec gfold [Foldable C] -> [A -> B -> B] -> B -> [C A] -> B
 defn gfold [$foldable f z xs]
   $foldable A B f z xs
 
 ;; glength : C A -> Nat
-spec glength {A : Type} {C : Type -> Type} [Seqable C] -> [C A] -> Nat
+spec glength [Seqable C] -> [C A] -> Nat
 defn glength [$seq xs]
   lseq-length [$seq A xs]
 
 ;; gconcat : C A -> C A -> C A
-spec gconcat {A : Type} {C : Type -> Type} [Seqable C] -> [Buildable C] -> [C A] -> [C A] -> [C A]
+spec gconcat [Seqable C] -> [Buildable C] -> [C A] -> [C A] -> [C A]
 defn gconcat [$seq $build xs ys]
   Buildable-from-seq $build A [lseq-append A [$seq A xs] [$seq A ys]]
 
 ;; gany? : (A -> Bool) -> C A -> Bool
-spec gany? {A : Type} {C : Type -> Type} [Foldable C] -> [A -> Bool] -> [C A] -> Bool
+spec gany? [Foldable C] -> [A -> Bool] -> [C A] -> Bool
 defn gany? [$foldable pred xs]
   $foldable A Bool (fn [a] [acc] (if [pred a] true acc)) false xs
 
 ;; gall? : (A -> Bool) -> C A -> Bool
-spec gall? {A : Type} {C : Type -> Type} [Foldable C] -> [A -> Bool] -> [C A] -> Bool
+spec gall? [Foldable C] -> [A -> Bool] -> [C A] -> Bool
 defn gall? [$foldable pred xs]
   $foldable A Bool (fn [a] [acc] (if [pred a] acc false)) true xs
 
 ;; gto-list : C A -> List A
-spec gto-list {A : Type} {C : Type -> Type} [Seqable C] -> [C A] -> [List A]
+spec gto-list [Seqable C] -> [C A] -> [List A]
 defn gto-list [$seq xs]
   lseq-to-list [$seq A xs]
 
diff --git a/racket/prologos/lib/prologos/core/lattice.prologos b/racket/prologos/lib/prologos/core/lattice.prologos
index ff62cce00..2c4837b12 100644
--- a/racket/prologos/lib/prologos/core/lattice.prologos
+++ b/racket/prologos/lib/prologos/core/lattice.prologos
@@ -119,12 +119,16 @@ defn rat-min [a b]
 
 ;; --- Set helpers ---
 
-spec set-subset? {A : Type} [Set A] [Set A] -> Bool
+spec set-subset? [Set A] [Set A] -> Bool
 defn set-subset? [a b]
   set-fold [fn acc x [and acc [set-member? b x]]] true a
 
 ;; --- Map helpers ---
 
+;; Note: explicit `{K V : Type}` retained because the body of `Map-K-V--Lattice`
+;; calls this function with explicit `K V` type args.  Without an explicit binder
+;; declaration, auto-introduction would order vars by source-walk (V before K),
+;; which silently flips the call-site type args.
 spec map-merge-with {K V : Type} [V V -> V] [Map K V] [Map K V] -> [Map K V]
 defn map-merge-with [join-fn m1 m2]
   map-fold-entries
@@ -135,6 +139,7 @@ defn map-merge-with [join-fn m1 m2]
     m1
     m2
 
+;; Note: explicit `{K V : Type}` retained for the same reason as map-merge-with.
 spec map-lattice-leq {K V : Type} [V V -> Bool] [Map K V] [Map K V] -> Bool
 defn map-lattice-leq [leq-fn m1 m2]
   map-fold-entries
diff --git a/racket/prologos/lib/prologos/core/map.prologos b/racket/prologos/lib/prologos/core/map.prologos
index a96f10fdb..7988f81e9 100644
--- a/racket/prologos/lib/prologos/core/map.prologos
+++ b/racket/prologos/lib/prologos/core/map.prologos
@@ -45,24 +45,24 @@ require [prologos::data::lseq-ops    :refer [list-to-lseq lseq-to-list]]
 ;; map-filter-vals : (V -> Bool) -> Map K V -> Map K V
 ;; Keeps only entries whose value satisfies pred.
 ;; Uses native map-filter-entries with a key-ignoring predicate.
-spec map-filter-vals {K V : Type} [-> V Bool] -> [Map K V] -> [Map K V]
+spec map-filter-vals [-> V Bool] -> [Map K V] -> [Map K V]
 defn map-filter-vals [pred m]
   map-filter-entries [fn k v [pred v]] m
 
 ;; map-keys-list : Map K V -> List K  (wraps AST map-keys as a function)
-spec map-keys-list {K V : Type} [Map K V] -> [List K]
+spec map-keys-list [Map K V] -> [List K]
 defn map-keys-list [m]
   map-keys m
 
 ;; map-vals-list : Map K V -> List V  (wraps AST map-vals as a function)
-spec map-vals-list {K V : Type} [Map K V] -> [List V]
+spec map-vals-list [Map K V] -> [List V]
 defn map-vals-list [m]
   map-vals m
 
 ;; map-merge : Map K V -> Map K V -> Map K V
 ;; Merge two maps. Right map wins on key collision.
 ;; Uses native map-fold-entries to fold over m2's entries.
-spec map-merge {K V : Type} [Map K V] -> [Map K V] -> [Map K V]
+spec map-merge [Map K V] -> [Map K V] -> [Map K V]
 defn map-merge [m1 m2]
   map-fold-entries [fn acc k v [map-assoc acc k v]] m1 m2
 
diff --git a/racket/prologos/lib/prologos/core/pvec.prologos b/racket/prologos/lib/prologos/core/pvec.prologos
index 2daa22cbc..e5377886f 100644
--- a/racket/prologos/lib/prologos/core/pvec.prologos
+++ b/racket/prologos/lib/prologos/core/pvec.prologos
@@ -116,22 +116,22 @@ require [prologos::data::nat            :refer [lt?]]
 ;; pvec-any? and pvec-all? use native pvec-fold.
 
 ;; pvec-any? : (A -> Bool) -> PVec A -> Bool
-spec pvec-any? {A : Type} [-> A Bool] -> [PVec A] -> Bool
+spec pvec-any? [-> A Bool] -> [PVec A] -> Bool
 defn pvec-any? [pred v]
   pvec-fold [fn acc x [if [pred x] true acc]] false v
 
 ;; pvec-all? : (A -> Bool) -> PVec A -> Bool
-spec pvec-all? {A : Type} [-> A Bool] -> [PVec A] -> Bool
+spec pvec-all? [-> A Bool] -> [PVec A] -> Bool
 defn pvec-all? [pred v]
   pvec-fold [fn acc x [if [pred x] acc false]] true v
 
 ;; pvec-from-list-fn : List A -> PVec A  (wraps AST pvec-from-list as a function)
-spec pvec-from-list-fn {A : Type} [List A] -> [PVec A]
+spec pvec-from-list-fn [List A] -> [PVec A]
 defn pvec-from-list-fn [xs]
   pvec-from-list xs
 
 ;; pvec-to-list-fn : PVec A -> List A  (wraps AST pvec-to-list as a function)
-spec pvec-to-list-fn {A : Type} [PVec A] -> [List A]
+spec pvec-to-list-fn [PVec A] -> [List A]
 defn pvec-to-list-fn [v]
   pvec-to-list v
 
@@ -142,7 +142,7 @@ defn pvec-to-list-fn [v]
 ;; Implementation: convert both pvecs to lists, zip-with on lists, convert
 ;; the result back to a PVec. The asymptotic cost is the same as a direct
 ;; index walk: O(n) for the dominant length.
-spec pvec-zip-with {A B C : Type} [A -> B -> C] [PVec A] [PVec B] -> [PVec C]
+spec pvec-zip-with [A -> B -> C] [PVec A] [PVec B] -> [PVec C]
   :doc "Combine two PVecs element-wise with a function; truncates to shorter."
 defn pvec-zip-with [f xs ys]
   pvec-from-list [zip-with f [pvec-to-list xs] [pvec-to-list ys]]
diff --git a/racket/prologos/lib/prologos/core/set.prologos b/racket/prologos/lib/prologos/core/set.prologos
index 9fc0a9879..113f5a2c8 100644
--- a/racket/prologos/lib/prologos/core/set.prologos
+++ b/racket/prologos/lib/prologos/core/set.prologos
@@ -102,28 +102,28 @@ require [prologos::data::list             :refer [List nil cons foldr]]
 ;; set-map : (A -> B) -> Set A -> Set B
 ;; Applies f to every element, collecting results into a new set.
 ;; Uses native set-fold to avoid List conversion.
-spec set-map {A B : Type} [-> A B] -> [Set A] -> [Set B]
+spec set-map [-> A B] -> [Set A] -> [Set B]
 defn set-map [f s]
   set-fold [fn acc x [set-insert acc [f x]]] [set-empty B] s
 
 ;; set-any? : (A -> Bool) -> Set A -> Bool
-spec set-any? {A : Type} [-> A Bool] -> [Set A] -> Bool
+spec set-any? [-> A Bool] -> [Set A] -> Bool
 defn set-any? [pred s]
   set-fold [fn acc x [if [pred x] true acc]] false s
 
 ;; set-all? : (A -> Bool) -> Set A -> Bool
-spec set-all? {A : Type} [-> A Bool] -> [Set A] -> Bool
+spec set-all? [-> A Bool] -> [Set A] -> Bool
 defn set-all? [pred s]
   set-fold [fn acc x [if [pred x] acc false]] true s
 
 ;; set-to-list-fn : Set A -> List A  (wraps AST set-to-list as a function)
-spec set-to-list-fn {A : Type} [Set A] -> [List A]
+spec set-to-list-fn [Set A] -> [List A]
 defn set-to-list-fn [s]
   set-to-list s
 
 ;; set-from-list-fn : List A -> Set A  (wraps via fold, erased type arg)
 ;; Note: We avoid calling set-from-list directly because it declares A :w,
 ;; but spec/defn generates A :0 (erased). Instead we fold with set-insert.
-spec set-from-list-fn {A : Type} [List A] -> [Set A]
+spec set-from-list-fn [List A] -> [Set A]
 defn set-from-list-fn [xs]
   foldr A [Set A] [fn a acc [set-insert acc a]] [set-empty A] xs
diff --git a/racket/prologos/lib/prologos/core/string-ops.prologos b/racket/prologos/lib/prologos/core/string-ops.prologos
index 85db2732c..a81b0b7fd 100644
--- a/racket/prologos/lib/prologos/core/string-ops.prologos
+++ b/racket/prologos/lib/prologos/core/string-ops.prologos
@@ -278,13 +278,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
 
diff --git a/racket/prologos/lib/prologos/data/map-entry.prologos b/racket/prologos/lib/prologos/data/map-entry.prologos
index 2cb7fc266..d1ddcdbe8 100644
--- a/racket/prologos/lib/prologos/data/map-entry.prologos
+++ b/racket/prologos/lib/prologos/data/map-entry.prologos
@@ -20,13 +20,13 @@ data MapEntry {K V}
   mk-entry : K -> V
 
 ;; Extract the key from a MapEntry.
-spec entry-key {K V : Type} [MapEntry K V] -> K
+spec entry-key [MapEntry K V] -> K
 defn entry-key [e]
   match e
     | mk-entry k _ -> k
 
 ;; Extract the value from a MapEntry.
-spec entry-val {K V : Type} [MapEntry K V] -> V
+spec entry-val [MapEntry K V] -> V
 defn entry-val [e]
   match e
     | mk-entry _ v -> v
diff --git a/racket/prologos/lib/prologos/data/transducer.prologos b/racket/prologos/lib/prologos/data/transducer.prologos
index 4cab24bb1..f8174c075 100644
--- a/racket/prologos/lib/prologos/data/transducer.prologos
+++ b/racket/prologos/lib/prologos/data/transducer.prologos
@@ -28,19 +28,19 @@ require [prologos::data::lseq     :refer [LSeq lseq-nil lseq-cell lseq-head lseq
 ;; ----------------------------------------
 
 ;; map-xf : transform each element through f before passing to reducer.
-spec map-xf {A B : Type} [A -> B] -> <(R :0 Type) -> [R -> B -> R] -> R -> A -> R>
+spec map-xf [A -> B] -> <(R :0 Type) -> [R -> B -> R] -> R -> A -> R>
 defn map-xf [f]
   fn [R :0 <Type>] [rf : <R -> B -> R>] [acc : <R>] [x : <A>]
     rf acc [f x]
 
 ;; filter-xf : only pass elements satisfying pred to the reducer.
-spec filter-xf {A : Type} [A -> Bool] -> <(R :0 Type) -> [R -> A -> R] -> R -> A -> R>
+spec filter-xf [A -> Bool] -> <(R :0 Type) -> [R -> A -> R] -> R -> A -> R>
 defn filter-xf [pred]
   fn [R :0 <Type>] [rf : <R -> A -> R>] [acc : <R>] [x : <A>]
     if [pred x] [rf acc x] acc
 
 ;; remove-xf : opposite of filter — remove elements satisfying pred.
-spec remove-xf {A : Type} [A -> Bool] -> <(R :0 Type) -> [R -> A -> R] -> R -> A -> R>
+spec remove-xf [A -> Bool] -> <(R :0 Type) -> [R -> A -> R] -> R -> A -> R>
 defn remove-xf [pred]
   fn [R :0 <Type>] [rf : <R -> A -> R>] [acc : <R>] [x : <A>]
     if [pred x] acc [rf acc x]
@@ -54,7 +54,7 @@ defn remove-xf [pred]
 ;;
 ;; In transducer algebra, composition is reversed from function composition:
 ;; xf1 transforms the input first, xf2 transforms the reducer wrapping.
-spec xf-compose {A B C : Type} <(S :0 Type) -> [S -> B -> S] -> S -> A -> S> <(S :0 Type) -> [S -> C -> S] -> S -> B -> S> -> <(S :0 Type) -> [S -> C -> S] -> S -> A -> S>
+spec xf-compose <(S :0 Type) -> [S -> B -> S] -> S -> A -> S> <(S :0 Type) -> [S -> C -> S] -> S -> B -> S> -> <(S :0 Type) -> [S -> C -> S] -> S -> A -> S>
 defn xf-compose [xf1 xf2]
   fn [R :0 <Type>] [rf : <R -> C -> R>]
     xf1 R [xf2 R rf]
@@ -65,7 +65,7 @@ defn xf-compose [xf1 xf2]
 
 ;; list-conj : a cons-to-front reducer for building lists.
 ;; Result is reversed since we fold left.
-spec list-conj {A : Type} [List A] -> A -> [List A]
+spec list-conj [List A] -> A -> [List A]
 defn list-conj [acc x]
   cons A x acc
 
@@ -76,14 +76,14 @@ defn list-conj [acc x]
 ;; transduce : apply a polymorphic transducer xf to list xs,
 ;; using reducer rf and initial accumulator init.
 ;; The xf is polymorphic in R — transduce specializes it internally.
-spec transduce {A B R : Type} <(S :0 Type) -> [S -> B -> S] -> S -> A -> S> [R -> B -> R] R [List A] -> R
+spec transduce <(S :0 Type) -> [S -> B -> S] -> S -> A -> S> [R -> B -> R] R [List A] -> R
 defn transduce [xf rf init xs]
   lseq-fold R A [xf R rf] init [list-to-lseq A xs]
 
 ;; xf-into-list-rev : transduce into a reversed list (fold-left with cons).
 ;; The xf is polymorphic in R — xf-into-list-rev specializes it to (List B).
 ;; Renamed from into-list-rev to avoid collision with prologos::core::collections::into-list.
-spec xf-into-list-rev {A B : Type} <(S :0 Type) -> [S -> B -> S] -> S -> A -> S> [List A] -> [List B]
+spec xf-into-list-rev <(S :0 Type) -> [S -> B -> S] -> S -> A -> S> [List A] -> [List B]
 defn xf-into-list-rev [xf xs]
   lseq-fold [List B] A [xf [List B] [list-conj B]] [nil B] [list-to-lseq A xs]
 
@@ -91,6 +91,6 @@ defn xf-into-list-rev [xf xs]
 ;; Uses xf-into-list-rev then reverses for correct element order.
 ;; One extra O(n) reverse, but fusion saves N-1 intermediate list allocations.
 ;; Renamed from into-list to avoid collision with prologos::core::collections::into-list.
-spec xf-into-list {A B : Type} <(S :0 Type) -> [S -> B -> S] -> S -> A -> S> [List A] -> [List B]
+spec xf-into-list <(S :0 Type) -> [S -> B -> S] -> S -> A -> S> [List A] -> [List B]
 defn xf-into-list [xf xs]
   reverse B [xf-into-list-rev xf xs]
diff --git a/racket/prologos/macros.rkt b/racket/prologos/macros.rkt
index ccfb4eb3d..aafeb382c 100644
--- a/racket/prologos/macros.rkt
+++ b/racket/prologos/macros.rkt
@@ -3033,6 +3033,22 @@
       ;; (don't look past non-constraint forms)
       [else (reverse constraints)])))
 
+;; Issue #20 / Direction 1+2 auto-introduction: rank kinds so that simpler
+;; kinds (Type) sort before higher-kinded ones (Type -> Type, etc.) when
+;; canonicalizing auto-detected implicit binder order.  Stable: equal ranks
+;; preserve relative order from `sort`.
+(define (kind-rank k)
+  (cond
+    ;; Any (Type n) — kind-Type at any universe level ranks first.
+    [(and (list? k) (= (length k) 2) (eq? (car k) 'Type) (exact-nonnegative-integer? (cadr k))) 0]
+    ;; (-> X Y) — single-arrow higher-kinded
+    [(and (list? k) (= (length k) 3) (eq? (car k) '->)) 1]
+    ;; Anything more elaborate
+    [else 2]))
+
+(define (implicit-binder-kind-ranks-before? a b)
+  (< (kind-rank (cdr a)) (kind-rank (cdr b))))
+
 ;; Format a kind datum as a readable string for error messages
 (define (datum->kind-string d)
   (cond
@@ -3362,6 +3378,10 @@
           (values body-tokens #f))))
   ;; Also handle inline keyword-headed children from WS mode
   ;; e.g. (:doc "...") as a direct child of the spec form
+  ;; List-valued keys (e.g. :where, :laws, :examples) must keep their values as
+  ;; a list even when only a single entry is present — a single-constraint
+  ;; `:where (Foo A)` would otherwise be silently flattened into the constraint
+  ;; itself, breaking expand-bundle-constraints downstream.
   (define-values (pre-meta-tokens metadata)
     (let loop ([remaining pre-meta-tokens-0]
                [kept '()]
@@ -3376,8 +3396,17 @@
          (define val (cdr entry))
          (define merged-val
            (cond
+             ;; (:doc "string") → just the string
              [(and (= (length val) 1) (string? (car val))) (car val)]
+             ;; List-valued keys: always keep val as a list of forms
+             [(memq key '(:where :properties :laws :includes :examples
+                          :see-also :implicits)) val]
+             ;; First element is a pair → assume list-of-forms (e.g. :examples
+             ;; with a single example form, or :method entries)
+             [(and (pair? val) (pair? (car val))) val]
+             ;; Single value → unwrap (e.g. :over Sym, :doc "..." already handled)
              [(= (length val) 1) (car val)]
+             ;; Multiple values → keep as list
              [else val]))
          (loop (cdr remaining) kept (hash-set meta key merged-val))]
         [else
@@ -3450,10 +3479,33 @@
         auto-detected-binders))
   (define all-implicit-binders
     (append over-binder merged-implicit-binders filtered-auto-detected-binders))
-  (define refined-implicit-binders
+  ;; Auto-detected names — used below to canonicalize their order after kind
+  ;; refinement.  Explicit (user-supplied) binder order is preserved verbatim.
+  (define auto-detected-names
+    (map car filtered-auto-detected-binders))
+  (define refined-implicit-binders-raw
     (if (or (null? all-implicit-binders) (null? all-constraints))
         all-implicit-binders
         (propagate-kinds-from-constraints all-implicit-binders all-constraints name)))
+  ;; Canonical-order auto-detected binders by kind: kind-`Type` before 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 consistent regardless of whether the user declares
+  ;; vars explicitly or relies on Direction 1/2 auto-introduction.
+  ;; Explicit (and `:over`) binders keep their declared order.
+  (define refined-implicit-binders
+    (cond
+      [(null? auto-detected-names) refined-implicit-binders-raw]
+      [else
+       (define explicit-binders
+         (filter (lambda (b) (not (memq (car b) auto-detected-names)))
+                 refined-implicit-binders-raw))
+       (define auto-binders
+         (filter (lambda (b) (memq (car b) auto-detected-names))
+                 refined-implicit-binders-raw))
+       (define sorted-auto
+         (sort auto-binders implicit-binder-kind-ranks-before?))
+       (append explicit-binders sorted-auto)]))
   ;; Detect and desugar variadic rest type: `A $rest` → `(List A)`
   ;; The $rest sentinel marks the preceding type as variadic.
   (define-values (desugared-type-tokens rest-type)
diff --git a/racket/prologos/tests/test-extended-spec.rkt b/racket/prologos/tests/test-extended-spec.rkt
index 0fb65f40b..b26f04513 100644
--- a/racket/prologos/tests/test-extended-spec.rkt
+++ b/racket/prologos/tests/test-extended-spec.rkt
@@ -644,6 +644,78 @@
     (define b-binder (assq 'B binders))
     (check-true (pair? b-binder))))
 
+;; ========================================
+;; 9b. Issue #20: Direction 1 + Direction 2 combined
+;; ========================================
+;; Validates the issue's target form — bare `A`, `B`, `C` with `:where`
+;; pinning the higher-kinded `C`'s kind. The bare-form spec-entry must equal
+;; the explicit-form spec-entry's implicit-binders.
+
+(test-case "spec: D1+D2 combined — kind-Type and HKT both auto-introduced"
+  (parameterize ([current-prelude-env (hasheq)]
+                 [current-module-definitions-content (hasheq)]
+                 [current-spec-store (hasheq)]
+                 [current-property-store (hasheq)]
+                 [current-functor-store (hasheq)]
+                 [current-preparse-registry (current-preparse-registry)]
+                 [current-trait-registry (hasheq)]
+                 [current-trait-laws (hasheq)])
+    (process-string
+      "(trait (MySeq (C : (-> (Type 0) (Type 0)))) (to-seq : (C A) -> (C A)))")
+    ;; Bare form — A, B, C all auto-detected; C kind inferred from :where
+    (process-string
+      "(spec gmap (A -> B) -> (C A) -> (C B) where (MySeq C))")
+    (define se (lookup-spec 'gmap))
+    (define binders (spec-entry-implicit-binders se))
+    (check-equal? (cdr (assq 'A binders)) '(Type 0))
+    (check-equal? (cdr (assq 'B binders)) '(Type 0))
+    (check-equal? (cdr (assq 'C binders)) '(-> (Type 0) (Type 0)))))
+
+(test-case "spec: bare form equals explicit form (D1+D2 idempotence)"
+  (parameterize ([current-prelude-env (hasheq)]
+                 [current-module-definitions-content (hasheq)]
+                 [current-spec-store (hasheq)]
+                 [current-property-store (hasheq)]
+                 [current-functor-store (hasheq)]
+                 [current-preparse-registry (current-preparse-registry)]
+                 [current-trait-registry (hasheq)]
+                 [current-trait-laws (hasheq)])
+    (process-string
+      "(trait (MySeq (C : (-> (Type 0) (Type 0)))) (to-seq : (C A) -> (C A)))")
+    (process-string
+      "(spec g-bare (A -> B) -> (C A) -> (C B) where (MySeq C))")
+    (process-string
+      (string-append
+        "(spec g-explicit ($brace-params A B : (Type 0))"
+        "                ($brace-params C : (-> (Type 0) (Type 0)))"
+        "                (A -> B) -> (C A) -> (C B) where (MySeq C))"))
+    (define bare (spec-entry-implicit-binders (lookup-spec 'g-bare)))
+    (define expl (spec-entry-implicit-binders (lookup-spec 'g-explicit)))
+    (check-equal? bare expl)))
+
+(test-case "spec: D2 single-constraint metadata :where preserves list shape"
+  ;; Regression: inline (:where (Foo A)) (a single constraint in metadata
+  ;; child form, not the trailing block form) used to be flattened from
+  ;; ((Foo A)) to (Foo A), which then crashed expand-bundle-constraints.
+  (parameterize ([current-prelude-env (hasheq)]
+                 [current-module-definitions-content (hasheq)]
+                 [current-spec-store (hasheq)]
+                 [current-property-store (hasheq)]
+                 [current-functor-store (hasheq)]
+                 [current-preparse-registry (current-preparse-registry)]
+                 [current-trait-registry (hasheq)]
+                 [current-trait-laws (hasheq)])
+    (process-string
+      "(trait (MySeq (C : (-> (Type 0) (Type 0)))) (to-seq : (C A) -> (C A)))")
+    ;; The (:where (MySeq C)) inline child shape is what the WS reader
+    ;; produces for a single-constraint :where keyword line.
+    (process-string
+      "(spec gmap2 (A -> B) -> (C A) -> (C B) (:where (MySeq C)))")
+    (define se (lookup-spec 'gmap2))
+    (check-true (spec-entry? se))
+    (define binders (spec-entry-implicit-binders se))
+    (check-equal? (cdr (assq 'C binders)) '(-> (Type 0) (Type 0)))))
+
 ;; ========================================
 ;; 10. flatten-property: :includes resolution
 ;; ========================================