为何使用未装箱类型时undefined函数支持轻量多态？

Great question—let's work through this using the boxing/unboxing definitions you pulled from the Levity Polymorphism paper as our foundation.

First, let's restate those definitions clearly to align our discussion:

boxed（装箱）：装箱值由指向堆的指针表示，Int和Bool是具有装箱值的类型示例。
unboxed（未装箱）：未装箱值由值本身表示（而非指向堆的指针），GHC.Prim模块中的Int#和Char#是此类类型的示例

Now, let's dive into why undefined plays nicely with unboxed types via levity polymorphism.

1. undefined is a bottom-type value #

In Haskell, undefined is a member of the bottom type (⊥)—a type that's a subtype of every other type in the language. By definition, this means it can legally inhabit any type, whether that type is boxed (like Int) or unboxed (like Int#). The problem before levity polymorphism was that GHC's type system couldn't express this flexibility across different "levities" (the paper's term for distinguishing boxed vs unboxed types).

2. Levity polymorphism solves the representation mismatch #

Without levity polymorphism, we'd be stuck writing separate versions of undefined for every unboxed type: undefinedInt# :: Int#, undefinedChar# :: Char#, and so on. That's not just tedious—it defeats the purpose of having a generic "non-termination/crash" value.

Levity polymorphism fixes this by letting undefined have a polymorphic type that abstracts over levity:

undefined :: forall (r :: RuntimeRep). forall (a :: TYPE r). a

Here, RuntimeRep captures whether the type a is boxed or unboxed. This single definition can be instantiated to any type, regardless of its representation.

3. GHC doesn't need a concrete value for undefined #

The key trick here is that undefined never actually produces a concrete value—it's just a stand-in for a computation that fails (e.g., throws an error or loops forever). For unboxed types, which require direct value representation (no heap pointer), this works because we don't need to allocate or construct a valid unboxed value. When you use undefined :: Int#, GHC just emits code that triggers the same error behavior as the boxed version—no need to shoehorn a pointer into an unboxed slot.

Putting it all together: undefined's bottom-type semantics, paired with levity polymorphism, let it act as a generic "invalid" value across both boxed and unboxed types without breaking their representation rules.

内容的提问来源于stack exchange，提问作者illabout