Polymorphic partial application at def-binding site fails inference (let-generalization gap)

[hierophantos]

Summary

Polymorphic partial application at a def binding site fails inference, even with explicit type annotations. The let-generalization gap blocks idiomatic combinator usage like def my-7 := [const 7] or def get-7 := [constantly 7].

Reproducer

Verified on current main (post-S2.e):

ns repro
spec constantly {A : Type} A -> Unit -> A
defn constantly [x]
  fn [u : Unit] x

;; Form (a) — bare partial application
def my-3 := [constantly 3]
;; Error: Could not infer type [constantly 3]

;; Form (b) — with type annotation
def my-3 : <Unit -> Int> := [constantly 3]
;; Error: Type mismatch "Unit -> Int" "<could not infer>" "[constantly 3]"

;; Form (c) — with explicit type instantiation
def my-3 := [constantly Int 3]
;; Error: Type mismatch (extra arg confusion)

All three fail. The polymorphic A cannot be pinned at the partial-application site, even when:

• The argument's type (Int from 3) should infer A := Int forward
• The annotation (Unit -> Int) should propagate backward to bind A := Int
• The explicit type argument should fill the implicit slot

What works (workarounds)

;; Monomorphic — A is fixed, no implicit to infer
spec constantly-int Int -> Unit -> Int
defn constantly-int [x] (fn [u : Unit] x)
def my-3 := [constantly-int 3]
[my-3 unit]    ;; → 3 ✓

;; Polymorphic but fully applied (bypasses the bind step)
[constantly 3 unit]    ;; → 3 ✓

;; Inline lambda (no combinator)
def my-3 := (fn [u : Unit] 3)
[my-3 unit]    ;; → 3 ✓

What this is and isn't

Is: a missing inference path for polymorphic partial application at def-binding sites.

Isn't the same as #20 (improved implicit inference / Directions 1+2). #20 is about introducing implicit {A : Type} binders for bare type variables. This issue is about resolving the implicit at partial-application time when it's already declared.

The design question

Two paradigms in dependent type systems:

Haskell-style let-generalization: let f = const 7 ⇒ f :: forall b. b -> Int. The polymorphism is preserved through the let binding.

Coq/Agda/Lean-style: requires either explicit type instantiation (@const _ 7), full bidirectional propagation through the bind site, or full-application before binding.

Prologos currently does neither cleanly. The annotation form def x : <T> := body should propagate T backward through body's elaboration; this currently doesn't reach the implicit type binder.

Scope (when designed)

• Decide: let-generalization (Haskell-style) vs explicit instantiation (Coq/Agda-style) vs hybrid
• Implement chosen approach in elaborator
• Test against canonical combinators: id, const, compose, flip, constantly
• Acceptance: at minimum def f := [const 7] produces f : forall b. b -> Int (or system-appropriate equivalent that the user can call freely)
• Coordinate with Improved implicit inference: implement Directions 1 + 2 (both, additive) from the 2026-02-22 design #20 (sibling implicit-inference work)
• Coordinate with PPN 4C broader elaboration-on-network direction

Out of scope for this issue

• Detailed implementation design (deferred to phase-time mini-design)
• The let-generalization vs explicit-instantiation decision (open architectural question)

References

• Surfaced via PR unify: lenient {m0, mw} compatibility (eigentrust pitfall #2) #17 (eigentrust pitfall Add EigenTrust reputation algorithm: implementation, tests, benchmark #2 review) and constantly discussion 2026-04-26
• Related: Improved implicit inference: implement Directions 1 + 2 (both, additive) from the 2026-02-22 design #20 (improved implicit inference)
• Prior art: the existing prelude const (works as 2-arg call only; same gap when partially applied)

Priority

Medium-high. Blocks idiomatic combinator-style code that users from Haskell / Clojure / TypeScript will naturally reach for. Compounds with each new contribution that uses partial application.