Summary
ML signature/binding arity is graded in one direction only. A parenthesised
(flat) signature domain enforces a flat binding, but a curried signature does
NOT enforce a curried binding — so a written int -> int -> int can silently
describe a function that lowers flat, and the author gets no diagnostic.
Reproduction
Four combinations, osprey s.ospml --check:
| signature |
binding |
result |
add : int -> int -> int |
add (a, b) = … |
accepted |
add : int -> int -> int |
add a b = … |
accepted |
add : (int, int) -> int |
add (a, b) = … |
accepted |
add : (int, int) -> int |
add a b = … |
rejected |
The rejection reads:
function `add`: a parenthesised signature domain declares flat parameters;
write `add (…) = …` to match
Row 1 is the gap: it is the mirror image of row 4 and is accepted in silence.
Why row 1 is a mismatch
docs/specs/0024-MLFlavorSyntax.md makes the two forms distinct lowerings, not
spellings of one thing:
[FLAVOR-ML-CURRY] (line 74): "Whitespace parameters curry. add x y = body
lowers to a one-parameter Stmt::Function whose body is a one-parameter
Expr::Lambda."
- Line 86: "Parenthesised comma-separated parameters are explicitly flat … The
flat binding lowers to one two-parameter Stmt::Function; the call lowers to
one two-argument Expr::Call."
So int -> int -> int describes the curried lowering and add (a, b) produces
the flat one. Row 4 is rejected for exactly this reason; row 1 is the same
disagreement with the operands swapped.
The corpus already contains one
tests/regressions/basics/functional/functional_showcase.test.ospml:17:
add : int -> int -> int
add (a, b) = a + b ?: 0
Its Default twin declares fn add(a, b) — flat — and the twins emit identical
IR, so the BINDING is the correct half and the signature is the misleading one.
The fix for this file is to write add : (int, int) -> int. Worth sweeping the
rest of the ML corpus for the same shape when the check lands.
Scope: a gap the branch narrowed, not one it opened
signature_mismatch is new on enforce-inferable-annotations — main has no
such function, so on main BOTH directions were accepted silently. The branch
closed the flat-signature direction. This issue is the remaining half, filed
separately rather than bolted onto the branch at push time because closing it
changes at least one corpus program and invalidates in-flight corpus runs.
Suggested direction
- Extend
signature_mismatch
(crates/osprey-syntax/src/ml/lower.rs) so a curried signature spine longer
than a flat binding's parameter list is rejected, with the mirror message:
name the binding form the signature implies.
- Fix
functional_showcase.test.ospml:17 to (int, int) -> int and sweep the
ML corpus for other curried-signature/flat-binding pairs.
- Add a rejection case under
examples/failscompilation/ for the newly
rejected direction, so both directions are pinned by a program, not only by
a unit test.
Acceptance
- All four rows above are decided consistently: the two matching combinations
compile, the two mismatched ones are rejected with a message naming the
binding form the signature requires.
- No ML corpus program carries a signature whose arity disagrees with its
binding.
Summary
ML signature/binding arity is graded in one direction only. A parenthesised
(flat) signature domain enforces a flat binding, but a curried signature does
NOT enforce a curried binding — so a written
int -> int -> intcan silentlydescribe a function that lowers flat, and the author gets no diagnostic.
Reproduction
Four combinations,
osprey s.ospml --check:add : int -> int -> intadd (a, b) = …add : int -> int -> intadd a b = …add : (int, int) -> intadd (a, b) = …add : (int, int) -> intadd a b = …The rejection reads:
Row 1 is the gap: it is the mirror image of row 4 and is accepted in silence.
Why row 1 is a mismatch
docs/specs/0024-MLFlavorSyntax.mdmakes the two forms distinct lowerings, notspellings of one thing:
[FLAVOR-ML-CURRY](line 74): "Whitespace parameters curry.add x y = bodylowers to a one-parameter
Stmt::Functionwhose body is a one-parameterExpr::Lambda."flat binding lowers to one two-parameter
Stmt::Function; the call lowers toone two-argument
Expr::Call."So
int -> int -> intdescribes the curried lowering andadd (a, b)producesthe flat one. Row 4 is rejected for exactly this reason; row 1 is the same
disagreement with the operands swapped.
The corpus already contains one
tests/regressions/basics/functional/functional_showcase.test.ospml:17:Its Default twin declares
fn add(a, b)— flat — and the twins emit identicalIR, so the BINDING is the correct half and the signature is the misleading one.
The fix for this file is to write
add : (int, int) -> int. Worth sweeping therest of the ML corpus for the same shape when the check lands.
Scope: a gap the branch narrowed, not one it opened
signature_mismatchis new onenforce-inferable-annotations—mainhas nosuch function, so on
mainBOTH directions were accepted silently. The branchclosed the flat-signature direction. This issue is the remaining half, filed
separately rather than bolted onto the branch at push time because closing it
changes at least one corpus program and invalidates in-flight corpus runs.
Suggested direction
signature_mismatch(
crates/osprey-syntax/src/ml/lower.rs) so a curried signature spine longerthan a flat binding's parameter list is rejected, with the mirror message:
name the binding form the signature implies.
functional_showcase.test.ospml:17to(int, int) -> intand sweep theML corpus for other curried-signature/flat-binding pairs.
examples/failscompilation/for the newlyrejected direction, so both directions are pinned by a program, not only by
a unit test.
Acceptance
compile, the two mismatched ones are rejected with a message naming the
binding form the signature requires.
binding.