Unison parity

Clay’s rule is parity first: the same terms, types, hashes, accepted and rejected programs and runtime behaviour as Unison, with only the surface syntax different. Deliberate language changes come after parity. Unison’s own tool (UCM 1.4.0) is the oracle.

How it is measured

Every definition of a real Unison library is read from the library’s stored form, printed as Clay source, put through Clay’s own front end, and its hash compared with the original (a “round trip”). Where the original hash comes from an older Unison than UCM 1.4.0, the printed program is also handed to UCM itself and the two hashes compared. A second run prints no type signatures at all, so Clay has to infer the type, and UCM checks that it infers the same. A third run makes small ill-typed edits and checks that Clay and UCM reject the same programs.

Where it stands (2026-10-30)

Measure	Result
Hashing of stored Unison code, four libraries (about 44,000 definitions)	100% identical
@unison/base written back as Clay and hashed, with signatures	97.5% agree with Share or with UCM; 143 of 7,995 cannot be printed yet; 35 are rejected by Clay
Same, with every signature removed (Clay infers), through UCM	about 99.3% of what is printed agrees; six known cases where the inferred type differs, each refused rather than stored
Ill-typed edits (7,500 over 1,600 definitions)	Clay rejects 7,517 mutants; only 4 cases where Clay accepts and UCM does not, none left that is a Clay bug except one subtlety about function equality
The libraries’ own tests, run in Clay’s engine in the page	1,032 of 1,077 pass; the rest need cryptography or compression builtins

Built as strict parity along the way: #hash references to library code, abilities on any arrow of a function type, Unicode and ! in names, first-class handler continuations, a declared but unperformed ability being accepted, and builtin("Name") for any Unison builtin.

What is left

• The checker’s handling of ability rows is a set of approximations of Unison’s algorithm. The plan is to port the relevant part of Unison’s typechecker instead of adding cases; this is what the remaining inference differences share.
• Some definitions cannot yet be written back as Clay (nested forall, special float values, a few pattern forms).
• Cryptography, compression, random bytes and tracing in the page engine; sockets, TLS and processes only against UCM.
• Unison’s source-level name rules (suffix resolution, block-scoped use, literate docs).

The full plan, with the missing pieces on both sides, is in docs/parity-methodology.md in the repository; the register of every remaining difference is docs/parity-divergences.md.