...but we currently don't do that.

We currently do the following simplifications:

1. type & bool & ~Literal[True] -> Never
2. bool & type & ~Literal[True] -> Never
3. bool & ~Literal[True] & type -> Never
4. ~Literal[True] & bool & type -> Never
5. type & ~Literal[True] & bool -> type & bool ‼️
6. ~Literal[True] & type & bool -> type & bool ‼️

After much puzzling, I figured out that this is what currently happens for each intersection:

1. type & bool & ~Literal[True] -> (type & bool) & ~Literal[True] -> type & Literal[False] -> Never
2. bool & type & ~Literal[True] -> (bool & type) & ~Literal[True] -> type & Literal[False] -> Never
3. bool & ~Literal[True] & type -> (bool & ~Literal[True]) & type -> Literal[False] & type -> Never
4. ~Literal[True] & bool & type -> (~Literal[True] & bool) & type -> Literal[False] & type -> Never
5. type & ~Literal[True] & bool -> (type & ~Literal[True]) & bool -> type & bool
6. ~Literal[True] & type & bool -> (~Literal[True] & type) & bool -> type & bool

All the simplifications we're doing look correct to me here (simplifying type & ~Literal[True] to type is accurate given that type and Literal[True] are disjoint types). It's just that we're missing some additional simplifications that turn out not just be desirable, but actually necessary for correctness given the simplifications we already have in place. Namely, type & bool must be recognised as disjoint types, given our simplifications of bool & ~Literal[True] -> Literal[False] and given that we recognise type and Literal[True] as being disjoint.

We'll naturally recognise bool and type as being disjoint once we flesh out our support for @final instance types, so there's nothing to do here that we weren't going to do anyway. But it's quite interesting!