-
Notifications
You must be signed in to change notification settings - Fork 1.6k
[red-knot] Super-basic generic inference at call sites #17301
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Changes from 77 commits
3be8257
4c76cb5
8048604
fe76d56
4346e7d
2380ade
178ee89
feb1ea9
3c1ad79
59430b6
77ffa80
6f86720
cf81967
6615df1
b2f5a2a
590680c
e6b7d40
debd60a
aa391fd
e57e62e
3df79cc
5b08e93
82e810f
a3d7253
15682d5
9e07efe
fb63c22
3459056
71d425e
233e938
9785202
c86af50
aa00895
d99d1d7
58f0995
42fd54a
6bd69f1
1d6a917
37692f1
3869dc6
0c1745b
8bdd9e2
39244dd
5694b3d
123b920
9e1767f
23ac0b6
6b27947
669aa21
575998e
f02fefa
cc3a3df
18af8b6
af52fd1
d3fd822
aa64990
e41f889
7eb7c28
adb4aba
968e637
fd7914a
7ebda98
6257e89
78cd92a
530e2bc
637fd48
ec5a588
27cb208
ea12548
c376dad
311dc59
5fc8425
7aaeb47
43554e2
aec3392
595ecae
58830fa
0d656db
7c3405a
6593d90
7ca6a60
dea493e
048bb8b
06859fa
d138405
0997eca
6ab1b90
bcb147f
78f73fc
145a776
3a7b638
cccc77d
993c6e3
2169282
5a4bd28
756ce9a
1f67883
3cf9559
beb64b8
c1e3470
4bd8128
3734599
836d02c
0744540
701cfd1
d3067b0
4823f43
87f3f62
beed962
94bf3f6
8f43e30
f38b43e
54fb8a2
b852485
394c762
347547b
523ddcb
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -51,25 +51,10 @@ the inferred type to e.g. `int`. | |
| def f[T](x: T) -> T: | ||
| return x | ||
|
|
||
| # TODO: no error | ||
| # TODO: revealed: int or Literal[1] | ||
| # error: [invalid-argument-type] | ||
| reveal_type(f(1)) # revealed: T | ||
|
|
||
| # TODO: no error | ||
| # TODO: revealed: float | ||
| # error: [invalid-argument-type] | ||
| reveal_type(f(1.0)) # revealed: T | ||
|
|
||
| # TODO: no error | ||
| # TODO: revealed: bool or Literal[true] | ||
| # error: [invalid-argument-type] | ||
| reveal_type(f(True)) # revealed: T | ||
|
|
||
| # TODO: no error | ||
| # TODO: revealed: str or Literal["string"] | ||
| # error: [invalid-argument-type] | ||
| reveal_type(f("string")) # revealed: T | ||
| reveal_type(f(1)) # revealed: Literal[1] | ||
| reveal_type(f(1.0)) # revealed: float | ||
| reveal_type(f(True)) # revealed: Literal[True] | ||
| reveal_type(f("string")) # revealed: Literal["string"] | ||
| ``` | ||
|
|
||
| ## Inferring “deep” generic parameter types | ||
|
|
@@ -82,7 +67,7 @@ def f[T](x: list[T]) -> T: | |
| return x[0] | ||
|
|
||
| # TODO: revealed: float | ||
| reveal_type(f([1.0, 2.0])) # revealed: T | ||
| reveal_type(f([1.0, 2.0])) # revealed: Unknown | ||
| ``` | ||
|
|
||
| ## Typevar constraints | ||
|
|
@@ -162,61 +147,39 @@ parameters simultaneously. | |
| def two_params[T](x: T, y: T) -> T: | ||
| return x | ||
|
|
||
| # TODO: no error | ||
| # TODO: revealed: str | ||
| # error: [invalid-argument-type] | ||
| # error: [invalid-argument-type] | ||
| reveal_type(two_params("a", "b")) # revealed: T | ||
| reveal_type(two_params("a", "b")) # revealed: Literal["a", "b"] | ||
|
|
||
| # TODO: no error | ||
| # TODO: revealed: str | int | ||
| # error: [invalid-argument-type] | ||
| # error: [invalid-argument-type] | ||
| reveal_type(two_params("a", 1)) # revealed: T | ||
| reveal_type(two_params("a", 1)) # revealed: Literal["a", 1] | ||
| ``` | ||
|
|
||
| ```py | ||
| def param_with_union[T](x: T | int, y: T) -> T: | ||
| return y | ||
|
|
||
| # TODO: no error | ||
| # TODO: revealed: str | ||
| # error: [invalid-argument-type] | ||
| reveal_type(param_with_union(1, "a")) # revealed: T | ||
| reveal_type(param_with_union(1, "a")) # revealed: Literal["a"] | ||
|
||
|
|
||
| # TODO: no error | ||
| # TODO: revealed: str | ||
| # error: [invalid-argument-type] | ||
| # error: [invalid-argument-type] | ||
| reveal_type(param_with_union("a", "a")) # revealed: T | ||
| reveal_type(param_with_union("a", "a")) # revealed: Literal["a"] | ||
|
|
||
| # TODO: no error | ||
| # TODO: revealed: int | ||
| # error: [invalid-argument-type] | ||
| reveal_type(param_with_union(1, 1)) # revealed: T | ||
| reveal_type(param_with_union(1, 1)) # revealed: Literal[1] | ||
carljm marked this conversation as resolved.
Outdated
Show resolved
Hide resolved
|
||
|
|
||
| # TODO: no error | ||
| # TODO: revealed: str | int | ||
| # error: [invalid-argument-type] | ||
| # error: [invalid-argument-type] | ||
| reveal_type(param_with_union("a", 1)) # revealed: T | ||
| reveal_type(param_with_union("a", 1)) # revealed: Literal["a", 1] | ||
| ``` | ||
|
|
||
| ```py | ||
| def tuple_param[T, S](x: T | S, y: tuple[T, S]) -> tuple[T, S]: | ||
| return y | ||
|
|
||
| # TODO: no error | ||
| # TODO: revealed: tuple[str, int] | ||
| # error: [invalid-argument-type] | ||
| # error: [invalid-argument-type] | ||
| reveal_type(tuple_param("a", ("a", 1))) # revealed: tuple[T, S] | ||
| reveal_type(tuple_param("a", ("a", 1))) # revealed: tuple[Literal["a"], Literal[1]] | ||
|
|
||
| # TODO: no error | ||
| # TODO: revealed: tuple[str, int] | ||
| # error: [invalid-argument-type] | ||
| # error: [invalid-argument-type] | ||
| reveal_type(tuple_param(1, ("a", 1))) # revealed: tuple[T, S] | ||
| reveal_type(tuple_param(1, ("a", 1))) # revealed: tuple[Literal["a"], Literal[1]] | ||
| ``` | ||
|
|
||
| ## Inferring nested generic function calls | ||
|
|
@@ -231,15 +194,9 @@ def f[T](x: T) -> tuple[T, int]: | |
| def g[T](x: T) -> T | None: | ||
| return x | ||
|
|
||
| # TODO: no error | ||
| # TODO: revealed: tuple[str | None, int] | ||
| # error: [invalid-argument-type] | ||
| # error: [invalid-argument-type] | ||
| reveal_type(f(g("a"))) # revealed: tuple[T, int] | ||
| reveal_type(f(g("a"))) # revealed: tuple[Literal["a"] | None, int] | ||
|
|
||
| # TODO: no error | ||
| # TODO: revealed: tuple[str, int] | None | ||
| # error: [invalid-argument-type] | ||
| # error: [invalid-argument-type] | ||
| reveal_type(g(f("a"))) # revealed: T | None | ||
| reveal_type(g(f("a"))) # revealed: tuple[Literal["a"], int] | None | ||
| ``` | ||
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I am not actually convinced there's a strong rationale for this TODO. I don't think there is any function body for
two_paramsthat would type-check and allow it to return anything other than"a"or"b". Same for a number of similar TODOs below.But I could be wrong; not asking to have these TODOs removed in this PR, just putting it out there that I'm not convinced :)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
if revealed type of return value of function most be
Literal["a"] | Literal["b"], then it's incorrect type checking, since there is only one type var:T.in other words, it should get
Literal["a"]only when calling bytwo_params("a", "a"). but when callingtwo_params("a", "b"), both of "a" and "b" are different shape of literal strings and it should show error. but if revealed type becamestr, the call oftwo_params("a", "b")is acceptable.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't agree. There's nothing special about a union type in a set-theoretic type system.
Literal["a", "b"]is a well-defined single type, just as much asstris, and the single typevarTcan bind to the union type just as well as it can bind to any other type.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
IIUC,
Twould beLiteral["a", "b"]when call it byreveal_type(two_params("a", "b")).It now makes sense to me, thanks for clarification.
What I was thinking is that when first parameter passed (
"a"), thenTtypevar locks toLiteral["a"]and by second parameter which isLiteral["b"]it will invalidate theT. Actually, I had rust backgrounding of generics in my mind:BTW, it's valid in Python generics.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is a good way to think about how the implementation works here, and how it will need to grow to support some of the other mdtests that still have TODOs.
Right now, the only "solving" that we do is to see that the param is a typevar, and the argument is "some type", and add to the pending specialization that the typevar maps to the type. But if we've already seen that typevar in a different parameter, instead of replacing the previous type, or requiring the previous and new types to be the same (as you thought might be the case), we merge them together into a union. This is the only "unification" that the implementation in this PR does.
This first example in this section is one that this PR doesn't addres, where we'll need to not just blindly union everything together — the type annotation is meant to be an actual restriction that we should enforce.
Uh oh!
There was an error while loading. Please reload this page.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes, I think this is a very useful example, thank you! But (to rephrase what @dcreager already mentioned), no Python type checker actually supports the general principle that if
two_params(T1, T2)is OK, thereforef = curry_two_params(T1); f(T2)should also be OK. In both mypy and pyright,two_params("a", 1)is fine (Tis solved toint | str), butf = curry_two_params("a"); f(1)is a type error (fis(str) -> str).In other words, there's no difference in principle here, just a difference in semi-arbitrary widening heuristics, that makes the same issue appear at a different level of type granularity.
Perhaps the mypy/pyright approach is the best one available, in practice! But it would certainly be satisfying if we can find a more general answer that doesn't depend on heuristics.
One approach to solve this kind of issue is unification of a constraint system across the entire scope. But this is quite hard to reconcile with flow typing.
Uh oh!
There was an error while loading. Please reload this page.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think this is another form of the same problem:
The common thread in the examples is that a type is returned from a generic function in which a type parameter appears in an invariant/contravariant position.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Is this another place where we'd lean on
OneOf? The type oflist_of_what(and maybe the type of a literal in general?) would belist[OneOf[Literal[1], int]]. i.e.OneOfmight be shaping up to be the way that we handle "cross-expression" constraints in general.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I do think it's plausible that we can leverage gradual typing here, though I'm not sure we need
OneOfin this case, I think "union withUnknown" suffices. (UsingOneOfstill requires us to make the arbitrary judgment that you aren't supposed to add strings to this list.) The unionUnknown | Literal[1]expresses the gradual type "some type at least as large asLiteral[1]but possibly larger", which has the nice property that if you ever try to use it somewhere you can't use an integer, it'll error -- but it'll allow things other thanLiteral[1]to be assigned to it.I think at least two things we would need to make this approach work would be narrowing such that if you have a list
lof typelist[Unknown | Literal[1]]and you dol.append("foo"), we subsequently consider it to be of typelist[Unknown | Literal[1] | Literal["foo"].There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Removed the TODOs. If we decide to make this change, test failures will tell us all the places that need to be updated.