@xgranade @whitequark like "too much busywork for the amount of bugs it finds" is not an experience I have had, but we write very different kinds of code so I'm definitely not arguing with that; I could see that 'ty' or 'pylance' might do far better with your code, or might even have a more rigorous approach to certain aspects of their type algebra. but all three happily give this program (and many like it) the thumbs-up:

x = 1
y = 2
locals()['y'] = 'oops'
print(x + y)

@whitequark @xgranade this is actually why I prefer mypy, specifically because (via plugins) it can accept an extension to the type system implemented with runtime hackery, and handle Zope Interface, while none of the other ones can. pydantic also has a similar thing (and dataclasses were originally supported via the 'attrs' plugin, although everybody else eventually got on board with those).

but I guess when it comes to "helpful" warnings, mypy probably does produce a lot more of those

@xgranade @glyph a type-checker that rejects well-typed programs is by definition buggy. if it's not fixed then it is unfit for purpose

we could have a broader discussion of what "well-typed" means for Python (it is not clear to me at all) but if the above is an accurate assessment of the consensus in mypy development then it is not a(n even aspirationally correct) type-checker

@glyph @whitequark

```
def f() -> None:
return

y = f()
```

main.py:4: error: "f" does not return a value (it only ever returns None) [func-returns-value]
Found 1 error in 1 file (checked 1 source file)

@xgranade @whitequark heh. fair enough I guess, although I am tempted to troll “that’s totally a valid type check once you realize that in certain contexts None means ‘null’ but in others it means ‘void’ “

(formally speaking, -> None is already lightly gibberish as it is an unprincipled pun for NoneType; but in support of your point, ty does accept NoneType but Mypy doesn’t)

@glyph @whitequark But that's my point... Python doesn't even have a void, but mypy acts like it does!

```
from typing import Any
def f() -> None:
pass

y: Any = f()
```

Assigning a value to a variable of type `Any` should always be allowed. That should be true in any gradually typed system.

@glyph @whitequark By way of getting at what I mean about expecting there to be rules I can follow, one of those is that if `x = y` typechecks, then `f = lambda: y; x = f()` should also type check.

That doesn't hold, though:

```
from typing import Callable

f: Callable[[], None] = lambda: None
y = f() # error

x: None = None
y = x # ok
```

That means I cannot in general refactor by extracting a value into a function that returns that value, which breaks the whole idea of a type system.

@glyph @whitequark Anyway, sorry for the long reply, but I guess the short version is that I don't think any of the above behavior is consistent with a type system, but it can be consistent with a linter.

That is, knowing the types of a program in Python is not sufficient to know if that program will pass mypy. I have to know about the context in which those types are used, which breaks the abstraction entirely. It makes mypy take on a *much* higher cognitive load.

@xgranade @whitequark or like… this? https://docs.astral.sh/ty/reference/rules/#ambiguous-protocol-member

that looks a lot like linting

@glyph @xgranade it is normal for a typechecker to include linting rules at the "warn" level. i mean even gcc has those

what is not normal / problematic for me in this context is having those be hard-rejects. "someone dreamed up a rule out of vibes and now i have to mangle perfectly well-formed code" is not something i accept

@whitequark @glyph Part of the ergonomic difference for me is that I do run ruff (sigh) with warnings as errors. Sometimes that results in false negatives (programs rejected that are valid). In those cases, I can leave a # noqa comment indicating why. 90% of the time that's an unused import that's actually used but it doesn't detect it, though I digress.

Declaring something as Any should be the polite way to spell "fuck off, type checker" but even *that* doesn't work in mypy... hence mangling.

@whitequark @glyph I think we have different philosophies on that, yeah... not even that I disagree, I just think of it differently? I'm happy working within what a tool wants me to do, it's something my mathy brain is OK with. Just tell me the goddamned rules.

Whereas that's something mypy does not do. The rules are, to your earlier point, vibed up.

@glyph @whitequark I mean, the example in question is ill-considered in the first place, I think. It's saying that I can assign a value to a variable in some cases but not others, even when the types are held invariant.

That aside, I think if mypy stuck to the documented rules of how Python types behave, *or* didn't call itself a type checker, I'd be much happier. Downgrading ad-hoc errors like func-returns-value to warnings is a good step towards that.

@glyph @whitequark I don't think so, no... it's a documented behavior of @functools.partial_ordering. In general, one of the main things that typing in Python does is formalize those kinds of requirements. That's basically a typeshed for the stdlib at that point.

The difference is that it doesn't matter how I get the class that violates the protocol, only that it does indeed violate it.

@glyph @whitequark I've definitely hit some, and should have written them down...

But yeah, None is one of the worst culprits. I see a lot of unit-vs-void confusion in GitHub issue threads, which doesn't inspire confidence that there might be a consensus to be found around mypy adopting a formal type system such as the one documented at docs.python.org.