Status: Accepted Related: ADR-020 (the ledger this reads), ADR-300 (the spans D7 waits on), ADR-014 (every module it moves makes this checker stronger without changing it), ADR-296 D17 (name for name, applied to types)
Nikaia has checked one of its own rules since ADR-020: Part II 12.1, that a sync function may
only call sync functions. Types it did not check. They were checked by rustc, after the
lowering, in Rust’s vocabulary, about a file the programmer did not write.
ADR-300 already places those messages back on the .nika line they came from, and the placement
is exact — the lowering is name for name, so only the position was ever wrong. But the text is
still Rust’s. A .nika file that puts a literal in a String field is told about
expected String, found &str`` by a compiler the programmer did not invoke, and Part III C.1’s
Iron Rule (“an untranslated backend error reaching the user is a Nikaia compiler bug”) says that
is a bug. The NK1xxx range — Syntax & types — was the only one in the catalogue with no
entries at all.
The thing standing in the way was never the algorithm. It was that Stage 0 cannot see most of
the types involved. Half of std is still Rust (ADR-014), and a Nikaia program calls push_str,
entry, map_or, chars and nth freely. A checker that had to have an opinion about those
would need either a second frontend that reads Rust, or a guess.
A type checker that guesses is worse than none. It reports errors that are not there, and the first one teaches the person reading it that the tool is to be worked around rather than believed.
Unknown is part of the type language, and it is not a type.contracts::ty::Ty is ast::Type with one addition and one subtraction. The subtraction is the
interner: a ledger is a file, so a type is text, and two types are the same when they are written
the same — name-for-name (ADR-296 D17) applied to types.
The addition is Unknown, written ?, which is the absence of a claim. It is what the
compiler records where it has nothing to say: the result of a method on a receiver it cannot
resolve, of ?, of ??, of an index, of a DSL block, of a generic parameter, of a function
whose ledger entry has no signature.
Unknown is compatible with everything, in both directions. Every rule in the checker has the
same shape: infer both sides, compare, and say nothing unless both are written down.
The consequence is the promise the tool is worth running for:
It never rejects a program that is correct.
It does not catch every program that is wrong, and that is stated rather than implied. What it catches is a function of how much is written down — a number that goes up as ADR-014 proceeds, without the checker changing.
Changed by ADR-251 D4: the ledger spells a signature as Nikaia source does — ref self, ref T, [T](x: T) — not in the & spelling below.
Part III 13.5’s ledger already recorded what a caller must know about a body it cannot see:
sync, throws, and what a result may point into. It gains two keys:
[fn."Stats::add"]
sync = true
signature = "(&Stats, temp: i32)"
[type."Reading"]
pub = true
fields = ["name: &str", "temp: i32"]One mechanism, three sources, in the order a call resolves: this unit’s own contracts, inferred
from the source being compiled; std’s, shipped in std.contracts; and a package’s, which
Part III 13.5 already says a package ships. Nothing about the checker changes when the third
arrives.
A signature is one key rather than two because a person reads a function as one fact, and
because a method’s receiver belongs in it: (&Stats, temp: i32) puts self first, so a caller
reads the arguments off the same list either way.
? where nothing binds it.Changed by ADR-295 D1-D2 and ADR-251 D4: the
parameter is no longer erased; it is written in the ledger and bound at each
call. What this decision protected - no false “i32 is not T” - holds by
binding instead of by erasure.
T is a name that stands for a type rather than being one, and the checker
never reports a value as “not T”. The ledger writes the parameter as the
source does, fn first[T](xs: T) -> T as [T](xs: T) -> T. At a call, T
is a variable bound from the arguments, so first(1) is checked as an i32;
a variable nothing binds is ? and fits anything, so a gap in the binding is
never a refusal. Self in a trait’s method stands for a type no call site
binds, so there it stays ?; on an impl’s own methods the ledger writes the
type the impl is on.
&str, and this is a divergence from Part I 2.4.Changed by ADR-282 D3: a text literal is a String wherever the use asks for one (an annotated let, a field, an argument, a return, beside other String text), and a view everywhere else.
Changed by ADR-309 D2: an f"…" literal is always a String; a plain "…" is a view unless its use asks for a String.
A literal with nothing asking for a String is a view of static text, and the checker says so.
Part I 2.4 says the opposite in a passing remark — let name = "Nikaia" // Compiler knows this is
a String — and 2.3 writes let strictly_string: String = "Hello". Part I 6.6 says something
incompatible with both, and says it about the language’s central performance promise:
Owned — a
Stringof its own — one allocation, only where you wrote.to_owned().
A literal that is a String allocates at every mention, in a language whose whole claim about
large inputs is that it does not. The two spec passages are a remark inside a type-inference
example; the third is the reason 1brc.nika runs in the time it does. The literal is a
view. Part I 2.3 and 2.4 are corrected here, and a String is made where somebody wrote that
they wanted one — which is ADR-013 D7’s rule, applied to the most common conversion there is.
3 is Unknown, not i32. Committing a literal to one numeric type would make add(3) an
error wherever the parameter is not that one — a false positive on the most ordinary line
there is. This is what the language below does too, and it is the one place the checker is
deliberately less precise than it could be.
Expression-level spans are open work in the parser, and the sync check has reported at
statement granularity since ADR-020 for the same reason. A caret on the right line is worth
having; the day expressions carry spans, both checks get narrower without either changing.
rule MEASUREMENT -> Reading = … -> { Reading { name, temp } } declares what it builds, and the
action is where a struct literal is most often typed out in full — so it is where a mistyped
field name most often is. What a pattern binds has no type here: that belongs to the parser
backend and Stage 0 does not read it, so every binding is ?. The rule’s return type is written
down, and that is enough for both checks that matter in an action — the shape it builds, and the
names of the fields it fills.
?.A parameter whose Rust type is a trait bound rather than a type accepts several types, and the
ledger must say so. fs::write(path: impl AsRef<Path>, data: impl AsRef<[u8]>) takes a String,
a &str and a buffer; recording data: &str would make the checker refuse
fs::write(path, text) for a String — a correct program, rejected, which is the one thing D2
promises cannot happen.
So the rule for every entry written by hand: a concrete Rust type is recorded, a bound is
recorded ?. The arity survives either way, and the arity is the half that catches the most.
std.contracts says this where the entries are, because it is the mistake a reviewer of that
file has to look for.
crates/nikaia/tests/typecheck.rs runs the checker over every .nika file in the
repository — the eight runnable examples, fortunes.nika, and std’s own modules — and fails
if any of them produces a finding. Beside it are the deliberately-wrong programs, one per code,
which are what makes a clean corpus evidence rather than a tautology: without them, a checker
that had quietly stopped working would pass.
The NK1xxx family exists. Nine codes, each with the reproduction Part III C.3 requires:
| Code | What it says |
|---|---|
NK1101 |
a call passes the wrong number of arguments |
NK1102 |
an argument is not what the parameter takes |
NK1103 |
a let says one type and is given another |
NK1104 |
a return, or a body’s last expression, is not what was declared |
NK1105 |
an assignment is not what the target holds |
NK1106 |
a struct literal gives a field the wrong type |
NK1107 |
a field that is not there |
NK1108 |
a condition that is not a bool |
NK1109 |
a call names an option the callee does not have (Part I, 5.1) |
Every one of them names a concrete way out, as Part III C.2 requires: &str against String
suggests .to_string(), two numbers suggest as, and a field that is not there is matched
against the ones that are — with a distance that counts a swapped pair as one edit, because
nmae for name is the typo this is for and plain Levenshtein charges two for it.
The case the checker exists for is a program the backend has not compiled, checked in the language it was written in.
std.contracts carries signatures in both of its halves — inferred for the
Nikaia modules and regenerated by a test that fails on drift, written by hand
and reviewed like code for the Rust ones. The hand-written share shrinks as
ADR-014 proceeds.
Where a type does travel, it travels. A method on a known receiver is looked
up under the Type::method name the ledger records, matching the module prefix
as a suffix — name-for-name resolution as everywhere else. A for over a
Vec[Row] binds a Row; a constructor hands back the type it is on.
What it does not catch. A method on a receiver whose type is not written down. The
element type of anything but a list, and of a list iterated as pairs. What a ? or a ??
unwraps. What a match arm binds. What a grammar pattern binds. Each of these is Unknown
because a signature is missing, and each becomes checkable when one is written — which is the
property D3 was chosen for.
std, which is exactly what it cannot do. Unification also propagates a wrong
guess: one bad binding becomes several errors, in places the programmer did not write. D2’s
rule cannot do that, because it never concludes anything it was not told.std.contracts costs a line
each and is reviewable.i32. It is what the language below does for an
unconstrained literal, and it would be right about let n = 42. It would be wrong about
add(3) wherever add takes anything else, which is more lines than it would be right about.signature as “takes no arguments”. It would turn every unwritten
contract into a false NK1101. An absent key is an absent claim, exactly as an absent sync
entry is (13.5), and the two absences must not mean different things in one file.&String stand where &str is wanted. It is what the language
below does at a call, and admitting it here would make the checker’s fits a subtyping
relation with one arbitrary member. Instead, &x where x is a String is inferred as
&str — the coercion is modelled where it happens, and the comparison stays equality.