`meet_types` gives unexpected results when meeting literal and Instance

[randolf-scholz]

The internal mypy.meet.meet_types function gives unexpected types, when one argument is a LiteralType, and the other is a Instance whose last_known_value is the other argument:

from mypy.meet import meet_types
from mypy.nodes import Block, ClassDef, SymbolTable, TypeInfo
from mypy.types import Instance, LiteralType, TypeOfAny

ST = SymbolTable()

def make_typeinfo(name: str, module_name: str = "__main__") -> TypeInfo:
    class_def = ClassDef(name, Block([]))  # Create a dummy ClassDef
    info = TypeInfo(ST, class_def, module_name)
    class_def.info = info  # circular reference
    return info

# Create demo types
str_info = make_typeinfo("str", module_name="builtins")
str_type = Instance(str_info, [], last_known_value=None)
max_literal = LiteralType("max", fallback=str_type)
max_instance = Instance(str_info, [], last_known_value=max_literal)

print("str_type:", str_type)                                  # str
print("max_literal:", max_literal)                            # Literal["max"]
print("max_instance:", max_instance)                          # Literal["max"]?
print(f"Meet type {meet_types(max_literal, max_instance)=}")  # Literal["max"]?
print(f"Meet type {meet_types(max_instance, max_literal)=}")  # Literal["max"]?

The predicted result is an Instance type with last_known_value=Literal["max"], but I think the result should be the LiteralType, since the former can be converted to plain str type later on, which would then be incorrect.

Similar issues are also present in the mypy.solve.solve_constraint function:

from mypy.constraints import SUBTYPE_OF, SUPERTYPE_OF, Constraint
from mypy.solve import solve_constraints
from mypy.types import AnyType, TypeVarId, TypeVarType

T = TypeVarType(
    "T",
    "T",
    id=TypeVarId(1),
    values=[],
    upper_bound=AnyType(TypeOfAny.unannotated),
    default=AnyType(TypeOfAny.unannotated),
)

uppers = [Constraint(T, SUBTYPE_OF, max_literal)]  # T <: Literal['max']
lowers = [Constraint(T, SUPERTYPE_OF, max_instance)]  # T >: Literal['max']?

print(f"solution={solve_constraints([T], lowers + uppers)}")  # Literal['max']?

[A5rocks]

cc @sterliakov (this behavior was added in #19279)

[sterliakov]

This is not #19279, I only touched join there, and with the opposite outcome: join(Instance(lkv=L), L) for some literal L returns L. Probably smth similar is needed in meet, but I don't exactly understand why: what's the actual problem caused by using an Instance with l.k.v. in this case?

can be converted to plain str type later on

yep, and so can Literal - it has a fallback type of Instance(builtins.str). Does it cause any externally observable issues? AFAIC the only problem of using an Instance with l.k.v. instead of Literal is that it may sometimes not be interpreted as a literal, breaking the inference, but not the promotion ability.

[A5rocks]

Oh sorry I just barely remembered "hey I think I saw something about this at some point" and found the PR. I should have taken a more thorough look!

[sterliakov]

Nah, never mind - it was a good idea to ping me here anyway:)

[randolf-scholz]

Does it cause any externally observable issues?

Well, I have been working on a PR that reworks inference for generic callables to fix a whole range of bugs. (Here's an earlier draft: #19399; I may push a more recent version soon)

Essentially, instead of the current two stage approach of first considering the outer context and then the inner, we do both simultaneously. Here's a case where this goes wrong due to this issue:

from typing import Mapping, Literal

x: Mapping[str, Literal["sum", "mean", "max", "min"]] = {"x": "sum"}

Here we consider the callable def [K, V](...) -> dict[K, V].

The outer constraints are: dict[K, V] <: Mapping[str, Literal["sum", "mean", "max", "min"]] which translates to

[1 <: builtins.str, 1 :> builtins.str, 2 <: Literal['sum'] | Literal['mean'] | Literal['max'] | Literal['min']]

and the inner constraints, based on the provided arguments are:

[1 :> Literal['x']?, 2 :> Literal['sum']?]

If we jointly solve these, we get

[builtins.str, Literal['sum']?]

Which somewhere later on gets coerced to [builtins.str, builtins.str], causing a [assignment] error.

Instead, if the solver produced [builtins.str, Literal['sum']], everything would be fine.

[sterliakov]

[builtins.str, Literal['sum']?]

And this is the correct type. Later conversion (erasing last known value) should not have happened in literal context. If it really makes other places much easier, maybe it's OK to try to change this, but in general Literal types should only be inferred in literal context (for meet/join - when at least one of the operands is a Literal type). I'd probably try to understand the reason for last known value erasure first, though.

[randolf-scholz]

but in general Literal types should only be inferred in literal context

What exactly do you mean by this? In my example, the variable is annotated with Mapping[str, Literal["sum", "mean", "max", "min"]]. Is this not a literal context?

(for meet/join - when at least one of the operands is a Literal type).

Which is the case for the example in #19560 (comment)

[randolf-scholz]

Sorry for being naive about the terminology here, but I would assume that a Literal context is whenever there appear type constraints referencing actual LiteralType types (rather than constraints containing just Literal? types)

[sterliakov]

Sorry, no, it was a rather general remark, it's fine to infer Literals here! My only point was that joining/meeting several Instances with l.k.v., for example, should never produce a Literal type - we try hard to never annoy people by inferring literals that prevent sound operations later.

And still the why is interesting, I don't see any obvious l.k.v. erasure between constraint solving and dict call checking.

[randolf-scholz]

My only point was that joining/meeting several Instances with l.k.v.,

Uhm, in the example only the lower bound is an instance, the upper bound is an actual LiteralType. What happens here is that within solve_one it exits here:

mypy/mypy/solve.py

Lines 321 to 322 in 07d4a1b

	elif is_subtype(bottom, top):
	candidate = bottom

Because it determines that Literal["sum"]? is a subtype of Literal["sum", "max", "min", "mean"].

A similar code is present in meet_type which causes the same behavior there:

mypy/mypy/meet.py

Lines 97 to 101 in 07d4a1b

	if not isinstance(s, UnboundType) and not isinstance(t, UnboundType):
	if is_proper_subtype(s, t, ignore_promotions=True):
	return s
	if is_proper_subtype(t, s, ignore_promotions=True):
	return t

It considers Literal[T]? a subtype of Literal[T] and so returns it as-is.

Maybe the problem here is related to the assignability vs subtype discussion? Literal[T]? should be assignable to Literal[T]. But should it really be a considered a subtype? Possibly this thing is in a similar category as Any, where it is a gradual subtype of Literal[T] and a gradual subtype of str.

[randolf-scholz]

Like to me, it would make sense (interpreting meet as intersection), and Literal? as the sort of gradual type mentioned above, if:

• meet(Literal["sum"]?, str) -> Literal["sum"]?
• meet(Literal["sum"]?, Literal["sum"]) -> Literal["sum"]
• meet(Literal["sum"]?, Literal["max"]) -> Never

[sterliakov]

Yes, looks reasonable! I agree current state is probably inconvenient. Let's try and see the tests and primer...