[tehnub]

Could you elaborate on that? It sounds like I may have an overly simplified understanding of the topic here—wouldn't be the first time.

[native_samples]

Static type systems don't imply fully dependent types. In Kotlin:

    sealed class Program
    class HaltingProgram : Program()
    class InfiniteProgram : Program()

    fun checkIsHalting(p: ByteArray) = if (halts(p)) HaltingProgram() else InfiniteProgram()

This program will type check just fine. The inferred return type will be Program because that's the nearest shared ancestor type of both possible return types. Good luck implementing the halts() function of course, but that's not the type system's problem.