4. Typechecking

The checker lives in packages/kernel-rs/src/check.rs, the same Rust crate as the hasher, so the browser gets a live check with no server. It is deliberately not a port of Unison’s 3,786-line Context.hs; its specification is a corpus of 174 programs recorded from UCM (its verdict and class of error for each).

Two modes

• A definition with a declared type is checked against it.
• A definition without one is inferred: Hindley-Milner, rank-1 polymorphism. A group of mutually recursive definitions is monomorphic while checking, then generalised.

let inc = (n: int): int => n + 1
let idn = (n: int) => n

The inferred type is stored and hashed. To prove it, UCM is handed the code without a signature, infers independently, and hashes; equal hashes prove equal types. Type variables are quantified by first occurrence and their names never reach a hash.

Inference in miniature

infer(env, term):
  Var x          -> instantiate(env[x])                    # fresh type variables for a generalised scheme
  Lam x body     -> t = fresh(); r = infer(env+{x:t}, body); return t -> r
  App f a        -> tf = infer(f); ta = infer(a); r = fresh()
                    unify(tf, ta -> r); return r
  Let x v body   -> tv = generalise(infer(v)); infer(env+{x:tv}, body)

unify walks two types, binding variables and failing on a clash; an occurs check prevents infinite types. Effects ride on arrows (a ->{Console} b) as one more thing to unify.

Errors point at the expression

The checker reports a child-index path (e.g. “root, child 1, child 0”) rather than a text position. A side table (spans.ts) maps paths back to source ranges, so nothing positional ever reaches a stored object or a hash. Messages are Clay-worded (messages.ts), with type names shown as int/string/bool.

One quirk copied from Unison: delayed computations

thunk(e) is Unison’s do. Its hidden parameter has no annotation, so it is a fresh type variable, which is how apply(thunk(7), "x") typechecks. When a definition (or a let, or a let rec group) finishes and the variable is still free, the checker sets it to Unit, as UCM does at generalization; that is why a lone thunk(5) is () => int and why a thunk bound with let and used with a string is an error. The binder is named () in the kernel term (names never reach a hash) so the checker can recognize it. UCM is the authority: the corpus case “thunk is not forced to unit” and thunk-relaxed.test.ts pin both behaviours.

What it does not do (honest list)

switch exhaustiveness is checked (including nested and list patterns); a declared-but-unused ability is refused (stricter than UCM); function values without annotations are refused because UCM adds an ability variable we do not fully model. See docs/open-issues.md.

Next: The oracle and the store.