I think I see your point, but I'm not sure if changing how Literals interact with generics is the right way of resolving it. Basically, as a general philosophy, I think it's important to prioritize having the type system itself be as internally consistent as possible, even if that means it sometimes makes performing inference more challenging.

For example, one spec-compliant way Pyre could reducing the need for excessive lookahead would be to decide that TypeVars can never *implicitly* be bound to a Literal type. This is almost the same as the idea you proposed in the issue tracker, with the core difference that users would still be allowed to explicitly construct generics parameterized by Literals. So, writing type hints like "G[Literal[7]]" would still be legal and the limitations would just be in how you perform inference.

Another spec-compliant way that also makes the tension you talked about vanish entirely would be to continue to infer that all int expressions like "7" are of type int and make users jump through some hoops if they want it to have an inferred type of Literal[7] instead. The idea is that while Literal[7] might be just another subclass of int, there's no requirement saying that there needs to be an easy "constructor" for this subclass. (Granted, this would make actually using Literal types somewhat inconvenient, but neither this PEP nor PEP 484 requires high-quality type inference so...)

Finally, possibly one change I do think we could make is to have the spec require best-effort rather then full backwards compatibility instead. This would let type checkers not have to worry about preserving compatibility in every single edge case. Would that help in your case?

-- Michael

On Fri, Mar 15, 2019 at 8:35 AM Mark Mendoza <mendoza.mark.a@gmail.com> wrote:

Moving discussion from https://github.com/Michael0x2a/peps/pull/1 as requested

@Michael0x2a Sorry, missed that response, Github's threading confuses me sometimes :). I think you just about captured my concern, which was that you would have something like this
```
from typing import TypeVar, Generic
from typing_extensions import Literal, Final
T = TypeVar("T")

class G(Generic[T]): ...

def foo(x: T) -> G[T]: ...

def takesGOfInt(x: G[int]) -> None: ...
def takesGOfLiteral7(x: G[Literal[7]]) -> None: ...

def bar() -> None:
x = foo(7) # 7 inferred to be Literal[7], typevar rules means that returns G[Literal[7]]
reveal_type(x) # should this be G[Literal[7]] or G[int]?
# arbitrarily far later
takesGOfLiteral7(x) # error here?
takesGOfInt(x) # or here?
```
Mypy currently (0.670) errors on `takesGOfLiteral7` which seems to violate the idea that literals are just another subclass of int etc.
I'm not sure that we'd want to force this behavior in the spec, as it seems to necessitate having inference depend on the type of the parameter it's called on, which can get confusing quickly (especially with overloads etc.).
There seems to be an inherent tension between two goals of the spec, having Literals be just like any other subclass of int (or string etc.) and having backwards compatibility in all cases.
Is there another way to avoid that spec-wise other than removing the hard requirement of maintaining backwards compatibility in all cases?

- Mark Mendoza
_______________________________________________
Typing-sig mailing list -- typing-sig@python.org
To unsubscribe send an email to typing-sig-leave@python.org
https://mail.python.org/mailman3/lists/typing-sig.python.org/