Mere type-checker — written in Mere, running in the browser

Paste a Mere expression or a full file on the left and press Infer. The Wasm module on this page tokenizes, parses, and runs Hindley–Milner inference on your input — all written in Mere itself, no server round-trip. The companion pages self-host fmt and self-host REPL cover the format and evaluate sides of the pipeline; this one closes the §S2.B loop.

Source: typer.mere (HM unifier + generalize / instantiate + decl driver), parser.mere, lexer.mere, bridged by selfhost-tyck.mere. The shared AST lives in contrib/parser/ast.mere.

(press Infer to type-check)

Pipeline

Four contrib libraries combine into the Wasm running on this page:

1. lexer.mere — source → tokens
2. parser.mere — tokens → AST
3. typer.mere — AST → type (this stage)
4. selfhost-tyck.mere — DOM glue (textarea → parse_and_infer → output)

typer.mere implements a textbook Hindley–Milner type inferencer with explicit substitutions ((int, ty) list), monomorphic infer over the expression AST, let-polymorphism via scheme = int list * ty and generalize / instantiate, pattern type checking that flows mono bindings through match arms and destructure-lets, permissive constructor / record handling (the field-by-field registry check is deferred — see "Limitations"), and top-level decl threading via infer_decl / infer_decls.

Cross-validation

dune runtest runs the self-host typer side-by-side with the OCaml-side Pipeline.type_of on a set of monomorphic source strings and asserts the displayed type strings match. As of the closing Stage 52f commit there are 12 such cross-validation cases — they're the same harness pattern the §S2.A self-host evaluator uses.

Limitations

• Permissive constructors and records. Without a registry of TopType / TopRecord declarations, the typer treats any constructor as producing a fresh meta and any record literal as the nominal TyCon name []. Field types and constructor argument types aren't checked. This is enough to type the §S2.A REPL programs but doesn't reject mistakes that the OCaml-side typer would.
• No effect / borrow / capability inference. The self-host typer covers the core HM slice. Phase 11+ borrow-check, Phase 36 effects, and Phase 8 capability inference are deferred — see DEFERRED.md §8.5.
• Errors abort the Wasm instance. Unbound variables, occurs-check failures, and type mismatches surface as fail calls that trap the Wasm. Reload the page to recover.
• Type variable names differ from the OCaml side. The self-host prints unresolved metas as '_0, '_1, …; the OCaml side uses 'a, 'b, …. Same semantics, different pretty-printer.

Why this matters

Phase 52 closes §S2.B — the self-host type-checker. Combined with §S1 (parser + fmt, Phase 49–50) and §S2.A (evaluator, Phase 51), Mere can now parse, format, type-check, AND evaluate its own source code, in the browser, with no server round-trip.