The type system

Mica’s type system answers one question about every value: what operations does this type support? The answer is not a list of special cases per type — it is a set of capabilities the type carries, and every rule in the compiler is written against capabilities rather than against names.

That is why the rules generalise. for i := lo to hi works over integers, enums, subranges, characters and error codes, because the rule asks for ordinal and not for int64. A generic constraint T is numeric admits exactly the types carrying numeric. A task parameter is admitted when its type carries plain. One vocabulary, read everywhere.

The capabilities

Two of these carry more weight than their one-line description suggests, and both have their own section below: ordinal, which decides where a value may be counted and dispatched on, and plain, which decides where a value may be transported byte-for-byte.

The primitive types

Read the float row against the integer row: a float is numeric and ordered like an integer, and deliberately not ordinal. It has no successor, no position in a discrete domain, and therefore no place in a case, an array index, or a for control variable. That single missing capability is the whole of the difference the rules see.

The constructed types

The sequence families

Four kinds above hold a run of elements, and programs move between them constantly, so what each one admits is stated here as one table rather than four. They differ in where the elements live and who decides how many there are:

One law governs every value among them, and the two halves are what the rest of this section elaborates: a value owns its elements all the way down, so a copy of a table of growable rows owns its rows, on every road a value travels — assignment, by-value parameter, result, record field, element of a larger aggregate; and a borrow is spelled where it is taken, so a window is formed at a visible Span and can never outlive the storage it names.

What each family admits

✅ admitted · ❌ refused, with the code the compiler prints.

Read the refusals as decisions, because each one is:

• A span writes nothing (5441, 5350). span of T is the borrow’s read face; writing keeps the pointer-spelled binder, so every write path in a program still says address at its call site.
• A span rests in no durable position (5440). A record field and an array element outlive the call that would fill them, and a borrow may not.
• A whole aggregate has no single value to compare (5487). The type still carries the equality capability — that is what admits it as a generic element and as a map value — but the operator over a block of elements is a walk, so the program writes the walk, or compares the fields that identify the value.
• A sequence is never disposed (5190). A dynamic array’s backing belongs to the region that allocated it and is reclaimed with it; the other three own no heap at all.
• An array’s element is a named type (2067, 2068). The diagnostic writes the two declarations it wants, so a jagged table reads as what it is.
• A list of values fills only what owns positions (5492, 5502). A dynamic array names a backing a literal has no region to allocate from, and a span borrows elements it does not own; both are filled by assigning into them after they exist.

The growth freeze

A named span may borrow a dynamic array, and while that window is in scope the compiler refuses to grow the array by name (5488) — an Append, a Resize, a whole-value assignment, or handing address d to a writable pointer parameter. The reason is the one thing a borrow cannot survive: growth may move the backing. The refusal is syntactic and scope-wide rather than a lifetime computation, and a conformant view argument is not caught by it, because the callee receives a window and never the descriptor it could grow.

plain — the transport capability

A value is plain when its bytes are its value: no string, dynamic array, pointer, or other heap-backed part anywhere in its layout. Records and fixed arrays inherit it — they are plain exactly when every part is.

Plainness is what makes a byte copy a correct copy, so it is the admission rule everywhere a value is transported rather than merely assigned:

• a task parameter, deep-copied at schedule;
• a generator parameter, deep-copied when the instance opens;
• a const parameter — the callee’s promise never to write its value, enforced across the callee’s whole body. Every plain type is admitted, and a plain aggregate wider than 16 bytes arrives as one address into caller-owned read-only storage instead of a copy: the same value under the same call-site spelling, with the copy’s absence unobservable by construction. The two modes carry the names the compiler’s own refusals print — by_constant_value for the small value, by_constant_address for the wide plain aggregate — and the procedures chapter teaches when to write the promise;
• a file of T, whose records are written as raw fixed-size images;
• the C boundary, where a Mica value is handed to a foreign frame.

A record holding a string is not plain, and the refusal says so: copying its bytes would hand the destination a second name for one owner’s memory, which is the hidden sharing the value model exists to prevent.

Promotion — what happens implicitly

Mica promotes widening, value-preserving conversions automatically, so mixed-width arithmetic reads the way it does on paper:

var
    small : int32;
    large : int64;
    ratio : float64;
begin
    large := small;          { int32 → int64: every value survives }
    ratio := large;          { int64 → float64: the numeric tower widens }
    ratio := ratio * small;  { the int32 operand promotes to float64 }

The rule is exactly “every value of the source type is a value of the target type”. What that rules out is as important as what it allows: int64 → int32 is not promotion, and neither is float64 → float32, because both lose values. Those need a cast, which is you taking responsibility for the range.

Do not write casts that promotion already performs. large := small as int64 says nothing the compiler did not already know, and it trains the eye to skim past casts — which is exactly where the value-losing ones hide.

Casts — what happens explicitly

x as T is the explicit conversion, admitted when the source type carries convertible. It is one syntax over two distinct operations, and the difference matters:

That distinction is why a float64 cannot ride an 8-byte word in the task spawn protocol even though it fits by size: the trip through the word is a numeric conversion, so 2.5 would arrive as 2. The type system’s answer is that a float is transported by its bytes, like a record — the same plain road.

An error domain carries no convertible at all. A domain value is born from its code names and from the failure channel, never from an integer.

The integer family — one card

Thirteen integer types share one pair of laws, and this card states both whole. Every cell below was produced by compiling one probe program against the shipped compiler, exactly as the sequence-families matrix above was derived. The family: the eight machine widths int8 int16 int32 int64 and uint8 uint16 uint32 uint64; the wide family int[N] / uint[N], whose four everyday widths the integers unit publishes as the importable names int128 uint128 int256 uint256; and bigint, the unbounded integer of the same unit.

What promotes — implicitly, transitively, and only where every value of the source is a value of the target:

Two absences carry the signedness law. A signed value never promotes to any unsigned type, because a negative value would not survive; an unsigned value promotes to a strictly wider signed type only, because the same-width signed type cannot hold its upper half. Everything else is the one widening rule applied transitively.

What casts — explicitly, with as:

The wide family’s rule is one sentence the compiler itself prints: a wide integer converts to and from int64 or uint64 only — widen a narrower integer to a 64-bit machine integer first, and spell a change of width or signedness inside the wide family through that same bridge, one step at a time.

What never converts — bigint stands outside both laws. It is a value like any other — it deep-copies, compares by verb, and travels every road a record travels — but no promotion reaches it and no cast crosses its allocation boundary. Its doors are explicit: FromInteger(x : int64) builds one, Text renders one, Parse reads one back, and Add Subtract Multiply Divide Modulo DivMod Pow Compare are its arithmetic.

Counts and indices — one signed domain

Every count and every index answers in the signed 64-bit domain, so the two meet without a conversion standing between them:

A count is signed because a count is arithmetic: Length(x) - 1 over an empty sequence is minus one, which is the answer a loop bound needs, and not the largest representable unsigned value.

Two counts read a shape rather than a run. A matrix answers its whole row-major element block — the same count its read view and every reduction over it walk — because a length says how many elements a value has and nothing else; the shape stays in the type, where the program wrote it. A span answers the width of the window it borrows, not the extent of the storage behind it.

Strings and the build encoding

A string is not plain, and it carries one more property no other type has: its in-memory representation is fixed per build, not per value.

--platform linux,amd64,utf-32 compiles every string in the program as UTF-32; --platform linux,amd64,utf-8 compiles every string as UTF-8. Encoding is never a property a single value carries, because a program in which two strings had different representations would need a tag on every string operation.

This has one consequence a program meets on its first line of output:

WriteLn("hello %ls", name);   { correct under utf-32, refused under utf-8 }
WriteLn("hello %s", name);    { correct under utf-8, refused under utf-32 }

The compiler checks the conversion against the build’s encoding and refuses the mismatch, so this is never a silent wrong-output bug. But it does mean one source file cannot print text under both encodings: an example, a tutorial snippet, or a library’s own sources must pick one. Length is unaffected — it answers a count of runes under both encodings — and so is everything that does not name a conversion specifier.

Text that crosses a boundary is a separate question with a separate answer: the net unit puts text on the wire as UTF-8 whichever encoding the program was compiled for, so a utf-32 program and a utf-8 program read each other exactly.

Case totality — every value answered

A case must say what happens to every value of its selector, and the compiler checks that it does. Over a bounded domain — an enum, an error domain, a bool, a subrange, a char, or an integer width through 32 bits — the arms must cover the domain or the statement must carry an else; the refusal counts the covered values against the domain. A 64-bit selector requires an else unless its range arms provably tile the whole domain. A masked case over a bitset always carries its default arm — an else or a full don’t-care pattern — because coverage by masked patterns is not provable. And an else behind arms that cover the whole domain is refused, exactly as a shadowed arm is: it can never fire, and its absence is what makes a later addition to an enum break every total dispatch site by name instead of being silently swallowed. A subrange dispatches over its declared domain: arms tiling 8..17 need no else, because naming a domain buys dispatch over exactly it.

Where the rules read capabilities

The vocabulary above is not documentation of an implementation detail — it is the surface the diagnostics speak:

When a diagnostic says a type “requires convertible” or “must be a plain value”, it is naming the row of this table it consulted — which is why the fix is usually to change the type rather than to argue with the rule.

Where a generic constraint is enforced

A constraint is checked where an operation happens, not where a type is merely stored. A generic type template holds its parameters without ever operating on them, so its parameter list carries no constraint of its own:

type Box of T = record item : T; end;

var
    counted : Box of int32;
    named : Box of string;    { admitted — a box only stores }

The constraint arrives with the first function written over the type, and it is that call which is refused:

function Unwrap(b : Box of T) : T;
gen
    T is numeric;

analyzer error 5210: type argument 'string' for type parameter 'T' does not
satisfy its constraint (requires numeric)

The division is deliberate: bounds belong on the functions that act, not on the definitions that hold. It keeps a container usable at every type it can physically store, and puts the requirement exactly where the requirement is real.