fix(typecheck): infer recursive functions' return type by fixpoint (#88) - #91
Conversation
Recursive functions returning a scalar were unwritable. The canonical shape,
straight out of examples/trefoil.tangle:
def length(w) = match w with
| identity => 0
| s1 . rest => 1 + length(rest)
| _ => 0
failed with "Cannot add Num and Word[0]".
Cause: while checking a function's own body, the function was bound with a
hard-coded return type of TWord 0, marked "placeholder" — and NOTHING ever
checked the inferred body type against that assumption. So the recursive call
`length(rest)` typed as Word[0], and `1 + length(rest)` was Num + Word[0].
A recursive function's return type occurs in its own derivation, so it must
be a FIXPOINT: assume a return type, check the body under that assumption,
and accept only if the body then has exactly the assumed type. Anything
weaker is a guess that merely failed to crash.
Candidate seeds are drawn first from the match arms that do NOT mention the
function (for `length` those are the two `0` arms, giving Num), then the
scalar types, then the original TWord 0 so prior behaviour stays reachable.
The list is finite and ordered, so this terminates. If no candidate is a
fixpoint we fall back to the original single pass, which re-raises its
original error — a definition that did not typecheck before still does not,
with the same message.
## The logic existed TWICE
check_statement had one copy and check_program's pass 1b had another, and
only check_program's is reached for whole programs — so the first version of
this fix changed nothing observable. They are now a single
`bind_function_def` called from both. That duplication is why the placeholder
survived: fixing one copy looked like fixing the bug.
## Scope
This closes the recursive-typing half of #88. The remaining example failures
are a DIFFERENT question — equal-width requirements on `==` and on match arms
— which cannot be changed in OCaml alone: Lean's `tEqWord` requires both
operands at the same width `n`, and TG-3's 496 kernel-checked obligations tie
OCaml's inference to that spec. It needs a cross-engine ruling like #50 did;
raised separately.
Tests: 5 new cases covering the `length` shape, that the inferred signature is
actually Num (not merely that it compiles), that a caller can use it at Num,
that non-recursive definitions are untouched, and that a genuinely ill-typed
recursive function still fails. Typecheck suite 119 -> 124; TG-3 still
1008/0; all other suites unchanged.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
![gitar-bot[bot]](https://avatars.githubusercontent.com/in/827041?s=60&v=4){kind=small}
|
Note Automatic reviews are paused because your trial's included automatic processing has been used for this period. Upgrade now, or comment "Gitar review" to run a review anytime. Code Review ✅ Approved 2 resolved / 2 findingsAdds fixpoint iteration to infer recursive function return types, successfully enabling scalar recursion like the length example. Consider expanding the candidate seed set and refining parameter handling in recursive_return_candidates.
✅ 2 resolved✅ Edge Case: Fixpoint candidates limited to scalars + TWord 0
✅ Quality: Seed inference ignores params; broad
|
| Compact |
|
Was this helpful? React with 👍 / 👎 | Gitar
|
|
Four of the five unparsed `conformance/valid/` programs — `v02_weave`,
`v08_crossing`, `v09_twist`, `v12_weave_expr` — use weave as a
**definition body**:
```tangle
def simple_crossing =
weave strands a:Q, b:Q into
(a > b)
yield strands b:Q, a:Q
```
The grammar allowed weave only as a top-level statement, so all four
failed. Typed strands (`a:Q`) and `yield strands` were never the problem
— those already parsed. Only the **position** did.
## Why the expression form is the right fix, not a corpus edit
My first instinct was that the corpus was wrong, since
`spec/grammar.ebnf` also said statement. Then I checked what a weave
statement actually *does*:
```ocaml
(* eval.ml *)
| WeaveBlock _wb -> (env, None) (* no-op *)
(* typecheck.ml *)
let _weave_ty = TTangle (input_boundary, output_boundary) in
gamma (* type computed, then DISCARDED *)
```
**As a statement, weave is inert.** It binds nothing, produces nothing,
and its type is thrown away. The construct could be written but never
used. Binding it to a name is the only thing that makes it reachable —
which is precisely what the corpus assumed all along.
The statement form is kept, so this is **purely additive**.
## Scope — no proof implications
Weave is outside the mechanised core: **0 occurrences in
`proofs/Tangle.lean`, 0 in the TG-3 corpus**. So this touches no proof
obligation, and `Weave` joins the other non-core constructors in
`tg3_emit`'s explicit rejection branch rather than being translated.
Threaded through `ast` (new `Weave of weave_block`), `parser`
(`primary_expr`), `typecheck` (types as the `Tangle[A,B]` it denotes;
body checked in the strand context exactly as the statement form does),
`eval` (the body *is* the value), and `pretty` (re-parseable form).
`expr_calls` also traverses into a weave body — otherwise recursion
inside one would be invisible to the #91 fixpoint search.
## What this does NOT fix: `v11_add_block`
`add{ 1 + 2 + 3 }` is **not a missing parse rule**. It is the **Harvard
data sub-language**:
| | |
|---|---|
| own expression grammar | literals, vars, arithmetic, equality,
`&&`/`\|\|`/`!`, calls, `if/then/else` |
| own type system | Int, Float, Rational, Hex, Binary, Bool, String,
Symbolic |
| own environments | `Π`, with visibility rules |
| own typing judgement | `⊢_hd` |
| conversion layer | Embed / Unembed |
| calling | bidirectional with Tangle |
**288 lines of `FORMAL-SEMANTICS.md` across 12 sections.** That is a
feature, raised separately. It remains the single entry in the corpus
manifest's known-gap list.
## Results
| | before | after |
|---|---|---|
| conformance | 14/19 | **18/19** |
| corpus manifest known-unparsed | 5 | **1** |
(It reported a *fake* 3/19 before #89 fixed the runner.)
The ratchet in `check-corpus.sh` **demanded** the manifest update — it
failed the build with *"now parses — drop it from
CONFORMANCE_KNOWN_UNPARSED"* for each file. That is exactly what it was
built to do.
## Tests
- weave as a definition body (the conformance form)
- **TG-4 round-trip**: pretty-print then re-parse yields the same AST —
needed because I changed `pretty.ml`
- guard that the statement form still parses (the change is additive)
Full suite green, 0 failures; TG-3 still 1008/0. `spec/grammar.ebnf`
updated to match, with the rationale recorded.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
1 participant
Recursive functions returning a scalar were unwritable. The canonical shape, straight out of
examples/trefoil.tangle:failed with
Cannot add Num and Word[0].Cause
While checking a function's own body, the function was bound with a hard-coded return type of
TWord 0, marked(* placeholder *)— and nothing ever checked the inferred body type against that assumption. Solength(rest)typed asWord[0], making1 + length(rest)aNum + Word[0].Fix
A recursive function's return type occurs in its own derivation, so it must be a fixpoint: assume a return type, check the body under that assumption, and accept only if the body then has exactly the assumed type. Anything weaker is a guess that merely failed to crash.
Candidate seeds come first from the match arms that don't mention the function — for
lengththose are the two0arms, givingNum— then the scalar types, then the originalTWord 0so prior behaviour stays reachable. The list is finite and ordered, so it terminates. If no candidate is a fixpoint, it falls back to the original single pass and re-raises its original error: a definition that didn't typecheck before still doesn't, with the same message.The logic existed twice
check_statementhad one copy andcheck_program's pass 1b had another — and onlycheck_program's is reached for whole programs. My first attempt at this fix therefore changed nothing observable, which is exactly how the placeholder survived so long: fixing one copy looks like fixing the bug. They're now a singlebind_function_defcalled from both.Scope — what this does NOT do
This closes the recursive-typing half of #88. The remaining example failures are a different question: equal-width requirements on
==and on match arms.That one cannot be changed in OCaml alone. Lean's rule requires both operands at the same width:
| tEqWord (Γ : Ctx) (e₁ e₂ : Expr) (n : Nat) : HasType Γ e₁ (.word n) → HasType Γ e₂ (.word n) → HasType Γ (.eq e₁ e₂) .booland TG-3's 496 kernel-checked obligations tie OCaml's
infer_exprto that spec. Changing one engine would silently break the differential. It needs a cross-engine ruling the way #50 did — raised separately, with the evidence.Tests
Five new cases, chosen so they can't pass vacuously:
lengthshape typechecksNumNumTypecheck suite 119 → 124. TG-3 still 1008/0. All other suites unchanged; corpus and RSR gates still green.
🤖 Generated with Claude Code