Summary

Vera's type checker permits Int <: Nat (with verifier-enforced non-negativity via Z3) AND Nat <: Int (widening, always safe). This bidirectional subtyping is documented in vera/types.py:204-210 and is a deliberate design choice, but it doesn't appear in any user-facing documentation. Agents discover it by writing array_length(...) (formally typed @Int), feeding it into a @Nat position, and being surprised when the type checker accepts it.

Why it matters

Two recent reports surfaced this:

1. array_length "returns Int but works as Nat" — an agent wrote a Conway's Life program, used array_length inside a @Nat-typed expression, and was confused when it worked. They wrote nat_to_int(array_length(...)) defensively in some places before realising it wasn't needed. Documented gap fixed in PR SKILL doc fixes + ROADMAP browser-target tier from Conway's Life agent experiments #601 as a tweak to the SKILL comment, but the underlying language feature is still implicit.

2. Inconsistency across docs — spec/09-standard-library.md:571 says array_length returns @Int, vera/README.md:317 says Int, the registration in vera/environment.py:515 says INT, and the SKILL just got changed to say Nat (PR SKILL doc fixes + ROADMAP browser-target tier from Conway's Life agent experiments #601). All five documents are individually defensible but collectively confusing.

Proposed fix

Add a brief "Int and Nat compatibility" subsection in spec/03-types.md (or wherever primitive types are introduced), explaining:

• Nat is Int refined as >= 0 — they share a runtime representation
• Nat <: Int always (widening); Int <: Nat permitted at type-check time, verifier discharges the refinement
• This is why functions like array_length, declared Int, can flow freely into Nat positions
• Practical implication for users: don't insert nat_to_int defensively; the conversion is implicit and verified

Plus a short cross-reference in SKILL.md so agents reading the agent-facing doc see it.

Alternative: change the registration

A more invasive fix would be to change array_length's registration from INT to NAT to match user expectations. This is cleaner for users but requires investigation of:

• Whether other built-ins flow array_length's result through paths assuming INT
• Whether the WASM ABI is affected (probably not — both are i64)
• Whether the verifier has any code paths that key off the formal type

This is the more disruptive option. The doc-only fix is the conservative starting point.

Acceptance

• A user reading the spec or SKILL can answer "is Nat assignable to Int and vice versa?" with one read
• The spec primitive-types section explicitly lists the bidirectional subtyping rule
• Cross-references from SKILL.md and vera/README.md point at the canonical explanation