flan/docs/SPIKE-INFERENCE.md

# The inference spike, answered: the concern was right, and not for the reason it was given

> **Nothing was built.** SPIKE-GENERICS.md is measurement-heavy because a branch existed to measure; this is a
> reading of `lib/check.ml`, `lib/session.ml`, `lib/parse.ml` and the specs, with small probe programs where a
> probe settles something a reading cannot. The one number quoted below — 1.8 ms for a whole-program check — is
> SPIKE-GENERICS.md's, and the delta an inference fixpoint would add to it **was not measured**. Every other
> claim is cited to a line.

The question: can a `defn`'s type annotations become optional, inferred from the body and its uses, without
breaking the live dev loop. The author wants `(defn settle [row col] ...)` to check while sketching.

**The answer is: don't, in that form — and the obstacle is not the dev loop.** The live loop handles a changed
inferred signature correctly the moment inference is body-local; `Session.compatible` catches it by construction
and says so in the right words. What stops `(defn settle [row col] ...)` is three things that were each decided
on purpose, for reasons written down at the time, and every one of them predates this question:

1. **The grammar.** `(defn settle [row col] ...)` is not a syntax error today. It **parses**, as one parameter
   `row` of type `col`. The spelling the author wants is the one spelling that provably cannot be given the
   meaning they want.
2. **Literal defaulting.** `(+ x 1)` does not say what `x` is. It says `1` is an `i32` unless something above it
   says otherwise, and under inference the "something above it" is gone. Inferring `x := i32` from that is not
   inference; it is a default wearing inference's clothes, and it moves its error to a call site.
3. **The generic reading is refused at the definition.** `(defn settle [row col] (+ row col))` read as generic
   gets plan.org's rule applied to it, which is the refusal SPIKE-GENERICS.md quotes verbatim: *`+` over the type
   variable `t` is refused*. Reusing `check_generic` does not buy inference; `check_generic` is the thing that
   rejects the example.

What *is* available, cheaply, with a precedent already in the file, is **return-type inference only**. That is
the scoped recommendation and its boundary is drawn at the end.

## What the previously-voiced concern got right, and what it got wrong

The concern, paraphrased: live re-evaluation of functions makes inference difficult.

**Wrong about the mechanism.** `Session.eval` re-checks the *whole* program on every `C-c C-c` —

```ocaml
(* session.ml:586 *)
  let program, env = Check.program_with_env decls in
  compatible ~origin:(Check.instantiation_origin env) ~loc t.program program;
```

— and `compatible` (session.ml:181) compares the new `Tast.program` against the installed one over
`Tast.fn`'s `params` and `ret`, which are types and not source text:

```ocaml
(* session.ml:191 *)
         let same =
           List.length f.Tast.params = List.length g.Tast.params
           && List.for_all2 Types.equal f.Tast.params g.Tast.params
           && Types.equal f.Tast.ret g.Tast.ret
         in
```

It does not know or care where a type came from. An inferred signature that changes is caught exactly as a
written one is, and the refusal already prints both tuples (session.ml:239): *"%s changes signature, from
(Fn [...] ...) to (Fn [...] ...); the calls already compiled into the running program pass the old one. Restart
to change it."* There is no lock to build and no "inferred at first definition, frozen thereafter" state to
keep: the whole-program re-check means the signature is recomputed from the current text every time, so it is a
pure function of what is in the buffer, and `compatible` is the diff. **The dev loop's machinery is already
sufficient.**

**Right about the conclusion, via a mechanism that has a name.** The soundness above holds *only while the
inferred signature depends on nothing but the edited function's own body.* The moment inference reads call
sites, the whole-program re-check turns from an asset into the hazard:

- Editing function `A` changes the types `A` passes to `B`.
- `B`'s signature is inferred from its uses, so `B`'s signature changes.
- `compatible` refuses, naming `B` — a function that appears nowhere in the form the author just evaluated —
  with two type tuples they never wrote, for a reason not visible at the line they edited.

That is not a hypothetical failure mode; it is the failure mode `session.ml`'s `?origin` parameter already
exists to soften for generics, and the comment there describes it in exactly these terms:

```ocaml
(* session.ml:200 *)
              The refusal then arrives about [sort!-i32], which appears
              nowhere in the file being edited, for a reason invisible at the
              edited line.
```

For a generic there is at least an answer to give — *this is the copy of the generic `sort!` at `i32`*. For a
use-directed inferred signature there is no such sentence. The honest one is "something else you edited changed
what this function's parameters are", and the set of things that could have done it is the program.

**So the discriminating constraint for the whole design is: inference may read the function's own body and
nothing else.** Everything below is downstream of that.

## Question 2 — direction and scope, and the two features that poison it

Full Hindley–Milner is out before the language's features are considered, because it is out by the constraint
above: HM's whole point is that a use constrains a definition. Constraining `defn` inference to the body makes
it **local/bidirectional**, which is what the checker already is.

### The checker is already bidirectional, and there is a worked precedent

`check` threads a `?want` — an expected type — through every expression, and the elaborate one-directional
inference the language already has is the `fn` literal:

```ocaml
(* check.ml:1980 *)
and check_fn ctx ~want loc (params : string list) body =
  let pts, ret =
    match want with
    | Some (Types.Fn (ps, r)) when List.length ps = List.length params -> ps, r
```

An `fn`'s parameters carry no types at all, and they get them from position. That is the feature the author is
asking for, already in the language, at a different binding form. And the refusal for when it is unavailable is
written, in the voice a `defn` version would have to borrow:

```ocaml
(* check.ml:1993 *)
      fail loc
        "nothing here says what this fn's parameters are — an fn takes its \
         types from the position it is written in, so it goes in an argument \
         whose parameter is a (Fn [T ...] R), and a name already written as a \
         defn goes anywhere"
```

Note the last clause. The `fn` literal's inference works *because* a `defn` is annotated. It is checking mode
all the way down, and `defn` is where the types enter the system.

### What a `defn` body can actually tell you about a parameter

Bidirectional inference has no synthesis rule for a variable. It can only propagate: `x` appears as the first
argument of `g`, `g`'s first parameter is `i64`, therefore `x : i64`. That is a use *inside the body*, which the
constraint permits, and it is genuinely enough for a large class of Flan functions — a body that calls the
prelude or the user's own annotated functions pins its parameters immediately.

It is not enough for the author's example, and the reason is the second poison.

### Literal defaulting: `(+ x 1)` — what is `x`?

`i32`, and not because anything inferred it.

```ocaml
(* check.ml:1803 *)
and int_literal loc ~want ?(default = Types.I32) n =
  match want with
  | Some (Types.Int k) -> mk loc (Types.Int k) (Tast.Int (in_range loc k n, k))
  ...
  | _ -> mk loc (Types.Int default) (Tast.Int (in_range loc default n, default))
```

Today the annotation supplies `want` and the literal takes the parameter's type. Probed
(`scratchpad/p2.flan`): `(defn f [x i64] i64 (+ x 1))`, `(defn g [x u8] u8 (+ x 1))` and
`(defn h [x f32] f32 (+ x 1))` all check, and the same literal `1` is an `i64`, a `u8` and an `f32` in the three
bodies. The arithmetic is overloaded over sized ints and floats, and the annotation is what selects the
overload.

Remove the annotation and there is nothing to select with. `(+ x 1)` would have to make `x` an `i32` by
*default*, which is a silent monomorphisation nobody wrote — and the error it produces lands at a call site,
not at the definition. That failure is already observable in the one place the language does infer a binding
with no annotation, the `let` (probe `p6.flan`):

```
(defn f [x i64] i64 (+ x 1))
(defn main [] ()
  (let [n 3]
    (println (f n))))

p6.flan:4:17: expected i64, found i32
  4 |     (println (f n))))
    |                 ^
```

The mistake is at line 3 — `n` defaulted — and the caret is at line 4. The same program with `f` taking `i32`
checks. NEXT.md:1718 records this hazard already in the wild: *"a `let` has no annotation, so `[3.5 -1.0]` is an
`[f64]` and every element in `programs/algorithms.flan` is…"*.

For a `let` this is contained: the binding, the default and the use are all inside one function, usually within
a few lines, and the annotation that would fix it is an argument away. For a `defn` parameter it is not
contained at all. The default would be baked into a *signature*, published to every call site in the program and
into the running process, and the first thing it does under `C-c C-c` is make `compatible` refuse when the
author later adds the annotation they meant.

**This is the concrete answer to the question as posed.** `(+ x 1)` cannot make `x` anything. The three
principled options are all worse than an annotation:

- **Default it to `i32`.** Silent, and wrong for a body about to be called with an `i64`.
- **Refuse it** — "nothing here says what `row` is." Correct, and it refuses the author's example, which is the
  one they asked for.
- **Generalise it** — make `row` a type variable. That is question 3, and it is refused at the definition.

No implicit widening (`sum-i32` returns `i64` by explicit cast, SPIKE-GENERICS.md question 5) closes the escape
where a default could be "widened later". Fixed arrays, value semantics and where-predicates are neutral —
none of them is harder to infer than to check, because none of them is inferred *from*; they are all checked
*against*. The poison is entirely in the two overloaded-by-expectation forms: the integer literal and the
arithmetic over it.

## Question 1, concluded — redefinition

Restating against the above, since it is the question the spike exists for.

**Under body-local inference, redefinition is a solved problem and needs no new machinery.** The inferred
signature is a function of the edited text; `compatible` compares it to the installed one; the refusal already
names both tuples and tells the author to restart. The only thing worth adding is one clause to the message:
that the types were inferred and from where, so the author is not hunting a signature they never wrote. That is
a `?origin`-shaped change, one call site, and `?origin` is the proof it fits.

**Under use-directed inference, it creates a new class of refusal with no good message**, for the reasons in the
section above. This is where "annotations required only for what the session already holds" would come in as a
mitigation — and it is worth saying plainly that **it is a mitigation for a problem the body-local design does
not have.** There is nowhere natural to keep the lock, either: `Check.program_with_env` builds a fresh `env`
each evaluation (SPIKE-GENERICS.md makes the same observation about the instantiation cache — *"there is no
persistent cache to invalidate and therefore no staleness to get wrong"*), so a lock would have to live in
`Session.t` as a new table of frozen signatures, with its own invalidation story, its own refusal, and its own
answer to "what does a fresh `flan check` of the same file do, which has no session." Do not build it. Pick the
design that does not need it.

## Question 3 — interaction with generics: "unannotated = generic" is refused at the definition

It is the reading that looks cheapest, because the machinery exists — `check_generic` (check.ml:5947),
`generic_call` and `instantiate` (check.ml:4964, 5043), the per-call-site instantiation cache, `bind_ty`
substituted left to right. Reading an unannotated `defn` as a generic one with fresh variables, then inferring
the `where` clauses from the operators the body uses, is a real design and someone will propose it.

**It fails on the author's example, by a rule plan.org chose deliberately.** plan.org:928:

> Generic parameters → inferred at call sites, no explicit instantiation. No type classes. An operator over a
> variable with no `where` clause asserting it is rejected at the definition; a `where` predicate is what admits
> it.

`build_program` runs the abstract pass over every generic body (check.ml:6202), and SPIKE-GENERICS.md quotes
what it says about exactly this shape:

```
spike/generics/reject.flan:1:26: + over the type variable t is refused: an unconstrained type variable supports
only what every type supports, and + is not that (plan.org, Types). Take the operation as a parameter — a
(Fn [t t] ...) — and call it here
```

So under the generic reading, `(defn settle [row col] (+ row col))` is refused at its definition. Confirmed
empirically — today's message for the author's literal example is a different one, because `col` is read as a
type name, but it lands in the same machinery (`scratchpad/p1.flan`):

```
p1.flan:1:19: generic code over the type variable col is not implemented yet — milestone 5 (see plan.org)
```

The "infer the `where` clauses from the operators used" repair is where this gets expensive rather than
impossible. Inferring `{:where (ordered? $t)}` from a `<` in the body is a constraint-collection pass — the
predicates are not a fixed lattice (`pred_entails` already has `ordered?` covering `equal?`), and the predicate
set would have to be closed under the operators, which is a type-class system by another road. plan.org:928 says
*no type classes* in the same breath. And it would still not save `(+ row col)`: there is no arithmetic
predicate, by design — the language's answer is "take the operation as a parameter", which is a *longer*
signature, not a shorter one. SPIKE-GENERICS.md's question 5 already paid this bill in the prelude: *"The
functions collapse; the calls get longer."*

**So unannotated must mean monomorphic**, which hands the whole question back to literal defaulting.

One thing the generics machinery *does* contribute, and it is the good news in this section: it proves the
checker can run a body more than once, with an environment installed and restored around it
(`check_generic`'s `saved_vars`/`saved_preds`/`finish`), and that re-checking bodies is cheap — 1.8 ms
whole-program, flat, dominated by the 1665-line prelude. An inference fixpoint is the same shape of cost. It was
not measured.

## Question 4 — allocators and ownership: this question closed on 2026-09-18

It was live, and it is not any more. **Signatures carry types and nothing else.**

- **Move-only is gone.** spec-memory.md:182: *"**The move-only concept itself is gone.** Everything copies — a
  container as much as an integer."* `is_move_only` does not appear anywhere in `lib/`. SPIKE-GENERICS.md's
  "Fiddly" row — ownership not being decidable without the concrete type, the one analysis that did not survive
  abstraction — was written before the repeal and no longer has a subject.
- **The allocator is not in the calling convention as a parameter.** It is a dynamic read: `context/allocator`
  and `context/temp` resolve to runtime primitives (check.ml:1860-1865), `with-allocator` rebinds a dynamic
  variable (check.ml:627), and an operation takes at most one explicitly-named allocator as an ordinary argument
  of type `Alloc` (check.ml:3354). Nothing about it is derived from a signature, so there is nothing for
  inference to see through.

Inference would have to infer a parameter of type `Allocator` the same way it infers any other — from a use
inside the body — and that is the ordinary case, not a special one.

## Question 5 — error quality

The repo's discipline is that a refusal names the thing and points at the line. Inference's structural problem
is that the cause and the symptom separate, and the `p6.flan` probe above is the language's own miniature of it:
the mistake is the default at line 3, the caret is at line 4.

The disciplines that keep it acceptable, in the order they matter:

1. **Body-local inference is the whole of the discipline.** It bounds the distance between cause and symptom to
   one function. Nothing else on this list would rescue a design without it.
2. **Never default in signature position.** A parameter whose type is not pinned by a use in the body is refused
   by name — *"nothing here says what `row` is; write its type"* — rather than silently becoming an `i32`. This
   is the `fn`-literal refusal at check.ml:1993, reworded for `defn`, and it is the single most important rule
   in the design. It is also the rule that refuses the author's example, and the report should not pretend
   otherwise.
3. **The instantiation-origin pattern, borrowed.** `Session.compatible`'s `?origin` shows how a refusal about a
   name the source does not contain gets an explanation. The inference version is smaller: the signature is
   inferred, and here is the form that pinned each parameter. One `Loc.note` per parameter.
4. **`Loc.failk` keys.** Every refusal in this checker is keyed (`check/unknown-function`,
   `check/predicate-not-carried`). An inference refusal gets `check/parameter-not-determined` and is testable
   like every other.

The annotation ridge that makes this work is not a new idea in the repo: it is plan.org:202 — *"Annotations at
function boundaries are unavoidable"* — and the reason given there is prescient about question 3's failure:
*"because compile-time overloading is incompatible with full inference."* Overloading is planned, not built
(plan.org:387, `defmethod` appears nowhere in `lib/`), so the incompatibility is a future collision rather than a
present one; but it is a collision the plan already foresaw, and any inference design that survives today has to
be checked against it before multimethods land.

## Question 6 — the two backends, the daemon, and eldoc

**Nothing downstream of the checker knows a signature was written.** `emit.ml`, `x86.ml` and `js.ml` read
`Tast.fn`'s `params` and `ret`, which are `Types.t` — they have never seen an `Ast.texpr`. The daemon is the
same:

```ocaml
(* dev.ml:1015 *)
let signature_of_fn (f : Tast.fn) =
  Printf.sprintf "%s [%s] %s" f.Tast.name
    (String.concat " " (List.map Types.to_string f.Tast.params))
    (Types.to_string f.Tast.ret)
```

The `defs` op (dev.ml:1025) and the disassembly header (dev.ml:2671) both go through it, and `flan.el`'s eldoc
reads the `defs` cache and nothing else. **So eldoc shows an inferred function's real signature, for free, in
the same format.** The comment right above it even removes the one objection someone would raise: *"Parameter
*names* are not in the Tast, so a signature shows types only"* (dev.ml:1014) — eldoc is already showing types
without names, so an inferred signature is indistinguishable from a written one in the echo area, which is the
correct behaviour and cost nothing to get.

The one thing that *does* read the annotation slot is the frontend, and it has a booby trap:

- `Ast.fn.ret` is already `Ast.texpr option`, and both `collect` sites read `None` as **`Unit`**
  (check.ml:5569 and 5706: `match fn.Ast.ret with None -> Types.Unit | Some t -> resolve env t`).
- `shim.ml:532` *produces* `ret = None` meaning `Unit`, for the struct-return wrapper. `shim.ml:589` and
  `cimport.ml:1579` both read `None` as void.
- `load.ml` maps over it in three places (314, 323, 354) and walks it for dependencies twice (637, 652).

So **`None` is taken**. "Infer me" needs a third state — `Ast.ret : Written of texpr | Unit | Infer`, or a
separate flag — and that is a small, mechanical edit across `load.ml`, `shim.ml`, `cimport.ml` and two `collect`
arms. Small, but it is not free, and anyone who reads `ret option` and concludes the slot is already optional
has misread it.

## Question 7 — cost, and the increments

### The grammar comes first, and it is not a detail

```ocaml
(* parse.ml:104 *)
let rec fields (f : Form.t) (items : Form.t list) : Ast.field list =
  match items with
  | [] -> []
  | name :: ty :: rest ->
    no_pattern name;
    { Ast.fname = sym name; fty = texpr ty; floc = name.loc } :: fields f rest
  | [ odd ] ->
    Loc.fail odd.loc "field %s has no type — these come in name/type pairs"
      (Form.to_string odd)
```

A parameter vector is a flat list of pairs. Probed:

- `(defn settle [row col] ...)` — **parses**, as `row : col`. Not an error. The error the author sees comes much
  later, from the type resolver, about a type named `col`.
- `(defn settle [row] i32 ...)` — `p4.flan:1:15: field row has no type — these come in name/type pairs`.
- `(defn settle [row col x] i32 ...)` — `p3.flan:1:23: field x has no type — these come in name/type pairs`.

So an odd count is a parse error and an even count is a silently different program. There is no count to
disambiguate by, which is precisely the finding NEXT.md item 4 records for `let`: *"`let` is a flat list of
pairs, so it cannot disambiguate by count the way `defvar` and `defconst` do — those read `[n t v]` as three
arguments to a form, and there is no such boundary between one pair and the next."*

And the meaning that would have to be given to `[row col]` is exactly the class of change this parser was
rewritten to make impossible. The `defn` return slot was made mandatory (parse.ml:904) because the optional
version *"was wrong twice in one day, the second time parsing `(defn f [] (Rune {.code 65}) (bar))` as a
function returning a Rune with a one-form body, silently, in every file in the language. A silent misparse is
the worst failure class available, and macros now generate definitions, which widens it."* `defunion` was
refused by name (parse.ml:881) for the identical reason. Making `[row col]` mean two unannotated parameters
reintroduces the pattern in the one form both of those decisions were about, and it breaks every existing
two-parameter signature in the corpus in silence.

**So a `defn` with unannotated parameters needs new syntax** — a marker, a separate vector, or a distinct form —
and the choice is a language-design decision, not a compiler one. NEXT.md item 4 already sketched the three
surfaces for the `let` version of the same problem and preferred the one that avoided new binding-vector syntax.
The cheap first step below is the one that needs **no** grammar change at all.

### What a full implementation touches, honestly

| | |
|---|---|
| **Grammar** | new parameter syntax in `parse.ml`'s `fields`/`defn` arms, plus its own refusals; a language decision before it is an edit |
| **AST and frontend** | a third state on `Ast.fn.ret` and a way to spell an un-annotated `Ast.field`; mechanical fallout in `load.ml` (5 sites), `shim.ml` (3), `cimport.ml` (2) |
| **The checker's two-pass split** | the real work. `collect` (check.ml:5545-5715) builds `env.fns` from annotations *alone*, before any body is looked at; `check_fn` (check.ml:5851) opens with `Hashtbl.find env.fns fn.Ast.name`. Inference breaks the split in both directions: a signature now needs its body, and a body needs its callees' signatures. The fix is a fixpoint, and the precedent is in the same function (check.ml:5725, the untyped-`defconst` loop) — *"Also to a fixpoint, and for the same reason: one untyped constant may be defined in terms of another declared after it. A constant that still does not check once no progress is left has a real error, so the last round is run without swallowing it."* |
| **Mutual recursion** | has no fixpoint. Two inferred functions each calling the other pin nothing, and must be refused **by name**, saying which two and that one of them needs an annotation. This is a new refusal with no analogue in the file |
| **The session** | one clause on the `compatible` message saying the types were inferred, in the `?origin` shape |
| **Backends, daemon, eldoc** | **untouched**, per question 6 |
| **Does not work** | "unannotated only for non-exported defns" is not available as a boundary. `Load` flattens every import into one namespace before checking (SPIKE-GENERICS.md's last "no plan" row says the same thing about generics across packages), so there is no export boundary at check time to draw the line at |

### The cheap first step, and it is a real one

**Infer the return type only.** Parameters stay annotated. `(defn settle [row i32 col i32] (+ row col))`.

It is worth taking seriously because everything expensive above evaporates:

- **One grammar decision instead of two, and it needs a marker.** Omitting the return slot cannot be decided by
  count, and the temptation to say otherwise should be resisted: `defvar` and `defconst` disambiguate by count
  because they have a *fixed maximum arity* — `[n t v]` is three slots and there is no fourth. A `defn` body is
  an unbounded list of forms, so `(defn f [] (a) (b))` is `ret=(a), body=(b)` or `infer-ret, body=(a) (b)` and
  nothing in the shape decides which. That is the same structural fact NEXT.md states about `let` — *"there is
  no such boundary between one pair and the next"* — moved to the boundary between the return slot and the
  first body form, and it is precisely the case that sank the slot the first time: `(defn f [] (Rune {.code
  65}) (bar))` is a two-form example, and a count-based rule has no rule to apply to it at all. The
  one-form case, contrary to appearances, is the safe one: `(defn f [] ())` means the same either way, and
  `(defn f [] Bar)` with no body is already refused by `check_fn`'s *"%s returns %s but has no body"*.

  So the scoped version requires a **marker** — `(defn f [] :- (foo))`, or whatever spelling wins. That is one
  new token in one parser arm, refusable by shape rather than by looking a symbol up in a table, which is the
  property parse.ml:904 says the old design lacked. It is a much smaller ask than the parameter-vector surgery
  optional parameters need, but it is **not free**, and this report claimed otherwise in an earlier draft.
- **No parameter defaulting.** Every parameter still has a type, so `want` still flows down into the body,
  `(+ x 1)` still means what it means today, and the integer-literal hazard never arises. This is the point: the
  return type is *synthesised from* a fully checked body, which is the one direction bidirectional checking
  actually supports.
- **The fixpoint is the `defconst` one**, with the same shape and the same stated limit. Two mutually recursive
  return-inferred functions do not converge and get refused by name in the last round — and the refusal should
  name the *chain*, not just the pair, because the chain is what an author has to break.
- **`compatible` needs no change, but there is a cascade and it is smaller than the use-directed one.** The
  inferred return is a function of the body, and a body contains calls: if `B`'s last form is `(A x)` then
  `B`'s return *is* `A`'s return, so editing `A` changes `B`'s signature and `compatible` refuses about `B`,
  which the author did not touch. This is the same shape as the hazard that rules out use-directed inference —
  but with one decisive difference: the primary refusal about `A` is present and correct, and every downstream
  one is *explainable in a sentence the compiler can write* — "B returns what A returns". The use-directed
  version has no such sentence. Propagation follows call edges out of the body, so it is bounded and nameable;
  that is the whole distinction.
- **eldoc, `defs` and both backends are unchanged**, per question 6.

It does not give the author `(defn settle [row col] ...)`. It gives them a `defn` that is shorter by one token,
and it removes the annotation that is most often mechanical — `()` on every mutating function in the corpus.
Whether that is worth a grammar decision is the author's call and this report does not make it.

## Verdict

**Do a scoped version, or do nothing. Do not build optional parameter annotations.**

The concern that was voiced was correct in its conclusion and wrong in its mechanism, and the distinction is the
useful part: **live re-evaluation is not what makes this hard.** `Session.compatible` already handles a changed
inferred signature correctly, in the right words, with no new machinery, the moment inference reads only the
edited function's body. If the dev loop had been the only obstacle, this would be a cheap feature.

What actually blocks it are three decisions the project already made on purpose:

- the parameter vector is a flat pair list, so `[row col]` already parses as something else, and giving it the
  wanted meaning reintroduces the silent-misparse class that mandatory return types and the `defunion` refusal
  were both introduced to close (parse.ml:881, parse.ml:904, NEXT.md item 4);
- integer literals default to `i32` when nothing expects otherwise (check.ml:1803), so an unannotated parameter
  is either silently monomorphised or refused — and the refusal refuses the motivating example;
- an unannotated parameter read as a type variable is rejected at its definition by plan.org's
  no-type-classes rule, which `check_generic` implements (check.ml:5947, plan.org:928).

**The scoped version's exact boundary:** parameter types stay mandatory; the return type becomes inferrable,
spelled with an explicit marker rather than by omission, from a body checked with every parameter already known;
inference reads the function's own body and never a call site; a return-inferred body that calls another
return-inferred function propagates along that call edge and no further; a cycle among them is refused by name,
naming the chain. Nothing downstream of `check.ml` changes. The grammar cost is one marker in one parser arm —
real, and one decision rather than the several optional parameters need.

**Top three risks**, in order:

1. **The grammar decision is the project, and it has already bitten twice.** Both times it bit, it bit
   silently — a program that compiled and meant something else. Any surface for "no annotation here" must be
   refusable by shape rather than by looking a symbol up in a table, or it will bite a third time. **The scoped
   version does not escape this** — a `defn` body is an unbounded form list, so an omitted return slot cannot be
   decided by count, which is why the marker above is a requirement and not a nicety. The difference between the
   scoped version and the full one is that the scoped version needs *one* such decision.
2. **Scope creep from "return only" to "parameters too."** The scoped version is pleasant and will immediately
   invite the next step, and the next step crosses from synthesis into defaulting. The line to hold is one
   sentence: *nothing may be defaulted in signature position.* Write it down before building, because
   the first `i32` that leaks into an inferred parameter will not announce itself — it will show up as a caller
   mismatch three functions away, as `p6.flan` shows.
3. **Compile-time overloading, when it lands.** plan.org:203 already says overloading and full inference are
   incompatible, and multimethods are still unbuilt. Any inference the language ships now becomes a constraint
   on how overload resolution can be specified later, and that bill is not payable in this lane.

## Reproducing

`dune build` is green; nothing in the tree was changed. The probes are one-liners and are quoted inline:

```lisp
;; p1 — the author's example: "generic code over the type variable col"
(defn settle [row col] (+ row col))

;; p2 — the annotation is what selects the arithmetic overload; all three check
(defn f [x i64] i64 (+ x 1))  (defn g [x u8] u8 (+ x 1))  (defn h [x f32] f32 (+ x 1))

;; p3, p4 — an odd parameter count is the only thing the parser refuses
(defn settle [row] i32 (+ row 1))          ; field row has no type
(defn settle [row col x] i32 (+ row col))  ; field x has no type

;; p6 — defaulting moves the error away from the cause
(defn f [x i64] i64 (+ x 1))
(defn main [] () (let [n 3] (println (f n))))   ; 4:17: expected i64, found i32
```