Type inference engine simplifies too aggressively

Reproduce the inference result with the plus_partial example, then inspect mypy's type-inference handling and the TypeRange introduced for #2993 and #2997. Compare the current upper-bound and precise-type cases with the requested lower- and upper-bound constraint; done means the example permits the safe plus_my_s(s) call without losing type safety.

This issue is broader than, but is closely related to, #3032.

Consider this code:

from typing import TypeVar, Callable

class Summable: ...
class MySummable(Summable): ...
T = TypeVar('T', bound=Summable)
def plus(a: T, b: T) -> T: ...

def plus_partial(t: T) -> Callable[[T], T]:
    def f(t1: T) -> T:
        return plus(t1, t)
    return f

my_s: MySummable
plus_my_s = plus_partial(my_s)

What should mypy infer for the type of plus_my_s?

The constraints are simple: T must be subtype of Summable because we use it in plus; and T must be supertype of MySummable because plus_partial has to accept my_s as an argument. So T has lower bound of MySummable and upper bound of Summable; any type within this range is fine.

Here, there's no such thing as the "most informative" ("optimal") type, since in the expression that plus_my_s is bound to , T appears both as a return type (covariant position) and as an argument type (contravariant). IOW, sometimes it's better to have T lower in the type hierarchy, sometimes higher. Therefore, mypy inference engine should not simplify the constraint any further, and just store the constraint itself internally.

However, mypy infers T == MySummable (and so, the type for plus_my_s is inferred as def (MySummable*) -> MySummable*). As a result, the following perfectly safe code fails type check:

s: Summable
plus_my_s(s)  # E: Argument 1 has incompatible type "Summable"; expected "MySummable"

even though direct use of plus would (of course) be accepted:

plus(my_s, s)  # ok

This could be fixed by supporting (at least internally) types with both upper and lower bounds (rather than only upper bound). A very similar problem came up in isinstance inference (#2993), which I fixed in #2997 by defining TypeRange that can store either a constraint with an upper bound, or a precise type.

Alternatively, this could be fixed by refusing to infer types in this situation and asking the user to provide annotation (although, the user is then out of luck if he actually wants to use partial_plus with both Summable and its subtypes - since we don't let users provide lower bounds for type variables).