T? Is Not null Makes It a TStatus: Accepted
Date: October 14, 2026
Answers: whether x != null before a use changes what x is at the use
Related:
ADR-140 (one spelling for one thing);
ADR-305 (the backend’s edition);
Part I 2.3, 3.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. Until now that held after x != null too: the test was a bool
like any other, and the program wrote (x ?? 0) > 3 beside a test that had
already ruled the fallback out.
A condition that proves a local or a parameter 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
(Part II), 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.Nothing else proves: || over a test that does not say null proves
nothing, nor does a test of another name.
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.
A field path (a.b != null) and the binding of an enum’s value in a
condition are not decided here. A field may be changed through another
name, or by a call between test and use, so proving it needs what the
compiler knows about who can write it; an enum’s value is bound by match
today. Each needs its own record.
A: nothing changes. x != null stays a bool, and every use writes
?? with a fallback that cannot run. It asks the author to repeat what the
compiler can see, and the fallback is dead code that reads as if it mattered.
C: a binding in the condition, if let v = x { … } or if x is v. It is a
second spelling of a match arm over a T? (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.