Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Chapter 15: Type Narrowing — Making Unions Useful

You defined number|string. You checked compatibility. You even inferred function types with generic parameters. But there’s a problem you’ve been ignoring since Chapter 11.

---@type number|string
local x = 42

local y = x + 1

This should work. x is clearly 42, which is a number. But the type checker sees number|string and gives up — it can’t prove x is safe for arithmetic. The union type you carefully built is now in the way.

What you need is narrowing: the ability to say “if this condition is true, then x is definitely a number.” That’s what this chapter builds.

The Problem: Unions Without Narrowing Are Decorative

Our type checker handles unions through is_compatible_with. A Union(Number | String) is compatible with Number — because one variant matches. But that’s the wrong question for arithmetic. The question isn’t “could this be a number?” — it’s “is this definitely a number?”

The difference matters:

CheckQuestionNumber | String in arithmetic
is_compatible_withCould this be a number?✅ Yes — compatible
narrowingIs this definitely a number?❌ No — might be a string

Without narrowing, unions are decorations on your type annotations. They don’t help the checker make decisions — they make it more cautious without making it smarter.

Three Guard Patterns

Lua gives you three ways to narrow a type at runtime. Our checker needs to recognize all three.

1. type(x) == "number" — Type Check

The most explicit narrowing. If type(x) returns "number", then x is definitely a number.

---@type number|string
local x = get_value()

if type(x) == "number" then
    local y = x + 1     -- x is Number here
else
    local z = x .. "!"  -- x is String here
end

In the then-block, x narrows from Number | String to Number. In the else-block, Number is removed from the union, leaving String.

2. x ~= nil — Nil Exclusion

Common in Lua: check that a value isn’t nil before using it.

---@type number|nil
local x = maybe_get_number()

if x ~= nil then
    local y = x + 1  -- x is Number here
end

This removes Nil from the union. After the check, x is Number.

3. if x then — Truthy Check

Lua’s truthy check excludes both nil and false.

---@type number|nil
local x = maybe_get_number()

if x then
    local y = x + 1  -- x is Number here (Nil removed)
end

Our Boolean type doesn’t distinguish true from false, so truthy narrowing removes both Nil and Boolean from the union. A production checker would have literal types (True, False) for more precise narrowing.

Adding Never — The Bottom Type

Before we write the narrowing logic, we need a new variant in our Type enum. When narrowing eliminates all possibilities — say, a String narrowed to Number — the result isn’t Nil. Nil is a real Lua type meaning “no value.” The result should mean “this code path is impossible.”

That’s Never, the bottom type:

#![allow(unused)]
fn main() {
#[derive(Clone, Debug, PartialEq, Eq, Hash, salsa::Update)]
pub enum Type {
    Number, String, Boolean, Nil,
    Never,              // NEW: the bottom type — impossible code path
    Function { params: Vec<Type>, ret: Box<Type> },
    Table { fields: Vec<(String, Type)> },
    Union(Vec<Type>),
    Var(String),        // from Chapter 12
    Ref(String),        // from Chapter 14
    Dynamic, Error,
}
}

Never has two special properties:

  1. It’s compatible with everything. Dead code can’t produce type errors. If a branch narrows to Never, any expression inside it type-checks — there’s no runtime value that could violate the type.

  2. It’s absorbed by unions. Number | Never simplifies to Number. An impossible alternative doesn’t change the set of possible values.

Property #2 means Type::union() needs to filter out Never:

#![allow(unused)]
fn main() {
impl Type {
    pub fn union(types: Vec<Type>) -> Type {
        let mut flat = Vec::new();
        for t in types {
            match t {
                Type::Union(inner) => flat.extend(inner),
                other => flat.push(other),
            }
        }

        // Remove Never — it's absorbed by unions
        flat.retain(|t| !matches!(t, Type::Never));

        flat.sort_by(|a, b| format!("{a:?}").cmp(&format!("{b:?}")));
        flat.dedup();

        if flat.is_empty() {
            return Type::Never;  // union of nothing is impossible
        }
        if flat.len() == 1 {
            return flat.pop().unwrap();
        }
        if flat.iter().any(|t| matches!(t, Type::Dynamic)) {
            return Type::Dynamic;
        }

        Type::Union(flat)
    }
}
}

The flat.retain line removes Never variants before checking for duplicates and singletons. If all variants are Never (an empty union), the result is Never — the whole thing is impossible. The flat.is_empty() guard is now necessary because retain might have emptied the list — previously, the list was never empty after flattening and dedup.

And is_compatible_with gains one more case:

#![allow(unused)]
fn main() {
(Type::Never, _) | (_, Type::Never) => true,
}

Never is compatible with everything — dead code can’t type-error.

How Narrowing Works: The narrow_to and remove Methods

Narrowing a type means: given a current type and a target type, produce the narrowest type that’s consistent with both.

narrow_to — “Narrow to exactly this type”

#![allow(unused)]
fn main() {
fn narrow_to(&self, target: &Type) -> Type {
    match (self, target) {
        // Can't narrow from Dynamic — we don't know what it is
        (Type::Dynamic, _) => Type::Dynamic,
        // Can't narrow TO Dynamic — but don't lose what we already know.
        // If someone writes type(x) == "unknowntype", the target resolves
        // to Dynamic. We shouldn't degrade Number to Dynamic because
        // the target type is unrecognized.
        (_, Type::Dynamic) => self.clone(),
        // Error stays Error
        (Type::Error, _) => Type::Error,
        // Var stays as-is — we don't know what it resolves to
        (Type::Var(_), _) => self.clone(),
        // Union: narrow each variant recursively, keep the non-Never results
        (Type::Union(variants), _) => {
            let narrowed: Vec<Type> = variants.iter()
                .filter_map(|v| {
                    let n = v.narrow_to(target);
                    if matches!(n, Type::Never) {
                        None    // This variant was incompatible — skip it
                    } else {
                        Some(n)
                    }
                })
                .collect();
            if narrowed.is_empty() {
                // No variant matches — this code path is impossible.
                // Return Never, not the target. If Union(String, Boolean)
                // narrows to Number, the result is Never (neither variant
                // is a Number), not Number (which would be a lie — the
                // condition can never be true, so the variable can never
                // have that type).
                Type::Never
            } else {
                Type::union(narrowed)
            }
        }
        // Same type? Already narrowed.
        _ if self == target => self.clone(),
        // Compatible but not equal (e.g., Ref("Node") narrowed to
        // a Table with the same fields) → keep self
        _ if self.is_compatible_with(target) => self.clone(),
        // Incompatible: this branch is impossible
        _ => Type::Never,
    }
}
}

For Union(Number | String).narrow_to(&Number): Number.narrow_to(&Number) returns Number (same type), String.narrow_to(&Number) returns Never (incompatible, filtered out). The result is Number.

For Number.narrow_to(&String): incompatible, so the result is Never — this branch can’t execute. The Never type was introduced above; it means “impossible code path,” which is distinct from Nil (a real Lua value).

The union arm uses recursive narrow_to instead of is_compatible_with. This matters for nested unions: Union(Number | String | Nil).narrow_to(&Number) calls narrow_to on each variant, and String.narrow_to(&Number) returns Never (filtered out), Nil.narrow_to(&Number) returns Never (filtered out), and Number.narrow_to(&Number) returns Number. If we used is_compatible_with instead, String.is_compatible_with(&Number) returns false — which happens to work here. But for Union(Union(Number | String) | Nil).narrow_to(&Number), is_compatible_with would keep the inner Number | String union intact (because Number | String is compatible with Number), while recursive narrow_to correctly narrows it to Number alone.

remove — “Remove this type from the union”

#![allow(unused)]
fn main() {
fn remove(&self, removed: &Type) -> Type {
    match self {
        Type::Union(variants) => {
            let kept: Vec<_> = variants.iter()
                .filter(|v| v != &removed)
                .cloned()
                .collect();
            Type::union(kept)
        }
        // If the type IS the removed type, this is an impossible branch
        _ if self == removed => Type::Never,
        // Dynamic and atomic types (Number, String, etc.) are unaffected —
        // if it's not a union and not the removed type, it stays the same.
        _ => self.clone(),
    }
}
}

For Union(Number | String).remove(&Number): Number is filtered out, leaving String.

For Union(Number | Nil).remove(&Nil): Nil is filtered out, leaving Number.

This is simpler than trying to compute a “complement type” (everything that isn’t Nil). We don’t need to know what all possible types are — we remove the one we know isn’t present.

remove_truthy — “Remove all truthy types”

The else-block of if x then needs to strip all truthy types from the union. We can’t chain remove calls because remove uses exact equality — remove(&Type::Table { fields: vec![] }) won’t match a Table with fields. Instead, remove_truthy filters by kind:

#![allow(unused)]
fn main() {
fn remove_truthy(&self) -> Type {
    match self {
        Type::Union(variants) => {
            let kept: Vec<Type> = variants.iter()
                .filter(|v| !v.is_truthy())
                .cloned()
                .collect();
            Type::union(kept)
        }
        _ if self.is_truthy() => Type::Never,
        _ => self.clone(),
    }
}

fn is_truthy(&self) -> bool {
    match self {
        // Truthy types: values of these types are always truthy
        Type::Number | Type::String => true,
        Type::Table { .. } | Type::Function { .. } => true,
        // Falsy types: only Nil and false are falsy in Lua
        Type::Nil | Type::Boolean => false,
        // Never is impossible, Dynamic is unknown — keep both
        Type::Never => false,
        Type::Dynamic => false,
        Type::Error => false,
        // Var and Ref are unknown — don't remove them
        Type::Var(_) | Type::Ref(_) => false,
        // Unions are handled by the caller
        Type::Union(_) => false,
    }
}
}

The key difference from remove: is_truthy returns true for any Table or Function variant, regardless of fields or signature. remove requires exact equality. When you’re filtering by category (truthy vs. falsy), kind-based filtering is what you need.

Extracting Narrowings from Conditions

We need a function that takes a condition expression and produces two sets of narrowings: one for the then-block and one for the else-block.

#![allow(unused)]
fn main() {
enum Narrowing {
    ToType(String, Type),      // narrow variable to this type
    RemoveType(String, Type),  // remove this type from variable's union
    RemoveFalsy(String),       // remove Nil and Boolean
    RemoveTruthy(String),      // remove truthy types (Number, String, Table, Function)
}

fn extract_narrowings(expr: &Expression) -> (Vec<Narrowing>, Vec<Narrowing>) {
    match expr {
        // type(x) == "number" → narrow x to Number
        // Also handles "number" == type(x) via .or_else()
        BinaryOp { left, op: BinOp::Eq, right } => {
            if let Some((var_name, type_name)) = match_type_check(left, right)
                .or_else(|| match_type_check(right, left))
            {
                let target = type_name_to_type(&type_name);
                return (
                    vec![Narrowing::ToType(var_name.clone(), target.clone())],
                    vec![Narrowing::RemoveType(var_name, target)],
                );
            }
            (vec![], vec![])
        }
        
        // x ~= nil → remove Nil from x
        // Also handles nil ~= x via .or_else()
        BinaryOp { left, op: BinOp::Ne, right } => {
            if let Some(var_name) = match_nil_check(left, right)
                .or_else(|| match_nil_check(right, left))
            {
                return (
                    vec![Narrowing::RemoveType(var_name.clone(), Type::Nil)],
                    vec![Narrowing::ToType(var_name, Type::Nil)],
                );
            }
            (vec![], vec![])
        }
        
        // if x then → remove falsy from then-block,
        //              remove truthy from else-block
        Name(name) => {
            let then_narrow = Narrowing::RemoveFalsy(name.clone());
            // else-block: x is falsy. Remove all truthy types from
            // the union, leaving only the falsy ones (Nil and Boolean).
            // This is correct for unions containing Boolean — unlike
            // narrowing to Nil, which would incorrectly drop Boolean.
            //
            // For `number|nil`, RemoveTruthy strips Number, leaving Nil.
            // For `number|boolean|nil`, RemoveTruthy strips Number,
            // leaving `boolean|nil`.
            let else_narrow = Narrowing::RemoveTruthy(name.clone());
            (vec![then_narrow], vec![else_narrow])
        }
        
        // not x → flip the narrowings
        UnaryOp { op: UnaryOp::Not, expr: inner } => {
            let (then, else_) = extract_narrowings(inner);
            (else_, then)  // Negation swaps then and else
        },
        
        _ => (vec![], vec![]),
    }
}
}

The not case is elegant: negation swaps the then/else narrowings. If type(x) == "number" narrows x to Number in the then-block, then not (type(x) == "number") narrows x to Number in the else-block.

The Helper Functions

extract_narrowings delegates the pattern matching to four small helpers. Here they are in full.

match_type_check recognizes the type(x) == "typename" pattern — a function call to type on one side, a string literal on the other:

#![allow(unused)]
fn main() {
fn match_type_check(left: &Expression, right: &Expression) -> Option<(String, String)> {
    // Left must be `type(x)`, right must be a string literal
    if let Expression::FunctionCall { func, args } = left {
        if let Expression::Name(fname) = func.as_ref() {
            if fname == "type" {
                if let Some(arg) = args.first() {
                    if let Expression::Name(var_name) = arg {
                        if let Expression::StringLiteral(type_name) = right {
                            // Strip surrounding quotes — the AST includes them
                            let unquoted = type_name.trim_matches('"');
                            return Some((var_name.clone(), unquoted.to_string()));
                        }
                    }
                }
            }
        }
    }
    None
}
}

match_nil_check recognizes x ~= nil — a variable name on one side, the Nil expression on the other:

#![allow(unused)]
fn main() {
fn match_nil_check(var_side: &Expression, nil_side: &Expression) -> Option<String> {
    if let Expression::Name(name) = var_side {
        if let Expression::Nil = nil_side {
            return Some(name.clone());
        }
    }
    None
}
}

type_name_to_type converts a Lua type name (from type()) to our Type enum. This is the same logic as the parse_type_name helper from Chapter 10, with additional cases for nil, table, and function:

#![allow(unused)]
fn main() {
fn type_name_to_type(name: &str) -> Type {
    match name {
        "number" => Type::Number,
        "string" => Type::String,
        "boolean" => Type::Boolean,
        "nil" => Type::Nil,
        "table" => Type::Table { fields: vec![] },
        "function" => Type::Function { params: vec![], ret: Box::new(Type::Dynamic) },
        _ => Type::Dynamic,
    }
}
}

A real type checker would emit “unknown type name” instead of falling back to Dynamic, but for our purposes this is honest: an unrecognized type is effectively unknown.

apply_narrowings takes a type environment and a list of narrowings, and produces a new environment with each narrowed variable’s type updated:

#![allow(unused)]
fn main() {
fn apply_narrowings(env: &TypeEnv, narrowings: &[Narrowing]) -> TypeEnv {
    let mut new_env = env.clone();
    for narrowing in narrowings {
        match narrowing {
            Narrowing::ToType(var_name, target) => {
                let current = new_env.lookup(var_name);
                let narrowed = current.narrow_to(target);
                new_env = new_env.extend(var_name.clone(), narrowed);
            }
            Narrowing::RemoveType(var_name, removed) => {
                let current = new_env.lookup(var_name);
                let narrowed = current.remove(removed);
                new_env = new_env.extend(var_name.clone(), narrowed);
            }
            Narrowing::RemoveFalsy(var_name) => {
                let current = new_env.lookup(var_name);
                // Remove Nil, then remove Boolean. For unions this
                // strips both. For non-union types, each remove is
                // a no-op if the type isn't Nil or Boolean.
                let narrowed = current.remove(&Type::Nil).remove(&Type::Boolean);
                new_env = new_env.extend(var_name.clone(), narrowed);
            }
            Narrowing::RemoveTruthy(var_name) => {
                let current = new_env.lookup(var_name);
                // Remove all truthy types from the union. What remains
                // are the falsy types: Nil and Boolean. For `number|nil`,
                // this strips Number, leaving Nil. For
                // `number|boolean|nil`, this strips Number, leaving
                // `boolean|nil`.
                let narrowed = current.remove_truthy();
                new_env = new_env.extend(var_name.clone(), narrowed);
            }
        }
    }
    new_env
}
}

Why RemoveTruthy Instead of ToType(Nil)

The else-block of if x then is the case where x is falsy. The falsy values in Lua are nil and false. Our initial instinct might be to narrow to Nil — after all, nil is the most common falsy value.

But that’s wrong when the variable’s type includes Boolean. Consider:

---@type number|boolean|nil
local x = get_value()

if x then
    -- x is number|boolean — Nil removed ✅
else
    -- x is... what?
end

In the else-block, x is falsy, so it’s either nil or false. That’s Nil | Boolean — not Nil alone. If we used Narrowing::ToType(x, Nil), the checker would think x is Nil and would strip the Boolean variant. That’s a lie — false is a valid value here.

RemoveTruthy fixes this. Instead of asserting “x is Nil,” it says “remove everything that’s truthy.” For number|boolean|nil, removing truthy types strips Number, leaving boolean|nil. Correct.

For the common case — number|nilRemoveTruthy strips Number, leaving Nil. Same result as ToType(Nil), but via a mechanism that doesn’t break when Boolean is in the union.

apply_narrowings creates a new TypeEnv for each branch rather than mutating the original. This is essential — the original environment is returned after the if, preserving the scope rule. If both branches narrowed x, those narrowings don’t leak. Chapter 16 covers what happens when you want them to.

A Subtle Bug: String Literals in the AST

There’s a trap waiting in the type(x) == "number" pattern. The analisar parser stores string literals with their quotes — so the AST token for "number" is "\"number\"", not "number". If match_type_check passes the raw token to type_name_to_type, the lookup fails (because "\"number\"" doesn’t match "number"), and the narrowing silently resolves to Dynamic.

The match_type_check helper above handles this with type_name.trim_matches('"') — strip the quotes before looking up the type name. This is the kind of parser/AST mismatch that’s invisible until you actually run the code. The narrowing logic was correct — the data was wrong. If your narrowing tests pass but the narrowed type shows up as Dynamic instead of Number, check what the parser actually gives you for the string literal.

The Scope Rule: Narrowings Don’t Leak

After the if block ends, narrowings go out of scope. We return the original environment, not the narrowed one.

---@type number|string
local x = get_value()

if type(x) == "number" then
    local y = x + 1  -- x is Number here
end

local z = x + 1  -- x is Number | String again

This is correct behavior: after the if, we don’t know which branch ran. The variable x could still be either type.

What about assignments inside the if? Our checker loses them too — any assignment to an existing variable inside an if block is discarded when the block ends. A production checker would do “environment merging”: if both branches assign to x, the post-if type is the union of both branches’ types for x. That requires tracking assignments within branches, which our current architecture doesn’t support.

The Key Change in check_stmt

The Statement::If arm now looks like this:

#![allow(unused)]
fn main() {
Statement::If { test, then_block, else_block } => {
    // Evaluate the condition
    infer_type(db, source, test.clone(), env.clone(), diagnostics);

    // Extract narrowings from the condition
    let (then_narrowings, else_narrowings) = extract_narrowings(test);

    // Keep the original env for after the if-else
    let original_env = env.clone();

    // Then-block: apply then-narrowings
    let then_env = apply_narrowings(&original_env, &then_narrowings);
    let mut env = then_env;  // shadow env with the narrowed version for this block
    for s in then_block {
        env = check_stmt(db, source, s, &env, annotations, diagnostics);
    }

    // Else-block: apply else-narrowings
    if let Some(else_block) = else_block {
        let else_env = apply_narrowings(&original_env, &else_narrowings);
        let mut env = else_env;  // shadow env with the narrowed version for this block
        for s in else_block {
            env = check_stmt(db, source, s, &env, annotations, diagnostics);
        }
    }

    // After the if-else, narrowings go out of scope
    original_env
}
}

apply_narrowings produces a new TypeEnv (not mutating the existing one) where each narrowed variable has its updated type. The original environment is returned after the if, preserving the scope rule.

What We’re Simplifying

No type narrowing for assignments. If x = 42 inside an if block, we don’t propagate that information.

No environment merging. After an if-else, we don’t merge the environments from both branches. This is the next chapter — Chapter 16 builds TypeEnv::merge to handle exactly this case.

No Boolean narrowing to true/false. Our Boolean type doesn’t distinguish true from false, so truthy narrowing removes the entire Boolean type from the then-block. But the else-block correctly preserves Boolean via RemoveTruthy — a number|boolean|nil variable narrows to boolean|nil in the else-block, not just nil. A production checker would have literal types (True, False) for more precise narrowing in both branches.

No narrowing across function calls. If f() returns number|string, we don’t narrow based on the return value.

No and/or compound conditions. The most common follow-up question after type narrowing: “what about if type(x) == "number" and x > 0 then?” Our extract_narrowings only handles single-variable guards. A compound and should apply the narrowings from both sides of the and in the then-block — type(x) == "number" narrows x to Number, and x > 0 is safe under that narrowing. But recognizing this requires understanding that and short-circuits: the right side only runs if the left side is truthy, so the left side’s narrowings are in scope for the right side. Our checker doesn’t build this dependency chain — it evaluates each expression independently. Supporting compound conditions means walking the and/or structure, accumulating narrowings from left to right, and threading them through the type-checking of the right operand. That’s a control-flow analysis, not a pattern match.

No pattern-based narrowing. Lua’s match-like patterns (e.g., if type(x) == "table" and x.value then) aren’t supported — only single-variable guards. This is the same limitation as compound conditions, but deeper: x.value requires narrowing x to a Table first, then checking that the field exists. Our checker doesn’t track field-level narrowing.

Next: Chapter 16: Environment Merging After Conditionals — After an if/else, each branch might have narrowed the same variable to different types. How do you merge them? The answer isn’t “pick one” — it’s to compute the union of what each branch learned.