Type Inference
The largest single area in the codebase (~12,700 lines): a reusable Hindley-Milner engine (pipeline::type_checking::type_engine, 5,688 lines — type variables, substitution, unification, type schemes) driven by an AST-walking inference pass (pipeline::type_checking::inference, ~6,973 lines across type_checking/inference/mod.rs and type_checking/inference/{declarations,expressions,lowering,narrowing,patterns}.rs). The engine/pass boundary is real, not incidental: type_engine is pub mod (usable by move_check and type_checking::construction too, both of which import from it directly), while type_checking::inference is a private submodule (mod inference; in type_checking/mod.rs) — only the driving pass is type_checking-internal, not the machinery it's built on. Owning crate: metel-frontend.
The pass that consumes this section's output to build the typed IR (type_checking::construction) is a separate section — see Type Construction.
Model
Inference describes programs in terms of variables, constraints, and schemes, then solves those constraints into types. Let-polymorphism is central: generalization records which variables are abstract, and each use receives fresh variables rather than sharing one accidental concrete choice (instantiation, generalization). Unification rejects infinite types (occurs check). The registry supplies the nominal facts that structural unification cannot infer on its own (type definitions).
This pass owns semantic decisions that require unsolved information, including ?
coercion and opaque-return validation. Construction consumes the result; it does not
silently infer it again (pass boundary). A
let-polymorphic closure remains in the scheme environment precisely so calls continue
to instantiate it (polymorphic closures).
Verifiable architecture claims
Owner metel-frontend unless a requirement names another.
Requirement №1
Type inference is Hindley-Milner with let-polymorphism: instantiate gives each use of a generalized binding fresh type variables, so one binding can be used at different types without the uses interfering.
Requirement №2
TypeDefinitionRegistry namespaces struct and enum definitions per declaring module, so same-named types in two modules keep distinct field and variant sets, including across merge_from. Block-local type ids are disjoint from name-resolver SymbolIds.
Requirement №3
?'s error-type compatibility is decided in inference, not construction: infer_propagate_error calls ctx.has_from_impl(target, source) when the error types differ and rejects a missing From impl as T0007.
Requirement №4
Inference and construction are separate passes: inference solves constraints and hands construction a substitution, frozen resolution facts and schemes; construction rebuilds typed IR from them and never runs the constraint solver, only best-effort matching when re-typing a generic body at a call.
Requirement №5
Let-bound polymorphic closures are represented in the polymorphic scheme environment rather than retained as a monomorphic fallback binding. Call sites instantiate the scheme; preserving an ordinary monomorphic environment entry would silently bypass that instantiation path.
Requirement №6
unify performs structural unification over InferType with an occurs check: binding a variable to a type that contains it (?t0 = ?t0[], ?t0 = (?t0) -> i64) is rejected as an infinite type rather than looping or being silently accepted.
Requirement №7
generalize quantifies a type over every free type variable that does not also appear free in the surrounding environment, so a variable still being solved elsewhere is never wrongly captured into a scheme.
Requirement №8
Array literals retain their intrinsic fixed length during inference, and
structural aspect-bound lookup may satisfy that sized type through the existing
one-way [T; N] → [T] coercion without changing the expression's type identity.
Known limitations
LIMIT-TYPE-INFERENCE-002 — Field access needs a concrete receiver type at the access site. A field access on an unannotated parameter is rejected; add a type annotation. Open record ↗knownLIMIT-TYPE-INFERENCE-003 — .. is not supported in an anonymous record pattern. A pattern ending in .. is rejected for a concrete anonymous record; name every field. Open record ↗knownLIMIT-TYPE-INFERENCE-005 — TypeVar identity is a global number, and generator ranges are kept apart by hard-coded offsets. A TypeVar is just a u32, so every generator in a run must start past the others; the frontend does that with unguarded constants (10,000, 1M-5M) scattered over six files. Open record ↗knownLIMIT-TYPE-INFERENCE-006 — Type checking is sequential by construction: one shared generator, one export generator, Rc state. Inference threads one &mut generator through every pass and one export generator through every module, and its context uses Rc, so modules cannot be checked in parallel. Open record ↗knownLIMIT-TYPE-INFERENCE-007 — Type checking time grows super-linearly with the number of functions in a module. Two confirmed O(n) per-function costs (metel-core#1232) cut an 8,000-function module from ~79s to ~6.6s; a smaller super-linear residual remains, unprofiled. Open record ↗Resolved (9)
LIMIT-TYPE-INFERENCE-004 — List<T> iteration. List<T> implements Iterable<T> with an independent cursor per loop. Open record ↗resolvedLIMIT-TYPE-INFERENCE-008 — Field-wise Clone is not entailed for a borrowed open row. A where all R: Clone grant on a borrowed open-row parameter is rejected before its body can be checked. Open record ↗resolvedLIMIT-TYPE-INFERENCE-009 — A partial nominal residual cannot be coerced to a row-conditional dyn aspect. Row-conditional dispatch works on a partial nominal residual, but coercion of that receiver to dyn Aspect fails. Open record ↗resolvedLIMIT-TYPE-INFERENCE-010 — A transparent public alias omitted its nominal type dependency. Alias expansion erased module context for nominal declarations referenced in the alias target. Open record ↗resolvedLIMIT-TYPE-INFERENCE-011 — A field-wise Clone grant does not entail Clone for an open-row record. An owned generic row with where all R: Clone cannot clone the entire open-row value inside its body. Open record ↗resolvedLIMIT-TYPE-INFERENCE-012 — Field-wise Clone is unavailable for records imported from another module. A public nominal record imported from another module has no visible field-wise Clone method, even when every field is Clone. Open record ↗resolvedLIMIT-TYPES-001 — RFC-0121 open rows were incomplete. Resolved: row extension, reusable row positions, decomposition, and row-conditional implementations are implemented. Open record ↗resolvedLIMIT-TYPES-002 — RFC-0123 field-wise row constraints were incomplete. Resolved: where all R: Aspect is enforced at calls and supplies the definition-time entitlement required for abstract by-value row narrowing. Open record ↗resolvedLIMIT-TYPES-004 — RFC-0173 generic-body checking was incomplete. Resolved: generic bodies retain declared bounds and row facts, and report rigidity failures at the causal expression. Open record ↗