Specify behavior for `Literal?` types.

[randolf-scholz]

Mypy's Literal? types are briefly documented here, however, their behavior is not completely specified.

Intuitively, a value like Literal["x"]? means that, depending on context, the value could be Literal["x"] or a plain str. This makes Literal["x"]? effectively a gradual type. I noticed some bugs with how mypy treats these types, most notably #19560. To holistically address such issues, I propose the following concrete specification:

0. prelim

Within this post, I interpret

• ≲ / mypy.subtypes.is_subtype as checking "assignable" / "consistent subtyping"
• <: / mypy.subtypes.is_proper_subtype as checking "(proper) subtyping"

If this is incorrect, please let me know.

1. AnyOf specification

We define:

1. x <: AnyOf[y₁, ..., yₙ] if and only if x <: Union[y₁, ..., yₙ]
2. x ≲ AnyOf[y₁, ..., yₙ] if and only if x ≲ yₖ for some k.
3. AnyOf[y₁, ...., yₙ] <: x if and only if Union[y₁, ..., yₙ] <: x
4. AnyOf[y₁, ...., yₙ] ≲ x if and only if yₖ ≲ x for all k.

2. Definition of Literal[T]?

Literal[T]? denotes a gradual type equivalent to one of

1. AnyOf[T, str] if T is a literal string
2. AnyOf[T, int] if T is a literal integer
3. AnyOf[T, bool] if T is a literal boolean
4. AnyOf[T, NoneType] if T is a lite
5. AnyOf[T, EnumType] if T is a literal enum

the first member is called its value, the latter its fallback.

It satisfies the following rules:

1. Literal[T]? is assignable to both its fallback and value.
2. Both its fallback and value are assignable to Literal[T]?.
3. Literal[T]? is a (proper) subtype of its fallback.
4. Its value is a proper subtype of Literal[T]?.
5. Literal[T]? is not a (proper) subtype of its value.
6. Its fallback is not a (proper) subtype of Literal[T]?.

Which (I think) makes Literal["x"]? essentially AnyOf[Literal["x"], str] (see python/typing#566)

Rationale:

• ① and ②: should be obvious.
• ③ and ④: is because in either case, when Literal["x"]? refers to Literal["x"] or when it refers to str,
  both times Literal["x"] is a proper subtype, and str a proper supertype.
• ⑤ and ⑥: are because the proper subtyping is not satisfied for both possible choices.

2. Changes to basic Ops

Below is a list of changes that derive from these rules and the assumption that meet and join are symmetric. These were generated using the following test script:

Details

from mypy.meet import meet_types
from mypy.join import join_types
from mypy.nodes import Block, ClassDef, SymbolTable, TypeInfo
from mypy.subtypes import restrict_subtype_away as restrict_types, is_proper_subtype, is_subtype, is_same_type
from mypy.types import Instance, LiteralType, TypeOfAny, AnyType, UnionType
from mypy.typeops import make_simplified_union as union


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_info.mro = [str_info] # Simplify MRO for this example
str_type = Instance(str_info, [], last_known_value=None)
max_litr = LiteralType("x", fallback=str_type)
sum_litr = LiteralType("y", fallback=str_type)
sum_inst = Instance(str_info, [], last_known_value=sum_litr)
max_inst = Instance(str_info, [], last_known_value=max_litr)
any_type = AnyType(TypeOfAny.unannotated)


print(f"\nMEET SCHEMA")
print(f"meet_types({max_litr!s:<16}, {str_type!s:<16}) = {meet_types(max_litr, str_type)}")
print(f"meet_types({str_type!s:<16}, {max_litr!s:<16}) = {meet_types(str_type, max_litr)}")
print(f"meet_types({max_inst!s:<16}, {str_type!s:<16}) = {meet_types(max_inst, str_type)}")
print(f"meet_types({str_type!s:<16}, {max_inst!s:<16}) = {meet_types(str_type, max_inst)}")
print(f"meet_types({max_litr!s:<16}, {max_litr!s:<16}) = {meet_types(max_litr, max_litr)}")
print(f"meet_types({max_litr!s:<16}, {max_inst!s:<16}) = {meet_types(max_litr, max_inst)}")
print(f"meet_types({max_inst!s:<16}, {max_litr!s:<16}) = {meet_types(max_inst, max_litr)}")
print(f"meet_types({max_inst!s:<16}, {max_inst!s:<16}) = {meet_types(max_inst, max_inst)}")
print(f"meet_types({max_litr!s:<16}, {sum_litr!s:<16}) = {meet_types(max_litr, sum_litr)}")
print(f"meet_types({max_litr!s:<16}, {sum_inst!s:<16}) = {meet_types(max_litr, sum_inst)}")
print(f"meet_types({max_inst!s:<16}, {sum_litr!s:<16}) = {meet_types(max_inst, sum_litr)}")
print(f"meet_types({max_inst!s:<16}, {sum_inst!s:<16}) = {meet_types(max_inst, sum_inst)}")

print(f"\nJOIN SCHEMA")
print(f"join_types({max_litr!s:<16}, {str_type!s:<16}) = {join_types(max_litr, str_type)}")
print(f"join_types({str_type!s:<16}, {max_litr!s:<16}) = {join_types(str_type, max_litr)}")
print(f"join_types({max_inst!s:<16}, {str_type!s:<16}) = {join_types(max_inst, str_type)}")
print(f"join_types({str_type!s:<16}, {max_inst!s:<16}) = {join_types(str_type, max_inst)}")
print(f"join_types({max_litr!s:<16}, {max_litr!s:<16}) = {join_types(max_litr, max_litr)}")
print(f"join_types({max_litr!s:<16}, {max_inst!s:<16}) = {join_types(max_litr, max_inst)}")
print(f"join_types({max_inst!s:<16}, {max_litr!s:<16}) = {join_types(max_inst, max_litr)}")
print(f"join_types({max_inst!s:<16}, {max_inst!s:<16}) = {join_types(max_inst, max_inst)}")
print(f"join_types({max_litr!s:<16}, {sum_litr!s:<16}) = {join_types(max_litr, sum_litr)}")
print(f"join_types({max_litr!s:<16}, {sum_inst!s:<16}) = {join_types(max_litr, sum_inst)}")
print(f"join_types({max_inst!s:<16}, {sum_litr!s:<16}) = {join_types(max_inst, sum_litr)}")
print(f"join_types({max_inst!s:<16}, {sum_inst!s:<16}) = {join_types(max_inst, sum_inst)}")

print(f"\nUNION SCHEMA")
print(f"union({max_litr!s:<16}, {str_type!s:<16}) = {union([max_litr, str_type])}")
print(f"union({str_type!s:<16}, {max_litr!s:<16}) = {union([str_type, max_litr])}")
print(f"union({max_inst!s:<16}, {str_type!s:<16}) = {union([max_inst, str_type])}")
print(f"union({str_type!s:<16}, {max_inst!s:<16}) = {union([str_type, max_inst])}")
print(f"union({max_litr!s:<16}, {max_litr!s:<16}) = {union([max_litr, max_litr])}")
print(f"union({max_litr!s:<16}, {max_inst!s:<16}) = {union([max_litr, max_inst])}")
print(f"union({max_inst!s:<16}, {max_litr!s:<16}) = {union([max_inst, max_litr])}")
print(f"union({max_inst!s:<16}, {max_inst!s:<16}) = {union([max_inst, max_inst])}")
print(f"union({max_litr!s:<16}, {sum_litr!s:<16}) = {union([max_litr, sum_litr])}")
print(f"union({max_litr!s:<16}, {sum_inst!s:<16}) = {union([max_litr, sum_inst])}")
print(f"union({max_inst!s:<16}, {sum_litr!s:<16}) = {union([max_inst, sum_litr])}")
print(f"union({max_inst!s:<16}, {sum_inst!s:<16}) = {union([max_inst, sum_inst])}")

print(f"\nRESTRICT SCHEMA")
print(f"restrict_types({max_litr!s:<16}, {str_type!s:<16}) = {restrict_types(max_litr, str_type)}")
print(f"restrict_types({str_type!s:<16}, {max_litr!s:<16}) = {restrict_types(str_type, max_litr)}")
print(f"restrict_types({max_inst!s:<16}, {str_type!s:<16}) = {restrict_types(max_inst, str_type)}")
print(f"restrict_types({str_type!s:<16}, {max_inst!s:<16}) = {restrict_types(str_type, max_inst)}")
print(f"restrict_types({max_litr!s:<16}, {max_litr!s:<16}) = {restrict_types(max_litr, max_litr)}")
print(f"restrict_types({max_litr!s:<16}, {max_inst!s:<16}) = {restrict_types(max_litr, max_inst)}")
print(f"restrict_types({max_inst!s:<16}, {max_litr!s:<16}) = {restrict_types(max_inst, max_litr)}")
print(f"restrict_types({max_inst!s:<16}, {max_inst!s:<16}) = {restrict_types(max_inst, max_inst)}")
print(f"restrict_types({max_litr!s:<16}, {sum_litr!s:<16}) = {restrict_types(max_litr, sum_litr)}")
print(f"restrict_types({max_litr!s:<16}, {sum_inst!s:<16}) = {restrict_types(max_litr, sum_inst)}")
print(f"restrict_types({max_inst!s:<16}, {sum_litr!s:<16}) = {restrict_types(max_inst, sum_litr)}")
print(f"restrict_types({max_inst!s:<16}, {sum_inst!s:<16}) = {restrict_types(max_inst, sum_inst)}")

print(f"\n SUBTYPE SCHEMA")
print(f"is_subtype({max_litr!s:<16}, {str_type!s:<16}) = {is_subtype(max_litr, str_type)}")
print(f"is_subtype({str_type!s:<16}, {max_litr!s:<16}) = {is_subtype(str_type, max_litr)}")
print(f"is_subtype({max_inst!s:<16}, {str_type!s:<16}) = {is_subtype(max_inst, str_type)}")
print(f"is_subtype({str_type!s:<16}, {max_inst!s:<16}) = {is_subtype(str_type, max_inst)}")
print(f"is_subtype({max_litr!s:<16}, {max_litr!s:<16}) = {is_subtype(max_litr, max_litr)}")
print(f"is_subtype({max_litr!s:<16}, {max_inst!s:<16}) = {is_subtype(max_litr, max_inst)}")
print(f"is_subtype({max_inst!s:<16}, {max_litr!s:<16}) = {is_subtype(max_inst, max_litr)}")
print(f"is_subtype({max_inst!s:<16}, {max_inst!s:<16}) = {is_subtype(max_inst, max_inst)}")
print(f"is_subtype({max_litr!s:<16}, {sum_litr!s:<16}) = {is_subtype(max_litr, sum_litr)}")
print(f"is_subtype({max_litr!s:<16}, {sum_inst!s:<16}) = {is_subtype(max_litr, sum_inst)}")
print(f"is_subtype({max_inst!s:<16}, {sum_litr!s:<16}) = {is_subtype(max_inst, sum_litr)}")
print(f"is_subtype({max_inst!s:<16}, {sum_inst!s:<16}) = {is_subtype(max_inst, sum_inst)}")

print(f"\n PROPER SUBTYPE SCHEMA")
print(f"is_proper_subtype({max_litr!s:<16}, {str_type!s:<16}) = {is_proper_subtype(max_litr, str_type)}")
print(f"is_proper_subtype({str_type!s:<16}, {max_litr!s:<16}) = {is_proper_subtype(str_type, max_litr)}")
print(f"is_proper_subtype({max_inst!s:<16}, {str_type!s:<16}) = {is_proper_subtype(max_inst, str_type)}")
print(f"is_proper_subtype({str_type!s:<16}, {max_inst!s:<16}) = {is_proper_subtype(str_type, max_inst)}")
print(f"is_proper_subtype({max_litr!s:<16}, {max_litr!s:<16}) = {is_proper_subtype(max_litr, max_litr)}")
print(f"is_proper_subtype({max_litr!s:<16}, {max_inst!s:<16}) = {is_proper_subtype(max_litr, max_inst)}")
print(f"is_proper_subtype({max_inst!s:<16}, {max_litr!s:<16}) = {is_proper_subtype(max_inst, max_litr)}")
print(f"is_proper_subtype({max_inst!s:<16}, {max_inst!s:<16}) = {is_proper_subtype(max_inst, max_inst)}")
print(f"is_proper_subtype({max_litr!s:<16}, {sum_litr!s:<16}) = {is_proper_subtype(max_litr, sum_litr)}")
print(f"is_proper_subtype({max_litr!s:<16}, {sum_inst!s:<16}) = {is_proper_subtype(max_litr, sum_inst)}")
print(f"is_proper_subtype({max_inst!s:<16}, {sum_litr!s:<16}) = {is_proper_subtype(max_inst, sum_litr)}")
print(f"is_proper_subtype({max_inst!s:<16}, {sum_inst!s:<16}) = {is_proper_subtype(max_inst, sum_inst)}")

print(f"\n SAME TYPE SCHEMA")
print(f"is_same_type({max_litr!s:<16}, {str_type!s:<16}) = {is_same_type(max_litr, str_type)}")
print(f"is_same_type({str_type!s:<16}, {max_litr!s:<16}) = {is_same_type(str_type, max_litr)}")
print(f"is_same_type({max_inst!s:<16}, {str_type!s:<16}) = {is_same_type(max_inst, str_type)}")
print(f"is_same_type({str_type!s:<16}, {max_inst!s:<16}) = {is_same_type(str_type, max_inst)}")
print(f"is_same_type({max_litr!s:<16}, {max_litr!s:<16}) = {is_same_type(max_litr, max_litr)}")
print(f"is_same_type({max_litr!s:<16}, {max_inst!s:<16}) = {is_same_type(max_litr, max_inst)}")
print(f"is_same_type({max_inst!s:<16}, {max_litr!s:<16}) = {is_same_type(max_inst, max_litr)}")
print(f"is_same_type({max_inst!s:<16}, {max_inst!s:<16}) = {is_same_type(max_inst, max_inst)}")
print(f"is_same_type({max_litr!s:<16}, {sum_litr!s:<16}) = {is_same_type(max_litr, sum_litr)}")
print(f"is_same_type({max_litr!s:<16}, {sum_inst!s:<16}) = {is_same_type(max_litr, sum_inst)}")
print(f"is_same_type({max_inst!s:<16}, {sum_litr!s:<16}) = {is_same_type(max_inst, sum_litr)}")
print(f"is_same_type({max_inst!s:<16}, {sum_inst!s:<16}) = {is_same_type(max_inst, sum_inst)}")

The feature results are based on commit 8dbc066 of PR #19605

MEET SCHEMA

left	right	master	feature	changed
"x"	str	"x"	"x"
str	"x"	"x"	"x"
"x"?	str	"x"?	"x"?
str	"x"?	str	"x"?	⚠️
"x"	"x"	"x"	"x"
"x"	"x"?	"x"	"x"
"x"?	"x"	"x"?	"x"	⚠️
"x"?	"x"?	"x"?	"x"?
"x"	"y"	Never	Never
"x"	"y"?	"x"	Never	⚠️
"x"?	"y"	"y"	Never	⚠️
"x"?	"y"?	"x"?	str	⚠️

JOIN SCHEMA

left	right	master	feature	changed
"x"	str	str	str
str	"x"	str	str
"x"?	str	str	str
str	"x"?	str	str
"x"	"x"	"x"	"x"
"x"	"x"?	"x"	"x"?	⚠️
"x"?	"x"	"x"	"x"?	⚠️
"x"?	"x"?	str	"x"?	⚠️
"x"	"y"	str	str	️
"x"	"y"?	str	str
"x"?	"y"	str	str
"x"?	"y"?	str	str

UNION SCHEMA

left	right	master	feature	changed
"x"	str	str	str
str	"x"	str	str
"x"?	str	str	str
str	"x"?	str	str
"x"	"x"	"x"	"x"
"x"	"x"?	"x"	"x"?	⚠️
"x"?	"x"	"x"	"x"?	⚠️
"x"?	"x"?	"x"?	"x"?
"x"	"y"	"x" | "y"	"x" | "y"
"x"	"y"?	"x" | "y"?	"x" | "y"?
"x"?	"y"	"x"? | "y"	"x"? | "y"
"x"?	"y"?	"x"? | "y"?	"x"? | "y"?

RESTRICT SCHEMA

left	right	master	feature	changed
"x"	str	Never	Never
str	"x"	str	str
"x"?	str	Never	Never
str	"x"?	Never	Never
"x"	"x"	Never	Never
"x"	"x"?	Never	Never
"x"?	"x"	"x"?	Never	⚠️
"x"?	"x"?	Never	Never
"x"	"y"	"x"	"x"
"x"	"y"?	Never	Never
"x"?	"y"	"x"?	"x"?
"x"?	"y"?	Never	Never

SUBTYPE SCHEMA

left	right	master	feature	changed
"x"	str	True	True
str	"x"	False	False
"x"?	str	True	True
str	"x"?	True	True
"x"	"x"	True	True
"x"	"x"?	True	True
"x"?	"x"	True	True
"x"?	"x"?	True	True
"x"	"y"	False	False
"x"	"y"?	True	True
"x"?	"y"	False	False
"x"?	"y"?	True	True

PROPER SUBTYPE SCHEMA

left	right	master	feature	changed
"x"	str	True	True
str	"x"	False	False
"x"?	str	True	True
str	"x"?	True	False	⚠️
"x"	"x"	True	True
"x"	"x"?	True	True
"x"?	"x"	True	False	⚠️
"x"?	"x"?	True	True
"x"	"y"	False	False
"x"	"y"?	True	False	⚠️
"x"?	"y"	False	False
"x"?	"y"?	True	False	⚠️

SAME TYPE SCHEMA

left	right	master	feature	changed
"x"	str	False	False
str	"x"	False	False
"x"?	str	True	False	⚠️
str	"x"?	True	False	⚠️
"x"	"x"	True	True
"x"	"x"?	True	False	⚠️
"x"?	"x"	True	False	⚠️
"x"?	"x"?	True	True
"x"	"y"	False	False
"x"	"y"?	False	False
"x"?	"y"	False	False
"x"?	"y"?	True	True

[randolf-scholz]

Some more comments on the proposed results:

1. meet

The proposed changes essentially derive from a version of the distributive law, interpreting meet as an intersection/AND and "x"? = AnyOf["x", str] as a union/OR:

• meet(x, y) ≝ max{z ∈ Lattice ∣ z <: x and z <: y} (z is a proper subtype of both x and y)
• I believe we have: meet(T, AnyOf[A, B]) ≲ AnyOf[meet(T, A), meet(T, B)],
  with equality if and only if AnyOf[meet(T, A), meet(T, B)] is a proper subtype of T and AnyOf[A, B] (proof tbd).

1. meet(str, "x"?) = meet(str, AnyOf["x", str]) = AnyOf[meet(str, "x"), meet(str, str)] = AnyOf["x", str] = "x"?
2. meet("x"?, "x") = meet(AnyOf["x", str], "x") = AnyOf[meet("x", "x"), meet(str, "x")] = AnyOf["x", "x"] = "x"
3. meet("x", "y"?) = meet("x", AnyOf["y", str]) = AnyOf[meet("x", "y"), meet("x", str)] = AnyOf[Never, "x"] = "x",
   but "x" is not a proper subtype of "y"?! So we get Never instead.
4. meet("x"?, "y") = meet(AnyOf["x", str], "y") = AnyOf[meet("x", "y"), meet(str, "y")] = AnyOf[Never, "y"] = "y",
   but "y" is not a proper subtype of "x"?! So we get Never instead.
5. meet("x"?, "y"?) = meet("x"?, AnyOf["y", str]) = AnyOf[meet("x"?, "y"), meet("x"?, str)] = AnyOf["y", "x", str],
   but AnyOf["y", "x", str] is not a proper subtype of "x"?! So we get str instead.

For the last case, since meet is a strong intersection (i.e. meet is the greatest lower bound, which structurally
would be the intersection type, but we only allow the meet to be an existing type in the lattice), i.e.

2. join

Again, using the distributive law, we can derive the following:

• join(x, y) ≝ min{z ∈ Lattice ∣ z :> x and z :> y} (z is a proper supertype of both x and y)
• I believe we have: join(T, AnyOf[A, B]) ≳ AnyOf[join(T, A), join(T, B)]
  with equality if and only if AnyOf[join(T, A), join(T, B)] is a proper supertype of T and AnyOf[A, B] (proof tbd).

Thus:

1. join("x", "x"?) = join("x", AnyOf["x", str]) ≳ AnyOf[join("x", "x"), join("x", str)] = AnyOf["x", str] = "x"? ⟹ join("x", "x"?)="x"?
2. join("x"?, "x"?) = join("x"?, AnyOf["x", str]) ≳ AnyOf[join("x"?, "x"), join("x"?, str)] = AnyOf["x"?, str] = "x"?

3. restriction

I am sure that the behavior on master (restrict("x"?, "x") -> "x"?) is not correct, but I am not sure what the correct resolution is.
We should have either:

1. restrict("x"?, "x") = str
2. restrict("x"?, "x") = Never

but not restrict("x"?, "x") = "x"? as it is on master. Currently, I opted for ② by modifying the covers_at_runtime function so that
Literal["x"] is considered to cover Literal["x"]? at runtime. I can see why one would want to do ①, but possibly this could produce some unexpected behavior
where a value is inferred as both Literal["x"] in the if and else branch, when this is not actually the case.