---
name: eliot-monomorphize
description: Use when editing, debugging, or reasoning about code under `lang/src/com/vanillasource/eliot/eliotc/monomorphize/` — the NbE (Normalisation by Evaluation) type checker for Eliot. Covers the semantic domain (SemValue), the bidirectional checker, the evaluator, pattern unification, and the TypeStackLoop that processes type stacks uniformly without any concept of "generic parameters."
---

# monomorphize: NbE type checker

## Scope of this skill

This skill governs all code under:

```
lang/src/com/vanillasource/eliot/eliotc/monomorphize/
├── fact/
│   ├── GroundValue.scala              (output: Direct, Structure, Type)
│   ├── MonomorphicValue.scala         (output fact: signature + runtime)
│   ├── MonomorphicExpression.scala    (output expression ADT)
│   └── NativeBinding.scala            (CompilerFact: vfqn → SemValue)
├── domain/
│   ├── SemValue.scala                 (VType, VConst, VLam, VPi, VNative,
│   │                                    VTopDef, VMeta, VNeutral, Spine)
│   ├── Env.scala                      (Vector[SemValue] + names; de Bruijn levels)
│   └── MetaStore.scala                (IntMap[Option[SemValue]]; fresh/solve/lookup)
├── eval/
│   ├── Evaluator.scala                (eval, applyValue, force, semToGround)
│   └── Quoter.scala                   (SemValue → GroundValue read-back)
├── processor/
│   ├── SystemNativesProcessor.scala   (Function → VPi, Type → VType, Bool primitives)
│   ├── DataTypeNativesProcessor.scala (type ctors → body-less VTopDef; spine grows on apply)
│   ├── MatchNativesProcessor.scala    (handleCases/typeMatch impls → VNative; reduces match)
│   ├── UserValueNativesProcessor.scala(user defs → VTopDef with lazy thunk)
│   └── MonomorphicTypeCheckProcessor.scala (entry point; builds refinement map; → TypeStackLoop)
├── unify/
│   └── Unifier.scala                  (pattern unification + postponement + TypeRefinement hook)
└── check/
    ├── Checker.scala                  (bidirectional check/infer)
    ├── CheckIO.scala
    ├── CheckState.scala               (env, nameLevels, unifier)
    └── TypeStackLoop.scala            (uniform top-down fold over type stack)
```

and its sibling tests under `lang/test/src/com/vanillasource/eliot/eliotc/monomorphize/`.

`monomorphize` is the sole monomorphic type-checker package. The prior experimental siblings (`monomorphize2`, `monomorphize3`) have been deleted; this package was promoted from `monomorphize3`.

## How NbE works

The core idea: ORE (syntax) is evaluated into `SemValue` (semantics) via Scala closures. Type equality becomes structural equality of normal forms. There is no constraint set, no worklist, no separate solving phase — unification happens locally as the checker walks the ORE.

### The semantic domain (`SemValue`)

| Variant | What it represents | Produced by |
|---|---|---|
| `VType` | The type of all types | Constant |
| `VConst(ground)` | Non-function ground values: literals (`42`, `"hi"`), compile-time `Bool` (`Direct(true/false)`) | Evaluator (literals), Bool natives |
| `VLam(name, closure)` | Runtime lambda closure | Evaluator (always, for `FunctionLiteral`) |
| `VPi(domain, codomain)` | Function type (dependent or non-dependent) | Checker (when checking `FunctionLiteral` against `VType`), `Function` native |
| `VNative(paramType, fire)` | Primitive awaiting a concrete argument | SystemNativesProcessor (Function, Bool ops), MatchNativesProcessor (handleCases/typeMatch) |
| `VTopDef(fqn, cached, spine)` | Lazy top-level definition **and** applied type/value constructor | UserValueNativesProcessor (cached body), DataTypeNativesProcessor (body-less) |
| `VMeta(id, spine, expected)` | Unsolved metavariable | Checker (fresh allocation via `MetaStore.fresh`) |
| `VNeutral(head, spine, tpe)` | Stuck application on a variable head | Evaluator (unresolved `ParameterReference`) |

### Type/value constructors are body-less `VTopDef`s

`DataTypeNativesProcessor` binds every type constructor (and abstract `type`) to
`VTopDef(fqn, None, SNil)`. Applying type args just grows its spine (`applyValue` on a
`VTopDef` appends). So `Int[2, 5]` is `VTopDef(IntFQN, None, [VConst(Direct(2)), VConst(Direct(5))])`
— **not** a `VConst(Structure)`. `VConst(Structure(...))` only appears after read-back
(`semToGround` / `Quoter`). This is load-bearing: `typeMatch`/`handleCases` dispatch on the
`VTopDef(head, None, spine)` shape, and the unifier's same-FQN case (and the TypeRefinement
hook) operate on these `VTopDef`s.

### VLam vs VPi — who produces what

This is the single most important invariant:

- **The evaluator always produces `VLam` for `FunctionLiteral`.** A lambda is a callable closure, regardless of whether it appears in a type or value position. `eval(env, FunctionLiteral(pn, _, body))` → `VLam(pn, arg => eval(env.bind(pn, arg), body))`.
- **The Checker produces `VPi` when checking a `FunctionLiteral` against `VType`.** In this context, the expression IS a function type (a dependent product).
- **The Checker produces `VLam` when checking a `FunctionLiteral` against `VPi(d, c)`.** The expression is a runtime lambda.
- **The `Function` native produces `VPi`.** `Function[A, B]` evaluates via `apply(apply(nativeFunction, A), B)` → `VPi(A, _ => B)`.

Both are applicable: `apply(VLam(_, c), x)` invokes the closure; `apply(VPi(_, c), x)` returns `c(x)`. `VConst` never represents function types.

### Env and closures

`Env` is `Vector[SemValue]` indexed by de Bruijn level. Variable lookup is by level, not by name. Closures are native Scala functions that capture the current env and body ORE. No ORE substitution ever happens.

`Spine` is a reversed cons list (`SNil | SApp(tail, head)`) for O(1) append.

### How computation runs

`eval` encounters `FunctionApplication(target, arg)` → calls `applyValue(eval(target), eval(arg))`.

- `VLam` → invoke closure (beta-reduction)
- `VPi` → invoke codomain closure (type-level computation)
- `VNative` → `fire(arg)` if arg is concrete, else stuck as `VNeutral`
- `VNeutral`/`VTopDef`/`VMeta` → append arg to spine

`force(v, metaStore)` walks solved metas and unfolds `VTopDef` when the cached body is available.

## Pipeline

### Entry point

`MonomorphicTypeCheckProcessor.generateFromKeyAndFact` delegates to `TypeStackLoop.process`.

### NativeBinding injection

Processors emit `NativeBinding` facts that map `ValueFQN → SemValue`:

1. **`SystemNativesProcessor`** — `Function` → curried `VNative` producing `VPi(A, _ => B)`; `Type` → `VType`; the compile-time `Bool` primitives `true`/`false` (`VConst(Direct(Boolean))`), `&&`, `typeEquals`, `lessThanOrEqual` (all `VNative`s that reduce only on concrete args, else stay stuck).
2. **`DataTypeNativesProcessor`** — Type constructors → body-less `VTopDef(fqn, None, SNil)` (spine grows on apply; see above).
3. **`MatchNativesProcessor`** — the abstract `PatternMatch.handleCases` / `TypeMatch.typeMatch` ability-impl FQNs → `VNative`s that dispatch a concrete `VTopDef(ctor, None, spine)` scrutinee (so `match` reduces during checking). Registered ahead of `UserValueNativesProcessor` (first-registration-wins) to intercept those FQNs. **Only `data` types get `TypeMatch`/`PatternMatch` impls** (auto-generated in `DataDefinitionDesugarer`); abstract `type X` declarations do not, so you cannot `match` on an abstract type's constructor.
4. **`UserValueNativesProcessor`** — User-defined values → `VTopDef(fqn, Lazy(eval(body)), SNil)`. The thunk captures its one-hop binding closure (`collectBindings`), so each `NativeBinding` SemValue is self-contained: holding it lets you `applyValue`+`force` it synchronously with no further prefetch. Uses a concurrent `generating` guard to prevent mutual-recursion deadlocks.

(`StdlibNativesProcessor` in the `stdlib` module similarly binds `inc`. `Bool` is an opaque `type Bool` in lang resources; its values exist only as the compile-time `VConst(Direct(Boolean))` representation — the JVM backend maps `Bool` to a platform boolean.)

### TypeStackLoop — the uniform fold

`TypeStackLoop.process` is the core algorithm:

1. **Pre-fetch** all `NativeBinding`s referenced in type stack levels and runtime body.
2. **Walk type stack top-down**: reverse the levels, fold with `expectedType = VType`. For each level: `checker.check(level, expectedType)`, then `expectedType = eval(level)`.
3. **Apply explicit type args**: fold `apply(sig, eval(typeArg))` for each, binding the type parameter name in the checker's state.
4. **Instantiate remaining**: peel any leftover `VLam` closures (phantom type parameters) by applying fresh metas.
5. **Check runtime body** against the monomorphized signature.
6. **Drain unifier**, report errors, quote signature to `GroundValue`.

**The fold body is identical for every level.** There is no branch for "is this level a type parameter?" Generics emerge naturally from `FunctionLiteral` levels being checked against `VPi` kinds from above.

### Bidirectional checker

Two modes:

- `check(tm, expected)` — checks a term against a known type. The `check` fallback path calls `infer`, then `instantiatePolymorphic` (peels leading `VLam`s with fresh metas), then unifies.
- `infer(tm)` — infers a term's type.

Key cases:

- **`ValueReference`**: fetch binding, fetch evaluated signature, apply explicit `typeArgs` via `applyValue`. Resolve ability methods via `tryResolveAbility`.
- **`FunctionApplication`**: infer target, then `applyInferred`. If target type is `VPi`, extract domain/codomain. If `VLam` (polytype at term level), instantiate with fresh meta and recurse. Otherwise unify against fresh `VPi(?dom, ?cod)`.
- **`FunctionLiteral` with annotation**: eval parameter type, bind, check body against return type.
- **`FunctionLiteral` without annotation, checked against `VPi`**: use `VPi`'s domain directly.

### Unifier

Pattern unification on `SemValue`s with postponement:

1. Force both sides.
2. `VType` vs `VType` → success.
3. `VConst(g1)` vs `VConst(g2)` → structural `GroundValue` equality.
4. `VPi`/`VLam` → extend with fresh variable, unify under binder.
5. Eta: `VLam(_, c)` vs other → unify `c(fresh)` against `apply(other, fresh)`.
6. `VNeutral` vs `VNeutral` with same head → zip spines.
7. `VMeta` → pattern rule: empty spine → solve directly; non-empty → postpone.
8. `VTopDef` vs `VTopDef` with same FQN → **TypeRefinement hook** (below) if the FQN has a custom refinement, otherwise zip spines.
9. Otherwise → error.

`drain()` retries postponed constraints until stable (no progress → stop).

### The TypeRefinement hook (dependent-type assignability)

`Unifier` carries `refinements: Map[ValueFQN, SemValue]` (default empty) — a type-constructor
FQN → its *custom* `TypeRefinement.assignableFrom` impl `SemValue`. In the `VTopDef`-same-FQN
case, if `fqn` has an entry, assignability is decided by **running the impl through the pure
evaluator** instead of by structural spine equality:

```
force(applyValue(applyValue(impl, fr /*target = expected = right*/), fl /*source = actual = left*/), metaStore) match {
  case VConst(Direct(true,  _)) => this                              // accept (e.g. range widening)
  case VConst(Direct(false, _)) => addMismatch(fl, fr, context)      // reject
  case _                        => unifySpines(...)                  // stuck → structural (still solves metas)
}
```

Direction matters: `unify(l = actual, r = expected)`, so `assignableFrom(target = expected, source = actual)` — accepts widening, not narrowing. The fall-back is what keeps generics working: when bounds contain unsolved metas the `lessThanOrEqual`/`typeEquals` natives stay stuck → the result is neither `true` nor `false` → ordinary `unifySpines` runs and solves the metas.

**Building the map** (`MonomorphicTypeCheckProcessor.buildRefinements`): scan the value's type
stack + runtime for `Qualifier.Type` value references; for each constructor that has a *custom*
`assignableFrom` impl, add it. Detection is **non-erroring**: scan the constructor's module names
(`getFact(UnifiedModuleNames)`) for an `assignableFrom` `AbilityImplementation`, confirm with
`AbilityMatcher.matchImpl`, then `fetchBinding`. It must NOT demand `AbilityImplementation` /
`AbilityImplementationCheck` for arbitrary types — those emit a hard "does not implement" error
for any type without an impl. A constructor with **no** custom impl is simply omitted; the unifier
then compares it structurally — which *is* the default (structural equality), so no per-type
default impl needs to be generated.

Constraints / gotchas:
- The hook is generic — it fires for any type with a custom `implement TypeRefinement[C]`. Never special-case a concrete type (e.g. `Int`) in the checker/unifier.
- Do **not** auto-generate a default `TypeRefinement` impl per type constructor: types declared across multiple resource files get duplicate markers (overlap errors), `Type` is `VType` (unmatchable), and the default body self-references `TypeRefinement[Type]`. "No impl = structural" already provides the default.
- The hook dispatches on the bare constructor (HKT-style, `TypeRefinement[T]`), so the dispatch query is `Structure(C, Seq.empty, Type)`.

### Quoting (`forceAndConst` / `Quoter`)

Two quoting paths exist:

- **`Checker.forceAndConst`**: the primary path used during type checking. Force, then pattern-match: `VConst` → ground, `VType` → `GroundValue.Type`, `VPi` → `Structure(Map("$typeName" → Function, "A" → dom, "B" → cod))`, fallback → `GroundValue.Type`.
- **`Quoter.quote`**: stricter read-back that fails on `VNeutral`/`VMeta`/`VLam`/`VNative`/`VTopDef`. Currently used less frequently.

## The hard rules

1. **No concept of "generic parameters."** Do NOT extract, count, or classify type stack levels as "type parameters" vs "signature." The TypeStackLoop treats all levels identically. Do NOT use `TypeParameterAnalysis`, do NOT walk leading `FunctionLiteral`s in a type to count type params, do NOT introduce any structure that distinguishes generic from non-generic levels.

2. **The evaluator produces VLam; the Checker produces VPi.** Do not produce VPi in the evaluator. Do not produce VLam in the Checker when checking against VType (that should be VPi). The `Function` native is a VNative that fires to produce VPi.

3. **No ORE rewriting.** ORE is read once into `SemValue` and then forgotten. There is no `substitute(ore, name, replacement)` anywhere in monomorphize. All substitution happens via closure application.

4. **No constraint set.** There is no list of `Constraint(left, right)` objects. Unification happens immediately and locally when the checker encounters a type mismatch between inferred and expected.

5. **NativeBinding pre-fetching.** The evaluator is synchronous and pure — it cannot do `CompilerIO`. All `NativeBinding` lookups must happen before evaluation via `prefetchBindings` / `collectBindings`, which populate a mutable cache the evaluator reads from.

6. **Mutable state management.** `Checker` has a `var state: CheckState` and `Unifier` has `var metaStore/depth/postponed/errors`. State mutations happen in-place. When binding a parameter, always use `state.bind(name, value)` which extends both `env` and `nameLevels` atomically.

## Diagnosing failures

**"Type mismatch" on a correct program.** Check that all referenced values have `NativeBinding` facts. If a `ValueReference` has no binding, the evaluator produces `VNeutral` (a stuck term), and unification fails when comparing it against the expected concrete type. Add the missing case to the relevant processor.

**Infinite loop / stack overflow.** Likely `force` unfolding a `VTopDef` that recursively references itself without the spine growing. `UserValueNativesProcessor` uses a `generating` guard for fact-level recursion, but `force` itself has no depth limit. Check that `force` only unfolds when the cached body is `Some`.

**"Cannot quote lambda"** from `Quoter`. A `VLam` survived to quoting time. This means a polymorphic value wasn't fully instantiated. Check that `TypeStackLoop.instantiateRemaining` peels all `VLam` closures after applying explicit type args.

**Wrong type for a generic value.** Check `fetchEvaluatedSignature` in `MonomorphicTypeCheckProcessor` — it evaluates only the last level of the type stack (via `foldLeft` that discards intermediate results). The signature `SemValue` should be a `VLam` for generic values. Then `applyTypeArgs` in `TypeStackLoop` applies explicit type args and `instantiateRemaining` handles the rest.

**Meta not solved.** After `drain()`, unsolved metas fall back to `GroundValue.Type` via `forceAndConst`'s fallback case. If this produces wrong types, the unifier likely postponed a constraint that should have been solved. Check that `solveMeta` handles the empty-spine case correctly.

**A refinement that should accept is rejected (or vice-versa).** Force `applyValue(applyValue(impl, expected), actual)` mentally: the impl must reduce to `VConst(Direct(true/false))`. If it stays stuck (→ `unifySpines` → structural), the usual cause is a referenced native being unresolved — e.g. `lessThanOrEqual`/`&&`/`typeEquals` not declared in the (test) module, or matching on an abstract `type` constructor that lacks a `TypeMatch` impl ("No TypeMatch.typeMatch implementation found"). Check direction too: `assignableFrom(target = expected, source = actual)`. A spurious "does not implement ability 'TypeRefinement'" means something demanded `AbilityImplementation`/`AbilityImplementationCheck` for an impl-less type — `buildRefinements` must use the non-erroring module-names lookup, not those facts.

## Anti-patterns (reject in review)

- **Inspecting ORE to count or classify type parameters.** No `extractLeadingLambdaParams`, no `TypeParameterAnalysis`, no "how many type parameters does this value have?" question. The type stack fold is uniform.
- **Producing `VPi` in the evaluator.** The evaluator always produces `VLam` for `FunctionLiteral`. Only the Checker and the `Function` native produce `VPi`.
- **Producing `VLam` in the Checker when the expected type is `VType`.** That should be `VPi`. A `FunctionLiteral` checked against `VType` is a type expression (dependent product), not a runtime lambda.
- **ORE substitution inside monomorphize.** There is no `OperatorResolvedExpression.substitute` call anywhere. All binding is via closure capture in Scala.
- **Calling `CompilerIO` from the evaluator.** The evaluator is synchronous and pure. All IO (fact fetching) must be done before evaluation via pre-fetching.
- **Adding a constraint list or worklist.** Unification is immediate and local, not deferred. The only "deferred" mechanism is the unifier's `postponed` queue for non-pattern meta spines.
- **Eagerly allocating metas for type parameters at `ValueReference`.** Implicit instantiation is driven lazily by `FunctionApplication` / `instantiatePolymorphic` / `instantiateRemaining`, not by peeking at the referenced value's structure.
- **Using `Map[String, SemValue]` for the environment hot path.** Env is `Vector[SemValue]` with de Bruijn level indexing. Name-to-level mapping is in `CheckState.nameLevels`, maintained by the Checker, not the Evaluator.
- **Pattern-matching on `SemValue` to count leading `VPi` binders or `VLam` closures.** The checker never asks "how many type parameters does this value have?" It applies what's given and lets unification figure out the rest.
- **Skipping `prefetchBindings` before evaluating.** The evaluator reads from a mutable cache. If bindings aren't pre-fetched, the evaluator produces `VNeutral` for unresolved references, leading to spurious type mismatches.
- **Forgetting to call `drain()` after the check/infer walk.** Postponed unification constraints accumulate silently. Without `drain()`, metas that depend on other metas being solved first will never be resolved.
- **Special-casing a concrete type (e.g. `Int`) in the checker/unifier for refinement.** The TypeRefinement hook is generic over any type with a custom impl. Recognize the *ability protocol* by name (as `MatchNativesProcessor` does for `PatternMatch`/`TypeMatch`); never the type.
- **Auto-generating a default `TypeRefinement` impl per type, or demanding `AbilityImplementation`/`AbilityImplementationCheck` for arbitrary types.** Auto-gen overlaps for split-module types and can't cover `Type`/`Function`; demanding the ability fact for an impl-less type emits a hard error. Detect custom impls non-erroringly (module-names + `AbilityMatcher.matchImpl`); treat "no impl" as the structural default.
- **Returning `false` (not stuck) from the Bool natives on non-concrete args.** `&&`/`typeEquals`/`lessThanOrEqual` must stay **stuck** (return a stuck `VTopDef`) when an argument isn't fully concrete, so the unifier falls back to `unifySpines` and still solves metavariables. Returning `false` would wrongly reject generic/open comparisons.

## Testing

Tests live at:

- `lang/test/src/com/vanillasource/eliot/eliotc/monomorphize/processor/MonomorphicTypeCheckProcessorTest.scala`
- `lang/test/src/com/vanillasource/eliot/eliotc/monomorphize/processor/MonomorphicTypeCheckTest.scala`
- `lang/test/src/com/vanillasource/eliot/eliotc/monomorphize/processor/MatchNativesProcessorTest.scala` — `match` reduction via `handleCases`/`typeMatch` natives.
- `lang/test/src/com/vanillasource/eliot/eliotc/monomorphize/processor/RefinementUnifyTest.scala` — the TypeRefinement hook (accept/reject/structural-fallback; nested-match + `lessThanOrEqual`/`&&` range refinement). `Bool`/`TypeRefinement` are not in `defaultSystemModules`, so tests that use them must register the modules (`ProcessorTest.boolImportContent` / `typeRefinementImportContent`) and the test source must `import eliot.lang.Bool` / `import eliot.lang.TypeRefinement`.

Run them:

```bash
./mill lang.test 2>&1 | grep -v DEBUG | grep "MonomorphicTypeCheck"
```

Tests construct source text inline. Follow the project testing conventions: single-line asserts, assert the `Seq` itself, prefer `.asserting(_ ...)`.

## Facts and keys

- `MonomorphicValue.Key(vfqn, specifiedTypeArguments)` — composite key. Same `vfqn` + different type args → different specialization.
- `MonomorphicValue` fields: `vfqn`, `specifiedTypeArguments`, `signature: GroundValue`, `runtime: Option[Sourced[MonomorphicExpression.Expression]]`. No `calculatedTypeArguments` — NbE folds them into the signature directly.
- `NativeBinding.Key(vfqn)` — maps a value FQN to its `SemValue` for the NbE evaluator.
- `MonomorphicExpression.expressionType: GroundValue` — always fully ground, no free variables or unsolved metas.