How Checking Works

This page explains what the tynix checker actually does, with references to the modules in packages/tynix-core/src that implement each part. It is written for people who want to predict the checker's behavior, write declaration packs, or contribute to the core. For the user-facing rules alone, see the type system overview and the language reference.

The short version: tynix runs Hindley-Milner inference (let-polymorphism, generalization per dependency group, rigid signatures) over a single structural type tree, extended with row-polymorphic records, subtyping for records, numbers and shapes, a consistency relation for the gradual dynamic boundary, soft inference variables that keep injected dependencies gradual, kind inference for higher-kinded aliases, and structural reduction for aliases and conditional types. Types never reach runtime: compilation is pure erasure.

The pipeline

Driver.analyzeText is the single entry point used by the CLI, the language server and the tests:

1. Load the declaration world for the file's workspace (cached per workspace root for the length of one CLI command or LSP request), on top of the built-in builtins prelude.
2. Parse the file (Parser, ParserExpr, ParserType, ParserLexer). Directive comments are scanned first, line by line, and attached to the next line of code.
3. Validate kinds of every alias and term-facing annotation (Kind).
4. Validate indexed annotations such as Vec, Range and Unit (Indexed.validateProgramIndexedTypes).
5. Collect local declare blocks and merge them with the world.
6. Check the root expression (Check.checkProgram).

The first error stops the pipeline. A file therefore reports one diagnostic at a time; check-project reports one per file. Parser and checker errors carry the source span they were raised at (see diagnostics).

Type representation

All phases share one data type, Type in Type.hs. There is no separate elaborated IR: parsing, checking, hovering and emitting all look at the same tree.

Polymorphism outside annotations is stored as a Scheme (a list of quantified variables plus a body). Results are made deterministic with closeMetas, which renames leftover inference variables to t0, t1, ... in order of first appearance.

Several "types" are encodings over TCon and TApp rather than constructors:

• List a is TApp (TCon "List") a, and the dictionary type AttrsOf a is TApp (TCon "AttrsOf") a.
• Vec n a, Matrix r c a and Tensor [d1 d2 ...] a are normalized by Indexed.normalizeIndexedType into one canonical tensor form, so all three spellings compare equal when they describe the same shape.
• Tuple [a b c] is a heterogeneous fixed-length list.
• Range lo hi base and Unit "label" base are numeric refinements and phantom units, interpreted by the subtyping relation.

Inference

Inference lives in Check.hs. It runs in a state monad holding a counter for fresh metas, a substitution map from metas to types, and the set of soft metas (see below). zonk applies the substitution, and bindMeta extends it after an occurs check (failure is TC0016).

The algorithm is syntax-directed. The interesting rules:

Field selection resolves the base type first. any and dynamic absorb the selection; unknown refuses it (TC0008); records look the field up; an open record with a dynamic tail gives dynamic for fields it does not list; a union succeeds only if every member has the field, and joins the results. Selecting from an unsolved meta binds it to an open record { a :: ?f; ...?r }, and selecting a new field from such a row extends the tail. This is row polymorphism: x: x.a + x.b is { a :: Number; b :: Number; ... } -> Number. The field metas created this way are soft.

Soft metas

Some unknowns stand for values tynix cannot know but that are usually polymorphic or overloaded in practice: arguments injected through an attribute-set pattern (callPackage-style { lib, fetchFromGitHub, ... }:) and fields selected from values of unknown shape (lib.mkOption). Their metas are marked soft. Calling a soft meta binds it to dynamic -> dynamic instead of fixing it to the argument types of the first call site, so the next call with different arguments does not fail. Plain lambda binders are not soft and keep full principal types: compose = f: g: x: f (g x) is forall t0 t1 t2. (t1 -> t2) %1 -> (t0 -> t1) %1 -> t0 %1 -> t2.

Literal widening

Singleton literal types are kept where they are useful and widened where they would only cause spurious errors: the default of a pattern field (b ? 2 accepts any Int), the argument of a callee whose type is still unknown, and if branches that are unified because the other side is unknown (so true and false meet at Bool).

let groups and generalization

A let block is checked in these phases:

1. Collect signatures. Duplicate signatures (TC0003), duplicate bindings (TC0004) and signatures without bindings (TC0005) are rejected. Nested paths are merged and inherit (s) a becomes a binding a = s.a. Dynamic names are rejected (TC0022).
2. Put every signed binding in scope with its signature's scheme. This is what allows polymorphic recursion through a signature.
3. Order the unsigned bindings by their free names and split them into strongly connected components. Each component is a group of mutually recursive bindings, processed in dependency order.
4. For each group, give its unsigned members fresh placeholder metas, infer each body, and constrain it against the placeholder.
5. Generalize each member over the metas that do not occur free in the environment outside the group. Metas shared with an enclosing lambda parameter stay monomorphic, as in Hindley-Milner.

Because every group is generalized before later groups see it, a helper is polymorphic for the rest of the let: let id = x: x; in { a = id 1; b = id "s"; } checks, and mutually recursive even / odd solve without annotations.

Signatures are rigid. A signed binding's body is checked against the signature with its quantified variables held abstract (skolemized): inside the body, a is a type that only equals itself. id :: forall a. a -> a; id = x: 1; is therefore rejected with type mismatch: 1 vs a. Other bindings instantiate the signature freshly at every use.

Directives

# @tynix-ignore and # @tynix-expected wrap the attempt to check one let item or the root expression. On failure, the checker discards the attempt's state and recovers by constraining dynamic against the expected type, so a suppressed binding keeps its signature. @tynix-expected on code that checks cleanly is itself an error (TC0006).

Constrain, unify and cast

Three operations reconcile two types. They differ in direction and in how much gradual slack they allow.

constrain actual expected is directional. It is used for signatures, function arguments and recursive placeholders. In order:

1. A fixed-shape sequence (vector, tuple) meeting a plain List is compared through its list view.
2. Metas are bound. A meta passed where unknown or AttrsOf unknown is expected is not pinned to that top type (an unknown attribute set only becomes an open row).
3. Functions compare argument types contravariantly and results covariantly, and the actual multiplicity must be a sub-multiplicity of the expected one (%1 -> may stand in for ->, not the reverse).
4. Records that still contain metas are compared field by field: every required expected field must be present, optional ones may be missing, and a missing field extends the actual record's row when its tail is still open. A record against AttrsOf v constrains the join of its field types against v.
5. Equal types, or isSubtype actual expected, succeed.
6. Gradual consistency is used only when dynamic occurs somewhere in either type. Two unrelated concrete types never pass by consistency.
7. If unsolved metas remain, fall back to unify.
8. Otherwise, for two records, the error names the first missing field (TC0009) or the first field whose type does not fit (TC0013 type mismatch in field ...); anything else is TC0013 type mismatch.

unify a b is symmetric and is used when both sides are partially unknown. It binds metas, recurses through functions (same multiplicity), applications and records (one record's fields must be a subset of the other's, else TC0014), and accepts subtyping in either direction or consistency involving dynamic, returning the join.

checkCast actual asserted is the most permissive. It succeeds if metas can be unified, or if actual <: asserted, asserted <: actual, or the two are consistent. So casts may widen, narrow, and cross any gradual boundary, but 1 as String is still TC0015.

Subtyping and the gradual lattice

Subtyping.hs implements isSubtype, isConsistent and joinTypes. Both sides are fully resolved first (aliases expanded, conditionals reduced, shapes normalized).

The rules, in the order the implementation tries them:

Consistency (isConsistent) is the gradual relation: two types are consistent if either is any or dynamic, or if one is a subtype of the other. The checker consults it only when dynamic actually appears in one of the types, which keeps the escape hatch from blurring two concrete types.

Joins (joinTypes) compute the type of if branches, list elements and union field lookups. any absorbs everything; same-label units join their payloads; tuples join positionally; tensors of equal rank join axis by axis (Vec 2 Int and Vec 3 Int join to Vec (2 | 3) Int); numeric families widen (Nat and Int to Int, otherwise Number); a subtype joins to its supertype; everything else becomes a flattened union.

Kinds and higher-kinded types

Kind.hs infers kinds; there is no kind syntax. The kind language is Type, k1 -> k2 and kind metas.

• Built-in constructors have fixed kinds: Int, String, Bool, Float, Number, Nat, Null and Path are Type; List and Tuple are Type -> Type; Vec, Tensor and Unit take two arguments; Matrix and Range take three.
• Every alias gets a placeholder kind k1 -> ... -> kn -> r with fresh metas. Its body is inferred with the parameters bound to k1 ... kn, and the body's kind is unified with r. Because all aliases get placeholders first, aliases may refer to each other in any order.
• Application f x unifies kind(f) with kind(x) -> ?r.
• Arguments of ->, record fields, union members and type-list items must have kind Type.
• A constructor that is neither built-in nor an alias (for example one only mentioned in a declaration pack you have not loaded) gets a flexible kind, so partial declaration packs do not fail kind checking.
• Every term-facing annotation (signatures, lambda annotations, casts, ambient entries) must have kind Type in the end, else TK0003.

Kind errors are TK0001 (mismatch) and TK0002 (occurs check). This is what rejects Int String and Twice List while accepting Functor List.

Aliases are expanded by Alias.expandAliases. An application is reduced when the head is an alias and at least as many arguments as parameters are present; extra arguments are re-applied to the expansion, which is what lets an alias return a type constructor. Expansion is bounded by a budget of 32 chained expansions per path to keep self-referential aliases from looping.

Conditional types and infer

Subtyping.resolveType normalizes a type before comparison: it erases a top-level forall, expands aliases, normalizes shapes, and reduces conditional types.

Alias.matchPattern walks the checked type and the pattern together:

• infer x binds x to whatever is at that position. A second infer x must see an identical type.
• Functions match if their multiplicities are identical and both sides match.
• Records match field by field over the pattern's fields; extra fields in the checked type are ignored.
• Applications and type lists match component-wise.
• Anything else matches only if it is syntactically equal.

If matching fails, the conditional falls back to isSubtype A P. Consequences worth knowing:

• There is no distribution over unions: a union is matched as a whole.
• A pattern written with -> does not match a %1 -> type.
• A conditional alias that recurses into itself is expanded eagerly and hits the budget; keep conditional aliases non-recursive.
• Output and hovers print the alias as written (ElementOf (List String)); comparisons use the reduced form.

Indexed types

Indexed.hs has two jobs: inferring precise shapes from list literals, and validating shape annotations before the checker trusts them.

Shape inference for a list literal:

Every tensor also has a list view (Vec 3 Int views as List Int, Matrix 2 3 Int as List (Vec 3 Int)), which is how fixed shapes flow into code that only asks for List.

Validation rejects annotations that cannot mean anything: tensor dimensions that are not natural-number-like, Range bounds that are not numeric or are reversed (Range 4 2 Nat), fractional bounds on a Nat range, and Unit labels that are not string literals.

Declarations and the ambient world

Driver builds the set of types that import can see.

• The built-in prelude is the base of every world. It is registry/workspace/builtins.d.tynix, embedded into every binary (as the generated BuiltinPrelude.hs), and it declares builtins plus aliases such as Derivation, DerivationArgs, FetchedSource, PathLike, FileType, TypeName and NameValuePair. Project aliases with the same name win, and a workspace declare "builtins" replaces the prelude's.
• The workspace root is the nearest ancestor of the source file that contains flake.nix, cabal.project, pnpm-workspace.yaml, tynix.config.tynix or a .git directory. Without one, the file's own directory is used, and only the .d.tynix files directly in it are loaded.
• In a real workspace, every .d.tynix under the root is loaded, except inside nested directories that are themselves workspaces. Hidden directories, node_modules, dist-newstyle, dist, target, result and result-* build links, and symlinked directories are skipped. A declaration file never contributes to its own analysis, and it must not contain an expression (TD0007).
• declarationPacks in tynix.config.tynix add files or directories. Packs that live under a registry/workspace/ directory are rebased onto your project root, so their relative targets (../../flake.nix) point at your files.
• Each declare target is resolved relative to the file that contains it, normalizing . and ... The target "builtins" is special and types the builtins identifier.
• A block with exactly one entry named default declares the module's whole value; any other block declares an attribute set of its entries.
• Each target may be declared once per world, else TD0002; duplicate entry names are TD0003.
• Aliases from all loaded declaration files share one namespace with the file's own aliases. Avoid defining the same alias name twice.

import is typed only when its argument is a path literal or a string literal; the resolved absolute path is looked up in the world. Any other import, and any path without a declaration, is dynamic. builtins is the record declared by the prelude (or by the workspace's own declare "builtins"), and the global builtins such as toString, map, throw, import, derivation, baseNameOf, dirOf, fetchTarball, isNull, removeAttrs and placeholder take the type of the matching member.

Erasure and compilation

Compile.hs does not translate anything; it deletes:

• type aliases and declare blocks,
• let signatures (name :: Type;),
• lambda annotations ((x :: Int): becomes x:) and pattern-field annotations ({ name :: String }: becomes { name }:),
• casts (e as T becomes e).

The remaining tree is pretty-printed as Nix. Names, structure, string forms (double-quoted or indented, including their escapes), nested attribute paths and operators are preserved; whitespace is normalized and comments are not carried over. Over a sample of 4000 nixpkgs files, the output parses to the same AST as the input under nix-instantiate --parse. Because the compiler only deletes, the generated .nix evaluates exactly like the .tynix would if Nix ignored the type syntax. tynix compile runs the full analysis first and refuses to emit output for a file that does not check.

Declaration emit (Emit.hs) renders the file's aliases verbatim and a declare block for the compiled .nix path, relative to where the declaration is written. If the root expression is an attribute set (or rec { }, or such a set behind casts) and its type is monomorphic, each field becomes an entry. Otherwise the whole root becomes default, quantified with forall if it is polymorphic.

Diagnostics

Diagnostics.hs assigns every message a stable code, prefixed by phase: TP parser, TK kind checker, TC type checker, TD driver. The message format is [CODE] text, prefixed with line:col: (and a space) when the error has a source span, and codes are never reused. The full catalogue with fixes is in diagnostics.

• Parse errors carry a line and column (3:12: [TP0004] ...) and the Megaparsec excerpt.
• Checker errors carry the span of the innermost expression whose inference failed: every parsed expression is wrapped in a located node, and a failure is attributed to the nearest enclosing one. The CLI prints the start as line:col: [CODE] message; the language server underlines the whole span. A call whose argument does not fit points at the argument, and a signature mismatch at the binding's body. A few errors raised before any expression is inferred, such as TC0022, have no span.
• The CLI prints text diagnostics to standard error and exits 1. With --format json, a structured report goes to standard output instead, versioned by schemaVersion; see the CLI reference.

Known limitations

These follow directly from the design above and are good to keep in mind:

• One diagnostic per file per run; fix and re-run to see the next.
• Implementing records whose fields have their own forall is not accepted yet; declare such values instead.
• Unions are not narrowed by if conditions: isAttrs x, x ? a and _tag checks do not refine x in the branches.
• Constraint contexts (Functor f =>) are parsed but not enforced; there are no type classes.
• Soft metas trade precision for adoption: calls through unannotated injected dependencies are not checked. Annotate the pattern field to check them.
• NixOS modules are typed as ordinary functions; the config / options fixpoint is not modelled.