(Hoping I figured out how to reply in the thread now... )
Yes, sorry for the cryptic message but it looks like you got it right. The
example isn't impressive but just like Steven is saying the value comes in
larger applications. In a web application for instance only the parsing
layer will have to deal with the runtime validation of the type. The
business logic and database layers can use static type checking to make
sure only the narrowed value is allowed. So it's kind of like a NewType
plus an "instantiation predicate" (I'm failing to find the correct term,
nothing is actually instantiated).
I thought it's relevant here since I imagine a NotType would also have to
rely a lot on runtime narrowing. If a downstream API takes Sequence &
Not[str] and we have a Sequence available, we'd have to narrow it with
something like assert not isinstance(..., str).