Types & inference

Built-in types

The primitive types are int (64-bit, signed, the default integer type), string, bool, float, bytes and unit. On top of them: list<T>, dict<T>, option<T>, tuples, and the user-declared records, variants and abilities (each has a page: Floats & bytes, Lists, dictionaries & options, Tuples & unit, Records, Variants & switch). Generics take one to N type parameters on records and variants, one on abilities.

Optional annotations, real inference

A top-level definition’s parameter types, return type, or both may be left off, and the checker infers what’s missing. This isn’t a stub: it’s a real Hindley–Milner core (rank-1 polymorphism; a group of mutually recursive definitions is treated as monomorphic while it’s checked, then generalized). The inferred type is stored and hashed exactly like a written one, and because the type is part of a definition’s identity, Clay can check itself against UCM by comparing hashes — UCM, given the same code with the signature stripped, infers independently, and an equal hash proves an equal type.

let inc = (n) => n + 1

let apply = (g, x) => g(x)

apply’s parameter g is itself a function — a higher-order argument. Getting this to infer, print and hash correctly (matching an implicit detail of how Unison itself models it) was one of the more fiddly rungs of this checker; it’s been solid since 2026-09-23.

Named type variables

An annotation may name a type variable with a leading quote. Variables are quantified implicitly, by first occurrence, exactly like the variables in a Unison signature, and they are rigid inside the body.

let pick = (x: 'a, y: 'a): 'a => x
let apply = (f: ('a) => 'b, x: 'a): 'b => f(x)
let bad = (x: 'a): 'b => x   // refused: expected `b` but found `a`

An annotation is part of a definition’s identity, as in Unison: pick above is declared on ONE variable, so it is a different (less general) definition from the inferred (x, y) => x, which has two. A curried function type with a shared effect variable is written with an effect list on each arrow, <'g>(nat) => <'g>('a) => 'a.

A parameter that works for every type (rank-2)

A function-typed parameter can be polymorphic itself: the function it receives must work for every a, so the body may use it at several types. The binder goes in front of the function type, with bare lowercase names (a tick variable such as 'e there would read as an effect variable):

let both = (f: <a> (a) => a): (int, string) => (f(1), f("x"))
let ok = (): (int, string) => both((x) => x)
let bad = (): (int, string) => both((x) => 1)   // refused: expected `a` but found `int`

This is Unison’s nested forall, and the order of the names is part of the type, so it is part of the hash.

Still refused, with a reason

The checker is deliberately conservative rather than guessing. Refused today, each for a concrete reason rather than a missing case:

• A function value that’s just another name for a function (let g = add, as opposed to a (params) => body written out) — a different, not-yet-attempted question about how a non-lambda function-typed definition should print.
• A return type with unannotated parameters — there’s nothing to hang the parameter types on.
• A local let is monomorphic — stricter than Unison, which generalizes local bindings; never silently wrong, just narrower.
• Inference stops at the first failing group rather than collecting multiple errors across a file in one pass.
• A float literal and an int never mix silently: convert with Float.fromInt / Float.truncate.

Unison’s own comparison operators are polymorphic ("a" < "b" typechecks in Unison); whether Clay should keep that or restrict </> to numbers is an open question, not yet decided.