Type system

This is Gale’s formal type-system specification. For syntax and practical examples, start with the language reference.

The rules below describe type inference, subtyping, exhaustiveness, and the runtime representation of checked programs. During prerelease development, the compiler and its regression tests are the source of truth when they disagree with this specification. For library APIs, see the standard library reference.

Conventions:

• “Static error” means the compiler rejects the program. “Warning” means it reports and continues. “Trusted” means the compiler relies on a declaration without checking its implementation.
• Γ ⊢ e ⇑ T reads “e synthesizes T”; Γ ⊢ e ⇓ T reads “e checks against T”; T <: U is subtyping; T ≡ U is equivalence (§2.8).
• Grammar fragments show the surface forms the type rules refer to; they are not a complete syntax definition.
• Example code uses gale fences. Emitted code uses elixir fences.
• Doctest input and expected values in iex> blocks are written in Gale in source files; the compiler lowers both sides to Elixir for ExUnit.

The supported target is Elixir 1.20 on OTP 28 or newer. Runtime checks use the Gale.Check module shipped with mix_gale.

1. Scope

1.1 Guarantees

For code compiled from Gale, the compiler guarantees that:

1. every expression is well typed under the rules of this document;
2. every public function, type, and behaviour has an explicit rank-1 type;
3. every case and receive over closed data is exhaustive (§6.4);
4. every module satisfies every behaviour it implements (§4.9);
5. every receive, self, and mailbox-requiring call occurs in a context with exactly the required mailbox type (§8);
6. pattern narrowing retains every union member whose lowered representation can match; combinations that would make a nominal constructor pattern ambiguous are rejected (§2.5), so narrowing is sound;
7. emitted Elixir preserves the runtime representation (§12.1) and calling convention (§12.3) established by the checked program.

Extern declarations, the standard library, and the BEAM are trusted. Gale does not verify their implementations.

1.2 Closed world

The guarantees cover values created and transported through Gale-checked operations, subject to the correctness of trusted interfaces. A typed BEAM handle models the contract of the resource it names: Pid<M>, typed OTP references, ETS tables, registries, and persistent keys do not revalidate their type arguments on every operation. Foreign code that uses such a resource must obey the same declared contract, just as an extern implementation must obey its Gale signature.

Dynamic data is represented as Term and refined explicitly. A checked projection validates eligible emitted function specs at runtime without changing function bodies (§11.2).

“Compatible with Elixir” means exactly this: every Gale type has one BEAM representation shared with idiomatic Elixir (§12.1), every public function is a plain exported function with an honest @spec, and module values are module atoms. It does not mean that Elixir’s own type checker reasons about Gale programs. A Gale server answers native GenServer.call/3 with the same request values used by Gale callers. Its request ADT is indexed by the reply type according to the stdlib protocol. Foreign callers are not checked, so they must send a valid constructor and accept its declared reply type.

1.3 Exclusions

Ordinary typing provides no termination, deadlock-freedom, eventual-reply, or exactly-once-reply proofs; no row variables or implicit record width; no higher-rank or existential types; no traits, protocols, implicit dictionary passing, or macros; no checking of handwritten Elixir. %{base | f: e} updates a field already present in the exact record or struct shape. Gale supports first-order type constructor parameters and indexed ADTs, but not arbitrary kind polymorphism or existential constructor fields.

1.4 Reserved and contextual words

The reserved words are:

mod alias as implements declares
pub fn type struct opaque extern exception raises
receives
case if cond with else receive after when
true false nil and or not in

do and end are rejected because they are reserved by the target syntax. catch and rescue are rejected the same way. Elixir special forms that are not already Gale keywords (for, import, quote, require, super, try, unquote, unquote_splicing) and definition macros the generated module relies on (def, defp, defmodule, defstruct, defexception, defmacro, defmacrop, defguard, defguardp, defdelegate, defimpl, defprotocol, defoverridable) are rejected as reserved target-language identifiers. Every other Kernel name (length, send, self, spawn, …) remains a legal Gale identifier; the emitter excludes colliding Kernel imports.

Lowercase identifiers may end in a single ?, conventionally for predicates: contains?, is_some?, and ready?. The suffix is part of the name; ready and ready? are distinct. It also works for local bindings and record fields. ? cannot appear inside an identifier or after an uppercase type/constructor name. Module names and module aliases remain snake_case. There are no ! names; foreign exceptions use the declared raises/Result boundary.

callback and optional are contextual in a module that declares a behaviour. down and exit are contextual only as VM-event arms inside receive. They may otherwise be ordinary identifiers.

Reserved words may still be used as record or struct field names when their position is unambiguous: before : in a field declaration/construction or after . in field access. This permits fields such as type in OTP data without weakening declaration-level keyword recognition.

cond requires a final literal true guard. else belongs only to if and with. spec, validator, Decoder, Encoder, call, cast, info, deferred, projected, handle_continue, terminate, and format_status are not language words. A library may use any of those names.

2. Types

2.1 Grammar

T ::= Never | Term
    | Integer | Float | String | Binary | Atom | :atom | AnyPid
    | {T1, …, Tn}                          n ≥ 0; {} is unit
    | %{f1: T1, …, fn: Tn}                 n ≥ 1; fields distinct
    | List<T> | Map<K, V>
    | N<T1, …, Tn>                         nominal type or alias, n ≥ 0
    | T1 | … | Tn                          n ≥ 2, normalized (§2.5)
    | fn(T1, …, Tn) -> T
    | fn(T1, …, Tn) receives M -> T
    | mod m                                singleton module type
    | mod B<T1, …, Tn>                     behaviour capability
    | a                                    type variable

Boolean is the built-in alias :true | :false; the literals true and false denote the atoms :true and :false. Timeout is the built-in alias Integer | :infinity. Option<A>, Result<A, E>, and Order are prelude ADTs (§4.4), not core forms. ChildSpec<A> is a prelude type for native child specifications: nominal, with no constructors, and an unknown representation the compiler projects to map() (§12.1).

2.2 Well-formedness

A type is well formed when:

• every nominal name resolves to a declaration and is applied to exactly its declared number of arguments;
• every type variable is a parameter of the enclosing declaration (§4.1);
• no transparent alias is recursive, directly or through other aliases; recursive ADTs and structs are allowed;
• record fields are distinct atoms;
• union members are well formed and pattern-compatible (§2.5); the union is then normalized.

Never is uninhabited. Term is inhabited by every BEAM term.

2.3 Primitive types

Type	Values
Integer	BEAM integers
Float	BEAM floats
String	UTF-8 encoded byte-aligned binaries
Binary	any byte-aligned BEAM binary
Atom	any atom
:atom	the single atom written; :name or quoted :"any text"
AnyPid	any BEAM pid, without a sendable mailbox type

Integer and float literals have types Integer and Float. Underscores may appear between digits (1_000, 1_000.5) and are stripped; there are no hex, octal, binary, or exponent spellings. String literals and expression heredocs have type String. Atom literals have their singleton type. Gale never creates an atom from a runtime string. String <: Binary; they are the same runtime value. type String = … is rejected as a builtin name, as type Binary = … is. There is no guard that refines to String.

The string escape set is exactly \", \\, \n, \t, \r, and \u{H…} (1–6 hex digits, a valid scalar, not a surrogate). Any other \ sequence is a static error. Expression heredocs remove the closing delimiter’s indentation from literal text lines and decode those escapes. Interpolated expressions retain their original source: the outer heredoc does not strip indentation inside a nested string or heredoc. Nested heredocs use their own closing indentation. @doc heredocs stay raw. Interpolated slots must be String, Integer, Float, Boolean, or Atom; Binary is rejected (convert with string.from_binary).

2.4 Structural types

Tuples. {T1, …, Tn} has arity n. {} is unit; its value is the empty BEAM tuple {}.

Records. %{f1: T1, …} describes BEAM maps with exactly the declared atom keys and field types. Records need no declaration; an alias may name a shape. Record subtyping preserves the complete field set and may widen field types. Structs remain nominal and do not implicitly become records.

For example, %{count: Integer} does not accept %{count: 1, extra: 7}. Write %{count: value.count} to construct the smaller map explicitly. This changes the runtime value by dropping omitted fields. Use Map<K, V> for arbitrary keys and Term for explicitly dynamic observations. Record patterns may still mention only the fields they bind; patterns do not change values.

Collections. Map literals use %{k => v} or atom-key %{k: v}; %{} is the empty map. List<T> is a proper list and Map<K, V> a dictionary keyed by K. List is covariant; Map is invariant in K and covariant in V. Elixir sets are exposed by the standard library as the invariant extern type gale_std.map_set.MapSet<T> rather than a core collection type. There is no set literal.

2.5 Unions

A union is a set of member types with no runtime discriminant. Normalization is applied whenever a union is formed:

1. flatten nested unions;
2. drop Never;
3. if any member is Term, the result is Term;
4. drop a member Ti when some other member Tj satisfies Ti <: Tj;
5. drop duplicates under ≡;
6. a single remaining member is that member; no remaining member is Never.

Normalization never solves inference variables: during steps 4 and 5 an unsolved variable is equivalent only to itself and is a subtype only of Term and of itself.

The compiler does not distribute unions through other constructors: {Integer, :left} | {Binary, :right} stays two untagged tuple members. Atom-tagged tuples that share a tag and arity must be written as one member with a union payload: {:same, Integer | Boolean}, not {:same, Integer} | {:same, Boolean}.

Pattern compatibility. Union members need not denote disjoint runtime sets except where this section requires unique outer discriminants. Structural overlap is handled conservatively: a pattern retains every member whose lowered representation it can match. A variable binds that narrowed union, and record patterns join common-field bindings across its members (§6.3). Tuple and list patterns join the component types of all retained members; matching a tuple tag first preserves the corresponding payload alternatives. Nominal constructor syntax is different because it asserts which declaration supplied a value even though that identity is erased. After alias expansion, forming a union is therefore a static error when it contains any of these pairs:

• two remaining members that share an outer discriminant: Integer, Float, the shared String/Binary binary kind, an atom literal, or an atom-tagged tuple of a given arity ({:tag, …} and ADT constructors that lower to that same tag and field count). Subtype members dropped by normalization do not count, so Boolean | :true and String | Binary stay the wider type;
• two distinct ADTs with constructors that lower to the same tag and the same field count (§4.4);
• two distinct extern exception types that name the same Elixir exception module;
• an ADT with a nullary constructor C and the atom literal :c where :c is C’s lowered atom, or the type Atom;
• an ADT with an n-field constructor and a tuple type of arity n + 1 whose first component admits the constructor’s tag atom (:tag or Atom).

An opaque type is checked through its representation, which the compiler loads from the declaring package even where the type is nominal to the program. Meters | :unknown is well formed when Meters is represented by Integer; Meters | Integer is a static error because the lowered values are the same. The union is not silently collapsed to Integer. Nominality still governs typing; only pattern compatibility looks through the representation.

AnyPid and the stdlib extern types Pid, Monitor, Timer, and Ref have compiler-known representations. Other extern types have an unknown representation. They may occur in unions, but a pattern cannot assume they are disjoint from a visible runtime shape: only a variable or wildcard may cover such a member unless its representation is compiler-known (§6.3). Body-less marker opaques are uninhabited: they are dropped like Never during union normalization and contribute no matching path.

Records, structs, untagged tuples, lists, and remaining primitives need no pairwise-disjointness rule beyond unique outer discriminants. Their lowered patterns carry structural information, and §6 retains every overlapping member. Record members are narrowed only through sub-patterns on common fields (§6.3).

2.6 Nominal types

ADTs (§4.4), structs (§4.5), opaques (§4.7), extern types (§4.8), behaviours (§4.9), and module singletons are nominal: two declarations are different types even when their bodies coincide. Nominality is static only. ADT constructors erase to atoms and tagged tuples, so two ADTs whose constructors lower to the same tags are indistinguishable at runtime; §6.3 states the consequence for patterns. Aliases (type N<…> = T) are transparent.

2.7 Function, mailbox, and module types

fn(T1, …, Tn) -> T is a closure of arity n. fn(…) receives M -> T is the same closure carrying the mailbox capability M (§8.1); a function type without receives has no mailbox. Mailbox types are compared exactly.

A function without a mailbox may run in any process: it never receives and never asks for self. It is therefore a subtype of the same function type with any mailbox (§3.1). The converse never holds.

mod m is the type of the module literal m and exposes all of m’s public functions. mod B<T…> exposes exactly the functions of behaviour B instantiated at T…. When m implements B<T…>, its singleton module type coerces to that behaviour capability under §3.1. Both forms are represented by the module atom at runtime; passing a module creates no object or callback dictionary.

A call written against a known module name is static. A call through a mod B<T…> parameter dispatches to that module atom at runtime and is checked against the instantiated behaviour before Elixir is emitted. An atom cannot be used as a module capability merely because it names a loaded module.

2.8 Equivalence

T ≡ U holds when, after alias expansion and union normalization, the two types are structurally identical: same primitive, same tuple arity and component types, same record field set and field types, same nominal symbol and equivalent arguments, same union member set, same function arity, parameter, mailbox, and result types, same module symbol or behaviour instance. Type variables are equivalent only to themselves.

3. Subtyping

3.1 Rules

Never <: T                      T <: Term
:a <: Atom
String <: Binary
T <: T1 | … | Tn                     when T <: Ti for some i, T not a union
T1 | … | Tn <: U                     when every Ti <: U
(T1, …, Tn) <: (U1, …, Un)          when every Ti <: Ui
%{f1: T1, …, fn: Tn} <: %{f1: U1, …, fn: Un}
                                     when every Ti <: Ui (same field set)
List<T> <: List<U>                   when T <: U
Map<K, V> <: Map<K', V'>             when K ≡ K' and V <: V'
gale_std.map_set.MapSet<T> <: gale_std.map_set.MapSet<U>
                                     when T ≡ U
N<T…> <: N<U…>                       per variance of N (§3.2)
fn(T…) -> T <: fn(U…) -> U           when every Ui <: Ti and T <: U, same arity,
                                     both without mailbox
fn(T…) -> T <: fn(U…) receives M -> U
                                     same conditions; no mailbox is below
                                     every mailbox
fn(T…) receives M -> T
  <: fn(U…) receives M' -> U         additionally when M ≡ M'
Pid<M> <: AnyPid
mod m <: mod B<T…>                   when module m implements B<T…> (§4.9)

Subtyping is reflexive and transitive. A subtype check that meets an unsolved inference variable follows the subsumption procedure of §5.4; it never searches for a least or greatest solution.

3.2 Variance

Gale has no source syntax for variance annotations. For transparent ADTs, structs, and aliases, the compiler infers each parameter’s most permissive sound variance from its uses. Constructor fields, struct fields, tuple components, function results, and covariant arguments are positive; function parameters and contravariant arguments reverse polarity. A use in both polarities or in an invariant position makes the parameter invariant. An unused parameter is invariant. Recursive declarations are solved together to a fixed point.

Opaque types, extern types, behaviour arguments, mailbox parameters, and other capability types are invariant because their complete uses are not visible in the declaration. The built-in collection variances are fixed by §2.4. In particular, typed process and server references are invariant. Variance affects only identity-preserving subtyping and never emits a runtime conversion.

3.3 Identity coercion invariant

Every subtyping relation above relates types whose values share a BEAM representation. Subsumption is therefore always an identity coercion: the compiler never inserts conversion code, and the runtime representation of a value is fixed by its synthesized type.

This is an internal compiler boundary, not manual casting syntax. Checked Core records the selected typed view while retaining the full runtime value. It inserts no BEAM conversion.

3.4 Non-rules

There is no subtyping between distinct nominal types other than the listed AnyPid and mod rules; structs do not implicitly become records or maps; records become Map<K, V> only under the field-by-field rule in §4.6; no numeric widening; no Boolean to Integer; no relation between function types of different arity, or between two different mailboxes (only the absence of a mailbox is below a mailbox); no intersection types.

4. Declarations

4.1 Modules, visibility, and type parameters

A source file declares one module: mod path.name. The file uses either the .🌀 or .gale extension; both compile, and both present for one module path is an error. The file is ordered: mod, optional @moduledoc, then alias clauses, then at most one declares B<T…> or extern "Native.Module" declares B<T…> clause, then any number of implements B<T…> as name clauses (§4.9), then an optional struct { } block if the module is a struct. That struct block is still part of the header. Types, functions, callbacks, and other declarations follow in any order:

gale fmt sorts the alias block by module path. The compiler still enforces the header boundary and singleton clauses such as declares and struct. The formatter also normalizes spacing around commas, colons, arrows, and operators such as +, ==, |>, and =. It preserves strings, comments, and line breaks.

mod account
struct { id: Integer, name: String = "unknown" }

That form emits Account as the struct module. A declaration-level named struct is not a language form: each struct owns its source file and is the module declared by that file (§4.5).

Names are pub or private to the module. Modules compiled from test/ must end in _test; their public functions are emitted as zero-argument ExUnit tests, so public test functions take no arguments. Assertions are ordinary gale_std.test.assert library calls rather than a language form. Only declarations (fn, type, opaque type, extern, declares, behaviour callbacks) introduce type parameters, written <A, B, C> after the name. A declaration’s type is the closed rank-1 scheme ∀ params. T; ∀ never appears inside a type. Local bindings and lambda parameters are monomorphic.

A value parameter that participates in strict equality is written A: Eq. Eq is a built-in, non-overloadable constraint, not a user-defined interface: it permits Gale’s existing strict runtime equality and introduces no custom comparison function. Calls, named type applications, constructors, and first-class function references must preserve the constraint. Term and types that store Term do not satisfy it. A phantom or indexed parameter absent from the runtime representation does not need Eq merely because the enclosing value is compared. Higher-kinded parameters continue to use F: Type -> Type; they cannot also declare Eq.

@moduledoc, @doc, and @typedoc accept a string or heredoc. @moduledoc occurs immediately after the module name, @typedoc immediately before a type declaration, and @doc immediately before any other declaration. Public documentation is emitted to Elixir; private declaration documentation is not.

4.2 Functions

pub fn name<A, B>(p1: T1, …, pn: Tn) [receives M] -> R { body }

Every parameter and the result are annotated. body is checked against R under mailbox M (or none). Two functions in one module may share a name only if their arities differ, and a name/arity pair is unique. Constructors live in their own namespace (§4.4). Types and functions also have separate namespaces: pub type Pair<A, B> and pub fn pair/2 may coexist. There are no default parameters and no overloading by type. The type of name at a use site is its scheme instantiated with fresh inference variables (§5.3). A public function may also be referenced through its module or an alias, for example library.transform. Its scheme is instantiated in the same way as a local reference. A local value shadows a same-named module alias. Overloaded references remain ambiguous; use a lambda containing an arity-specific call.

4.3 Aliases

pub type N<params> = T names T transparently. Recursive aliases are a static error.

4.4 Algebraic data types

pub type N<params> = C1 | C2(T, U) | C3(f: T, g: U = default)

A constructor has zero or more positional fields. A field may carry a label; labels permit C3(f: x, g: y) keyword form in direct calls and patterns and do not affect the type. Fields with defaults must follow fields without.

Defaults are typechecked in the declaring module, cannot mention other fields, and elaborate to a generated hidden public function per field in the declaring module (public so that other modules can call it; hidden from documentation) that is called wherever the argument is omitted; omission is allowed only in a direct constructor call, never through the constructor’s function value.

Constructors are namespaced by their ADT: the full name is M.N.C. An unqualified C resolves when imports leave exactly one candidate; the expected type never selects a constructor. Constructors are first-class:

None : N<A>                        nullary constructor is a value
Some : fn(A) -> N<A>               constructor with fields is a function of full arity

Representation: a nullary constructor is the atom of its name in snake_case (OneForOne → :one_for_one); a constructor with fields is the tuple {tag, field1, …}. Within one ADT every constructor must lower to a distinct tag (FooBar and Foobar collide; static error). Two ADTs may lower to the same tags; nominality is not recoverable at runtime, so such ADTs may never share a union (§2.5). The prelude declares pub type Option<A> = None | Some(A), pub type Result<A, E> = Ok(A) | Error(E), and pub type Order = Less | Equal | Greater. The parameters of Option and Result are inferred covariant.

4.4.1 Indexed constructors

A constructor may fix the result instance of its ADT:

pub type Request<Reply> =
  | Count : Request<Integer>
  | Add(amount: Integer) : Request<Integer>
  | Reset : Request<:ok>

Count has type Request<Integer> and Reset has type Request<:ok>. Matching request: Request<R> refines R in each branch. Thus a value of type ReplyTo<R> accepts an Integer in the Count branch and :ok in the Reset branch. The refinement is branch-local and cannot escape the match. When the scrutinee has a concrete index, incompatible constructors are unreachable and must not be included in an exhaustive match.

The result annotation uses :, not ->, and must name an instance of the ADT being declared. Each index is a kind-0 declaration parameter or a first-order type from primitives, atoms, tuples, and injective named constructors. Higher-kinded parameters and applications such as F<A> are not valid indices. Every type parameter used by a constructor field must also occur in its result; existential constructor fields are not supported. Indexed ADTs are invariant. Constructor defaults follow the ordinary rules above.

Type parameters may also be used as first-order constructors:

pub type Box<F: Type -> Type, A> = Box(value: F<A>)

pub fn unwrap<F: Type -> Type, A>(box: Box<F, A>) -> F<A> {
  case box { Box(value) -> value }
}

F must be declared as a type constructor. Its arity must remain consistent throughout the declaration. Built-in constructors such as List and named constructors such as Request may be supplied for F. Constructor parameters are not runtime values, and Gale does not provide arbitrary kind polymorphism, higher-rank types, or existential types.

Erlang typespecs cannot represent higher-kinded applications, so constructor-valued type arguments are emitted conservatively as term() while Gale retains the precise type.

Indexed constructors use the same atom and tuple BEAM representation as ordinary ADTs. Their indices are erased.

4.5 Structs

mod path.n
struct<params> { f1: T1, f2: T2 = default, … }

Construction uses %N{f1: e1, …}; parenthesized struct construction is rejected. Fields without defaults are required; fields with defaults may be omitted under the rules of §4.4. Field access and update use record syntax (§5.6). Structs are nominal. Construct a record explicitly when projecting their fields; neither structs nor records implicitly convert into the other. Updating a struct preserves its nominal type.

Representation: an Elixir struct whose module is the Gale module’s Elixir name (accounts.user → Accounts.User); the compiler emits defstruct, @enforce_keys for fields without defaults, and @type t().

4.6 Records

Records have exact structural shapes (§2.4) and need no declaration. Field access requires the field in the static shape. %{base | f: e} updates an existing field and preserves the complete record or struct type. Adding a field through update is a static error; construct the new record shape explicitly.

pub fn rename(r: %{id: Integer, name: String}, name: String) -> %{id: Integer, name: String} {
  %{r | name: name}
}
pub fn only_id(r: %{id: Integer, name: String}) -> %{id: Integer} {
  %{id: r.id}
}

Gale has no implicit width subtyping or row variables. Functions state their complete record shapes. Widening field types within that shape preserves the runtime value; explicit projection constructs a different record. An exact record is a subtype of Map<K, V> when every atom field key is a subtype of K and every field value is a subtype of V.

4.7 Opaque types

pub opaque type N<params> = T is transparent inside the declaring module and nominal outside it: no subtyping other than <: Term, and construction or inspection only through the module’s functions. A pub opaque type N<params> with no body is a marker type with no values; it may appear in signatures and as a type argument. Runtime decoders for an opaque type, when useful, are ordinary functions supplied by its declaring module.

4.8 Externs

pub extern "Enum.map" name<params>(p: T, …) [receives M] -> R [raises E]
pub extern "Process.sleep" name(timeout: Timeout) -> :ok
pub extern type N<params>
pub extern struct "URI" Uri { scheme: Nilable<String>, port: Nilable<Integer> }
pub extern exception "Exception" E { field: T, … }
pub extern mod "Enum" name [implements B<T…> …]

An extern function is a trusted foreign contract. Every public or private extern emits a spec-bearing def or defp; its body calls the declared MFA. A remote is emitted with its full module name, so extern "Process.sleep" calls Process.sleep. Gale aliases are resolved to full module names during checking and do not emit Elixir aliases. Erlang remotes (:erlang.send) are unchanged. A leading Elixir. in an extern spelling is accepted and removed in generated code. All Gale callers call that wrapper. Checked typespec output can therefore validate the foreign boundary (§11.2).

An extern with no raises clause preserves the foreign function’s native return and failure behavior. A declaration may name the exception classes that are an expected part of the API:

extern ":ets.lookup" raw_lookup<K, V>(
  table: Term,
  key: K
) -> List<{K, V}>
  raises EtsError

Its Gale result is Result<List<{K, V}>, EtsError>. The wrapper maps a normal return to Ok, a declared exception to Error, and reraises every other exception with its original stack trace. It does not catch exits or throws.

An extern exception is nominal in Gale and projects to the named Elixir exception struct. It may appear in raises directly or in a union of extern exceptions. Two such types naming the same Elixir exception module cannot be members of one union because their patterns have the same runtime representation. Exception fields cannot have defaults, and Gale cannot construct or update exception values.

An extern type is nominal and projects to term() unless the compiler knows its representation. An extern mod is a statically known native module atom. Without implements it exposes no callable behaviour surface; each implements B<T…> licenses mod name <: mod B<T…>. Atoms never acquire module capabilities dynamically.

Extern structs

extern struct "URI" Uri { ... } declares a Gale type whose values are native %URI{} structs. Gale emits @type uri() :: %URI{...} and uses uri() in function specs. It emits no defstruct and does not copy values. Typed field access, construction, patterns, and updates use the native struct. At Gale function boundaries in test and development builds, runtime checks verify the native module and recursively check declared fields; additional native fields are allowed. Construction requires all declared fields. The native defstruct supplies defaults for undeclared fields. Nilable<T> describes fields that may be nil. Extern structs have no type parameters. See the Externs chapter for examples and constructor caveats.

The compiler derives Elixir specs from Gale signatures. spec is not Gale syntax, and runtime reflection is never module or behaviour evidence.

Term results of externs make no shape claim; the caller decodes them before using a more precise type. A mod type in an extern signature is trusted like every other extern type assertion. There is no unsafe declaration or expression in Gale; trusted foreign code is identified by extern.

4.9 Behaviours and implementations

One source module may declare one behaviour. The declaration is part of the module header and its callbacks are module-level declarations:

mod storage
declares Store<K, V>

callback fetch(key: K) -> Option<V>

optional callback close() -> :ok

pub fn helper<A>(value: A) -> A { value }

declares B<params> creates the nominal behaviour module.B<params> and brings its parameters into scope for callback declarations. A callback is always a function, so there is no redundant callback fn form. The declaring module may also contain ordinary types and functions.

An extern behaviour maps the same Gale contract to an existing BEAM behaviour:

mod gale_std.gen_server
extern "GenServer" declares Server<A, S, Call: Type -> Type, Cast, Info, C>

callback init(args: A) -> Init<S, C>
optional callback handle_cast(message: Cast, state: S) -> Next<S, C>

A non-extern declaring module emits a real BEAM behaviour module, including its callback declarations and optional-callback metadata. An extern declaration instead names the native behaviour module and does not emit a second behaviour contract.

Callback declarations contain signatures only; required and optional callbacks cannot carry bodies. An optional callback may be omitted by any implementation. When an implementation supplies one, it is checked against the instantiated callback signature. Gale emits no fallback function for an omitted callback. Native behaviours keep their native omission semantics: the BEAM library may ignore an absent callback, log, or fail if code attempts to invoke it.

An implementation keeps ordinary function syntax:

mod memory_store
alias storage

implements storage.Store<Binary, Integer> as store

pub fn fetch(key: Binary) -> Option<Integer> {
  None
}

implements B<T…> as name is required on a module header. It binds a private type alias name for the instantiated capability mod B<T…>. It does not rename the module; the module value remains m. The name is the local type for this instantiation, typically the phantom on ServerRef / ServerTarget / StartResult / ChildSpec, so those annotations do not repeat mod B<T…>. It has no runtime effect and no additional subtyping rule. The name must not collide with a type declaration or module alias. Use ordinary pub type Service = name to re-export it. Named implementation bindings are module headers; extern mod … implements B<T…> cannot take as.

A module m with implements B<T…> as name is checked as follows, with B’s parameters substituted by T…:

1. m implements B at most once;
2. no name/arity pair is a callback of two behaviours implemented by m;
3. every non-optional callback has a pub function of the same name and arity in m; callback type parameters, if any, match in number and are compared under renaming;
4. the implementing function’s type is a subtype of the instantiated callback type (§3.1): broader parameters, narrower result, identical mailbox;
5. every optional callback may be omitted; when present, it is checked by rules 3–4.

Callback-local type parameters shadow same-named behaviour parameters and remain generic in the implementing module’s exported interface. Private implementation state types can instantiate behaviour parameters.

Any number of distinct modules may implement the same instantiated behaviour. There is no global canonical implementation for a type; the caller selects the module value to pass.

The literal m synthesizes mod m; implements B<T…> as name licenses the coercion mod m <: mod B<T…>. The abstract behaviour capability exposes required callbacks only, because optional callbacks are not guaranteed to exist. An optional callback is callable through a concrete module only when that module explicitly defines it. A call through a mod value is a dynamic module call (§12.3). Module values cannot be forged from atoms.

For every implemented behaviour, the Elixir backend emits @behaviour and @impl using the behaviour’s Elixir module name. A Gale-declared behaviour uses the generated module, for example @behaviour Storage. An extern behaviour uses the native spelling from extern "…" declares, so extern "GenServer" declares Server<…> emits @behaviour GenServer. It never emits @impl true and never invokes the behaviour as an Elixir macro. A Gale alias resolves in Gale: after alias gale_std.gen_server, GenServer.call emits a call to the full Gale wrapper module. Behaviour parameters remain authoritative in Gale even when the native callback spec is broader.

4.10 Name resolution

Declarations are collected into lexical and package environments before their bodies are checked. alias a.b.c makes the module available as c, while alias a.b.c as d makes it available as d; aliases can name a namespace prefix, so alias a.b.c as c permits c.d.f. Header aliases are in scope for declares/implements and for the rest of the module, so alias gale_std.gen_server then implements gen_server.Server<…> as counter is the ordinary form. Functions, types, constructors, and structs from another module must always be qualified through that module name or alias. Local declarations remain unqualified. Resolution is environment based and never uses expression types to choose between declarations. Two modules with the same final segment can be used together by giving them distinct as names. The same is required when the last segment collides with the package prefix: alias gale_std.supervisor as otp_supervisor in package supervisor.*, and alias gale_std.ets as std_ets in package ets.

A local function or extern shadows an automatically available Elixir Kernel function or macro only at the same name and arity. The Elixir backend emits the corresponding import Kernel, except: [...] entries automatically; no source annotation is required. Calls and operations introduced by the compiler itself remain explicitly qualified, so this shadowing cannot change their meaning.

4.11 Explicit dispatch

Gale has no implicit type-directed dispatch. A generic operation takes a function or an explicit mod B<T…> capability. Closed alternatives use ADTs and pattern matching.

pub fn sort<A>(values: List<A>, compare: fn(A, A) -> Order) -> List<A>

pub fn encode<A>(encoder: mod encoding.Encoder<A>, value: A) -> Json {
  encoder.encode(value)
}

encode(user_json, user)
encode(pretty_user_json, user)

The call site selects the implementation. The compiler performs no implementation search and inserts no dictionary or runtime-type dispatch.

5. Expressions

5.1 Bidirectional judgments

Every fully annotated expression form has a synthesis rule; some also have a check rule. A lambda with an omitted parameter annotation is the only form that requires an expected type (§5.8). When e is checked against T and has no check rule, it is synthesized as U and U <: T is required (subsumption). Check mode is used at exactly these sites:

• arguments of calls and constructor applications, against parameter types;
• function bodies and lambda bodies, against the result type;
• field values in record/struct construction and update;
• elements of list and tuple literals when an expected type exists;
• arms of case, cond, with, and receive when an expected type exists;
• behaviour implementation checking (§4.9).

Declared signatures, annotations on bindings, and expected types propagated from these sites are the only sources of expected types.

Evaluation is strict. Function arguments, tuple and list elements, map entries, record fields, and explicitly supplied constructor or struct fields evaluate left to right in source order. Omitted-field defaults then evaluate in declaration order. Blocks run in statement order; and and or short-circuit; only the selected arm of a branch evaluates.

5.2 Join

Where several sub-expressions determine one type without an expected type (arms, collection elements, after bodies), their types are joined pairwise, left to right. join(T, U) is defined by the first applicable rule:

1. T ≡ U: the result is T.
2. Either side is an unsolved inference variable: unify (§5.4); the result is the solved type.
3. Both sides have the same head constructor: List, Set, Map, tuples of one arity, records with the same field set, the same struct, or the same nominal type. Join covariant arguments and fields componentwise; unify contravariant and invariant arguments because Gale has no intersection operation. If every component succeeds the result is that constructor applied to the results; otherwise restore the inference-variable state from before this rule and fall through.
4. Otherwise the result is the normalized union T | U (§2.5). If that union is ill-formed under the pattern-compatibility rules, the join is a static error.

Join never distributes an existing union through a constructor, so written types stay as written; only synthesized types are merged. Consequently:

[Some(1), None]                     ⇑ List<Option<Integer>>
[1, :infinity]                      ⇑ List<Integer | :infinity>
cond { c -> [1]  true -> [:x] }     ⇑ List<Integer | :x>
cond { c -> 1  true -> :x }         ⇑ Integer | :x
cond { c -> %{a: 1}  true -> %{b: 2} } ⇑ %{a: Integer} | %{b: Integer}

5.3 Instantiation

A reference to a declared generic function or constructor replaces its parameters with fresh inference variables. There is no explicit instantiation syntax; a binding annotation or a declared signature pins a variable when inference alone does not.

5.4 Inference variables

Inference variables are solved by first-order unification (equality), never by accumulated subtype constraints. There is no binding generalization; every binding is monomorphic.

Unification unify(T, U) is structural. Two types unify when they are the same primitive, tuples of one arity with pairwise unifying components, records with the same field set and pairwise unifying fields, the same nominal or collection constructor with pairwise unifying arguments (variance does not matter for unification), function types of one arity with pairwise unifying parameters, results, and mailboxes (absent unifies only with absent), or the same module or behaviour instance. A rigid type parameter unifies only with itself. An unsolved variable unifies with any type that does not contain it (occurs-check failure is a static error) and is solved to that type; two unsolved variables become aliases. A union unifies only with an equivalent union or with a bare unsolved variable; unions containing unsolved variables are never taken apart.

Subsumption sub(T, U) decides T <: U and may solve variables. The first applicable rule is used, and no rule is retried on failure:

1. T ≡ U, T is Never, or U is Term: succeed without solving.
2. T or U is a bare unsolved variable: unify(T, U). The variable takes the other side exactly; exact-shape subtyping and union membership are then checked at later uses, not folded into the solution.
3. T and U have the same head constructor (§5.2 rule 3, plus struct with the same nominal constructor): recurse componentwise per variance, using sub in covariant positions, sub with sides swapped in contravariant positions, and unify in invariant positions and mailboxes.
4. T is a union: sub(Ti, U) for every member.
5. U is a union and T is not: if some member Ui satisfies T <: Ui without touching any unsolved variable, succeed; otherwise, if exactly one member has the same head constructor as T or is a bare variable, sub(T, Ui); otherwise fail.
6. Otherwise apply the closed rules of §3.1 directly.

These six rules are the complete procedure. A program that fails rule 5 needs a binding annotation or a declared signature; the checker does not search for a cleverer instantiation. Rule 1 prevents Never and Term from over-tightening a variable; rule 2 prevents the checker from ever guessing a least type. When a later failure involves a variable that rule 2 previously committed, the diagnostic names the chosen type and recommends a binding annotation at the binding or call site when a wider union or record was intended.

Defaulting. A variable still unsolved when checking of the enclosing top-level function finishes is solved to Never. Nothing constrained it, so every instantiation would have typechecked; Never is the one that claims the least ([] is a List<Never>, spawn(fn() -> work()) is a Pid<Never>). Defaulting occurs before exhaustiveness and mailbox checks.

5.5 Literals, variables, tuples, collections

integer ⇑ Integer      float ⇑ Float      "…" ⇑ String      :a ⇑ :a
true ⇑ :true           false ⇑ :false
nil ⇑ :nil             {} ⇑ {}
x ⇑ Γ(x)
{e1, …, en} ⇑ {T1, …, Tn}                  each ei ⇑ Ti
[e1, …, en] ⇑ List<join(T1, …, Tn)>       [] ⇑ List<A> fresh A
[h | t] ⇑ List<T>                          h ⇑ T, t ⇓ List<T>

Check rules push the expected component or element type into each sub-expression. %{k => v, …} constructs Map<K,V>; %{name: v} uses an atom singleton key :name. %{} is an empty map with fresh key/value types. Synthesis joins the key types and value types across entries. Checking against Map<K,V> pushes those types into every key and value, including lambdas. Entries evaluate from left to right, key before value; the last duplicate key wins. Unlike records, map literals do not expose statically named fields. Set values are built through stdlib functions. An interpolated string has type String; each interpolation must be String, Integer, Float, Boolean, or Atom. Binary interpolation is a static error naming from_binary. An expression heredoc is typed as String and interpolates the same way; @doc heredocs are raw.

5.6 Records and structs

%{f1: e1, …} ⇑ %{f1: T1, …}               each ei ⇑ Ti
e.f ⇑ T                                    e ⇑ R, R a record or struct with f: T
e.f ⇑ join(T1, …, Tn)                      e ⇑ R1 | … | Rn, every Ri a record or
                                           struct with f: Ti
%{e | f: e'} ⇑ R                           e ⇑ R, R a record or struct with f: T,
                                           e' ⇓ T
%N{f: e, …} ⇑ N<A…>                       fields checked against declared types

Field access on a union requires the field in every member; the result is the join of the field types. Update requires a single record or struct type. e.f on any other type is a static error.

5.7 Constructors

A nullary constructor is a value of its ADT type instantiated fresh. A constructor with fields applied directly, C(e1, …), checks arguments against field types (defaults may be omitted, §4.4) and synthesizes the ADT type. A constructor with fields used without application synthesizes its function type at full arity. Direct application emits the tagged value without allocating a closure.

5.8 Lambdas

fn(x: T, y) [receives M] -> e

Parameters without annotation are allowed only in check mode against an expected function type of the same arity, which supplies them. The body is checked or synthesized under mailbox M (or none) and the lambda has type fn(T…) [receives M] -> R. A lambda has a mailbox only when it writes receives; an expected type never supplies one. A lambda without receives checked against fn(…) receives M -> R is accepted through the no-mailbox subtyping rule of §3.1 and cannot receive. Lambdas capture variables by value.

5.9 Calls

Form	Resolution	Backend classification
f(args)	function in scope	LocalCall / StaticModuleCall
path.f(args)	path a module	StaticModuleCall
e.f(args) with e ⇑ mod …	behaviour or singleton function f	DynamicModuleCall
e.f(args) otherwise	static error; use e |> f(args)	n/a
e(args)	e ⇑ fn(T…) [receives M] -> R	ClosureCall
a |> f(args)	f(a, args)	as rewritten
generated extern wrapper body	declared MFA	ExternCall

Arity must match exactly. Arguments are checked against parameter types after instantiation (§5.3); the call synthesizes the instantiated result.

When a call has an expected result type, the checker first attempts subsumption from its instantiated result to that expected type. A successful attempt guides argument checking, including lambda result types. Named refinements are preserved: an expected List<Nonnegative> can make a mapping callback return Nonnegative. If this preliminary attempt fails because argument information is still needed, its substitutions are discarded and ordinary argument checking proceeds. The completed call must still satisfy the expected result type. This scheduling does not change the subsumption rules or introduce a search for alternative solutions.

Calling a function whose type carries receives M requires the current context to have a mailbox M' with unify(M, M') (§8.1); a context without a mailbox fails. Pipelines insert the first argument; dot calls dispatch only through modules and mod capabilities. They define no methods on ordinary values.

5.10 Operators

Operator	Typing
<>	String × String → String; otherwise Binary × Binary → Binary (String is accepted on either side by subtyping)
++	List<A> × List<A> → List<A>; compatible element types
+ - *	Integer × Integer → Integer or Float × Float → Float; never mixed
/	Float × Float → Float
== !=	related operand types; result Boolean
< <= > >=	two Integers, two Floats, or two subtypes of Binary; result Boolean
in, not in	list membership; compatible element types; guards use literal lists (§6.5)
and or	Boolean × Boolean → Boolean
unary not	Boolean → Boolean
unary -	Integer → Integer or Float → Float

Equality compares complete runtime values using strict Elixir === / !==. Operands must be related by assignability in at least one direction; two atom singletons are also comparable. This admits a union and one of its members, String and Binary, and two values of the same A: Eq parameter. Unbounded parameters, unrelated parameters A and B, or Integer and Float, cannot be compared directly. Narrow or explicitly convert values into a compatible domain first. Direct Term comparisons are rejected, including Term nested in collections, records, tuples, and stored data representations. Pins apply the same equality-admission rule.

Equality does not insert conversions or establish nominal type identity. It observes extra runtime fields even if a foreign value violates a trusted exact-record signature. Gale has no === or !== spelling and no coercing equality operator or raw term-comparison API.

Ordering compatibility is symmetric. Both bytes < text and text < bytes typecheck. Integer/Float ordering requires explicit numeric conversion, just like arithmetic; / remains Float-only. Integer division and remainder are ordinary gale_std.integer.div and gale_std.integer.rem calls. and and or are short-circuit and require Boolean; they do not accept other terms as truthy. Operators are not user-definable.

Operator precedence follows Elixir for the supported operators. In particular, |> binds more tightly than comparisons, so x |> f() == y compares the pipeline result. <> and ++ associate right, below +/- and above in. Neither is permitted in guards.

List subtraction uses gale_std.list.subtract(left, right). It removes the first strictly equal occurrence for each item on the right, preserving remaining order and multiplicity. Numeric a - -b is subtraction of a negated value.

5.11 Blocks and bindings

A block { s1 … sn e } evaluates statements then e, whose type it takes. A bare expression in statement position is evaluated once and its result is discarded, like _ = e. A block used where statements are required must have a final expression; {} is the empty tuple. A new-line ( after a completed expression starts another expression, rather than chaining a call on the previous result. Keep chained calls on the same line. p [: T] = e synthesizes e (or checks it against T) and binds the variables of p, which must be irrefutable (§6.2). Bindings are immutable and lexically scoped; rebinding a name shadows it.

5.12 case

case e { p1 [when g1] -> e1  …  pn [when gn] -> en }

e ⇑ T; each pi is checked against T (§6.1); each gi ⇓ Boolean under the arm’s bindings and is restricted to guard-safe forms (§6.5); arm bodies are checked against the expected type or joined (§5.2). The arms must be exhaustive for T (§6.4). A case with no arms is well typed only when T ≡ Never; it is then exhaustive and has type Never (or the expected type). This is how a Never-typed value is eliminated.

5.13 cond

cond { g1 -> e1 … true -> en }: every gi ⇓ Boolean; the last arm’s condition is the literal true, otherwise a static error; bodies are checked or joined. Each body receives facts from its successful condition. Later conditions and bodies also receive facts from earlier conditions being false.

5.14 if

if g { e1 } else { e2 }

g ⇓ Boolean; e1 and e2 are checked or joined. Recognized type tests narrow bindings separately in the successful and unsuccessful branches. For x : Integer | String, if is_integer(x) gives the first branch Integer and the second String. The expression emits as a case on g.

5.15 with

with { p1 <- e1  …  pn <- en  final } [else { arms }]

Each ei ⇓ Result<Ai, Ei> under the bindings of earlier steps; pi is an irrefutable pattern for Ai. final ⇑ F. Without else, the expression has type Result<F, E1 | … | En> and final is wrapped in Ok. With else, the arms match the value of type E1 | … | En exhaustively, each arm is checked against the expected type when present and otherwise joined with Result<F, Never>; every arm type must be a Result. with introduces no new type and emits the target language’s native with special form with the same Ok/Error shape.

5.16 receive

See §8.2.

6. Patterns

6.1 Forms and binding

A pattern p is checked against a scrutinee type T and produces bindings:

Pattern	Requirement on T	Bindings
_	any	none
x	any	x : T
^x	position admits x’s type (§6.3)	none
literal	T admits the literal’s type (§6.3)	none
-n	numeric literal pattern; T admits Integer or Float	none
(p)	grouping; not a one-tuple	as p
"lit" <> x / "lit" <> _	non-empty string prefix; T admits String	x : String if T is String, else x : Binary
{p1, …, pn}	tuple member of arity n	components
[], [p1, … | tail]	List<A>	each pi : A, tail : List<A>
%{f1: p1, …}	record or struct with every fi static	pi : Ti
C(p1, …), C	ADT with constructor C	field types
%N{f: p, …}	struct N	field types

Inside [ ], | is list cons ([head | tail]), matching Elixir syntax. Everywhere else, | belongs to types and declarations; p1 | p2 is not a pattern. Write separate case, receive, or with … else arms, or use a guard when several values share behavior. (p) is grouping in patterns, expressions and types; one-tuples are unwritable. In receive, all pattern and guard tests happen before a message is consumed. Prefix string patterns have only the shape non-empty "lit" <> variable or _; "" <> rest is a static error. Prefix patterns are allowed in case, receive, and with … else arms, not in ordinary or successful with bindings.

Naming a record key absent from the static shape is a static error. A struct pattern lists any subset of fields. Constructor resolution follows §4.4. Every binding name may occur at most once in one pattern; Gale has no repeated-variable pattern. Equality against an existing value is written as a pin.

A pin ^x compares its position against the value x holds when the match starts; it binds nothing. The name must denote a binding in scope at pattern entry, so a pin never reads a binder introduced by its own pattern: in {x, ^x} the pin refers to the enclosing x while the arm binds a new, distinct x. The pinned variable’s type must be a subtype of the position’s type. Pins are exempt from the one-binding rule. %{x: a, other: ^a} is well formed. An arm whose pattern carries a pin is refutable exactly like a guarded arm (§6.4). A pin survives into the lowered BEAM pattern itself, which is what lets a receive arm such as {:reply, ^tag} keep the VM’s selective-receive optimization (§8.2).

When T is a union, a record pattern %{f1: p1, …} is checked against every record or struct member whose representation can match; every such member must have every fi in its static shape. A known non-map representation is excluded. An opaque member with an overlapping representation, or an extern member with an unknown representation, makes the destructuring pattern a static error because accepting it would inspect a hidden representation. A record member lacking fi cannot match that field under exact-shape semantics. The current checker conservatively requires common fields when checking union record patterns; use separate arms with a shared atom-literal discriminator, such as %{kind: :a, …} and %{kind: :b, …}.

6.2 Irrefutable patterns

_, variables, tuples of irrefutable patterns, record patterns whose sub-patterns are irrefutable, struct patterns whose sub-patterns are irrefutable, and single-constructor ADT patterns whose sub-patterns are irrefutable are irrefutable. Everything else is refutable, including prefix string patterns, pins, and literals. Ordinary bindings and with bindings require irrefutable patterns.

6.3 Narrowing and representation

When T is a union, a pattern first retains every member whose lowered BEAM representation could match; it is a static error if no member matches. A variable binds that narrowed union. Record patterns additionally expose fields present in every retained record or struct member and join (§5.2) each common field’s types. A wildcard sub-pattern does not split members, and record members are split only by common-field sub-patterns (§6.1).

Tuple and list patterns can destructure outer unions. For example, {:ok, Integer} | {:error, String} can be matched with {:ok, value} and {:error, reason}, giving value : Integer and reason : String. When several alternatives remain, corresponding bindings receive their joined types. This does not make List<A> | List<B> equivalent to List<A | B>.

Refutable tuple, list, and partial map patterns may inspect Term. A tuple pattern establishes arity; its unknown elements start as Term and may be refined by nested patterns or guards. A partial map pattern establishes the presence of its atom keys, not an exact record type. Matching a Map<K,V> requires compatible keys and gives fields type V; matching Term gives fields type Term. Construct a record explicitly after decoding its fields. A cons pattern on unknown Term gives its tail type Term, because BEAM cons cells may have improper tails. These refutable checks are not allowed in ordinary or successful with bindings that require irrefutable patterns.

Nominal constructor patterns require an established nominal type. A raw tag inside Term does not establish a constructor’s type arguments. Likewise, patterns must retain overlapping opaque/unknown extern alternatives instead of assuming those values cannot match a visible runtime shape. Destructuring that would invent nominal identity or payload types is rejected.

6.4 Exhaustiveness and redundancy

case and receive arms must cover the scrutinee type. Coverage is decided by a standard constructor-matrix algorithm over the lowered pattern space: atoms (finite for literal unions and ADT tags, open for Atom), integers, floats and binaries (open; covered only by wildcards), tuples by arity, lists by [] / cons, maps by required keys, and structs by module tag. A prefix string pattern is treated exactly as a string-literal arm: unreachable after a wildcard, and otherwise not analysed for prefix containment. Recognized total type tests and atom-literal membership can contribute to coverage when they are guaranteed true for a variant. Boolean combinations are evaluated in short-circuit order. Thus complementary is_integer/is_binary guards cover Integer | String, including inside tuple and record fields and ADT payloads. Arbitrary predicates, such as n > 0, do not establish complete coverage. Pins (§6.1) also cannot cover a case alone: equality with an existing value can fail. A non-exhaustive case is a static error. An arm that can never match given earlier arms is also a static error.

6.5 Guards

A guard is a Boolean expression built from variables, literals, the operators of §5.10 except <> and ++, the membership test e in [l1, l2, …], and these prelude BIFs:

is_atom is_binary is_boolean is_float is_integer is_list
is_map is_nil is_number is_pid is_reference is_tuple
is_function is_function/2
byte_size map_size is_map_key map_get length abs

In a guard, e in [l1, l2, …] requires a list of literals (atom, integer including negative, float, string, boolean, nil). Each li must be <: the type of e, except atom literals may test any atom-typed binding (including a narrowed singleton that makes the test always false). Empty literal lists are allowed. Outside guards, in and not in accept typed lists and emit the native Elixir operators. There is no range syntax; use gale_std.range for native ranges. No other expression or call is guard-safe. Guards cannot bind variables.

A positive type-test guard refines its tested binding while the arm body is checked. The refinements are is_binary to Binary, is_integer to Integer, is_float to Float, is_boolean to Boolean, is_atom to Atom, is_number to Integer | Float, is_pid to AnyPid, is_map to Map<Term, Term>, is_nil to :nil, and is_reference to Ref. Known nominal representations retain their identity rather than becoming a different type. is_tuple and is_function remove known nonmatching union members. Gale has no universal tuple or function type, so either predicate leaves an arbitrary Term as Term; destructure a tuple with a tuple pattern and call a function through a statically known fn(…) -> … type. is_function(value, arity) is guard-safe but does not add a callable function signature. is_list preserves known List<T> alternatives and excludes non-list alternatives, but cannot promote arbitrary Term to a proper List<Term>: BEAM’s test also accepts improper cons cells. Use decode.list to validate unknown lists, including their tails. When e is a variable and every in literal is an atom (including true, false, nil), the arm sees e as the atom union intersected with its declared type. Integer, float, and string lists refine nothing. and checks its right side with successful-left facts; or uses unsuccessful-left facts. not exchanges success and failure facts. False paths remove fully excluded members of known unions; a positive atom-membership test also removes known non-atom members. Complements of arbitrary Term and unknown extern representations remain conservative. Type-test predicate refinements and the Boolean-combination rules also apply in ordinary Boolean expressions, if, and cond; in remains guard-only. Disjunction merges possible successful paths without assuming either alone must have held. Arbitrary calls do not acquire type-predicate semantics. A later case arm receives the expressible remainder of earlier arms. This includes the scrutinee itself and inspected tuple or record fields. A remainder that would require an occurrence type for a particular list position or ADT payload is not invented; write the complementary guard on that later arm. A guard the static type already decides (is_binary(s) on s : String) is not an error: it refines to the same type, or to Never when the test cannot hold.

Types do not automatically become function-head guards. A parameter declared as Binary is a static contract, not an instruction to emit when is_binary(parameter). Guards are emitted when source control flow actually discriminates a broader value. The backend may lower an equivalent top-level case into function clauses without changing that rule.

7. Binaries

String is UTF-8 text; Binary is any byte-aligned binary. String <: Binary and they share a runtime value. A string literal is a UTF-8-encoded String. Unicode operations live in gale_std.string, while byte-oriented operations live in gale_std.binary. is_binary refines Term to Binary, never String. Prefix matching "GET " <> rest lowers to <<"GET ", rest::binary>> and types rest from the scrutinee.

Arbitrary non-byte-aligned bitstrings and general <<…>> construction or pattern syntax are deferred together. Until that feature exists, a foreign API that really returns an arbitrary bitstring can be modeled conservatively as Term; is_binary refinement safely accepts its byte-aligned results.

8. Processes and mailboxes

8.1 Mailbox capability

A function or lambda with receives M runs with mailbox M. Inside it, and only there:

• receive is permitted and its user arms are typed against M;
• a call whose function type carries receives M' requires unify(M, M').

A function without receives has no mailbox; calling a mailbox-requiring function from it is a static error. The capability is part of the function type and compared exactly (§3.1). self needs no special rule: its stdlib type is fn() receives M -> Pid<M>, so calling it instantiates M and the call rule unifies that variable with the enclosing mailbox. spawn and spawn_link take fn() receives M -> A and return Pid<M>; a worker without receives is accepted by the no-mailbox subtyping rule and yields Pid<Never> after defaulting. send takes Pid<M> and M. These are stdlib externs, not syntax.

8.2 receive

receive {
  p [when g] -> e                 # user arm, p checked against M
  down(m) d -> e                  # m : Monitor; d : Down
  exit(s) x -> e                  # s : TrapExit; x : ExitEvent
  after t -> e                    # t : Timeout
}

User arms must be exhaustive for M (§6.4) unless a wildcard arm is present. VM-event arms require an in-scope value of the named capability type; they lower to the BEAM patterns {:DOWN, ^ref, :process, pid, reason} and {:EXIT, pid, reason}, with is_pid(pid) guards. They do not widen M or contribute to its application message coverage. The event binding receives the complete Down or ExitEvent tuple, including its process and reason fields. _ may discard it. A monitor capability is pinned before introducing the event binding, so reusing its name for the event does not change which monitor the arm matches. The PID guards prevent malformed sender fields from entering a handler typed with AnyPid. after requires t ⇓ Timeout (§2.1); its body joins with the arms. The whole expression is checked or joined like case.

An unguarded _ covers every remaining declared message. It consumes a matching message; it does not leave that message queued for later. A timeout is not a handler for missing message variants and does not satisfy coverage.

M is a closed protocol, not an Erlang filter: because user arms are exhaustive for M, every message that obeys the Pid<M> contract is consumed by some arm. The compiler generates no implicit catch-all. VM events for which no arm is present and foreign terms that match no written source pattern stay queued, as in Erlang; an explicit wildcard arm may consume foreign terms that violate the modeled Pid<M> contract (§1.2).

Pinning a value that existed before the receive, for example {:reply, ^ref, result} -> result with a reference or tag created earlier, lowers to the BEAM pin pattern itself, so the VM can skip messages already sitting in the mailbox instead of scanning them (selective receive). A when guard cannot trigger that optimization, which is why the monitor arm above is pinned rather than guarded.

8.3 Process reference types

AnyPid is built in. The stdlib declares Pid<M>, Ref, Monitor, and Timer as extern types and TrapExit as an opaque capability. The compiler recognizes these exact gale_std.process types: Pid<M> as a pid and Ref, Monitor, and Timer as references for representation checks and typespec emission. Unrelated types with the same basename remain ordinary nominal types. Pid<M> is invariant and is a subtype of the non-sendable AnyPid; M is erased at runtime (§11.3). Monitor and Timer are not subtypes of Ref. None of Ref, Monitor, or Timer can appear in a schema or decoder result; is_reference refines Term to Ref only.

9. Failures

Gale has one class of function. Panics, exits, and timeouts are not reflected in types. A foreign exception is reflected only when an extern explicitly declares raises E; that boundary converts the declared exception to Result<_, E> as specified in §4.8. Otherwise a stdlib operation preserves the native BEAM failure behavior or uses an ordinary Gale function to normalize an expected result. The compiler diagnoses obviously invalid literals in BEAM option positions but makes no general value-range claim; ordinary types make no range claim.

10. OTP

OTP has no compiler-specific syntax or checking rule. The standard library models it with extern behaviours, ordinary functions, unions, module values, and erased handle parameters. Implementations therefore follow §4.9 and emit native callback modules without use macros or runtime adapters. Exact OTP contracts are listed in the standard library.

11. Runtime boundary

11.1 Trusted typed interfaces

An extern signature is a contract asserted by the programmer or standard library. The compiler typechecks Gale callers against it but cannot check that the foreign implementation obeys it. Generic stdlib handles follow the same rule: their type arguments describe the resource contract and are trusted at runtime.

Consequently, normal operations on Pid<M>, typed OTP references, Ets<Name, K, V>, registries, persistent keys, and similar handles neither carry nor invoke hidden validators or decoders. Incorrect foreign use is a violated interop contract and may fail at runtime; it does not make every correctly modeled operation pay a validation cost.

A value whose shape is not part of a trusted contract enters Gale as Term. Decoder<A> = fn(Term) -> Result<A, DecodeError>, encoders, validators, and schema values are ordinary library abstractions used explicitly where an API really handles dynamic data. They are not reserved words, declaration modifiers, implicit evidence, or compiler-derived values.

11.2 Development and test checks

Ordinary output uses Elixir @spec, @type, @opaque, and @typep. When runtime_typechecks is enabled, the compiler wraps every Gale function and extern forwarding function in Gale.Check.call. The wrapper validates its named arguments, runs the original body once, and validates the result. Caller metadata comes from the macro expansion site, so errors identify the module, function, arity, argument name, and nested value path.

Checks use compiler-emitted descriptors rather than Elixir typespec functions. Named and recursive types resolve through one hidden descriptor function on the type’s owning module. A Gale type and function can therefore lower to the same name and arity without colliding.

What those checks can see is the runtime representation, not the full Gale type. Erased parameters (§11.3) are checked as their representation: a Pid<M> is checked as pid(), a ServerRef<M> as its handle representation, a Term as term(). Record checks enforce their exact declared keys and field types. String checks additionally validate UTF-8; plain BEAM specs remain String.t(). Extern-struct checks require the native module and recursively validate their declared fields while allowing additional native fields. They return the original value unchanged. Function values are checked for arity; these checks do not wrap foreign callbacks to enforce their argument and result types. Unconstrained function type parameters are erased to Term. The checks therefore find extern implementations and foreign callers that violate the representation contract; it cannot detect a foreign process sending the wrong M. It is a debugging aid, not part of the guarantees of §1.1.

Ordinary output performs no runtime type validation.

11.3 Erased parameters

Mailbox, service, message, and resource type parameters are compile-time information. For example, Pid<M> is represented by a pid and a typed ETS handle by the underlying table identifier; their parameters are not stored as runtime type evidence. The trusted-interface rule of §11.1 applies whenever such values cross into foreign code.

12. Projection

12.1 Representation

Gale	BEAM value	Elixir typespec
Integer / Float	integer / float	integer() / float()
String	UTF-8 binary	String.t()
Binary	binary	binary()
Atom / :a / Boolean	atom	atom() / :a / boolean()
{T…}, {}	tuple, {}	{…} / {}
record	map with required atom keys	%{f: t}
ADT	atom or tagged tuple	union of atoms/tuples
struct	Elixir struct	Module.t()
extern struct	native Elixir struct	generated Gale @type name() :: %Module{...}
List<A> / Map<K,V>	list / map	[a] / %{optional(k) => v}
gale_std.map_set.MapSet<A>	Elixir MapSet	MapSet.t(a)
fn(A…) -> B	closure	(a… -> b)
Pid<M> / AnyPid	pid	pid()
Ref / Monitor / Timer	reference	reference()
mod …	module atom	module()
Term / Never	any / none	term() / none()
represented opaque	declaring representation	generated @opaque
marker opaque	no values	none()
ChildSpec<A>	map	map()
extern type	foreign value	generated @type … :: term() unless built in

12.2 Typespec emission

Every emitted function has a spec. Function type parameters are erased to term() in that spec; type-declaration parameters remain typespec variables. Mailbox and other phantom parameters are erased. Behaviour implementations carry module-qualified @behaviour and @impl. Gale behaviours use the generated module name; extern behaviours keep the native spelling from extern "…" declares.

An exact Never parameter emits none(), including on behaviour callbacks. The generated empty-case body rejects every foreign value. A Never result emits no_return(). Gale’s checker enforces static language contracts; Dialyzer is not part of the required toolchain.

Optional runtime checks also use compiler-emitted descriptors (§11). Typespecs describe a less precise projection of Gale types: a Pid<M> is pid(), a record is an open map, a mod B<T…> is module(), and String.t() is checked as a binary. A consumer reading the specs learns the representation contract, never the Gale type.

12.3 Calling convention

Checked calls are classified for emission as: LocalCall → local call; StaticModuleCall → Module.function(args); DynamicModuleCall → module_atom.f(args) with the module in a variable; ClosureCall → fun.(args); and ExternCall → the local generated extern wrapper. Only that wrapper’s body names the declared native MFA, with absolute Elixir module names so a Gale alias cannot redirect it; ordinary Gale callers call or reference the wrapper. Gale == and != lower to strict Elixir === and !==. The emitter consumes resolved, typed Core; it never performs name resolution or type-directed redispatch.

The compiler’s builtin namespace exposes the native prelude operations under qualified names such as builtin.length. These names use checked primitive identities and emit native calls. Static aliases and function references work; the namespace itself is not a runtime module value or a mod type.