Vitte Type System v1

This is the normative contract for the canonical HIR type checker. Each rule is linked to an implementation procedure, production tests, and registered diagnostics by schemas/type_system/rules.json.

Judgments

• Gamma |- e : T: expression typing.
• Gamma |- s => Gamma': statement and environment transition.
• Gamma |- A <= E: directional coercion.
• Impls |- T : Trait: visible trait evidence.
• Variants |- match exhaustive: finite pattern coverage.

Normative rules

T-LITERAL, T-NAME, T-DECLARED-TYPE, T-ASSIGN, T-RETURN, T-UNARY, T-BINARY, T-CONDITION, T-BRANCH, T-CALL, T-GENERIC-INFER, T-GENERIC-BOUND, T-MEMBER, T-METHOD, T-CAST, T-COERCE, T-IMPL, T-COHERENCE, T-CONSTRAINT-ACYCLIC, and T-MATCH-EXHAUSTIVE.

The complete premises and conclusions are maintained in the adjacent Markdown specification. CI rejects missing implementation symbols, tests not called by the production run list, and unregistered diagnostic codes.