[red-knot] No panic for illegal self-referential f-string annotations

[sharkdp]

Summary

I went down another rabbit hole trying to fix all sorts of panics related to illegal type expressions. Some highlights from the linter corpus:

x: f"{x}"
x: (y := x)
x: lambda y: y
type X = Annotated[int, lambda: re.compile("x")]

This fixes the last two remaining entries in KNOWN_FAILURES except for those related to salsa-cycles. But I really don't know if the approach taken here — to infer Type::Unknown for sub-expressions of illegal expressions — is the right one. And even if it is, I'm not sure if my implementation of it is fully correct (see for example the exception for expressions with an inner scope). I thought I'd still open a PR so we can discuss the general problem.

Side remark: After having fixed a few of those panics over the last weeks, my impression is that our approach to upholding the invariant "we infer and store a type for each and every expression, even if illegal in this context" is extremely brittle. The only way we enforce it right now is through the corpus tests. But there is an exponentially large number of branches in type inference (or alternatively: an exponentially large number of weird edge cases like the above), which makes me think that we might need another way to enforce this constraint, e.g. at the (Rust) type-system level instead of the test level.

Test Plan

cargo nextest run -p red_knot_workspace -- --ignored linter_af linter_gz

[github-actions]

ruff-ecosystem results

Linter (stable)

✅ ecosystem check detected no linter changes.

Linter (preview)

✅ ecosystem check detected no linter changes.

[AlexWaygood]

Side remark: After having fixed a few of those panics over the last weeks, my impression is that our approach to upholding the invariant "we infer and store a type for each and every expression, even if illegal in this context" is extremely brittle. The only way we enforce it right now is through the corpus tests. But there is an exponentially large number of branches in type inference (or alternatively: an exponentially large number of weird edge cases like the above), which makes me think that we might need another way to enforce this constraint, e.g. at the (Rust) type-system level instead of the test level.

I definitely agree with this, if it's possible. But I haven't thought at all about how we might redesign our infrastructure to make this possible!

[AlexWaygood]

There are several type annotations on this line, and it's hard to tell which annotation this is referring to without counting the columns. Could we improve the error message so it specifies which variable or annotation the diagnostic is complaining about?

[MichaReiser]

Including arbitrary expressions is something that I'm always worried about because it can lead to very long messages, but including the name might be an option or David can come up with something that avoids this.

What should help here is when we have rich diagnostics that also show a code frame

[sharkdp]

When I wrote that error message, I was looking for something like a ast::Expr::human_readable_name() method that would return "lambda expression" for a Expr::Lambda etc., but didn't find anything.

I'm happy to improve this error message though once we agree that this is even the right approach to begin with.

What should help here is when we have rich diagnostics that also show a code frame

👍

[AlexWaygood]

What should help here is when we have rich diagnostics that also show a code frame

That should help for sure, but it's also useful to have important information in the summary line for when a user is using --output-format=concise. I found --output-format=concise to be very useful when filing PRs to upgrade projects to Ruff 0.8, because there were many new violations on some codebases, and it was very hard to scroll through them all when using the default verbose output.

[AlexWaygood]

But I really don't know if the approach taken here — to infer Type::Unknown for sub-expressions of illegal expressions — is the right one. And even if it is, I'm not sure if my implementation of it is fully correct (see for example the exception for expressions with an inner scope). I thought I'd still open a PR so we can discuss the general problem.

Yeah, I'm not sure about this either. I think there are two reasons why we want to infer types for all sub-expressions:

1. So that you get a useful tool-tip telling you what the type of something is when you hover over a subexpression of a type annotation in a red-knot-powered IDE
2. In the long term, we want to rewrite Ruff to use red-knot as a semantic-inference backend, and we may have rules that want to know the type of subexpressions of annotations even when the overall annotation is invalid. (Some rules might want type information even if the rule itself is not about enforcing valid annotations or types.)

I think inferring Unknown for all subexpressions of invalid annotations is probably okay for the first of these (if the annotation is invalid, it's invalid), but probably not great for the second of these.

[carljm]

our approach to upholding the invariant "we infer and store a type for each and every expression, even if illegal in this context" is extremely brittle.

Yeah, I agree. I'm having a hard time thinking of how we could enforce this invariant in the type system. (At least without major re-architecting.)

I think I am reaching the conclusion that we should just have a default fallback to Unknown for any expression that we've failed to store a type for, and if we discover cases where we have Unknown where there should be a more precise type, we treat that as a bug like any other type inference bug, fix it and add a test.

I think this seems like the right answer to me in particular due to invalid syntax, because a) we can't reasonably expect to cover the full space of possible invalid syntax with any testing strategy, and b) I think, in general, Unknown is the right answer for invalid syntax cases that we cannot understand otherwise.

I think inferring Unknown for all subexpressions of invalid annotations is probably okay for the first of these (if the annotation is invalid, it's invalid), but probably not great for the second of these.

I'm not sure it isn't the best option for the second, too. How symbols in type expressions are interpreted is contextual, and if we've departed from a valid context, I think it's reasonable to say that we really don't know what the type of sub-expressions should be.

[carljm]

I would be more inclined to switch to a default fallback of Unknown at lookup time (instead of panic), rather than adding all this infrastructure to walk a tree and store an explicit Unknown for everything in it.

But I don't feel strongly about it, and won't object if this PR is merged as-is.

[AlexWaygood]

I think inferring Unknown for all subexpressions of invalid annotations is probably okay for the first of these (if the annotation is invalid, it's invalid), but probably not great for the second of these.

I'm not sure it isn't the best option for the second, too. How symbols in type expressions are interpreted is contextual, and if we've departed from a valid context, I think it's reasonable to say that we really don't know what the type of sub-expressions should be.

But remember that we won't just be using red-knot from the linter for its type-inference capabilities, but also for its more general "symbol-aware" capabilities.

For example, take PYI062. This rule tries to detect duplicate members in a literal slice. When it's ported to red-knot, it will need to work largely off the AST, as it does now, because in our red-knot representation of a Literal annotation we'll eagerly deduplicate Literal elements as we add them to a UnionType. But the rule still needs to know that the symbol Literal is actually the symbol typing.Literal or typing_extensions.Literal before it starts traversing the AST, and for that it needs red-knot's multifile type-inference capabilities. It doesn't really matter for that rule whether the Literal slice occurs in the context of an annotation that is overall invalid; it can still do an accurate analysis of the Literal slice inside the invalid annotation. But if we infer Unknown for all subexpressions in the annotation, we won't be able to inform that rule whether or not the symbol Literal is actually typing(_extensions).Literal or if it's some other Literal symbol.

[carljm]

Yes, I understood all of that from your first comment. This is the assumption I'm not sure I agree with:

It doesn't really matter for that rule whether the Literal slice occurs in the context of an annotation that is overall invalid; it can still do an accurate analysis of the Literal slice inside the invalid annotation.

I'm not sure it's reasonable to expect that rule to fire inside an arbitrary invalid context, because the meaning of these expressions is contextual.

For example, the first "argument" to Annotated is not a type expression: should that lint rule fire on a Literal slice that occurs there?

[AlexWaygood]

For example, the first "argument" to Annotated is not a type expression: should that lint rule fire on a Literal slice that occurs there?

Yes, I think it should! It's just as much an error to have duplicate elements in a Literal slice even if the Literal is not part of a type expression, because the typing module at runtime eagerly deduplicates elements:

>>> from typing import Literal
>>> Literal[1, 1]
typing.Literal[1]

So even if the Literal is part of the first argument to Annotated for whatever reason, it's always going to be incorrect to pass duplicate elements to the Literal slice.

[carljm]

Yes, I see that it would be nice to correctly infer the type of a reference to something like typing.Literal in any context.

I wish we weren't constrained by Salsa query granularity, so we didn't have to do the extra work of type inference on expressions that are useless for type checking, just because a lint rule or an LSP hover might (but probably in many cases never will) ask for it.

[AlexWaygood]

I wish we weren't constrained by Salsa query granularity, so we didn't have to do the extra work of type inference on expressions that are useless for type checking, just because a lint rule or an LSP hover might (but probably in many cases never will) ask for it.

Right. Though the consolation here is that invalid annotations should generally be pretty rare in well-written code, so the "extra cost" of inferring sub-expressions in these invalid annotations should be pretty minimal, I'd wager.