prefer more precise declared type over gradual inferred type

[carljm]

In a case like this:

from typing import Any

def f(x: Any):
    y: str = x
    reveal_type(y)

We currently reveal Any because we prefer inferred over declared type. But in this case that's counter productive because our inferred type is just Any.

One policy we could use here is that if the declared type is assignable to the inferred type, that suggests it is at least as precise, and we should prefer it.

[sharkdp]

if the declared type is assignable to the inferred type, that suggests it is at least as precise

Thinking about this again, that's obviously not true. If the types are reversed (declared type is Any, inferred type is str), they are also assignable.

I reopened this ticket because I found the following problem, which is somewhat reversed. Now the declared type is less precise, but that's exactly the intention of the author:

from typing import Any

_default: Any = object()

def f(x: int = _default):  # Red Knot: Default value of type `object` is not assignable to annotated parameter type `int`
    pass

https://playknot.ruff.rs/4b49ce75-02f7-49b1-a798-f9f6d0744d0a

[mikeshardmind]

A Policy I think would work well here to avoid clobbering developer intent, but would be more complex to implement.

• If both types result in no type errors, use the more precise one.
• If the declared type results in a type error, emit an error. (even if the inferred one doesn't, there's something wrong, possibly with the type declaration, not the runtime code)
• If the inferred type results in a type error, but the declared one doesn't and the value is assignable to the declared type, use the declared type.

The third part of this principle here also avoids what was a rather contentious issue with other type checkers and inference of Literal types causing type errors with invariant generics

A simpler rule to implement here would be to prefer the more precise type unless the declared type is a gradual type or the more precise type is only a refinement type of the declared type, otherwise use the declared type. This should cover all the cases currently within python's type system where preferring precision results in false positives that directly conflict with developer intent, but may become a more complex rule overall if the type system gains more than just Literal and LiteralStr for refinement types.

[carljm]

Unfortunately I think "results in a type error" is simply not feasible as a predicate for making this decision, implementation-wise. In principle the "resulting type error" could be anywhere in the code base, so effectively this heuristic would mean unbounded fixpoint iteration of the entire type-check.

Also I suspect that such a heuristic is not a good idea for user experience, either, because it would make the behavior very "jumpy" and subject to non-obvious non-local effects. Perhaps there really is a type error that needs to be fixed later in the function, but one interpretation of an earlier assignment "hides" that error with a gradual type -- are we sure that we should really prefer hiding the later error?

We will need to find a heuristic or principle that is predictable and local to the two types in the assignment.

If we want to base decisions on which type is "more precise", that also requires a definition of "more precise" in terms of subtyping and assignability; it's not self-evident what that definition is.

[mikeshardmind]

The simpler version can be restated as the following order of operations, which should not require any new definitions or specification clarity:

• If the declared type is gradual, and the inferred type is not, use the declared type.
• If the inferred type is a value-constrained form (refinement type, currently: Literals) of the declared type, use the declared type
• If the inferred type is a subtype by structural or nominal subtyping, use the inferred type
• otherwise, use the declared type

[carljm]

Now the declared type is less precise, but that's exactly the intention of the author

I think a fundamental question is whether we want to support that code example, without requiring a type: ignore. It seems obviously unsound, and can result in a function parameter annotated as int taking on a value that is not of type int. The author seems to desire that unsoundness, and is trying to use a declared type of Any as a way to silence the type checker. But red-knot currently doesn't interpret a declared type that way (as a form of cast), instead we interpret it as setting an upper bound on the types that can be assigned to a name.

[mikeshardmind]

That code example may have come from my own code based on a comment elsewhere. If so, It's used as a sentinel value where no default value is appropriate and should not change the public API The function needs to distinguish between no value provided without changing the types allowed to be passed. I'd be inclined to remove it if there was a better option here, but type checkers don't really allow for true divergence between public API and a default value which isn't allowed to be passed by a user in any other way.

Late bound defaults (pep 671) looked promising to me as a future better way, though that's still in draft.

If you've got another solution that works for this without arguably abusing the way Any is defined in the type system, I'd be less inclined to ask you to consider supporting this particular use.

That said, I think the set of steps I provided above is somewhat reasonable even outside of the case of Any, it should work without conflicting with developer intent with things like a fully known tuple vs variadic tuple (gradual length component), as well as avoid the issue of being too or less specific than a developer intended with Literals.

[carljm]

Isn't it possible to achieve this soundly today with overloads? Effectively you are wanting to "split" the public signature of the function from the private internal signature, and overloads permit this split:

from typing import overload

@overload
def f(x: int) -> int: ...

@overload
def f() -> int: ...

def f(x: int | None = None) -> int:
    if x is None:
        return 0
    return x

f()
f(1)
f(None)  # type error, there's no overload that accepts `None`

This is admittedly more verbose.

It's also of course possible to use the Any version with an explicit typing.cast to Any on the RHS instead of relying on type checkers ignoring a clearly-correct inferred type. This seems to me like a reasonable compromise when intentionally doing something unsound.

[mikeshardmind]

overloads have a problem where they have a runtime effect. Same with cast. This ruins other goals (no eager typing imports) that are frankly more important to me than satisfying a type checker for something where the immediate first line of the function is handling the default.

FWIW, This particular pattern has been noted as common in various peps researching it. See 671 for an example.

[mikeshardmind]

It's also of course possible to use the Any version with an explicit typing.cast to Any on the RHS instead of relying on type checkers ignoring a clearly-correct inferred type.

Oh, also there's a slight problem with calling it relying on inference behavior:

Any is the annotated type in a direct assignment, and this is accessible at a module level, there's no guarantee that the order of execution doesn't have another value assigned if this is modified in line with it's annotated type during import.

[mikeshardmind]

Oh, one more problem 🙃 (sorry, I missed it at first, responding too quickly)

your overload example isn't properly expressible if None is a valid input and there's an actual need for a sentinel object. There's no way to include the sentinel marker that's guaranteed unique (an instance of an object) without ruining the type checking of the body for the library:

compare this version for a fair comparison:

Code sample in pyright playground

[carljm]

I think the desire to not import typing can be managed with TYPE_CHECKING, even using overloads or cast.

I think the overload approach doesn't really have a problem with finding a sentinel value, assuming there is some type that is not a valid external input to the function. For example, if valid inputs are int | None, then you can't use None as sentinel, but the sentinel can be a string literal, etc. Of course this would be nicer with a dedicated sentinel type in the standard library.

It's a good point indeed that even local confidence in inferred types in module global scope is technically unsafe, given that any import could trigger external code that mutates this module's globals, and any call could trigger such an import, and almost any Python code can trigger a call (via dunder methods etc.), and we are currently choosing to ignore this possibility. This is a case where the unsoundness may be sufficiently rare in practice that the cure is worse than the disease, but I'm not averse to saying that in global scope we should always union the inferred type with the declared type (and with Unknown if no declared type) to reflect this possibility. But I would want to address the unsoundness via this union, not simply by ignoring the inferred type entirely, because the latter would allow way too many obvious type errors to pass silently. So with that union, we'd still error on the unsound-default pattern, because Any | object is not assignable to int.

[carljm]

Actually I think unions and intersections might provide an interesting generalized path forward here. In a scope where we don't consider arbitrary external mutation mid-execution to be possible (this is currently all scopes, but as mentioned above it could exclude module-global scope to be more sound), we could infer the intersection of the declared and inferred type, which is a formal way to say "it has to be both, and we want the most precise knowledge available". In cases without gradual types, this intersection would just simplify to the more precise inferred type, as we do today.

If we want to consider the possibility of arbitrarily-timed external mutation in module global scopes, then in that case we would want to take the union rather than the intersection. "We can only trust the declared type as upper bound, but the inferred type is a lower bound."

[mikeshardmind]

I think the desire to not import typing can be managed with TYPE_CHECKING, even using overloads or cast.

overload cannot without harming runtime introspection, a runtime use of inspect would get the incorrect annotation and no overloads to be found with typing.get_overloads

cast can, but I'm going to be very blunt, if someone ever writes:

if t.TYPE_CHECKING:
    x: t.Any = t.cast(t.Any, object())
else:
    x = object()

I'm going to tell them to just use a type ignore instead. object() is assignable to Any, and Any is what I have said via annotations is what a type checker should treat it as, I don't see any value in a type checker ignoring a developer use of Any in an inline assignment. That's a pretty significant sign they know they are doing something a type checker doesn't understand or working around some other issue.

[DiscordLiz]

we could infer the intersection of the declared and inferred type, which is a formal way to say "it has to be both, and we want the most precise knowledge available". In cases without gradual types, this intersection would just simplify to the more precise inferred type, as we do today.

I know intersections haven't been accepted yet, but wouldn't this mean the example should be fine? Any & T doesn't reduce based on all of the working discussion that has happened.

In fact, while I'm not positive on this (I think it works, but I'd need to work out the Literal interactions), I think in the case of a default value, the 4 step process that doesnt require any sort of recursive checking @mikeshardmind gave you here should be equivalent to what you propose under the current working definition of intersections without relying on a definition of intersections.

[carljm]

Red-knot already has intersections as a core part of our type model. All of our type narrowing is implemented exclusively through intersections and reduction of intersections. Our intersections behave as has been discussed (including that Any & T does not reduce). So "not relying on a definition of intersections" is an anti-goal for red-knot. We will much prefer to define our logic in terms of core primitives of gradual set-theoretic types (including intersections) which we've already implemented, rather than multi-step heuristics with at-first-glance arbitrary-seeming treatment of different kinds of types.

So yes, it's true that if we infer the intersection of the declared and inferred type, that means that a declared type of Any will allow subsequent uses that require a narrower type than the inferred type. I think this is defensible, as it does give the developer the option of using an explicit declared type of Any to express that there are known constraints on the type of this name that the developer is responsible for ensuring, and that aren't reflected in the type system. Annotating with Any is an unusual thing to do, and it's clearly expressing some kind of developer intent to opt that name out of type checking. (Otherwise, a variable annotation of Any in our model would be indistinguishable, in local-scope use of the name, from a variable annotation of object -- both would simply mean that any type can be assigned to the name in that scope.) If we do this, it will mean that un-annotated names are no longer equivalent to names explicitly annotated as Any (barring our Unknown/Any distinction) -- we will definitely not want to intersect the inferred type of unannotated names with Unknown.

The question is what we do in the module-global scope, if we decide that we should respect the possibility of external mutation of module globals while the module scope is mid-execution (which we should really probably have a separate issue to discuss.) I had suggested above that we union declared and inferred type in this case, but I think that's not consistent; if a variable annotation of Any in function scopes means "this could be an arbitrarily narrow type", then it should also mean that in module-global scope. I think that leads to the conclusion that we'd simply respect declared types only in module global scope, but I'm not sure I'm happy with the results of that for un-annotated names (they would simply be Unknown and lose all type checking.) EDIT: on second thought, I think the corollary of not intersecting Unknown with the inferred type in function scopes, would be that in module global scope we would infer the union of Unknown with the inferred type for un-declared names, so we would still get type-checking on that lower bound, and we'd infer solely the declared type for declared names. This seems potentially reasonable.