Summary

This PR adds exhaustiveness checking and unreachable arm detection for match expressions in BAML's type system. The implementation uses a value-based model (ValueSet) inspired by the treatment of pattern matching in TAPL.

Key capabilities:

• Detect non-exhaustive matches (missing cases) with helpful error messages listing uncovered patterns
• Detect unreachable arms (arms that can never match because previous arms already cover them)
• Handle type aliases by expanding them to their underlying types
• Treat enums as finite types, expanding them to their individual variants
• Support literal patterns (integers, strings, booleans) and union patterns (200 | 201)

Key Design Decisions

1. Value-Based Model (ValueSet)

The core insight is that pattern matching operates on values, not types. A pattern like Status.Active matches one specific value, while s: Status matches all values of type Status.

The ValueSet enum captures this:

pub enum ValueSet {
    All,                                    // Catch-all: `_` or `other`
    OfType(Name),                           // Type pattern: `s: Status`
    EnumVariant { enum_name, variant_name }, // Specific variant: `Status.Active`
    Literal(Literal),                       // Literal value: `42`, `"hello"`
    Union(Vec<ValueSet>),                   // Union pattern: `200 | 201`
    Empty,                                  // Guarded pattern (doesn't contribute)
}

This separation allows clean reasoning about what values each arm covers.

2. Guards Do NOT Contribute to Exhaustiveness

Per BEP-002, guarded patterns are treated as Empty value sets. A pattern like x: int if x > 0 might not match negative numbers, so it can't guarantee coverage.

match (n) {
  x: int if x > 0 => "positive"
  // Still need a catch-all because guard doesn't cover all ints
}

3. Type Alias Expansion

Type aliases are expanded during exhaustiveness checking. For type Result = Success | Failure, matching on r: Result requires covering both Success and Failure.

4. Finite vs. Infinite Types

• Finite types (enums, booleans): Expanded into individual values for precise tracking
• Infinite types (int, string, classes): Represented as abstract OfType sets, only exhaustive via catch-all

5. Singleton Types for Literal Unions

Added singleton types (Ty::Singleton(SingletonValue)) to support exhaustiveness checking of literal unions like 200 | 201 | 204. This follows the type-theoretic notion of singleton types—types inhabited by exactly one value.

Files Changed

Algorithm Overview

The exhaustiveness checker maintains a list of covered ValueSets as it processes arms:

1. Expand scrutinee type into required value sets

   • Enums → individual variants
   • Optionals → inner type + null
   • Type aliases → expanded recursively

2. For each arm, convert pattern to ValueSet:

   • Check if arm is unreachable (already fully covered by previous arms)
   • Add to coverage list (unless guarded)

3. After all arms, find uncovered value sets:

   • Report as TypeError::NonExhaustiveMatch with helpful error message

Test Coverage

The implementation includes unit tests for:

• ValueSet display formatting
• Coverage logic (type patterns, enum variants, literals)
• Type alias expansion (union members covered separately)
• Enum exhaustiveness (type pattern expands to all variants)
• Literal-to-type coverage (42 is covered by int pattern)
• Catch-all coverage (covers everything)

Known Limitations / Future Work

Error Span Improvements

Currently, unreachable arm errors point to the entire match expression rather than the specific unreachable arm. This requires tracking arm spans in HIR.

// TODO(exhaustiveness): Improve error spans to point to the specific unreachable
// arm rather than the entire match expression. Requires tracking arm spans in HIR.

Uninhabited Types (Zero-Variant Enums)

Empty matches on uninhabited types should be allowed (there are no cases to handle). Currently only empty unions are detected; zero-variant enums require database access.

// TODO(exhaustiveness): Check for zero-variant enums. This requires database
// access to look up enum definitions. Currently only empty unions are detected.

Cyclic Type Alias Detection

Recursive type aliases like type A = A | B could cause infinite recursion during expansion. A cycle detection mechanism should be added.

// TODO(exhaustiveness): Add cycle detection for recursive type aliases like
// `type A = A | B`. Currently this would cause infinite recursion.

Example Usage

enum Status { Active, Inactive, Pending }

function ProcessStatus(s: Status) -> string {
  match (s) {
    Status.Active => "active"
    Status.Inactive => "inactive"
    // Error: Non-exhaustive match, missing: Status.Pending
  }
}

function WithCatchAll(s: Status) -> string {
  match (s) {
    Status.Active => "active"
    _ => "other"  // OK: catch-all covers remaining cases
  }
}

type Result = Success | Failure

function HandleResult(r: Result) -> string {
  match (r) {
    s: Success => "ok"
    f: Failure => "error"
    // OK: both union members covered
  }
}