Improved implicit inference: implement Directions 1 + 2 (both, additive) from the 2026-02-22 design

[hierophantos]

Summary

Resurrect and complete the planned-but-unimplemented "Improved Implicit Binder Inference" work from docs/tracking/2026-02-22_IMPROVED_IMPLICIT_INFERENCE.org (status: PLANNED). Reduce the need for redundant {A : Type} and {C : Type -> Type} binders in spec signatures.

The two directions in the design are additive, not mutually exclusive — they handle disjoint variable kinds and a single spec can benefit from both:

Direction	Handles	Eliminates
1	kind-Type variables (A, B, C)	{A : Type}
2	higher-kinded variables (C : Type -> Type) used as type constructors	{C : Type -> Type} (when constrained via :where)

Surfaced as a non-blocking observation while reviewing pitfall PRs #4, #5, #15, #16 — each adds new specs using explicit {A B C : Type} binders that, post-cleanup, would not be needed.

Current state

• Direction 1 — works in many cases coincidentally but is not documented as canonical, not reliable across all cases, and stdlib uses explicit binders inconsistently. Working example in lib/prologos/core/algebra.prologos:

  spec sum [Add A] -> [AdditiveIdentity A] -> [List A] -> A
  

  No explicit {A : Type}, but works.
• Direction 2 — not implemented. Higher-kinded variables still need {C : Type -> Type} even when :where constraints fully determine the kind.

Target state

A single spec benefiting from both directions at once:

;; Before: explicit binders for both kind-Type and higher-kinded
spec gmap {A B : Type} {C : Type -> Type} [A -> B] -> [C A] -> [C B]
  :where (Seqable C) (Buildable C)

;; After: D1 handles A, B (no binder needed); D2 handles C (kind inferred from `:where (Seqable C)`)
spec gmap [A -> B] -> [C A] -> [C B]
  :where (Seqable C) (Buildable C)

Explicit binders remain for:

• Pedagogic clarity
• Disambiguation (rare cases where context doesn't pin the kind)
• Specs with no constraining position (e.g., spec empty {A : Type} [List A])

Motivating examples (recent contributions)

• PR Add pvec-zip-with library function (eigentrust pitfalls #13) #5: {A B C : Type} [A -> B -> C] [PVec A] [PVec B] -> [PVec C] → [A B -> C] [PVec A] [PVec B] -> [PVec C]
• PR parse-reader: splice multi-line spec continuations so -> stays top-level #4 test cases use {A : Type} that wouldn't be needed
• lib/prologos/core/generic-ops.prologos (6 specs): {A B : Type} {C : Type -> Type} paired with :where constraints — Direction 2 eliminates the explicit binder

Scope

Both directions are in scope; they can land in the same PR or sequentially:

• Implement Direction 1: documented, reliable kind-Type auto-introduction in extract-implicit-binders (macros.rkt)
• Implement Direction 2: kind inference from :where in propagate-kinds-from-constraints (macros.rkt)
• Mechanical refactor pass over lib/prologos/** to drop redundant binders
• Update prologos-syntax.md and docs/spec/grammar.org to document the canonical form

Out of scope:

• Curried ([A -> B -> C]) vs uncurried ([A B -> C]) function-type style convention — related but separate decision; tracked separately

Source

• Design: docs/tracking/2026-02-22_IMPROVED_IMPLICIT_INFERENCE.org
• Touch points: extract-implicit-binders and propagate-kinds-from-constraints in macros.rkt; trait store for kind lookups; process-spec pipeline

Priority

Medium-high (per the original design). Compounds with each new contribution adding explicit {A : Type} binders. Low risk — additive (bare form already partially works).