A type is a name, not a discount from real C

Mirror-C's type checker runs entirely inside the block editor — the machine underneath has no static semantics of its own, so a program that builds is a program the machine is guaranteed to run without a type error. What that checker enforces, and how far the fragment's type universe reaches, is this chapter.

The type universe

Two is the ceiling, for both constructors, by one decision. T a[n][m][k] and T*** are both refused by name — in the block editor, in the type checker, and in the text importer. Nothing about the machine underneath breaks at three levels or three extents; the bound is pedagogical. A three-dimensional array or a triple pointer has no honest two-dimensional picture to draw, and the picture is the thing this tool claims is faithful.

Structs, unions, enums

A struct, union or enum is referred to everywhere by name only. The field or member list is not inlined into the type — it lives in a definitions table on the program, looked up the same way a function call resolves a function name. That indirection is what makes a self-referential shape like a linked list's struct Node { struct Node *next; } expressible at all: inlining the field list would never terminate.

• struct. Drawn as a container of cells, one per field, exactly the way an array's elements are drawn. p->next = q is not a metaphor for reassigning a pointer — it visibly moves the arrow from wherever it pointed to q's target.
• union. One footprint, several views. The members are drawn stacked, and the container is as wide as its widest member — a char view visibly covers only one of the four bytes an int view covers in the same union. Writing one member makes every other member's value indeterminate; reading a member you did not last write reaches IndeterminateRead, the identical stuck reason an uninitialised scalar reaches (see Semantics).
• enum. A named set of integer constants, usable anywhere an int is expected.

sizeof, and const

A cell's on-screen width is sizeof of its type, computed once from the type itself and read by nothing semantic — it is geometry, not behaviour. That distinction is not incidental: an earlier version of the checker keyed a write's truncation rule off a cell's width rather than its type, which quietly admitted bool b; b = 44;, because sizeof(bool) and sizeof(char) are both one byte even though the two types convert differently. The quarter-width rule for char is still exactly a requirement; it is just derived from the type on demand rather than stored as a fact of its own that a rule could accidentally consult instead of the type.

const is a qualifier the machine carries and never reads. All of its force is at the surface: the editor refuses to build any write to a const lvalue, so no program the block editor accepts ever executes one, and the machine underneath needs no rule for it at all. A by-value struct or union cannot be marked const in this fragment — there is no initialiser form for one, so an uninitialisable const object would be inexpressible either way — but a pointer to one can, and const struct S *p is exactly where the qualifier's propagation matters: every field reached back through p inherits the same restriction.

The Typing tab

The Inspector's Typing tab renders the same well-formedness judgement that gates ◉ Load, as a genuine derivation: pick a function, and each statement's premises expand into a classic premises-over-a-bar proof tree with the rule name at the bar's right end. Every judgement in the tree is a button — clicking one selects and centres the block it is about — and the printer icon in the tab renders the selected function's whole derivation as a one-page document.

The context threaded through the tree is not one fixed Γ. It is a sequence of incrementally-named contexts — Γ₀ ⊢ s ⊣ Γ₁, Γ₁ ⊢ s′ ⊣ Γ₂, and so on — because a C function's context genuinely grows with every declaration and shrinks again at every scope exit. A block's closing row visibly reverts to the same context name it opened with, which is the derivation's own way of showing a scope's variables have gone out of it.

The Problems tab

The same checker's diagnostics surface as a clickable list in the Problems tab, with a matching warning icon on the offending block and a running count in the status bar. One checker, three places the same list shows up — nothing here re-derives its own answer.