Narrowing#
Narrowing is how a union becomes one of its members inside a branch. A test proves a fact about a name or a dotted path, and that fact holds for the rest of the branch that proved it.
local function widthOf(s: string?): integer
if s then
return #s -- s is string here
end
return 0
endNarrowing tests#
Every test below ends up attached to a name or a dotted path, which is the key the checker records the fact against.
| Construct | Example |
|---|---|
| Truthiness of a name | if s then |
| Truthiness of a dotted path | if config.name then |
| Negation | if not s then ... else ... end |
| Nil comparison | if s ~= nil then |
| Discriminant field | if shape.kind == "circle" then |
is operator |
if v is Point then |
| C type test | if ffi.istype<Point>(v) then |
| Predicate call | if isPoint(v) then |
Short-circuit and |
if a and a.b then |
elseif chain |
elseif shape.kind == "square" then |
| Ternary arms | v is Point ? v.x : 0 |
| Loop condition | while node do |
| Guard clause | if not s then return end |
| Never-returning call | bail("missing") |
assert statement |
assert(s) |
Discriminant narrowing follows a copied local, so binding the tag to a new name first does not lose the fact:
local kind = shape.kind
if kind == "circle" then
print(shape.radius) -- shape is the circle arm here
endAn elseif chain subtracts as it goes, so each branch sees only what the earlier ones left. See Unions for what the checker reports when such a chain leaves a member unhandled.
assert#
assert narrows in both positions. Its signature subtracts nil from the return value, and as a bare statement it narrows its argument the way a never-returning helper does, because the builtin returns only on the truthy arm:
Being truthy, it subtracts false as well as nil, and it reads a name or a dotted path like every other test. A message argument makes no difference. It narrows only when assert is the builtin: a locally shadowed assert is an ordinary call and proves nothing.
Tests that do not narrow#
A test proves nothing when the checker cannot tie it to a stable key, or when there is nothing left for the fact to say.
type compares a string#
type(x) == "string" does not narrow, which is the limit readers hit first:
local function f(s: string | number): string
if type(s) == "string" then
return s
end
return "no"
end
-- NUPP2002: return 1: number | string is not a stringtype is an ordinary function and nothing ties its result back to s. Write s is string.
The one subject it does classify is unknown, which claims nothing a declaration could contradict: type(u) == "table" makes u a table in the branch the test holds in, type(u) ~= "string" makes it a string after the early return, and the other branch goes on knowing nothing. "function" names no type honestly and is left alone; write u as function(): nil, or the signature you mean.
The result narrows even though the argument does not, because type answers from a closed set: "nil" | "boolean" | "number" | "string" | "table" |
"function" | "thread" | "userdata" | "cdata". A comparison against a name LuaJIT never returns is caught where it is written, and a returning dispatch over the set reports the exhaustiveness lint for the names it leaves out. A guard chain whose remaining cases are handled by the code after it says so with @allow("exhaustiveness").
Computed expressions#
Only names and dotted paths narrow. An index like a[i], a call result, or any other computed expression has no stable key to hang a fact on. Bind it to a local and narrow that:
local entry = entries[index]
if entry then
print(entry.name) -- entry is narrowed; entries[index] would not have been
endDive deeper
A fact is recorded under a textual path: s, or cfg.server.port. Two evaluations of a[i] are two separate reads, and nothing in the path says i held the same value both times or that a was not written in between. Tracking one would mean proving that neither the index nor the table changed across every statement between the test and the use, which is the analysis narrowing exists to do without.
A write clears a fact: an assignment to the path or to anything above it, and a call the checker can see writing there. What a called function writes is read from its source, whether it is checked before or after the call: a field assigned through a parameter or self, including through a copy of one, a captured local it assigns, and whatever the functions it calls do in turn, a callback it is handed among them. A call that could write the path forgets the fact and everything under it; a call that writes some other field keeps it. A call the checker cannot see into -- a function value read from another module's field, a parameter typed as a function -- is trusted to write nothing.
A loop body's writes are forgotten at the loop's entry, and at a label a later goto jumps back to, because the body runs again after them. A function literal does not carry a narrowing of a captured local that is assigned after the literal is made, since the literal may run after that assignment.
any#
any never narrows, because it is already compatible with everything. Reach for a predicate function or an as cast where you know more than the annotation does. See overview.md for what any gives up.
Falsy and#
The truthy side of and proves both operands. The falsy side proves neither, since either test could have been the one that failed:
if a and a.b then
print(a.b) -- a is not nil and a.b is truthy
else
print(a) -- nothing was proved: a may still be nil
endExhausted subtraction#
Subtraction takes members away from a union one test at a time, and a type that is not a union survives it: subtracting string from string leaves string, so the false arm of a test that could not have failed says what the declaration said. A chain that tests every member therefore ends holding the last one, not never:
local function f(v: string | number)
if v is string then
print(v)
elseif v is number then
print(v)
else
-- v is number here: string was subtracted, and number, the last
-- member standing, is not a union to subtract from
end
endFacts live in a scope#
A narrowed fact dies with the scope that proved it, and assigning to a name clears the facts for that name and everything beneath it:
local function f(s: string?)
if s then
s = maybeName() -- facts for s are cleared here
end
endThe declared type is what an assignment is checked against, so clearing a fact never lets a wider value in. It only takes back what the test had proved.
Predicate functions#
When narrowing cannot see what you know, write a predicate. The return type v is T names a parameter and a type:
local function isPoint(v: any): v is Point
return v ~= nil and v.x ~= nil and v.y ~= nil
end
local function use(v: any)
if isPoint(v) then
print(v.x)
end
endThe body is trusted. The checker verifies that the name is a parameter and that the parameter could hold that type, and takes the rest on faith.
Dive deeper
Proving a predicate would mean deriving v is Point from the body's chain of field tests, which is the same shape-inference problem the is operator exists to avoid. Trusting the body keeps the escape hatch one function wide: the signature says what is being asserted, the callers get an ordinary narrowing test, and the unchecked step is confined to a body a reader can see whole. See overview.md for the other rules that trade soundness for compatibility.
Guard clauses#
A function that returns never narrows the code after a call to it, the way an inline error does:
local function bail(msg: string): never
error(msg)
end
local function use(s: string?)
if not s then
bail("missing")
end
print(#s) -- s is string here
endThe checker infers this for a body whose every path raises, so the never return type is only needed where it cannot see that: an imported C abort, a declaration file with no body, or a loop that never ends. See Primitive types for the rest of what never does.
Switch arm narrowing#
Switch cases apply their facts only within their own arm. A static case narrows the selector to the matched literal; case is T narrows it to T. Earlier cases are subtracted before a later arm is checked, so the else arm sees the unmatched residue:
local text = switch value do
case is string as s -> s
case is Point as point {x, y} -> `(${x}, ${y})`
else -> "none" -- value is the portion not covered above
endas point is a const binding of the narrowed whole value. {x, y as vertical} introduces const locals for direct fields; those names exist only in that arm. The original selector remains narrowed too. Type cases are ordered, so a broad case before a narrower one can make the latter unreachable.
See switch expressions for runtime-testable types and block arms.
Returning-branch exhaustiveness#
When every branch of a dispatch over a closed set of literals returns, the checker reports the members left out as the exhaustiveness lint:
local type Color = "red" | "green" | "blue"
local function name(color: Color): string
if color == "red" then
return "warm"
elseif color == "green" then
return "cool"
end
return "unknown" -- NUPP2107: "blue" is unhandled
endExhaustiveness counts single literal types and unions of them. It does not run over a union of records, where a dispatch tests a discriminant field rather than the value. See Unions for the rule and Lints for the lint's severity and suppression.
FAQ#
Does a call between the test and the use lose the narrowing?#
Only when the callee can be seen to write what was tested: through a parameter the tested value was passed as, through self, or to a captured local, directly or through the functions it calls. Any other call keeps the fact. Computed expressions says what a call is taken to write, and reassigning the name yourself always clears it, as Facts live in a scope shows.
Should I write is or a predicate function?#
Write v is T when T is runtime-testable on its own, which covers records, structs, C types, and literals. Write a predicate when the test is a shape check the checker cannot perform, or when the same check is repeated in several places. See Interfaces for what an is edge proves.
Does narrowing change the generated Lua?#
No. A narrowed type is a fact the checker carries and erases, so the branch lowers to the Lua you wrote. See strictness.md for the two things that do survive.