[eyelidlessness]

This is a good example of how `never` is treated as `never`. Everything is assignable to the bottom type and intersecting with it will always be the bottom type, by definition. It’s also a good example of how the top type `any` casts to whatever you choose, because that’s also by design. Both types are vacant, the bottom type is infectious. That’s a good thing. And it works the same way with `unknown`, which it also should because once something is known to be part of the null set it should stay known as the null set.

[consilient]

> Everything is assignable to the bottom type

Other way around: everything is assignable to the top type (`unknown`), and the bottom type (`never`) is assignable to everything.

> It’s also a good example of how the top type `any` casts to whatever you choose

Which is precisely why `any` isn't the top type: if you allow `any`, then types no longer form a lattice, and there is no bottom or top.

If you restrict yourself to a sound fragment, then `unknown` is the top type. Compare `(x: unknown) => boolean` (two inhabitants up to function extensionality) to `(x: any) => boolean` (infinitely many inhabitants).

> And it works the same way with `unknown`, which it also should because once something is known to be part of the null set it should stay known as the null set.

But `unknown` isn't the null set: it's the "set" (insofar as we're pretending that types are sets of values, which isn't quite true) of all terms.

[eyelidlessness]

> Other way around: everything is assignable to the top type (`unknown`), and the bottom type (`never`) is assignable to everything.

Yep, sorry that’s what I meant.

> Which is precisely why `any` isn't the top type: if you allow `any`, then types no longer form a lattice, and there is no bottom or top.

I’m not sure I understand.

> If you restrict yourself to a sound fragment, then `unknown` is the top type. Compare `(x: unknown) => boolean` (two inhabitants up to function extensionality) to `(x: any) => boolean` (infinitely many inhabitants).

Sure, but I was referring to an exception I make for ignored parts of a type, in a type param. This example would be more analogous as:

  <T extends (x: unknown, ...rest: any[]) => boolean>

Which I hope makes my exception more clear, even if you don’t agree with it. It hopefully communicates that x is of interest and rest is not.

> But `unknown` isn't the null set: it's the "set" (insofar as we're pretending that types are sets of values, which isn't quite true) of all terms.

I was referring to never as the null set. Once you narrow anything—any, unknown, etc—to never, you can’t widen it to anything (without an unsafe cast of course).