I don't understand why you have Literal[2] here, where is this behaviour for _sage_input_ documented?

Also, Literal only works for Python literals. So Literal[2] means the int 2, not the Sage Integer 2.

It's defined here:

not the Sage Integer 2.

I don't think there is a good way to express this as a type.

not the Sage Integer 2.

I don't think there is a good way to express this as a type.

If Integer(2) is acceptable input (which I believe it is from some of the examples) then we can't use Literal[2] here. If only Integer(2) is acceptable then use Integer. If Integer(2) and int(2) are both acceptable then either Integer | int, or if you want to use Literal then Integer | Literal[2].

This is a good, simple example of the sage vs python integer typing issue we were discussing in the other PR.

My impression is that python is not aiming to become strongly typed but that the purpose of these type annotations is to mainly help developers write better code. Applying this philosophy here, the typing for coerced should reveal at least these two 'bugs':

1. Pass 1 or 3 (or another integer) as an argument to sage_input
2. Assume in the implementation of sage_input that it's always a boolean

So in particular, if you have an integer and you would like to pass it as coerced, you would want to check that it's equal to 2 before going ahead, eg using:

Integer num = ... 
if num == 2:
    _sage_input(..., num)
else:
    raise "expected num to be 2, but got ..."

At this point the type checker is able to deduct that num is the literal 2 (although it's not, it's only equal to it)

I feel like supporting (and highlighting the need) for such a pattern is more important than being 100% right about the typing info. One can always add a pyright: ignore comment if the typing is to strict/wrong, but one is sure to have covered the case correctly. Of course, you don't want to force to many such comments - it would be stupid to artificially restrict the possible input to int if half of sage's code is passing in Integer and that works well.

Curious what you think about it.

This ended up being a longer response than I expected, I've been thinking about type annotations a lot lately.

This is a good, simple example of the sage vs python integer typing issue we were discussing in the other PR.

Just thinking out loud, definitely don't do this in this PR and don't do this without a sage-devel discussion, but is there anything preventing Integer from being a subclass of int? It would solve a lot of annoyances with Integer. I'm guessing it would be too slow for such an important Sage object.

My impression is that python is not aiming to become strongly typed but that the purpose of these type annotations is to mainly help developers write better code.

Interesting, I think about it differently. My impression is that type annotations are for linters/type checkers to check that typing rules are respected without having to enforce type checking at runtime. But using Literal for parameters I think is beginning to veer into the territory of validating the values of inputs rather than just their types. So to me the utility of type annotations is the ability to have most of the benefits of strongly typed code without the runtime overhead by running a linter/type checker on the code which enforces the rules strictly. The more we adhere to this approach the more useful the type checkers will become (and the more bugs they'll be able to find). Perhaps user code does weirder things that respect the spirit but not the letter of type annotations (for example, a function that accepts Integer as a parameter but a user passes a Rational with denominator 1). Users shouldn't have to worry about details like that, and the nice thing about types not being checked at runtime is that something like that will (usually) work fine. I don't think many Sage users are running mypy or pyright on their Sage scripts. On the other hand, Sage developers should be expected to write slightly more explicit code that doesn't rely on the coercion system handling incorrect types (if only because relying on the coercion system will introduce overhead that could be avoided by more explicit code).

A big reason I favour the stricter annotations approach is that in theory it could be used by Cython to generate more efficient code one day (Cython's ability to use Python annotation is currently a bit limited though, but if we have strict type annotations then as Cython improves here so will the speed of Sage).

Something to consider: when Literal is used for a parameter, arguments cannot be a variable. So this is invalid:

def foo(a: Literal[5]) -> int:
    return a + 1

b = 5
foo(b)  # invalid, b is not a literal

That's kind of awkward, so I don't think I like Literal for parameters. It's probably best used only as a return type annotation for functions that return a constant (so things like .is_finite for objects that are always/never finite).

Curious what you think about it.

I think that we should use the most specific type annotation that is correct (doesn't require pyright: ignore). Having to use pyright: ignore defeats the purpose of type checking the function, the only time I'd use it is if there is a bug in the type checker and we don't want to wait for the type checker to get fixed before merging the PR. If it's legitimately too hard to come up with a correct annotation then we shouldn't annotate it. Or, just annotate it with the most specific correct thing (even if that annotation is more permissive than the function in reality). I don't think an annotation that is slightly too permissive is an issue. We probably have plenty of functions in Sage that accept only a positive Integer and check at runtime if the Integer is non-positive and raise an error if so, but I don't think there is a need to have a more specific PositiveInteger type.

Literal doesn't support Integer, so if a function accepts Integer then we can't use Literal there. I was discussing Literal with @fchapoton in #40972 and he thinks we should probably avoid it for now, and this situation seem like a good example of why we might want to avoid Literal. Personally I don't think Literal needs to always be avoided, but the only situation where I think it is likely to be useful is for return annotations, not parameter annotations (in #40972 (comment) I give an example of a hypothetical optimization Cython could make using Literal, but the Cython compiler doesn't currently have that optimization so it's a somewhat moot point).

(@fchapoton curious what you think about using Literal only for return but not parameter annotations.)

So for this PR, my suggestion is to change the annotation to bool | Integer | int, as this is the most specific correct annotation that avoids the Literal weirdness (even bool | Integer | Literal[2] is weird as the foo example above shows). Setting to needs work for now.

If you want to do a bit more as a separate PR, there is also my suggestion from #40634 (comment) to have a types.py module where we can define common type aliases/unions that are used in Sage (like Integer | int).

Thanks a lot! I don't have too much time at the moment to properly respond, but please have a look at this playground where I played around with your example:

https://pyright-play.net/?code=GYJw9gtgBALgngBwJYDsDmUkQWEMoAySMApiAIYA2AsAFB0AmJwUwYYAFOQFyHFlUA2gFYAugEooAWgB8mFDG50oKqCBIwAriBRRyUANRQAjHToAjKAF4owum07nJUAMTyAblSQMANFEtIAM5QKGD4%2BpT8FDT0tCia0DamtA4c8RDiZrSopGi8OdZQAORFrlCBkBoAFqgYqJ6RvlBhVWQA7kEksK3yudY2wpjBKCTuZFCjVJrkpAx6wQhwIEhoVfjqAMZgaChIAF4kwTBVM5j4G%2BQoofgnCAgkKHTqY1QA%2BvD3HDkkaJJuOfZ2F8FD9MrEkCxvhgrAMlLRVGpRiQ3h8SMDcn8%2BKRoiJRMpVKkoWCgA

The foo(b) call is not marked as invalid in this example, as pyright is able to properly recognize that b is Literal[5]. Some other code like

num = 1
foo(num)

is properly marked as invalid.

(Note that the behavior under mypy might be different - in my experience pyright is usually the better option.)

(Note that the behavior under mypy might be different - in my experience pyright is usually the better option.)

Good to know, I did use mypy for that example (I happened to have mypy but not pyright already installed).

Still, my suggestion is the same. Let's not use Literal for parameters for now (at least not for integers because the whole int vs Integer thing makes it too complicated). I don't want to rely on implementation-specific behaviour of one of the two major type checkers. From a quick reading of the differences, it seems pyright is probably the best choice for our CI at least since it's faster right now, but it looks like mypy also has some advantages. And mypy might get improvements in the future that make it preferable (mypyc looks very interesting, but it's in alpha right now).