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.

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.