# KEEP: Covered Sealed Subtyping (allow sealed intermediates across modules that preserve exhaustiveness)

**Type:** Design proposal  
**Status:** Draft  
**Discussion:** _TBD (GitHub issue # to be created)_  
**Authors:** Jordan Terrell (@jordan.terrell)  
**Kotlin Version:** _TBD (language version flag suggested)_  
**Targets:** Kotlin/JVM (primary), Kotlin/JS, Kotlin/Native (no platform-specific behavior intended)

---

## Summary

This proposal relaxes Kotlin’s current restriction that _all_ direct subtypes of a `sealed` class or interface must be declared in the same package and module as the sealed type. It introduces **covered sealed subtyping**:

> A `sealed` type **S** may be extended in other modules by a **sealed** intermediate subtype **I**, **provided that every concrete leaf of I is also a subtype of exactly one of S’s declared sealed variants**. When this “coverage” condition holds, `when`-exhaustiveness for **S** remains unchanged (still determined solely by **S**’s declared variants).

This enables domain-specific sealed families layered on top of shared algebraic data types (ADTs) without breaking exhaustiveness guarantees.

---

## Motivation

### The pain today

* **Sealed hierarchies cannot be layered across modules.** Kotlin enforces that direct inheritors of a `sealed` type be in the same package and module. This prevents downstream libraries from creating intermediate sealed families that _refine_ a common ADT while preserving the ADT’s exhaustive pattern-matching semantics.
* **Loss of expressiveness and ergonomics.** Consider a shared ADT and a downstream domain that wants domain-specific, sealed alternatives with extra fields and constraints. Today, you must either:
    * Collapse everything into one module, or
    * Avoid inheritance from the base sealed type and instead write adapters/projections—boilerplate-y and less type-directed.
* **Unnecessary limitation for sound patterns.** If an intermediate family’s **leaves** are all already subtypes of _one of the base sealed variants_, then a `when` over the **base** type remains exhaustive using **only those variants**. Disallowing such layering is conservative beyond what type soundness demands.

### Contrived → real example

A simple ADT:

```kotlin
// moduleA / packageA
sealed interface Contract<A, B> {
    interface First<A> : Contract<A, Nothing>
    interface Second<B> : Contract<Nothing, B>
}
```

A downstream domain wants a refined family without introducing _new_ base variants:

```kotlin
// moduleB / packageB
import packageA.Contract

sealed class ClassFamily<A, B> : Contract<A, B> {
    class OneFirst<A> : ClassFamily<A, Nothing>(), Contract.First<A>
    class TwoFirst<A> : ClassFamily<A, Nothing>(), Contract.First<A>
    class OneSecond<B> : ClassFamily<Nothing, B>(), Contract.Second<B>
    class TwoSecond<B> : ClassFamily<Nothing, B>(), Contract.Second<B>
}
```

The base `Contract` is not semantically expanded: **every concrete leaf of ClassFamily is a First or Second**. A `when` on `Contract` remains exhaustive with only `First`/`Second`. Yet today this is rejected solely because `ClassFamily` extends `Contract` across modules.

A more realistic, domain-flavored variant:

```kotlin
// moduleA / packageA
sealed interface Possible<out T, out E> {
    interface Success<out T> : Possible<T, Nothing> { val value: T }
    interface Error<out E>   : Possible<Nothing, E> { val error: E }
}

fun <T, R, E> Possible<T, E>.map(f: (T) -> R): Possible<R, E> =
    when (this) {
        is Possible.Success -> object : Possible.Success<R> { override val value = f(this@map.value) }
        is Possible.Error   -> this
    }
```

```kotlin
// moduleB / packageB
import packageA.Possible

sealed class DomainResult<out T, out E> : Possible<T, E> {
    data class Happy<T>(
        override val value: T,
        val extra: Int
    ) : DomainResult<T, Nothing>(), Possible.Success<T>

    data class Sad<E>(
        override val error: E,
        val message: String
    ) : DomainResult<Nothing, E>(), Possible.Error<E>
}
```

A `when` on `Possible<_, _>` is still exhaustive with `Success`/`Error`.

---

## Proposed solution

### Core idea

Allow cross-module `sealed` inheritance **only** for _sealed intermediates_ whose **leaves are fully covered** by the base sealed type’s declared variants.

**Definition (Coverage):** Let `S` be a sealed type with declared variants `V = {V1, …, Vn}` (the direct subtypes declared in `S`’s module). A sealed subtype `I : S` declared outside S’s module is **covered** iff **every** non-abstract, instantiable descendant `L` of `I` (a leaf in `I`’s sealed hierarchy):

* Is a subtype of **exactly one** `Vi ∈ V` (syntactically: its supertype chain includes `Vi`), and
* There exists no path by which `L` is a subtype of two or more distinct `Vi, Vj` (to avoid ambiguity in exhaustiveness).

When `I` is covered, it **does not contribute** new cases to `S`’s exhaustiveness set. A `when` on a value typed as `S` remains exhaustive using only `V`.

### Syntax

No new syntax is required. The rule is a **semantic relaxation** of where `sealed` may be extended.

### Semantics (informal)

* **Sealed-intermediate allowance:** A type `I` declared in a different module/package may inherit from sealed base `S` iff:
    * `I` is itself `sealed` and
    * `I` passes **coverage** (as above).
* **Leaf obligations:** For any leaf `L` under `I`, the compiler enforces that `L` is a subtype of exactly one `Vi`. If `L` fails this, compilation of **L’s module** fails with an error identifying the uncovered or multiply-covered leaf.
* **Exhaustiveness:** When matching on `S`, only `V` (the base’s declared variants) determine exhaustiveness. Cross-module sealed intermediates never add new cases to `S`’s exhaustive set.
* **Final/frozen variants:** If all `Vi` are non-extendable (e.g., final classes), downstream leaves cannot subtype them; the coverage condition cannot be satisfied; the attempt to define `I : S` fails. This preserves the base author’s intent.

### Illustrative example

```kotlin
// Base module
sealed interface Expr {
    interface Lit : Expr { val value: Int }
    interface Add : Expr { val left: Expr; val right: Expr }
}

// Downstream module
sealed interface RichExpr : Expr {
    // Leaves must also subtype exactly one variant:
    data class Number(override val value: Int) :
        RichExpr, Expr.Lit

    data class Plus(
        override val left: Expr,
        override val right: Expr,
        val srcSpan: IntRange
    ) : RichExpr, Expr.Add
}

// Exhaustive with only the base variants:
fun eval(e: Expr): Int = when (e) {
    is Expr.Lit -> e.value
    is Expr.Add -> eval(e.left) + eval(e.right)
}
```

---

## Alternative approaches

* **Status quo (forbid cross-module inheritance).** Simple and predictable, but blocks ergonomic layering and forces adapters.
* **Use adapters/projections (asBase() / asDomain()).** Works but duplicates boilerplate and loses type-directed navigation; exhaustiveness is then on the _domain_ type, not the base ADT.
* **Make the base module own every extension.** Centralizes code but harms modularity and ownership boundaries.
* **Permit cross-module direct subclasses freely.** Violates sealed exhaustiveness guarantees; unsound.
* **Annotation-driven whitelist of permitted external subtypes.** Requires base module to know downstreams a priori (not viable for libraries).

The proposed **coverage** rule is an approach that preserves exhaustiveness while restoring modular layering.

---

## Detailed design

### 1. Rules of inheritance

* **Allowed:** `sealed` `I` declared in a different module/package may directly inherit from sealed base `S` **iff** coverage holds.
* **Still disallowed:** Any **non-sealed** direct subclass of `S` outside S’s module; any direct **concrete** subclass of `S` outside S’s module.
* **Interfaces vs classes:** The rule applies uniformly to `sealed interface` and `sealed class`. For interfaces, “leaf” means an instantiable concrete class; an interface leaf is not instantiable and is not considered a leaf for coverage—coverage must be proven at concrete class level.

### 2. Coverage checking

At **compile time of the module that declares I (and its leaves)**:

* Build the sealed-subtree for `I`. Identify all **concrete leaves** `L`.
* For each `L`, check its supertype chain for membership in the base variants `V = {V1, …, Vn}`.
* Emit diagnostics:
    * **Uncovered leaf:** “Concrete subtype `L` of sealed intermediate `I : S` does not implement any variant of base sealed type `S` (`{V}` expected).”
    * **Ambiguous coverage:** “Concrete subtype `L` implements multiple base variants `{Vi, Vj}`; exactly one required.”
* For **generic** bases: use standard Kotlin subtype rules with variance; “implements variant” holds if a valid supertype instance exists (e.g., `L : V<…>` with arguments well-formed under variance).
* **Transitive intermediates:** If `I1 : S` (external) and `I2 : I1` (also external, sealed), coverage is checked on **I2**’s leaves; `I1` is considered covered iff all transitive leaves are covered. (Effectively, coverage is a property of the entire sealed subtree.)

### 3. Exhaustiveness algorithm

Current Kotlin exhaustiveness for `when` over `S` enumerates S’s **declared** direct variants. This proposal **does not change** that set nor require the compiler to discover external subclasses. Instead:

* Treat any external sealed intermediates as **transparent** for the purpose of `S`-exhaustiveness; they do not introduce new cases because their leaves are already subtypes of existing variants.
* If coverage fails anywhere, that downstream code does not compile; thus, compiled code that reaches consumers upholds exhaustiveness.

Implication: `when (x: S)` remains exhaustive with branches `{V1, …, Vn}` only.

### 4. Bytecode & metadata

* **No runtime enforcement needed.** Kotlin sealed checks are compile-time. This proposal maintains that.
* **Metadata:** No new metadata is strictly required for exhaustiveness (which still uses `S`’s declared variants). For better tooling, the compiler **may** emit a marker in the intermediate’s metadata indicating it is a **covered sealed subtype** of `S` (e.g., a flag or “covered-base” entry), but this is optional.
* **Interoperability with Java sealed types:** Out of scope; follow existing Kotlin rules. This proposal neither expands nor reduces interop beyond the current capabilities.

### 5. Error-prone cases & restrictions

* **Double-coverage** (leaf implements two variants): **forbidden.**
* **No-coverage** (leaf implements none): **forbidden.**
* **Final variants:** If a base variant is a final class (non-extendable), downstream leaves cannot subtype it; the intermediate cannot be covered; compilation fails where the intermediate is declared.
* **Visibility:** Private/internal base variants behave as today. If a variant is not visible to downstream code, it cannot be implemented; the intermediate will fail coverage unless all required leaves target visible variants. This keeps base authors’ encapsulation intact.
* **Type aliases:** Coverage analysis operates on expanded types.
* **Multiple platforms:** The rule is platform-agnostic.

### 6. Generics and variance

Coverage uses Kotlin’s normal subtype relation with variance. Examples:

```kotlin
sealed interface Box<out T> {
    interface Full<out T> : Box<T>
    interface Empty : Box<Nothing>
}

// downstream
sealed class FancyBox<out T> : Box<T> {
    data class Some<T>(val t: T) : FancyBox<T>(), Box.Full<T>     // OK
    data object None              : FancyBox<Nothing>(), Box.Empty // OK
}
```

The compiler validates that `Some<T>` is a subtype of `Box.Full<T>` (which is a declared variant) and `None` is a subtype of `Box.Empty`. Mixed-variance pitfalls are handled by the existing type checker; coverage is rejected if the subtype relation doesn’t hold.

---

## Impact on existing code

* **Backwards-compatible.** Existing code continues to compile and behave the same. This is a **relaxation** of a restriction.
* **No migration required.** Libraries may opt into the pattern; consumers see no change in pattern-matching behavior.
* **Tooling:** IDEs and linters could gain new inspections/quick-fixes (e.g., “Make intermediate sealed” / “Implement base variant XYZ”).
* **Binary compatibility:** No change to the base sealed type’s ABI. External modules that adopt covered intermediates compile to normal class files; no new runtime assumptions are introduced.

---

## Reference implementation

**Feasibility notes:**

* **Checker:** Extend `SealedInheritorInSameModuleChecker` (frontend) to:
    * Allow external inheritors if they are `sealed` and
    * Trigger a **SealedCoverageChecker** that computes leaves and validates coverage against the base’s declared variants.
* **Exhaustiveness:** `WhenChecker` logic remains unchanged for base `S` (still enumerates `S`’s declared variants). No need to enumerate external subtypes.
* **Diagnostics & PSI/IR:** Coverage computation can be performed on FIR with module scope to discover the sealed subtree for the intermediate `I`. Leaves are the instantiable classes with no sealed children in the same module.
* **Prototype plan:**
    * Phase 1: FIR-only proof-of-concept for JVM, guarded by a language feature flag (e.g., `LanguageFeature.CoveredSealedSubtypes`).
    * Phase 2: IDE quick-fixes and enhanced diagnostics.
    * Phase 3: JS/Native parity (expected minimal changes).

---

## Unresolved questions

* **Should ambiguous coverage (leaf implements two variants) be forbidden or allowed if disambiguated by specificity?** Proposal: **forbid** for simplicity and clarity of `when` exhaustiveness.
* **Do we need an opt-in language flag initially?** Proposal: Yes—ship behind a language version flag for early adopters.
* **Should the compiler warn if an intermediate currently has no leaves (coverage vacuously true)?** Proposal: No warning; acceptable during incremental development.
* **Should we expose a public compiler API hook for tools to query coverage?** Nice-to-have for analyzers, but not required.

---

## Appendix: Additional examples

### 1) Domain layering over an Either-like ADT

```kotlin
// Base module
sealed interface Possible<out T, out E> {
    interface Success<out T> : Possible<T, Nothing> { val value: T }
    interface Error<out E>   : Possible<Nothing, E> { val error: E }
}

// Downstream module
sealed class DomainResult<out T, out E> : Possible<T, E> {
    data class Happy<T>(
        override val value: T,
        val extra: Int
    ) : DomainResult<T, Nothing>(), Possible.Success<T>

    data class Sad<E>(
        override val error: E,
        val message: String
    ) : DomainResult<Nothing, E>(), Possible.Error<E>
}

// Exhaustiveness over the base remains unchanged:
fun <T, E> handle(p: Possible<T, E>) = when (p) {
    is Possible.Success -> println("Yay: ${p.value}")
    is Possible.Error   -> println("Uh oh: ${p.error}")
}
```

### 2) Disallowed: uncovered leaf

```kotlin
// Downstream
sealed class Bad : Possible<Int, String> {
    // ERROR: Not a subtype of Success<Int> or Error<String>
    data class Unknown(val code: Int) : Bad()
}
```

### 3) Disallowed: ambiguous leaf

```kotlin
// Hypothetical where a leaf accidentally implements two variants:
data class Confused<T, E>(
    override val value: T,
    override val error: E
) : DomainResult<T, E>(), Possible.Success<T>, Possible.Error<E> // ERROR
```

---

## Conclusion

**Covered sealed subtyping** restores a valuable form of modularity to Kotlin’s sealed hierarchies without weakening exhaustiveness guarantees. By allowing _sealed_ intermediates across modules **only when all leaves are already subtypes of the base’s declared variants**, the language gains a powerful pattern for layering domain models over shared ADTs—cleanly, soundly, and without runtime impact.