feat(types): add Never bottom type for narrowing exhaustiveness

Narrowing wants a way to say 'this case is unreachable.' Concrete
example: a switch over a closed string-enum that handles every
literal. After the last case, the residual type of the discriminant
is the empty set - no value remains. Code at that point is provably
unreachable, but it still needs to type-check (the user may write
something there that we don't want to flag spuriously).


Never is that empty type. It's the bottom of the lattice: no value
inhabits it at runtime, so it's vacuously a subtype of everything.
That property is what makes exhaustiveness composable - the residual
type from peeling cases lands in Never naturally, and post-switch
code typed against Never can flow into any subsequent slot.


Two assignability rules earn their keep:


  - Never accepts only Never. A real value assigned into a slot
    typed Never means narrowing was unsound - we thought the branch
    was unreachable, but the user reached it.


  - Everything else accepts Never. Vacuously, because the source
    can never produce a value, so the target's constraints don't
    matter. Implemented via the same flows-into-anything fast path
    used for any and dynamic.


Void is the exception: it accepts Never (vacuously) but still
rejects any and dynamic, since the gradual-typing rule that lets
typed slots silently accept any values would also let
'x = print(...)' slip through. Never doesn't break that guarantee
because there are no Never values to slip.


Users never write 'never' themselves; it appears only in inferred
types and error messages.

Author: amterp

rts/rl/consts.go

@@ -212,6 +212,7 @@ const (
 	T_ERROR      = "error"
 	T_ANY        = "any"
 	T_DYNAMIC    = "dynamic"
+	T_NEVER      = "never"
 	T_VOID       = "void"
 	T_LIST       = "list"
 	T_MAP        = "map"

rts/rl/typing.go

@@ -80,6 +80,7 @@ var (
 	_ TypingT = (*TypingErrorT)(nil)
 	_ TypingT = (*TypingAnyT)(nil)
 	_ TypingT = (*TypingDynamicT)(nil)
+	_ TypingT = (*TypingNeverT)(nil)
 	_ TypingT = (*TypingVoidT)(nil)
 	_ TypingT = (*TypingAnyListT)(nil)
 	_ TypingT = (*TypingListT)(nil)
@@ -232,6 +233,35 @@ func (t *TypingDynamicT) IsCompatibleWith(TypingCompatVal) bool {
 	return true
 }
 
+// TypingNeverT is the bottom type. No value inhabits it at runtime; the
+// static checker synthesizes it when narrowing has eliminated every variant
+// of a type (e.g. a switch over a string-enum that handles every literal
+// leaves `Never` as the residual). Users never write `never` themselves.
+//
+// As a subtype of everything, Never is assignable into any slot - that's
+// what makes the "you exhausted the switch" property compose naturally with
+// the rest of the type checker. But nothing except Never is assignable TO
+// Never; assigning a real value into a Never-typed slot signals a soundness
+// issue (the checker thought a branch was unreachable, but the user reached
+// it anyway).
+type TypingNeverT struct{}
+
+func NewNeverType() *TypingNeverT {
+	return &TypingNeverT{}
+}
+
+func (t *TypingNeverT) Name() string {
+	return T_NEVER
+}
+
+// IsCompatibleWith returns false: no value has type Never at runtime. This
+// matters when the static type happens to flow into a function call boundary
+// check - any actual value will fail the compatibility test, which is the
+// correct outcome since reaching such a call would mean narrowing was wrong.
+func (t *TypingNeverT) IsCompatibleWith(TypingCompatVal) bool {
+	return false
+}
+
 type TypingVoidT struct{} // -> void
 
 func NewVoidType() *TypingVoidT {

rts/rl/typing_assignable.go

@@ -8,15 +8,16 @@ package rl
 // compatibility logic together; the runtime IsCompatibleWith methods remain
 // alongside their types.
 
-// isAnyLike reports whether other is one of the universally-consistent types:
-// `any` (user-written escape hatch) or `dynamic` (the implicit form assigned
-// when static inference can't pin a type). Every concrete IsAssignableFrom
-// checks this first so values of these types can flow into any target without
-// false negatives. The set grows again when the checker adds `error_type`
-// (poisoned, for cascade prevention).
+// isAnyLike reports whether other is a "flows-into-anything" type: `any`
+// (user-written escape hatch), `dynamic` (the implicit form assigned when
+// inference can't pin a type), or `never` (the bottom type, vacuously a
+// subtype of everything because no value inhabits it). Every concrete
+// IsAssignableFrom checks this first so values of these types can flow into
+// any target without false negatives. The set grows again when the checker
+// adds `error_type` (poisoned, for cascade prevention).
 func isAnyLike(other TypingT) bool {
 	switch other.(type) {
-	case *TypingAnyT, *TypingDynamicT:
+	case *TypingAnyT, *TypingDynamicT, *TypingNeverT:
 		return true
 	}
 	return false
@@ -54,6 +55,9 @@ func typesEqual(a, b TypingT) bool {
 	case *TypingDynamicT:
 		_, ok := b.(*TypingDynamicT)
 		return ok
+	case *TypingNeverT:
+		_, ok := b.(*TypingNeverT)
+		return ok
 	case *TypingVoidT:
 		_, ok := b.(*TypingVoidT)
 		return ok
@@ -236,14 +240,27 @@ func (t *TypingDynamicT) IsAssignableFrom(TypingT) bool {
 	return true
 }
 
-// Void is the type of expressions that produce no value (e.g. print()). Only
-// itself is assignable to it; this catches `x = print(...)` at the type
-// checker rather than at runtime.
+// Void is the type of expressions that produce no value (e.g. print()).
+// Only Void itself and Never are assignable to it. Notably `any` and
+// `dynamic` are NOT - that's how `x = print(...)` gets caught instead of
+// being silently swallowed under gradual consistency.
 func (t *TypingVoidT) IsAssignableFrom(other TypingT) bool {
+	if _, ok := other.(*TypingNeverT); ok {
+		return true
+	}
 	_, ok := other.(*TypingVoidT)
 	return ok
 }
 
+// Never is the bottom type: only Never itself can flow into a Never slot.
+// (Other types DO accept Never as a source because Never is a vacuous
+// subtype of everything - that's handled by the isAnyLike short-circuit at
+// the top of every other IsAssignableFrom.)
+func (t *TypingNeverT) IsAssignableFrom(other TypingT) bool {
+	_, ok := other.(*TypingNeverT)
+	return ok
+}
+
 // --- Collections (invariant) ---
 
 // AnyList is the unparameterized list type. It accepts any concrete list or

rts/rl/typing_assignable_test.go

@@ -79,6 +79,39 @@ func TestAssign_DynamicIsUniversallyConsistent(t *testing.T) {
 	assert.True(t, strList.IsAssignableFrom(dynT))
 }
 
+func TestAssign_NeverIsBottom(t *testing.T) {
+	neverT := rl.NewNeverType()
+	intT := rl.NewIntType()
+	strList := rl.NewListType(rl.NewStrType())
+
+	// Never accepts only Never.
+	assert.True(t, neverT.IsAssignableFrom(rl.NewNeverType()))
+	assert.False(t, neverT.IsAssignableFrom(intT))
+	assert.False(t, neverT.IsAssignableFrom(strList))
+	assert.False(t, neverT.IsAssignableFrom(rl.NewVoidType()))
+
+	// Every other type accepts Never as a source - it's vacuously a subtype
+	// of everything because no value inhabits it. This is what makes
+	// "switch exhausted all cases, residual is Never, post-switch code is
+	// reachable as anything" work cleanly.
+	assert.True(t, intT.IsAssignableFrom(neverT))
+	assert.True(t, strList.IsAssignableFrom(neverT))
+	assert.True(t, rl.NewAnyType().IsAssignableFrom(neverT))
+
+	// Even void accepts Never (vacuously).
+	assert.True(t, rl.NewVoidType().IsAssignableFrom(neverT))
+}
+
+func TestAssign_NeverHasNoValues(t *testing.T) {
+	// No runtime value should ever be considered compatible with Never. The
+	// runtime never sees Never directly today, but the contract matters if
+	// it ever flows through a call-boundary check.
+	neverT := rl.NewNeverType()
+	assert.False(t, neverT.IsCompatibleWith(rl.NewIntSubject(0)))
+	assert.False(t, neverT.IsCompatibleWith(rl.NewStrSubject("")))
+	assert.False(t, neverT.IsCompatibleWith(rl.NewNullSubject()))
+}
+
 func TestAssign_DynamicAndAnyAreDistinct(t *testing.T) {
 	// They behave identically for IsAssignableFrom today, but they're not the
 	// same type. The static checker must be able to tell them apart - that's