check: `?` in a body whose result type is inferred #747

New issue

Open

opened 2026-11-13 12:39:36 +00:00 by orion · 0 comments

orion commented

2026-11-13 12:39:36 +00:00

Collaborator

Context

docs/TYPECHECKER.md section 9 (spec gaps) records a hole and leaves it open: a function without a written result type whose body applies ?, such as fn probe() { read()? }, is accepted with the result Void. The ? has nowhere to return the error to, and no issue tracks the hole.

Source

Cleanup audit 2026-11 (#742), finding F7; the report is docs/project/2026-11-cleanup-audit.md.
docs/TYPECHECKER.md section 9, the gap on a body whose result is inferred.

Goal

One rule, decided in the spec gap and enforced: ? in a body whose result type is inferred is refused with a message that asks for the result type (the recommendation of the audit: inferring a Result from a ? hides the error type from the signature, which CONCEPT's rule on written signatures of public functions argues against), or the result is inferred as the record of the gap decides.

Design record point

docs/TYPECHECKER.md section 9; CONCEPT, the section on ? and on inferred result types.

Acceptance criteria

The spec gap carries a _Decision: line with the rule
Checker tests pin the rule for a function, a method and a closure body, with the message
fn probe() { read()? } no longer type checks as Void
The four gates and the fixpoint are green

Dependencies

None.

Seed

None, unless the compiler's own source relies on the hole; then the source is fixed in the same PR (the seed reads both).

Size

One PR, one commit.

## Context `docs/TYPECHECKER.md` section 9 (spec gaps) records a hole and leaves it open: a function without a written result type whose body applies `?`, such as `fn probe() { read()? }`, is accepted with the result `Void`. The `?` has nowhere to return the error to, and no issue tracks the hole. ## Source - Cleanup audit 2026-11 (#742), finding F7; the report is `docs/project/2026-11-cleanup-audit.md`. - `docs/TYPECHECKER.md` section 9, the gap on a body whose result is inferred. ## Goal One rule, decided in the spec gap and enforced: `?` in a body whose result type is inferred is refused with a message that asks for the result type (the recommendation of the audit: inferring a `Result` from a `?` hides the error type from the signature, which CONCEPT's rule on written signatures of public functions argues against), or the result is inferred as the record of the gap decides. ## Design record point `docs/TYPECHECKER.md` section 9; CONCEPT, the section on `?` and on inferred result types. ## Acceptance criteria - [ ] The spec gap carries a `_Decision:` line with the rule - [ ] Checker tests pin the rule for a function, a method and a closure body, with the message - [ ] `fn probe() { read()? }` no longer type checks as `Void` - [ ] The four gates and the fixpoint are green ## Dependencies None. ## Seed None, unless the compiler's own source relies on the hole; then the source is fixed in the same PR (the seed reads both). ## Size One PR, one commit.

orion added the

loop

label

2026-11-13 12:39:36 +00:00

orion referenced this issue

2026-11-13 12:41:38 +00:00

cleanup: 2026-11 audit plan (epic) #742