The Nix language has been in an awkward tooling position for years. You can get syntax highlighting, go-to-definition, and basic completion from nil or evaluation-aware completions from nixd, but neither tool produces type errors. Neither tells you that you passed a string where a derivation was expected, or that you are calling a function with the wrong argument structure. A recent project at johns.codes documents what it actually takes to close that gap, and the implementation surfaces some genuinely interesting problems that go beyond “Nix is dynamically typed.”
The Language Is Simpler Than It Looks, Until It Isn’t
The core of the Nix expression language is a small functional language: lambdas, let-in bindings, conditionals, integer arithmetic, strings with interpolation, lists, and attribute sets. A grammar fits on a few pages. The type theory needed to handle that core is well-understood. Hindley-Milner inference handles the lambda calculus cleanly, and with polymorphism you can type builtins.map as (a -> b) -> [a] -> [b] and move on.
The complications are three specific features: with expressions, first-class import, and open attribute set patterns.
with introduces all attributes of an expression into the current scope:
with pkgs; [
git
vim
tmux
]Here git, vim, and tmux are resolved through pkgs, but at parse time you have no idea what attributes pkgs exposes. The identifier resolution is deferred until evaluation. Lexical scope, which every standard type inference algorithm depends on, is gone for any identifier that might come from a with.
First-class import compounds this:
let
lib = import ./lib.nix;
in
lib.mapAttrs (name: value: ...) configThe type of lib depends on the content of ./lib.nix, which is itself an arbitrary Nix expression. A static checker either has to evaluate it (expensive, and sometimes impossible without the full Nix store), treat it as opaque unknown, or require external type declaration files.
Open attribute set patterns are the third issue:
{ stdenv, lib, fetchFromGitHub, ... }:
stdenv.mkDerivation { ... }The ... means the function accepts any attribute set that has at least stdenv, lib, and fetchFromGitHub. This is structural subtyping with row polymorphism. You need a type system that can express “an attribute set with at least these fields” and allow additional fields through without losing track of them. Hindley-Milner alone cannot express this.
Why with Is the Hardest Piece
TypeScript faced JavaScript’s with statement and solved the problem by refusing to support it in strict mode, which TypeScript always uses. That is not available to a Nix type checker. with is idiomatic Nix. The canonical way to write a NixOS configuration module uses with lib; at the top level to bring mkOption, types, optionalString, and dozens of similar utilities into scope. Banning with would make the type checker reject essentially all real NixOS configuration code.
The practical options are limited. You can treat with expr; as introducing a scope with type unknown for any unresolved identifier, degrading gracefully to untyped behavior within the with body. This is sound in the sense of not producing false positives, but it destroys type information precisely in the code that uses with most heavily. You can attempt to evaluate the with expression statically and extract its attribute types, which works when the expression is a simple module-level reference but fails for computed values. Or you can require that the with expression have a known type via annotation, shifting the burden to the user.
None of these options is satisfying. They all represent a fundamental tension between the tooling you want to build and the language as actually written in the wild.
What Existing Tools Do and Don’t Do
nil is the most mature Nix LSP written in Rust. It provides completion, go-to-definition, find-references, and rename. Its analysis is syntax-level and scope-level: it understands Nix’s scoping rules, can trace identifier definitions through let-in and function patterns, and handles basic completion from attribute set fields. It does not attempt type inference. When you hover over a function application, you get the source location of the function definition, not a type.
nixd takes a different approach by embedding the actual Nix evaluator. Rather than static analysis, it performs evaluation and uses evaluation results to drive completions and hover information. This means it can offer completion items drawn from real nixpkgs evaluation rather than synthetic approximations. The trade-off is that evaluation-based analysis is slow, cannot report errors in unevaluated code paths, and cannot tell you about type mismatches before evaluation fails.
Neither nil nor nixd produces diagnostics for type errors. A project that adds type checking is doing something categorically different from either of them.
The TypeScript Precedent and Its Limits
TypeScript remains the canonical example of adding a type system to a dynamically typed language, and most of the architectural lessons transfer. Gradual typing with an escape hatch (any in TypeScript, something equivalent in Nix) allows the type checker to handle real-world code that has untyped regions. Structural typing matches how Nix’s attribute sets actually work. Type declaration files (.d.ts) provided a path for typing existing JavaScript libraries without modifying them, and an analogous .d.nix format could type builtins and nixpkgs exports without touching the originals.
But TypeScript had advantages Nix does not. JavaScript identifiers are always lexically resolvable at the point of use. TypeScript’s structural type system does not need row polymorphism because JavaScript classes and object literals do not use the same open-pattern syntax Nix function arguments do. And TypeScript was designed by a team at Microsoft with significant resources and the ability to control what features were supported.
For Nix, you need row polymorphism to handle { a, b, ... }: patterns correctly. You need a story for with that does not reject idiomatic code. You need a treatment of import that does not require evaluating arbitrary files. These are requirements that go beyond the TypeScript playbook.
LSP Architecture Choices
Beyond the type theory, building an LSP requires specific engineering decisions. The standard modern approach is tree-sitter for parsing: it produces a concrete syntax tree incrementally, tolerates syntax errors gracefully (so the language server does not lose all information when the file is mid-edit), and tree-sitter-nix already exists as a well-maintained grammar.
For the analysis layer, the state of the art is Salsa-style incremental computation, the framework behind rust-analyzer. Salsa tracks which analysis results depend on which inputs and invalidates only what needs recomputation when a file changes. For a Nix type checker this matters because nixpkgs has tens of thousands of .nix files, and re-type-checking everything on every keystroke is not viable.
The LSP protocol itself specifies the communication layer: JSON-RPC over stdin/stdout, with well-defined request/response schemas for textDocument/hover, textDocument/completion, textDocument/publishDiagnostics, and textDocument/definition. The type checker feeds into publishDiagnostics to report type errors, and into hover to display inferred types. This part of the implementation is relatively straightforward given libraries like tower-lsp for Rust.
What Declaration Files Would Look Like
The builtins are the most tractable starting point for a Nix type environment. There are roughly one hundred of them, they have fixed types, and they are the foundation every Nix expression uses. Providing a hand-written type environment for builtins.map, builtins.filter, builtins.foldl', builtins.attrNames, builtins.mapAttrs, and the rest is straightforward work, even if some of the types are polymorphic and require a more expressive type language.
For nixpkgs, the problem is larger. Nixpkgs exposes tens of thousands of packages and library functions through its attribute set hierarchy, and any type checker that cannot reason about nixpkgs.lib or the most common stdenv.mkDerivation call sites will have limited practical utility. TypeScript had DefinitelyTyped for this: a community-maintained repository of declaration files for popular JavaScript libraries. Nix would need something equivalent, and the initial investment would be significant.
Nickel Shows the Alternative Path
Nickel is the most serious attempt to build a typed configuration language in the Nix tradition from scratch. It uses gradual typing with blame tracking: type contracts are enforced at runtime at the boundary between typed and untyped code, and when a contract is violated, the blame mechanism identifies which side of the boundary is responsible. Starting from scratch allowed Nickel to make with impossible and import bounded in ways that make type inference tractable. The 1.x series has been actively developed and is practically usable.
The instructive comparison is not that Nickel is better or worse, but that it demonstrates the cost of legacy. Typed Nix has to work with all existing Nix code, including with, untyped imports, and open attribute sets. Nickel had no such constraint. Retrofitting types is always harder than designing them in from the beginning, and a Nix type checker is doing the harder thing in service of the larger existing ecosystem.
That trade-off is worth making. The amount of Nix code in production, the size of nixpkgs, and the number of NixOS configurations written over the last decade mean that a type checker that works with real Nix code is genuinely valuable in a way that a typed alternative language cannot yet match. The engineering is difficult, but the target is real.