Ruta graveolens  ·  notes from a language experiment  ·  cultivated since 2025

Never Type

The never type, written !, is the type of an expression that transfers control away from its context rather than producing a value — a diverging expression (docs/formal/01-core-calculus.md §5.7).

Expressions of type ! include:

  • return expressions
  • break expressions
  • continue expressions
  • Infinite loops

Type Coercion

A type coercion is an implicit type conversion applied during type checking. Rue has exactly one coercion: the never type coerces to any type. The core states this as subsumption on the bottom type — the (Sub-Never) rule of docs/formal/01-core-calculus.md §5.7 — while every other typing rule demands exact type identity.

When type checking requires a value of type T, an expression of type ! is accepted at T. The conversion is vacuously sound: ! has no values (3.4:9), so re-typing a diverging expression at T converts no run-time value and creates no ownership obligation (docs/formal/01-core-calculus.md §5.7). This lets diverging expressions appear in any context where a value is expected.

fn test(x: i32) -> i32 {
    // `return 100` has type !, which coerces to i32
    let y = if x > 5 { return 100 } else { x };
    y * 2
}

fn main() -> i32 {
    test(3) + test(10)  // 6 + 100 = 106
}

When both branches of an if expression or all arms of a match expression have type !, the entire expression has type !.

fn diverges(x: i32) -> i32 {
    // Both branches return, so the if has type !
    // This coerces to i32 (the function's return type)
    if x > 0 { return 1 } else { return 0 }
}

fn main() -> i32 { diverges(5) }

! propagates through any composite expression that control cannot fall out of, not only if and match. A block expression has type ! when control cannot reach its end: either its tail expression has type !, or a statement within it diverges — for example an expression statement whose expression has type ! — which makes the remainder of the block, and thus the block's end, unreachable. A loop expression with no reachable break likewise has type ! (3.4:2). By the coercion of 3.4:3, such an expression may appear wherever a value of any type is expected.

fn test(x: i32) -> i32 {
    // The block's tail expression is `return`, so the block has type !,
    // which coerces to the i32 the `let` expects.
    let y = { return 100 };
    y * 2
}

fn main() -> i32 { test(3) }  // exit code 100

Diverging Functions

A function with return type ! never returns normally.

Memory Representation

The never type is a zero-sized type. See Zero-Sized Types for the general definition.