Inside Keel's Type Checker: How Types Actually Flow Through Your Code

We wrote a whole blog post about what Keel's type system does for you. It was upbeat and reassuring. "The compiler catches your bugs!" "You can sleep at night!" All true.

What we did not mention is what it took to build. That is what this post is about: the actual Rust code running underneath, the data structures it leans on, the algorithms that do the work, and the bugs that made me reconsider my career choices on at least two separate occasions.

If you have ever wondered how a compiler decides that 1 + 2.5 is a Float, or how it figures out the type of x in |x| x + 1 when you pipe integers through List.map, or what is going on in the exhaustiveness checker when it tells you that you forgot about Blue -- this is for you.

Seventeen Variants and a Lot of Boxes

Every type in Keel is a variant of a single Rust enum. Here it is:

#[derive(Clone, Debug, PartialEq, Serialize)]
pub enum Type {
    Boolean,
    String,
    Char,
    Float,
    Int,
    Unit,
    Never,
    Unknown,
    Var(String),
    Function(Box<Type>, Box<Type>),
    Record(Vec<(String, Type)>),
    Tuple(Vec<Type>),
    List(Box<Type>),
    Enum(String, Vec<Type>),
    Maybe(Box<Type>),
    Result(Box<Type>, Box<Type>),
    Custom(String, Vec<Type>),
    Native(usize),
}

Eighteen variants. Every type annotation you write, every type the compiler infers, every mismatch it catches -- all built from this one enum and some Boxes. When I first sketched this out, I expected it to be way bigger. It turned out that simple primitives, a recursive Function type, compound types for collections and records, and a handful of special cases get you surprisingly far.

The design is straightforward: primitive types get their own variants. Compound types use Box or Vec for their inner components. A function type like Int -> Int -> Int becomes Function(Int, Function(Int, Int)) -- curried, the same way the language itself works.

Two variants deserve closer attention.

Unknown is the compiler's way of saying "I have no idea yet." When a lambda parameter has no type annotation and no surrounding context, it starts as Unknown. Inference fills it in as context arrives. If it is still Unknown when compilation finishes -- well, the compiler has to ask you for help. Nobody likes asking for help, but dishonesty is worse.

Never is the type of values that can never exist at runtime. If you match on a Result(Unknown, Int) and write an Ok n -> branch, the n has type Never -- the value is syntactically present but logically impossible. This is Keel's version of Rust's ! or Haskell's Void. I did not appreciate how much Never would earn its keep until I tried removing it and watched about forty tests fail in creative ways.

As we discussed in Why Keel Is Written in Rust, making this a Rust enum means we get exhaustive matching for free. Every function that processes a Type must handle every variant. Add a new variant? The Rust compiler points at every place in the codebase that needs updating. It is like having a co-worker who remembers everything and never gets tired of code review.

Where Inference Lives

The inference engine is TypeInferenceContext, which bundles a scope and a string interner:

pub struct TypeInferenceContext {
    pub scope: Scope,
    pub string_interner: StringInterner,
}

The main method is infer_type, which takes an expression and returns a Type. The logic is a case-by-case walk over the Expr enum:

• Literals are trivial. Int(42, _) returns Type::Int. Even I can get that right.
• Variables look up the scope and return whatever type is registered there.
• Binary operations infer both operands, then call infer_binary_op_type to figure out the result. Integer plus float? Float (numeric promotion). Comparison? Always Boolean. String concatenation with ++? String. The full binary op handler is about 200 lines and covers arithmetic, comparison, logical, concatenation, cons, function composition, and pipe operators.
• Lists infer each element's type and unify them into a common type. [1, 2, 3] infers to List Int. An empty [] is List Unknown -- the element type gets filled in later from context.
• Records infer each field's value type and assemble a Record type: { name = "Alice", age = 30 } becomes Record([("name", String), ("age", Int)]).
• Function calls are the interesting part.

The Heart of It: Applying a Function Type

When the compiler sees f x, it has to figure out what the application returns. The method apply_function_type does this through a lightweight unification:

pub fn apply_function_type(&self, func_type: Type, arg_type: Type) -> Type {
    match func_type {
        Function(param_type, return_type) => {
            let mut subs = HashMap::new();
            if Self::match_types(&param_type, &arg_type, &mut subs) {
                Self::substitute_vars(*return_type, &subs)
            } else {
                // type error path...
            }
        }
        // ...
    }
}

It takes the declared parameter type (which might contain type variables like a), matches it against the actual argument type, builds a substitution map (a => Int), and applies those substitutions to the return type.

For example, List.map has type (a -> b) -> List a -> List b. If you call it with a function of type Int -> String, the matcher produces {a: Int, b: String}. The return type List b becomes List String. This is how generic functions work without requiring you to write List.map<Int, String> everywhere -- which, let's be honest, nobody wants to type.

The match_types function handles structural matching recursively: it unifies Function against Function, List against List, Tuple against Tuple, and so on, collecting variable bindings along the way. Unknown types are treated as wildcards -- they match anything, which gives the system flexibility during incremental inference.

Lambda Inference: Types Flow Through Pipes

This is the piece that makes Keel's pipe style feel natural. When you write:

[1, 2, 3] |> List.map (|x| x * 2)

The compiler needs to figure out that x is an Int without you saying so. Here is how that works:

1. The pipe operator |> desugars to a function application: List.map (|x| x * 2) [1, 2, 3].
2. The compiler infers the type of List.map -- which is (a -> b) -> List a -> List b.
3. Before inferring the lambda's body, it extracts the expected first parameter type from List.map's signature: a -> b.
4. extract_lambda_param_types unwraps this curried function type into individual parameter types. For a single-parameter lambda, it produces [a].
5. Inside infer_lambda_type_with_expected, the parameter x gets the expected type a.
6. From the surrounding context -- [1, 2, 3] is List Int -- the type variable a resolves to Int.
7. The body x * 2 infers to Int, so b also resolves to Int.

The priority system for resolving lambda parameter types is explicit in the code:

// Priority 1: Explicit type annotation in the pattern (|x: Int|)
// Priority 2: Expected type from call context
// Priority 3: Type::Unknown (requires manual annotation)

When a lambda stands alone -- let f = |x| x + 1 -- there is no context, and Priority 3 kicks in. That is when you get the "Lambda parameter requires a type annotation" error. I briefly considered full Hindley-Milner unification for this case, weighed it against my sanity, and decided to just ask the user for a type annotation. Sometimes the pragmatic answer wins.

This system also handles multi-parameter lambdas. When you write:

[1, 2, 3, 4] |> List.foldl (|acc x| acc + x) 0

The method extract_lambda_param_types unwraps the curried function type b -> a -> b into [b, a] for a two-parameter lambda. Context resolves both a and b to Int. Getting this right took multiple attempts and more than a few "wait, how does Haskell do this?" rabbit holes.

Unification: Finding Common Ground

When the compiler needs to reconcile two types -- the branches of an if expression, the arms of a case, the elements of a list -- it calls unify_types. This is where numeric promotion lives, and where things get deceptively subtle:

pub fn unify_types(&mut self, t1: Type, t2: Type) -> Type {
    let t1 = self.resolve_type(t1);
    let t2 = self.resolve_type(t2);

    if t1 == t2 { return t1; }

    if matches!(t1, Never) { return t2; }
    if matches!(t2, Never) { return t1; }

    if matches!(t1, Unknown) { return t2; }
    if matches!(t2, Unknown) { return t1; }

    match (t1, t2) {
        (Int, Float) | (Float, Int) => Float,
        (Maybe(a), Maybe(b)) => Maybe(Box::new(self.unify_types(*a, *b))),
        (Result(ok1, err1), Result(ok2, err2)) => Result(
            Box::new(self.unify_types(*ok1, *ok2)),
            Box::new(self.unify_types(*err1, *err2)),
        ),
        // ... structural recursion for all compound types
        _ => Unknown,
    }
}

Never earns its keep here. If one branch of a case returns Int and another is unreachable (type Never), they unify to Int. Without Never, I would have needed special-case logic for unreachable branches, or the compiler would report bogus type mismatches on perfectly good code. It is one of those things that seems obvious in hindsight but took me an embarrassing amount of time to realize.

Type alias resolution runs first via resolve_type, which is why type alias UserId = Int works seamlessly. By the time unification fires, UserId has already been replaced with Int. The resolver tracks visited aliases in a HashSet to prevent infinite loops. I discovered the need for this the hard way, when I accidentally wrote type alias A = A during testing and watched the compiler lock up. Don't laugh -- or do, I deserve it.

The Scope: Where Types Live

The Scope struct is the type system's memory. It has ten HashMap fields tracking variables, functions, enums, type aliases, modules, and more -- plus a parent link for lexical scoping. Every key is a usize, not a String. That is the string interner at work: "totalCount" maps to an integer, and from that point on, every lookup and comparison uses integer equality instead of walking character arrays. It is one of those optimizations that feels almost too simple, but it made a noticeable difference.

The functions field maps names to a list of (arg_type, return_type) pairs -- that is how overloading works. Both fn inc : Int -> Int and fn inc : Float -> Float are stored under the same interned index. When you call inc 5, the scope's lookup_fn_impl_with_context method iterates the overloads and finds one where the parameter type matches Int. It even handles different-arity overloading, using context to disambiguate whether the caller expects a function result or a final value.

Lexical scoping uses the parent chain. Every scope lookup checks the current scope first, then walks up. Creating a new scope for a function body or case arm is just Scope::new(Some(Box::new(current_scope))). Simple, reliable, and easy to reason about.

Exhaustiveness Checking: Accounting for Every Possibility

The exhaustiveness checker in exhaustiveness.rs answers a deceptively simple question: does a case expression handle every possible value?

The algorithm first walks the branches, tracking whether a catch-all (wildcard or variable) has been seen. If no catch-all exists, it dispatches to type-specific checks. For booleans, it tracks whether True and False are both covered. For enums, it collects all variant names from the scope and checks which appear in the patterns. For Maybe, it checks Just and Nothing. For Result, Ok and Err.

The enum checker is representative. It collects all variants from the type definition, walks the patterns to mark which are covered, and reports the rest:

let variant_names = scope.collect_enum_variant_names(enum_name, string_interner);
let mut covered_variants: HashSet<String> = HashSet::new();

for pattern in patterns {
    match pattern {
        Pattern::Wildcard | Pattern::Var(_, _) => {
            // Catch-all covers everything
            for variant in &variant_names {
                covered_variants.insert(variant.clone());
            }
        }
        Pattern::Constructor(name, _) => {
            covered_variants.insert(name.clone());
        }
        // ... or-patterns, qualified variants, etc.
    }
}

let missing: Vec<String> = variant_names
    .into_iter()
    .filter(|v| !covered_variants.contains(v))
    .collect();

A few edge cases complicate things. Or-patterns like Red | Yellow -> "warm" contribute each alternative to the covered set. Guards are harder -- Active n if n > 3 does not cover all Active values. When guards are present without a catch-all, the checker emits a warning: "Guard exhaustiveness cannot be verified." Fully analyzing guard expressions would be a whole separate project, and an honest warning felt like a better trade-off than silence. Unreachable patterns after a catch-all get flagged as dead code.

The checker also validates pattern-type compatibility. Match a Maybe with an Ok pattern? check_pattern_type_compatibility catches the mismatch before the code ever gets near the VM. As we describe in the pattern matching post, this is what makes refactoring feel safe instead of terrifying.

Type Aliases: Simple Idea, Tricky Corners

Type alias resolution looks straightforward on paper -- replace the alias name with its underlying type. And it mostly is. But parameterized aliases add a twist:

type alias Pair a = (a, a)

When you write Pair Int, the resolver has to substitute a => Int throughout the underlying type, producing (Int, Int). The substitute_type_vars method handles this, building a mapping from parameter names to concrete types and walking the type structure to apply it.

The Custom to Enum conversion is another subtlety. When the parser sees a type name like Direction, it does not know yet whether it is a type alias or an enum -- both are uppercase identifiers. It produces Custom("Direction", []), and the resolver checks the scope: if Direction is a declared enum, it becomes Enum("Direction", []). If it is a type alias, it expands to the underlying type. This two-phase design keeps the parser blissfully simple and pushes type resolution to the phase where scope information is actually available. Separation of concerns -- when it works, it is beautiful.

The Two Faces of Unknown

After inference runs, a final validation pass walks the AST to make sure no Unknown types remain unresolved. But there is a subtle distinction between two methods on the Type enum: contains_unknown and is_unresolvable.

contains_unknown does what it says -- any Unknown anywhere in the type tree makes it return true. But is_unresolvable is more lenient:

pub fn is_unresolvable(&self) -> bool {
    match self {
        Type::Unknown => true,
        Type::Result(ok, err) => ok.is_unresolvable() && err.is_unresolvable(),
        Type::Maybe(inner) => match inner.as_ref() {
            Type::Unknown => false, // Maybe(Unknown) is valid for Nothing
            _ => inner.is_unresolvable(),
        },
        // ... structural recursion for other types
    }
}

A Result(Int, Unknown) contains an unknown type, but it is not unresolvable. It just means you wrote Ok 42 without ever using the Err branch, so the error type was never constrained. That is perfectly fine code. A bare Unknown at the top level, on the other hand -- that is a genuine problem.

Getting this two-tier check right was one of those moments where the fog lifts. Without it, the compiler would either reject perfectly good code like let x = Ok 42 (what is the error type? does not matter, it is never used) or silently accept genuinely ambiguous code like let f = |x| x + 1 (what is x? could be anything). The dividing line turned out to be exactly whether the unknown type is nested inside a resolved container or standing on its own.

Compile-Time Types vs. Runtime Values

Something that surprised me early on: the Type enum and the RegisterValue enum are completely separate hierarchies. At compile time, everything is a Type. At runtime, everything is a RegisterValue:

pub enum RegisterValue {
    Int(i64),
    Float(f64),
    Tuple(usize),       // heap index
    List(usize),        // heap index
    Record(usize),      // heap index
    Enum(usize, usize, Option<usize>),  // interned names + optional args
    Closure(Closure),
    // ...
}

Notice the difference: Type::Record(Vec<(String, Type)>) carries field names and types. RegisterValue::Record(usize) is just a heap index -- the actual data lives on the heap, and field names are interned integers. All the structural information the type system tracked gets used during compilation to generate correct bytecode, and then it vanishes. The VM does not need it because the type checker already verified everything.

This separation is why Keel has a rich type system with zero runtime type overhead. The RegisterValue enum is compact: scalars are inline, compound values are heap indices. There is no type tag that gets checked at runtime (except the enum variant tag for dispatch). The VM trusts the compiler. It is a nice relationship built on rigorous testing and, I like to think, mutual respect.

What Is Not Built Yet

I want to be honest about what is missing. The inference is bottom-up with contextual propagation, not full Hindley-Milner -- some programs that would type-check in Haskell need explicit annotations in Keel. Type classes for ad-hoc polymorphism (comparable, number) are on the roadmap; function overloading covers the most common cases for now. Higher-kinded types are absent -- List is a type, not a type-level function you can pass around.

These are deliberate scope decisions. The current system handles the patterns that matter for data work: generics, sum types, pattern matching, pipe-friendly inference. I would rather ship a type system that works well for its use cases than one that is theoretically complete but confusing in practice.

Poking Around

If you want to see types in action, the playground shows inferred types inline. Write a function, pipe some data through it, and watch the types resolve.

The source is on Codeberg. The files to read are compiler/types.rs (the Type enum), compiler/type_inference.rs (the inference engine), compiler/exhaustiveness.rs (the pattern checker), compiler/type_validation.rs (the final sweep), and compiler/scope.rs (where types are stored). They are documented thoroughly, mostly because future-me has a terrible memory and past-me learned that the hard way.

If a type error message does not make sense, that is a bug. Genuinely. Let us know.