More precise inferred type for literal ints

[grievejia]

Describe the Bug

Minimal repro:

reveal_type(1 + 2)

Expected: reveals Literal[3]
Actual: reveals int

Sandbox Link

https://pyrefly.org/sandbox/?code=GYJw9gtgBALgngBwJYDsDmUkQWEMogCmAboQIYA2A+vAoQFBGmU2KEAUAjFANRQBMASiA

(Only applicable for extension issues) IDE Information

No response

[yangdanny97]

Why do we want to do constant folding in a typechecker? Is there a real world example that would benefit from this?

[ndmitchell]

I think there is some limited benefit in some limited cases. + on int for example. Since people could define constants relative to each other. Bit or might be the other standard way.

[connernilsen]

For the good first issue tag, are there any pointers we could give for where to start looking at the changes that need to be made?

[purepani]

This seems like it shouldn't exist without support in the python typing system.
You would likely need to do something like

from typing import Self, Add
class NewInt:
    ...
    def __add__[M](self: Self, other: M) -> Add[Self, Other]

where Add is a new generic type. This then turns into a whole dependent typing system. I think this is likely not a good idea.

[erictraut]

FWIW, I added support for literal math in pyright about a year ago. It's a popular feature among pyright users, although the use cases it supports are admittedly somewhat niche.

@purepani, this would require more generalized support in the typing type system if it were extended beyond int, str and bytes types. However, the Literal special form in the type system is limited to specific classes. It doesn't support subclasses of int, for example. That makes it type safe to do "literal math" statically if both operands are known to be Literal types.

[yangdanny97]

@connernilsen

For the good first issue tag, are there any pointers we could give for where to start looking at the changes that need to be made?

Probably just add some special-casing to https://github.com/facebook/pyrefly/blob/main/pyrefly/lib/alt/operators.rs#L223

New test cases in https://github.com/facebook/pyrefly/blob/main/pyrefly/lib/test/operators.rs

A basic approach should be easy, but the devil is in the details

Some things to think about:

• what operations should we support? (for example, maybe we don't do division to avoid divide-by-zero or dealing with floats)
• operations between two unions of literals can cause a big blowup - how do we deal with that? (Eric's link explains how Pyright does it - but there are other ways, like not doing this for unions at all)
• not doing this in loops/lambdas like Pyright seems sensible but it does complicate the implementation a bit

[martindemello]

I feel like operations on unions of literals should fall back to the non literal type, the reasoning being that a single literal could represent a precise value that some niche cases might want to track operations on as part of the type system, and a union of literals might semantically be an enum, but the cross product of two unions of literals is very unlikely to represent something the type system cares about. (maybe a units library could contrive a use case)