Introduction

Purpose and Audience

Core Solidity is an update to the Solidity programming language. It both extends the language with new features (ADTs, Parametric polymorphism, Typeclasses), and diverges from Classic Solidity in incompatible ways (most notably by removing inheritance). This document targets compiler implementers, tooling developers, and language researchers. It is a reference specification, not a tutorial.

A prototype implementation exists at argotorg/solcore. The implementation is a research prototype. It contains bugs, lacks optimizations, and will change.

Compilation Architecture

Compilation proceeds by succesive translation between the following representations:

1. Core Solidity: The user-facing language with all syntactic features. Supports higher-order functions, pattern matching, type classes, and modules. This is a superset of SAIL, with all additional language constructs being defined in terms of desugaring passes (syntactic transformations) into SAIL.

2. SAIL: A minimal first-order intermediate representation. All syntactic sugar has been removed. Type classes are resolved to concrete instances. Polymorphic functions are specialized to monomorphic versions. Pattern matching is compiled to simple case trees.

3. Hull: A low-level representation close to Yul. Retains algebraic data types (binary sums and products) but otherwise resembles Yul. Hull code is translated directly to Yul, which is then compiled to EVM bytecode.

4. Yul: The existing Yul assembly language currently used in solc. Core Solidity is designed in a way that allows the use of alternative or additional representations at this level in the future.

Each transformation step simplifies the language and moves closer to the EVM execution model.

Document Structure

• Compilation Pipeline: Describes the compilation pipeline and how representations relate
• SAIL: Specifies the desugared intermediate representation
• Core Solidity: Specifies the user-facing language features
• Hull: Specifies the low-level IR before Yul emission

Status

This is a research prototype. The language design is not stable. Features may be added, removed, or changed. The implementation has known bugs and missing functionality. Do not use this for production systems.

SAIL

SAIL (Solidity Advanced Intermediate Language) is the source language of the Core Solidity compiler. It extends Solidity's surface syntax with a statically-typed functional core: angle-bracketed generic parameters, traits for constrained overloading, and algebraic data types with exhaustive pattern matching. Every SAIL program is compiled to monomorphic Core IR, named Hull, through specialization, then translated to Yul and assembled into EVM bytecode.

This section documents the SAIL language itself. The chapters are ordered from the most foundational concepts to the most advanced:

• Syntax covers lexical conventions, literals, and the overall structure of a source file.
• Built-ins lists the types, values, and operators available without any import, along with the full set of EVM opcodes accessible inside assembly blocks.
• Variable Declaration and Assignment explains let bindings and mutation.
• Functions describes function signatures, free functions, contract methods, and recursive definitions.
• Assembly Blocks details the rules for embedding raw Yul inside a SAIL function body.
• Datatypes introduces algebraic data type declarations and pattern matching.
• Parametric Polymorphism explains generic parameter lists, type variable instantiation, and the specialization strategy.
• Type Classes covers trait declarations, impl declarations, superclass constraints, and the three soundness conditions the compiler enforces.
• Modules describes the import and export system, qualified names, and visibility rules.
• Type Inference explains the bidirectional constraint-based algorithm, what must be annotated explicitly, and the error messages the compiler produces when inference fails.

Source syntax

This compiler follows the source grammar implemented by solcore-rs on its new-syntax branch (reference revision 59f11626, including the parser's existing pragma, export, and type-alias extensions), with named-field structs carried forward from local main. Sources and imported modules use .sol. A module a.b maps to a/b.sol relative to the importing module's directory.

Older source spellings are not accepted. In particular, there are no data, class, instance, or forall declarations, postfix type locations or array types, as expressions, named function results, or destructuring let bindings. Interface and library declarations are outside this grammar.

Modules

Imports and declarations may be interleaved:

import std;
import * from std;
import * from std hiding {debug};
import * as math from @vendor.math;
import {foo, bar as baz} from lib.helpers;

Plain imports introduce module qualifiers. Wildcard and selective imports open public names and may have a hiding clause. A wildcard is written *, not {*}. Selectors and hiding lists may name operators using parentheses, such as (+). String-path imports and the former import M.{item} spelling are rejected.

The reference parser retains these export forms:

export {foo, Option(*), Result(Ok), (+)};
export helpers;
export helpers as publicHelpers;
export helpers.{foo, Option(*)};
export helpers.*;

Pragmas

The implemented switches use their hyphenated names, with an optional list of target identifiers:

pragma no-coverage-condition;
pragma no-patterson-condition Trait;
pragma no-bounded-variable-condition Trait;
pragma no-generic-instance-for MyType;

The pragma parser also preserves unknown identifier directives. It does not accept the former pragma solcore ... namespace or Solidity version expressions.

Types and bindings

Named bindings put their name before a colon and type. Type arguments use nonempty angle-bracket lists; tuple and function types may be empty.

word
Option<word>
collections.Map<address, Option<word>>
(word, bool)
mapping(address => word)
array<word>
memory<DynArray<word>>
calldata<array<word>>
storage<mapping(address => word)>
function(word, bool) returns (word)
function(word)
@word

@T is a type witness in expression position and abbreviates Proxy<T> in type position. Locations are ordinary unary constructors (memory<T>, storage<T>, calldata<T>); there are no T memory, T[], or T[N] forms.

let count: word = 1;
let inferred = compute();
let output: word;
let witness: @word = @word;
let values: memory<DynArray<uint256>> = [1, 2, 3];
let constant: comptime<word> = 42;

Local bindings introduce one identifier. An initializer uses =, never :=. Comptime parameters use comptime name: Type; comptime locals and results use comptime<Type>.

The parser also accepts comptime<Type> inside other types. The current compiler supports its evaluation mode only on direct local bindings and function results, alongside the comptime parameter modifier. Nested uses, including enum payloads, type arguments, aliases, and function-type inputs or results, produce a diagnostic at the unsupported type instead of discarding the compile-time requirement.

Transparent type aliases retain the reference parser's type syntax and parenthesized binders, including inside contracts:

type Word = word;
type PairOf(a) = (a, a);

Functions and contracts

Named function parameters require types. Omitting returns declares a unit result. Result entries are positional types; multiple entries form a tuple.

function identity<T>(value: T) returns (T) { return value; }
function pair(x: word) returns (word, word) { return (x, x); }
function nop() {}
function increment(x: word) returns (word) { x + 1 }
function constant(comptime x: word) returns (comptime<word>) { return x; }

Only a named function may end with an implicit result expression without a semicolon. Nested blocks, match arms, lambdas, constructors, and fallbacks require statement terminators.

contract Counter {
    value: word;
    constructor(initial: word) payable { value = initial; }
    function read() public returns (word) { return value; }
    function update(next: word) public payable { value = next; }
    fallback() payable { return; }
}

Contract functions accept public, then payable, before returns and where. Constructors and fallbacks are implicitly public and accept only payable. Top-level functions and trait/impl methods take neither attribute. There are no external, internal, private, pure, view, or receive declaration forms.

Lambdas retain lam, allow inferred parameters, and use an optional arrow result:

let increment = lam (x: word) -> word { return x + 1; };
let identity = lam (x) { return x; };

Enums, structs, traits, and implementations

enum Option<T> { None, Some(T) }

trait Eq<T> {
    function eq(left: T, right: T) returns (bool);
}

impl<T> Eq<Option<T>> where T: Eq {
    function eq(left: Option<T>, right: Option<T>) returns (bool) {
        match ((left, right)) {
            case (.None, .None) { return true; }
            case (.Some(x), .Some(y)) { return Eq.eq(x, y); }
            default { return false; }
        }
    }
}

The first trait parameter is the instance-head type. Further parameters are trait arguments. where T: Convert<U> constrains Convert<T, U>; multiple constraints are comma-separated and may be enclosed in parentheses. default impl is supported. An enum may have no variants, and each variant may have positional payload types. #[derive(...)] accepts a nonempty list of trait paths and is supported on top-level and contract-local enums. Explicit derives use the Generic representation and the existing trait implementations for its components.

Structs extend the reference grammar with named product fields. They accept the same angle-bracket type parameters and derive attributes as enums, at top level or inside contracts. Each field has a type and ends with a semicolon; field names must be unique within the struct. Constructors take values in field order:

#[derive(Eq)]
struct Pair<T> {
    left: T;
    right: T;
}

function first(value: Pair<word>) returns (word) { return value.left; }
function pair() returns (Pair<word>) { return Pair.Pair(1, 2); }

A member read evaluates its receiver once. Storage-backed struct fields support member updates through the storage API. A contract-local struct's type belongs to its declaring contract, so separate contracts can reuse the same type name.

Constructors use qualified names (Option.Some(1)) or expected-type shorthand (.Some(1)); the same forms appear in patterns. Tuple patterns and _ are supported in matches. Every match has at least one case/default arm, with default last. A comptime label is written case comptime expression { ... }.

Expressions and statements

Calls, member calls, indexing, tuples, array literals, and ternary expressions are supported. Unary operators are ! and ~; binary operators are *, /, %, +, -, &, ^, |, comparisons, equality, &&, and ||. Precedence matches the reference parser; bitwise operators bind more tightly than comparisons. Comparison and equality operators do not chain. There are no unary +/-, shifts, exponentiation, increment/decrement, or as expressions.

Statements include let, assignment, expressions, return, blocks, if, while, for, break, continue, match, and assembly. Compound assignments are +=, -=, *=, /=, %=, &=, |=, ^=, and unary ~=. Address expressions in compound assignments are evaluated once. for headers may contain comma-separated declarations/assignments and omit each header part. There are no unchecked blocks or bare revert statements.

Assembly blocks use the reference Yul source grammar. Compiler-internal Yul quotation templates are not source-language expressions.

Lexical rules

Identifiers start with a Unicode letter and continue with Unicode letters, numbers, or underscores. _ is a wildcard, not a binding name. Hyphenated identifiers are restricted to pragmas; put spaces around subtraction. Nested block comments and line comments are supported. Strings use double quotes and the escapes \n, \t, \", and \\. Integers are decimal or lowercase-0x hexadecimal. List trailing-comma rules follow the reference parser; ordinary function calls do not permit a trailing argument comma.

Built-ins

SAIL provides a small set of types, values, and operators that are available in every source file without any import. These are wired into the compiler's initial environment. In addition, every assembly block has access to the full set of EVM opcodes through Yul primitives.

Primitive Types

Five types are built into the language kernel.

pair and sum are the internal representation of all user-defined algebraic data types. A data type with multiple constructors is encoded as a nested sum, and a constructor with multiple fields is encoded as a nested pair. User code rarely names pair or sum directly; they appear implicitly through enum declarations and tuple syntax.

word

word is the only numeric type at the kernel level. Every integer literal in SAIL has type word. There is no numeric overloading: 42, 0xff, and 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff are all word values.

function decimals() returns (word) {
    return 18;
}

bool

bool has exactly two constructors, true and false, both of which are always in scope.

function isActive(paused: bool) returns (bool) {
    match (paused) {
        case false {
            return true;
        }
        case true {
            return false;
        }
    }
}

() — Unit

The unit type () has a single value, also written (). Functions that perform side effects and return nothing omit the returns clause.

function setOwner(newOwner: word) {
    assembly { sstore(0, newOwner) }
}

Tuple Syntax

The syntax (A, B) is shorthand for pair<A, B>. Tuples with more than two elements are right-nested pairs: (A, B, C) means pair<A, pair<B, C>>.

enum Transfer {
    Transfer(word, word, word)
}

function unpack(t: Transfer) returns ((word, word, word)) {
    match (t) {
        case Transfer(from, to, amount) {
            return (from, to, amount);
        }
    }
}

Infix Operators

SAIL provides eight infix operators as syntactic sugar over ordinary function calls. The parser rewrites each operator to the corresponding function call before name resolution; the functions themselves must be in scope at the point of use.

The table uses -> only as compact mathematical notation for inferred type schemes; source function types use function(...) ... returns (...).

Because the operators desugar to function calls, the compiler resolves them through the normal type class and name resolution machinery. The functions lt, gt, le, ge, ne, and, or, and not are not built into the kernel; they must be brought into scope before use.

Note The && and || operators do not short-circuit in the current implementation. Both operands are always evaluated before the logical operation is performed.

import {lt, ge, and} from std;

function isValidAmount(amount: word, balance: word) returns (bool) {
    return amount > 0 && amount <= balance;
}

The invokable Trait

The kernel defines one built-in type class:

trait invokable<Self, Args, Ret> {
    function invoke(self: Self, args: Args) returns (Ret);
}

invokable is the compiler's mechanism for encoding higher-order functions. When a function-typed value is passed as an argument or stored in a data structure, the compiler generates an invokable implementation that captures the closure and implements invoke. User code rarely interacts with invokable directly. A dedicated chapter covers higher-order functions and the defunctionalization transformation in detail; see Lambda Functions.

Assembly Primops

Inside an assembly { } block, all EVM opcodes are available as Yul primitives. Each opcode is treated as a function that operates exclusively on word values. Variables declared in the surrounding SAIL scope are accessible by name inside the block.

The sections below list every available opcode grouped by category, along with its Yul type signature. As in the operator table above, -> is mathematical type-scheme notation in these tables, not SAIL source syntax.

Arithmetic

function checkedAdd(x: word, y: word) returns (word) {
    let result: word;
    let overflow: word;
    assembly {
        result   := add(x, y)
        overflow := lt(result, x)
    }
    if (overflow != 0) {
        assembly { revert(0, 0) }
    }
    return result;
}

Bitwise

Comparison

Comparison opcodes return 1 if the condition holds and 0 otherwise. The result type is word, not bool; use tobool or a match on the result to convert.

function isOwner(account: word) returns (bool) {
    let owner: word;
    let result: word;
    assembly {
        owner  := sload(0)
        result := eq(account, owner)
    }
    if (result != 0) {
        return true;
    } else {
        return false;
    }
}

Hashing

function storageSlot(account: word) returns (word) {
    let slot: word;
    assembly {
        mstore(0, account)
        slot := keccak256(0, 32)
    }
    return slot;
}

Memory

Storage

function transfer(to: word, amount: word) {
    let callerSlot: word;
    let toSlot: word;
    let senderBal: word;
    let recipientBal: word;
    assembly {
        callerSlot   := caller()
        toSlot       := to
        senderBal    := sload(callerSlot)
        recipientBal := sload(toSlot)
        sstore(callerSlot, sub(senderBal, amount))
        sstore(toSlot,     add(recipientBal, amount))
    }
}

Call Data

Return Data

Code

Control Flow

return and revert have a polymorphic return type a because execution does not resume after them; they can appear in any expression position regardless of the expected type.

Stack and Program Counter

Gas

External Calls

Contract Creation

Logging

function emitTransfer(from: word, to: word, amount: word) {
    let transferTopic: word;
    assembly {
        transferTopic := 0xddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef
        mstore(0x00, amount)
        log3(0x00, 0x20, transferTopic, from, to)
    }
}

Blockchain Context

These opcodes expose information about the current transaction and block. All return word.

function onlyOwner(ownerSlot: word) {
    let owner: word;
    let msgSender: word;
    let isAuth: word;
    assembly {
        owner     := sload(ownerSlot)
        msgSender := caller()
        isAuth    := eq(msgSender, owner)
    }
    if (isAuth != 0) {
        return;
    } else {
        assembly { revert(0, 0) }
    }
}

Variable Declaration and Assignment

SAIL distinguishes two kinds of mutable state: local variables declared inside function bodies and field variables declared inside contract bodies. Local variables exist only for the duration of a function call; field variables persist in contract storage across transactions.

Local Variable Declaration

A local variable is introduced with the let keyword inside a function body. The type annotation and the initialiser are both optional.

Declaration without annotation or initialiser

let x;

The compiler assigns a fresh type variable to x and infers its type from subsequent uses. The variable must be assigned before it is read; the compiler does not insert a default value.

Declaration with a type annotation

let bal: word;

The type is fixed to word at the point of declaration. The variable is still uninitialized; it must be assigned before use.

function loadBalance(account: word) returns (word) {
    let bal: word;
    assembly { bal := sload(account) }
    return bal;
}

Declaration with an initialiser

An initialiser provides a value at declaration time. The type may still be omitted and will be inferred from the initialiser expression.

let amount = 100;        // type inferred as word
let fee: word = 3;       // type annotation and initialiser together

Initialised declarations are useful when the right-hand side is an expression whose type would otherwise be ambiguous:

enum Result {
    Ok(word),
    Err(word)
}

function safeTransfer(from: word, to: word, amount: word) returns (Result) {
    let result = Result.Err(0);   // type inferred as Result from constructor
    let bal: word;
    assembly { bal := sload(from) }
    if (gte(bal, amount)) {
        result = Result.Ok(amount);
    }
    return result;
}

Assignment

Simple assignment

An assignment statement writes a new value to an existing variable or to a contract field. The left-hand side must be an lvalue: a name or an indexed expression.

x = expr;

The type of expr must match the declared type of x.

contract Vault {
    balance: word;

    function deposit(amount: word) {
        let next: word;
        next = balance;
        balance = add(next, amount);
    }
}

Compound assignment

The += and -= operators combine a read, an arithmetic operation, and a write in a single statement.

balance += amount;   // equivalent to balance = balance + amount
balance -= amount;   // equivalent to balance = balance - amount

Compound assignment is most commonly used with contract fields:

contract ERC20 {
    totalSupply: word;
    feePool: word;

    function mint(amount: word) {
        totalSupply += amount;
        feePool     += div(amount, 100);
    }
}

Contract Field Variables

A field variable is declared inside a contract body with a mandatory type annotation and an optional initialiser. Fields are stored in contract storage and retain their values between calls.

contract Token {
    owner: word;
    supply: word;
    paused: bool;
}

Fields are accessed and assigned by name from any function inside the same contract. A field cannot be accessed from a free function.

contract Token {
    supply: word;

    function mint(amount: word) {
        supply += amount;
    }

    function totalSupply() returns (word) {
        return supply;
    }
}

Field initialisers

An optional initialiser sets the field's value at deployment time. It is evaluated once when the contract is deployed.

contract Token {
    supply: word = 0;
}

Contextual Assignment

The left-hand side of an assignment may be any expression that denotes an lvalue. When the expected type of the right-hand side is determined by the left-hand side, the contextual constructor shorthand .Constructor can be used on the right-hand side.

enum Result {
    Ok(word),
    Err(word)
}

function main() returns (Result) {
    let r: Result;
    r = .Ok(0);         // equivalent to Result.Ok(0)
    return r;
}

Conditional Statement

The if statement executes a block conditionally on a boolean expression. An optional else branch handles the false case.

if (condition) {
    // executed when condition is true
}

if (condition) {
    // true branch
} else {
    // false branch
}

if is a statement, so use the conditional expression condition ? yes : no when a value is required:

contract Token {
    paused: bool;

    function transfer(to: word, amount: word) {
        if (paused) {
            assembly { revert(0, 0) }
        }
    }
}

Note The condition must be of type bool. SAIL does not implicitly convert word to bool. Use an explicit comparison (x != 0) when the condition originates from a word value.

For Loop

The for statement provides a C-style counted loop. Its header has three clauses separated by ;:

for ( ForInitStmt ; Condition ; ForPostStmt ) Body

The condition is any expression of type bool; the loop runs while it is true.

Initialisation clause

The init clause runs once before the first iteration. It may:

• Declare a new local variable (typed or untyped, with or without an initialiser):

  for (let i = 0; i < 10; i = i + 1) { ... }
  for (let i: word; i < 10; i = i + 1) { ... }
  

• Assign to an already-declared variable:

  let i: word;
  for (i = 0; i < 10; i = i + 1) { ... }
  

• Use a compound assignment or a plain expression.

Post-iteration clause

The post clause runs after each iteration, before the condition is re-tested. It accepts assignments, compound assignments, and expression statements, but does not introduce new bindings:

let i: word;
let s = 0;
let j = 1;
for (i = 0; i <= 0; i = i + 1) {
    s = j;
}

Complete examples

Accumulate a sum from 1 to 10:

import {Num, Add, Sub, Eq, Ord, Bounded, Typedef, le} from std;

contract Sum {
    function main() returns (word) {
        let s = 0;
        for (let i = 1; i <= 10; i = i + 1) { s = s + i; }
        return s;    // 55
    }
}

Loop variable declared before the for:

contract Sum {
    function main() returns (word) {
        let i: word;
        let s = 0;
        for (i = 1; i <= 10; i = i + 1) { s = s + i; }
        return s;
    }
}

Loop variable shadows an outer declaration:

contract Shadow {
    function main() returns (word) {
        let i = 100;
        let s = 0;
        for (let i = 1; i <= 10; i = i + 1) { s = s + i; }
        // i is 100 here again
        return s;
    }
}

Nested if inside a for body:

contract ForInner {
    function main() returns (word) {
        let result = 0;
        for (let height = 0; height < 7; height = height + 1) {
            if (true) { result = height; } else {}
        }
        return result;
    }
}

Scope rules

A variable declared in the init clause is in scope for the condition expression, the post-iteration clause, and the entire body.

The loop body is its own block; declarations inside it do not escape to the enclosing function.

Note The condition must be of type bool. SAIL does not implicitly convert word to bool. Use an explicit comparison (le(i, 10) or i <= 10) when comparing integer counters.

Expression Statements

Any expression may appear as a statement. The expression is evaluated for its side effects and the result is discarded. This is the standard way to call a function whose return type is ().

function emitTransfer(from: word, to: word, amount: word) {
    assembly {
        mstore(0x00, amount)
        log3(0x00, 0x20, 0xddf252ad, from, to)
    }
}

function main(to: word, amount: word) {
    emitTransfer(caller(), to, amount);    // expression statement: result () is discarded
}

Scope and Shadowing

Local variables are in scope from their declaration to the end of the enclosing block. A variable declared in an inner block shadows an outer declaration of the same name for the duration of that block.

function computeFee(amount: word) returns (word) {
    let fee: word = 1;
    {
        let fee: word = div(amount, 100);    // shadows outer fee inside this block
    }
    return fee;                              // refers to the outer fee; returns 1
}

Note The compiler uses unique identifiers internally, so shadowing is safe and does not cause name collisions in the generated code.

Functions

A function definition introduces a named computation that takes zero or more typed parameters and returns a value of a declared type. Functions can be defined at the top level of a source file, called free functions, or inside a contract body.

function name(param1: Type1, param2: Type2) returns (ReturnType) {
    // body
}

Every top-level function must carry a complete type signature: every parameter must be annotated with its type, and a value-producing function declares its result in a returns (...) clause. A function with no returns clause has the unit result type. The compiler rejects any top-level definition that leaves a parameter unannotated.

Note The complete-annotation requirement applies to free functions and contract methods. It does not apply to lambda expressions or to local bindings inside a function body, where the compiler infers types from context.

Parameters

Parameters are declared as a comma-separated list enclosed in parentheses. Each parameter has the name-first form name: Type.

function transfer(to: word, amount: word) {
    let bal: word;
    assembly { bal := sload(caller()) }
    assembly { sstore(caller(), sub(bal, amount)) }
    assembly { sstore(to, add(sload(to), amount)) }
}

A function that takes no arguments is written with an empty parameter list:

function sender() returns (word) {
    let s: word;
    assembly { s := caller() }
    return s;
}

Return Type

Return types follow the parameter list in a returns (...) clause. Multiple result types are separated by commas.

A function that returns no meaningful value omits the clause:

function emitTransfer(from: word, to: word, amount: word) {
    assembly {
        mstore(0x00, amount)
        log3(0x00, 0x20, 0xddf252ad, from, to)
    }
}

Every execution path through a value-producing body must end with a return statement whose expression has the declared return type. A bare return; returns unit.

Free Functions

A function defined outside any contract body is called a free function. Free functions are visible throughout the file in which they are defined and can be imported by other modules.

function isContract(addr: word) returns (bool) {
    let size: word;
    assembly { size := extcodesize(addr) }
    return gt(size, 0);
}

contract Token {
    function onlyContract(addr: word) {
        if (isContract(addr)) {
            return;
        } else {
            assembly { revert(0, 0) }
        }
    }
}

Polymorphic Functions

A function that works uniformly over multiple types can be made polymorphic by listing generic type parameters in angle brackets after the function name.

function identity<A>(x: A) returns (A) {
    return x;
}

function fst<A, B>(p: (A, B)) returns (A) {
    match (p) {
        case (x, y) {
            return x;
        }
    }
}

Generic type parameters are instantiated at each call site. The compiler specializes the function for every concrete type combination that appears in the program.

Note Polymorphic functions are monomorphized by the specializer before code generation. Each distinct instantiation produces a separate function in the output. A call to identity with a word argument becomes identity$word in the compiled output. No polymorphism survives to the generated Yul.

Constrained Functions

A function may require that one or more of its type variables satisfy a type class constraint. Constraints are written after the return clause in a where clause.

trait Checked<A> {
    function checkedAdd(x: A, y: A) returns (A);
}

function safeTransfer<T>(from: word, to: word, amount: T)
    returns (T)
    where T: Checked
{
    return Checked.checkedAdd(amount, amount);
}

Multiple constraints on different type variables are separated by commas:

function transfersEqual<A, B>(x: (A, B), y: (A, B))
    returns (bool)
    where A: Eq, B: Eq
{
    match ((x, y)) {
        case ((xa, xb), (ya, yb)) {
            return Eq.eq(xa, ya);
        }
    }
}

At each call site the compiler checks that the supplied types satisfy all listed constraints. If no instance is found a type error is reported.

Recursive Functions

A function may call itself recursively. The compiler adds the function name to the typing context before checking the body.

function sumBalances(slot: word, count: word) returns (word) {
    if (eq(count, 0)) {
        return 0;
    } else {
        let bal: word;
        assembly { bal := sload(slot) }
        return add(bal, sumBalances(add(slot, 1), sub(count, 1)));
    }
}

Mutually recursive functions are also supported. The compiler detects mutual dependencies automatically through strongly-connected-component analysis and type-checks the group as a unit. Both functions must be defined in the same file.

enum TxStatus {
    Pending,
    Confirmed
}

function isPending(s: TxStatus) returns (bool) {
    match (s) {
        case TxStatus.Pending {
            return isNotConfirmed(s);
        }
        case TxStatus.Confirmed {
            return false;
        }
    }
}

function isNotConfirmed(s: TxStatus) returns (bool) {
    match (s) {
        case TxStatus.Confirmed {
            return isPending(TxStatus.Pending);
        }
        case TxStatus.Pending {
            return true;
        }
    }
}

Contract Functions

Functions defined inside a contract body have access to the contract's field variables. They follow the same signature rules as free functions.

contract ERC20 {
    totalSupply: word;

    function mint(amount: word) {
        totalSupply = add(totalSupply, amount);
    }

    function getTotalSupply() returns (word) {
        return totalSupply;
    }
}

Contract functions may read and write field variables. Free functions can only operate on their parameters and locally declared variables.

Pattern Matching in Function Bodies

Functions may use match statements to deconstruct algebraic data type values.

enum Result {
    Ok(word),
    Err(word)
}

function unwrapOrZero(r: Result) returns (word) {
    match (r) {
        case Result.Ok(v) {
            return v;
        }
        case Result.Err(_) {
            return 0;
        }
    }
}

Patterns may be nested arbitrarily. The wildcard pattern _ matches any value without binding it. The compiler checks that the set of patterns covers all possible constructors of the scrutinee type and reports an error for incomplete matches.

Assembly in Function Bodies

Functions may contain assembly blocks to access EVM opcodes directly. Inside an assembly block, Yul syntax is used. Variables declared in the surrounding SAIL scope are accessible by name inside the block.

function loadBalance(account: word) returns (word) {
    let bal: word;
    assembly {
        bal := sload(account)
    }
    return bal;
}

Variables assigned inside an assembly block must be declared with let in the enclosing SAIL scope before the block opens. The type of such variables must be word, since Yul operates exclusively on 256-bit machine words.

Warning The type checker cannot verify the semantic correctness of Yul code. Incorrect assembly can produce contracts that silently compute wrong results or revert unexpectedly. Minimize the size of assembly blocks and document any non-obvious invariants.

Missing Annotation Error

Omitting a parameter type on a top-level function is a compile-time error. The compiler reports the offending signature and explains what is missing.

// Error: parameter 'x' has no type annotation.
function bad(x) returns (word) {
    return x;
}

Top-level function must have complete type annotations:
  function bad(x) returns (word)
Annotate every parameter (name: Type).

Type inference remains available inside function bodies for local variables and intermediate expressions. Only the function signature itself requires explicit annotations at the top level.

Assembly Blocks

SAIL allows inline assembly blocks that embed Yul statements directly in a function body. Assembly blocks provide unrestricted access to EVM opcodes and are the primary mechanism for operations that SAIL has no built-in syntax for, such as storage reads and writes, event emission, and ABI encoding helpers.

function loadBalance(account: word) returns (word) {
    let bal: word;
    assembly {
        bal := sload(account)
    }
    return bal;
}

Warning The type checker cannot verify the semantic correctness of Yul code. Incorrect assembly can produce contracts that silently compute wrong results or revert unexpectedly. Minimize the size of assembly blocks and document any non-obvious invariants.

Yul Sublanguage

The contents of an assembly { … } block are written in Yul, the low-level intermediate language used by the Solidity compiler. Yul operates exclusively on 256-bit machine words, the native value type of the EVM.

SAIL variables whose type is word are accessible by name inside the block. Variables of other SAIL types cannot be referenced directly in Yul.

Variable Declaration

Inside an assembly block, Yul variables are declared with let and assigned with :=. Yul let is separate from SAIL let: Yul variables exist only within the enclosing Yul block.

assembly {
    let ptr := mload(0x40)   // Yul variable; exists only in this block
}

Multiple names may appear on the left-hand side of a single let to receive the multiple return values of a built-in opcode:

assembly {
    let success, returndata := call(gas(), target, value, argOffset, argSize, 0, 0)
}

Assignment

An assignment in Yul uses :=. The left-hand side must be either a Yul variable or a SAIL word variable in scope.

function storeBalance(account: word, amount: word) {
    assembly {
        sstore(account, amount)   // EVM opcode: write amount to storage slot account
    }
}

Assigning to a SAIL variable communicates a result back to the SAIL scope:

function getFreeMemPtr() returns (word) {
    let ptr: word;
    assembly {
        ptr := mload(0x40)
    }
    return ptr;
}

Conditionals

Yul provides an if statement that executes a block when a condition is non-zero. There is no else branch in Yul; use switch for multi-way dispatch.

assembly {
    if iszero(success) {
        revert(0, 0)
    }
}

Switch

The Yul switch statement dispatches on a value. Each case arm matches a literal. An optional default arm matches any value not handled by a case.

assembly {
    switch selector
    case 0x70a08231 {
        // balanceOf selector
    }
    case 0xa9059cbb {
        // transfer selector
    }
    default {
        revert(0, 0)
    }
}

For Loops

Yul's for statement provides a general loop with an initialisation block, a condition expression, a post-iteration block, and a body block.

contract ERC20 {
    function sumSlots(startSlot: word, count: word) returns (word) {
        let endSlot: word;
        let total: word;
        assembly {
            endSlot := add(startSlot, count)
        }
        assembly {
            for { let i := startSlot } lt(i, endSlot) { i := add(i, 1) }
            {
                total := add(total, sload(i))
            }
        }
        return total;
    }
}

The initialisation block may be empty ({}). break, continue, and leave control loop execution:

Nested Blocks

An assembly block may contain nested Yul blocks { … }. Variables declared inside a nested block are not visible outside it.

assembly {
    {
        let tmp := mload(0x00)   // tmp is scoped to this inner block
        mstore(0x20, tmp)
    }
    // tmp is not in scope here
}

Accessing SAIL Variables

Only SAIL variables of type word can be read or written inside an assembly block. This restriction is enforced at compile time: every SAIL name that appears inside Yul must resolve to a variable or parameter whose type is word. Parameters, local variables declared with let, and contract field variables are all subject to this rule.

function transfer(account: word, amount: word) {
    let bal: word;
    assembly {
        bal    := sload(account)      // account and bal are SAIL word variables
        sstore(account, sub(bal, amount))
    }
}

Note Variables assigned inside an assembly block must have been declared with let in the enclosing SAIL scope before the block opens.

Rejected: parameter of type bool

A parameter of type bool cannot be named inside Yul. The compiler reports a type mismatch because Yul has no boolean type and cannot represent the value.

// Error: bool is not word.
function bad(paused: bool) {
    assembly {
        sstore(0, paused)
    }
}

Types: bool and word do not unify
 - in: function bad(paused: bool) { ... }

To work with a bool value inside an assembly block, convert it to a word first using an explicit conditional in SAIL.

Rejected: variable of an algebraic data type

A local variable whose type is a user-defined algebraic data type is equally rejected. Sum and product types are not EVM words and have no direct Yul representation.

enum Result { Ok(word), Err(word) }

// Error: Result is not word.
function bad(r: Result) returns (word) {
    let res: word;
    assembly {
        res := r
    }
    return res;
}

Types: Result and word do not unify
 - in: function bad(r: Result) returns (word) { ... }

To operate on structured values from assembly, extract the relevant word fields first in SAIL, pass them as word parameters or local variables, and perform the Yul computation on those.

Common EVM Operations

The following table lists the EVM opcodes most frequently used in assembly blocks. For the full list see the EVM opcode reference.

Assembly and the Hull IR

Assembly blocks pass through the compilation pipeline unchanged. The SAIL compiler includes them verbatim in the Hull IR, and the Yul code generator reproduces them without transformation. This means the programmer has full control over the generated Yul but also bears full responsibility for its correctness.

Datatypes

SAIL provides algebraic data types (ADTs) for defining structured values. An ADT declares a named type together with one or more constructors. Each constructor describes one way to build a value of that type and may carry zero or more fields of arbitrary types.

enum Option<A> {
    None,
    Some(A)
}

Data types may be defined at the top level of a source file or inside a contract body.

Enumeration Types

The simplest kind of algebraic data type has only nullary constructors with no fields. Such a type acts as a finite enumeration.

enum TokenStatus {
    Active,
    Paused,
    Deprecated
}

Each constructor is a distinct value of the type. Enumerations are commonly used wherever Solidity uses enum.

contract Registry {
    enum TokenStatus {
        Active,
        Paused,
        Deprecated
    }

    function statusCode(s: TokenStatus) returns (word) {
        match (s) {
            case TokenStatus.Active {
                return 1;
            }
            case TokenStatus.Paused {
                return 2;
            }
            case TokenStatus.Deprecated {
                return 0;
            }
        }
    }

    function main() returns (word) {
        return statusCode(TokenStatus.Active);
    }
}

Constructors with Fields

A constructor can carry one or more fields. The field types are listed in parentheses, separated by commas.

enum TxStatus {
    Pending,
    Settled,
    Failed
}

enum TxOutcome {
    Success(TxStatus),
    Revert(TxStatus),
    Unknown
}

A constructor with fields is applied like a function: TxOutcome.Success(TxStatus.Settled) produces a value of type TxOutcome wrapping a value of type TxStatus.

Enum-constructor payloads are extracted by pattern matching; unlike named struct fields, positional payloads have no record-style field access. The pattern mirrors the constructor application:

function outcomeCode(x: TxOutcome) returns (word) {
    match (x) {
        case TxOutcome.Success(TxStatus.Settled) {
            return 1;
        }
        case TxOutcome.Revert(TxStatus.Failed) {
            return 2;
        }
        default {
            return 0;
        }
    }
}

Parametric Data Types

A data type can be parameterized by one or more type variables, making it a generic or parametric type. The type variables are listed in angle brackets after the type name.

enum Option<A> {
    None,
    Some(A)
}

Here A is a type variable. Option<word> is the type of optional words, Option<bool> is the type of optional booleans, and so on. The type variable A may appear in the field types of any constructor.

contract Option {
    enum Option<A> {
        None,
        Some(A)
    }

    function just<A>(x: A) returns (Option<A>) {
        return Option.Some(x);
    }

    function maybe(defaultValue: word, opt: Option<word>) returns (word) {
        match (opt) {
            case Option.None {
                return defaultValue;
            }
            case Option.Some(x) {
                return x;
            }
        }
    }

    function main() returns (word) {
        return maybe(0, Option.Some(42));
    }
}

The type checker verifies that every use of a parametric type supplies the correct number of type arguments. Applying Option to two arguments, for instance, is a type error.

Nested Pattern Matching

Patterns may be nested to arbitrary depth to match inside multiple layers of constructors in a single arm.

enum Option<A> {
    None,
    Some(A)
}

// Unwrap an approval amount nested in two Option layers.
function resolveApproval(outer: Option<Option<word>>) returns (Option<word>) {
    match (outer) {
        case Option.Some(Option.Some(x)) {
            return Option.Some(x);
        }
        default {
            return Option.None;
        }
    }
}

The wildcard _ matches any value without binding it. It can appear at any depth in a pattern.

Opaque Wrappers

A single-constructor, single-field type is the standard idiom for introducing a distinct type that is represented by an existing type at runtime. This is similar to Haskell's newtype or Solidity's user-defined value types.

enum uint256 {
    uint256(word)
}

uint256 is a type distinct from word even though it carries exactly one word field. The type checker treats them as incompatible, preventing accidental mixing. The wrapper is removed during compilation: uint256 values occupy exactly one EVM word, just like word.

Wrapping and unwrapping are done explicitly with the constructor and a pattern:

function wrap(x: word) returns (uint256) {
    return uint256(x);
}

function unwrap(x: uint256) returns (word) {
    match (x) {
        case uint256(w) {
            return w;
        }
    }
}

The standard library defines uint256, bytes4, bytes32, and address this way, each wrapping word.

Phantom Type Parameters

A type parameter that does not appear in any constructor field is called a phantom type parameter. It carries no runtime information but allows the type system to distinguish values that would otherwise be identical.

// A is phantom: the constructor Proxy carries no field of type A.
enum Proxy<A> {
    Proxy
}

Proxy<word> and Proxy<bool> are distinct types at compile time but produce the same runtime value. Phantom types are useful for passing type information to functions without allocating extra memory.

trait MemoryType<A> {
    function size(prx: Proxy<A>) returns (word);
}

impl MemoryType<word> {
    function size(prx: Proxy<word>) returns (word) {
        return 32;
    }
}

The Proxy<A> argument lets the caller select which MemoryType implementation to use without passing an actual value of type A.

Note Because phantom type parameters leave the constructor's result type partially undetermined, the type checker requires an explicit type annotation whenever a Proxy value is constructed in a context where the type cannot be inferred from surrounding expressions. Use an explicit conversion, Proxy as Proxy<word>, to resolve the ambiguity.

Tuples

SAIL has built-in support for product types (tuples). A tuple type is written as a parenthesised, comma-separated list of component types. Tuple values are written the same way.

function swap(p: (word, bool)) returns ((bool, word)) {
    match (p) {
        case (x, b) {
            return (b, x);
        }
    }
}

Tuples of more than two elements are right-nested pairs internally. The type (word, bool, word) is represented as pair<word, pair<bool, word>>.

The unit type () is the zero-element tuple. It carries no information and is used as the return type of functions that exist only for their side effects.

function storeBalance(account: word, amount: word) {
    assembly { sstore(account, amount) }
}

Note Tuple patterns may appear anywhere a pattern is expected, including inside constructor patterns:

impl<A, B> Nth<Zero, (A, B), A> {
    function nth(idx: Proxy<Zero>, tup: (A, B)) returns (A) {
        match (tup) {
            case (x, _) {
                return x;
            }
        }
    }
}

Contextual Constructor Syntax

In a context where the expected type is known, the module qualifier can be omitted from a constructor name by prefixing it with .. The compiler resolves the constructor to the appropriate type automatically.

enum Option<A> {
    None,
    Some(A)
}

function just(x: word) returns (Option<word>) {
    return .Some(x);   // equivalent to Option.Some(x)
}

function nothing() returns (Option<word>) {
    return .None;      // equivalent to Option.None
}

The same shorthand works in patterns:

function isNone(o: Option<word>) returns (bool) {
    match (o) {
        case .None {
            return true;
        }
        case .Some(_) {
            return false;
        }
    }
}

The compiler reports an error if the expected type is not known or if the constructor name is ambiguous.

Type Synonyms

A type synonym introduces a new name for an existing type. Synonyms are purely a compile-time device: the compiler expands them before type checking and they leave no trace in the generated code.

type Int = word;
type Point = pair<Int, Int>;

function makePoint(x: Int, y: Int) returns (Point) {
    return (x, y);
}

function getX(p: Point) returns (Int) {
    match (p) {
        case (x, _) {
            return x;
        }
    }
}

Synonyms can have type parameters, written in parentheses after the name:

type Map(k, v) = pair<k, v>;   // toy example

Warning Recursive type synonyms are not allowed. A synonym must not refer directly or indirectly to itself. Attempting to define type A = B; and type B = A; simultaneously is a compile-time error.

Runtime Encoding

Algebraic data types compile to a uniform binary encoding in the generated Hull/Yul code.

Sum types (types with more than one constructor) are encoded as nested binary sums using inl (left injection) and inr (right injection). A type with n constructors becomes a right-nested binary tree of depth ⌈log₂ n⌉. For example, a three-constructor type enum T { A, B, C } is encoded as:

A  →  inl ()
B  →  inr (inl ())
C  →  inr (inr ())

Product types (constructor fields, tuples) are encoded as right-nested pairs. The three-field constructor enum T { T(word, bool, word) } becomes pair<word, pair<bool, word>>.

This uniform encoding is what the match compiler and the Hull back-end operate on. It is not visible at the SAIL level.

Parametric Polymorphism

A parametric polymorphic function works uniformly over any type. The caller does not need to know which concrete type is used; the function behaves identically for all instantiations. SAIL supports parametric polymorphism through generic parameter lists in function signatures.

Type Variables and Generic Parameters

A type variable is a placeholder for any concrete type. To introduce type variables in a function signature, list their names in angle brackets after the function name.

function id<A>(x: A) returns (A) {
    return x;
}

The signature function id<A>(x: A) returns (A) states that id accepts one argument of any type A and returns a value of the same type A. The same type variable A appears in both the parameter and the return position, so the caller knows that the output type equals the input type.

Multiple type variables are separated by commas:

function fst<A, B>(p: (A, B)) returns (A) {
    match (p) {
        case (x, y) {
            return x;
        }
    }
}

function snd<A, B>(p: (A, B)) returns (B) {
    match (p) {
        case (x, y) {
            return y;
        }
    }
}

Type variables may appear in parameter types, the return type, and in type arguments to other type constructors:

enum Option<A> {
    None,
    Some(A)
}

function just<A>(x: A) returns (Option<A>) {
    return Option.Some(x);
}

function fromOption<A>(defaultValue: A, opt: Option<A>) returns (A) {
    match (opt) {
        case Option.None {
            return defaultValue;
        }
        case Option.Some(x) {
            return x;
        }
    }
}

Call-Site Instantiation

At each call site, the compiler determines the concrete type for every type variable from the types of the supplied arguments. No explicit type application is needed; the inference engine handles instantiation automatically.

function id<A>(x: A) returns (A) {
    return x;
}

contract C {
    function main() returns (word) {
        return id(42);      // A is instantiated to word
    }
}

Each combination of concrete types produces a distinct specialization during compilation. A call to id with a word argument becomes id$word in the generated output, and a call with a pair type becomes a separate function with a distinct name. No polymorphism survives to the generated Yul.

Polymorphic Functions with Pattern Matching

Polymorphic functions frequently deconstruct structured values through pattern matching. The match compiler operates on the inferred type at each call site after instantiation.

enum Pair<A, B> {
    Pair(A, B)
}

function fst<A, B>(p: Pair<A, B>) returns (A) {
    match (p) {
        case Pair(x, y) {
            return x;
        }
    }
}

function snd<A, B>(p: Pair<A, B>) returns (B) {
    match (p) {
        case Pair(x, y) {
            return y;
        }
    }
}

function addAmounts(x: word, y: word) returns (word) {
    let res: word;
    assembly { res := add(x, y) }
    return res;
}

// A transfer record holds (sender address, amount).
function totalTransferred(p: Pair<word, word>) returns (word) {
    return addAmounts(fst(p), snd(p));
}

contract ERC20 {
    function main() returns (word) {
        return totalTransferred(Pair(100, 200));
    }
}

Mutually Recursive Polymorphic Functions

Polymorphic functions may call each other recursively. The compiler resolves mutual dependencies through strongly-connected-component analysis and checks all functions in a group together. Both functions must be defined in the same file.

enum Option<A> {
    None,
    Some(A)
}

function orElse<A>(primary: Option<A>, fallbackValue: Option<A>)
    returns (Option<A>)
{
    match (primary) {
        case Option.Some(v) {
            return Option.Some(v);
        }
        case Option.None {
            return pickFirst(fallbackValue, primary);
        }
    }
}

function pickFirst<A>(x: Option<A>, y: Option<A>) returns (Option<A>) {
    match (x) {
        case Option.Some(v) {
            return orElse(x, y);
        }
        case Option.None {
            return y;
        }
    }
}

The Subsumption Test

When a function declares generic parameters, the compiler verifies that the body is at least as polymorphic as the declared signature. This check is called the subsumption test. It prevents signatures that claim more generality than the body actually provides.

The test works in three steps:

1. The declared type is skolemised: each type variable is replaced by a fresh rigid constant that cannot be unified with any other type.
2. The body is type-checked independently, producing an inferred type.
3. The inferred type must unify with the skolemised declared type. If a rigid constant would need to be unified with a concrete type (such as word), the body is not polymorphic enough and the compiler reports an error.

Error: return type is more polymorphic than the body

The most common subsumption failure occurs when the annotation promises that the function works for any type a, but the body always produces a specific type such as word.

// Error: the body always returns word, but the annotation says a.
function wrong<A>(x: word) returns (A) {
    return x;
}

Type not polymorphic enough! The annotated type is:
forall a . word -> a
but the infered type is:
word -> word
in:
function wrong<A>(x: word) returns (A)

The diagnostic renders inferred type schemes with mathematical forall and -> notation; those tokens are not source syntax. The body return x has scheme word -> word because x is declared as word. The skolemised declared type requires the result to be a rigid variable A, which cannot be unified with word. The compiler rejects the definition.

Error: wrong type variable in the return position

A function that swaps the return type variable is caught by the same test.

// Error: the body returns the first component (type A),
//        but the annotation declares the return type as B.
function fst<A, B>(p: (A, B)) returns (B) {
    match (p) {
        case (x, y) {
            return x;
        }
    }
}

Type not polymorphic enough! The annotated type is:
forall a b . (a, b) -> b
but the infered type is:
forall $t . ($t, $t) -> $t
in:
function fst<A, B>(p: (A, B)) returns (B)

The body returns x, which has the type of the first component. The inferred type therefore unifies both components and the return, making them all the same variable $t. The skolemised declared type requires the return to be the rigid variable B (the second component), which is distinct from A. The unification fails and the compiler reports the error.

Error: type variable forced to word by an assembly block

Assembly blocks operate exclusively on word values. If the body uses a type variable as if it were word inside an assembly block, the inference engine forces that variable to word, making the function monomorphic in the body while the annotation still declares a type variable.

// Error: the assembly block forces A to word,
//        so the body is monomorphic.
function double<A>(x: A) returns (A) {
    let res: word;
    assembly { res := add(x, x) }
    return res;
}

Type not polymorphic enough! The annotated type is:
forall a . a -> a
but the infered type is:
word -> word
in:
function double<A>(x: A) returns (A)

The correct way to write this function is to restrict the parameter type to word explicitly and drop the generic parameter:

function double(x: word) returns (word) {
    let res: word;
    assembly { res := add(x, x) }
    return res;
}

If a computation must be polymorphic in a type class sense (working for all types that support addition), use a constrained type variable instead of an assembly block. See the Type Classes section for details.

Specialization and Naming

The compiler eliminates all polymorphism before code generation through a process called specialization (or monomorphization). Every call site that instantiates a polymorphic function at a concrete type combination produces a separate function definition in the output. The compiler chooses names of the form name$Type for each specialization, for example id$word or fst$word$bool.

This means:

• There is no runtime representation of type variables.
• Each specialized version is compiled independently and can be optimized on its own.
• Whole-program compilation is required: the specializer must see all call sites to determine which instantiations to generate.

Note A polymorphic function that is never called is not emitted at all. Only the specializations that are actually needed by the program appear in the compiled output.

Type Classes

A type class defines a named set of operations that a type must implement. Any type that provides implementations for all required operations is said to be an instance of the class. Type classes enable constrained polymorphism: a function may be parameterized over a type variable and simultaneously require that the variable belongs to one or more classes.

Trait Declarations

A trait declaration introduces a type-class name, a main type variable, and zero or more method signatures. Generic parameters follow the trait name in angle brackets.

trait Eq<A> {
    function eq(x: A, y: A) returns (bool);
    function ne(x: A, y: A) returns (bool);
}

The first type variable, A, is the main type argument of the type class. Every implementation must supply a concrete type for this variable.

A class with no methods defines a pure marker class:

trait Serializable<A> {}

Superclass Constraints

A trait may require that its main type argument already belongs to another type class. This constraint is called a superclass constraint and follows the trait head in a where clause.

trait Ord<A> where A: Eq {
    function lt(x: A, y: A) returns (bool);
    function lte(x: A, y: A) returns (bool);
}

Any implementation of Ord must also satisfy Eq. The compiler verifies this at each impl declaration. If a function requires A: Ord, the constraint A: Eq is automatically available without listing it explicitly.

Impl Declarations

An impl declaration provides implementations for all methods of a trait for a specific type. The impl head names the trait and supplies a concrete type for the main type variable.

impl Eq<word> {
    function eq(x: word, y: word) returns (bool) {
        let res: word;
        assembly { res := eq(x, y) }
        return res;
    }
    function ne(x: word, y: word) returns (bool) {
        let res: word;
        assembly { res := iszero(eq(x, y)) }
        return res;
    }
}

A polymorphic implementation applies to a family of types. Generic parameters on impl list the type variables that appear in the impl head:

enum Pair<A, B> {
    Pair(A, B)
}

impl<A, B> Eq<Pair<A, B>> where A: Eq, B: Eq {
    function eq(x: Pair<A, B>, y: Pair<A, B>) returns (bool) {
        match (x, y) {
            case (Pair(xa, xb), Pair(ya, yb)) {
                return Eq.eq(xa, ya);
            }
        }
    }
    function ne(x: Pair<A, B>, y: Pair<A, B>) returns (bool) {
        return Eq.ne(x, y);
    }
}

Calling Class Methods

Trait methods are called with a qualified name of the form TraitName.method. The compiler resolves the correct implementation from the argument types:

enum Option<A> {
    None,
    Some(A)
}

function senderMatches<A>(sender: A, expected: Option<A>)
    returns (bool)
    where A: Eq
{
    match (expected) {
        case Option.None {
            return false;
        }
        case Option.Some(e) {
            return Eq.eq(sender, e);
        }
    }
}

Overlapping Implementations

SAIL does not support overlapping implementations. Two impls overlap when the same type can match both heads. The compiler reports an error at the second declaration:

enum Box<A> {
    Box(word)
}
trait C<A> {}

impl<A> C<Box<A>> {}

// Error: overlaps with the more general implementation above.
impl C<Box<word>> {}

Overlapping implementations are not supported
impl C<Box<word>>
overlaps with:
impl<T> C<Box<T>>

Main and Weak Type Arguments

When a trait has more than one type parameter, the first parameter is called the main type argument. The remaining parameters are called weak type arguments.

//          main ──┐         ┌── weak
trait Convert<A, B> {
    function convert(x: A) returns (B);
}

The distinction matters for instance resolution and for the three soundness conditions the compiler enforces.

Main type argument (A in Convert<A, B>): used as the primary key for instance lookup. The compiler selects an instance by matching the main type first. It must be determinable independently of the weak arguments.

Weak type arguments (B in Convert<A, B>): represent additional types involved in the relationship. They may be determined by the main type argument through the coverage condition, but they cannot introduce type variables that are unconstrained at the call site.

Example: weak argument determined by main type

In the following instance, the main type Wei uniquely determines the weak type Ether. The instance is well formed because the weak type variable is replaced by a concrete type:

trait Convert<A, B> {
    function convert(x: A) returns (B);
}

enum Wei {
    Wei(word)
}
enum Ether {
    Ether(word)
}

impl Convert<Wei, Ether> {
    function convert(x: Wei) returns (Ether) {
        match (x) {
            case Wei.Wei(w) {
                let e: word;
                assembly { e := div(w, 1000000000000000000) }
                return Ether.Ether(e);
            }
        }
    }
}

contract C {
    function main() returns (word) {
        let result = Convert.convert(Wei.Wei(2000000000000000000));
        match (result) {
            case Ether.Ether(v) {
                return v;
            }
        }
    }
}

Instance Soundness Conditions

To guarantee that instance resolution terminates and remains coherent, the compiler enforces three conditions on every instance declaration. Violating any of them is a compile-time error. Each condition can be relaxed by a pragma when a specific instance is known to be safe.

Coverage Condition

Every type variable that appears in a weak type argument position must be determined by the main type argument. The set of type variables bound by the main type must cover all type variables bound by the weak types.

Rejected example

enum Box<A> {
    Box(word)
}
trait MyClass<A, B> {}

// Error: B appears only in the weak position; Box<A> does not determine B.
impl<A, B> MyClass<Box<A>, B> {}

Coverage condition fails for class:
MyClass
- the type:
Box<A>
does not determine:
B

Accepted example

Replacing the unconstrained variable B with a concrete type eliminates the violation:

impl<A> MyClass<Box<A>, word> {}

Patterson Condition

For each constraint in the instance context, the measure of the constraint must be strictly smaller than the measure of the instance head. The measure of a predicate is the total number of type constructors and type variables it contains, counting repetitions. Each type constructor or type variable contributes 1 to the measure, regardless of nesting.

This condition prevents instance search from entering an infinite loop when the same type class is used in both the context and the head.

Rejected example

trait C1<A> {}
trait C2<A> {}

// Context: U:C1 has measure 2, U:C2 has measure 2, total 4.
// Head:    U:C1 has measure 2.
// Context measure (4) is not strictly smaller than head measure (2).
impl<U> C1<U> where U: C1, U: C2 {}

Instance
U : C1
does not satisfy the Patterson conditions.

Accepted example

Wrapping the main type in a constructor increases the head measure so that each context constraint is strictly smaller:

enum Wrap<A> {
    Wrap(A)
}

// Context: U:C1 has measure 2.
// Head:    Wrap<U>: C1 has measure 3 (Wrap + U + C1 name).
// 2 < 3, so the Patterson condition holds.
impl<U> C1<Wrap<U>> where U: C1 {}

Bound Variable Condition

Every type variable that appears in the instance context must also appear in the instance head. A type variable present only in the context cannot be determined from the types at the call site, making instance resolution ambiguous.

Rejected example

enum Box<A> {
    Box(word)
}
trait Eq<A> {}
trait Container<A, B> {}

// Error: C appears in the context constraint C: Eq
//        but not in the impl head Container<Box<A>, A>.
impl<A, C> Container<Box<A>, A> where C: Eq {}

Bounded variable condition fails!

Accepted example

Remove the unused variable from the context, or include it in the head:

// No context needed.
impl<A> Container<Box<A>, A> {}

// Or: bring C into the head through the weak argument.
impl<A, C> Container<Box<A>, C> where C: Eq {}

Pragmas

A pragma is a compiler directive that relaxes one of the three instance soundness conditions. Pragmas are written at the top level of a source file, before any declarations.

There are three pragmas, one per condition:

Each pragma has two forms:

// Disable for a specific list of classes (comma-separated).
pragma no-coverage-condition ClassName1, ClassName2;

// Disable globally for all classes in this file.
pragma no-coverage-condition;

Pragmas apply only to the file in which they appear. Importing a file does not inherit its pragmas, and the importing file's pragmas do not affect the imported declarations.

Warning Disabling these conditions can allow instances that cause the compiler's instance resolution to loop or produce incoherent results. Use pragmas only when you understand the implications for the specific class and instance involved.

pragma no-coverage-condition

Disables the coverage check for the listed classes. Use this when a weak type argument is deliberately left undetermined by the main type, for example in open type-indexed families where the relationship is established by context rather than by the instance itself.

pragma no-coverage-condition MyClass;

enum Box<A> {
    Box(word)
}
trait MyClass<A, B> {}

// Accepted: coverage condition is disabled for MyClass.
impl<A, B> MyClass<Box<A>, B> {}

Without the pragma, this declaration would produce:

Coverage condition fails for class:
MyClass
- the type:
Box<A>
does not determine:
B

pragma no-patterson-condition

Disables the Patterson measure check for the listed classes. Use this for class hierarchies where the instance search is known to terminate through structural arguments not captured by the simple measure metric.

pragma no-patterson-condition C1;

trait C1<A> {}
trait C2<A> {}

// Accepted: Patterson condition is disabled for C1.
impl<U> C1<U> where U: C1, U: C2 {}

Without the pragma, this declaration would produce:

Instance
U : C1
does not satisfy the Patterson conditions.

pragma no-bounded-variable-condition

Disables the bound variable check for the listed classes. Use this when a context variable is intentionally existential, meaning it is chosen by the instance rather than derived from the call site.

pragma no-bounded-variable-condition Container;

enum Box<A> {
    Box(word)
}
trait Eq<A> {}
trait Container<A, B> {}

// Accepted: bound variable condition is disabled for Container.
impl<A, C> Container<Box<A>, A> where C: Eq {}

Without the pragma, this declaration would produce:

Bounded variable condition fails!

Combining Pragmas

Multiple pragmas may appear in the same file and may target the same class from different directives. All specified conditions are disabled independently:

pragma no-coverage-condition MyClass;
pragma no-patterson-condition MyClass;
pragma no-bounded-variable-condition MyClass;

enum Box<A> {
    Box(word)
}
trait Eq<A> {}
trait C1<A> {}
trait MyClass<A, B> {}

// Accepted: all three conditions are disabled for MyClass.
impl<A, B, C> MyClass<Box<A>, B> where C: Eq, (A, B): C1 {}

Modules

Every SAIL source file is a module. A module can import definitions from other modules and control which of its own definitions are visible to importers through export declarations. The module system provides explicit namespace management: a name imported from another module is not automatically available without qualification unless the import form places it directly into scope.

File Layout

A source file is a sequence of import declarations and top-level declarations in any order. Import declarations may appear before, after, or interleaved with top-level declarations.

( import-declaration | top-level-declaration )*

The conventional style places all imports at the top of the file, but this is not enforced by the compiler.

Import Forms

SAIL provides four import forms. Each form controls how the imported names are placed into scope and whether they require qualification to use.

Full module import

import modname;

Loads the module and makes all its exported names available under the qualified prefix modname. No names are introduced into the unqualified scope.

// token.sol exports: Token, transfer
import token;

function doTransfer(t: token.Token, to: word, amount: word) {
    token.transfer(t, to, amount);
}

Module import with alias

import * as Alias from modname;

Same as a full import but assigns a shorter alias to the module. All qualified references must use the alias; the original module name is not available as a qualifier.

import * as T from token;

function doTransfer(t: T.Token, to: word, amount: word) {
    T.transfer(t, to, amount);
}

After this import, writing token.transfer(t, to, amount) is an error because token is not a known qualifier in this file.

Selective import

import {Name1, Name2} from modname;

Loads the listed names directly into the unqualified scope. They can be used without any prefix.

import {Token, transfer} from token;

function doTransfer(t: Token, to: word, amount: word) {
    transfer(t, to, amount);
}

Each item in the selector list may optionally be renamed with as:

import {keep as keep_, drop as drop_} from selectlib;

function main(x: word) returns (word) {
    return drop_(keep_(x));
}

The original name keep is not placed into scope. Only the alias keep_ is available. Multiple items may be renamed independently in the same selector list.

Constructors of an imported type must still be qualified with the type name even when the type itself was selectively imported:

import {Token} from token;

function makeActive() returns (Token) {
    return Token.Active;    // correct
}

// Error: unqualified constructor.
function makeBad() returns (Token) {
    return Active;
}

Unqualified constructor:
Active
Use Type.Constructor form.

Wildcard selective import

import {*} from modname;

Places every exported name from the module into the unqualified scope. Individual names may be excluded using hiding:

import {*} from globlib hiding {idWord};

function main(x: word) returns (word) {
    let y: T = mkT(x);    // mkT is in scope; idWord is not
    match (y) {
        case T.T(v) {
            return v;
        }
    }
}

The hiding clause accepts a comma-separated list of names to suppress:

import {keep, drop} from selectlib hiding {drop};

function main(x: word) returns (word) {
    return keep(x);    // drop is not in scope
}

Module Paths

A module path identifies the source file of a module relative to a root directory. Dots in the path correspond to directory separators.

Relative paths

A name without a lib. prefix is a relative path. The compiler resolves it relative to the directory that contains the importing file.

import foo.bar;          // loads foo/bar.sol
import foo.bar.baz;      // loads foo/bar/baz.sol

After a plain import foo.bar, the module is accessible under the full dotted qualifier:

import foo.bar;

function main() returns (word) {
    return foo.bar.value();
}

Library paths

A path that begins with lib. is treated as an absolute library path, resolved from the root of the current library rather than the current directory.

export lib.some.module;          // re-exports some/module.sol from the library root

Library paths are mainly used in re-export declarations to expose a module from a different directory tree. They are not commonly used in import statements directly.

External library paths

A path that begins with @libname. refers to a module in a separately configured external library root. External libraries are registered in the build configuration; the compiler resolves them to absolute paths at build time.

import @extlib.math.api;

contract External {
    function main() returns (word) {
        return math.api.sum(39);
    }
}

An alias keeps the reference concise:

import * as MathApi from @extlib.math.api;

function main() returns (word) {
    return MathApi.sum(39);
}

Standard library

The name std and any name that begins with std. are resolved to the standard library. The standard library root is configured separately from user libraries.

import std;

function main() returns (word) {
    return std.addWord(21, 21);
}

Qualified Names

When a module is imported with a full or aliased import, its exported definitions are accessed through a dotted qualifier. The qualifier may prefix types, functions, and constructors.

Qualified type names

import token;

function doTransfer(t: token.Token, to: word, amount: word) {
    token.transfer(t, to, amount);
}

Qualified constructor expressions

Constructors are written as qualifier.TypeName.Constructor:

import token;

function makeActive() returns (token.Token) {
    return token.Token.Active;
}

Qualified constructor patterns

The same qualified form is used in pattern matching:

import token;

function isActive(t: token.Token) returns (word) {
    match (t) {
        case token.Token.Active {
            return 1;
        }
        case token.Token.Paused {
            return 0;
        }
    }
}

Qualified names with aliases

When the import carries an alias, replace the module name with the alias in all qualified references:

import * as T from token;

function makeActive() returns (T.Token) {
    return T.Token.Active;
}

Export Declarations

An export declaration controls which definitions an importing module can see. Definitions that are not listed in an export declaration are private to the file.

Implementation extension The canonical new syntax deliberately leaves export and re-export syntax undecided. The forms in this section describe the current compiler extension and may change when the interoperability model is finalized.

Note A file without any export declaration exports nothing. All definitions are private unless explicitly exported.

Explicit export list

export { Name1, Name2, TypeName };

Names are listed by their unqualified identifier.

export { Bool, not, C, D, id };

Exporting a type with constructors

By default, exporting a type name makes the type visible but keeps its constructors private. An importer can use the type in signatures but cannot construct or pattern-match on its values.

To export constructors explicitly, list them in parentheses after the type name:

export { Token(Ok) };           // exports only the Ok constructor
export { Token(Ok, Err) };      // exports both constructors
export { Bool(*) };             // exports Bool and all its constructors

Wildcard export

export { * };

Exports everything defined in the file. Constructors of all types are also exported.

Re-exporting another module

A module may forward its imports so that importers receive them as if they came from the re-exporting module.

Re-export a whole module:

// api.sol: makes all of util's exports available under api.util.*
export lib.reexport_module.pkg.util;

An importer of api then accesses the re-exported names through the full chain:

import reexport_module.pkg.api;

function main() returns (word) {
    return api.util.unwrap(api.util.Wrap.Mk(1));
}

Re-export a module under an alias:

// api_alias.sol
export lib.reexport_module.pkg.util as Utils;

import reexport_module.pkg.api_alias;

function main() returns (word) {
    return api_alias.Utils.unwrap(api_alias.Utils.Wrap.Mk(1));
}

Re-export selected names from a module:

import hidden_ctor_lib;

export hidden_ctor_lib.{Token(Ok)};    // re-exports Token type with Ok constructor only
export hidden_ctor_lib.{mkErr};        // re-exports only the mkErr function

Hidden Constructors

When a constructor is not exported, importers receive an opaque type: they can name the type and pass values around, but they cannot construct new values directly or inspect existing ones through pattern matching. The only way to create or examine values of an opaque type is through the functions the module chooses to export.

// hidden_ctor_lib.sol
export {Token(Ok), mkOk, mkErr};

enum Token {
    Ok(word),
    Err(word)
}

function mkOk(x: word) returns (Token) { return Token.Ok(x); }
function mkErr(x: word) returns (Token) { return Token.Err(x); }

The module exports Token with only the Ok constructor visible. The Err constructor is private.

An importer that selects only the type cannot use the hidden constructor:

import {Token} from hidden_ctor_lib;

// Error: Err is not exported.
function bad() returns (Token) {
    return .Err(1);
}

No matching constructor for shorthand expression:
.Err

Pattern matching on the hidden constructor is equally rejected:

import {Token, mkErr} from hidden_ctor_lib;

// Error: Token.Err is not in scope.
function bad(x: word) returns (word) {
    match (mkErr(x)) {
        case Token.Err(v) {
            return v;
        }
        default {
            return 0;
        }
    }
}

Undefined name: Token.Err

Transitive Imports

Importing a module does not automatically make its own imports visible. If module A imports module B, and module C imports module A, then C sees only the names that A chose to export. Names that B exported to A but that A did not re-export are not visible in C.

// transitive_dep_base.sol
export { g };
function g() returns (word) { return 1; }

// transitive_dep_mid.sol
import {g} from transitive_dep_base;
export { f };
function f() returns (word) { return g(); }

// transitive_dep_main_select.sol
import {f} from transitive_dep_mid;
function main() returns (word) { return f(); }    // g is not in scope here

Name Shadowing

A locally defined function or parameter shadows an imported name of the same identifier. The imported name remains accessible through its qualified form.

import token;

// Local 'transfer' shadows token.transfer for unqualified calls.
function transfer(to: word, amount: word) { return; }

function main(to: word, amount: word) {
    token.transfer(to, amount);    // uses the imported transfer, not the local one
}

A locally defined name also shadows a selectively imported name:

import {balanceOf} from erc20lib;

// Local 'balanceOf' shadows the imported one.
function balanceOf(account: word) returns (word) { return 0; }

function main(account: word) returns (word) {
    return balanceOf(account);    // calls the local balanceOf
}

Common Errors

Using an unqualified name after a full import

A full import (import modname;) requires all names to be qualified. Using an imported name without the qualifier is an error:

import token;

// Error: 'transfer' is not in scope unqualified.
function main(to: word, amount: word) {
    transfer(to, amount);
}

Undefined name: transfer

The fix is to qualify the call: token.transfer(to, amount);.

Using the original name after aliasing

When an alias replaces the module name, the original name is not a valid qualifier:

import * as T from erc20.token;

// Error: erc20 is not a qualifier in this file.
function main(to: word, amount: word) {
    erc20.token.transfer(to, amount);
}

Undefined name: erc20

The fix is to use the alias: T.transfer(to, amount);.

Using a type without qualifying its constructor

Selectively importing a type name does not bring its constructors into the unqualified scope. Constructors must always be written as TypeName.Constructor:

import {Token} from token;

// Error: unqualified constructor.
function makeActive() returns (Token) {
    return Active;
}

Unqualified constructor:
Active
Use Type.Constructor form.

Using a type not in scope at all

Importing a module without qualification and then using a name without the module qualifier fails:

import token;

// Error: Token is not in the unqualified scope.
function bad(t: Token) returns (word) {
    return 0;
}

Undefined type constructor:
Token

Use token.Token, or switch to a selective import.

Type Inference

SAIL uses a constraint-based bidirectional type inference algorithm. The algorithm divides type information into two flows: a bottom-up flow that generates a type from an expression, and a top-down flow that pushes an expected type down into an expression. Both flows run simultaneously through unification, which merges type information from different sources into a consistent solution.

The scope of inference is deliberately limited. Top-level function signatures require complete explicit annotations. Inference operates freely inside function bodies: local variable types, intermediate expression types, and the types of arguments to generic functions are all inferred automatically without any annotation.

What Requires Annotations

Every top-level function must carry a complete type signature: every parameter must be annotated, and a value-producing function must declare its result in a returns (...) clause. Omitting that clause declares a unit-returning function. This rule applies to free functions and to functions defined inside a contract body.

// Required: every parameter is annotated; no returns clause means unit.
function transfer(to: word, amount: word) {
    let bal: word;
    assembly { bal := sload(caller()) }
    assembly { sstore(caller(), sub(bal, amount)) }
    assembly { sstore(to, add(sload(to), amount)) }
}

For a full description of the annotation requirement and the error it produces, see Functions.

What Is Inferred

Inside a function body, the compiler infers types for:

• Local variables declared with let, whether or not they carry an annotation.
• Intermediate expressions and subexpressions.
• Type arguments to polymorphic function calls.
• Type class constraints required by the body.

The inferred types are propagated through unification. Whenever the type of an expression is used in a position where another type is expected, the two are unified: the algorithm finds the most general substitution that makes them equal, or reports an error if no such substitution exists.

Local Variable Inference

A let declaration without a type annotation introduces a fresh type variable. The compiler assigns a concrete type to that variable as soon as enough information is available from the surrounding context.

Inferred from initialiser

When a let declaration includes an initialiser, the type is taken from the initialiser expression. Integer literals always have type word.

function demo() returns (word) {
    let amount = 100;     // amount : word, from the integer literal
    let flag   = true;    // flag : bool, from the boolean literal
    return amount;
}

Inferred from subsequent use

When no initialiser is present, the type is inferred from the first use of the variable.

function loadBalance(account: word) returns (word) {
    let bal: word;            // annotated; no inference needed
    assembly { bal := sload(account) }
    return bal;
}

function compute(account: word) returns (word) {
    let x;                    // no annotation, no initialiser
    x = sload(account);       // first assignment: x : word
    return x;
}

Inferred from return context

A variable whose type depends on an algebraic data type can have its type fixed by the expected return type.

enum Result {
    Ok(word),
    Err(word)
}

function demo() returns (Result) {
    let x = Result.Err(0);     // x : Result, inferred from constructor
    return x;
}

Contextual Constructor Shorthand

A constructor expression written as .Constructor (with a leading dot and no type prefix) is resolved using the expected type at the point of use. The compiler uses the context to determine which type the constructor belongs to.

In a return statement

The declared return type provides the expected type:

enum TxStatus {
    Pending,
    Confirmed,
    Reverted
}

function initialStatus() returns (TxStatus) {
    return .Pending;    // resolved as TxStatus.Pending from the return type
}

In a typed assignment

The declared type of the left-hand side provides the expected type:

enum TxStatus {
    Pending,
    Confirmed,
    Reverted
}

function demo() returns (TxStatus) {
    let s: TxStatus;
    s = .Confirmed;     // resolved as TxStatus.Confirmed from the declared type of s
    return s;
}

Error: ambiguous shorthand

If no expected type is available, the shorthand cannot be resolved and the compiler reports an error:

enum TxStatus {
    Pending,
    Confirmed,
    Reverted
}

function bad() returns (word) {
    let x = .Pending;   // no expected type available for x
    return 0;
}

Cannot resolve shorthand constructor expression without expected constructor type:
.Pending

The fix is to annotate the variable: let x: TxStatus = .Pending;.

Integer Literals

An integer literal always has type word. There is no numeric type class or overloading for integer literals in SAIL. Every integer literal that appears in source code is a 256-bit EVM word value.

function demo() returns (word) {
    let amount   = 1000;
    let decimals = 18;
    let mask     = 0xffffffffffffffffffffffffffffffffffffffff;
    return amount;     // amount, decimals, mask all have type word
}

Polymorphic Function Call Inference

When a polymorphic function is called, the compiler instantiates the type variables from the types of the supplied arguments. No explicit type application is needed.

function id<A>(x: A) returns (A) {
    return x;
}

function demo() returns (word) {
    return id(42);    // A instantiated to word at this call site
}

For a pair function with two type variables, both are instantiated independently:

enum Pair<A, B> {
    Pair(A, B)
}

function fst<A, B>(p: Pair<A, B>) returns (A) {
    match (p) {
        case Pair(x, y) {
            return x;
        }
    }
}

function demo() returns (word) {
    return fst(Pair(42, true));    // A = word, B = bool
}

Constraint Inference

When a function body calls a type class method, the compiler generates a constraint on the type variable involved. If the function is top-level and already carries an annotation, the annotation must list the constraint explicitly. If the annotation omits the constraint, the subsumption check catches the mismatch.

At a call site where the type variable is fixed to a concrete type, the compiler checks that an instance exists for that type. If no instance is found, the compiler reports an unsolved constraint error.

Constraint resolved at call site

trait Encodable<A> {
    function encode(x: A) returns (word);
}

impl Encodable<word> {
    function encode(x: word) returns (word) { return x; }
}

function encodeField<A>(x: A) returns (word) where A: Encodable {
    return Encodable.encode(x);
}

contract ERC20 {
    function main() returns (word) {
        return encodeField(42);    // a = word; word:Encodable resolved
    }
}

Error: no instance for the required type

If the concrete type at the call site has no matching instance, the compiler reports which constraint could not be satisfied and which instances are defined:

trait SafeArith<A> {
    function safeAdd(x: A, y: A) returns (A);
}

// No implementation for word is declared.
function bad(x: word, y: word) returns (word) {
    return SafeArith.safeAdd(x, y);
}

Cannot entail:
word : SafeArith
using defined instances:

The fix is either to declare impl SafeArith<word> { ... } or to add the constraint to the calling function's signature so the obligation is propagated to the caller:

function bad<A>(x: A, y: A) returns (A) where A: SafeArith {
    return SafeArith.safeAdd(x, y);
}

Phantom Type Variables

A phantom type parameter is a type parameter of a data type that does not appear in any constructor field. When a phantom constructor is used inside a function body and the phantom parameter cannot be determined from the context, the compiler reports an ambiguous type variable error.

enum TypedSlot<A> {
    TypedSlot(word)    // A is phantom: it appears in no field
}

function bad() returns (word) {
    let s = TypedSlot.TypedSlot(0);     // a is unconstrained; no context fixes it
    return 0;
}

Ambiguous type variable(s) $1 in definition of bad.
This typically occurs when a constructor has phantom type parameters.
Please, add a type signature to fix the ambiguous type variable.

The fix is to annotate the let declaration with the full type, giving the phantom parameter a concrete value:

function good() returns (word) {
    let s: TypedSlot<word> = TypedSlot.TypedSlot(0);
    return 0;
}

Unification Errors

A unification error occurs when two types that must be equal turn out to be incompatible. The compiler reports the two types and the expression that triggered the failure.

Return type mismatch

function bad(amount: word) returns (bool) {
    return amount;    // amount: word; expected bool
}

Types: bool and word do not unify
 - in: function bad(amount: word) returns (bool) { return amount; }

Match arm return type mismatch

All arms of a match statement must agree with the function's declared result. Returning different types in different arms is a unification error:

enum Result {
    Ok(word),
    Err(word)
}

function bad(r: Result) returns (word) {
    match (r) {
        case Result.Ok(v) {
            return v;
        }
        case Result.Err(_) {
            return false;    // word expected; bool returned
        }
    }
}

Types: bool and word do not unify
 - in: false
 - in: function bad(r: Result) returns (word) { ... }

Algebraic data type vs primitive mismatch

User-defined types and primitive types such as word are never interchangeable:

enum TxStatus {
    Pending,
    Confirmed
}

function bad(n: word) returns (TxStatus) {
    return n;    // word is not TxStatus
}

Types: TxStatus and word do not unify
 - in: function bad(n: word) returns (TxStatus) { return n; }

Scope of Inference

Inference is local to function bodies. Each function is checked independently, and no type information flows between sibling functions except through their declared signatures. The declared signature of a function is the only interface that callers see; the body is invisible to inference in other functions.

This means that the order of function definitions in a file does not affect the types that inference assigns to expressions inside any given function. Mutually recursive functions are type-checked as a group (see Functions), but even then each function's signature must carry complete annotations.

Core Solidity

Lambda Functions

Numeric Types

Arithmetic

Data Locations

ABI Encoding / Decoding

Contracts talk to each other and to the outside world through the contract application binary interface (ABI). Function arguments arrive as ABI-encoded calldata, return values leave as ABI-encoded memory, and both sides must agree on the same byte layout. Core Solidity implements this layout the same way Solidity does, following a "head and tail" scheme.

Unlike most languages, Core Solidity does not bake ABI encoding into the compiler. The whole mechanism lives in the standard library as a small family of type classes, so encoding follows the type of a value and extends to user-defined types through the same instance-resolution machinery described in Type Classes. The compiler contributes only the lower-level pieces that cannot be expressed in the language itself, namely compile-time keccak256 for selectors and the uniform runtime layout of sums and products (see Datatypes).

Overview

Three cooperating classes describe how a type participates in the ABI:

All three are exported from std, together with the two user-facing entry points abi_encode and abi_decode. A type is ABI-encodable exactly when it is an instance of these classes, and every primitive type shipped by the standard library already is.

Entry points

The function abi_encode serializes a value and returns it as an ordinary memory<bytes>, that is, a length-prefixed [length | data] block like any other bytes value. It reserves one word for the length, writes the encoded region right after it, and stores the region's byte length in that leading word.

function abi_encode<ty>(val: ty) returns (memory<bytes>)
    where ty: ABIAttribs, ty: ABIEncode;

Because the result carries its own length, it composes with the rest of the bytes API: the caller can query it with MemorySize.len and MemoryPointer.ptr, concatenate it, hash it, or return it, without tracking the encoded size separately.

function encodeAmount(amount: uint256) returns (memory<bytes>) {
    return abi_encode(amount);
}

The dual function abi_decode reads a value back. Because the result type cannot be inferred from the input alone, the target type and the source reader are passed as Proxy values (see Phantom Type Parameters).

function abi_decode<decodable, reader, ty, decoded>(
    value: decodable, pty: @ty, prdr: @reader
) returns (decoded)
    where decodable: HasWordReader<reader>, ABIDecoder<ty, reader>: ABIDecode<decoded>;

Most programs never call abi_decode directly. The contract dispatcher decodes incoming calldata automatically (see Contract Dispatch below), so hand-written decoding is only needed for lower-level work.

Layout metadata: ABIAttribs

Before a value can be laid out, the encoder needs to know two things about its type: whether the type is static (its size is fixed and known in advance) or dynamic (its size depends on the value), and how many bytes it occupies in the head of the encoding. The trait ABIAttribs records both.

trait ABIAttribs<self> {
    function headSize(ty: @self) returns (word);
    function isStatic(ty: @self) returns (bool);
}

Both methods take a @self rather than a value, because the answer depends only on the type. A default instance classifies every type as static with a 32-byte head, and concrete types override it as needed:

impl ABIAttribs<uint256> {
    function headSize(ty: @uint256) returns (word) { return 32; }
    function isStatic(ty: @uint256) returns (bool) { return true; }
}

Dynamic types such as bytes, string, and dynamic arrays report a 32-byte head (they occupy a single offset word there) but are not static. Aggregates combine their components: a pair adds the head sizes of its parts and is static only when both parts are static.

Head and tail layout

The standard ABI splits an encoded region into a head and a tail. Static values are written inline in the head. A dynamic value writes a 32-byte offset into the head, pointing at the position in the tail where its actual bytes live. Decoders follow that offset to recover the value. This indirection is what lets a fixed-size head describe variable-size data.

head                                   tail
┌───────────┬───────────┬───────────┐  ┌──────────────────────────┐
│ uint256   │ offset  ──┼──────────────►│ length │ data ...        │
│ (inline)  │ (dynamic) │   ...     │  └──────────────────────────┘
└───────────┴───────────┴───────────┘

The encoder threads two cursors through the whole process, one advancing over the head and one over the tail, so an arbitrarily nested value is written in a single pass. This is the standard encoding, not the packed one: every static slot is padded to a full 32-byte word. For the tight, unpadded layout used when building hash preimages, see Packed Encoding.

Encoding: ABIEncode

A type is encodable when it implements encodeInto, which writes a value into a memory region and returns the updated tail cursor.

trait ABIEncode<self> {
    // basePtr: start of the encoded region
    // offset: bytes from basePtr to the first free head slot
    // tail: index of the first free tail byte
    function encodeInto(x: self, basePtr: word, offset: word, tail: word) returns (word);
}

Static primitives write their word straight into the head slot and leave the tail untouched:

impl ABIEncode<uint256> {
    function encodeInto(x: uint256, basePtr: word, offset: word, tail: word) returns (word) {
        let repx: word = Typedef.rep(x);
        mstore(basePtr + offset, repx);
        return tail;
    }
}

Dynamic instances such as memory<bytes> and memory<string> do more: they store the relative offset into the head, copy the [length | data] block into the tail, pad it up to a multiple of 32, and return the advanced tail cursor. The standard library provides instances for uint256, address, bool, bytes4 (right-aligned), bytes32, bytes, string, dynamic arrays, tuples, the unit type, pairs, and sums.

Decoding: ABIDecode and word readers

Decoding reverses the process. It must work against two different byte sources, memory and calldata, which are read with different opcodes. Core Solidity abstracts over the two with the WordReader class.

trait WordReader<ty> {
    function read(reader: ty) returns (word);
    function advance(reader: ty, offset: word) returns (ty);
    function copyToMem(reader: ty, dst: word, cnt: word) returns (());
}

MemoryWordReader implements it with mload and mcopy, CalldataWordReader with calldataload and calldatacopy. Every decoder is written once against WordReader and therefore works uniformly on both sources.

The decoding class itself carries the decoded type in its result position:

trait ABIDecode<decoder, decoded> {
    function decode(ptr: decoder, currentHeadOffset: word) returns (decoded);
}

Decoders for value types validate the incoming word before wrapping it. Reading a bool requires the raw word to be 0 or 1, and reading an address requires the upper 96 bits to be clear. A violation reverts with a dedicated error selector, so malformed calldata is rejected rather than silently accepted. Dynamic arrays over calldata are decoded lazily: the length and each element are read on demand, which avoids copying an entire array into memory when only a few elements are used.

Aggregates: tuples, products, and sums

Tuples and constructor fields are products, and Core Solidity represents them as right-nested pairs (see Tuples). The pair instances encode the left component at the current offset and the right component at the offset advanced by the head size of the left, which reproduces the ordinary struct-of-fields ABI layout. A separate ABITuple wrapper recovers the flat-tuple grouping that pairing would otherwise hide, so a multi-argument tuple is laid out as one ABI tuple rather than a chain of nested pairs.

The primitive sum<f, g> is encoded with a leading tag word, 0 for the left injection and 1 for the right, followed by the selected branch. A static sum places the tag and branch inline in the head; a dynamic sum places a single offset word in the head and the [tag | branch] block in the tail. User-defined enums use the same surrounding layout with a variant-specific tag, as described below.

User-defined types

Structs and enums encode and decode without any hand-written instances. The mechanism reuses the generic-programming bridge:

1. The Generic<rep> class establishes an isomorphism between a user type and its sums of products representation built from the primitives sum, pair, and unit.
2. Importing std.ABIGeneric brings the marker trait ABIDeriving into scope, which signals the compiler to derive the instances.

import * from std;
import * from std.ABIGeneric;

struct Person {
    wallet: address;
    balance: uint256;
}

function encodePerson(p: Person) returns (memory<bytes>) {
    return abi_encode(p);
}

Given the import, the compiler auto-derives Generic, a concrete ABIAttribs, and a concrete ABIDecode implementation for each supported local type. A single-constructor enum or struct uses the generic ABIEncode bridge and lays out its fields in order, without a tag word.

An enum with multiple constructors also gets a concrete ABIEncode implementation. Each variant carries one bytes32 tag equal to keccak256("Name(argSigs...)"), where Name is the constructor name and its field signatures use the SigString convention. These tags replace the primitive sum's positional 0/1 tags at the ABI boundary.

Note ABIDecode needs a concrete implementation because its result-position type variable cannot be monomorphized through a default implementation. ABIAttribs also needs a concrete implementation to override the standard library's catch-all 32-byte layout. Multi-constructor enums need a concrete encoder so their variant names remain available when forming wire tags.

Function selectors

A call is routed by its four-byte selector, the first four bytes of the keccak256 hash of the canonical function signature. The signature string is built by the SigString class, which maps each type to its ABI name (uint256, address, bool, bytes, string, T[], and comma-joined products), and the Selector class turns it into the four-byte prefix.

impl<name, payability, args, rets, fn> Selector<Method<name, payability, args, rets, fn>>
    where name: SigString, args: SigString {
    function compute(prx: @Method<name, payability, args, rets, fn>) returns (bytes4) {
        let nameProxy: @name = @name;
        let argsProxy: @args = @args;
        let hash = keccakLit(sigStr(nameProxy) + "(" + sigStr(argsProxy) + ")");
        return bytes4(shr(224, hash));
    }
}

The hash is computed with keccakLit, which the compiler folds during comptime evaluation. A method's selector is therefore a constant baked into the contract, with no runtime hashing cost.

Contract dispatch

The three classes above come together in the contract entry point, which the compiler injects automatically (this pass can be turned off with --no-gen-dispatch). On each call the generated dispatcher:

1. reads the incoming selector from the first four bytes of calldata,
2. compares it against each method's compile-time selector in turn,
3. decodes the remaining calldata into the method's argument tuple with abi_decode,
4. calls the method,
5. encodes the result with abi_encode and returns it.

Because abi_encode yields a well-formed memory<bytes>, the last step is direct: the dispatcher returns the encoded region using its length prefix (MemorySize.len) and data pointer (MemoryPointer.ptr), with no need to measure the allocated memory to recover the size.

Argument decoding uses a CalldataWordReader, so calldata is read in place without first copying it to memory. Before a non-payable method runs, the dispatcher checks that the call carries no value and reverts otherwise. If the calldata is shorter than the selector plus the method's head, or if no selector matches, control falls through to the contract's fallback.

The same information also drives the Solidity-style ABI JSON that the compiler emits alongside the bytecode, so external tools see the familiar interface description.

Packed encoding

The standard head and tail encoding is what contracts use for calldata and return data. A second, tighter layout is available for building hash preimages, where every byte matters and offsets would be noise. The concat function concatenates values with no padding, and keccak256_ hashes the result:

function commitment(a: bytes32, b: address) returns (bytes32) {
    return keccak256_(concat(a, bytes32(Typedef.rep(b))));
}

This packed path is separate from ABIEncode. It is the building block used, for example, to construct the EIP-712 typed-data digests in std.eip712, where a struct hash is the keccak256 of its type hash concatenated with its encoded members.

Contracts

Hull

Hull is an intermediate language used by the Core Solidity compiler between SAIL and the Yul backend. Every SAIL program is lowered to Hull after type-checking, monomorphization, and match compilation. Hull is then translated to Yul for final code generation.

Hull retains algebraic data types (products and sums) from SAIL, but eliminates polymorphism, type classes, higher-order functions, and all surface syntax sugar. The result is a first-order, monomorphic language whose structure maps directly onto Yul constructs.

Note Hull is produced by the compiler and is not intended to be written by hand. The concrete syntax described in this document exists to make diagnostic .hull output readable. It can be inspected by passing the -dump-hull flag to the sol-core binary.

Relation to the Compilation Pipeline

The Core Solidity performs all stages up to and including Hull emission. The yule compiler takes Hull as input and produces Yul. Yul is then compiled to EVM bytecode by the standard solc compiler.

Types

All types in Hull are monomorphic. Type variables are fully instantiated by the specializer before Hull is produced.

word

word is a 256-bit unsigned integer, corresponding to the native word size of the EVM. All arithmetic values, storage addresses, and ABI-encoded data are ultimately represented as word.

bool

bool is the Boolean type. Its only values are the literals true and false.

unit

unit is the zero-size type. Its only value is (). It carries no information and occupies no storage. unit appears as the payload type of nullary constructors in sum types. For example, the None branch of Option(word) has payload type unit.

Product Types

A product type is written as:

(T1 * T2)

It holds two values simultaneously, one of type T1 and one of type T2. The * operator is right-associative, so A * B * C is parsed as A * (B * C).

The projections fst and snd extract the left and right components of a product value, respectively.

Note N-ary products are not yet implemented. Products with more than two components are encoded as right-nested pairs: (A, B, C) is represented as (A * (B * C)).

Sum Types

A sum type is written as:

(T1 + T2)

It holds a value of either type T1, tagged as the left branch, or type T2, tagged as the right branch. The + operator is right-associative, so A + B + C is parsed as A + (B + C).

Sum values are constructed using injection expressions (inl, inr, in(k)) and deconstructed using match statements.

An n-ary sum can also be written as sum(T1, T2, ..., Tn), but the binary right-nested encoding is what the Yul code generator uses internally.

Named Types

A named type is written as:

Name{T}

It attaches a human-readable label to an underlying structural type T. The name is purely documentary: the Yul backend strips it and operates on the underlying structure. Named types originate from user-defined data declarations in Core Solidity; the specializer fills in the concrete type arguments and wraps the result in a named type to preserve the original name in diagnostic output.

For example, the Core Solidity declaration:

data Option(a) = None | Some(a);

when specialized at a = word produces the Hull named type:

Option{(unit + word)}

Function Types

Function types are written as:

(T1, T2, ..., Tn -> R)

Function types appear only in function definitions; they are not first-class values. Hull has no higher-order functions and no closures.

Expressions

Integer Literals

An integer literal is a non-negative decimal integer that denotes a word value. The value must fit in 256 bits.

42
1000000

Boolean Literals

true and false are the two values of type bool.

Unit

The expression () is the single value of type unit.

Variables

A variable refers to a locally declared name. Variable names follow the same identifier rules as Yul: they may contain letters, digits, _, and $.

Note The compiler conventionally uses names beginning with $ for compiler-generated variables, such as $alt for the payload variable introduced by a match alternative. User-visible names do not begin with $.

Pairs

A tuple expression constructs a product value:

(e1, e2)

The type of (e1, e2) is (T1 * T2) where T1 and T2 are the types of e1 and e2. Tuples with more than two elements are right-nested: (e1, e2, e3) is equivalent to (e1, (e2, e3)).

Projections

fst(e) evaluates to the first component of the pair e. snd(e) evaluates to the second component.

fst(e)
snd(e)

Both e must have a product type.

Sum Injections

A sum injection constructs a sum value. The following three forms are available:

The type annotation T is the target sum type, not the type of e. This annotation is mandatory: the Yul code generator needs the full sum type to compute the correct memory representation of the injected value without re-running type inference.

For example, inr<Option{(unit + word)}>(42) injects the word 42 into the right branch of Option{(unit + word)}, representing Some(42). inl<Option{(unit + word)}>(()) injects () into the left branch, representing None.

Function Calls

A function call applies a named function to a list of arguments:

f(e1, e2, ..., en)

All call targets in Hull are statically known names produced by the specializer. There is no dynamic dispatch or virtual call mechanism.

Conditional Expressions

A conditional expression selects between two alternatives based on a boolean value:

if<T> cond then e1 else e2

cond must have type bool. Both e1 and e2 must have type T. The type annotation T is mandatory. Conditional expressions are generated by the if-desugaring pass from Core Solidity if/else expressions.

Statements

Statements are executed sequentially inside function bodies and blocks. There are no statement separators; statements are delimited by whitespace and the structure of the enclosing block.

Variable Declaration

let x : T

Declares a mutable local variable x of type T. The declaration does not initialize the variable; it must be assigned before it is read. This corresponds directly to Yul's uninitialized let declaration.

Warning Reading a variable before it has been assigned is undefined behaviour at the Yul level. The compiler always assigns variables before reading them, but hand-written Hull must respect this invariant.

Assignment

lhs := rhs

Assigns the value of rhs to lhs. The left-hand side is most commonly a variable name, written as x := e.

Expression Statement

A bare expression can be used as a statement:

e

The expression is evaluated for its side effects and the result is discarded. This form is used for calls whose return type is unit.

Return

return e

Returns the value of e from the enclosing function. Every execution path in a Hull function must end with a return or revert.

Block

{
  stmt1
  stmt2
  ...
}

A block groups a sequence of statements. Blocks are used as the bodies of match alternatives and function definitions.

Match

match<T> e with {
  inl $alt => { ... }
  inr $alt => { ... }
}

Deconstructs the sum-typed expression e of type T. Each alternative names the payload of its branch and executes the corresponding block. The following constructor patterns are available:

The type annotation <T> is mandatory. It is used by the Yul translator to determine the memory layout of the sum type.

Note Sum types with more than two constructors are represented as right-nested binary sums. Deconstructing them requires nested match expressions: the outer match separates the first constructor (left branch) from the remainder (right branch), and inner matches continue the decomposition.

Function Definition

function f(x1 : T1, x2 : T2, ...) -> R {
  stmt1
  stmt2
  ...
}

Defines a named function with explicitly typed parameters and a single return type. Hull functions are translated directly to Yul functions.

The following properties hold for all Hull functions:

• Parameters and the return type must be given explicit Hull types.
• Functions are first-order: no function-typed parameters or return values.
• Each function has exactly one return type.
• The specializer produces unique names for each monomorphic instantiation, for example map$word or maybe$Word.

Assembly Block

assembly {
  <Yul statements>
}

An inline assembly block embeds raw Yul statements directly in the Hull output. The block passes through unchanged into the generated Yul. Assembly blocks are used to access EVM primitives such as mload, mstore, add, iszero, revert, and similar opcodes.

See the Yul documentation for the complete overview of Yul syntax.

Revert

revert "message"

Immediately aborts execution. The string literal is a diagnostic label. The match compiler generates revert statements for branches that are unreachable at the Core Solidity level but must be given a code path in the Hull output.

Comment

/* text */

A block comment. Comments carry no semantics and are stripped during Yul translation. The compiler inserts comments to annotate which source-level constructor each $alt variable corresponds to, for example:

inl $alt => { /* None */
              return n
            }

Alternatives

An alternative is a branch in a match statement:

Con $var => { body }

Con is one of inl, inr, or in(k). $var is a fresh variable name that is bound to the payload of the matched constructor. body is a block of statements. The bound variable has the payload type of the matched branch: for inl and inr on a sum type (T1 + T2), the payload types are T1 and T2 respectively.

Contracts and Objects

At the top level, a Hull program consists of named objects following the Yul object model. An object has a name, a code block containing statements, and zero or more inner objects:

object "ContractName" {
  code {
    ...deployment code...
  }
  object "ContractName_deployed" {
    code {
      ...runtime code...
    }
  }
}

The outer object's code block is the deployment (constructor) code. The inner object's code block is the runtime code. This structure corresponds exactly to the Yul object notation used by solc. During Hull emission, the Core Solidity contract body is split into these two objects automatically.

Concrete Syntax Reference

The grammar diagrams below use the railroad diagram convention: rounded boxes denote terminals (keywords and punctuation literals) and rectangular boxes denote non-terminals.

Types

PrimaryType: the base forms that can appear in any type position:

Type: combines primary types with * (product) and + (sum), both right-associative:

Expressions

PrimaryExpr: literals, variables, tuples, and calls:

Expr: the complete expression grammar, including injections, projections, conditionals, and primary expressions:

Statements

Stmt: the complete statement grammar:

Block: a brace-enclosed sequence of statements:

Auxiliaries

Arg: a typed parameter in a function definition:

Con: a constructor tag in a match alternative:

Alt: a match alternative, binding the payload to a name:

Objects

Object: a named code container, optionally containing inner objects:

Examples

The following examples show Core Solidity source programs alongside the Hull they produce. All examples are accepted by the Core Solidity prototype.

Identity Function

The simplest possible Hull function passes its argument through unchanged:

function id(x : word) -> word {
    return x;
}

Hull output:

function id (x : word) -> word {
  return x
}

Optional Value

The following Core Solidity program defines an Option type and a maybe function that extracts the contained value or returns a default:

data Option(a) = None | Some(a);

function maybe(n : word, o : Option(word)) -> word {
    match o {
        | None    => return n;
        | Some(v) => return v;
    }
}

After specialization at a = word, the Hull output is:

function maybe$Word (n : word, o : Option{(unit + word)}) -> word {
  match<Option{(unit + word)}> o with {
    inl $alt => { /* None */
                  return n
                }
    inr $alt => { /* Some */
                  let var_1 : word
                  var_1 := $alt
                  return var_1
                }
  }
}

Note that the function is renamed from maybe to maybe$Word by the specializer to reflect the type instantiation. The Option{(unit + word)} named type preserves the original constructor name in the type annotation.

Enumeration Type

The following program defines a three-constructor enumeration and converts it to an integer:

data Color = Red | Green | Blue;

function fromEnum(c : Color) -> word {
    match c {
        | Red   => return 0;
        | Green => return 1;
        | Blue  => return 2;
    }
}

Hull output:

function fromEnum (c : Color{(unit + (unit + unit))}) -> word {
  match<Color{(unit + (unit + unit))}> c with {
    inl $alt => { /* Red */
                  return 0
                }
    inr $alt => match<(unit + unit)> $alt with {
                  inl $alt => { /* Green */
                                return 1
                              }
                  inr $alt => { /* Blue */
                                return 2
                              }
                }
  }
}

The three-constructor type Color is encoded as the right-nested binary sum (unit + (unit + unit)). The outer match separates Red (left) from the remaining constructors (right). An inner match then separates Green (left) from Blue (right).

EVM Arithmetic via Assembly

The following contract uses an inline assembly block to invoke the add EVM opcode:

contract Add1 {
    function main() -> word {
        let res : word;
        assembly { res := add(40, 2) }
        return res;
    }
}

Hull output:

object "Add1" {
  code {
    ...deployment code...
  }
  object "Add1_deployed" {
    code {
      function main () -> word {
        let res : word
        assembly {
          res := add(40, 2)
        }
        return res
      }
    }
  }
}

The assembly block is reproduced verbatim in the Hull output and passes through unchanged into the generated Yul.

Compilation Pipeline