Problems with TypeIs

Sorry, it’s also my fault for not being clearer that I was deferring to the existing post about negation rather than rehash it as well in my hesitation to rehash everything.

I showed it happens with protocols instead of sequence too.

Actually, the pep says that typecheckers should error for invalid TypeIs functions too

The pep links the pep483/484 definition of consistent, which is subtyping based. When I wrote that example, I made sure to start with a TypeIs function that was specified as safe use and create an unsafe example using it.

Is it not a spec contradiction for the spec to say that it should follow the theory, but then allow things we knew were unsound? What about a specification problem that there are functions specified as safe that aren’t?

Can you be sure there aren’t other problems that we haven’t discovered yet? We’re arguing about one case that’s clearly wrong, and ignoring that the presence of such a case means any reasoning used to justify the soundness of the feature is flawed, so other conclusions from it are also suspect.