From Scope Analysis to Type Inference: What Building a Nix Type Checker Actually Requires

The Nix expression language has had language server support for years now. rnix-lsp came first, built on the rnix crate’s rowan-based concrete syntax tree. Then nil by oxalica improved significantly on scope analysis and name resolution, using a Salsa-based incremental computation model borrowed from rust-analyzer’s architecture. nixd took a different path entirely: rather than infer types statically, it links against the actual Nix evaluator and queries it as a co-process, getting completion data by evaluating the real nixpkgs tree.

None of them do static type inference. A recent post on johns.codes documents the attempt to build one from scratch, along with a full LSP implementation. The scope of that problem is worth unpacking, because the gap between “name resolution” and “type inference” is not a short engineering distance.

What scope analysis gives you and what it does not

il’s approach is worth understanding precisely. It performs scope analysis: given an expression, it can tell you which binding a name refers to, whether a variable is used, and what names are in scope at a given position. This is enough for go-to-definition, find-references, and rename. It is not enough to tell you that builtins.map (x: x + 1) ["a" "b"] is a type error.

nixd gets closer to type information by actually evaluating expressions. If you hover over a nixpkgs attribute, nixd can tell you its evaluated type because it called the Nix evaluator and got a runtime value back. The limitation is structural: nixd’s “type” is a runtime observation, not a static inference. It cannot check code before evaluation, it cannot catch errors in code paths that aren’t exercised during the LSP session, and it depends on a working Nix installation and a successful evaluation of potentially large expression trees.

Static type inference means computing type information without evaluating the program at all. That is what a type checker and LSP from scratch needs to provide, and Nix’s design makes this considerably harder than it is for most languages.

The specific constructs that break standard inference

Hindley-Milner type inference, the algorithm underlying ML, Haskell, and OCaml, is the natural starting point for any purely functional language. Nix is purely functional and lazy, so you might expect HM to apply. It does not transfer cleanly for several reasons.

The first is attribute set merging. Nix’s // operator merges two attribute sets, with right-hand fields overriding left-hand ones:

let base = { a = 1; b = 2; };
    override = { b = "changed"; c = 3; };
in base // override
# => { a = 1; b = "changed"; c = 3; }

The result has a field b whose type changed from integer to string. Standard HM has no mechanism for this. The result type is neither the type of base nor the type of override but a computed combination of both. Modeling this requires row polymorphism, a type system extension originally formalized by Didier Rémy and later developed extensively by researchers working on Haskell’s extensible records problem.

Row polymorphism treats record (attribute set) types as a “row” of labeled fields plus a polymorphic tail representing additional unknown fields. A function that accepts any record with at least a field a : int has type { a : int | r } where r is a row variable. Merging two records produces a new row that is the union of their field sets, with appropriate handling for conflicts. This is the theoretical machinery that a Nix type checker needs, and it substantially increases the complexity of the inference algorithm compared to plain HM.

The second problem is with. The with expr; body construct brings all attributes of expr into scope:

with pkgs; [
  git
  ripgrep
  fd
]

Here, git, ripgrep, and fd are names that come from the pkgs attribute set. A scope-based analysis can note that these names might be resolved through with, but without knowing the type of pkgs statically, it cannot verify that those names exist. In practice, nixpkgs has tens of thousands of attributes, so there is no way to materialize its type without either evaluating it or maintaining a separate type index.

The third is dynamic attribute access: set.${dynamicKey} where dynamicKey is a runtime expression. The type of such an access is necessarily unknown unless the type checker can statically evaluate the key expression, which in general it cannot.

Lazy evaluation creates a subtler problem. Nix does not evaluate expressions until their values are demanded. This means a program can contain type errors in branches that are never reached, and those errors will not surface at runtime. Whether a type checker should flag unreachable branches is a design decision, but it means the checker cannot take “this code path is never evaluated” as evidence of safety.

The LSP protocol layer and what types unlock

An LSP implementation involves a specific set of protocol methods, and not all of them benefit equally from type information. Hover documentation, go-to-definition, find-references, and rename all work reasonably well with scope analysis alone. Completion of attribute field names, type error diagnostics, and inlay hints showing inferred types all require actual type information.

Field completion is the most practically valuable. If your type checker knows that an expression has type { name : string; version : string; src : path; buildInputs : list derivation }, it can complete . access against that known set of fields, with types shown for each. This is the experience Rust users get from rust-analyzer and Go users get from gopls, and it is what Nix has been missing.

Type error diagnostics follow: knowing that a function expects list string and receives string lets the LSP underline the error with a message, rather than letting it surface as a Nix evaluation error at build time. For NixOS configuration specifically, this matters because configuration errors currently surface only when you run nixos-rebuild, not while you are editing.

Inlay hints showing the inferred type of a binding give users feedback on what the type checker has deduced, which is useful both for understanding and for catching cases where the inferred type is not what was intended.

Parsing and incremental computation

Building the type checker requires a parsing foundation and an incremental computation layer. The two main options for Nix parsing are tree-sitter-nix and the rnix crate. tree-sitter-nix produces error-tolerant concrete syntax trees and is used by Neovim and Helix for syntax highlighting. The rnix crate, also based on rowan, is what nil uses and produces a lossless CST with good incremental update properties.

For incremental computation, the obvious prior art is Salsa, the query-based incremental framework used by both nil and rust-analyzer. Salsa allows you to define computations as queries with automatic dependency tracking and fine-grained invalidation. When a file changes, only the computations that depend on that file’s content are re-run. For a type checker that needs to remain responsive during editing, this is important: full re-inference on every keystroke is not viable for large configurations.

The LSP server protocol itself can be implemented with tower-lsp in Rust, which handles the JSON-RPC transport and async method dispatch, leaving the implementor to focus on the analysis rather than the protocol mechanics.

What a working result changes

The comparison point for understanding what this project would deliver is the gap between writing Rust and writing C. In C, you discover many errors at runtime or in testing. In Rust, the compiler tells you about them while you are still editing. Nix is currently a C-like experience for configuration authors: you find out your mkDerivation is missing a required attribute, or that you passed a string where a list was expected, when you run the build.

A static type checker for Nix would move a significant class of those errors into the editor. The NixOS module system’s lib.types declarations would become static contracts checkable without evaluation. nixpkgs functions like stdenv.mkDerivation could have their expected attribute types specified and checked. The with pkgs; pattern could be validated against a pre-computed type index of nixpkgs attributes.

None of this requires solving all of Nix’s typing hard cases. Gradual typing, the approach TypeScript and mypy demonstrated for JavaScript and Python respectively, allows a type checker to coexist with dynamic any-typed expressions. An escape hatch for the cases row polymorphism or dynamic keys make unanalyzable is not a failure; it is what makes the system usable in practice.

The project at johns.codes is working in territory that nil, nixd, and rnix-lsp have not entered. The theoretical tools, row polymorphism for attribute sets and Hindley-Milner extended with gradual typing, are well understood. The engineering challenge is substantial but tractable. If it gets far enough to handle the common patterns in real NixOS configurations, it would be the most significant Nix tooling development since nil shipped.