Values and types

Every Silk expression has one precise type. Expected contexts may select the type of an exact literal before it becomes a value, but an already-typed value changes type only through one of the language's explicitly defined compatibility relations.

Ownership behavior is defined by ownership and borrowing. Function, callable, and match result types are defined by functions, callables, and control flow. This page defines the identities, construction rules, and ordinary compatibility of foundational values, nominal structs and scalar enums, arrays, references, slices, and structural unions.

Terminology

• A value is the result represented by a successfully typed expression.
• A type classifies a value and determines which source operations may accept it.
• A precise type is the expression's own type before an expected boundary performs a compatible injection, widening, or access weakening.
• An expected context is a source position that already requires a type, such as a declared return, parameter, struct field, array element, or assignment destination.
• Contextual literal selection chooses a representable type for an exact literal that has not yet become a typed value.
• Compatibility determines whether an already-typed source value may satisfy an expected type.
• A foundational scalar is bool, char, an integer type, or a floating-point type. A scalar enum is instead a nominal type with one fixed-width integer representation.
• A nominal type is identified by its declaration rather than by the shape of its fields.
• An aggregate is a value containing other values, such as a struct, fixed array, or structural union payload.
• A view provides lexical access to storage it does not own. References, slices, and string values may retain such access.
• Injection places one precise value into a structural union containing its type.
• Widening converts one structural union into another containing every source member.

Foundational type identity and compatibility

TYPE-001 — Foundational type spellings are lowercase and distinct

Status: Confirmed

Silk defines these scalar types:

The foundational non-scalar types are unit (), bottom never, and immutable UTF-8 view string. Every spelling denotes a distinct type. Uppercase forms such as I32, Bool, and String are not aliases; String may instead name an ordinary standard-library owning type.

fn classify(flag: bool, scalar: char, count: usize) -> f64 {
  return 0.0
}

Boundary: Distinct foundational types are not interchangeable merely because their runtime representations could have the same width. u32, char, and f32 remain three different types.

Diagnostics: An unresolved type spelling reports SEM0001. A value declaration used where a type is required reports SEM0018.

Evidence: scalar catalog, integer scalar specification, floating scalar specification, string specification.

TYPE-002 — Unit has one value and never has none

Status: Confirmed

() is both the unit type's spelling and its sole value. A function result omitted from its declaration is (), bare return returns (), and reaching the end of a unit body produces ().

never is uninhabited: no expression completes by producing a never value. An expression of type never is compatible with every expected type because control does not reach that boundary with a value.

struct StopError {}

effect fn stop() -> never ! StopError {
  fail StopError {}
}

effect fn number() -> i32 ! StopError {
  return run stop()
}

The return is valid. stop either propagates its typed failure or does not return; it never creates an i32 or a bottom payload.

Boundary: never is not a default value, null value, or runtime union tag. Source cannot construct, store, inspect, or return a completed never value.

Diagnostics: Unit return mismatches use the ordinary return diagnostic. A never expression receives no conversion diagnostic when used at another expected type.

Evidence: unit result rule, failure bottom rule, type compatibility.

TYPE-003 — Compatibility is exact except for closed named relations

Status: Confirmed

An already-typed value satisfies an expected type when the two types are identical or one of these relations applies:

1. never satisfies any expected type.
2. A precise value injects into a structural union containing its type.
3. A structural union widens into another containing every source member.
4. Callable invocation mode weakens under CALLABLE-003.
5. Effect run access weakens under the Effect ownership rules.

No other subtyping or implicit conversion exists.

fn preserve(value: u8) -> u8 {
  return value
}

Boundary: Numeric width, signedness, representation, array length, ownership, text encoding, and borrow access do not create compatibility. In particular, i32 does not become u8 because its runtime value fits, an array does not decay into a slice, and string does not become owned String.

Diagnostics: The enclosing boundary selects the diagnostic: arguments use SEM0012, struct fields SEM0025, array elements SEM0030, assignments SEM0037, and incompatible union widening SEM0040. Return mismatches report SEM0129.

Evidence: compatibility implementation, callable modes, Effect access.

Scalar values and literals

INT-001 — Integer types have exact signedness and width

Status: Confirmed

The fixed-width integer name states both signedness and value width. u8 through u64 are unsigned; i8 through i64 are signed. usize and isize use the selected target's pointer width: 64 bits on required native targets and 32 bits on wasm32-unknown-unknown.

Every integer type is Copy and cleanup-free. Integer types remain distinct even when two selected types have the same physical width.

fn nativeIndex(value: usize) -> usize {
  return value
}

fn fixedIndex(value: u64) -> u64 {
  return value
}

usize and u64 are not compatible on a 64-bit target despite using equally wide values there.

Boundary: Silk does not promote a narrower integer, change signedness, or convert between fixed and pointer-sized integers implicitly. Such transformations require explicit operations.

Diagnostics: An out-of-range integer literal reports SEM0002. A negative literal selected as usize reports SEM0060. An already-typed mismatch uses the diagnostic of its expected boundary.

Evidence: integer scalar specification, usize specification, scalar catalog.

INT-002 — Integer literals are exact until an immediate context selects their type

Status: Confirmed

An integer literal retains its exact mathematical magnitude until typed. An immediate expected integer type selects that type when the magnitude is representable. Without a numeric context, the literal defaults to i32.

struct Header {
  code: u8
}

fn header() -> Header {
  return Header { code: 255 }
}

The field contract selects u8 for 255. The literal is not first made i32 and then narrowed. Immediate contexts include concrete parameters, returns, struct fields, contextual array elements, assignment destinations, and a known homogeneous operator operand.

Boundary: Context does not retype an existing value:

fn invalid() -> Header {
  let code = 255
  return Header { code }
}

code is already i32, so the field reports a mismatch. A later use cannot retroactively change the binding to u8.

Diagnostics: A literal outside the selected type's range reports SEM0002 before MIR lowering. The diagnostic must retain its exact magnitude rather than a rounded host-number approximation.

Evidence: integer literal specification, literal elaboration tests.

FLOAT-001 — Floating literals select f32 contextually and otherwise default to f64

Status: Confirmed

f32 and f64 are distinct Copy scalar types using IEEE binary32 and binary64 values. A floating literal retains its exact source value until a contextual floating type rounds it; without such a context it defaults to f64.

fn small() -> f32 {
  return 1.25
}

fn defaulted() -> f64 {
  let value = 1.25
  return value
}

Basic floating behavior preserves signed zero and keeps NaN unordered. The complete operation and explicit conversion APIs belong to the expressions and operators reference.

Boundary: Integers do not become floats implicitly, and f32 does not widen to f64 after it has been typed. A conversion must be explicit even when mathematically exact.

Diagnostics: A floating spelling that cannot produce a supported floating value reports SEM0095. Contextual type mismatches use the enclosing boundary's ordinary diagnostic.

Evidence: floating scalar specification, floating tests.

CHAR-001 — char holds exactly one Unicode scalar value

Status: Confirmed

char is a Copy 32-bit scalar whose valid values are Unicode scalar values: 0 through 0x10ffff, excluding the surrogate range 0xd800 through 0xdfff. A character literal contains exactly one scalar, not one byte.

fn snowman() -> char {
  return '\u{2603}'
}

'é' is also one char even though its UTF-8 encoding uses more than one byte. char supports equality and ordering by scalar value.

Boundary: char is not an integer type. Arithmetic is unavailable, and conversion to or from an integer requires an explicit checked or named operation.

import silk.char { fromU32, toU32 }
import silk.option { Option }

fn checked(value: u32) -> Option<char> {
  return fromU32(value)
}

fn scalarNumber(value: char) -> u32 {
  return toU32(value)
}

fromU32 returns Some<char> for 0...0xd7ff and 0xe000...0x10ffff. It returns None for surrogate values and larger integers, without truncating or trapping. toU32 is total because every existing char is already a valid scalar. Canonical string traversal returns char; callers choose toU32 explicitly when they need its integer value.

Diagnostics: A literal containing zero or multiple scalar values reports LEX0007. Malformed escapes and invalid scalar spellings receive their literal diagnostic without constructing a partial char. Supplying u32 where char is required, or char where u32 is required, uses the ordinary type-mismatch diagnostic; fromU32 represents an invalid integer as None rather than a diagnostic or trap.

Evidence: character literal specification, character scalar catalog, character tests, conversion and engine tests.

TEXT-001 — string is immutable UTF-8 text and byte strings are byte views

Status: Confirmed

string is a Copy immutable view of valid UTF-8, distinct from every scalar and from &[u8]. An ordinary text literal has type string and program lifetime. A byte-string literal has type &[u8] and preserves exact bytes.

fn greeting() -> string {
  return "olá"
}

fn firstByte() -> u8 {
  return b"ok"[0]
}

Text-literal equality compares exact decoded Unicode scalar sequences, equivalently their canonical UTF-8 bytes. It performs no normalization, case folding, or locale-sensitive comparison.

Boundary: A byte view remains binary data even when its bytes are valid UTF-8. Forming a string from runtime bytes requires validation or a narrow unsafe operation. A runtime string view retains the lifetime of its backing owner; copying the view does not detach that loan.

Diagnostics: Invalid UTF-8, malformed escapes, and invalid byte values report SEM0085 without publishing partial static data. Lifetime violations use the ordinary borrow diagnostics.

Evidence: static text specification, string specification, string ownership tests.

TEXT-002 — Text conversions and access units are explicit

Status: Confirmed

Silk does not implicitly convert between string, owned String, and &[u8]. Conversions that copy into owned storage, borrow owned storage, expose UTF-8 bytes, or validate bytes are explicit operations. No conversion allocates invisibly.

string has no index operator and no unitless length. APIs name their observation unit, such as byte length, UTF-8 bytes, Unicode scalars, or grapheme clusters.

Boundary: A text literal does not become an owning String because a field or parameter expects one. text[0] is invalid because the intended unit could be a byte, Unicode scalar, or grapheme. Because string is an ordinary Copy view value, it may appear in valid aggregate positions and may itself be borrowed: &string, &mut string, and &[string] follow the ordinary reference, mutation, slice, aggregate-storage, and nested-loan rules. Mutating through &mut string may replace the view value; it does not make the viewed UTF-8 storage mutable. A containing value cannot outlive a runtime string view's backing owner merely because the view is nested.

Diagnostics: Indexing string reports the non-indexable-type diagnostic. Implicit text conversions use the enclosing type-mismatch diagnostic.

Evidence: string access and conversion specification, string type diagnostics.

Constant values

CONST-001 — A constant has an explicit scalar or string type and one static initializer

Status: Confirmed

A const declaration requires a type annotation. Its type is one foundational scalar type or string, and its initializer is one matching literal whose value is valid for that type. Constants do not infer their type, evaluate computed expressions, or hold aggregate values.

pub const limit: i32 = 2
const ratio: f64 = 1.5
const enabled: bool = true
const separator: char = ':'
const pattern: string = r"\d+"

A constant lowers to an immediate value. It has no address and cannot be borrowed, assigned, or moved.

Boundary: Function calls, operators, field access, aggregate construction, and other computed expressions are not constant initializers. An initializer of the wrong scalar type is also invalid.

Diagnostics: A constant outside this contract reports SEM0086 at its declaration.

Evidence: typed constant tests, numeric constant tests, constant analysis.

CONST-002 — Target facts are the only non-literal constant initializers

Status: Confirmed

The following target facts may replace the literal in a constant declaration. The selected target determines their values.

pub const MAX: usize = Target.usizeMax
pub const BITS: u32 = Target.pointerBits

This vocabulary exists because one source literal cannot express every pointer-width bound on both 32-bit and 64-bit targets.

Boundary: Target is recognized only as the root of one of these initializers. An unknown fact, a fact used at the wrong declared type, a target fact in an ordinary expression, or a computed initializer such as Target.pointerBits + 1 is invalid.

Diagnostics: An invalid target-fact constant reports SEM0086. Outside a constant initializer, Target follows ordinary name resolution and is unresolved unless the program declares that name.

Evidence: target-fact catalog, target-dependent constant tests.

Nominal struct values

STRUCT-001 — A struct declaration creates one nominal type

Status: Confirmed

A top-level struct declaration creates a type identified by its canonical module and declaration, including its generic arguments when present. Field shape, import alias, source traversal order, and target layout do not participate in nominal identity.

struct ScreenPosition { x: i32 }
struct WorldPosition { x: i32 }

ScreenPosition and WorldPosition are incompatible even though their fields have the same name and type. A zero-field struct such as struct End {} is an ordinary nominal marker type.

Every field has one explicit type, fields are ordered by declaration, and field names are unique. Structs and fields are private by default; pub exposes them under the module visibility rules.

Boundary: Silk has no shape-based struct compatibility. A public contract cannot expose a private nominal type, and a direct or mutual inline field cycle does not acquire hidden indirection.

Diagnostics: Duplicate fields report SEM0017; a public contract exposing a private type reports SEM0019; inline recursive layouts report SEM0020.

Evidence: struct type specification, declaration index.

STRUCT-002 — Raw struct construction is complete and visibility-based

Status: Confirmed

A raw struct literal is available wherever every required field is visible. It must initialize every field exactly once with a compatible value. Initializers evaluate in source order, while the completed value retains canonical declaration field order.

struct Point {
  pub x: i32
  pub y: i32
}

fn origin() -> Point {
  return Point { y: 0, x: 0 }
}

Because both fields are public, another module may construct Point directly. A type with any private required field instead preserves construction control and exposes visible ordinary constructor functions when external construction is intended.

Boundary: Unknown, duplicate, missing, inaccessible, or mistyped initializers produce no partially initialized value. Construction never fills omitted fields with defaults. A diagnostic for hidden required fields does not expose their names or types. A declarationless opaque nominal type, such as a runtime handle, has no source constructor; an empty semantic field list does not turn it into an ordinary zero-field struct.

Diagnostics: Unknown fields report SEM0022; duplicates SEM0023; missing visible fields SEM0024; incompatible field values SEM0025. Inaccessible construction needs one stable semantic code that does not reveal hidden field details.

Current compiler: Aligned. Construction resolves every named initializer to its canonical field, checks that field's visibility, and uses SEM0021 when a required field is inaccessible or the nominal type has no source struct declaration.

Evidence: struct value tests, struct literal elaboration.

STRUCT-003 — Field projection follows the declared nominal field

Status: Confirmed

value.field resolves the subject's nominal type and the field declared by that type. Nested projection associates from left to right and preserves the access mode of the underlying place.

struct Position { pub start: i32 }
struct Token { pub position: Position }

fn start(token: &Token) -> i32 {
  return token.position.start
}

The final expression has the declared type i32. Reading that Copy leaf does not move token or its Position field.

Boundary: A non-struct has no fields. A field name is resolved only against the subject's actual nominal declaration; Silk does not search other same-shaped structs or extension namespaces. Private fields are inaccessible outside their defining module.

Diagnostics: Projection from a non-struct reports SEM0026; an unknown field reports SEM0027; an inaccessible field reports SEM0028.

Evidence: struct projection specification, projection ownership.

STRUCT-004 — Inline aggregate dependencies must be finite

Status: Confirmed

Every value stored directly inside a struct contributes to its finite inline type dependency. Acyclic nesting is valid regardless of declaration order. A direct or mutual cycle made only of inline fields is invalid because it has no finite complete value.

struct Position { value: i32 }
struct Span {
  start: Position
  end: Position
}

Boundary: struct Node { next: Node } is invalid. The compiler does not guess a pointer or make the field optional. Recursion requires an explicit finite or indirect representation supplied by ordinary library types. A zero-length [Node; 0] still retains Node in its type identity and does not erase an otherwise recursive dependency.

Diagnostics: Every member of one inline recursive component receives the canonical SEM0020 cycle diagnostic without losing its nominal declaration identity.

Evidence: inline dependency specification, inline reach tests.

STRUCT-005 — Struct ownership follows the explicit Copy contract

Status: Confirmed

A struct is affine unless it explicitly requests Copy. The compiler accepts impl Copy only when every field is Copy and the struct has no cleanup behavior. Copying never runs user code.

Aggregate moves, partial-move prohibition, mutation, and cleanup are defined by the ownership reference rather than by field shape alone.

Boundary: A field-only scalar struct does not become Copy automatically. An owner of allocated memory cannot request Copy merely because its physical representation contains a copyable pointer.

Diagnostics: Invalid implicit copying reports OWN0003. An invalid impl Copy reports SEM0083 and identifies the first affine, cleanup-bearing, cyclic, or unavailable reason.

Evidence: owned value classification.

Scalar enum values

ENUM-001 — A scalar enum declares one closed nominal member set

Status: Confirmed

enum Name { ... } declares one nonempty, source-ordered set of uniquely named, fieldless members. The declaration creates a nominal type identified by its canonical module and name. Only a qualified member path such as Status.Ready constructs a value; the bare spelling Ready does not become a module binding.

enum Status {
  Pending,
  Ready,
  Done,
}

fn initial() -> Status {
  return Status.Pending
}

Two enum declarations remain different types even when they use the same representation, member names, and discriminants. Every safe value of an enum names exactly one declared member. Members have no payload, generic arguments, fields, or independent visibility marker; the enum declaration's visibility governs the complete member set.

Boundary: Silk does not infer an enum from an unqualified member name, an integer, or another enum's same-spelled member. An empty enum, a repeated member name, or a payload-bearing member is invalid rather than creating an open or data-carrying sum type. Use structural unions of nominal structs when alternatives need payloads.

Diagnostics: An empty enum reports SEM0146; a repeated member name reports SEM0148 at the later name and relates the first declaration. An unknown qualified member reports SEM0153. Using a member through another canonical enum reports SEM0154. A bare member name receives the ordinary unknown-name diagnostic.

Evidence: scalar enum specification, enum declaration tests, enum name-resolution tests.

ENUM-002 — The representation and discriminant sequence are explicit and checked

Status: Confirmed

An enum without a representation uses exactly u8. enum(R) Name may select only u8, u16, u32, u64, i8, i16, i32, or i64; Silk never infers a wider representation from member values.

The first implicit discriminant is 0. Every later implicit member takes the preceding member's discriminant plus one, including after an explicit optionally negative decimal integer literal.

enum(i16) ExitCode {
  Success,
  Interrupted = 130,
  Failed,
}

The discriminants are 0, 130, and 131. Each explicit value and implicit successor must fit the selected representation, and discriminants must be unique.

Boundary: usize, isize, floating types, aliases, nominal integer wrappers, and inferred representations are unavailable. An explicit discriminant is not a general constant expression; the current syntax accepts an optionally negative decimal integer literal. An unsigned enum cannot use a negative discriminant.

Diagnostics: An unsupported representation reports SEM0147; a duplicate discriminant reports SEM0149 at the later member and relates the first. An explicit out-of-range discriminant reports SEM0150, an overflowing implicit successor SEM0151, and a negative discriminant under an unsigned representation SEM0152.

Evidence: scalar enum representation rules, enum parser tests, discriminant tests.

ENUM-003 — A scalar enum has its representation's layout but keeps nominal identity

Status: Confirmed

A valid enum has exactly the size, alignment, and calling shape of its selected fixed-width integer, with no hidden tag or metadata. This representation choice is not visible as type compatibility: the source value remains the enum's nominal type through storage, calls, equality, and matching.

Every scalar enum is a compiler-sealed Copy value with no cleanup obligation. Reading or passing an enum copies its member value without consuming the original binding.

enum Mode { Read, Write }

fn same(value: Mode) -> bool {
  let copy = value
  return copy == value
}

Boundary: Matching integer layout does not permit implicit integer conversion, cross-enum conversion, or arbitrary bit patterns to inhabit an enum. User code cannot implement or replace the enum's sealed Copy behavior, and an enum cannot admit a Drop implementation.

Diagnostics: An attempted user Copy conformance uses the invalid-conformance diagnostic SEM0083; an invalid Drop implementation uses SEM0084. Mixing an enum with its representation integer reports SEM0155 at the incompatible boundary.

Evidence: sealed enum ownership, layout tests, enum ownership tests.

ENUM-004 — Enum.value exposes the backing integer in one direction

Status: Confirmed

For an enum E represented by integer type R, E.value(value) accepts exactly E and returns that member's declared discriminant as R. The generated operation is total, allocation-free, failure-free, and requirement-free.

enum(i8) Status {
  Unknown = -1,
  Ready,
}

fn code(status: Status) -> i8 {
  return Status.value(status)
}

Status.value(Status.Unknown) returns -1. There is no built-in inverse operation because only declared discriminants are valid enum inhabitants.

Boundary: An enum does not become an integer in arithmetic, ordering, assignment, arguments, or returns. An integer does not become an enum even when its value equals a member discriminant. Enum.value exposes representation; it does not erase the nominal type of the original value or promise that arbitrary representation bits can be reconstructed safely.

Diagnostics: Either implicit enum-to-integer or integer-to-enum use reports SEM0155. A wrong enum argument uses the ordinary argument mismatch or the more specific canonical-enum diagnostic where applicable.

Evidence: enum value operation, analysis facade tests, backend enum tests.

Fixed arrays, references, and slices

ARRAY-001 — A fixed array type includes its element type and length

Status: Confirmed

[T; N] is one inline fixed-array type whose identity contains the canonical element type T and non-negative integer length N. Different lengths are different types. Nested and zero-length arrays retain every element type and length in their identity.

fn pair(values: [i32; 2]) -> [i32; 2] {
  return values
}

[i32; 2] is incompatible with [i32; 3]. [Token; 0] remains distinct from [End; 0] even though neither contains a runtime element.

Boundary: Array<T, N> is a compiler display encoding found in older artifacts, not valid Silk source syntax. Length is not inferred across a declared parameter or result type.

Diagnostics: Malformed fixed-array syntax receives a parser diagnostic. A contextual array literal with the wrong length reports SEM0031.

Evidence: fixed-array source syntax, fixed-array specification, array ownership.

ARRAY-002 — An array literal constructs one homogeneous complete value

Status: Confirmed

An array literal evaluates elements once from left to right. With an expected [T; N], every element is analyzed in immediate T context and the written length must be N. Without an expected array type, the first available element selects the precise element type, later elements must be compatible with it, and the written count becomes the length.

fn bytes() -> [u8; 3] {
  return [1, 2, 3]
}

fn defaults() -> [i32; 3] {
  let values = [1, 2, 3]
  return values
}

The first literal uses contextual u8; the second defaults its first element to i32 and retains that element type. [] requires an expected array type because it has no element from which to select T.

Boundary: An uncontextualized heterogeneous literal does not invent a union or numeric common type. Invalid elements do not create a partially initialized array.

Diagnostics: An empty literal without context reports SEM0029; an incompatible element reports SEM0030 at that element; a contextual length mismatch reports SEM0031 at the literal.

Evidence: fixed-array specification, array elaboration.

INDEX-001 — Array and slice indexing uses checked usize

Status: Confirmed

subject[index] requires a fixed array or slice subject and a usize index. A known out-of-range literal is rejected during analysis. A dynamic index checks index < length at runtime and traps before reading, projecting, or evaluating a replacement value.

fn read(values: [i32; 3], index: usize) -> i32 {
  return values[index]
}

Fixed arrays use their type-level length; slices use their runtime length. Zero-length and zero-sized-element values retain their logical bounds.

Boundary: An i32 variable is not an index even when non-negative. Indexing a string is invalid because text access must name its unit. Ownership determines whether reading or replacing the selected element is valid.

Diagnostics: A non-indexable subject reports SEM0032; a non-usize index SEM0033; a known out-of-bounds index SEM0034. A dynamic overrun is a runtime trap rather than a typed failure.

Evidence: fixed-array indexing, slice indexing, index diagnostics.

VIEW-001 — References and slices include access mode in their type

Status: Confirmed

&T and &mut T are shared and exclusive lexical references to one complete T. &[T] and &mut [T] are shared and exclusive runtime-length contiguous views. Slice type identity includes element type and access mode, but not the source array's length.

fn first(values: &[i32]) -> i32 {
  return values[0]
}

fn use() -> i32 {
  let values = [1, 2]
  return first(&values)
}

The explicit borrow converts neither array ownership nor array type. It creates a view for the borrow's lexical lifetime. Arrays of different lengths may therefore be borrowed for the same &[T] parameter.

Boundary: There is no implicit array-to-slice decay. Shared access cannot strengthen to exclusive access, and borrowed views cannot become owned values. Valid type positions, reborrowing, returned views, storage restrictions, and loan endings follow the ownership reference.

Diagnostics: Invalid borrowed-view positions report SEM0054; invalid borrow positions and operands use SEM0055 and SEM0056; exclusive borrowing of an immutable root uses SEM0057; invalid reborrowing uses SEM0058; implicit array decay uses SEM0059.

Evidence: runtime slice specification, borrow rules, returned views.

Structural unions and inference

UNION-001 — A structural union is a normalized set of ordinary value types

Status: Confirmed

A | B denotes a finite, unordered, duplicate-free set of canonical ordinary value types. Nested unions flatten, member order does not affect identity, duplicate members disappear, never is the empty union, and a one-member union normalizes to that member. Members need not be nominal: scalars, arrays, string, and other detached concrete value types use the same union operation. A callable or Effect member must additionally retain one finite exact, opaque, or composite representation; its bare structural contract has no standalone storage layout.

struct Token { kind: i32 }
struct End {}

fn next(done: bool) -> Token | End {
  if done {
    return End {}
  }
  return Token { kind: 1 }
}

Token | End, End | Token, and Token | (End | Token) are the same type.

fn describe(code: i32) -> i32 | string {
  if code == 0 {
    return "none"
  }
  return code
}

Executable members use their ordinary representation syntax:

fn add(left: i32, right: i32) -> i32 { return left + right }

fn selected() -> typeof(add) | i32 {
  return add
}

typeof(add) contributes the callable's exact finite environment plan. An opaque result binder can do the same for an Effect construction without exposing its private runner identity. By contrast, fn(i32) -> i32 | i32 and Effect<i32> | i32 are invalid: those structural contracts alone do not identify storage.

Boundary: Union formation does not erase ownership, lifetime, Effect requirements, callable access, or another member property. A lexical borrow cannot become an owned union member; a union never makes it detached. Requirement rows remain capability rows rather than value unions.

Generic unions normalize again after monomorphic substitution. If A | B specializes with both parameters equal to i32, the instance carries i32, not two indistinguishable tags. HIR retains the authored mapping and MIR deterministically recomputes the concrete mapping and canonical order.

Diagnostics: An unresolved or otherwise unavailable member reports that member's ordinary type diagnostic. A borrow or bare executable contract reports SEM0039 because it has no detached finite storage plan. A valid non-nominal or represented executable member produces no diagnostic.

Current compiler: Aligned. Normalization, compatibility, target layout, ownership, cleanup, HIR/MIR mappings, evaluation, LLVM, and Wasm consume canonical ordinary member identities. Exact and opaque executable representations remain compiler-private while their public contract spelling is preserved.

Evidence: union normalization, ordinary failure values.

UNION-002 — Precise injection and union widening occur only at immediate expected boundaries

Status: Confirmed

A precise value is compatible with an expected union containing its type. A union value is compatible with a wider expected union only when the target contains every source member.

struct Token { kind: i32 }
struct End {}
struct Fault {}

fn widen(value: Token | End) -> Token | End | Fault {
  return move value
}

The conversion preserves the active member and complete payload. Immediate union contexts include declared returns, parameters, struct fields, contextual array elements, and assignments.

Boundary: Compatibility never subtracts or guesses a member. Token | Fault cannot become Token | End, and a value does not narrow merely because control reaches a use that wants one member. Pattern matching performs explicit narrowing.

Union conversion does not rewrite the source expression's precise type. Runtime tags distinguish members even when their layouts happen to match, but remain internal deterministic compiler data with no source-visible, serialization, or stable ABI identity.

Diagnostics: A target missing any source member reports SEM0040, naming the source, target, and uncovered members. Ownership diagnostics still apply when moving an affine payload.

Evidence: structural union specification, compatibility implementation, match narrowing.

INFER-001 — A binding keeps the precise type of its initializer

Status: Confirmed

An unannotated local binding receives the precise type of its initializer after literal selection. Later uses do not widen, narrow, or otherwise rewrite that type. Each use is checked independently against its own expected context.

struct Token { kind: i32 }
struct End {}

fn accept(value: Token | End) -> i32 {
  return match move value {
    Token { kind } => kind
    End {} => 0
  }
}

fn use() -> i32 {
  let token = Token { kind: 42 }
  return accept(move token)
}

token remains Token; only the call argument injects it into Token | End.

Boundary: Expected types do not flow backward through an already-completed binding:

fn acceptByte(value: u8) {}

fn invalid() {
  let value = 1
  acceptByte(value)
}

value is i32, so the call is invalid. Writing the literal directly as acceptByte(1) permits the parameter to select u8 before the literal becomes a value.

Diagnostics: Binding inference itself produces no diagnostic when the initializer has a type. An unavailable initializer leaves the binding unavailable. A later incompatible use reports at that use, such as SEM0012 for the call above.

Evidence: semantic binding facts, literal contextualization, union conversion specification.