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.

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
}

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, narrow to Nil in else-block
        Name(name) => {
            let then_narrow = Narrowing::RemoveFalsy(name.clone());
            // else-block: x is falsy. We narrow to Nil — the primary
            // falsy type. This is an approximation: `false` is also
            // falsy in Lua, but our type system doesn't distinguish
            // True from False within Boolean. For the common case
            // (Nil checks), this is correct.
            //
            // Why narrow to Nil at all, rather than leaving the type unchanged?
            // In practice, `if x then` is almost always used with
            // `number|nil` or `string|nil` — where Nil is the only falsy
            // variant. Narrowing to Nil in the else-block is correct for
            // those cases, and it's strictly more informative than leaving
            // the type as `number|nil` (which would make the else-block
            // unable to prove x is nil).
            let else_narrow = Narrowing::ToType(name.clone(), Type::Nil);
            (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);
            }
        }
    }
    new_env
}
}

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. Our Boolean type doesn’t distinguish true from false, so truthy narrowing removes the entire Boolean type. A production checker would have literal types.

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

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.

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.