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

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;
• 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.

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.