Any can be considered a type that has all values and all methods. Combined with the definition of subtyping above, this places Any partially at the top (it has all values) and bottom (it has all methods) of the type hierarchy. Contrast this to object – it is not consistent with most types (e.g. you can’t use an object() instance where an int is expected). IOW both Any and object mean “any type is allowed” when used to annotate an argument, but only Any can be passed no matter what type is expected (in essence, Any declares a fallback to dynamic typing and shuts up complaints from the static checker).

@erictraut I appreciate the focused feedback across multiple specific points.

If you're considering writing a PEP on this topic, you may want to leverage the work he has already done. He may be interested in working with you on such an endeavor. If you think that a PEP is needed to clarify the meaning of Any, then it would be good for it to be written prior to (or at least in parallel with) the PEP for intersections.

I've started writing it and will reach out at a later date. I've seen some of the in-progress work you're talking about, and while I largely agree with him, on Any, I disagree so it's definitely a discussion I'd like to have with him. I think in parallel is more appropriate than holding up the PEP, as the approach I believe to be more robust is defining Any is to define it as a special construct outside the type system, and modeling how we want it to behave to best "Fit in" as naturally as possible while addressing the needs of gradual typing. I don't think prior would be necessary, treating Any as more of a codified exception would not change what is a pragmatic outcome for the handling of Any in intersections, only the definitions we use to discuss it, and the definitions I have in mind are not dissimilar to the ones we currently have or the ones which other efforts have come up with. It is more that merely setting Any outside the type system as special allows for consistent logic for most other cases.

For example, if you want to mandate reducibility for intersections with Any, then you should also mandate it for unions.

The logic for reducing Any from an Intersection would be different from doing so from a Union. I can't argue removal from a Union, but can for an intersection, and it comes down to "what is the identity element for this operation?" This line of logic corresponds to removing Never from Unions, which is something type checkers currently do, and removing object from Intersections, which I don't think was controversial. Any being more complicated seems a good reason to keep it on the surface, but does Any function as both a top type and a bottom type in an intersection, or can we consider it functioning more like object does, and say that removal is consistent with the removal of Never from Unions, but partially limiting behavior?
Keeping Any has sharp edges that I do not see as having value, which leads me to...

That's why I continue to question whether this capability is sufficiently motivated at this time. On the other hand, there's clearly some passion for this feature among this group, and that's good to see.

My motivations would prefer Intersection not be added if we can't resolve some of these issues, but I think this leaves an unfortunate gap in the protocol-based and mixin cases that were at the very origin of this. If we reach a conclusion that now is not the right time to add an intersection, then in the absence of a full intersection, I would argue that there should still be a Merge (or some other name) construct that can merge protocols with disjoint interfaces. Should an intersection be added later, that very specific case should be identical for whatever rules we later agree on for Intersections, but this would help with one of the largest use-cases currently motivating the feature, and would closely mirror Rust's traits in terms of structural typing.

My personal perspective on this comes from primarily fully typed code, that still needs to use library code which may not always be fully typed. I have gone through the gradual typing process on multiple code bases, over 500k lines in total, and found that outside of discovering things that should just be generic over many possible types, the most efficient path towards typing was to start with the removal of Any and work on everything that then causes, then do it again with the next Any, and so on. Leaking Any in unexpected ways, especially if there were regressions in what was typed, was a big challenge when working with other teams as we worked on this, and places where it could happen caused more problems than code we knew was untyped still, so I'm quite negative on "unexpected" and even "unintuitive" Any because I've been through that with simpler cases before.

In reply to @ippeiukai's point about mandated vs. optional aspects of the type system...
There's a principle I like to use when deciding whether a typing feature should be spec'ed or left as a choice for each type checker. I ask myself whether the feature is needed to describe the interface of a module or whether it's used only to validate the code that comprises the implementation of a module.
Library authors and stub maintainers need to be able to describe an interface in a way that is treated consistently by all type checkers. By contrast, developers typically pick one type checker to run on their  implementation. (@ippeiukai, you mentioned that you use both mypy and pyright, but I suspect you're in a small minority.)
Type narrowing and type inference behaviors fall entirely within the implementation bucket, so I think it's justifiable for these behaviors to differ slightly between type checkers. By contrast, type consistency rules are important for enforcing an interface in a consistent manner, so it's important for all type checkers to use the same rules here. That's where specifications play an important role.
If you agree with my reasoning, then you'll see why it's important to specify the behavior of T & Any with regard to type consistency and attribute access.

I'll try to keep things focused too, and avoid restoking arguments and just stick to what we can agree on and what we need to decide here.
If forbidding Any from intersections is untenable from the perspective of type checkers, and the goal is the rules remain consistent with the rules for Union, I think there are only two options left to consider.
Any & T -> T
Consistent* with the rules for Union. I believe this is fine for typed code, but makes intersection less useful for gradual typing users.
* To the extent that we view Any as having the function of the top type in this context. I believe this is a good interpretation for the context, but we do need to consider if it is arguable that Any is acting in capacity as the bottom type here too.
Any & T -> Any
I do not think this would not be consistent with the equivalent rules for Union.
Any & T irreducible
If we go this route, determining that the Any is more than the top type here, then I agree with @mikeshardmind that we need good rules for resolving the type of the attributes of this intersection in an unsurprising manner. If it's just intersections all the way down, we really have Any & T -> Any in a disguise. So a potentially consistent option is equivalent to an inconsistent one. This may be a good place to discuss pragmatic exceptions based in likely intent like what @randolf-scholz suggested here but without the potential configuration flag.
If it's intersections all the way down, I would not support Intersections being added.

IMHO there is a consistent way to get Any & T - > T by thinking of Any not as a type, but more like NaN.
NaN * x = NaN = NaN / x

And that could be true for Any:
Any | x = Any = Any & x

I'm not convinced that this is preferable to e.g. not reducing, but it seems both consistent and simple to me.
It is of course annoying to deal with Any leaking into typed code, but that's already the case, and I'm not convinced collapsing the intersection makes that meaningfully worse.  Mypy at least offers some options to help with this (notably --disallow-untyped-calls picks up on non explicit Any at least).  But perhaps a stricter option which treats Any as object universally would help with users who don't appreciate gradual typing.

In another thread, I proposed the following general rules (slightly expanded and with simplified syntax). I think these are non-controversial.
Distributivity
A & (B | C) <=> (A & B) | (A & C)
A | (B & C) <=> (A | B) & (A | C)
Subtyping
C <: (A | B) if C <: A or C <: B
C <: (A & B) if C <: A and C :< B
(A | B) <: C if A <: C and B <: C
(A & B) <: C if A <: C or B <: C
Attribute type evaluation
(A | B).x:

Invalid if x is missing from either A or B
(A.x | B.x) if x is present on A and B

(A & B).x:

Invalid if x is missing from both A and B
A.x if x is present on A but not B
B.x if x is present on B but not A
(A.x & B.x) if x is present on A and B

Now, let's naively replace A with Any in the above rules and see what happens.
Distributivity
Simple replacement works fine and doesn't create any contradictions.
Subtyping
C <: (Any | B)
C <: (Any & B) if C <: B
(Any | B) <: C if B <: C
(Any & B) <: C
No surprises here. This looks good.
Attribute type evaluation
(Any | B).x:

Invalid if x is missing from B
(Any | B.x) if x is present on B

(Any & B).x:

Any if x is not present on B
(Any & B.x) if x is present on B

All of these rules are analogous between unions and intersections, all of them make logical sense, and they're all consistent with the goals of gradual typing.
Now, let's consider the alternative proposal where the union Any | T is not reduced but the intersection Any & T is reduced to T.
Distributivity
Any & (B | C) => (B | C)
(Any & B) | (Any & C) => (B | C)
Any | (B & C) => Any | (B & C)
(Any | B) & (Any | C) => (Any | B) & (Any | C)
Once again, simple replacement works fine and doesn't create any contradictions.
Subtyping
C <: (Any | B)
C <: (Any & B) if C :< B
(Any | B) <: C if B <: C
(Any & B) <: C
This produces the same results as above. No contradictions here.
Attribute type evaluation
(Any | B).x:

Invalid if x is missing from B
(Any | B.x) if x is present on B

(Any & B).x which reduces to B.x:

Invalid if x is missing from B
B.x if x is present on B

Here the rules produce asymmetric results between union and intersection, which is unintuitive. This rules also produce results that are inconsistent with the goals of gradual typing and the way that Any is defined in PEP 483.
From this analysis, I conclude that there are two solutions that produce consistent and logical results:

Both Any | T and Any & T reduce to Any.
Both Any | T and Any & T are irreducible.

The first of these options is how TypeScript works, but it's inconsistent with the way Python type checkers currently treat Any | T. We could decide to change that behavior (since it's not mandated in any spec), but doing so would be disruptive, and it would lead to more false negatives in mixed-type code.
I think that leaves us with option 2 as the best (and really only viable) option for Python.
@DiscordLiz, I'm not sure what you mean by "intersections all the way down". Can you clarify?

@DiscordLiz, I'm not sure what you mean by "intersections all the way down". Can you clarify?

Sure. If the rules for then resolving the interface of Any & T irreducibly includes Any at every step, rather than deferring to T when possible, it is no different than it being Any & T
With (Any & T).foo , if this is treated as Any.foo & T.foo (Which is fine for everything except Any) and not "check for the existence of an interface on the concrete type, and if not, use the behavior of Any", then it was shown earlier in the thread that this was no different than Any & T

To be more clear, the part you have above

(Any & B).x:

Any if x is not present on B
(Any & B.x) if x is present on B

This is not different than just collapsing Any & T to Any and being done with it for structural typing, which was the primary motivation for the pep between mixins and protocols. I'd find this having a negative impact, as it would make the point of even specifying T of having an intersection there pointless.
from where import UntypedLibraryType
from typing import Protocol

class Mine(Protocol):

    def foo(self, x: int, /) -> int:
        ...

def fn(x: UntypedLibraryType & Mine):
    x.foo(1)  # this is how I expect it to be used
    x.foo("blah")  # this works because UntypedLibraryType is Any, and I would intend this as an error

In terms of there being a compatible Any.foo there

class Annoyance:

    def foo(self, x: int | str, /) -> int:
        ...

Any is compatible with everything, so we're assuming an interface like this might exist, and trying to use Any in an intersection (from untyped code) washed away expectations.
At minimum, I'd want by specification that there needs to be a configurable error in type checkers for Any in an intersection if this is the behavior people want, because I'd rather be told I have Any from somewhere I didn't expect erasing my other expectations.

@erictraut

From this analysis, I conclude that there are two solutions that produce consistent and logical results:

Both Any | T and Any & T reduce to Any.
Both Any | T and Any & T are irreducible.

I reached a slightly different result than you did with an additional observation.
Any | T is irreducible and Any & T is inconsistent.
For all non-any types, an intersection between two types, A & B, when compared to either type alone, the intersection can only narrow the possible types which satisfy the intersection, and can only widen the possible interface of the type which satisfies it.
Any & T under these rules widens the possible types while widening the possible interface, and is inconsistent with this observation.
If we look at the corresponding rule for Any | T:
For all non-any types, a union between two types, A | B, when compared to either type alone, the intersection can only widen the possible types which satisfy the intersection, and can only narrow the possible interface of the type which satisfies it.
Any | T's behavior is consistent with this observation.
We've already ruled out excluding Any from an intersection, so I won't rehash that right now, but these rules are not consistent behaviorally with Any.

It seems that the issue here is really how Any interacts with the contravariance of the parameter argument. Since Callable[..., R] ≤ Callable[[T1, ..., Tn], R], this broadens the signature of any method to (*args: Any, **kwargs: any) when naively intersecting with Any.
Therefore, I think we need to discuss intersections of Any with generic classes, in particular what happens when we assume contravariance. Any & Callable[[X], Y] should be the most important example.

@mikeshardmind

Contradiction by Any & T

Any & T under these rules widens the possible types while widening the possible interface, and is inconsistent with this observation.

This only has a contradiction with protocols because for protocols subtyping is also the interface, but it is still a pretty important point. The subtyping rules being handled seperately works fine for concrete types.

@mikeshardmind, widening and narrowing are concepts that are based on subtyping rules and set theory. Any doesn't follow subtype relationships, so you cannot widen or narrow Any, nor does it make sense to say that Any is wider or narrower than another type. Does that make sense? Because of this, the contradictions you mention above don't seem sound to me.
Any is meant to represent "any type that can conservatively satisfy the rule that is being applied to it". I think PEP 483 is pretty clear on this, and this is how Any is treated throughout the type system and in type checker implementations today. If I understand you correctly, you would like to redefine what Any means. Is that correct? If so, then I think it's important for you to formally document your new proposed definition so others can comment on it and consider how it might affect the intersection feature. You mentioned that you're already working on this in the form of a draft PEP. Absent a new agreed-upon definition of Any, I think we need to stick with the current definition.
We all understand that the Any type can create "blind spots" in static type analysis and that Any has a tendency to propagate into other types during type evaluation. The introduction of intersections won't change that. As annoying as Any can be, ignoring its presence or dropping it from a type isn't sound. Doing so will create both false positives and false negatives. It will also lead to problems when attempting to compose type features (both existing and new).
@DiscordLiz, you said "I'd want by specification that there needs to be a configurable error in type checkers for Any in an intersection". I presume that you're referring specifically to the case where the left-hand side of a member access expression (lhs.rhs) evaluates to a type that includes an intersection with Any. I think it's a reasonable feature request for a type checker, but I'm not in favor of mandating it in the spec. Both mypy and pyright already have strict-mode features that flag dangerous uses of an implicit Any. I think these existing checks should satisfy your needs.

@erictraut

widening and narrowing are concepts that are based on subtyping rules and set theory. Any doesn't follow subtype relationships, so you cannot widen or narrow Any, nor does it make sense to say that Any is wider or narrower than another type. Does that make sense? Because of this, the contradictions you mention above don't seem sound to me.

While it makes sense that we could say it is ignored here because of this, I think this has negative effects on the outcome of Any & T to do so, I can almost guarantee that the majority of python users are not people who proactively read every pep, and read them only when a situation does not seem to make sense or when they otherwise want more information.
This is a behavioral inconsistency in this case, so even if the definitions allow for it, I suspect there will be people who find it surprising. I was intentional in calling it an inconsistency, and defining the inconsistency in relation to observed behavior and not directly based on subtyping, as I think such contradictions are also important for not having behavior "feel" surprising to users. It is my opinion that this outcome will be harder to teach and harder for people to have a natural intuitive instinct for.

Any is meant to represent "any type that can conservatively satisfy the rule that is being applied to it". I think PEP 483 is pretty clear on this, and this is how Any is treated throughout the type system and in type checker implementations today. If I understand you correctly, you would like to redefine what Any means. Is that correct? If so, then I think it's important for you to formally document your new proposed definition so others can comment on it and consider how it might affect the intersection feature. You mentioned that you're already working on this in the form of a draft PEP. Absent a new agreed-upon definition of Any, I think we need to stick with the current definition.

While I would like to redefine Any, my desire to redefine Any is only tangentially applicable here*, and I don't think that we need the definitions I'm working on for this here either. I would argue that (Any & T).foo essentially invalidating what is provided by T.foo by intersecting it with Any is not "conservatively satisfying" the rule, but over-eagerly looking for compatibility in a way that loses information.
Viewing Any from the perspective of gradual typing, it does not make sense to me to throw away type info. The idea of Any's infinitely compatible-ness doesn't seem pragmatic to its purpose of gradual typing in this instance.

* The updated definition for Any I'm writing for is as follows, the bolded part would be relevant.

Any is a special construct that exists outside the normal rules of the type system. It may be used to indicate entirely untyped objects and entirely unknown types. In the presence of more concrete type information in scope, the more concrete information should take precedence in the same scope All types are Any until information to the contrary exists.

I believe this is a more pragmatic definition for how Any should behave if the goal is gradual typing, and that outside of this current case with attributes and methods of Any & T, it already matches the current behavior of Any
It is still missing many important details about behavior, but that's the summation of purpose and intent.

@erictraut

[...]I think it's a reasonable feature request for a type checker, but I'm not in favor of mandating it in the spec. Both mypy and pyright already have strict-mode features that flag dangerous uses of an implicit Any. I think these existing checks should satisfy your needs.

Accurate to what I want, yes. I understand why you would not want to mandate this, and why you would want to have this be only for strict-modes, but I think there are too many conflicting expectations for what people want the behavior of Any & T to be to not mandate this. This isn't the only thread, we're just a handful of loud passionate people going in circles and refining a little bit each go around. The main thread for this has had many more users chime in on what they want, and some of it has included stating Any & T -> T as an expectation. The original typing peps also had that written. This isn't a "small" misunderstanding, but something that even the people defining Any this way thought should happen. Documentation can only go so far here, and I think this is an extreme enough case that there needs to be mandated proactivity about making sure users know where they may add in false-negatives with this, or it undermines the safety reasons for type checking.
I already use strict modes, so for my own use this is fine. If enough other people don't see it as being that likely to cause issues, then maybe such a mandate isn't needed. As long as I have a way to detect when it could happen without intent for my code, I can wash my hands of Any & T's actual behavior.
@mikeshardmind

While I would like to redefine Any, my desire to redefine Any is only tangentially applicable here*

No, I think if you intend to have that definition be considered, you need to rush that PEP and we need to evaluate Intersection and how it would look following it. Your proposed definition appears to have Any & T irreducible still, but resolve attributes differently. If I'm misunderstanding this, please let me know, but I don't want to comment more on that until you handle the other parts of redefining this. As I'd be fine with an outcome of it being implictly banned by warning in strict-modes for my own use cases.
I don't think your definition would be possible to accept if Intersection is added with the most recent proposed ruleset.

Hi everyone, I edit the top comment to make it easier for new people to participate.  Specifically, I linked as many arguments as I could.
There were a few arguments that I couldn't find comments for, so I removed them, but if you want to make a point that I removed please either comment which argument should be resurrected with a link to a comment that supports it, or make the argument yourself and we can link that comment.
I tried to summarize the arguments on one line if I could.  If I misrepresented something you said or you have a better summary, comment and I'll fix the summary.
I also tried to make the introduction more succinct and in particular moved the arguments from the introduction to the argument sections.

This was @CarliJoy's comment in the issue text.  I'm adding it here so that I can link to it in the issue.
We use this example:
class Before:
    before: str

T = TypeVar("T", bound=Before)

class Foo(Protocol):
    foo: str

def f[T](x: T) -> T & Foo:
    x.foo = "foo"
    return x

def g() -> Any:
    return Before()
reveal_type(f(g()))
reveal_type(g.before)

Any is valid assignment for T. But after passing it to f, the type checker stops me from using .before, which seems strange.

@NeilGirdhar We may have another choice:
Arguments in favour to allow both "An Intersection containing Any becomes Any" and "Treat T & Any as irreducible in general"
For the sake of argument, I want to suggest the spec to leave the choice between  "An Intersection containing Any becomes Any" and "Treat T & Any as irreducible in general" to the type checkers. This follows the idea of leaving things optional. https://github.com/CarliJoy/intersection_examples/issues/1#issuecomment-1657229031
@erictraut has already argued against this.
https://github.com/CarliJoy/intersection_examples/issues/1#issuecomment-1657233003
But, to that, @DiscordLiz has argued that not-reducing can be effectively same as reducing to Any.
https://github.com/CarliJoy/intersection_examples/issues/1#issuecomment-1657267240, https://github.com/CarliJoy/intersection_examples/issues/1#issuecomment-1657269163
I believe both accommodates gradual typing well, and I don't really mind type checkers behaving either way (I've personally been using TypeScript far longer than Python). When it comes to eliminating implicit Any from codebase, there are other options for that.

Argument for Any & T collapsing to Any: Any is also used to tell the type checker "Don't check this object, just ignore it", we would loose this meaning if Any disappears from an Intersection.

I was not the first one to argue this, but I believe this is the strongest argument against "Remove Any from Intersections".
I quote from PEP-483:

in essence, Any declares a fallback to dynamic typing and shuts up complaints from the static checker

(strangely, PEP-483 is also the pep that suggested Any would disappear from Intersection in the first place...)

@erictraut @mikeshardmind @ippeiukai @DiscordLiz @NeilGirdhar I opened https://github.com/CarliJoy/intersection_examples/issues/16 for a more focused discussion on what I believe being the showstopper of coming to an agreement here. (https://github.com/CarliJoy/intersection_examples/issues/1#issuecomment-1657275614)

@ippeiukai

@NeilGirdhar We may have another choice:
...allow both "An Intersection containing Any becomes Any" and "Treat T & Any as irreducible in general"

Thanks for bringing this up.  Mike says "I've started writing it and will reach out at a later date."  I think we should wait until he has written his proposal and then we can link that.  It will be confusing for someone coming to this thread to follow a link to a comment that says "work in progress".

I was not the first one to argue this, but I believe this is the strongest argument against "Remove Any from Intersections".

I can't find any earlier comments arguing this, so I'll link you making this argument if you don't mind.

I haven't read all this, but Any is neither a top type nor a bottom type wrt. subtyping.  Intersection with Any is dual to union with Any (where it's kept).
Informally, a type like A & Any is known to be statically an A (possibly a subtype) but it is also dynamically typed so you can invoke non-A methods on it as if it had type Any.

It seems like we're approaching consensus?  If so, can we resolve this issue to irreducible, or are we still debating?

Are we nearing consensus?  @mikeshardmind are you still working on an alternate proposal?
Once we agree on this, would it make sense to copy into the PEP: arguments from the "support" section of the accepted idea, and arguments from the "against" section of the rejected ideas?

@NeilGirdhar

are you still working on an alternate proposal?

Any attempt at this will reconcile itself with this pep at a later date, and I'm on the same page with not reducing Any from the intersection here which seems to be the outcome we all are at through different means and discussion.

So, we're currently in a call with some people in discord, there's a potential middle ground that helps with both safety and compatibility here, losing neither fully.
class B:
    def foo(self, t: int) -> int:
       ...
a: B & Any
a.foo(1) # int
a.bar # Any
a.foo("bar")  # disallowed, pragmatically, concretely known information taking precedence over gradual

class CompatFoo(Protocol):
    """ Never needs to exist in python code, can just describe a C library's behavior"""
    @overload
    def foo(self, t: int) -> int:
       ...
    @overload
    def foo(self, t: str) -> str:
       ...

b: B & Any & CompatFoo  # CompatFoo introduces the static information allowing this
b.foo("bar")  # str

That would mean that replacing a concrete type with Any could create type errors, which I find extremely confusing.

Was there an argument against irreducibility that needs to be added to the list?

irreducibility is no different from Any & T = Any, which erases known type information. It makes gradual typing bleed into typed code rather than adhere to the goal of gradually become more strongly typed as we cover more with annotations and the type system learns to express more.

I'm okay with the middle ground proposed. Gradual typing is super useful, but I don't want code to become less typed accidentally. If Any can really happen in an intersection from untyped code accidentally (why? how?)  and therefore can't be disallowed from intersections, then that means it can also accidentally make typed code less safe if it isn't reduced or treated as special.
if I write
from math_library import Polynomial  # provides a few things like .order, a property returning a numeric value
from gui_library import ImplementsGraphable

def foo(f: Integral & ImplementsGraphable):
    f.order("hmm")

I want this to fail. If this silently doesn't fail because ImplementsGraphable is for whatever reason Any, intersections have made things worse.
I just don't believe that people actually have real world cases of intentional use with Any, and that even if they do, those cases certainly shouldn't involve creating a class that is compatible with arbitrary other classes with static information magically, and that even if they do there, those cases aren't worth reducing safety for everyone else when there is a presented way to still express that "yes, this is compatible"

irreducibility is no different from Any & T = Any,

That's a confusing way to put it because Any & T = Any was a different proposal.  Yes, it's true that Any & T  being irreducible (in some cases) means that in those cases you will end up with a broader type.

I think this is a pragmatic fence that limits the issues in both directions.

Okay, then could you please  add a proposal as one of the options, and link to a comment with an explanation of your proposal and any arguments you have for it?

That's a confusing way to put it because Any & T = Any was a different proposal. Yes, it's true that Any & T being irreducible (in some cases) means that in those cases you end up with a broader type than you expect. This is analogous to how Any | T being irreducible (in some cases) means that in those cases you end up with a narrower type than you expect.

Yes, but in the case of a narrower interface, this is safe. In the case of a wider-than-intended interface in a situation that some people claim could happen without the writer's knowledge, it is not.
Gradual typing should mean that things become better typed with time, not that some typing features necessitate the elimination of all gradual typing before they are useful and safe to use. Theory and pragmatism conflict here, and I will defer to pragmatism in most cases where this is true so long as the rules for doing so are easy to reason about.

Okay, then could you please add a proposal as one of the options, and link to a comment with an explanation of your proposal and any arguments you have for it?

above has been edited.

It would be significantly more surprising and common to run into a case where a type is Any because it is untyped upstream...

I think it would really useful to find a real-world example where the last line here actually happens:
a: B & Any
a.foo(1) # int
a.bar # Any
a.foo("bar")

If so, we can look at fixing them with fewer special cases.   For example, by marking B.foo as "non-colliding" with anything different (so that (B & T).foo is identical to B.foo).  Or maybe there are other solutions.  But we don't really have a real-world example of a problem, and I think that special cases are going to cause significant problems in both the type checker implementation, in understandability, and in generic code.

I think that special cases are going to cause significant problems in the type checker implementation, in understandability, and in generic code.

Any is already a special case people have to reason about with extra steps. My goal with that proposition is to keep the special casing extremely minimized, and preserve the potential usefulness of intersections in both the fully typed and gradually typed cases. Changing it to be non-colliding makes it less useful in the fully typed case and breaks some of the use cases people want intersections for.
There's already a way to explain this in terms of teaching it, because of the change that was made without a PEP to allow subclassing Any to specify part of an interface. This would have the same behavior as that, and could arguably include saying this is the preferred expression of that idea.

A real world example are any libraries which aren't fully typed but partly typed.
A concrete example for a.foo("bar")  is quite hard to find as this is invalid code that is expected to fail on runtime…
Django might be a good example.  Django-stubs still have/had a long way to go but Mixin are quite common. So having a Mixin where a parameter is detected as Any is not unlikely.
I don't get

If so, we can look at fixing them with fewer special cases. For example, by marking B.foo as "non-colliding" with anything different (so that (B & T).foo is identical to B.foo).

The suggested idea is only a "special case" for Any which is special by definition. It is a very simple rule "Intersections with Any  are as concrete as possible otherwise Any".
I don't see any other option. What is a type checker expected to do in case we Any irreducible?
a: B & Any
a.foo(1) # int & Any ??
a.bar # Any
a.foo("bar") # Any but there is no matching function call, so just ignore B ?

That's much more confusing.

The suggested idea is only a "special case" for Any which is special by definition. It is a very simple rule "Intersections with Any are as concrete as possible otherwise Any".

Have you considered what's going to happen with type variables that are bound to Any, but take on particular values?
At the end of the day, this rule is an additional special case with a lot of interactions.  From what I've seen, special cases tend to cause more problems than they solve.  Especially unforeseen ones.
Any is special, but it has a formal meaning, and I think that whatever is chosen should be entirely consistent with that meaning—unless there's a really good reason for inconsistency.  We don't even have on motivating example.

So having a Mixin where a parameter is detected as Any is not unlikely.

Sounds like a good example.  Can you illustrate how client code would find the irreducible definition problematic, but Michael's "deferring" behavior would be an improvement?

So having a Mixin where a parameter is detected as Any is not unlikely.

Right, and I think users of that mixin should not have to add type-ignores or casts.  It should be permissive now, and then when those Anys are replaced with concrete types it should continue working.  With the deferring behavior, there may be type errors today that need to be ignored.
On the other hand, I understand the motivation to catch type errors today that you might not otherwise catch.  It is a trade-off.  I think we need more concrete examples illustrating that this is really necessary.

What is a type checker expected to do in case we Any irreducible?

Yes, you got it right.  In the irreducible case, the rule is:  A&B has the union of the interfaces of A and a B—just like A|B has the intersection of their interfaces.  And the union of an interface with an Any interface is an Any interface.

Any but there is no matching function call, so just ignore B ?  That's much more confusing.

It's exactly the same reason that you ignore B with unions (which is the dual of intersections):
def f(x: B | Any) -> None: ...

f(y)  # Ignores B!

What's especially odd is that there is no corresponding special case for unions. Are you also arguing that A | Any should have "the interace of A where A has attributes, and otherwise has other attributes set to Any"?

There's nothing odd about this in my opinion. The goal of gradual typing is to incrementally be able to type more, and to balance the needs of code that is not typed with that which is.
The case with union promotes this, the case with intersection does not. With A | Any it's only safe to use what's provided by A until checked which you have. With an intersection, you are claiming to have both interfaces. If Any can arise unintentionally here, then this is unintentionally always a potentially infinite interface and I'd rather we not add intersections than add a footgun because we didn't want to do the work of making pragmatic choices that put users over tools.

Have you considered what's going to happen with type variables that are bound to Any, but take on particular values?

Yes, this came about after significant discussion in discord. Something important to note is there's a worse issue by not doing this with TypeVars.
Any is compatible with a typevar with a concrete bound. There is no way to reverse this and say that "we just don't allow gradual types"
One of the examples that came up in the discussion is below:
from typing import TypeVar, Any

T = TypeVar("T", bound=object)

def foo(bar: T) -> T:
    return bar

baz: Any = ...
reveal_type(foo(baz))  # Type of "foo(baz)" is "Any"

This demonstrates that there's no way to opt out of Any to try and avoid the infinite interface problem, it really needs to be handled at the type system level. And even if we could hypothetically handle this by also changing the behavior of typevars, would you want it to be a trap to use intersections without explicitly adding bound=object?

I don't see why your exact same argument then doesn't apply to unions.  Why not argue that Any can infect unions and make it so that any object is passed into a function that accepts Any | T?  And therefore, by your own logic, union should be modified so that Any | T accepts only T to keep type-checking stricter and catch potential bugs.  Of course, that would cause all kinds of new type errors—just like your proposal would cause type errors for intersections with Any.

I don't see why your exact same argument then doesn't apply to unions.

Because Any | T doesn't allow more than T's interface. I explicitly spelled this out here with

The case with the union promotes this, the case with the intersection does not. With A | Any it's only safe to use what's provided by A until checking which you have. Because the natural behavior of a Union is that (pre-narrowing) the allowed interface gets smaller, there's no conflict with the goals of gradual typing and Any's existence in the first place.

but if you need an example
def foo(x: int | Any) -> None:
    x.this()  # Cannot access member "this" for type "int" Member "this" is unknown

While there is a symmetry between Any and Union, it is not the one you are arguing.

Because Any | T doesn't allow more than T's interface.

I know, but I mean on the other side.  Just as Any & T widens the interface, Any | T widens what parameter values can be passed.

it is not the one you are arguing.

I'm not talking about the interface of what's accessible within f, but rather the parents of what's passed to the union.  Since union is the dual of intersection, the logically consistent thing with your rule that—narrows the interface of an intersection—would be something that—narrows the children of what can be passed to a union.
And so, it would be something more like
def foo(x: int | Any) -> None: ...

foo(y)

And normally y can be anything, but if we follow your logic and make it consistent, then y  should be a child of some weird hybrid of int and Any, although I'm not sure what that hybrid would look like.

And normally y can be anything, but if we follow your logic and make it consistent, then y should be a child of some weird hybrid of int and Any, although I'm not sure what that hybrid would look like.

I think you're misunderstanding something here. Nothing about that example follows from the logic I have presented. I'm not proposing we restrict what goes in, but what is safely knowable about something. The two are different concepts. Nothing about
def foo(x: int | Any) -> None: ...

foo(y)

places a need to know what type y is outside of foo. Anything using x inside the body still needs to know what is safe to access on foo, and there's no issue here.

Nothing about that example follows from the logic I have presented. I'm not proposing we restrict what goes in, but what is safely knowable about something

That comes from the duality.  The kind of parameter that can be passsed into a union is a union of of the types.  The kind of interface that comes out of an intersection is the union of the intersections.  That's why the example looks like that.
Therefore, if you want to prevent Any from "infecting" intersections, then in my opinion, it's logically consistent to prevent it from infecting unions in a similar way.

The duality here breaks down because what is accepted as a type, and what is usable in the presence of a type have different effects on safety with partial unknowns.

That's a fair thing to argue, but I'm still not convinced.

should not degrade type information in the presence of other type information.

Yes, as much as possible.  But we already have that Any in X | Any "degrades type information" and that's exactly the same thing that's happening for intersections.

then it only exists as a trap

I don't see this as a "trap".  There are plenty of times that type checkers even stumble and types become "unknown" or Any.  This can happen in all kinds of ways.  Trying to make things stricter than they are can cause problems: as you pointed out, it can hide overloads that come from the Any side of the intersection.
But yes, it has the benefit that you get stricter types when the Any side  of the intersection doesn't collide with the other type on the used interface.  I wouldn't describe not getting these strict annotations as a "footgun" or a "trap".   It just means that type checking is less effective when you're using gradual typing.  Which is how things work today with unions.

Yes, as much as possible. But we already have that Any in X | Any "degrades type information" and that's exactly the same thing that's happening for intersections.

No, it isn't. X | Any doesn't introduce unsafety as using X | Any still requires checking the interface first. Please address This point, Its now been made 3 times and you keep trying to just say they are duals and that this also degrades information, but a concrete example was shown how it does not.

Any as an element in an intersection is not the dual of Any as an element in a Union anyhow. This is old news and was discussed in multiple contexts already.
object in an intersection and never in a union are each identity elements. Any is neither of these things, and there is not some true equivalence here. There isn't a universal property here.

But yes, it has the benefit that you get stricter types when the Any side of the intersection doesn't collide with the other type on the used interface. I wouldn't describe not getting these strict annotations as a "footgun" or a "trap". It just means that type checking is less effective when you're using gradual typing. Which is how things work today with unions.

It's a trap because the entire reason we're needing to do this is that the inability to ban Any from Intersections was because it could come in from anywhere If a type checker fails to get the type of one operand of an intersection, and falls back to Any, and we keep your view that it should be treated as that, This means all intersections are no better than Any, with silent failure built in.
This isn't how it works with unions AS WAS DEMONSTRATED already. Please actually read before responding to things and review the examples. They were presented after a lengthy discussion and consideration by those who were still working on making progress on this.

but a concrete example was shown how it does not.

I addressed your example.  You're misunderstanding the duality.
def f(x: X | Y): x.a
def g(x: X & Y): x.b

implies that:

f accepts variables y that are in the union of X and Y and a is in the intersection of their interfaces
g accepts variables y that are in the intersection of X and Y and b is in the union of their interfaces

And so your example is not the right application of this duality.   What you're showing is that this is not in the intersection of X and Y, which we know.  That is not my point.
My point is that:

since you want to make it so that where b would ordinarily be in the union of the interfaces, it should instead be in a restricted interface,
then you should also push for an equivalent restriction on which variables y are in the accepted by f.

Please watch your tone. It's not appropriate to suggest that people aren't reading what you're writing.

A concrete case annotating your own example for effects in scope was given as to how the difference between what goes into a function and what is used by a function have differing effects on type safety, yet you continue to insist that the two need to be duals of each other. You have not explained why from a theory standpoint, and appear to be latching onto a mental model of this that is incorrect. To that point, you've also ignored what another contributor pointed out that this has already been hashed out, and that these are not the duals you are presenting.
I can go get the various prior comments if you would prefer, but you continue to assert they are duals of each other, there are comments in this and other issues in this repository you have interacted with that show they are not or reference prior discussion you have taken a part in that show they are not.

was given as to how the difference between what goes into a function and what is used by a function have differing effects on type safety, yet you continue to insist that the two need to be duals of each other.

No, I actually agreed with you right here:

That's a fair thing to argue, but I'm still not convinced.

So I agree that it's perfectly fair to argue that there should be a deviation from keeping the duality consistent.  But I'm more motivated by logical consistency since I'm not convinced about the practical benefits of what you're proposing.

mental model of this that is incorrect

I explained exactly what I mean by duality in my previous comment:

f accepts variables y that are in the union of X and Y and a is in the intersection of their interfaces
g accepts variables y that are in the intersection of X and Y and b is in the union of their interfaces

If this is incorrect, then please feel free to clarify why.

Also, in case you hadn't noticed, we're not using the top-level index as a way to have arguments.   If you have additional supporting arguments, add them to arguments for.  I don't think it's a good idea to have a back-and-forth in the index.  It will just get too messy.

Everybody please calm down. Moderator can we put this thread in slow mode?

I'm going to take a break for a while anyway :smile:

So I agree that it's perfectly fair to argue that there should be a deviation from keeping the duality consistent. But I'm more motivated by logical consistency since I'm not convinced about the practical benefits of what you're proposing.

If you're not motivated by practical examples, then I don't have much else to say. Gradual typing and Any in python are special and are the essence of allowing for pragmatism. Things that need to interact with Any should have to consider if they are interacting in a way that furthers that goal, or we may as well advocate Any be removed outright.
If you want to get into the weeds of purism and consistency, most languages don't actually have an equivalent to Any as Ω (python's use), they have ? Much of the theory we are building on also uses ?, and does not allow Ω to be specified.
I'm also proposing that this is treated the same as an existing case with Any, so not only is the special case easy to explain, but type checkers already need to support this special case. There's nothing newly special here, but there are practical benefits.

I explained exactly what I mean by duality in my previous comment:

f accepts variables y that are in the union of X and Y and a is in the intersection of their interfaces
g accepts variables y that are in the intersection of X and Y and b is in the union of their interfaces

If this is incorrect, then please feel free to clarify why.

It is accurate that the union of X and something concrete that isn't X widens the pool of types, and may narrow the known minimum interface.
It is also accurate that the Intersection of X and something concrete that isn't X narrows the pool of types, and may widen the known minimum interface.
It does not follow from this that widening one is as unsafe as widening the other, and an example above was shown how the case of unions remains failing safe in the presence of unexpected Any, rather than failing silently ignoring what is there.

I would suggest for each of the viable possibilities of which there are I think 4/5 we could make a real world example that illustrates what the resulting type is, or what error is raised. Based on the call earlier, it seems like perhaps a TypeVar based example that uses an external library would be a good candidate for comparing each option - perhaps something like the below:
from typing import TypeVar, Generic, Protocol
import numpy as np
from dataclasses import dataclass
T = TypeVar("T")

class A(Protocol):
    @staticmethod
    def bar():
        return 1

@dataclass
class Test(Generic[T]):
    @staticmethod
    def foo(x: T) -> T & A:
        x.bar = A.bar
        return x
y = np.cos(1) # External library, type is Any here
z = Test.foo(x = y) # What is type of z

Appreciate the monkey patch isn't ideal here, but it does illustrate a case where this could come up

Below I've tried to follow through the logic for what happens if we assume each of the options. I'm trying not to make a statement here about which I prefer just provide clarity, although it is worth noting that option 1 leads to a misleading type.
Example set up
from typing import TypeVar, Generic
import numpy as np
from dataclasses import dataclass
T = TypeVar("T")

class A:
    @staticmethod
    def bar() -> int:
        return 1

@dataclass
class Test(Generic[T]):
    @staticmethod
    def foo(x: T) -> T & A:
        x.bar = A.bar
        return x
y = np.cos(1) # External library, type is Any here
# Let's assume y has attribute ndim (as it happens it actually does)

1. T & Any = T
incorrect
z = Test.foo(x = y) # z has type A
z.ndim # Error does not have attribute ndim, incorrect

2. T & Any = Any
correct, but perhaps loses some info
z = Test.foo(x = y) # z has type A
z.ndim # fine - type unknown but this is expected
z.bar() # also fine, although type of return is unknown in bar

3. T & Any is an error
correct, maybe a little restrictive
z = Test.foo(x = y) # We get an error here.

We can fix this by giving y a type, but it might make code a bit longer sometimes. Is it worth making it longer? Perhaps
4. Any is not reduced within intersections.
Leaves more work for the type checker, but also more flexibility
z = Test.foo(x = y) # z has type Any & A
z.ndim # Fine I think, returns type Any
z.bar() # Returns type of int? If the type checker is smart enough

5. Any is only considered in an intersection in deference to non-gradual types.
Not sure I'm clear on the difference between this and option 4, perhaps if you could fill out this example @mikeshardmind? Happy to edit this to include.

^ I think I'll actually put the above as a file in the repo, makes it easier for people to edit and correct

https://github.com/CarliJoy/intersection_examples/pull/30
https://github.com/CarliJoy/intersection_examples/blob/158b9ba3369b6e270feb895515f2e28aea128511/docs/any_type_options.md
I would suggest we do the following:

Fill out the document with any additional detail I might have missed for each option
Once each of the options is clear, we eliminate any options that could lead us to an incorrect or misleading type hint (e.g. most likely option 1 here, maybe others)
Evaluate user experience in each case, what happens to the person that tries this, are they helped by what happens (we can give each a rating out of 5 perhaps)
Evaluate how easy life will be for type checker developers (again, rating out of 5)

I'm hoping that perhaps we can agree on the ratings quite simply, but if not we could vote for them somehow.

Also, I've been trying to stay impartial on this to promote clarity, but I'll express my own opinions briefly on the above:
My favourite I think is Option 2, but options 3-5 are also viable to me.

Earlier in the discussion people noted typescript does option 2, which is certainly worth mentioning.
It's also the least work for people making type checkers, which is always a plus - you could argue though 3 is also a small amount of work, but 4 & 5 seem like they could be more complex.
It's less work for the user than 3 also, as it doesn't force them to type external libraries etc.
The main disadvantage is that some information has been lost, e.g. the & A in the above example, which means users can't see they have the methods of A etc. While this is true, it seems like maybe not such a loss - we are in a case where the user is providing Any, so the fact they get some Any's in return is maybe not so bad.

Mostly though I'm keen to find a solution to this, as really it seems like quite an edge case that's created an impasse.

Thanks a lot for the write up Mark! Especially for spelling out all the possible options - it really helps get a better understanding of the situation. FWIW I'm also leaning towards option 2 which I think is the most natural and simple to understand (and it works for TS so can't be that bad :sweat_smile:)

we are in a case where the user is providing Any, so the fact they get some Any's in return is maybe not so bad.

The user may not intend to be providing Any is the problem with this. According to Eric, and the reason why we can't just forbid them:

intersections with Any will arise, often in the bowels of the type checker's logic where there's no good way to report an error to the user

This presents the question: If the typechecker that is meant to be better at correctly reasoning about types than a developer who isn't focusing on this problem can't be sure where this can arise, and that it can do so in a way where there is no good way to inform a user, to the point where there's a real concern from a maintainer of pyright about just erroring, how can users be sure their use of intersections isn't silently hiding errors?

@mikeshardmind I certainly follow this as a strong reason against option 3 - if this needs to be done inside the type checker, and I'm willing to take Eric's word for it, banning it isn't really an option (I'll add this to example doc).
In the same post though, Eric also says:

Intersections and unions are two sides of the same coin. For every rule that applies to unions, there should be an analogous rule that applies to intersections (and vice versa)

From a symmetry point of view, if Any | A -> Any, then Any & A -> Any is very symmetrical. So that seems to be a good reason for option 2.
Re TS, if the programming languages are very different perhaps it's not a great analogy, but I thought it was at least worth re-acknowledging.

From a symmetry point of view, if Any | A -> Any, then Any & A -> Any is very symmetrical. So that seems to be a good reason for option 2.

The appropriate symmetrical analog would be Any & A -> A.

The appropriate symmetrical analog would be Any & A -> A.

You're right that this would be closer to what you would expect from type theory, but from the example below option 1 seems quite misleading, so I guess I mean option 2 is perhaps more symmetrical when compared to options 4 and 5.
https://github.com/CarliJoy/intersection_examples/blob/158b9ba3369b6e270feb895515f2e28aea128511/docs/any_type_options.md#1-t--any--t

Just looking at this example, option 1 seems best to me, it's easy to understand the semantics, and if I'd actually want to widen to Any it's easy to do this manually:
z: Any = Test.foo(x = y)
z.ndim

Or, probably better: add a type ignore on the bad attribute access until typing is enabled for the foreign library.

Just looking at this example, option 1 seems best to me, it's easy to understand the semantics, and if I'd actually want to widen to Any it's easy to do this manually:
z: Any = Test.foo(x = y)
z.ndim

Or, probably better: add a type ignore on the bad attribute access until typing is enabled for the foreign library.

I do understand the motivation for option 1, it has a certain appeal - but I guess my argument would be if you have to add type:ignore or move the type to something else like Any, that's not the right type. If I inspect the available attributes with dir, what I get no longer matches the attributes available in the displayed type. Until I saw the example I was actually quite on the fence between options 1 and 2, but really I think it comes down to this:

Being given a type that's too broad for the attributes available - there won't be any errors raised when we do some things that are invalid.
Being given a type that's too narrow for the attributes available - there will be errors raised when we do things that are valid

The second one just seems much worse to me than the first, but I guess that is personal preference somewhat.

Perhaps a middle ground between 1 and 3 is possible? Such that type checkers can yield an error when "not in the bowel".

It seems like currently, a lot of arguments get reiterated that have already been made and discussed. I'd recommend people new to the thread to check the pinned comments at the top, in particular:

Eric's analysis: https://github.com/CarliJoy/intersection_examples/issues/1#issuecomment-1657265867
Comments on the nature of Any:

https://github.com/CarliJoy/intersection_examples/issues/1#issuecomment-1661862059
https://github.com/CarliJoy/intersection_examples/issues/14#issuecomment-1658778823
https://github.com/CarliJoy/intersection_examples/issues/1#issuecomment-1654835860

    def foo(x: T) -> T & A:
        x.bar = A.bar
        return x

I think it's a great idea to have an example to compare the different options.  But I think there are some problems with this example: Just because you've set the bar attribute, that doesn't make x a subtype of A.  (It doesn't even respond true to isinstance(x, A)).  You could have made it a protocol (and removed staticmethod), but I think this pretty uncommon as a use of intersections.
Debatably, a more common way for intersections to turn up is through the use of isinstance or match.  For example:
def f(x: T):
  if isinstance(x, U):
    reveal_type(x)  # T & U

I think this would make your examples much easier to understand.  (This is debatable whether intersections turn up here at all though, and we can debate that in another thread if there are doubters.)

so I guess I mean option 2 is perhaps more symmetrical when compared to options 4 and 5.
Option 2: Any | A -> Any vs Any & A -> Any
Option 4/5: Any | A -> Any vs Any & A -> Any & A

Just FYI, Any | A is currently irreducible in type checkers today.  So that is what it is for all of the options unless you're proposing changing it.  So from a symmetry point of view, 4 and 5 are the most symmetric.

I think it's a great idea to have an example to compare the different options. But I think there are some problems with this example: Just because you've set the bar attribute, that doesn't make x a subtype of A. (It doesn't even respond true to isinstance(x, A)). You could have made it a protocol (and removed staticmethod), but I think this pretty uncommon as a use of intersections.

Yeah point taken, I appreciate the isinstance issue - tried to make something with inheritance then wasn't sure how to initialise the class. It would be really cool to have a second real world example for each option, so if you have another idea in mind perhaps push up another md doc to my branch. I'd like it to be in the same structure if possible.

Just FYI, Any | A is currently irreducible in type checkers today. So that is what it is for all of the options unless you're proposing changing it. So from a symmetry point of view, 4 and 5 are the most symmetric.

Fair enough - yeah in that case I think that's certainly a +1 for 4 and 5 - there are still some question marks over what it means to be Any & X though I think, and whether Any is maybe a clearer type to an end user. Certainly though I think 2,4 & 5 are really the primary candidates.

I would hesitantly suggest that the difference between 4 and 5 is largely about how the type is interpreted by the type checker - in both cases we have Any & X -> Any & X, it's just about what this means to the type checker when accessing attributes. That just leaves option 2 - based @erictraut 's comment:

From this analysis, I conclude that there are two solutions that produce consistent and logical results:
Both Any | T and Any & T reduce to Any.
Both Any | T and Any & T are irreducible.
The first of these options is how TypeScript works, but it's inconsistent with the way Python type checkers currently treat Any | T. We could decide to change that behavior (since it's not mandated in any spec), but doing so would be disruptive, and it would lead to more false negatives in mixed-type code.

It seems that option 2 would have the largest impact for type checker implementers, so maybe should be avoided. Also as @NeilGirdhar points out options 4 and 5 have more symmetry with union.
I'm wondering if we're now only debating 4 vs 5 really, perhaps we could close this issue (as resolved as Any & X) and open a new one to decide how the type checker should interpret Any & X, which really seems to be the sticking point. Perhaps we can even draw some inspiration from how Any | X is currently handled?

Here's an example that might work for Any  & U
from __future__ import annotations
from typing import Any, TypeVar, reveal_type

class C:
    def bar(self) -> None: ...

T = TypeVar('T')

def f(x: T) -> T & C:
    assert isinstance(x, C)
    reveal_type(x)  # Should be T & int, but basedmypy gives "C (narrowed from T)"
    x.foo()  # Should be okay?
    return x  # Should be okay, but basedmypy gives an error that C cannot be returned.

def g(y: Any):
    z = f(y)
    reveal_type(z)  # Any & C as desired.

The question between 4 and 5 is what is the interface of z?  z.foo() is Any in both cases, but z.bar is Any in case 4 and None in case 5.  And the question comes down to whether this special case is more practical.

Please differentiate between defining a variable, setting it and getting a property from it. They are inherently different!
def setter(var: T_to_set):
    # Defining
    a: T
    def fn(b: T) -> None:
        b.some_property

    c = cast(T, Something)
    d = ExpressionThatEvaluatesToT

    # a, b, c, d define exactly the same type for the type checker

    # Setting
    a = c = d = var
    fn(var)

    # both lines above are handled the same by the type checker

    # Accessing something and determining its type, all below are evaluated the same
    a.some_property
    # The b.some_property case is checked in the function itself
    c.some_property
    d.some_property

    # Methods/callables could contain overloads but called with identical types this is the same

Please let us first only talk about using Intersection when Accessing properties. Setting is a whole different problem set that we can focus on after.
Also this helps to keep the examples much simpler. Because if we switching contextes between what is allowed for Setting and for Accessing make things more complicated.

I'm wondering if we're now only debating 4 vs 5 really, perhaps we could close this issue (as resolved as Any & X) and open a new one to decide how the type checker should interpret Any & X, which really seems to be the sticking point.

I'm fine with this.

Perhaps we can even draw some inspiration from how Any | X is currently handled?

I'm also fine with this if we're viewing it from the lens of the effect on the boundary between fully typed and gradually typed code. That boundary is the only place where user code should ever see this happen, and therefore needs to be pragmatic about who becomes responsible for the effects (which library is most effected, the typed or untyped one and do each the typing user and the non-typing user get what they expect?)

Ok great! I'll close this then and reference this in a new thread that's just about Any & X and how we access variables from this type. For anyone finding this in future - based on lengthy discussion re various options for how Any is used with intersection:

Any & T -> T was eliminated based on examples
Any & T -> Any was eliminated based on asymmetry with union (Any | T -> Any | T) and difficulty with implementation due to this assymetry.
Any & T -> ERROR was eliminated due to this intersection being required in the internals of type checkers, rendering it impossible.
Any & T -> Any & T The last option, which has been chosen, is symmetric with the way union works Any | T -> Any | T. There has been some discussion as to how this type should be interpreted, and the types of it's attributes and methods, but this discussion is being moved to a new thread (see below).

There is now a large majority for this (https://github.com/CarliJoy/intersection_examples/issues/1#issue-1817147039) so it seems like the best way forward with the pep.

For the sake of reference, here how intersections and unions are currently handled in MyPy currently.
import typing as t

class Foo:
    def exists(self) -> bool:
        return True

def needs_bool(x: bool) -> None:
    ...

def foo(x: Foo | t.Any) -> None:
    t.reveal_type(x.exists())  # Revealed type is "Union[builtins.bool, Any]"
    needs_bool(x.exists())  # main.py:13: error: Item "Foo" of "Foo | Any" has no attribute "anything"  [union-attr]
    t.reveal_type(x.anything)  # error: Item "Foo" of "Foo | Any" has no attribute "anything"  [union-attr], reveals Any
    if not isinstance(x, Foo):
        t.reveal_type(x.anything)  # reveals Any without error, as we ruled out Foo from the Union

class A:
    common: str
    a: int

    def fn_a(self, a: int) -> int:
        return a

    ab_mix: "A"

class B:
    common: str
    b: str

    def fn_b(self, b: str) -> str:
        return b

    ab_mix: "B"

def internal_intersection(x: A) -> None:
    if isinstance(x, B):
        t.reveal_type(x) # Revealed type is "Any"
        # Can't be resolved as there is a conflict in classes
    if isinstance(x, int):
        t.reveal_type(x)  # Revealed type is "__main__.<subclass of "A" and "int">"
        t.reveal_type(x+10) # Revealed type is "builtins.int"
        # MyPy already determines the correct __add__ method

class X:
    x: int

class Y:
    y: str

class Z(X,Y):
    z: bool

def internal_intersection_2(x: Z) -> None:
    if isinstance(x, Y):
        t.reveal_type(x) # Revealed type is "__main__.Z"
        # That is really smart of MyPy to determine that
        t.reveal_type(x.x) # Revealed type is "builtins.int"
    if isinstance(x, int):
        t.reveal_type(x) # Revealed type is "__main__.<subclass of "Z" and "int">"
        t.reveal_type(x+10) # Revealed type is "builtins.int"
        # MyPy already determines the correct __add__ method

# `T & Any` -> `T` for isinstance
def internal_intersection_any(x: t.Any) -> None:
    if isinstance(x, Y):
        t.reveal_type(x) # Revealed type is "__main__.Y"
    if isinstance(x, int):
        t.reveal_type(x) # Revealed type is builtins.int"

MyPy Play

Re-opening this as some arguments in favor of option 4 over option 5 in #31 have contradicted the reasons why other options were taken off the table.

Just an observation - I've had an idea that I think maybe explains why it's been so difficult to reach a consensus on this topic. Based on some of the discussion in the other thread as well, it seems that there is a divide between those who prefer false negatives and those who prefer false positives. The Any intersection seems that it will have to create one or the other in some scenarios, and I'm wondering if preference for each is based on a factor deeper than personal preference.
MyPy vs Pyright
For now I'm limiting my discussion of this to these two as they're both very popular - other type checkers I will exclude in this comparison. Although I am most familiar with pyright, I have now seen a little of mypy, but interestingly some of what it was doing felt quite strange to me. Prior to this I'd thought choice of type checker didn't really affect very much, but now I think this might be at the very heart of this debate. I propose that users of pyright prefer false negatives, while users of mypy prefer false positives.
Why would this be?
In pyright in general type: ignore is considered a nono - anywhere you use a type: ignore you risk adding in many kinds of error, as most things come up as "generalTypeIssue" - this includes syntax errors. A false positive therefore is a pain, because it means you can introduce other kinds of error, so in general I avoid them like the plague. False negatives on the other hand (particularly in "basic" mode), are commonplace.
In mypy in contrast, typing errors are much more granular - you can easily specify a type: ignore with a qualifier, so if I wish to allow specifically an any to be used, or some other specific constraint, it's very easy. Therefore a false positive is not such a big deal - you just say "I really want to specifically this intersection here" and your problem goes away. A false negative on the other hand perhaps is considered a terrible thing in mypy (this is speculation on my part).
How does this relate to the Any discussion?
Each option we can follow to a "false negative" or "false positive" result:

T & Any = T -> False positive -> preferred by mypy users
T & Any = Any -> False negative -> preferred by pyright users
T & Any is an error -> False positive -> preferred by mypy users
T & Any -> T & Any -> Depends on interpretation -> leads to a different discussion.

What do we do about this?
If my theory is correct, in some way this is good news, because it means that some of this may not, and perhaps should not, be specified by the PEP. But we still have to agree on a type across all type checkers, so that means T & Any -> T & Any is really the only candidate - but then the interpretation we leave up to the type checker.

For now I'm limiting my discussion of this to these two as they're both very popular - other type checkers I will exclude in this comparison. Although I am most familiar with pyright, I have now seen a little of mypy, but interestingly some of what it was doing felt quite strange to me. Prior to this I'd thought choice of type checker didn't really affect very much, but now I think this might be at the very heart of this debate. I propose that users of pyright prefer false negatives, while users of mypy prefer false positives.

Well, call me the contradictory case. I only support pyright. Where mypy differs is largely worse for users since pyright's feedback will show up for VSC users. I believe that static analysis is most useful as a step in the process, not as feedback that must be entirely addressed at all times, and that false positives are better than false negatives. You don't need to type ignore most false positives, you can simply document the root cause and leave them there, error and all, allowing you to still get feedback, while knowing "hey, in this case, we know it's not a problem", this doesn't hide a problem, and instead better serves to document for future people touching it why something might not be as immediately obvious as other similar code.
Given this, I tend to vastly prefer false positives, but I also tend to do what I can to give the type checker more information to nudge it to knowing it is fine, or report or PR upstream, either stubs, types directly, or issues in a type checker when it can be confirmed as a false positive. This in general allows gradual improvement of the overall ecosystem.
I understand that false positives can be seen as an annoyance, and maybe there are cases where we should avoid them. It's not fully about false negatives vs false positives for me, but a balance of considering how and where each can occur, and the severity of the issue, and how much the false outcome (in either direction) would violate the reasonable expectations of a non-expert.
If you told someone that Any & T would never be checked more than Any could reasonably ask all of the following

Why the type checker allows Any in an intersection?
Why doesn't the type checker just show me this is Any instead of Any & T then?
Why is this behavior different from subclassing from both Any and T, where it still checks T?

If my theory is correct, in some way this is good news, because it means that some of this may not, and perhaps should not, be specified by the PEP. But we still have to agree on a type across all type checkers, so that means T & Any -> T & Any is really the only candidate - but then the interpretation we leave up to the type checker.

This cannot differ. This would lead to the diverging behavior situation that's been more than hashed out enough in this and other threads already. The subtyping behavior we choose needs to be defined here.

You don't need to type ignore most false positives, you can simply document the root cause and leave them there, error and all, allowing you to still get feedback

In many open source projects, you need to satisfy the type-checker in order to pass CI. Your use-case seems rather special. False positives are doubly problematic there, since it makes the review process even more tedious ("is this type-ignore really justified?")

In many open source projects, you need to satisfy the type-checker in order to pass CI. Your use-case seems rather special. False positives are doubly problematic there, since it makes the review process even more tedious ("is this type-ignore really justified?")

I think people are assuming too much of type checkers being correct and shouldn't do this, never the less, the proposal here with a false positive does include a way to resolve it Without a type ignore by simply adding the missing information with 1 additional protocol in the intersection. This has a nice analogue with the subclassing route with Any and reconciling.
class Inter(Any, T):
    """ Structurally equivalent to Any & T, not nominally ""
    ...

class Inter(Any, T):
    attribute_we_need_from_untyped_base: str

# vs

class Compact(Protocol):
    attribute_we_need_from_untyped_base: str

# +
from x import SomethingThatsAny
SomethingThatsAny & T & Compat

This is also safer than that type ignore because it continues working if the thing is later typed.

In many open source projects, you need to satisfy the type-checker in order to pass CI. Your use-case seems rather special. False positives are doubly problematic there, since it makes the review process even more tedious ("is this type-ignore really justified?")

I hadn't considered this but it's a very good point about CI checks, I'm starting to think my dislike towards false positives may be an opinion most of the community shares in general, so this is something to keep in mind.

I think people are assuming too much of type checkers being correct and shouldn't do this, However, the proposal here with a false positive does include a way to resolve it without a type ignore by simply adding the missing information with 1 additional protocol in the intersection. This has a nice analogue with the subclassing route with Any, leading to increased consistency of user expectations, and it doesn't hide future errors, and it remains compatible if the other type later becomes fully typed.

I think this example assumes that the external library here is something very simple, that can be easily reproduced with a protocol matching the features used. I would argue this doesn't really work in practice, because many external libraries have many attributes and methods - it's the equivalent of having to type the entire external library (or at least all the parts of it you want to use).

My general thoughts from the whole thread on this I think are:
T & Any = T -> Leads to false positives, asymmetric with union
T & Any = Any -> Leads to false negatives, asymmetric with union
T & Any is an error -> False positives in some cases, but in practice impossible according to Eric
T & Any -> T & Any -> Depends on interpretation, hence new thread
Are any of these points controversial or incorrect?

Strictly speaking, no, but there's some lost nuances here.
The most important one is that it's very hard to claim anything about symmetry from these examples, even where there is some, because the symmetry is not exhibited by just swapping | for & and expecting opposite results should always be the case. Any symmetry claim here should be qualified in how the symmetry is exhibited to avoid misconceptions.
There's some other lost nuance along the way, but that's the only one that I think would be detrimental to leave out in any summary.

I think this particular ship may have long since sailed - type checkers are fast becoming a standard to which modern codebases hold themselves accountable, we have to move with the times.

Type checkers themselves still don't hold themselves to this. That other people would block a PR on this that fixes an issue speaks to the social issues of typing.

I think this example assumes that the external library here is something very simple, that can be easily reproduced with a protocol matching the features used. I would argue this doesn't really work in practice, because many external libraries have many attributes and methods - it's the equivalent of having to type the entire external library (or at least all the parts of it you want to use).

It doesn't. That's actually my intent that people do this. Then PR it upstream. They also have another escape hatch: don't use an intersection on a type that isn't typed yet. Just say Any instead of UntypedisAny & T. until the Any side of that is typed. IF we give people the false positive case, they can make a decision about which way is best for them to resolve it. If we have the false negative case, we only lose out on potentially caught errors.

Type checkers themselves still don't hold themselves to this. That other people would block a PR on this that fixes an issue speaks to the social issues of typing.

It's a fair point, but I do think we have to take into account how this will be used in practice.

It doesn't. That's my intent that people do this. Then PR it upstream. (After all, if people are doing this because they see it as the future of modern code, surely they can help modernize the things they rely on right?)

This is quite an optimistic view - don't get me wrong I'm all for encouraging people to contribute to open source projects, but equally we can't expect people to write a type system for all of numpy...

They also have another escape hatch: don't use an intersection on a type that isn't typed yet. Just say Any instead of UntypedisAny & T. until the Any side of that is typed.

This doesn't resolve the examples that use generics those where people may not have a choice but to use an Any object in an intersection (because let's suppose some external library is using T & A where T is a TypeVar). It's forcing people to essentially cast Any & T back to Any, which is honestly what I would do in practice in this use case.

And then the last one, they still have the type ignore.

Again, previous point on type:ignore leading to issues.

If we give people the false positive case, they can make a decision about which way is best for them to resolve it. If we have the false negative case, we only lose out on potentially caught errors.

I guess my point stems to that all the available options for the false positive are kind of bad - a Hobson's choice isn't much of a choice.

We sitting here designing the feature should be able to see that if someone takes the time to do Any & T, they probably think something more than just Any is going to be checked, so the arguments about false positives ring a bit hollow for me, this is more explicitly a user asking for both halves to be checked.

I actually think this a strong point - I think it's a strong case for the Any & T -> Any option but still. The only real argument against this one that I've seen was that it was mentioned it would be difficult to implement. If we go with option 4 I completely agree that it has to do more than just Any or it's misleading, but that's probably a discussion for the other thread.

https://github.com/CarliJoy/intersection_examples/blob/main/legacy_examples/intersect_lib/user_example.py
In this example, the user hasn't made untyped_lib or intersect_lib (let's assume these are both big well established libraries), but they wish to use them together. Having a false positive in user_example just seems really strange to me - all they want to do is combine one large untyped library with another library that uses intersection.

The only real argument against this one that I've seen was that it was mentioned it would be difficult to implement.

It be extremely odd and surprising for the subtypes of A & B to be narrower than A, but for the subtypes of A & Any to be broader than A.

If we go with option 4 I completely agree that it has to do more than just Any

This has come up a few times in various comments, but in option 4, T & Any is not Any.   It does "do more".  Of course, the subtypes still must be subtypes of T.
Moreover OP(T & Any) is not exactly OP(Any) in general.  It has to obey LSP, so for z of type T & Any, z.x is:

Any if x is not present on T, but
T.x & Any otherwise.
But the latter can give errors unlike Any.  For example, if x is a callable, and you try to call it with arguments that are incompatible with T.x that violates LSP and is a type error.

Also, this thread has been going on for almost half a year.  It might be worth looking at how we can transition from debate to a conclusion so that we can write this PEP and have intersections soon.  Are there any options we can eliminate now?  Which options are still on the table?

Are there any options we can eliminate now? Which options still have supporters?

I'll leave where I stand on each option here for now:
Remove Any from Intersections:
I'm fine with this option. I know that pure theory says it is irreducible, but I don't think pure theory is actually pragmatically useful with the current definition of Any.
I do not have this option as a preference, and would only advocate for it as a last resort prior to options that I am actively against.
An Intersection containing Any becomes Any:
I'm strongly against this option. It would be the worst outcome of all options here for anyone specifying an intersection thinking it was gaining any level of safety. Should any type someone in this position is in not be determinable by a type checker, they actively make what they are typing less typed by using a feature that should make things more typed.
Disallow Any in Intersection
I'm still of a positive opinion on this. I am okay with disallowing things that don't have some amount of type information to be passed into typevars that interact with intersections. keeping in mind that we already established that isinstance is not an intersection creator, it's a type guard which has different semantic meaning and will not be changed, I don't think this is as potentially disruptive as people have claimed it will be. I could advocate for it, but only as a secondary choice.
Treat T & Any as irreducible in general
I am strongly against the original interpretation of this option. if it behaves as an intersection with Any for all attributes present on T, then it is inconsistent with other existing typing decisions (subclassing of Any) and presents all the same issues as treating T & Any as Any, where more specification may lead to less ability for things to be checked.
Any is only considered in an intersection in deference to non-gradual types.
This is the previous option, reconciled with existing typing decisions (subclassing of Any) and the idea that if a user specifies more, we can reasonably assume they intended to check more. This is my preference between the 5 options.

Regarding the false positives thing, we should probably create a thread and link to various comments about false positives there. What do you think?

I don't think the discussion about false positives vs negatives as been productive. That might be general pessimism from the idea that it feels like we've been retreading the same ground again and again.
I think we need to focus on taking a look at how intersections are actually going to be used by users and look for which would be more surprising to a user, that something does error or that something else does not. Basically, I think we need to determine where and how each would occur and only discuss the tradeoffs between the specific circumstances, not as an attempt to say "all false positives are worse" or "all false negatives are worse", so I think we can only meaningfully examine this once we agree on what options are viable to compare.

I think we need to focus on taking a look at how intersections are actually going to be used by users and look for which would be more surprising to a user,

Good idea.  Do we have examples of "how intersections are actually going to be used" checked in to the repository yet?  I know we have test cases that standardize the behavior of conformant implementations.  I'm not asking about that.

I don't think the discussion about false positives vs negatives has been productive.
not as an attempt to say "all false positives are worse" or "all false negatives are worse"

We don't need to dismiss anything as "out of the question", but I think that there were many comments about the pernicious nature of false positives and it is something that a reader may want to consider.  It doesn't decide anything, and we can collect all the arguments for and against just like we did here.  Ultimately, these ideas can inform the PEP.

I'll leave where I stand on each option here for now... [in summary]
option 1: okay
option 2: no
option 3: yes
option 4: "I am strongly against the original interpretation"--I'm going to take this as no since everyone who responded to it seems to be responding to "the original interpretation".
option 5: yes

I'll let the others speak up about their preferences, and hopefully we can eliminate most of the options.

Good idea. Do we have examples of "how intersections are actually going to be used" checked in to the repository yet? I know we have test cases that standardize the behavior of conformant implementations. I'm not asking about that.

Some of the tests could be turned into practical use cases, but otherwise we don't. We should really try adding some actual real-life examples which could help clarify which options are workable and which aren't. (there has also been lots of examples shared throughout these issues, but they're all scattered around rather than living centrally in the repo..) Otherwise I feel like we're going in circles arguing for different options without any real progress..

Great point/idea

Sure yeah I agree, we need to break the cycle, and I think getting more real world examples is a good thought. I tried to do this for the false positive discussion here: https://github.com/CarliJoy/intersection_examples/blob/main/legacy_examples/intersect_lib/user_example.py
...but perhaps this example needs more context for why it would happen. Just a thought - is it worth setting up a PR for each example? Then people can discuss each one on a separate thread, and add more details etc.
I think it might be quite good to see the "protocol" use case in a practical example, that I know I've discussed quite a bit with @mikeshardmind. Then we can hopefully find a version that satisfies the use cases, rather than the other way around.
I'll voice my preferences below on current options:
Remove Any from Intersections Any & T -> T:
I think this one just leads to extremely misleading information. Any & T -> T means that T no longer has the properties of Any, or in other words it's an inner join not an outer join. This is the worst of all available for me, because it leads to a type that will cause the user to interrogate their code and find no reason why it's not working.
An Intersection containing Any becomes Any Any & T -> Any
Fine with this one - I'm not really sure what is lost by it becoming Any, as Any & T has all the properties of Any, and so does Any. Any also has all the properties of T because it's anything.
Disallow Any in Intersection Any & T -> ERROR
This one is weird - I think the error would be misleading, and there are scenarios where this would causes issues for user (see earlier example), so I guess I'm against this one - but less against it than Any & T -> T. This at least explains the issue well to a user trying to fix it. This is kind of my "last resort" option I suppose.
Treat T & Any as irreducible in general / Any is only considered in an intersection in deference to non-gradual types. Any & T -> Any & T
Not sure I really get these yet - it would be good to see more examples with the implications of each. I think broadly though that this is probably a good way in to the problem, as it might give us the flexibility to allow for more use cases. We can tune the interpretation to the use cases.

https://docs.google.com/spreadsheets/d/1JLOF0d20olalPHZrR3AoElGY4gpSpl8uDyOafJVFaZ0/edit?usp=sharing
I've added @mikeshardmind and myself to this to get people started - feel free to add a row! It's full edit access so go ahead and modify as you like - I've tried to limit us to 4 categories of opinions in an effort to aid readability - the idea is that people can then update their preferences as we go through examples etc.

@mark-todd Regarding Any & T -> Any & T, again consider Eric's comment:

(Any & B).x:
Any if x is not present on B
(Any & B.x) if x is present on B

So if B.x is an int, we know that (Any & B).x is (Any & int). This knowledge would be lost if the type was simplified to Any. This clearly makes a difference if then you have code like
def foo(obj: A&B):  # A untyped.
    if not isinstance(obj.x, int):
        return "123"
    else:
        return 42

If Any & T is simplified to Any, then the type checker will infer the return type of this method as str | int, but if Any & T is preserved, it can tell you that the if-branch is unreachable. Secondly, preserving Any & T plays nicer when a library eventually becomes typed, since all the Any & T simply become S & T.

@mark-todd Regarding Any & T -> Any & T, again consider Eric's comment:

(Any & B).x:
Any if x is not present on B
(Any & B.x) if x is present on B

So if B.x is an int, we know that (Any & B).x is (Any & int). This knowledge would be lost if the type was simplified to Any. This clearly makes a difference if then you have code like
def foo(obj: A&B):  # A untyped.
    if not isinstance(obj.x, int):
        return "123"
    else:
        return 42

If Any & T is preserved, it can tell you that the if-branch is unreachable, otherwise it can't. Secondly, preserving Any & T plays nicer when a library eventually becomes typed, since all the Any & T simply become S & T.

Sure yeah I agree, we need to break the cycle, and I think getting more real world examples is a good thought. I tried to do this for the false positive discussion here:

I wouldn't call this a real world example for this. We really need examples that are actually representative of problems intersections solve that aren't otherwise solvable today to examine the consequences. Any minimal example that only exhibits the behavior looses the surrounding context of "why is an intersection needed to solve this", and will not be useful to determine whether a false negative or false positive is the more harmful outcome.

The difference between option 4 and 5:
option 4:

(Any & B).x:
Any if x is not present on B
(Any & B.x) if x is present on B

option 5:

(Any & B).x:
Any if x is not present on B
(B.x) if x is present on B

option 5 is in-line with the behaviors already existing in the type system, option 4 is not. See details in this comment

An Intersection containing Any becomes Any Any & T -> Any
Fine with this one - I'm not really sure what is lost by it becoming Any, as Any & T has all the properties of Any, and so does Any. Any also has all the properties of T because it's anything.

@mark-todd, Any doesn't have all the properties of T. If T has a property foo with a particular type Bar, then the type of T.foo is Bar, while the type of Any.foo is Any. Reducing Any & T to Any removes information known to be true.

I've added @mikeshardmind and myself to this to get people started - feel free to add a row! It's full edit access so go ahead and modify as you like - I've tried to limit us to 4 categories of opinions in an effort to aid readability - the idea is that people can then update their preferences as we go through examples etc.

I dont think we should split this into a google doc. We have proper attribution of comments here, the ability to link to other things as needed when discussing it, and more.

@mark-todd, Any doesn't have all the properties of T. If T has a property foo with a particular type Bar, then the type of T.foo is Bar, while the type of Any.foo is Any. Reducing Any & T to Any removes information known to be true.

@tylerlaprade I've thought on it some more and I think I follow your reasoning here - I've updated my opinion in the spreadsheet.

The one real world example I have with a false positive comes back to class decorators, and specifically using them in untyped code. I think this one also remains far-fetched.
@augmenting_decorator
class X:
    """ Everything here is completely untyped """
    ...

Where augmenting_decorator is something like:
def augmenting_decorator(typ: type[T]) -> type[T & AugmentProtocol]:
    ...

We have real world examples of decorators like this that have worse typing than this currently, but I don't think we have any examples where people have an untyped class using them. and care about that class passing type checking.

@DiscordLiz

I dont think we should split this into a google doc. We have proper attribution of comments here, the ability to link to other things as needed when discussing it, and more.

I think it's fine as long as it ends up back in here at the end if it helps keep track, I'm going to go ahead an record your answers in it to keep things in sync at least

The one real world example I have with a false positive for case 5 comes back to class decorators, and specifically using them in untyped code. I think this one also remains far-fetched.
@augmenting_decorator
class X:
    """ Everything here is completely untyped """
    ...

Where augmenting_decorator is something like:
def augmenting_decorator(typ: type[T]) -> type[T & AugmentProtocol]:
    ...

We have real world examples of decorators like this that have worse typing than this currently, but I don't think we have any examples where people have an untyped class using them. and care about that class passing type checking.

I don't think I see how this creates a false positive in case 5 - could you elaborate?
In terms of making it real, this just requires X to be an external lib without typing, and augmenting_decorator to come from another library.

In terms of making it real, this just requires X to come from an external lib without typing, and augmenting_decorator to come from another library.

Most people don't write functions as decorators intending them as glue between the user and yet another library. When that's the intent, they usually provide a wrapped class directly. Some languages would actually forbid this kind of thing (like rust does with determining the rules for who can be the implementor of a trait), so I'm not particularly concerned about it being possible but of it being reasonably likely to come up in real-world use cases as I'm trying to determine if there are any likely common questions to come up rather than rare cases that we know would leave the type checker with less information.

I don't think I see how this creates a false positive in case 5 - could you elaborate?

If the decorated class is completely untyped, the decorator is typed, and is exported as a symbol in a library that has a py.typed file, it could create a false positive. I see this as an unreasonable case to consider, as if you are claiming to export typed symbols, you should probably have typed classes to start with.

Amusingly, there's also an option with the best of both 4 and 5, but it brings back needing type negation.
Under such an option, we continue not reducing Any, and applying Any's inclusion recursively. Someone can then explicitly specify that they aren't allowing that type to overlap with specific things:
Explicit declaration using this option for the beahvior of option 5
def augmenting_decorator(typ: type[T & ~AugmentProtocol]) -> type[T & AugmentProtocol]:
    ...

And then this would be as permissive as we have in 4:
def augmenting_decorator(typ: type[T]) -> type[T & AugmentProtocol]:
    ...

Based on prior feedback and people thinking that was too complex with too many other unanswered questions for this pep, I think 5 is still the better call, but maybe this helps some people see why I thought it would be neccessary.

Most people don't write functions as decorators intending them as glue between the user and yet another library. When that's the intent, they usually provide a wrapped class directly. Some languages would actually forbid this kind of thing (like rust does with determining the rules for who can be the implementor of a trait), so I'm not particularly concerned about it being possible but of it being reasonably likely to come up in real-world use cases as I'm trying to determine if there are any likely common questions to come up rather than rare cases that we know would leave the type checker with incomplete information (And a possible false positive to go with)

There are quite a few libraries that provide class decorators as their main output - take pytest fixtures, fastapi routers & dataclasses to name just a few. Some of these are designed for specific purposes, but I guess it doesn't seem at all far fetched to me that some future library uses a decorator with an intersection (currently working on a more realistic example).

If the decorated class is completely untyped, the decorator is typed, and is exported as a symbol in a library that has a py.typed file, it could create a false positive. I see this as an unreasonable case to consider, as if you are claiming to export typed symbols, you should probably have typed classes to start with.

Apologies, I'm probably missing something obvious, but this only explains the setup and not the false positive. As I see it, any properties of AugmentProtocol would be fully described, and anything anything else is considered Any - where's the false positive?