The Eidos-level builtin signature table (doc/eidos.md §7, doc/synolon.md §6): the signature scheme every Prim occurrence must instantiate, and the one-way matcher the linter checks occurrences with.

Matching is first-order and unification-free: scheme variables bind to the occurrence type's subterms, bindings must agree (up to natNorm), and everything else compares structurally. Type-level arithmetic on the scheme side (Vec ((i + n) + m) a and the like) cannot be inverted by matching, so arithmetic subterms become deferred equations, checked only when substitution makes both sides nat-closed and skipped otherwise — the check is deliberately partial there (sound: it never rejects a correct instance).

A builtin with no recorded signature (Nothing) has its occurrence types trusted, as all builtins were before this table existed: currently only Extern (its parameter-list type is legacy-shaped).