Issue #497: Decide: the checker stays silent about a type it does not know (Part III C.4) - is that right? -> no

compiler, note · opened 2026-10-06 · updated 2026-10-10 · 7 comments

What it is. Part III C.4 says: A message appears only where both sides are written down. Where a type is not known, such as a method on a receiver std has no signature for, or what a ? unwraps, the compiler says nothing, which is not the same as approving. The checker never rejects a program that is correct. ADR-286 D34 (it fails open) and ADR-010 D1’s polarity are the same idea applied elsewhere.

What a program sees today. Where the checker says nothing, the program is lowered to Rust, and rustc’s refusal reaches the user in rustc’s words. ADR-005 D7 maps it to the .nika line, but it is still about a file nobody wrote (Part III C.1). This session alone found five such cases:

a mixed integer comparison, push and a generic T (#482, now fixed);
Bytes::to_text (#489);
return ref (#442);
nowhere::wobble (#488).

Where the question comes from. The owner, in the decision round on #488 (6 Oct): the silence for types the checker does not know is questionable and should be looked at closely. Nothing is blocked. But every silence is a place where a defect reaches the user as a backend message.

A decision basis is owed before this is asked:

Inventory: every place in check/mod.rs that returns unknown and stays silent, grouped by cause:
- no ledger signature;
- an unresolved method;
- a ?;
- a generic;
- a type the checker cannot work out;
- others.
Measurement: of the programs in tests/errors and the examples, how many end in a rustc refusal, and from which group.
How others do it:
- Rust and Swift: a name or type that cannot be resolved is always an error;
- TypeScript strict: no implicit any;
- mypy: --strict vs gradual typing.
Options, each with what goes wrong if it is wrong:
- keep failing open;
- fail closed (an unknown type is an error that names what is missing, e.g. a ledger entry);
- fail closed per group, where the cause is a gap of this compiler rather than of the program;
- a warning in between.
Recommendation, after the measurement.

Comments

keywan-ghadami, 2026-10-06

Measured: refuse every unknown type, and see what breaks (6 Oct)

The owner’s direction: refuse, and look at what breaks. Hard-coded on a local branch and not pushed. The patch is kept by the deciding session.

What was changed. In Checker::expr, every expression whose type comes out Ty::Unknown became an error. Three things were left out:

an integer or float literal, and an open number (ADR-285 D23), which are typed later by their uses;
structural expressions (+, if, block, match, return, throw, catch, range, break, continue), which are only unknown because a part is;
an expression with an unknown part that was already reported (a cascade).

So each count is a root cause. Only a top-level Unknown was counted; an unknown inside a type (Vec[?]) was not.

Corpus:

every .nika under examples, tests, benches and the test fixtures: 62 files, 59 of them clean before;
std’s Nikaia half (nikaia lower-std).

Result

	Programs (62 files)	`std` tools (80 files)
Root causes	139 distinct (187 with repeats)	120 distinct
Programs clean before that now fail	24 of 59	lower-std would stop at the first
Real program errors found	0	0

By cause (programs + std):

Cause	Programs	std	Kind
A grammar’s bindings (`s:until(…)`, `t:term`) and what is computed from them	~42	~94	checker limit: a grammar binding gets no type
`std` paths the ledger does not type: `fs::Root::Anywhere`, `http::Method::Post`, a constructor as a value (`Summary`)	20	2	ledger gap
The error bound in a `catch` (`f"{error}"`)	20	-	checker limit
A float `let` typed by its use (`let mut px = 0.0`), and indexes into a list of them	~15	-	checker limit: open floats are not tracked like open integers
`x.parse()` typed by the annotation (`let n: i32 = …`)	7	-	checker limit: result typed by use
A lambda’s parameters (`fn(acc, m)`, `fn (row)`)	~7	-	checker limit
A `dsl` block’s result and its fields	~9	-	checker limit
Function values passed as arguments (`holes_of`, `name_is`), `match` on such a call	-	~14	checker limit
Methods with no signature: `sort_by_key`, `as_str`, `is_some`	5	-	ledger gap
`html::escape`, `hyper_shim::serve_once` (foreign)	5	-	ledger gap / foreign
`panic(…)`	2	-	checker limit: no never type
loop counters, others	a few	~10	mixed

What it says

Today, failing closed would break 24 of 59 working programs and most of std’s Nikaia half, and it would find no program error.
Almost all of it is the checker’s own blind spots, not the programs’:
- grammar bindings (by far the largest group);
- catch bindings;
- lambda parameters;
- open floats;
- typing by use (parse);
- dsl results;
- function values;
- the never type.
Each is a gap that can be closed: the type is knowable in every one of these cases.
The ledger gaps are a smaller group (about 30): std enum variants and constructors used as values, and a few methods.

So the useful order is to close the gaps first, then turn on failing closed. The five cases found today that rustc reported were all in places where the checker did know the types and simply did not ask (#482, #489, #442, #488). They are a different class from this one.

Possible next decisions (for the owner)

Fail closed as the goal: C.4 changes once the gaps are closed.
Close the gaps in order of size:
- grammar bindings;
- catch;
- lambda parameters and function values;
- open floats;
- typing by use;
- dsl results;
- never type;
- ledger entries.
Each is a build issue.
Measure again after each one with the same patch; switch on failing closed when the count of programs that were clean before reaches 0.

Generated by Claude Code

keywan-ghadami, 2026-10-07

Decided (owner, 7 Oct): failing closed is the goal; the gaps are closed first, one issue per kind

Goal: the checker refuses an expression whose type it does not know. C.4’s says nothing is changed in the specification when the switch is turned on, not now.
Order: one build issue per kind of gap, linked below. Re-measure after each with the patch below. Turn on failing closed when no program that was clean before breaks; that step gets its own decision round (ADR + C.4).
This issue stays open as the tracker, labelled note.

The measuring patch (apply on a local branch; never push)

Measure: nikaia lower every .nika under examples tests benches crates/nikaia/tests, then nikaia lower-std, and count NK9999 / STRICTSTD lines.

--- a/crates/nikaia/src/check/mod.rs  (in Checker::expr)
         self.reached = self.reaching.take();
+        let strict_before = self.checked.findings.iter().filter(|f| f.code == "NK9999").count();
         let ty = self.value_of(expr, span);
+        let strict_cascade =
+            self.checked.findings.iter().filter(|f| f.code == "NK9999").count() > strict_before;
 …
             self.a_value_with_a_cleanup_made(&ty);
         }
+        let open_literal = matches!(expr, Expr::LitInt { .. } | Expr::LitFloat(_))
+            || matches!(expr, Expr::MethodCall { receiver, .. } if matches!(**receiver, Expr::LitInt { .. }));
+        let open_number = match expr {
+            Expr::Variable(name) => self.binding(self.parsed.text(*name)).is_some_and(|l| l.open_number.is_some()),
+            _ => false,
+        };
+        let structural = matches!(expr, Expr::Binary { .. } | Expr::Unary { .. } | Expr::If { .. } | Expr::Block(_)
+            | Expr::Match { .. } | Expr::Return(_) | Expr::Throw(_) | Expr::TryCatch { .. } | Expr::Range { .. }
+            | Expr::Continue | Expr::Break);
+        if matches!(ty, Ty::Unknown) && !open_literal && !open_number && !strict_cascade && !structural {
+            let kind: String = format!("{expr:?}").chars().take_while(|c| c.is_alphanumeric()).collect();
+            self.checked.findings.push(Finding { severity: Severity::Error, span: *span, code: "NK9999",
+                message: format!("STRICT unknown type: {kind}"), notes: Vec::new(), help: None, labels: Vec::new() });
+        }
         ty
--- a/crates/nikaia/src/sysroot.rs  (in lower_tools_at, before `let refusals`)
+        let source_text = std::fs::read_to_string(&path).unwrap_or_default();
+        for f in checked.findings.iter().filter(|f| f.code == "NK9999") {
+            let line_no = source_text[..f.span.at().min(source_text.len())].matches('\n').count() + 1;
+            eprintln!("STRICTSTD\t{}\t{}\t{}", path.display(), f.message, line_no);
+        }
   … and `.filter(|f| f.code != "NK9999")` on `refusals`.

The full version adds the method, field or callee name to the message. It is kept in the deciding session’s scratchpad, which is temporary.

Generated by Claude Code

keywan-ghadami, 2026-10-07

The gaps, one build issue per kind, largest first:

#500 grammar bindings
#501 the catch binding
#502 lambda parameters and function values
#503 open floats
#504 a result typed by its use (parse)
#505 a dsl block’s result
#506 panic as never
#507 ledger gaps

Re-measure after each one with the patch above.

Generated by Claude Code

keywan-ghadami, 2026-10-07

Re-measured after 0.0.611 (d85751e)

Same patch as above, with the callee/field/method name in the message. Every .nika under examples tests benches crates/nikaia/tests was lowered with nikaia lower --no-cache (62 files). std’s half was not re-measured this round (it needs the sysroot.rs half of the patch).

Built since the first measurement: #506 (panic is never), #501 (the catch binding), #503 (a float literal is f64), #505 step 1 (dsl html is a String), #507 step 1 (fs::Root::Anywhere is an fs::Root). #488 also landed (a call through an unknown head is NK1181).

	before (6 Oct)	now
Root causes in the programs	139 distinct (187 with repeats)	102 distinct (115 with repeats)
Programs clean before that the patch breaks	24 of 59	21

What is left, by cause (with repeats):

Cause	Count	Issue
A grammar’s bindings and what is computed from them (`calc` 23, `json` 16, `k-nucleotide`, `report`, `inventory/stock`)	~70	#500
`.parse()`: not in the language at all	6	#504, now `decision`
A list literal of integers (`trend`: `readings[day]`, `before`, `after`, `average`)	10	#513, new: it was counted under floats, but `trend`’s readings are integers
Lambda parameters and `sort_by_key`	~6	#502
A constructor or method as a value (`Summary`, `Summary::merge`, `Report::merge`)	5	#507 step 2
`hyper_shim::serve_once` (`overlaps.nika`, which is now `NK1181` anyway: a loose file naming a crate it does not declare)	4	#507 step 4
`dsl mysql` result and `bound.id`, `bound.active`	3	#505 step 2 / #114
`is_some`, `as_str` on text: Rust methods, not Nikaia ones	2	#507 step 3
`html::escape` (ledger says `-> ?`)	1	#507 step 4
`http::Method::Post`	1	#507 step 1: a case of a type the shipped ledger does not list
`call panic`	2	not a gap: since #506 a `panic(…)` is a jump, so the patch should count it with `return` (structural); it does not yet

For the next measurement: add Expr::Call to panic to the patch’s structural list. Measure std again with the sysroot.rs half.

Generated by Claude Code

keywan-ghadami, 2026-10-07

Re-measured after 0.0.624 (f3e3184)

Method as before: 62 files, nikaia lower --no-cache, programs only (not std). One change to the patch: a panic(…) call counts as structural, because it has been a jump since #506.

	6 Oct	after 0.0.611	now
Root causes (distinct)	139	102	47
with repeats	187	115	57
Programs clean before that the patch breaks	24	21	18

What is left, by cause:

Cause	Count	Issue
`.parse()`: not in the language	6	#504 (`decision`)
A list literal of integers (`trend`)	7	#513 (`decision`)
A tuple pattern’s parts in a `match` arm (`calc` `n`, `json` `n`)	3	#522, new
An empty list filled by `push` (`k-nucleotide` `row`)	4	#523, new
A `dsl html` `<for>` name (`r`, `e`)	4	#524, new
`overlaps.nika`: a loose file naming a crate it does not declare	8	none: it is `NK1181` since #488
`measurements` fixture (`Summary` is Rust-side, `is_some`)	4	fixture, plus #507 step 3 (`decision`)
`sql_statement` fixture (`args`, `query`, `bound.id`, `bound.active`, the `dsl mysql` block)	5	#114 / #505 (`blocked`)
`http::Method::Post`	1	a package’s type, read without the package
`as_str` (`k-nucleotide`)	1	#507 step 3 (`decision`)

sort_by_key (3 root causes) was fixed in 0.0.624: the ledger said -> ?.

What is left is almost all decisions (#504, #513, #507) and three small build issues (#522-#524). After those, the only failures are the fixtures and the deliberately unbuildable overlaps.nika. That is the point where the switch to failing closed can be prepared for its decision round.

Generated by Claude Code

keywan-ghadami, 2026-10-10

Re-measured after 0.0.737 (programs and `std`)

Same patch as above, with three changes:

an open number now includes an element of a literal list (#513) and an integer comptime without a type (ADR-287 D21);
a panic(…) counts as a jump.

How it was counted. The corpus has grown to 152 files (examples tests benches crates/nikaia/tests, nikaia lower --no-cache per file). A file of a project is lowered with its project, so a count per file repeats the project’s hits. The numbers below are distinct source locations. std’s half was measured with the sysroot.rs half of the patch.

The 0.0.734 row is a full run. The 0.0.737 row re-lowered the files that still had hits at 0.0.735, plus all of std. Every change in between only gives a type to something that had none.

	6 Oct	0.0.624	0.0.731 (#513 in)	0.0.734	0.0.737
Programs, distinct root causes	139	47 (62 files)	62	48	27
of which gaps of the checker					10
`std`’s Nikaia half	120	not measured		14	0

Built in this round

#504: text::parse_<T> (0.0.733).
#509 and #507: NK1171 for a member a known type does not have (0.0.734). The corpus run behind it found:
- one Rust habit, k-nucleotide’s as_str;
- five entries std lacked: Vec::first, Vec::last, HashMap::clear, io::IoError::message and io::IoError::full.
#512: the handler’s error where several error types arrive (0.0.734).
0.0.735-0.0.737: the kinds the measurement showed. Each is a type written down nearby:
- an if/match of numbers is an open number (a branch that leaves is no value), and an if of a typed number and a literal is the typed one;
- for k in 0..<n over literals, and for x in a literal list, bind the open number;
- a bare pattern name binds the matched value, and a pattern inside a pattern binds from its part’s type;
- a lambda returned, put in a field or bound by an annotated let takes the declared fn type;
- a field read through Shared is the held value’s field;
- a grammar binds dec[f64](…) as an f64, and a choice of rules that agree as their type.

What is left (27)

Not a gap of the checker (17):

Where	Count	Why
`examples/foreign-runtime/overlaps.nika`	8	a loose file naming a crate it does not declare; `NK1181` since #488
`sql_statement` fixture	5	`dsl mysql` rows: #114 / #505 (`blocked`)
`measurements` fixture	3	`Summary` is Rust-side
`hello-http`: `http::Method::Post`	1	a package’s type, read without the package

Gaps (10):

Kind	Count	Where	What it needs
A literal list’s element through `iter`, `zip`, `windows` and the lambda over a window	4	`trend`	the open element carried through the sequence methods’ `$T`; the checker has no type for an open number to bind `$T` to, so this needs more than a local fix
A map whose value comes from an open literal written by index: `let mut m = collections::HashMap()`, `m["a"] = 7`	2	`coalescing`	ADR-285 D34 for a map’s values. D34 says it for a literal list, so this needs a decision or a sentence in D34
A `dsl` parameter list `...args: Self::dsl`	2	`dsl_parameters`	the driver’s parameter type (ADR-299)
`field.of(value)` over `T::fields` in a generic body	1	`reflection`	the type differs per field; it is known per unrolling. Not a gap: the patch should count it as structural
`error.message` (a field, no parentheses) where the error is a `?`	1	`supervision`	`supervisor::run` throws `?` (the box), which C.4 leaves unknown by design; the test probably means `message()`

Found on the way: reduce (Part I 5.3, numbers.reduce(0) fn(acc, n) { … }) is in no ledger and is lowered as Rust’s reduce, which does not exist. Since 0.0.734 it is NK1171, where before it was a backend error.

The two that need the owner:
- D34 for a map’s values;
- whether a ? error (the box) stays unknown under failing closed.
Building:
- trend’s element flow, which needs an open number that can stand where a type variable is bound;
- the dsl parameters.
The switch to failing closed then gets its decision round (ADR + C.4), with the fixtures and overlaps.nika as the known exceptions.

Generated by Claude Code

keywan-ghadami, 2026-10-10

develop is green again under failing closed (0.0.739-0.0.741)

After c723cb8 (0.0.738, NK1245 switched on), cargo test --workspace --release had 72 failing tests. Three commits fixed them forward. CI run 765 on 52903c9 (0.0.741) passed.

Commit	Failing tests (nikaia package)
c723cb8 0.0.738	72
28b96c0 0.0.739	52
8fecfa3 0.0.740	19
52903c9 0.0.741	0 (whole workspace)

Now typed (the checker knows the type)

A method of a generic type of the program’s own binds T from the receiver: h.seen() on a Holder[i64].
Vec() whose first push is a number holds one open number (ADR-285 D34).
x ?? "none" over a T? whose T nothing typed has the fallback’s type.
A lambda in a list of a declared fn type takes that type.
A dsl statement with :name holes is its text.
full() on a type with impl Error.
Seen[T] answers T’s methods.
A type seen through (deref: fs::Mapped, Shared) answers methods and indexes with what it holds.
A package’s enum case is a value of the enum (http::Method::Post).
A dependency’s files are checked against what that package itself reaches, under its own name for it (c::Id where this build calls the package deep).

Not refused where they stand (ADR-286 D41, Part III C.4)

The owner should look at these. Each is a place where NK1245 is not said, rather than a gap closed:

NK1245 waits for the other refusals. Where a file holds any other error, NK1245 is dropped. Usually its unknown type is that error’s leftover.
A name is asked where it is bound, not where it is read. This covers a let, a loop, a lambda parameter and a spread, and also a member of a name bound without a type.
- Risk: an untyped lambda parameter (fn(x) { x + 1 } in a place that declares no type) is no longer refused at x. Only the lambda value is refused, and only where it is not passed directly to a callee.
What an open number passes through is open:
- hand(7);
- Holder { value: 21 }.value;
- a task’s join();
- an index or member of a value whose type argument is still ?;
- xs ?? 0 and xs ?? return over a T? nothing typed.
Risk: rx.recv() ?? return over a channel of a struct nothing typed is silent too. The channel’s element type is not inferred from send.
Left to a later refusal or another build:
- asset("…") takes its comptime’s type;
- a DSL driver’s Self::dsl is a type of each call site;
- a call through a package whose ledger this build does not read is left to that package’s own build;
- dsl markdown {…} and a missing grammar entry are refused by the lowering, which names what is missing.

Tests and examples changed

typecheck::a_field_of_an_unknown_type_says_nothing is now …_is_refused: it expects NK1245.
The “fine” program in lambdas.rs read .id of an i64; it now reads it of a Row.
run_names_the_file needed a program the checker passes and rustc refuses. It now uses u8 << 9.
tests/language/src/kept_functions.nika used Rust’s Duration::from_millis; it now uses 1.millis().
Three specification blocks rustc refused are now NK1245: Part I 4.3, 4.7 and 9.1. They are fragments that use a User declared elsewhere, or an http::read the package does not have. EXPECTED.txt, COMPILES.txt and the floor (60 to 57) follow.
Already red before NK1245, and fixed on the way: a clippy question_mark lint on std::text and a clone_on_copy lint in check/mod.rs.

Still open from this issue

Channels: the element type should come from send, so rx.recv() gets a real type instead of item 3’s exemption.
Untyped lambda parameters (risk in item 2).
D34 for a map’s values.

Generated by Claude Code

Back to Open Issues

Issue #497: Decide: the checker stays silent about a type it does not know (Part III C.4) - is that right? -> no

Comments

keywan-ghadami, 2026-10-06

Measured: refuse every unknown type, and see what breaks (6 Oct)

Result

What it says

Possible next decisions (for the owner)

keywan-ghadami, 2026-10-07

Decided (owner, 7 Oct): failing closed is the goal; the gaps are closed first, one issue per kind

The measuring patch (apply on a local branch; never push)

keywan-ghadami, 2026-10-07

keywan-ghadami, 2026-10-07

Re-measured after 0.0.611 (d85751e)

keywan-ghadami, 2026-10-07

Re-measured after 0.0.624 (f3e3184)

keywan-ghadami, 2026-10-10

Re-measured after 0.0.737 (programs and std)

Built in this round

What is left (27)

Next

keywan-ghadami, 2026-10-10

develop is green again under failing closed (0.0.739-0.0.741)

Now typed (the checker knows the type)

Not refused where they stand (ADR-286 D41, Part III C.4)

Tests and examples changed

Still open from this issue

Re-measured after 0.0.737 (programs and `std`)