flesh out void types

exotic-sizes.md

@@ -81,9 +81,33 @@ consider passing in `0` as Undefined Behaviour.
 
 Rust also enables types to be declared that *cannot even be instantiated*. These
 types can only be talked about at the type level, and never at the value level.
+Empty types can be declared by specifying an enum with no variants:
 
 ```rust
-enum Foo { } // No variants = EMPTY
+enum Void {} // No variants = EMPTY
 ```
 
-TODO: WHY?!
+Empty types are even more marginal than ZSTs. The primary motivating example for
+Void types is type-level unreachability. For instance, suppose an API needs to
+return a Result in general, but a specific case actually is infallible. It's
+actually possible to communicate this at the type level by returning a
+`Result<T, Void>`. Consumers of the API can confidently unwrap such a Result
+knowing that it's *statically impossible* for this value to be an `Err`, as
+this would require providing a value of type Void.
+
+In principle, Rust can do some interesting analysees and optimizations based
+on this fact. For instance, `Result<T, Void>` could be represented as just `T`,
+because the Err case doesn't actually exist. Also in principle the following
+could compile:
+
+```rust,ignore
+enum Void {}
+
+let res: Result<u32, Void> = Ok(0);
+
+// Err doesn't exist anymore, so Ok is actually irrefutable.
+let Ok(num) = res;
+```
+
+But neither of these tricks work today, so all Void types get you today is
+the ability to be confident that certain situations are statically impossible.