Handle "impossible" intersections

This issue is about handling an "impossible" intersection by static type checkers.  We consider two cases:
It must be transformed to Never
Arguments in favor:

@mikeshardmind argues that is unsafe.
@gandhis1 argues not doing so creates divergent behavior between typecheckers
@mikeshardmind argues not doing so creates divergent behavior between typecheckers in a different way in a related case

It is up to the type checker to reduce it or not
Arguments in favor:

@erictraut argues that the conditions are complex and expensive.
@erictraut argues in the context of reduction and normalization.
@CarliJoy argues that there are problems caused by inconsistent typing definitions in the standard library.

(Please edit this comment. I haven't gone through the whole issue to add links to everyone's arguments.)

I don't really think this needs it's own issue. We can detect some cases where an intersection is impossible to satisfy, and that should result in Never

@mikeshardmind I already wrote an algorithm for protocols in the current specification under https://github.com/CarliJoy/intersection_examples/blob/main/specification.rst#protocol-reduction
Could you adopt this algorithm to accompany this?

I'm not in a position to do anything formal at the moment, but that said I already posted a partial list of "trivial" reductions in the discord server, I'll post them here as well.
Note, removal of Any was included prior to some people finding that controversial, don't read into it as a mandate that this approach is the resolution
Trivial Removal of Any
Any & P -> P
Any & P & Q -> P & Q
Subtype relationship example
(copied directly from draft, already included)
(Note: examples for Any above also follow this rule of more specific types taking precedence)
Intersection[str, Employee, Manager] is Intersection[str, Manager]
concrete types which fully satisfy protocols
SupportsIndex & int -> int
Reductions involving None
None & ConcreteType -> Never
None & ProtocolNoneDoesntSatisfy -> Never
None & ProtocolNoneSatisfies -> None  (ie. bool)
Interaction with other Final types
(Note: None follows all of these rules, no special casing of None)
FT is a final type
NBFT is another type that isn't in FT's bases
BFT is a type that is in FT's bases
SFTP is a protocol (heh) that FT satisfies
NSFTP is a protocol that FT does not satisfy
FT & NBFT -> Never
FT & BFT -> FT
FT & NSFTP -> Never
FT & SFTP -> FT

In addition to this post, there's also if you have two types with incompatible interfaces -> Never as it would be impossible to satisfy both requirements requested by use of the intersection. I don't think artificially creating overloads works, for reasons above, complexity, and so on. It also behaves more like a Union at that point, so if you want a Union, just use a Union.

In addition to this post, there's also if you have two types with incompatible interfaces -> Never as it would be impossible to satisfy both requirements requested by use of the intersection. I don't think artificially creating overloads works, for reasons above, complexity, and so on. It also behaves more like a Union at that point, so if you want a Union, just use a Union.

That's where we disagree.
Creating overloads is actually one use case for intersections. I.e. think of Callable[[int], str] & Callable[[float], [str].
People already said that would expect an overload there.
Of course the special cases about staticmethods and classmethods are non trivial and need some evaluation.

I would expect this to be an error. If I wanted that, the correct tool is a Union, not an intersection.
Callable[[int], str] | Callable[[float], [str] has the behavior you are putting into the intersection here by creating overloads artifically.

The specification is also stricter on allowable type combinations than what is required by python. It is possible to have multiple inheritance from multiple builtin types without it being in error. This is why my post was specific to mention type compatibility as well as if a class was marked as being final

The specification is also stricter on allowable type combinations than what is required by python. It is possible to have multiple inheritance from multiple builtin types without it being in error. This is why my post was specific to mention type compatibility as well as if a class was marked as being final

That is not correct, see https://github.com/CarliJoy/intersection_examples/blob/main/test_basetypes.py I didn't find any combination that is valid.

I should have been so much more specific. There is no rule in the interpreter or at runtime that multiple inheritance from builtin classes is impossible. The specification implies this off it being true for the current types there, but one can imagine that it may not remain true. It should be both sufficient, more succinct, and more permanently correct to say that A & B is not valid if class(A, B) is not valid.

Anyhow, if you are resolving this by adding overloads, I'm no longer interested in intersections. I consider this to be antithetical to why I want an intersection in python. Everything else there's been disagreement about I could see multiple paths out of, but this would result in me just not using the feature ever. It would be more correct to just hand out protocols that specify exactly my intent at that point.
If I specify A & B where A is mine, and B is a library's, I expect that A & B are out-of-the-box not incompatible interfaces. Hiding the incompatibility with artificially inserted overloads that then have to be checked for an outcome when used breaks expectations and some of the reasons for Intersections. I want to be able to use this as if it is A and as if it is B. If I wanted to check which interface I had, I wouldn't need an intersection.

Well the correct definition would be A & B is never if class (A, B) or class(B, A) raises TypeError.
There are two Problems with this definition:

Performance: You need to check all permutations of all arguments
It requires running the code what a type checker never should do (strongest arguemt)
How should type checker not implemented in python know this? And there are even multiple implementations of python next to CPython. So maybe in one of this implementation class (int, float) maybe even works. So typing will now depend on the compiler?

I read through the current specification, and I need to state more than just simple agreement that the overloads are a mistake. This creates a situation where intersections do something that could never be valid on real classes for protocols, and only for protocols. Protocols are already only a definition structurally, I would expect any incompatibility to be a mistake.
You can't hack this together for real classes, because it would become an LSP violation. This breaks symmetry between structural and nominal typing.

That's not a good reason for blocking possible intersections. I'm with Eric: you should leave this up to type checkers.

Okay, then leave it up to type checkers. The current spec instead mandates a synthetically created overload and this is what I took issue with, and what you attempted to demonstrate was "fine actually".

Sorry, that's not what I was saying.  What I was saying was that trying to block "incompatible interfaces" would end up blocking intersections that were actually possible, and I was presenting the overloads as an example of a possible intersection.

I think we fully agree that compatible things should not be blocked if at all reasonably possible, and only disagreed on the specific example given being reasonably possible.

Fair enough.  It sounded like you were suggesting an incremental approach:

It is possible to start with what is currently possible to do correctly, and expand incrementally as there is demonstrated need for it.

I don't want to go through all of these issues that will sit unsolved for years.  Better to not induce them to be created in the first place.

and doesn't require an answer to that being satisfactory to be immediately apparent

Right.

Fair enough. It sounded like you were suggesting an incremental approach:

Well, to be fair, I was, but not in a way that I believed required this to become a progress blocker or extra rules to specifically block something valid. I think Eric's comments made the case far more elegantly than I did, but it is my belief that if the rules we pick are fundamentally sound, then it doesn't matter if we do not have all the answers, but if we have special cases for things, we actually do need all the answers that are relevant to those special cases, or the rules become ambiguous.
Because I was operating with the lens of the current draft specifying a specific behavior for how to solve an intersection, rather than only defining the intersection and whether something is considered a sound intersection based on general rules, I was attempting to show that the prescribed behavior for a specific case was not able to completely solve all instances of that case, and was therefore partially ambiguous, and better not to have that included as a result. Even simpler though is what Eric said, just define it correctly from base rules and let implementations handle the implementation of the definition.

While I understand the need for practicality to determine what rules are checked or not, I'm not thrilled at the idea of allowing for even more areas where the various type checkers can have inconsistent errors. This freedom is beneficial for type checker maintainers but a burden to type annotation maintainers. Libraries often have to choose a single type checker to support or attempt to support both and regularly run into conflicts (as I have witnessed with pandas-stubs).
I don't want to derail this thread with a debate on that more general issue, but simply want to offer a counterpoint as to why mandating a consistent set of errors that all maintainers can agree on actually may be desirable. If something will likely end up being non-performant or tedious to implement, perhaps now is the time to refine that.

@gandhis1 thanks for laying out this potential conflict. I am sure we can find a solution the fits to both target groups.
A PEP that doesn't limit type checker maintainers in their implementation but is still well enough defined to ensure compatible results of different checkers.
Seeing the different opinions about how strict a type checker should be i.e. when it comes to differing function parameter definition I am also fearing we would increase the problem of type checkers giving different results.
Maybe one type checker implements a strict understanding of intersection and another a flexible.
A maintainer of type annotations for code that is valid python but wasn't well designed (i.e. not 100% following the LISP completely) could run in serious troubles.
Even worse would be if one type checker is strict with one aspect and the other in another.
@erictraut I fully understand your concern about the final PEP becoming to complex and unsound. Still don't you think that formulating that target what should evaluate to Never could be formulated without falling into a logical/complex trap?
@mikeshardmind I am not an expert so feel free to come up changes of the draft :-)

Specifying that an intersection type should be reduced to Never under certain circumstances is less problematic than dictating that an intersection type should be disallowed (and generate an error condition) under certain circumstances. There are many places where an intersection type may be generated within the internal bowels of a type checker (just as a union type may be generated), and it's not always possible to know how to present the user with an intelligible error message or determine which node in a parse tree to associate that error with.
Specifying that an intersection should be reduced to Never is still somewhat problematic for the following reasons:

It requires normalization (i.e. distributing intersections over unions) and reduction logic to be applied any time an intersection type is generated internally to the type checker. The normalization will necessarily change the way the type is "spelled" (i.e. how it appears within an error message), so users may be confused about why the type appears different from how they typed it.
Normalization and reduction are both costly, and this is on a hot path in the type checker. Neither pyright nor mypy attempt to apply any reduction to unions except for duplicate removal and the removal of Never, both of which are cheap checks. Neither mypy nor pyright attempt to eliminate subtypes within unions, for example. Doing so would affect type checking performance — significantly in some cases. If we limit reduction to cases that involve Any (as TypeScript does), that can be done efficiently because it doesn't require normalization and can be done with an O(n) algorithm. But other rules (those that involve subtype checks) are very expensive and require normalization and pairwise operations that result in O(n^2) performance (where n is the number of types in the intersection).
Reducing certain intersections to Never requires us to correctly and completely identify all of the rules about which conditions cause such reduction. Changing the rules even slightly in the future will result in breaking changes to the type system. I have low confidence that we can establish a comprehensive list of all conditions that can result in intersections that are not realizable at runtime. The Python runtime is so full of exceptions and special cases that it makes this difficult. If we indicate that no reduction is performed — or that reduction is performed only in a few very specific cases (e.g. with Any), then we avoid this problem.
It creates an inconsistency with unions. No reduction rules are stipulated in the typing standard for unions. In practice, type checkers do not reduce unions except for the few specific cases noted above (duplicate and Never removal).

It requires normalization (i.e. distributing intersections over unions) and reduction logic to be applied any time an intersection type is generated internally to the type checker. The normalization will necessarily change the way the type is "spelled" (i.e. how it appears within an error message), so users may be confused about why the type appears different from how they typed it.

With regard to this case, we can (and maybe even should) say that the canonical form for intersections and unions should be Disjunctive Normal Form. (there are good reasons for choosing this form in terms of thinking about it and structuring of code that would operate on these) This then gives a good way to explain to users, it would be consistent, and it wouldn't be something that changes with every little change to the type system.
I originally thought there should be cases removed for detectability as Never to help assist users in reasoning about why certain combinations don't need to be considered, but I think your points about performance, as well as all the various potential exceptions and changes over time, is a good reason not to except for perhaps the most basic cases such as T & Never, and that even in that case, we can leave choosing to simplify it to Never to type checkers to decide.

With regard to this case, we can (and maybe even should) say that the canonical form for intersections and unions should be Disjunctive Normal Form.

I also suggested disjunctive normal form last year.

Given the example in https://github.com/CarliJoy/intersection_examples/issues/5#issue-1818919668, wouldn't it be more useful to just coerce (A&B).foo to Never, instead of A&B itself? I see several advantages:

Sometimes we might want to use the intersection of 2 classes despite the incompatibility of some methods, if we only intend to use compatible methods.

This might especially be important when one of the classes implements __getattr__, since, strictly speaking, if A implements __getattr__ then it shadows any methods of B not implemented by A.

As a concrete example, consider pandas.DataFrame, which during __init__ adds column names as attributes if they don't shadow any existing attributes.

Also, one might consider the possibility of users fixing incompatible signatures through @override

Type-checkers can still warn when incompatible classes get created, and raise errors as soon as an incompatible method gets used (since Never cannot be called)

Given the example in #5 (comment), wouldn't it be more useful to just coerce (A&B).foo to Never, instead of A&B itself? I see several advantages:

I think it's better to leave it up to type checkers.  But in general, I agree that that's probably what would end up happening in practice.   Mandating that A&B must fail induces a quadratic time (minimum) check.

Given the example in https://github.com/CarliJoy/intersection_examples/issues/5#issue-1818919668, wouldn't it be more useful to just coerce (A&B).foo to Never, instead of A&B itself? I see several advantages:

Sometimes we might want to use the intersection of 2 classes despite the incompatibility of some methods, if we only intend to use compatible methods.

No. This is quite literally the use case for Union. Observe:
from typing import reveal_type

class A:
    foo: int
    bar: int

class B:
    foo: int

def show_union(x: A | B) -> None:
    reveal_type(x.foo)
    reveal_type(x.bar)

main.py:12: note: Revealed type is "builtins.int"
main.py:13: error: Item "B" of "A | B" has no attribute "bar"  [union-attr]
main.py:13: note: Revealed type is "Union[builtins.int, Any]"
Found 1 error in 1 file (checked 1 source file)

Intersection having this behavior violates the motivating cases for it, and the generally understood definition that we are specifying multiple constraints that each much apply in the case of an intersection, whereas with Union we are applying multiple constraints that one or more must apply.

I now think it's better to leave it up to type checkers.

I think the behavior of attribute access needs to be well defined, but that any early termination to Never would be entirely up to type checkers

@mikeshardmind "No. This is quite literally the use case for Union."
When one uses A & B the expectation is that (A & B).foo = A.foo & B.foo and not A.foo | B.foo. What I am saying is that I want to be allowed to use A & B even if for some attribute bar, A.bar is incompatible with B.bar, (in the sense A.bar & B.bar = Never), because in certain situations I might only be interested in using attribute/method (A & B).foo = A.foo & B.foo. Type checkers should (imo) in most cases not coerce A&B to Never (only when it is impossible at runtime to create a subclass, e.g. due to baseclass/metaclass conflict, such as in class A(int, str) (https://github.com/CarliJoy/intersection_examples/issues/5#issuecomment-1648816964).)
I disagree that for the example given in the original post an intersection is impossible. https://github.com/CarliJoy/intersection_examples/issues/5#issue-1818919668
class A:
    foo: int
    @staticmethod
    def more_complicated() -> int: ...

class B:
    foo: str
    def more_complicated(self, something: int) -> str: ...

The following seems to be formally just fine:
class C(A, B):
    foo: Never
    def more_complicated(self: object, *args: Any) -> Never: ...

I would want the behavior:
c: C = C()  # ✔
x: object = C.foo  #  ✘ can't assign Never
C.bar()
y: int  = 0  # ✘ unreachable

@randolf-scholz
That sounds like a case for a protocol describing the behavior you actually want instead of asking a type checker to make sense of an incompatible definition. There have been discussions in the discord about this case and making it more ergonomic with something like ProtocolFromType and Omit (Omit to explicitly discard things from the runtime type that you don't care about for the generated protocol), but you're missing the part where the interface a type has is a distinctly different thing from an instance of an object satisfying the requirement of being a type.
you can't have a real class that satisfies the type system in the example there, incompatible subclasses generate errors themselves.

That sounds like a case for a protocol describing the behavior y

The problem with is that you don't always have control of the code producing the intersection.  The intersection might be produced synthetically in a generic function or class.  So, you can't simply rewrite the intersection using a protocol even if that's the ideal solution.
Second, just because the return value of the methods in the intersection of the classes has type Never, that doesn't mean that the intersection is impossible.  Perfectly valid methods can return Never, for example, if they raise unconditionally.  So, it's still possible for there to be a valid subclass.

@randolf-scholz
https://github.com/python/typing/issues/213#issuecomment-1646681413 already explains why only viewing the types of the  attributes of the object and not checking for compatibility of type isn't valid here.
I suggested ProtocolFromType in the discord to help make this case easier. I also suggested we limit Intersections to only protocols because I believe this is the only real use case for intersections. This also gets rid of the stupidity of Any. If you already have a class that validly subclasses multiple classes, you can just type hint that. I was not the first person to suggest this. @erictraut did over a year ago

Second, just because the return value of the methods in the intersection of the classes has type Never, that doesn't mean that the intersection is impossible. Perfectly valid methods can return Never, for example, if they raise unconditionally. So, it's still possible for there to be a valid subclass.

The attributes conflict. you can't subclass from both int and str, so it is impossible for a subclass to be a valid subclass of both A and B because the subclass would violate replacement for at least one of these.

The attributes conflict

Okay, I thought we were still talking about method.  It's fine to deduce unreachable/never when the subclass is impossible.  I don't think it's fine to raise any kind of type error just because the intersection has shown up.

Returning Never from something typed to return something specific would Also violate replacement.

Isn't it the bottom type?  Surely, an ordinary method with the same signature would not violate replacement.  And if that method raises unconditionally, that wouldn't violate replacement.  So I don't see why narrowing its return to Never would violate anything new.  The return type is covariant, so narrowing should always be okay.

It violates basic subtyping replacement.
In the intersectionless example
class A:
    foo: int
    @staticmethod
    def more_complicated() -> int: ...

class B:
    foo: str
    def more_complicated(self, something: int) -> str: ...

class Invalid(A, B):  # It's a type error  here before we even use it
    foo: Never
    def more_complicated(self, *args: Any) -> Never: ...

def example(x: A):  # but we pass in an instance of `Invalid`
    x.foo  # This should be int, but passing an instance of Invalid breaks everything. You can't *have* something here.
    x.more_complecated()
    # This should return an int and must error instead of only erroring if something unexpected happened.
    # This one might technically be allowable, but if your example to make something work
    # requires making it in fact not work, maybe we can find a better option for people
    # all type checkers currently see this as an error to define `Invalid` this way.

main.py:17: error: Signature of "more_complicated" incompatible with supertype "A"  [override]
main.py:17: note:      Superclass:
main.py:17: note:          @staticmethod
main.py:17: note:          def more_complicated() -> int
main.py:17: note:      Subclass:
main.py:17: note:          def more_complicated(self, *args: Any) -> NoReturn

@mikeshardmind I'm not a type theorist, but from my pedestrian understanding the bottom type in a sound type system satisfies 2 essential properties

It is a subtype of every other type. In particular, Never ≤ (int & str)
It is uninhabited, i.e. no instances of Never can be created.

in particular we can have no instance of int & str, because int & str = Never due to base/meta-class conflict.
however, we can have a function like def stop() -> never: raise RuntimeError('no way')

Now, I hope we can agree that for example this means we should be allowed to intersect:
class A:
    def foo(self) -> int: ...
class B:
    def foo(self) -> str: ...
class C(A, B):
    def foo(self) -> Never: ...

c: A&B  = C()

because otherwise, you'd need to already disallow any class that has a Never-annotated method. You object that it is different for attributes. OK, what about properties?
class A:
    @property
    def foo(self) -> int: ...
class B:
    @property
    def foo(self) -> str: ...
class C(A, B):
    @property
    def foo(self) -> Never: ...

c: A&B  = C()

This should be ok as well, right? But properties can act as attributes, we can even add setters and deleters.
What you are essentially saying is that any class X that has an attribute annotated as Never is itself equal to Never, which I just don't see why this should be true. Case in point one can write code like
from typing import Never

class A:
    x: Never
    def foo(self) -> Never: raise RuntimeError

a: A = A()  # ✔ no error

and neither mypy nor pyright will complain about it.

    x.more_complecated()
    # This should return an int and must error instead of only erroring if something unexpected happened.

Methods in Python make no promises about exceptions.  The subclass method raising unconditionally, and being annotated as such is acceptable.

We should make sure, that the problem that was actually the starting point of the original thread can be handled through our definition:
(Here quote copy)

This question has already been discussed […] long time ago, but now I stumble on this in a practical question: How to annotate something that subclasses two ABC's. Currently, a workaround is to introduce a "mix" class:
from typing import Iterable, Container

class IterableContainer(Iterable[int], Container[int]):
    ...

def f(x: IterableContainer) -> None: ...

class Test(IterableContainer):
    def __iter__(self): ...
    def __contains__(self, item: int) -> bool: ...

f(Test())

but mypy complains about this
error: Argument 1 of "__contains__" incompatible with supertype "Container"

But then I have found this code snippet in #18
def assertIn(item: T, thing: Intersection[Iterable[T], Container[T]]) -> None:
    if item not in thing:
        # Debug output
        for it in thing:
            print(it)

Which is exactly what I want, and it is also much cleaner than introducing an auxiliary "mix" class. Maybe then introducing Intersection is a good idea, @JukkaL is it easy to implement it in mypy?

By ilevkivskyi on May 6, 2016
The problem I see is that typing in Python was introduced later in the development and it seems that not even the standard library is typed in a way that it fulfil the typing theory in total.
So if we are too strict with our definitions the Intersection won't be useful to people even if it is "correct" in theory.

@mikeshardmind
  In your example
main.py:17: error: Signature of "more_complicated" incompatible with supertype "A"  [override]
main.py:17: note:      Superclass:
main.py:17: note:          @staticmethod
main.py:17: note:          def more_complicated() -> int
main.py:17: note:      Subclass:
main.py:17: note:          def more_complicated(self, *args: Any) -> NoReturn

 This has more to do with special casing of `@staticmethod` by type-checkers. The decorator prepends the missing `self` argument, promising not to use it. This is a statement about runtime behavior and not types.

Btw: I was not able to extract the Typing Defition of Iterable nor Container  from the typedshed.
Maybe someone can help me here?

@mikeshardmind By the way, I would agree that the following variant should raise an error:
class A:
    foo: int
class B:
    foo: str
class C(A,B):  # <-- no error should be raised here
    foo: Never
    def __init__(self, arg: object) -> None:
        self.foo = arg  # <--- an error should be raised on this line instead

What happens when object is replaced with Any might need discussion, but let's not do that here.
Why should the error be raised at this line? Well, because it is only at this point we try to create an instance of Never, which is not allowed according to the second axiom that the bottom type is uninhabited.

Btw: I was not able to extract the Typing Defition of Iterable nor Container from the typedshed. Maybe someone can help me here?

They are in https://github.com/python/typeshed/blob/main/stdlib/typing.pyi

@randolf-scholz

Why should the error be raised at this line? Well, because it is only at this point we try to create an instance of Never, which is not allowed according to the second axiom that the bottom type is uninhabited.

Yeah, that's the main problem I have here, the secondary problem is that I think the definition of Never currently adopted is actually subtly incorrect for how it is currently treated, but we can shelve that for later, I've started drafting a PEP to amend some definitions to be more accurate to the pragmatic current use.
So, speaking of pragmatism...
What if we went about this like the protocol-only option, but with a little more flexibility in real-world use?
People have clearly stated they primarily care about the structural component (ie. how it gets used). Everyone keeps trying to hand wave the other component of satisfying this. What if we just... embraced that instead.
that being:

Intersections result in a virtual protocol intersecting the interfaces of the types or protocols they are provided.

By definition at that point, satisfying the structure is satisfying the protocol, so essentially: Intersections are how it is valid to use an object, and not of the type of the object, and it must be valid for an object to be used that ay when it comes to assignability.
This also squares well with older comments about what is and isn't well-defined behavior of intersections.

Personally I'd love it if intersections were not restricted to Protocols since that would allow to formalize requests X & Proto :  give me a subclass of X that also provides the following interfaces.
Currently the only way to do this is to create an abstract base class that is a subclass of X and ask users to manually subclass this class. This is undesirable for the very same reasons protocols were introduced in the first place: https://peps.python.org/pep-0544/#rationale, it does against the idea of duck-typing.
For example: I work a lot with pytorch and effectively everything component of a neural network has to be a torch.nn.Module. Some component might have to provide certain functionality, for instance I might want to specify an "encoder" component that is an nn.Module with both an encode and a decode method. Ideally, I'd want to write a protocol Encoder and then type hint such components as nn.Module & Encoder.
So at the least I'd love to see intersections of arbitrary types with Protocols in order to specify mixin functionality. The need for intersections of arbitrary types with arbitrary types is probably less common.

I just don't get why the stdblib defined __x as object here?

I guess so that this is acceptable:
x = [1, 2, 3]
if None in x: ...

This has more to do with special casing of @staticmethod by type-checkers. The decorator prepends the missing self argument, promising not to use it. This is a statement about runtime behavior and not types.

Well, not really. Type checkers special casing staticmethod would be a lack of understanding of descriptors, and that isn't really all that is happening here.
We can't just ignore the descriptor protocol existing or the difference between bound and unbound methods.
class A:
    foo: int
    @staticmethod
    def more_complicated() -> int: ...

class B:
    foo: str
    def more_complicated(self, something: int) -> str: ...

def edge_case(x: A & B):
    type(x).more_complicated  # Note this has well-defined and detected types for both A and B, and they cannot be reconciled

We can't just ignore the descriptor protocol existing or the difference between bound and unbound methods.

The issue is that the descriptor protocol cannot be annotated using Python's current typing.  If you could annotate it, then I don't think there's an issue.

def edge_case(x: A & B):
    type(x).more_complicated  # Note this has well-defined and detected types for both A and B, and they cannot be reconciled

So, from A we have
Callable[[], int]

and from B we have
Callable[[B, int], str]

And the reconciliation has return type Never, and parameter specs as above.

Can we say the central question of this issue is whether an impossible intersection A & B either:

is an error,
must be transformed to Never by static type checkers, or else
can be left as A & B?

I think "must be an error" was already ruled out by the fact that it can arise inside type checker internals, but otherwise yes I think that's an accurate summary of the question

@mikeshardmind In that case, would it be okay if I organized the main comment like we did with #1?  Under each of the two options, we can link to arguments for and against?

@NeilGirdhar yeah, I think that's a great idea

Originally comment by @mikeshardmind in https://github.com/CarliJoy/intersection_examples/issues/3#issuecomment-1648381563

So a derived type that inherits from the members of the intersection can simply resolve the problem by having overloads (for example) that accomodate all of its parent classes.

overloads do not solve this. A & B says that this must satisfy both A and B. This is not possible in some cases by strict incompatibility. artificially adding overloads cannot bandaid over this suitably, and even detecting where it could theoretically would mean that it is not enough to just be a subclass of both A and B, but that you then must reimplement any interfaces which conflicted to accept the overload. This is an unreasonable ask for type checkers for something that won't even work all of the time. Consider these two interfaces:
class A:
    foo: int

    @staticmethod
    def more_complicated() -> int:
        ...

class B:
    foo: str

    def more_complicated(self, something: int) -> str:
        ...

There is no case for overloads here, and this violates requesting compatible interfaces with both A and with B by the intersection. I can't safely do something.foo and know the type anymore, and I can't even safely attempt to call something.more_complicated to then check the resulting type.
Requesting an impossible intersection should be treated as an error.

After some thinking, I believe one should simply treat A&B as an abstract structural type, even if A and B are somehow incompatible.
This seems important to allow for some wiggle room, given that PEP698 @override exists, as well as other tricks like ABCMeta.register and __subclasscheck__. For instance:
class A:
    @staticmethod
    def more_complicated() -> int: ...
class B:
    def more_complicated(self, something: int) -> str: ...
class C(A,B)
    @overrride
    def more_complicated(self, something: int = 0) -> str: ...

c: A&B = C()  # should raise no error!

@randolf-scholz According to PEP698

When type checkers encounter a method decorated with @typing.override they should treat it as a type error unless that method is overriding a compatible method or attribute in some ancestor class.

I don't think override requires a special concern here.
This should absolutely error, and does so. Just not on the last line, override already requires that we are overriding something in a compatible manner.
main.py:7: error: Missing return statement  [empty-body]
main.py:10: error: Missing return statement  [empty-body]
main.py:14: error: Missing return statement  [empty-body]
main.py:14: error: Signature of "more_complicated" incompatible with supertype "A"  [override]
main.py:14: note:      Superclass:
main.py:14: note:          @staticmethod
main.py:14: note:          def more_complicated() -> int
main.py:14: note:      Subclass:
main.py:14: note:          def more_complicated(self, something: int = ...) -> str
Found 4 errors in 1 file (checked 1 source file)

Similarly, it's an error to claim to be a subclass of something and not be, or to register with an ABC and not implement that abc's methods.

Has anyone answered Eric's concerned (linked in the issue)?

@mikeshardmind Even then, the example C(A,B) I gave feasibly works as a subclass of both A and B at runtime, so someone may insist of using it. We can modify the example as
class A:
    @staticmethod
    def more_complicated() -> int: ...
class B:
    def more_complicated(self, something: int) -> str: ...
class C(A,B)
    def more_complicated(self, something: int = 0) -> str: ...  # type: ignore

# possibly even add: C = cast(C, A&B)

c: A&B = C()  # should raise no error!

If you add a type ignore to something, yes things are going to stop being checked properly. This isn't a good argument to make intersections worse

@mikeshardmind I think his point is how you like the rest of the code to work?  Does he now need to type-ignore every A&B?

It's a totality of errors that I don't think we need to be responsible for. If you break out of what can be checked by means of type ignore, there's not much a type-checker can be assumed to do that relies on that.

I think his point is how you like the rest of the code to work? Does he now need to type-ignore every A&B?

To be more specific, from then on, A&B should still just be A&B, if you erroneously broke something with a type ignore, that is on you and not the type checker to resolve.

If you break out of what can be checked by means of type ignore, there's not much a type-checker can be assumed to do that relies on that.

I don't think that reflects how code is actually written.  Have you looked at a major type-annotated project?  They have hundreds of type-ignores, but they still rely on type checking.

The proposal at the top is for A&B to be transformed unconditionally to Never

And that would be correct behavior. A and B are incompatible via the definitions of subtyping. Slapping a type ignore doesn't fix that, it ignores that.

And that would be correct behavior. A and B are incompatible via the definitions of subtyping. Slapping a type ignore doesn't fix that, it ignores that.

Okay, but you where do you want the type-ignore to go?  At every single use of A&B?

@mikeshardmind But, how is it worse? With this you'd need a single type-ignore, if A&B flagged every time you'd need a type:ignore every single time as @NeilGirdhar said.
The only disadvantage I see with keeping A&B structural is that you do not get immediate feedback when you use it, and a type-checker has reason to believe that A is incompatible with B.
But this can be quite easily alleviated by adding such messages whenever someone tries to implement a subclass of A&B.
class C(A,B):
    def more_complicated(self, something: int = 0) -> str: ...  # ✘ incompatible with A.more_complicated

The type-checker should flag both lines:

class C(A,B) should give a message such as  "A and B are incompatible parent classes", which I can choose to ignore.
def more_complicated  should give a message such as "incompatible with A.more_complicated", which I can choose to ignore.

I'd say the code is fundamentally flawed to request an impossible subclass from an intersection. This isn't something to fix by ignoring, it's something to fix by writing better code.

This isn't something to fix by ignoring, it's something to fix by writing better code.

It may not even be your code though.  A and B could come from other libraries, be outside your immediate control, or have other constraints on them that prevent their compatibility.

If your example here requires breaking substitution rules (it does) and then proceeding to ignore the type checker telling you that that is your problem (it also does) then your example is deeply flawed.

That's a fine idealism, but A and B could come from other libraries, be outside your immediate control, or have other constraints on them that prevent their compatibility.

Then don't request an intersection of incompatible things? Request two objects if you need two things. Request a protocol that does specifically what you actually want, etc. Whoever owns the broken intersection needs to be responsible for fixing it.

@mikeshardmind

I'd say the code is fundamentally flawed to request an impossible subclass from an intersection. This isn't something to fix by ignoring, it's something to fix by writing better code.

True, but keep in mind what Eric said in (6) https://github.com/CarliJoy/intersection_examples/issues/1#issuecomment-1657212910. Python is too dynamic for every correct piece of code to be properly statically typed.
Type hinting should not be annoying to the user, that will only hurt adoption. Having to type: ignore every single A&B when I know for a fact that my implementation of the supposedly impossible subclass of both A and B is correct is annoying.

my implementation of the supposedly impossible subclass of both A and B is correct is annoying.
your implementation of A&B broke substitution. you may not see it that way, but it does.

@mikeshardmind Yes it broke static subtyping, which I may choose to ignore if I know it works at runtime (again, see Erics comment). I should be able to do this with minimum effort by putting type: ignore after offending lines in the class body of C(A,B). There is little gained from flagging every single A&B.

here is little gained from flagging every single A&B.

There's no benefit, and real harm to be had from static typing to allow A&B as it alone breaks the rules of static typing. If you want your C just create it and then use that instead of A&B
Additionally, you type ignored the definition that would have to be checked to see if your use is fine, so you broke it that way too.
We can only write the rules for what can be checked statically and gradually, what happens when you break out and ignore the rules entirely should be not be our concern.

@randolf-scholz

Type hinting should not be annoying to the user, that will only hurt adoption. Having to type: ignore every single A&B when I know for a fact that my implementation of the supposedly impossible subclass of both A and B is correct is annoying

Specifying A&B to begin with is incorrect. There is nothing that is compatible with both A and with B by the rules.
If you want something else, specify something else. @DiscordLiz gave you one such obvious answer right above.
@NeilGirdhar

But, how is it worse? With this you'd need a single type-ignore, if A&B flagged every time you'd need a type:ignore every single time

Because you're compromising on what can be checked when people follow the rules for a hypothetical that presumes breaking the rules, and then silencing the error. Designing a feature this way just doesn't make sense, and if you don't want to follow the rules, you don't have to use static analysis. It's an optional feature.

There's no benefit, and real harm to be had from static typing to allow A&B to be anything other than Never as it alone breaks the rules of static typing. If you want your C just create it and then use that instead of A&B

Someone might want to create their own D  (or multiple subclasses of A and B) that at runtime is compatible with both A and B, despite A and B not being able to be equal statically.
Also, if we really want to be nitpicky, I might propose:
class C(A,B):
    foo: Never

Which is compatible with both A and B statically. In fact, for any number of classes T1 ... Tn one can create a trivial subclass of T1 & ... & Tn this way, which kind of proves that the intersection is not empty.

if you don't want to follow the rules, you don't have to use static analysis. It's an optional feature.

But the issue is that people want to "follow the rules" sometimes

There's no benefit, and real harm to be had from static typing to allow A&B to be anything other than Never as it alone breaks the rules of static typing. If you want your C just create it and then use that instead of A&B

Someone might want to create their own D (or multiple subclasses of A and B) that at runtime is compatible with both A and B, despite A and B not being able to be equal statically.
Also, if we really want to be nitpicky, I might propose:
class C(A,B):
    foo: Never

Which is compatible with both A and B statically. In fact, for any number of classes T1 ... Tn one can create a trivial subclass of T1 & ... & Tn this way, which kind of proves that the intersection is not empty.

Great, if you want to argue that, then A&B.foo should still be considered as an error, as it could not exist as anything but Never, which is not satisfiable at runtime. This does not argue what you think it does, just shifts where Never would exist in your scenario.

Great, if you want to argue that, then A&B.foo should still be considered as an error, as it could not exist as anything but Never, which is not satisfiable at runtime. This does not argue what you think it does, just shifts where Never would exist in your scenario.

I think everyone here agrees with that?  If an attribute resolves to Never, that's fine.  But the question is whether impossible intersections must be transformed to Never.

@NeilGirdhar

I think everyone here agrees with that? If an attribute resolves to Never, that's fine. But the question is whether impossible intersections must be transformed to Never.

If an attribute resolves to Never, the class can't be created at runtime. It's still a problem

@mikeshardmind
class C(A,B):
    def __getattr__(self, name: str) -> Never:
        raise AttributeError
c: C = C()

@mikeshardmind
class C(A,B):
    def __getattr__(self, name: str) -> Never:
        raise AttributeError
c: C = C()

If we have to consider this case in static analysis, you should show how it breaks all other existing assumptions of static analysis already @randolf-scholz . This is not an argument you can make in good faith.

@mikeshardmind What does it break statically? Raising an exception is valid behavior. I think @DiscordLiz argued very much the same in https://github.com/CarliJoy/intersection_examples/issues/16#issuecomment-1660807281
And there might be quite practical reasons to allow this. For example, A and B might be huge classes with 99% compatibility but just 1 or 2 methods that are incompatible. It would be quite reasonable to create an intersection that unconditionally raises an exception when trying to access the few conflicting methods but works fine otherwise.
And please don't insinuate bad faith, I am being quite serious here.

It literally doesn't work like you think it does, resolution via MRO happens prior to getattr here.

Fine, my bad. Change __getattr__ to __getattribute__ and it does.

And there might be quite practical reasons to allow this. For example, A and B might be huge classes with 99% compatibility but just 1 or 2 methods that are incompatible. It would be quite reasonable to create an intersection that unconditionally raises an exception when trying to access the few conflicting methods but works fine otherwise.
And please don't insinuate bad faith, I am being quite serious here.

Your suggested "Fix" was to create a class that cannot exist at runtime except via dynamic attribute tricks that are already out of scope for static analysis I can't view this as anything but that.
What you want here is perfectly typable with only the single ignore by creating your subclass, ignoring on it and then using that class as your type hint rather than this impossible intersection. Since you were told this already within the same time that you are arguing for Intersection to do nonsensical things to support breaking the rules, rather than just use this, how else should I interpret this other than an attempt to undermine use of static analysis?

@mikeshardmind What does it break statically? Raising an exception is valid behavior. I think @DiscordLiz argued very much the same in #16 (comment)
And there might be quite practical reasons to allow this. For example, A and B might be huge classes with 99% compatibility but just 1 or 2 methods that are incompatible. It would be quite reasonable to create an intersection that unconditionally raises an exception when trying to access the few conflicting methods but works fine otherwise.
And please don't insinuate bad faith, I am being quite serious here.

It literally doesn't work like you think it does, resolution via MRO happens prior to getattr here.

Fine, my bad. Change __getattr__ to __getattribute__ and it does.

No, that's not what I argued.
foo: Never is different from foo(A) -> Never
In the case of the incompatible parameter list or type, you have the first one. In the case of incompatible return type you have the second.
I also told you how to get what you claimed to want without intersection, so I don't know why you would think I in any way agree with you on this.

@randolf-scholz

What does it break statically? Raising an exception is valid behavior.

Never as an Attribute means the class cannot be instantiated. Never is not satisfiable at runtime, so it is impossible for a class with an attribute to have a type of Never to have instances that exist at runtime. This is different from a function that can never return a value.
Doing something "clever" like __getattribute__ and having it raise an error on a specific attribute doesn't work within the framework of static analysis, this is dynamic resolution at runtime that there is no way to signal to the typechecker currently.
This might be resolvable with adding something like TypeScript's Omit, but not like this; There's no method to communicate this to the type checker properly without additional things.
I'll take you at face value that you really think this is worth it*, but I can't take arguments that go this far out of their way to break the rules seriously, because doing so, and then arguing it should be specifically supported in the face of the more obvious answer if that's what you really want would be sacrificing accuracy of static analysis for those actually playing by the rules for those who are not. That would be a bad priority.
* Separate from "good faith", you have presented a motivation you feel is worth it. The motivation has an obvious answer which you were presented with and then continued to argue for making the feature worse for the people it was for in spite of. I've presumed bad faith here because you chose to continue to more and more convoluted ways to justify it rather than use the obvious alternative that did what you said you wanted. The alternative would be that you ignored another contributor to this offering you a solution for whatever reason, which is just as problematic.

I've presumed bad faith here because you chose to continue to more and more convoluted ways

Sorry, but I don't think assuming bad faith is a productive way to have a conversation.
Just a reminder, but the choice is between mandating that type checkers must resolve impossible intersections to Never, versus type checkers can resolve them to Never.  In the latter case, type checkers can take into account what their users are doing and what their users want.  Are you absolutely sure that your mandated behavior will accord with that?
Maybe it depends on the kind of experience you have writing annotated code, but it's the Wild West in some projects.  People do all kinds of things, and expect them work.  Telling people "don't use static typing" is probably unreasonable.  And forcing them to do some things may be reasonable or unreasonable.
Also, mandating has significant downsides (see Eric's two linked comments) that no one seems to have addressed.

I've presumed bad faith here because you chose to continue to more and more convoluted ways

Sorry, but I don't think assuming bad faith is a productive way to have a conversation.

Are we or are we not creating a feature for static analysis? If your answer is to make it worse for the primary use case while ignoring another option someone provided which doesn't have to do that, you're not being a productive participant.

Just a reminder, but the choice is between mandating that type checkers must resolve impossible intersections to Never, versus type checkers can resolve them to Never. In the latter case, type checkers can take into account what their users are doing and what their users want. Are you absolutely sure that your mandated behavior will accord with that?
Maybe it depends on the kind of experience you have writing annotated code, but it's the Wild West in some projects. People do all kinds of things, and expect them work. Telling people "don't use static typing" is probably unreasonable. And forcing them to do some things may be reasonable or unreasonable.

Actually, you were told to use a specific option that only required the one ignore, why are you still ignoring this?

Also, mandating has significant downsides (see Eric's two linked comments) that no one seems to have addressed.

I specifically did, We need to mandate otherwise we run afoul of diverging behavior between type checkers, which was also one of Eric's concerns.

Doing something "clever" like getattribute and having it raise an error on a specific attribute doesn't work within the framework of static analysis, this is dynamic resolution at runtime that there is no way to signal to the typechecker currently.

There is a way of signaling it (which admittedly type-checkers currently do not support), which is adding @overload with string-Literal:
class A:
    @overload
    def __getattr__(self, name: Literal["foo"]) -> Never:
    @overload
    def __getattr__(self, name: Literal["bar"]) -> int:
    def __getattr__(self, name: str):
        if name == "foo":
            raise ValueError("forbidden")
        if name == "bar":
            return 42
        raise AttributeError

A clever type-checker should be able to deduce that A.foo is Never and A.bar is int. Since type-checkers do not support this currently, one can emulate it via:
class A:
    foo: Never
    bar: int

    def __getattr__(self, name: str):
        if name == "foo":
            raise ValueError("forbidden")
        if name == "bar":
            return 42
        raise AttributeError

I specifically did, We need to mandate otherwise we run afoul of diverging behavior between type checkers

What's wrong with type checkers diverging with respect to false negatives on implementation code?

which was also one of Eric's concerns.

Actually, he specifically said that type checkers only have to agree on interface code.  And my interpretation was that they only have to agree about what things mean—not what's an error.  So, it would be unreasonable for one type checker to implement impossible intersections as object and another to implement it as Never.
But in this case, the choice is between indeterminate and Never.  In which way can this cause problems?  How does someone using an indeterminate form cause interfaces to be bad?

https://github.com/CarliJoy/intersection_examples/issues/5#issuecomment-1666554118
There's no benefit, and real harm to be had from static typing to allow A&B to be anything other than Never as it alone breaks the rules of static typing. If you want your C just create it and then use that instead of A&B

Using C is not a reasonable work-around since A&B might be in a generic function, so C doesn't yet exist.
And "breaking the rules of static typing" is not intrinsically a downside.

And just to clarify how the second option would happen.  Type checkers have large corpuses that they validate their rules on (e.g., the MyPy primer).  If the second option were taken, they could try reducing to Never to see how many errors that would cause.  They can then decide based on real world code which policy to take.
The mandating option forces their hand.  And I just don't see how you can be so sure that that's the better option.   Why not let type checkers gather data and decide after intersections are added?

@NeilGirdhar

And "breaking the rules of static typing" is not intrinsically a downside. We're actually deciding what those rules should be.

The proposed intersection A&B, as well as all instances of classes C proposed by @randolf-scholz break the fundamental rules of subtyping. We can't really have static analysis period if something this fundamental is violated.

But in this case, the choice is between indeterminate and Never. In which way can this cause problems? How does someone using an indeterminate form cause interfaces to be bad?

An attribute being never means the class can't exist at runtime. It isn't indeterminate, it's literally not possible under the rules we are building on.
A & B can be an exported type as a type alias or as an annotation in something exported. If type checkers disagree on the existence of objects which satisfy this, it's divergent behavior with respect to that concern.

What's wrong with type checkers diverging with respect to false negatives on implementation code?

It isn't a false negative, you've violated the rules that intersection is predicated on to satisfy it
@randolf-scholz

Doing something "clever" like getattribute and having it raise an error on a specific attribute doesn't work within the framework of static analysis, this is dynamic resolution at runtime that there is no way to signal to the typechecker currently.

There is a way of signaling it (which admittedly type-checkers currently do not support), which is adding @overload with string-Literal:

do you see the words "to the type checker" in what you quoted? I accounted for it being possible in the future, and if you want this, you can argue that type checkers support this independently from trying to make intersections worse. Adding this after the fact would work fine without special casing here.

We can't really have static analysis period if something this fundamental is violated.

Yes you can?

It isn't indeterminate, it's literally not possible under the rules we are building on.

The indeterminate is A&B (even though an attribute has type never).  And leaving it indeterminate means that it can be used in ways that don't use that attribute.

If type checkers disagree on the existence of objects which satisfy this,

How does anyone get access to "the existence of objects which satisfy this"?  How does this ever come up?

It isn't a false negative,

We're talking about false negatives.  In one case, code that should fail at runtime won't be flagged, in the other case it will be flagged.  This is a false negative.

An attribute being never means the class can't exist at runtime. It isn't indeterminate, it's literally not possible under the rules we are building on.

No, it only means the attribute cannot be safely accessed. If A.foo is Never, it only says that if you try to access A.foo, it raises an exception.

The indeterminate is A&B (even though an attribute has type never). And leaving it indeterminate means that it can be used in ways that don't use that attribute.

You. Can. Not. Have. An. Object. That. Is. Never. At. Runtime. It's impossible by definition of Never. It isn't indeterminate, you literally can't populate the object's fields correctly at runtime.

You. Can. Not. Have. An. Object. That. Is. Never. At. Runtime. It's impossible by definition of Never.

100% agreed.

you literally can't populate the field that is Never correctly at runtime.

100% agreed.

as this violates LSP for the base.

This I do not agree with.
Look, if you can have:
class A:
    def foo(self) -> int:...
class B(A):
    def foo(self) -> Never: ...

which is considered valid, you sure as hell can have
class A:
    foo: int
class B(A):
    foo: Never

All it says is that when you try to access B.foo, you get a Never, an exception, which is a valid subtype of int. How is this in your mind any different than B.foo() vs A.foo() in the prior example? Because 2 brackets are missing? B.foo literally nothing but eye-candy for B.__getattr__("foo")/B.__getattribute__("foo").

class A:
    foo: int
class B(A):
    foo: Never

If mypy and pyright accept this, I'd consider it a bug. This isn't just "a convenience-wrapper for B.__getattr__("foo")/B.__getattribute__("foo")" as you put it. Attributes of classes exist in multiple ways which are a documented part of the python data model, and __getattribute__ is not the only one.
There are other ways this interacts, like vars or __dict__ which don't interact with __getattribute__
Typing what you are showing here properly requires other things we don't have currently. I'm not saying it can't be done in the future, in fact I have, multiple times already, pointed to ideas to make it work. Most specifically bringing up typescript's Omit as a real potential solution for this. But you're asking to make something that isn't possible be ignored as okay just because someone might break the rules, and that's not a useful perspective for static analysis.

If mypy and pyright accept this, I'd consider it a bug.

Maybe you should file the bug to see what they say?  They tend to reply very quickly.

@NeilGirdhar Because when you actually apply this in a real example rather than only add the annotations, you see that it already errors in both ways Never was proposed to solve this.

It's not worth my time to keep arguing with stupid things that shouldn't (and don't) actually work, and it's getting increasingly tiresome doing so with people here.

It's not worth my time to keep arguing with stupid things that shouldn't (and don't) actually work, and it's getting increasingly tiresome doing so with people here.

Do you realize that the people who are reviewing the PEP (including Eric) have upvoted Eric's comments?  Ultimately, for the PEP to be accepted, we'll need convincing arguments for every part of the specification.  Saying that something is "stupid" isn't a convincing argument.

You. Can. Not. Have. An. Object. That. Is. Never. At. Runtime. It's impossible by definition of Never. It isn't indeterminate, you literally can't populate the attribute that is Never correctly at runtime. You also can't not populate the attribute at all, as this violates LSP for the base.

It doesn't matter that no such object could exist.  The point is that the type checker knows that a static type is A & B, and it can--if it chooses--proceed with type inference using A & B.  You are arguing that the type checker must:

detect that A & B is impossible, and
normalize A & B to Never.
But why must it do so?

It seems that all of your arguments so far are simply tautological: "it's correct".  That doesn't mean that it's practical or better for type checking.  Maybe it is practical and better for type checking, but that would be much easier to figure out when you have data based on real world examples.
As Eric has explained, there are costs to detection and normalization.  People run Pyright as an incremental type checker in their IDE, which means that it has to be fast.
Have you given examples of common problems that normalization detects?  The sorts of bugs that it would detect?  Arguing from correctness is unconvincing.
If you can't prove that the benefits outweigh the costs, why should it be specified in the PEP?  Why not let type checkers make that decision?

It's not worth my time to keep arguing with stupid things that shouldn't (and don't) actually work, and it's getting increasingly tiresome doing so with people here.

Do you realize that the people who are reviewing the PEP (including Eric) have upvoted Eric's comments? Ultimately, for the PEP to be accepted, we'll need convincing arguments for every part of the specification. Saying that something is "stupid" isn't a convincing argument.

You. Can. Not. Have. An. Object. That. Is. Never. At. Runtime. It's impossible by definition of Never. It isn't indeterminate, you literally can't populate the attribute that is Never correctly at runtime. You also can't not populate the attribute at all, as this violates LSP for the base.

It doesn't matter that no such object could exist. The point is that the type checker knows that a static type is A & B, and it can--if it chooses--proceed with type inference using A & B. You are arguing that the type checker must:

detect that A & B is impossible, and
normalize A & B to Never.

But why must it do so?

Because if we leave this to the choice of type checker, then this leads to a case where different type checkers can have different behavior. This is a problem for library authors. I'm not rehashing this beyond this. I have said this numerous times already today in this back-and-forth, and prior here and other threads.

Because if we leave this to the choice of type checker, then this leads to a case where different type checkers can have different behavior. This is a problem for library authors.

In which way is it problem for library authors?  What sort of correct code can library authors write that would have different meanings between type checkers?

Other people have pointed to real world issues with prior divergent type checking behavior in this very thread too
There was the issue of diverging behavior in type checkers with Unions brought up at the typing summit which was the motivation for standardization and formalizations
It is an issue for library authors if their users get locked into a singular type checker due to differences in behavior.
Here's another case of divergent behavior causing problems for library authors

Sorry, I'm arguing about any of that.  I'm simply asking:  If we don't mandate normalization, then what sort of correct interfaces can library authors write that would have different meanings between type checkers?
We just need a couple examples so that we can add this to the PEP.

Sorry, I'm arguing about any of that. I'm simply asking: If we don't mandate normalization, then what sort of correct interfaces can library authors write that would have different meanings between type checkers?

None, normalization to Never finds the incorrect use in the case we've been discussing, so framing it around correctness would mean we should reduce it to Never.
If you're suggesting to ignore correctness here, I think that's not helpful, but what would happen is a library author would potentially have some users that could fake it incorrectly, and some that would correctly see that the library can't take a type there. So you now have a library author that wasn't properly warned by their type checker of choice encouraging misuse to the portion of their users that is also using the faulty type checker.
The divergence becomes more important in the case where it actually can be resolved with a Never, albeit with potentially different results, and divergence is less about correctness and more about consistency
# library code
__all__ = ["some_func"]
...
def some_func(x: A & B):
    return x.foo()  # where A.foo incompatible return with B.foo, making raising the only option which is correct.

Some users would see that they can call it, and others would see this as an error. If the library author themselves is in the first camp, this is a problem, especially if they are relying on the return working when it shouldn't and might be caused by an implementation that did not need to even consider intersections before (See related case in 17)

Sorry, I'm arguing about any of that. I'm simply asking: If we don't mandate normalization, then what sort of correct interfaces can library authors write that would have different meanings between type checkers?

Normalization to Never finds the incorrect use in the case we've been discussing, so framing it around correctness would mean we should reduce it to Never.

Finding "incorrect use" is not a thing that must be consistent between type checkers.  That's why I asked about different meanings.  Meanings have to be consistent.  It is already the case that some errors are detected by some type checkers, and others by others.

So you now have a library author that wasn't properly warned by their type checker of choice encouraging misuse to the portion of their users that is also using the faulty type checker.

All type checkers are "faulty" if you mean that they don't report all errors.  Mandating that they have to report errors doesn't help with that.

Some users would see that they can call it, and others would see this as an error. If the library author themselves is in the first camp, this is a problem, especially if they are relying on the return working when it shouldn't and might be caused by an implementation that did not need to even consider intersections before

Yes, it's a problem that they can report to their type checker, and their type checker can prioritize detecting that error based on:

how common they perceive that error to be,
how much effort it will take to fix, and
how computationally efficient a solution would be.
Mandating that they have to is just you making the decision for them with less information.  It just seems presumptuous.

Mandating that they have to is just you making the decision for them with less information. It just seems presumptuous.

It's preventing issues of compatibility, which have been an issue in the past and have also been an issue that those maintaining type checkers have expressed not wanting to have happen with new features and this is a consistent thing that has been stated

We need to define what the correct behavior is.
The correct behavior must not leave room for divergence between type checkers.

If a type checker doesn't catch an error, that's different from the PEP not saying what should be considered erroneous, and to be raised by users to their type checker of choice.
This should not require this much repeated explanation

A few thoughts:

I would typically like to find out if I make an unimplementable type, however, I don't need this directly because a type checker will tell me that it isn't satisfied when I try to implement it.
I also have a linter to tell me if I'm not using some code, which prevents accidentally including something that I haven't covered in tests.  I don't need an explicit error for the type.
I don't like the idea of erroring on Never, because it feels akin to erroring in the empty sequence.  It is not uncommon for Api authors to think that asking for an empty list should raise an error, but in practice it makes it more annoying to work with.  The suggestion of erroring on never triggers my olfactory sense.
type checkers can be wrong.  When they mistakenly assert that something is impossible I'd like to be able to locally tell them via a cast that they are wrong.  If I'm mistaken with that cast, that is on me.
A simpler spec is less likely to be implemented incorrectly, and easier to raise bugs against when a type checker diverges, because it's clear for both the reporter and maintainer if the behaviour matches the spec.
a simpler spec is more likely to be correct.  There was a table posted that included at least one typo, which is one way for errors to enter. A subtle error being specified makes everything harder.
there was an argument that we should reduce to maximise the information available, but if the reductions are sound then it's impossible to gain information with a reduction.
(A & ~A) ==> Never is actually lossy wrt what is valid usage (every usage of Never is valid, but only provably valid usages of A or of ~A.). It may be nonsense, but that doesn't mean it's not useful.
many of the examples provided relate to practical rather than theoretical impossibilities.  E.g., int & str may be impossible in cpython, but may be possible in other implementations.   f(*args: Any, **kwargs: Any) - > Never: raise Exception() should be a valid substitute for any function as far as I can tell.
"practically impossible" subtypes may still be behaviourally possible utilising e.g. __isinsancecheck__ etc.
relatedly, it's not possible to prevent a library author providing impossible intersections, and it'd be preferable to be able to handle them gracefully.
I expect that unintentional Never intersections will be extremely uncommon in practice, and forcing type checkers into prescribed reductions without knowing the performance impact seems questionable.
because I need to deal with library code that may be under specified with types in my use case, and I have no control over the implementation, I'm often faced with being forced into gradual typing, potentially just because of cost.  I would much prefer if I could keep as much type information as possible, and using 'impossible' intersections provides a way for me to do so, as long as they behave simply and consistently in this case.
the completely pure, no gradual typing perspective is not representation of any of the code bases I have worked with, even with requirements for high quality types in internal code.  Limitations of  library types of the type checker means that I occasionally need to provide the type checker with Information it wasn't able to work out, or in some cases provide minor lies based on actual usage.  This is possible only when errors are contained to the problematic area, and thus solutions can be contained to the problematic area.

I don't like the idea of erroring on Never, because it feels akin to erroring in the empty sequence. It is not uncommon for Api authors to think that asking for an empty list should raise an error, but in practice it makes it more annoying to work with. The suggestion of erroring on never triggers my olfactory sense.

I just want to remark that erroring on Never actually facilitates the usage of empty containers. If instances of Never are not allowed to exist, then list[Never] matches with and only with the empty list.

there was an argument that we should reduce to maximise the information available, but if the reductions are sound then it's impossible to gain information with a reduction.

The reductions that "Added information" did so by bringing in a subtyping relation known by the type checkers. That's where the "extra" information came from, while also simplifying the form.
All the arguments about gradual code and type checker bugs are moot because we're talking about the specification for what the correct behavior is. The fact that you may need to lie for pragmatic reasons at times should not be a concern of the pep.

A simpler spec is less likely to be implemented incorrectly, and easier to raise bugs against when a type checker diverges, because it's clear for both the reporter and maintainer if the behaviour matches the spec.
a simpler spec is more likely to be correct. There was a table posted that included at least one typo, which is one way for errors to enter. A subtle error being specified makes everything harder.

Intersections are complex. Unions have a specification error #22 Start with what's correct, find ways to express simplicity after you have correctness, not before, or you're likely taking a shortcut that hasn't been proven correct.

Anyhow, best of luck, but I don't think this will be the group to do this correctly. The focus is on the wrong places, and I'm tired of having multiple forms of the same arguments.

There's two other issue with not handling impossible intersections at the point of the intersection here:

Not handling it at the point of the intersection would mean that typing.assert_never suddenly doesn't function properly in the body of a function taking an intersection.
Library code that itself builds on other libraries.

Example for the second one
# Not My Library:

class A:
    val1: int
    val2: int
    ...

    def some_method(self) -> int:
        ...

# Some wrapping

AMixinIterable:

    def __iter__(self) -> Iterator[int]:
        ... # implementation required, but not shown here

def do_something_common(A & AMixinIterable):
    ...

Lets say at the time, the library didn't want to add iteration to A, so someone wrapped A making it iterable and adding a convenience method for something relatively common that relied on this
If later down the line the upstream library decides to make A iterable, but instead of iterating integer values, they iterate pairs of names and integer values, the library that only ever wrapped behavior is broken, but only end users see the error, not the people maintaining this wrapper.

They should see the error if they have any tests. Also, as emphasized multiple times, no one is arguing that type-checkers cannot check this with an opt-in/opt-out strictness flag.

Can you please provide an example?

class A(Protocol):
    @staticmethod
    def foo(x: int) -> int:
        ...

class B(Protocol):
    def foo(self, x: int) -> str:
        ...

def bad_usage_should_be_detected(x: (A & B) | None):
    if x is None:
        return # This is fine
    else:
        tying.assert_never(x)  # A & B needs to be detected as Never due to being strictly incompatible.

This is a toy example, but one can reasonably conclude that this could arise more naturally and that we shouldn't ignore existing parts of the type system while designing this.

They should see the error if they have any tests. Also, as emphasized multiple times, no one is arguing that type-checkers cannot check this with an opt-in/opt-out strictness flag. Regarding

The problem is by making this opt-in, you have divergence potential between type checkers, and I just showed an example that meets the criteria Eric gave for this being library interface, and therefore not something which should diverge.

This is a toy example, but one can reasonably conclude that this could arise more naturally and that we shouldn't ignore existing parts of the type system while designing this.

Your example is begging the question...

Your example is begging the question...

No, it's literally demonstrating the issue.

There's also another reason intersection need to detect this if you still aren't convinced, decorators.
Decorators become more expressive with intersections, and we can do something where the decorator intersects the given type with a protocol by adding generated methods to a new constructed class with the same bases. If the incompatibility isn't detected, this becomes a way to violate LSP without it being detected by type checkers

Your example is begging the question...

No, it's literally demonstrating the issue.

It's literally presuming the conclusion:
tying.assert_never(x)  # A & B needs to be detected as Never due to being strictly incompatible.

What's needed is an example that start by assuming the contraposition, i.e. that A&B is generally just an abstract type that is completely uniquely determined by its subtyping rules, and shows that this leads to (non-benign) divergence either when a user tries to use library code that was checked using strict rules which checking non-strict themselves or vice versa.

The entire point of typing.assert_never is detecting when a type is no longer satisfiable due to exhausting the previously possible types. If A& B isn't be reduced to Never when A and B are mutually incompatible, this is broken by adding intersections. This doesn't need a fully fleshed-out example that adds intersections to make that point, the toy example + the fact that such intersections were already determined to be possible to arise in type-checking innards (hence not being able to ban Any from intersections because it could come in elsewhere) should be sufficient.
You also didn't address the point about a class decorator, which is much easier to demonstrate concretely.

class Comparable(Protocol):
    def __eq__(self, other) -> bool:  ...
    def __ne__(self, other) -> bool: ...
    def __.lt__(self, other) -> bool: ...
    # rest elided to not type this all out, all the comparison funcs though

def add_cmp_funcs(klass: type[T]) -> Type[T & Comparable]:
    """ add other comparison functions from `__eq__` and `__gt__`   """
    # implementation left out, see things like functools.total_ordering

If this isn't detected for incompatibility, you have situations like with ORMs where their comparison functions don't directly compare, they partake in query building. Classes such as those should be detected as incompatible.
Beyond this, there are other cases that may be less obviously an issue, such as a decorator that adds caching, but the name used for caching on the class is already taken.

What's needed is an example that start by assuming the contraposition, i.e. that A&B is generally just an abstract type that is completely uniquely determined by its subtyping rules, and shows that this leads to (non-benign) divergence either when a user tries to use library code that was checked using strict rules (warn at intersection of incompatible classes) while checking non-strict themselves or vice versa.

already given including how this type would end up exported to a user.

The example doesn't work for multiple reasons. I only responded to one aspect of it. Let's take it apart then.
First, I want to note that the example is incomplete and leave open multiple questions. For one, you write:

Lets say at the time, the library didn't want to add iteration to A, so someone wrapped A making it iterable and adding a convenience method for something relatively common that relied on this

Yet do_something_common is annotated as A & AMixinIterable instead of say WrappedA.
Secondly, it is unclear how then the iteration in do_something_common is performed. If, for instance, a helper function like iter_vals(x: A) -> Iterator[int] is used, there is no issue with A implementing a separate __iter__. On the other hand, if the library subclasses A as WrappedA, then when the other library updates A it will show up as a type-error within the body of WrappedA.
Finally, I want to emphasize that tests here does not mean that any other tools are needed. One can have completely static tests. Type-checking the tests/ directory is very common and useful because it validates that stuff that is supposed to be plugged together can in fact be plugged together.
If you still believe this example works, I'd ask you to provide a full-code variant.

Have you never dealt with a mix in before? The point here is to not prescribe the final class, only the minimum things it needs to satisfy

Finally, I want to emphasize that tests here does not mean that any other tools are needed. One can have completely static tests. Type-checking the tests/ directory is very common and useful because it validates that stuff that is supposed to be plugged together can in fact be plugged together.

Testing my tests for type issues doesn't make sense. While my code is fully typed under strict with no type ignores, many things tests need to do involve testing that appropriate errors are raised in specific misuse. Type checking this would create a lot of noise.
Change the mix in for a protocol and you get the same issue. Idk what isn't clear about that to you, your response isn't addressing the issues presented, so I can only assume a misunderstanding somewhere here.

Testing my tests for type issues doesn't make sense.

Of course it does. Tons of high profile packages do it. All of your functions may type check individually, but in tests one often checks directly or indirectly checks type-safe composability.

Idk what isn't clear about that to you, your response isn't addressing the issues presented, so I can only assume a misunderstanding somewhere here.

Your example is missing the function body and return type for do_something_common, which is relevant here. For example:
def do_something_common(x: A & Iterator[int]) -> list[int]:
    return list(A)

Would immediately raise an error if the library added __iter__(self) -> Iterator[tuple[str, int]] to A.
Look, there are exactly 2 options: Either, the function body of do_something_common contains any code that is incompatible with x.__iter__() yielding tuple[str, int] & int or there isn't.
In the first case, if the other library updates A you'd see the type error occurring in the function body. In the latter, the function remains type-safe.

Taking my response out of context, classy... The decision not to test tests was deliberate, and you decided to quote me leaving out a specified rationale. Why bother discussing if this is how it is going to go?

Your code as well as my code or any particular individual's code is irrelevant for this discussion. I was merely pointing out that many libraries type-check their tests, and for good reason. If you want to test misuses, there's it not TYPE_CHECKING or putting a type: ignore at the top of the tests-file that checks misuse.

The body of the function actually is irrelevant because stubs for things implemented in C exist and could do this.

Your code as well as my code or any particular individual's code is irrelevant for this discussion. I was merely pointing out that many libraries type-check their tests, and for good reason. If you want to test misuses, there's it not TYPE_CHECKING or putting a type: ignore at the top of the tests-file that checks misuse.

Misuse is one of many reasons. It just doesn't work the way you are suggesting in some environments, and unfortunately, I'm not legally allowed to share many motivating examples relating to my work, so I have to construct very basic examples with no relation to my work to participate here.

And you still haven't addressed why you think this shouldn't result in Never, only saying that other things should see an issue as well.

If we stop coming up with "but this might be hard to implement" and instead just focus on correctness, we can get to the point where we have a spec, and can then discuss the merits and challenges with those who maintain type checkers as part of accepting it. But we aren't even having that discussion, people are raising hypotheticals that are predicated on being incorrect. I don't know how we are supposed to productively continue this discussion without a hard refocusing on strict correctness while leaving the details of implementation to those implementing checks based on what is defined to be correct.

sigh I'd be willing to compromise to that language, but I think it has the library edge case mentioned before that may encourage downstream users to try and satisfy an unsatisfiable type via an ignore rather than raise the issue in the right place.

@randolf-scholz would you be amenable to that limited scope for when type checkers must determine if it is actually Never? If so, we need to create the rules for that, but it keeps it to places where that information is specifically requested, and if type checkers so more that is up to them.

Actually, @mikeshardmind this doesn't solve your decorator example. This needs detection in that case because the implementation of the decorator could be to construct a new class in c code not visible to type checking

Yep... Basically, it needs to always happen unless people think they can correctly exhaustively come up with every specific case it might matter

For the question of a decorator, if we have:
class A:
   def foo(self) -> A:
        return A()

class B:
    def foo(self) -> B:
        return B()

(They could also be protocols if we want to stick to structural cases)
I hope we can agree that A & B is not impossible.
But it seems like we can encounter the same error as if it was Never when creating a decorator:
def add_b_to_type(x: type[T]) -> type[T & B]:
    ... # Implementation goes here

reveal_type(add_b_to_type(A))

From a type perspective, everything seems fine
Now it's possible that I'm misunderstanding what would go into the implementation of decorators that add methods such as add_b_to_type, and it handles  clashing definitions recursively (or I guess errors, implying -> Never, which is a subtype of everything), but it feels like if there is a mechanism for doing so, that is provably correct to the type system, then that same mechanism should cover the impossible intersection case, and then I don't see why we should put more emphasis on the Never case than the, to my mind much more common, technically possible but kind of awkward and realistically unlikely case.
(But I don't think we should convert the "technically possible but kind of awkward and realistically unlikely case" to Never if there is any possibility of satisfying it, because it is a valid case, that someone could want).

the intersection needs to be checked for correctness

The intersection is always correct no?  It's just a question of whether it can be reduced, in particular to Never, which could be interesting in various ways.

The intersection is always correct, no? It's a question of whether it can be reduced, in particular to Never, which could be interesting in various ways.

Realistically, I view specifying a type that reduces to Never as incorrect as it means you have code that is impossible to reach correctly, and likely signals other issues. If only a portion of it reduces to Never and we reach that in a branch that errors out (typing.assert_never) it's a little different. We have a pragmatic case of that that results from distributivity in discord.
The thing about implementation potentially not being visible means the reduction to Never does need to happen in the intersection whether or not an annotation that reduces to Never ends up viewed as erroneous by type checking though, as we can't just defer that to "well, whoever calls it should run into it being impossible", that may not ever be visible.
def recreate_in_c(T) -> T & Comparable:
    # call into c-extension, create a new type in c code, etc
    return something_from_c

This isn't even outlandish, there are existing libraries that do things like this already, and the type system has special support for some things like this (See dataclass_transform) because the methods they use are often opaque to type checking.

Realistically, I view specifying a type that reduces to Never as incorrect as it means you have code that is impossible to reach correctly, and likely signals other issues. If only a portion of it reduces to Never and we reach that in a branch that errors out (typing.assert_never) it's a little different. We have a pragmatic case of that that results from distributivity in discord.

It is a controversial topic that uther people disagree with.  By trying to avoid charged terms like 'incorrect', we can focus on what behaviour is useful in what situation.
Similarly, in:

The thing about implementation potentially not being visible means the reduction to Never does need to happen in the intersection whether or not an annotation that reduces to Never ends up viewed as erroneous by type checking though,

It doesn't 'need' to do anything.  It needs to have certain behaviour if we want certain behaviour to happen.  Some of that behaviour is controversial, and taking it as a given is kind of antagonistic.
One example here is that to provide stubs for opaque implementations is a version of adding a type: ignore*, and some commenters have argued that we shouldn't have to reason, or influence decisions about desired behaviour from any use thereof.

In the return type here, if you pass a type that isn't compatible with Comparable, the intersection needs to be the cause of the error "Hey, you're trying to do something with Never here"
def augment_in_c(typ: type[T]) -> type[T & Comparable]:
    # call into c-extension, create a new type in c code, etc
    return something_from_c

This isn't even outlandish, there are existing libraries that do things like this already, and the type system has special support for some things like this (See dataclass_transform) because the methods they use are often opaque to type checking.

What if there's something that is compatible with Comparable, but has behaviour that's divergent?  E.g., if it returns a sub type of bool for the specified methods?  Are we confident in that case that the decorator does the right thing?  What if it doesn't, and just overrides the operators to a bool?  Wouldn't we like to know that too?

The thing about implementation potentially not being visible means the reduction to Never does need to happen in the intersection whether or not an annotation that reduces to Never ends up viewed as erroneous by type checking though,

It doesn't 'need' to do anything. It needs to have certain behaviour if we want certain behaviour to happen. Some of that behaviour is controversial, and taking it as a given is kind of antagonistic.

No, it quite literally needs to be checked for compatibility here. There is no other place to do so in such an example, and prior arguments were predicated on "but you'll know if it's incompatible when you create the actual object" (Assuming the implementation was visible to type checkers). If it isn't checked here, then it isn't checked at all despite being typed code.

What if there's something that is compatible with Comparable, but has behaviour that's divergent? E.g., if it returns a sub type of bool for the specified methods? Are we confident in that case that the decorator does the right thing? What if it doesn't, and just overrides the operators to a bool? Wouldn't we like to know that too?

If this is possible, then T & Comparable aren't incompatible, and it shouldn't be reduced to Never. However, this being possible depends on both T and Comparable being possible to reconcile.

Realistically, I view specifying a type that reduces to Never as incorrect as it means you have code that is impossible to reach correctly, and likely signals other issues. If only a portion of it reduces to Never and we reach that in a branch that errors out (typing.assert_never) it's a little different. We have a pragmatic case of that that results from distributivity in discord.

It is a controversial topic that uther people disagree with. By trying to avoid charged terms like 'incorrect', we can focus on what behaviour is useful in what situation.

We're talking about a specification for what is correct and what isn't. I'm not going to tiptoe around words here. If you try to call code that can't legally be called, something, somewhere is incorrect. If you try to use an instance that has a type of Never, something, somewhere, is incorrect. Nothing about that should be contentious, the very definition of Never includes is that it is an uninhabited and uninhabitable type.

No, it quite literally needs to be checked for compatibility here.

No, it quite literally doesn't.
There is nowhere else that it can be checked, and that is not the same thing.

The point of type-checking is that types are checked. Are you suggesting we should knowingly create a situation where a type isn't checked despite having the relevant information and mechanism to do so? If so, to what end?

@diabolo-dan

One example here is that to provide stubs for opaque implementations is a version of adding a type: ignore*, and some commenters have argued that we shouldn't have to reason, or influence decisions about desired behaviour from any use thereof.

actually, people said if the type ignore breaks the rules it was a problem. There was significant acceptance for the fact that not everything is possible to express in python currently.

No, it quite literally needs to be checked for compatibility here.

No, it quite literally doesn't.
There is nowhere else that it can be checked, and that is not the same thing.

The point of type-checking is that types are checked. Are you suggesting we should knowingly create a situation where a type isn't checked despite having the relevant information and mechanism to do so? If so, to what end?

Stubs and casts are not currently checked.  They are inputs that allow the checking of the code that uses them.

Additionally, this is an example that has the "contentious" intersection in the return type of a function. Whatever we decide here has to be consistent across type checkers, or we get divergent behavior issues for libraries, so we either need to mandate it is checked or it isn't.

Then let's mandate that it isn't.
A linter can still pick it up and warn about it, if it's important to people.

Stubs and casts are not currently checked. They are inputs that allow the checking of the code that uses them.

That isn't equivalent.

Then let's mandate that it isn't.

Let's Mandate it is. This is the safer option, and mandating it isn't by definition cuts off the ability for it to be checked within specification.

That isn't equivalent.
I'm confused, wasn't that exactly what you're example was? Stubs for a C based implementation?

Mandating the reductions based on available type information needs to be discussed with type checking maintainers, but we have a case that shows we either need to mandate it or mandate it isn't and a case that shows that mandating it isn't causes a loss of type safety. These reductions will need to happen anyway in the internals of typecheckers to work with typing.assert_never, so there should not be added complexity for this, only more things that need to use it.

I'm confused, wasn't that exactly what you're example was? Stubs for a C based implementation?

@diabolo-dan Not exactly. All the stuff in the code block is in a python file, there's extension code called to create the type elided on the line with the comment.
Such a transformation would be opaque in the same way existing code already is, and there is a precedent for this with dataclass_transform helping provide accurate type information even when type checkers do not have a means to understand the implementation. It would be opaque, but the addition of the interface represented by Comparable would be correct (not running into "well, you started by breaking the rules though")
Because the logic for this kind of reduction will already be needed for typing.assert_never as @DiscordLiz pointed out, I'm not arguing for any additional complexity in type checkers by arguing this, but this will probably have a runtime impact still as more things will need to have this reduction applied.

@mikeshardmind @diabolo-dan If the concern is impact on type checkers, I think we can claw back some of that runtime cost if we lean into what Eric said about it being an issue primarily for libraries with divergence.

If the intersection is part of an exported type or function signature in a module, reductions MUST be applied.
If the specific presence of a comparison with Never, reductions MUST be applied.
When determining if an object may be assigned to an intersection, if the object is of an unknown type, reductions MUST be applied first. If the type of the object is known, typecheckers MAY opt to instead check if the object is compatible with all operands of the intersection.

This should significantly limit the surface area for the full reductions to take place.

It would be opaque, but the addition of the interface represented by Comparable would be correct (not running into "well, you started by breaking the rules though")

Do you agree that that correctness must imply that it raises an exception if presented with an argument that would return an impossible type?
I think we can agree that there are a class of wrong behaviors that a reduction to never would resolve. I think we disagree on:

how likely these cases are
how special these cases are
how easy these cases are to mitigate in other ways
the cost of introducing them

@diabolo-dan I've gone through your initial question below, as well as my perspective on each of your bullet points. I hope this can get us closer to something we can put into language for a first round PEP draft.

It would be opaque, but the addition of the interface represented by Comparable would be correct (not running into "well, you started by breaking the rules though")

Do you agree that that correctness must imply that it raises an exception if presented with an argument that would return an impossible type?

Starting here, not in the type system, no. In the type system, it should reduce to Never in that case, indicating the misuse.
At runtime, correct implementations could also detect the incompatibility, but if they are documented to take something specific, it's not necessarily their responsibility to error if it is misused. (see prior discussion about reasons libraries rely on documentation for this with performance, rather than checking each time). Runtime checks are expensive. We don't have this happening at compile time like compiled static languages, anything checked like this at runtime has an associated cost that gets paid at each call. I'm willing to have CI take 10x as long to gain 1% in production speed. The object returned in the case of a function not erroring, but documented as misuse is in error, even without an exception raised, so I view this as an "ideal" when it comes to codebases that are fully typed. This lack of runtime exception is less viable absent stronger tests (See below) and good typing though.

I think we can agree that there are a class of wrong behaviors that a reduction to never would resolve.

Yeah, I don't think anyone has said a reduction to Never isn't useful, thankfully. We have enough common ground to not be that far apart, it's just how to determine when it must happen, when it may happen, and when it must not happen.

I think we disagree on:

how likely these cases are

Well, decorators that modify classes are pretty common, and Mixins are an original motivating case for the PEP. I think combinations of and modifications to concrete types that are specifically intended as being combined of used to augment, modify, etc are likely one of two of the most common cases these will be used for, the other being intersections of protocols in the same way multiple trait bounds are specified in rust for composing structural compatibility.

how special these cases are

I'm not sure there's anything special here other than that in this set of circumstances, the intersection is the only point where it can be detected should we add intersections. To me, that feels like it becomes our responsibility because we're adding something and creating a blindspot in the type system, while aware that we are doing so and that we don't have to.

how easy these cases are to mitigate in other ways

I would hope that anyone writing opaque code that modifies classes also has tests and good errors when passing invalid things, but in this case it's also partially about the person using it who may not be the author of said code having a good experience with typing. Typing gets more useful the larger the community buy-in on it is (more contributors to gradually type things that aren't typed, and discover things that aren't yet expressible that they want), and part of that is ensuring a smooth experience when users use typed libraries.

the cost of introducing them

Well, the reductions are definitely needed already for typing.assert_never, if this is the primary hangup on this, why don't we start by proposing it as mandated, either always or in the limited set of cases @DiscordLiz proposed above that limit it to where it seemingly would have impact beyond a single code base, but come to the table with the PEP discussion ready to work with those maintaining type checkers to determine how costly this actually is and seeing if it is viable, needs adjustment of scope rather than preemptively assuming it will be too much.

Are we still discussion whenever some Intersections should resolve to Never by Definition?
And the two related questions:

Does this PEP need to define it or should we leave it to type checkers to decide which intersections resolve to Never?
If yes, what kind of rules *need to be included in the PEP?

Sorry I am really lost in where the discussion went and unable to conclude stuff.
Could we come back to the main topic and create discussions for the other more broad stuff?

@CarliJoy We have 1 case for sure where we can't leave it to type checkers and need to mandate resolution to Never because of the existence of typing.assert_never If it is left up to type checkers and not mandated for this case, then we aren't mandating compatibility with existing type system features.
The course of the discussion since finding that case is drawing the lines on where else that mandate should exist, but the fact that we have a case where it is clearly needed means we aren't adding extra complexity to require it elsewhere, only potentially extra runtime for it to be run in more places.

@CarliJoy Further summarizing the competing ideas that have been put here:
(Me): Mandate it always in the first PEP draft, but be open to discussing this with type-checking maintainers
(@DiscordLiz): Mandate it in cases where it can effect code outside of the module it is in
(Several others, at least at last stated): Don't mandate it at all*
(@diabolo-dan): Mandate that it isn't reduced
* This one has other problems for type-checking divergence that no other option has

@CarliJoy We have 1 case for sure where we can't leave it to type checkers and need to mandate resolution to Never because of the existence of typing.assert_never If it is left up to type checkers and not mandated for this case, then we aren't mandating compatibility with existing type system features.

That is very much still under discussion.

Is it? I don't think anyone came up with a counter to this point at all when it was presented.

Is it? I don't think anyone came up with a counter to this point at all when it was presented.

@randolf-scholz was countering this point as recently as 2 days ago.  It seems premature to believe that he's stopped posting because he's been persuaded to agree with you, rather than hasn't had time to continue for now.
I haven't personally addressed it (yet) because I have limited time (and emotional energy), and I think that we probably need to make progress on other parts of the discussion first before we can fruitful progress there.

was countering this point as recently as 2 days ago. It seems premature to believe that he's stopped posting because he's been persuaded to agree with you, rather than hasn't had time to continue for now.

I don't see anything he said as countering it. He said an example was begging the question when it wasn't; The example was specifically demonstrating how typing.assert_never would no longer function as documented and purposed if we don't mandate this. After this was pointed out, he moved on to other things without addressing that point.

I haven't personally addressed it (yet) because I have limited time (and emotional energy), and I think that we probably need to make progress on other parts of the discussion first before we can fruitful progress there.

Any direction in particular? Seriously, it feels like we're going in circles and not actually wrapping up anything, and I actually think many other open questions are predicated on whether or not we are mandating reductions, and if so, in what cases. This has specific effects on if #17 remains needed. Specifically, #17 is no longer needed, only nice, if incompatible intersections are detected in the intersection themselves.

I don't see anything he said as countering it. He said an example was begging the question when it wasn't; The example was specifically demonstrating how typing.assert_never would no longer function as documented and purposed if we don't mandate this. After this was pointed out, he moved on to other things without addressing that point.

I stand by this point, because the whole example was built on the presumption that A&B must be set equal to Never, when my position is that A&B should be defined purely by its subtyping rules. This is crucial when we take serious the reality that nominal subtypes of A and B can exist even when A and B are incompatible.
The reasoning that we must need for type hinting code with C-implementation I find unconvincing, since, in that case, if the library that provides A makes any changes of A's interface the code is plausibly no longer type-safe, regardless of whether or not A is intersected with anything in the function type-hint.
The discussions here are straining and take a lot of time, I would also propose to instead focus on other issues and start writing a rough draft. Each party can independently add a proposal regarding the issue of incompatible intersections, and we should try to get some external opinion on that matter and also check what other languages like TypeScript do about it.

I stand by this point, because the whole example was built on the presumption that A&B must be set equal to Never, when my position is that A&B should be defined purely by its subtyping rules. This is crucial when we take serious the reality that nominal subtypes of A and B can exist even when A and B are incompatible.

Which then breaks use of typing.assert_never, something which still hasn't been addressed. Saying "Well A&B should just be handled by it's subtyping rules" isn't useful in the context of this issue. typing.assert_never is a specific request for "is this type no longer inhabitable?" Never can always be used in place of a type, but that isn't what assert_never is asking. Assert_never is used to assert that code based on the exhaustion of valid types (uninhabitabile, is only Never) and therefore unreachable
See the documentation on this for details, but the relevant line:

For a call to assert_never to pass type checking, the inferred type of the argument passed in must be the bottom type, Never, and nothing else.

Nobody has actually said anything that squares this issue or outright says they are fine breaking typing.assert_never.

The discussions here are straining and take a lot of time, I would also propose to instead focus on other issues and continue writing a rough draft. Each party can independently add a proposal regarding the issue of incompatible intersections, and we should try to get some external opinion on that matter and also check what other languages like TypeScript do about it.

If people would stop breaking the existing rules we might take a lot less time. How much time has been spent by people still trying to say that they can create a class that breaks the rules of static typing and then use that in an example? Can we start with getting everyone on the same page about what is and isn't correct with the existing typing rules so we stop wasting time on this?
You're still doing it even now after it's been pointed out:

I stand by this point, because the whole example was built on the presumption that A&B must be set equal to Never, when my position is that A&B should be defined purely by its subtyping rules. This is crucial when we take serious the reality that nominal subtypes of A and B can exist even when A and B are incompatible.

@randolf-scholz I believe mypy is incorrect about allowing this as a subtype, and I'll be filling an issue later. There's non-obvious conflicts between LSP and strictly structural subtyping which have not been specified since the addition of Never as something which can be used in more places directly than just a return, and static typing currently is supposed to enforce multiple concepts of typing, not just structural.
However, even if this is correct, all you've shown is that you're "Solving" an incompatibility by reducing to Never, which at some point in an intersection may also be the only correct way to interpret it, and have not stated why we should not check if this is the only available solution when people are explicitly asking for "is there any possible other type left" with typing.assert_never

It's also worth noting Nothing isn't a subtype of all other types and treating it as such is incorrect. http://bit.ly/python-subtyping
the bottom type in a type system is just a way to indicate that a type specification is uninhabited.

@randolf-scholz
Hmm interesting example.
If change Never to anything else MyPy will complain

main.py:7: error: Incompatible types in assignment (expression has type "int", base class "A" defined the type as "Callable[[A, int], None]")  [assignment]

I feel like the people with proper background on the formal theory need to discuss some flaws within the existing Python typing system first before we can discuss further here.
So lets wait for this issue to settle.
I also would highly recommend that we base our PEP on formal theory. It seems that it was neglected quite a lot in the past which leads to inconsistencies. I rather not want to create PEP that increases them.
Of course being a dynamic language, you can do everything that violates the LSP principle. The goal of introducing formal typing to your code base is that this is actually not happening.
I don't see a real life use case in which we need to allow/consider behaviour that brakes LSP. This would introduce problems on so many other fronts...
The only reason why type checkers can determine LSP incomptible subclassing is because they know that order matters and the last definition is picked.
But as want and need Intersections to be independent of order this can't be done here.
Consider
from typing import Never, Any, reveal_type

class A:
    def foo(self, x: int) -> None: ...

class B:
    foo: int

def foo(val: Any) -> None:
    reveal_type(val)
    if isinstance(val, A) and isinstance(val, B):
        reveal_type(val)  # should be A&B -> currently not printed at all
        reveal_type(val.foo)  # should be never ?  -> currently not printed all

Mypy Play
The isinstance check is fulfilled in runtime by both C(A,B) and C(B,A) but the results differ for both. So it is impossible for a type checker to determine the result, therefore it only can raise an error here.
So I don't see any reason why we should consider this in this PEP.
@DiscordLiz and @mikeshardmind I really have no good understanding of formal typing theory, bottom and top types etc.
But if we say val.foo evaluates to Never, it seems logical to me, that if we define a
class C(A,B):
    foo: Never

is valid, because it is actually the result that would expect from A&B. Probably missing something here...
If you have time and energy, could you explain for a dummy like me why this logic is flawed?

@CarliJoy This is not surprising that your example errors, since int is not a subtype of Callable[[A, int], None].
The reason nothing is printed for the last reveal_type is because mypy deems that A and B are incompatible, so the code after the if-clause becomes unreachable, and reveal_type within unreachable sections are ignored. (mypy-play with --warn-unreachable).
Now, when we look in the type hierarchy, we have: Never <: Callable[..., Never] <: Callable[[T1, ..., Tn], R], for any types Tₖ and R. So for instance, it would be considered type safe to have
# Example ①
class A:
    def foo(self, x: int) -> None: ...

class B:
    def foo(self, x: int) -> Never: raise NotImplementedError

With this, no unreachable errors are emitted (mypy-play). However, regarding LSP, there are versions of LSP that the B above violates, in particular (LSP-exception):

New exceptions cannot be thrown by the methods in the subtype, except if they are subtypes of exceptions thrown by the methods of the supertype. (wikipedia)

The point I am making is that, apparently, the above is not part of the python typing ecosystem. Therefore, if we accept examples ① as valid type-safe subtyping, then it would have to accept that example ② is valid, type-safe subtyping.
# example ②
class A:
    @property
    def foo(self) -> int: return 0

class B:
    @property
    def foo(self) -> Never: raise NotImplementedError

and, as a final logical conclusion also example ③
# example ③
class A:
    def foo(self) -> int: return 0

class B:
    foo: Never

    def __getattribute__(self, key):
        if key == "foo":
            raise NotImplementedError
        return super().__getattribute__(key)

The reason is the following interpretation: If we define / annotate A.foo as something, say Callable[[int], None], then this defines a contract that looking up the attribute 'foo' of A produces an object of that type. Ergo, the following should be considered quasi equivalent:
# example ④
class A:
    foo: T

class A:
     @overload
     def __getattribute__(self, key: Literal["foo"]) -> T: ...  # promise that getattr(A, "foo") yields T.
     @overload
     def __getattribute__(self, key: str) -> Any: ...  # actual signature of object.__getattribute__

After all, the interpreter converts A.foo to a __getattribute__ lookup. But since Callable[Literal["foo"], Never] <: Callable[Literal["foo"], T] it appears that the logical consequence of accepting ① is that we also have to accept ② and ③.
Notably, this means that subclasses can choose to for example raise NotImplementedError instead of actually implementing a given interface. What type-checking still guarantees that the code will not raise any TypeError. Whetehr LSP is violated depends on what variant of LSP python typing tries to adhere to. Example ① indicates that (LSP-exception) is not part of it.

        reveal_type(val.foo)  # should be never ?  -> currently not printed all

I would argue it should be
int & Callable[[int], None]*

Technically this should be an anonymous protocol callable that matches the parameter types.

This is implementable in python:
class CallableInt(int):
    def __call__(self, x: int) -> None: ...

It's relatively unlikely that this is what was intended by the user, but it's not impossible, so a type checker shouldn't really be considering it unreachable.

One possible resolution: Behavioral LSP states that

Preconditions cannot be strengthened in the subtype.
Postconditions cannot be weakened in the subtype.

For functions, the contra-variance of arguments and co-variance of return types can be equivalently described as a set of pre-conditions and post-conditions. In particular, the covariance of the return type of Callable[..., R] is equivalent to the post-condition isinstance(return_value, R).
However, when we try to substitute Never for R there is a problem: the equivalence to a post-condition is no longer true, since  Never is supposed to be uninhabited (no instances of the type can exists). Therefore, the post-condition must fail.
This suggests one could consider a modified subtyping rule for functions:
Callable[...., R] <: Callable[..., S] if and only if either R==S==Never or Never ≨ R <: S.
I.e. if S≠Never we assume subtyping includes the post-condition and if S=Never it doesn't. This is a weak version of (LSP-exception) that forbids functions to unconditionally raise if their ancestor didn't. It would make example ① void, and, consequently, the whole argumentative chain from ① - ④ would fall apart. In particular, this would guarantee that __getattribute__(self, "some_literal_string") is not allowed to raise unconditionally if the parent didn't.
@DiscordLiz @mikeshardmind What do you think about this?

@randolf-scholz I think this is at the crux of the issue, but resolving that Never isn't a subtype of other types over in the linked typing issue leads to the same result, so you may want to add your details about how Never currently interacts with that.
It's worth noting that the set-theoretical definition being argued over in that thread is more general, but reaches the exact same conclusion of the limited modified subtyping rule you have there

@CarliJoy I think @DiscordLiz has provided a much clearer explanation of why even though A.foo & B.foo = Never, that doesn't mean C.foo can be defined to depend on Never over here
Some code to go with the prose she wrote:
int # singular static type
class A: ...  # singular static type
class B: ... # also a singular static type
ABAlias = A & B  # *also* a singular static type
Any  # This is the top type, and could be anything. This is not a singular type.
Never  # This is the bottom type, and can't be anything.

class SomeClass:
    foo: ABAlias  # This is a type specification, spelled with a singular type, but this is not a singular type!
    # As an annotation, this is the set of all potential types which are also A & B
    # and of which until further inference happens, is only safe to use what is provided by A&B.
    # Never doesn't provide A&B, so allowing this would violate LSP, even if Never was possible to exist!

def x() -> Never:  # Never isn't a singular type, it's the absence of a type being returned at all!
def y(foo: Never):  # Because There are no types which are never, this code isn't callable.

@randolf-scholz I think you hit the nail right on the head for the current issues with Never and LSP. This is a good formulation and good example of the desirable properties of LSP that are broken with the currently accepted definitions. My only qualm with layering on an exception instead of changing the definition, is that it appears to me that they have the same effects on all currently valid code. With this being the case, changing the rules to match those of the definitions which don't have the bottom type participate in subtyping freely gives us what is correct in more things which could be added to python later, as there are other features of type systems which are provably correct with those definitions, including rules for how they compose, that we can freely take in the future as they are proven already if we take the definition for the bottom type from the set-theretic view.
@CarliJoy It's basically that if a type relies on the existence of Never (needs an instance of Never to exist for it to exist), the type itself can't exist. I think we need to wait on the outcome of the wider typing discussion on Never, because a definitive statement there could remove this from being the concern of this PEP or not depending on how strongly worded the definitive statement is.
And @CarliJoy following up on @mikeshardmind's above example there's also A | B, which is a set of static types. In an annotation, the annotation allows the set of all possible types that can claim to be members of {A, B} by substitutability, which is a possibly wider set of types defined by a subtyping relation to a set of types. I believe you [Michael] were aware of this given your wording in the discussion in python/typing, but it's worth mentioning for completeness.

Thank you @DiscordLiz and @mikeshardmind . I understand it now a bit better.

that forbids to substitute a function with another function that unconditionally raises if the original didn't.

I also don't see what this has to do with LSP-exception since you don't know whether the superclass method raised the exception that the child class method is unconditionally raising.   I also don't see why there's anything wrong with subclasses raising unconditionally where their superclasses don't.  That already happens in ordinary code.
Is there any progress towards resolving the top level topic, which is "should reduction to never be mandated?"
Yes, if you don't mandate reduction, then assert_never won't do what you want it to.  Is there any evidence that many people will use it to test whether two interfaces are entirely compatible?  What seems more like is that people will inherit from two interfaces and write tests for the various functions, and in those tests, it will come up that there are type errors.  That is tested without mandated reduction.
I think ultimately, if you want to mandate this behaviour, then given that there are significant runtime and implementation costs, those will have to be justified with real world examples of bugs that would be caught by not reducing.

@NeilGirdhar

Yes, if you don't mandate reduction, then assert_never won't do what you want it to. Is there any evidence that many people will use it to test whether two interfaces are entirely compatible? What seems more like is that people will inherit from two interfaces and write tests for the various functions, and in those tests, it will come up that there are type errors. That is tested without mandated reduction.

It doesn't actually matter if we think they will or not. It's been confirmed that if intersections get added, they may end up in inference inside of type checker internals. We can't build this to be knowingly incompatible with other typing features that are supposed to work everywhere, especially with this being the only one of those with actual runtime behavior associated. assert_never is not for writing tests, it's for exhaustive matching against types in runtime code, and getting the type checker to confirm you actually exhausted all possible types in your handling. Getting this wrong has runtime impact as it causes assertion errors.
However

Is there any progress towards resolving the top level topic, which is "should reduction to never be mandated?"

Somewhat, and related to the above, this and #17 are both pending discussion here https://github.com/python/typing/issues/1458
There are 5 outcomes for that that I can forsee, and 3 of them leave us able to restrict mandating when intersections need to be resolved from "a lot of places" to "only when the existence of Never is specifically checked for" (Which is currently only typing.assert_never) and remove the need for Not as a requirement, and instead turn it into a nice addition. 1 of the remaining 2 options also makes the rules for Not immediately obvious, and therefore non-expensive, both in terms of PEP language and type implementation.
@DiscordLiz Also came up with a slightly broader set than this which would be needed in the remaining 1 case [here](Mandate it in cases where it can effect code outside of the module it is in)
We're quite close to being able to close much of the controversial issues with intersections and focus on picking how much needs mandating (And presenting good arguments for it) based on clearing up a couple of foundational details where some behaviors aren't well defined in python PEPs

I think ultimately, if you want to mandate this behaviour, then given that there are significant runtime and implementation costs, those will have to be justified with real world examples of bugs that would be caught by not reducing—in order to be convincing to the people reviewing the PEP.

Will do, and I'm making a conscious effort to make sure we mandate the bare minimum actually necessary in light of these costs., as well as opportunity costs where this interacts with potential future features. If it ends up the assert_never case is the only case, type checkers will almost never encounter it and can defer the reduction until reaching an intersection passed to assert_never, rather than needing to reduce it eagerly. This makes the cost directly proportional to the number of places user code specifically is asserting that something is Never and that the type checker should check this is true.

We're quite close to being able to close much of the controversial issues with intersections and focus on picking how much needs mandating (And presenting good arguments for it) based on clearing up a couple of foundational details where some behaviors aren't well defined in python PEPs