T? Is Not null Makes It a T - for a Name and for a Path of Fields from ItStatus: Accepted
Date: October 27, 2026
History: the record this one replaces is archived in docs/history/adr; read it only for how the decision was reached
Answers: whether x != null before a use changes what x is at the use,
and the question the replaced record left open: whether the same holds for a
field (if self.f != null { self.f.len() }) and for the value an enum holds
Related:
ADR-140 (one spelling for one thing);
ADR-258 (the four weights);
ADR-281 (a lock’s value is reached only through its doors);
ADR-305 (the backend’s edition);
ADR-306 D17 (a field is a name of the walk while nothing can change it);
ADR-352;
Part I 2.3, 3.5, 6.5; Part III 17.1
Is x a T after a test proved it is not null? T? is a type of its
own with none of T’s operators (Part I 2.3), so x > 3 over an i64? is
NK1102. Without a rule the test is a bool like any other, and the program
writes (x ?? 0) > 3 beside a test that has already ruled the fallback out.
And for a field? Most T? a program tests are fields: self.cache,
node.next, p.name. if p.name != null { p.name.len() } is NK1125 until
this record, and a program writes let n = p.name first, a second name for a
value that already has one. Rust code moving into Nikaia (if let Some(x) =
&self.f) meets this on nearly every page.
| Language / tool | Its answer | What it costs there | Source |
|---|---|---|---|
| Kotlin | smart cast of a local, and of a val property without a custom getter declared in the same module; never of a var property |
a var field needs ?.let { } or a local copy: another thread or an alias may write it between test and use |
Kotlin docs, Type checks and casts (from memory, not checked) |
| TypeScript | narrows property paths (a.b.c); an assignment to the path or a prefix resets it, a call does not |
unsound: a call that writes the field through an alias keeps the narrowed type | TypeScript handbook, Narrowing (from memory, not checked) |
| Swift | no narrowing; if let x = self.f, guard let, binding a new name |
a second name for every test; the original stays optional | Swift book, Optional Binding (from memory, not checked) |
| Rust | no narrowing; if let Some(x) = &self.f, the borrow checker forbids a write to self.f while x lives |
a binding per test; the borrow rules do the proving | Rust reference, if let |
What does not transfer. Kotlin’s refusal of a var field is about the
JVM: any other reference to the object, in any thread, may write it at any
time. A Nikaia value has one owner, a mut view is exclusive, a shared value
is reached only through a lock’s doors under a name of its own (ADR-281), and
a task sees only what is moved or shared into it. So what can write a field
between test and use is visible in the function itself: a write to the path,
or a mut hand-over of it. That is the reason TypeScript’s syntax can be
had here with Rust’s soundness.
A: nothing changes. Every use writes ?? with a fallback that cannot run.
if x != null { use((x ?? 0) + 1) }B: names only. A local or a parameter narrows; a field is copied first.
let name = p.name
if name != null { print(name.len()) }C: names and paths of fields from them; the proof ends at what can write the path.
if p.name != null { print(p.name.len()) }D: as C, but every call ends a path’s proof (Kotlin’s line, made stricter).
if p.name != null { log("x"); print(p.name.len()) } // NK1102 under DE: a binding in the condition, if let v = x { … } or if x is v.
if let name = p.name { print(name.len()) }| Option | D1 the special case pays | D2 compiler works | D3 no cost common case | D4 consistent | If it is wrong |
|---|---|---|---|---|---|
| A | no: every test pays a dead fallback | no | no | yes | dead code reads as if it mattered |
| B | the field pays a copy | for names | names yes, fields no | no: a field is a name for ADR-306 D17 but not here | one let too many per field |
| C | yes: only a path with a write in between loses the proof | yes: the walk ADR-306 D17 already runs | yes | yes: the same path rule as D17 | NK1102 naming the write; the program adds a let |
| D | no: an unrelated log call ends the proof |
yes | no: most bodies call something | no: D17 keeps a fact across a ref call |
noise refusals |
| E | no: a second name per test | yes | no | no: a second spelling of a match arm (ADR-140); covers neither \|\| nor an early exit |
two ways to say one thing |
C is chosen.
A condition that proves a local, a parameter, or a path of fields from one
(D4) is not null makes it a T wherever that proof holds, and only there.
Elsewhere it is the T? it was declared, and an operator of T over it is
NK1102.
Why. Nikaia proves what it can rather than check it at run time or leave
it to the author: an index the compiler proves in bounds is not checked
(ADR-306), a division by a divisor proved not zero is not guarded. A test
x != null is the same kind of knowledge, stated by the program itself. Where
the compiler sees it, the code after it cannot meet null, so x > 3 there
is correct and refusing it is noise; where it cannot see it, the refusal
stays. Internally the name has another type at that point, which is all the
rule is: the type follows what is proved.
a && b: what a proves holds in b and in the branch the whole
condition leads into. if x != null && x > 3 { … }: the right operand and
the body see T; the else branch keeps T?.a || b: what a proves false holds in b; the whole proves for the
else branch what both sides prove false. if x == null || x > 3 reads
x as T on the right; if x == null { … } else { … }: the else sees
T.!a swaps the two.if x == null { return } (or break, continue,
throw), x is T for the rest of the block, as the block goes on only
where the test failed. The same for an else that leaves.while x != null { … }: the body sees T.match guard (#879, owner, 2026-10-27): what the guard proves
holds in that arm’s body, as for an if condition, and && inside the
guard carries its proof to its right. In (x, _) if x != null => x, x
is a T in the body. The proof reaches no other arm: the next arm is
tried exactly where the guard failed.Nothing else proves: || over a test that does not say null proves
nothing, nor does a test of another name or another path. The same places
hold for a path: if p.next == null { return } makes p.next a T for
the rest of the block.
Why. These are the places the test runs before the read on every path.
They are the ones Kotlin, TypeScript and Swift’s guard cover, and each
follows from how &&, || and a jump already run.
A name assigned between the test and a use is a T? again from the
assignment on, and a use after it that needs a T is NK1102, with a note
and a label naming the assignment. A loop opened inside the proven region that
assigns the name takes the proof back for the whole loop, since its next turn
reads the name after the write.
Why. The proof is about the value the test saw. A write puts another value
in its place, which may be null.
p.name, self.cache, a.b.c: a path that starts at a local or a parameter
(self included) and goes on through fields only is proved and taken back
like a name. Two paths are the same path when they name the same root and the
same fields in the same order.
Not a path: anything through an index (v[i].f), a call result (f().x,
m.get(k).f), or a lock’s value. The first two are computed anew at each
read, so a test of one says nothing about the next; a lock’s value is read
only inside its door (ADR-281), where the door’s own name is a local and its
paths narrow. Such a test proves nothing, and a use that needs a T is
NK1102 with a note that the read is not a path.
Why. It is the path ADR-306 D17 already calls a name for a bound or a
length; a null test is one more fact about the same path, kept by the same
walk.
A path’s proof holds until the first of:
p.name = …,
p = …);mut hand-over of the path or of a path it is part of: a method that
changes its receiver called on it (p.rename() with ref mut self), or the
path or a prefix passed as a mut argument;overlap branch or a select arm that sees the root
and may change it.An assignment to a sibling (p.age = 3 keeps p.name) and a call that only
reads (ref or a copy of the root, or a call that is not handed the root at
all) keep the proof. A loop inside the proven region that does one of these
takes the proof back for the whole loop, as D3. A use that needs a T after
it is NK1102, with a note and a label naming the write.
Why. A ref view cannot write, a mut view is exclusive, and a field
is never shared between owners, so only these can put another value at the
path between test and use. The rule is ADR-306 D17’s, so a bound and a
null fact about the same path end at the same place. A parameter the
function only borrows keeps its paths’ proofs for the whole region, as D17
keeps its facts: nothing in the body can be handed it to change.
match only.A binding in a condition, if let v = x { … }, if x is Some(v) or
if e is Leaf(v), is refused. match binds the value an enum or a T?
holds, and a T? tested with != null needs no binding (D1).
Why. It is a second spelling of a match arm (ADR-140: one thing, one
way), it adds a name for a value that already has one, and it covers neither
|| nor an early exit. This closes what the replaced record left open about
enums.
let x = self.f stays, and is needed only to keep the old value.Copying a field into a local before a test is allowed, as any let is, and
narrows the local by D1. It is needed only where the program must keep the
value across a write to the path (D5); elsewhere if self.f != null says it.
Why. A rule that made the copy necessary would repeat B’s cost; one that forbade it would forbid keeping a value.
check/narrow.rs and tools/check_narrow.nika. The
walk that ends them is the one ADR-306 D17 needs..as_ref().unwrap(), or
.as_mut().unwrap() where it is written through (#621’s form). rustc checks
the result again, so a wrong proof is a build error, never a wrong run.if let Some(x) = &self.f as
if self.f != null with x replaced by self.f, and keeps the let only
where the body writes the field (D7). The field gap
is closed.NK1102 names the write that took the proof back, or says
the read is not a path (D4); NK1125 no longer meets a field test.tests/compiler/: a path narrowed in each D2 place, a sibling
write that keeps it, a ref mut self call and an assignment to a prefix that
end it, v[i].f that does not narrow, and a refused if let.A path through an index whose index is itself proved unchanged (v[i].f
with v and i not written) is left out; it may join D4 when a program
needs it.