The Never type is the most unusual type in FLIN's type system. It has no values. You cannot create a Never. You cannot store a Never. You cannot pass a Never to a function. Its purpose is not to describe data -- it is to describe impossibility.
And yet, this type with no values is one of the most important types in the entire system. It is the mechanism by which the compiler proves that your code handles every case. It is the type-theoretic foundation of exhaustiveness checking.
What Never Means
In type theory, the Never type (also called the bottom type, or "!" in Rust, or "never" in TypeScript) is the type of computations that do not produce a value. A function that always throws an error returns Never. A match arm that the compiler proves is unreachable has type Never. A variable that has been narrowed to nothing -- because every possibility has been handled -- has type Never.
flin// A function that never returns
fn panic(message: text) -> never {
log_error(message)
abort()
}
// A match arm that is unreachable
match direction {
North -> "north"
South -> "south"
East -> "east"
West -> "west"
// No _ needed -- all variants covered
// Any additional arm would have type never (unreachable)
}Never in the Type System
Never is represented as a variant in the FlinType enum:
rustpub enum FlinType {
Int,
Number,
Text,
Bool,
// ...
Never, // The bottom type
Any, // The top type
}Never and Any are duals. Any is the supertype of everything -- every type is assignable to Any. Never is the subtype of everything -- Never is assignable to every type.
This subtype relationship has a practical consequence: a function returning Never can be used anywhere. If panic() returns Never, then panic() is a valid int, a valid text, a valid User. Because panic() never actually produces a value, it is vacuously compatible with every type.
rustfn types_compatible(&self, expected: &FlinType, actual: &FlinType) -> bool {
match (expected, actual) {
// Never is compatible with everything (subtype of all types)
(_, FlinType::Never) => true,
// Any accepts everything (supertype of all types)
(FlinType::Any, _) => true,
// ...
}
}The first rule -- Never is compatible with everything -- means you can write:
flinfn get_value(id: int) -> int {
user = User.find(id)
if user {
return user.score
}
panic("User not found") // returns never, but int is expected -- OK
}The panic() call returns Never, which is assignable to int. The compiler accepts this because it knows the function will never actually return at that point.
Exhaustiveness Checking
Exhaustiveness checking is the compiler's guarantee that every possible case in a match expression or if-else chain is handled. It works by progressively narrowing the type of the matched value until nothing remains -- until the type reaches Never.
On Enums
The simplest form of exhaustiveness checking is on enums:
flinenum Color { Red, Green, Blue }
match color {
Red -> "#FF0000"
Green -> "#00FF00"
// ERROR: non-exhaustive -- missing Blue
}The algorithm:
rustfn check_enum_exhaustiveness(
&self,
enum_type: &FlinType,
arms: &[MatchArm],
span: Span,
) {
let FlinType::Enum { variants, .. } = enum_type else { return };
let variant_names: HashSet<String> = variants.iter()
.map(|(name, _)| name.clone())
.collect();
let mut covered: HashSet<String> = HashSet::new();
let mut has_wildcard = false;
for arm in arms {
match &arm.pattern {
Pattern::EnumVariant { variant, .. } => {
covered.insert(variant.clone());
}
Pattern::Wildcard | Pattern::Identifier { .. } => {
has_wildcard = true;
}
Pattern::Or(patterns) => {
for p in patterns {
if let Pattern::EnumVariant { variant, .. } = p {
covered.insert(variant.clone());
}
}
}
_ => {}
}
}
if !has_wildcard {
let uncovered: Vec<&String> = variant_names.difference(&covered).collect();
if !uncovered.is_empty() {
self.report_error(&format!(
"non-exhaustive match on {}: missing variant(s): {}",
enum_type.display_name(),
uncovered.iter().map(|s| s.as_str()).collect::<Vec<_>>().join(", ")
));
}
}
}Start with the set of all variants. For each arm, mark the variant as covered. If any variants remain uncovered and there is no wildcard, report an error.
On Booleans
Booleans have exactly two values, so exhaustiveness is straightforward:
flinmatch flag {
true -> "yes"
false -> "no"
}Both values are covered. No wildcard needed. The compiler verifies:
rustfn check_bool_exhaustiveness(&self, arms: &[MatchArm], span: Span) {
let has_true = arms.iter().any(|a| matches_literal_bool(&a.pattern, true));
let has_false = arms.iter().any(|a| matches_literal_bool(&a.pattern, false));
let has_wildcard = arms.iter().any(|a| is_wildcard(&a.pattern));
if !has_wildcard && (!has_true || !has_false) {
let missing = if !has_true && !has_false {
"true, false"
} else if !has_true {
"true"
} else {
"false"
};
self.report_error(&format!("non-exhaustive match on bool: missing {}", missing));
}
}On Union Types
Union type exhaustiveness works by tracking which members have been handled:
flinvalue: int | text | bool = getData()
match value {
is int -> handle_int(value)
is text -> handle_text(value)
is bool -> handle_bool(value)
}Each is arm covers one member of the union. After all three, the union is fully covered. If an arm is missing:
flinmatch value {
is int -> handle_int(value)
is text -> handle_text(value)
// ERROR: non-exhaustive -- bool is not covered
}The type subtraction mechanism from the type guard article drives this. After is int and is text, the remaining type is bool. If no arm handles bool and there is no wildcard, the match is non-exhaustive.
On Infinite Types
Integers, strings, and floating-point numbers have infinite possible values. Exhaustiveness checking cannot enumerate all of them. For these types, a wildcard arm is required:
flinmatch count {
0 -> "none"
1 -> "one"
_ -> "many" // required for int
}Without the _ arm, the compiler rejects the match:
error[E0015]: non-exhaustive match
--> app.flin:5:1
|
5 | match count {
| ^^^^^ patterns 0, 1 do not cover all possible int values
|
= hint: add a wildcard arm: _ -> ...The Never Type in Practice
Unreachable Code Detection
When type narrowing reduces a variable to Never, any code using that variable is unreachable:
flinvalue: int | text = getData()
if value is int {
// value: int
} else if value is text {
// value: text
} else {
// value: never -- this branch is unreachable
// The compiler may warn about dead code
}After handling int and text, the union is exhausted. The else branch has type Never, meaning no value can reach it. The compiler can flag this as dead code.
Function Return Type
Functions that unconditionally throw, exit, or loop forever return Never:
flinfn unreachable(message: text) -> never {
log("UNREACHABLE: " + message)
abort()
}
fn todo(feature: text) -> never {
panic("TODO: " + feature + " not implemented")
}These functions are useful as placeholders and error handlers. Because Never is a subtype of everything, they can be used in any expression position:
flinfn process(value: int | text) -> text {
match value {
is int -> text(value)
is text -> value
_ -> unreachable("all types covered")
}
}The wildcard arm calls unreachable(), which returns Never. Since Never is assignable to text (the function's return type), the compiler accepts it.
Exhaustive Match as Expression
When a match expression is exhaustive, the compiler knows that one arm will always execute. This means the match always produces a value:
flinenum Direction { North, South, East, West }
// This match always produces a text value
description = match direction {
North -> "heading north"
South -> "heading south"
East -> "heading east"
West -> "heading west"
}
// description: text (guaranteed)Without exhaustiveness, the match might not execute any arm, and description would be uninitialized. Exhaustiveness checking guarantees initialization.
The Never Type in the VM
At the VM level, Never does not exist as a runtime value. There is no Value::Never variant. The Never type is purely a compile-time concept -- it exists only in the type checker.
This is by design. A value of type Never can never be created, so the VM never needs to represent one. Any code path that the type checker determines leads to a Never value is guaranteed to be unreachable at runtime (via a call to panic, an infinite loop, etc.).
rustpub enum Value {
Int(i64),
Number(f64),
Text(String),
Bool(bool),
None,
Object(Box<Object>),
List(Vec<Value>),
// No Never variant -- it never exists at runtime
}Error Messages
Exhaustiveness errors are some of the most user-friendly in FLIN's compiler:
error[E0015]: non-exhaustive match
--> app.flin:10:1
|
10 | match shape {
| ^^^^^ missing variant(s): Triangle
|
= note: Shape has variants: Circle, Square, Triangle, Rectangle
= note: arms cover: Circle, Square, Rectangle
= hint: add a match arm: Triangle -> { ... }
= hint: or add a wildcard: _ -> { ... }The error lists what is missing, what is covered, and suggests two fixes: either handle the specific missing variant or add a wildcard. Both are valid solutions, and the developer chooses based on their intent.
Design Decisions
Exhaustiveness is required, not optional. Some languages make exhaustiveness checking a warning. FLIN makes it an error. This is a deliberate choice for safety. If you match on an enum, you must handle every variant. Period. If you add a variant to an enum, every match must be updated.
Wildcards opt out of exhaustiveness for specific arms, not globally. A wildcard _ covers all remaining cases. It is explicit -- the developer is saying "I am aware there are other cases, and I am choosing to handle them uniformly." This is different from ignoring the other cases.
No fallthrough. Unlike C's switch, FLIN's match arms do not fall through. Each arm is independent. This eliminates an entire class of bugs where a missing break causes unintended execution of the next case.
Guard clauses do not count for exhaustiveness. An arm with a guard (x if x > 0) might not match even if the pattern matches. The compiler cannot determine at compile time whether the guard will be true, so guarded arms are treated as potentially non-matching for exhaustiveness purposes.
flinmatch count {
x if x > 0 -> "positive"
x if x < 0 -> "negative"
// Still need: _ -> "zero" or 0 -> "zero"
// Guards might both be false for count = 0
}The Theoretical Foundation
Never and exhaustiveness are deeply connected through the Curry-Howard correspondence -- the observation that types correspond to propositions and programs correspond to proofs. In this view:
- A match expression is a proof that every case is handled
- An exhaustive match is a complete proof
- A non-exhaustive match is an incomplete proof
Neveris the proposition "this cannot happen," and a value of typeNeverwould be a proof of the impossible
FLIN developers do not need to know any of this. But the theory explains why these features exist and why they interact the way they do. Exhaustiveness checking is not an arbitrary compiler rule -- it is a logical consequence of the type system's design. The compiler is not being pedantic. It is being correct.
This is Part 41 of the "How We Built FLIN" series, documenting how a CEO in Abidjan and an AI CTO designed and implemented a programming language from scratch.
Series Navigation: - [39] Tuples, Enums, and Structs - [40] Type Guards and Runtime Type Narrowing - [41] The Never Type and Exhaustiveness Checking (you are here) - [42] Generic Bounds and Where Clauses - [43] While-Let Loops and Break With Value