Inference: a section over a fully-specced user function doesn't infer its type in a no-expected-type position

[hierophantos]

Summary

A partial application (section) over a user function whose signature is fully known fails to synthesize its type when there is no expected type from context (e.g. a bare def := …). The same partial works everywhere an expected type is supplied. The section case is the compelling one: the hole's type is fully determined by the function's spec, so it should synthesize without needing an annotation.

Repro (HEAD 4e56da1d, via process-file)

spec pow Int Int -> Int
defn pow [x n]
  match n
    | 0 -> 1
    | _ -> * x [pow x .(n - 1)]

;; WORKS — an expected type is supplied:
pow 2 10                              ;; => 1024
map [pow 2 _] '[1 2 3 4]              ;; => '[2 4 8 16]   (map checks the arg against [A -> B])
[pow 2 _] 3                           ;; => 8            (applied directly)
def k : <Int -> Int> := [pow 2 _]    ;; k 5 => 32       (annotated)

;; FAILS — no expected type:
def g := [pow 2 _]                    ;; ERROR: Could not infer type
def f := [fn [x] [pow 2 x]]           ;; ERROR: Could not infer type

Diagnosis

The failure is specific to the pure-synthesis position (no expected type):

• Section [pow 2 _] — the hole type is fully determined by pow's spec (Int), so a section over a fully-specced function should synthesize Int -> Int on its own. This is the gap to close.
• Unannotated lambda [fn [x] [pow 2 x]] — deriving the domain from the body's use of a specced function is the more standard "synthesis needs annotation-or-expected-type" limitation (lower priority; may be by-design).

Contrast: keyword-operator sections ([+ _ 1]) do work in synthesis position (from the N6e first-class-ops arc); user-function sections do not.

Related (minor)

A function type in a def/the annotation must use angle brackets <Int -> Int>; the square-bracket form [Int -> Int] silently mis-parses as application and yields a confusing "Unbound variable" error. A clearer diagnostic (or accepting [T -> T]) would help.

Notes

• Owner-confirmed the section-over-a-fully-specced-function case should be made to work.
• On the same first-class-ops surface as the N6e arc.