diff --git a/mypy/join.py b/mypy/join.py
index a074fa522588..ec9649642594 100644
--- a/mypy/join.py
+++ b/mypy/join.py
@@ -141,11 +141,18 @@ def join_instances(self, t: Instance, s: Instance) -> ProperType:
                     new_type = join_types(ta, sa, self)
                 assert new_type is not None
                 args.append(new_type)
-            result: ProperType = Instance(t.type, args)
+            lkv = t.last_known_value if t.last_known_value == s.last_known_value else None
+            result: ProperType = Instance(t.type, args, last_known_value=lkv)
         elif t.type.bases and is_proper_subtype(
             t, s, subtype_context=SubtypeContext(ignore_type_params=True)
         ):
             result = self.join_instances_via_supertype(t, s)
+        elif s.type.bases and is_proper_subtype(
+            s, t, subtype_context=SubtypeContext(ignore_type_params=True)
+        ):
+            result = self.join_instances_via_supertype(s, t)
+        elif is_subtype(t, s, subtype_context=SubtypeContext(ignore_type_params=True)):
+            result = self.join_instances_via_supertype(t, s)
         else:
             # Now t is not a subtype of s, and t != s. Now s could be a subtype
             # of t; alternatively, we need to find a common supertype. This works
@@ -626,13 +633,17 @@ def visit_typeddict_type(self, t: TypedDictType) -> ProperType:
     def visit_literal_type(self, t: LiteralType) -> ProperType:
         if isinstance(self.s, LiteralType):
             if t == self.s:
+                # E.g. Literal["x"], Literal["x"] -> Literal["x"]
                 return t
             if self.s.fallback.type.is_enum and t.fallback.type.is_enum:
                 return mypy.typeops.make_simplified_union([self.s, t])
+            # E.g. Literal["x"], Literal["y"] -> str
             return join_types(self.s.fallback, t.fallback)
         elif isinstance(self.s, Instance) and self.s.last_known_value == t:
-            return t
+            # E.g. Literal["x"], Literal["x"]? -> Literal["x"]?
+            return self.s
         else:
+            # E.g. Literal["x"], Literal["y"]? -> str
             return join_types(self.s, t.fallback)
 
     def visit_partial_type(self, t: PartialType) -> ProperType:
diff --git a/mypy/meet.py b/mypy/meet.py
index c11d7d5d1aaa..5b73d66dfb72 100644
--- a/mypy/meet.py
+++ b/mypy/meet.py
@@ -81,6 +81,11 @@ def meet_types(s: Type, t: Type) -> ProperType:
     t = get_proper_type(t)
 
     if isinstance(s, Instance) and isinstance(t, Instance) and s.type == t.type:
+        # special casing for dealing with last known values
+        lkv = meet_last_known_values(t.last_known_value, s.last_known_value)
+        t = t.copy_modified(last_known_value=lkv)
+        s = s.copy_modified(last_known_value=lkv)
+
         # Code in checker.py should merge any extra_items where possible, so we
         # should have only compatible extra_items here. We check this before
         # the below subtype check, so that extra_attrs will not get erased.
@@ -113,6 +118,30 @@ def meet_types(s: Type, t: Type) -> ProperType:
     return t.accept(TypeMeetVisitor(s))
 
 
+def meet_last_known_values(
+    left: LiteralType | None, right: LiteralType | None
+) -> LiteralType | None:
+    """Return the meet of two last_known_values."""
+    if left is None:
+        return right
+    if right is None:
+        return left
+
+    lkv_meet = meet_types(left, right)
+
+    if isinstance(lkv_meet, UninhabitedType):
+        return None
+    if isinstance(lkv_meet, LiteralType):
+        return lkv_meet
+
+    msg = (
+        f"Unexpected result: "
+        f"meet of last_known_values {left=!s} and {right=!s} "
+        f"resulted in {lkv_meet!s}"
+    )
+    raise ValueError(msg)
+
+
 def narrow_declared_type(declared: Type, narrowed: Type) -> Type:
     """Return the declared type narrowed down to another type."""
     # TODO: check infinite recursion for aliases here.
@@ -1114,8 +1143,14 @@ def visit_typeddict_type(self, t: TypedDictType) -> ProperType:
     def visit_literal_type(self, t: LiteralType) -> ProperType:
         if isinstance(self.s, LiteralType) and self.s == t:
             return t
-        elif isinstance(self.s, Instance) and is_subtype(t.fallback, self.s):
-            return t
+        elif isinstance(self.s, Instance):
+            # if is_subtype(t.fallback, self.s):
+            #     return t
+            if self.s.last_known_value is not None:
+                # meet(Literal["max"]?, Literal["max"]) -> Literal["max"]
+                # meet(Literal["sum"]?, Literal["max"]) -> Never
+                return meet_types(self.s.last_known_value, t)
+            return self.default(self.s)
         else:
             return self.default(self.s)
 
diff --git a/mypy/solve.py b/mypy/solve.py
index e3709106996c..b2ea2037652e 100644
--- a/mypy/solve.py
+++ b/mypy/solve.py
@@ -319,7 +319,8 @@ def solve_one(lowers: Iterable[Type], uppers: Iterable[Type]) -> Type | None:
     elif top is None:
         candidate = bottom
     elif is_subtype(bottom, top):
-        candidate = bottom
+        # Need to meet in case like Literal["x"]? <: T <: Literal["x"]
+        candidate = meet_types(bottom, top)
     else:
         candidate = None
     return candidate
diff --git a/mypy/subtypes.py b/mypy/subtypes.py
index 350d57a7e4ad..7d32221e35a0 100644
--- a/mypy/subtypes.py
+++ b/mypy/subtypes.py
@@ -548,6 +548,13 @@ def visit_instance(self, left: Instance) -> bool:
                     assert isinstance(erased, Instance)
                     t = erased
                 nominal = True
+                if self.proper_subtype and right.last_known_value is not None:
+                    if left.last_known_value is None:
+                        # E.g. str is not a proper subtype of Literal["x"]?
+                        nominal = False
+                    else:
+                        # E.g. Literal[A]? <: Literal[B]? requires A <: B
+                        nominal &= self._is_subtype(left.last_known_value, right.last_known_value)
                 if right.type.has_type_var_tuple_type:
                     # For variadic instances we simply find the correct type argument mappings,
                     # all the heavy lifting is done by the tuple subtyping.
@@ -628,8 +635,14 @@ def visit_instance(self, left: Instance) -> bool:
                         return True
                     if isinstance(item, Instance):
                         return is_named_instance(item, "builtins.object")
-        if isinstance(right, LiteralType) and left.last_known_value is not None:
-            return self._is_subtype(left.last_known_value, right)
+        if isinstance(right, LiteralType):
+            if self.proper_subtype:
+                # Instance types like Literal["sum"]? is *assignable* to Literal["sum"],
+                # but is not a proper subtype of it. (Literal["sum"]? is a gradual type,
+                # that is a proper subtype of str, and assignable to Literal["sum"].
+                return False
+            if left.last_known_value is not None:
+                return self._is_subtype(left.last_known_value, right)
         if isinstance(right, FunctionLike):
             # Special case: Instance can be a subtype of Callable / Overloaded.
             call = find_member("__call__", left, left, is_operator=True)
@@ -964,6 +977,12 @@ def visit_typeddict_type(self, left: TypedDictType) -> bool:
     def visit_literal_type(self, left: LiteralType) -> bool:
         if isinstance(self.right, LiteralType):
             return left == self.right
+        elif (
+            isinstance(self.right, Instance)
+            and self.right.last_known_value is not None
+            and self.proper_subtype
+        ):
+            return self._is_subtype(left, self.right.last_known_value)
         else:
             return self._is_subtype(left.fallback, self.right)
 
@@ -2138,6 +2157,11 @@ def covers_at_runtime(item: Type, supertype: Type) -> bool:
     item = get_proper_type(item)
     supertype = get_proper_type(supertype)
 
+    # Use last known value for Instance types, if available.
+    # This ensures that e.g. Literal["max"]? is covered by Literal["max"].
+    if isinstance(item, Instance) and item.last_known_value is not None:
+        item = item.last_known_value
+
     # Since runtime type checks will ignore type arguments, erase the types.
     if not (isinstance(supertype, FunctionLike) and supertype.is_type_obj()):
         supertype = erase_type(supertype)
diff --git a/mypy/test/testsubtypes.py b/mypy/test/testsubtypes.py
index b75c22bca7f7..5be32f628de1 100644
--- a/mypy/test/testsubtypes.py
+++ b/mypy/test/testsubtypes.py
@@ -1,7 +1,7 @@
 from __future__ import annotations
 
 from mypy.nodes import CONTRAVARIANT, COVARIANT, INVARIANT
-from mypy.subtypes import is_subtype
+from mypy.subtypes import is_proper_subtype, is_subtype, restrict_subtype_away
 from mypy.test.helpers import Suite
 from mypy.test.typefixture import InterfaceTypeFixture, TypeFixture
 from mypy.types import Instance, TupleType, Type, UninhabitedType, UnpackType
@@ -277,6 +277,74 @@ def test_type_var_tuple_unpacked_variable_length_tuple(self) -> None:
     def test_fallback_not_subtype_of_tuple(self) -> None:
         self.assert_not_subtype(self.fx.a, TupleType([self.fx.b], fallback=self.fx.a))
 
+    def test_literal(self) -> None:
+        str1 = self.fx.lit_str1
+        str2 = self.fx.lit_str2
+        str1_inst = self.fx.lit_str1_inst
+        str2_inst = self.fx.lit_str2_inst
+        str_type = self.fx.str_type
+
+        # other operand is the fallback type
+        # "x"  ≲ str  -> YES
+        # str  ≲ "x"  -> NO
+        # "x"? ≲ str  -> YES
+        # str  ≲ "x"? -> YES
+        self.assert_subtype(str1, str_type)
+        self.assert_not_subtype(str_type, str1)
+        self.assert_subtype(str1_inst, str_type)
+        self.assert_subtype(str_type, str1_inst)
+
+        # other operand is the same literal
+        # "x"  ≲ "x"  -> YES
+        # "x"  ≲ "x"? -> YES
+        # "x"? ≲ "x"  -> YES
+        # "x"? ≲ "x"? -> YES
+        self.assert_subtype(str1, str1)
+        self.assert_subtype(str1, str1_inst)
+        self.assert_subtype(str1_inst, str1)
+        self.assert_subtype(str1_inst, str1_inst)
+
+        # other operand is a different literal
+        # "x"  ≲ "y"  -> NO
+        # "x"  ≲ "y"? -> YES
+        # "x"? ≲ "y"  -> NO
+        # "x"? ≲ "y"? -> YES
+        self.assert_not_subtype(str1, str2)
+        self.assert_subtype(str1, str2_inst)
+        self.assert_not_subtype(str1_inst, str2)
+        self.assert_subtype(str1_inst, str2_inst)
+
+        # check proper subtyping
+        # other operand is the fallback type
+        # "x"  <: str  -> YES
+        # str  <: "x"  -> NO
+        # "x"? <: str  -> YES
+        # str  <: "x"? -> NO
+        self.assert_proper_subtype(str1, str_type)
+        self.assert_not_proper_subtype(str_type, str1)
+        self.assert_proper_subtype(str1_inst, str_type)
+        self.assert_not_proper_subtype(str_type, str1_inst)
+
+        # other operand is the same literal
+        # "x"  <: "x"  -> YES
+        # "x"  <: "x"? -> YES
+        # "x"? <: "x"  -> NO
+        # "x"? <: "x"? -> YES
+        self.assert_proper_subtype(str1, str1)
+        self.assert_proper_subtype(str1, str1_inst)
+        self.assert_not_proper_subtype(str1_inst, str1)
+        self.assert_proper_subtype(str1_inst, str1_inst)
+
+        # other operand is a different literal
+        # "x"  <: "y"  -> NO
+        # "x"  <: "y"? -> NO
+        # "x"? <: "y"  -> NO
+        # "x"? <: "y"? -> NO
+        self.assert_not_proper_subtype(str1, str2)
+        self.assert_not_proper_subtype(str1, str2_inst)
+        self.assert_not_proper_subtype(str1_inst, str2)
+        self.assert_not_proper_subtype(str1_inst, str2_inst)
+
     # IDEA: Maybe add these test cases (they are tested pretty well in type
     #       checker tests already):
     #  * more interface subtyping test cases
@@ -287,6 +355,12 @@ def test_fallback_not_subtype_of_tuple(self) -> None:
     #  * any type
     #  * generic function types
 
+    def assert_proper_subtype(self, s: Type, t: Type) -> None:
+        assert is_proper_subtype(s, t), f"{s} not proper subtype of {t}"
+
+    def assert_not_proper_subtype(self, s: Type, t: Type) -> None:
+        assert not is_proper_subtype(s, t), f"{s} not proper subtype of {t}"
+
     def assert_subtype(self, s: Type, t: Type) -> None:
         assert is_subtype(s, t), f"{s} not subtype of {t}"
 
@@ -304,3 +378,53 @@ def assert_equivalent(self, s: Type, t: Type) -> None:
     def assert_unrelated(self, s: Type, t: Type) -> None:
         self.assert_not_subtype(s, t)
         self.assert_not_subtype(t, s)
+
+
+class RestrictionSuite(Suite):
+    # Tests for type restrictions "A - B", i.e. ``T <: A and not T <: B``.
+
+    def setUp(self) -> None:
+        self.fx = TypeFixture()
+
+    def assert_restriction(self, s: Type, t: Type, expected: Type) -> None:
+        actual = restrict_subtype_away(s, t)
+        msg = f"restrict_subtype_away({s}, {t}) == {{}} ({{}} expected)"
+        self.assertEqual(actual, expected, msg=msg.format(actual, expected))
+
+    def test_literal(self) -> None:
+        str1 = self.fx.lit_str1
+        str2 = self.fx.lit_str2
+        str1_inst = self.fx.lit_str1_inst
+        str2_inst = self.fx.lit_str2_inst
+        str_type = self.fx.str_type
+        uninhabited = self.fx.uninhabited
+
+        # other operand is the fallback type
+        # "x" - str -> Never
+        # str - "x" -> str
+        # "x"? - str  -> Never
+        # str  - "x"? -> Never
+        self.assert_restriction(str1, str_type, uninhabited)
+        self.assert_restriction(str_type, str1, str_type)
+        self.assert_restriction(str1_inst, str_type, uninhabited)
+        self.assert_restriction(str_type, str1_inst, uninhabited)
+
+        # other operand is the same literal
+        # "x"  - "x"  -> Never
+        # "x"  - "x"? -> Never
+        # "x"? - "x"  -> Never
+        # "x"? - "x"? -> Never
+        self.assert_restriction(str1, str1, uninhabited)
+        self.assert_restriction(str1, str1_inst, uninhabited)
+        self.assert_restriction(str1_inst, str1, uninhabited)
+        self.assert_restriction(str1_inst, str1_inst, uninhabited)
+
+        # other operand is a different literal
+        # "x"  - "y"  -> "x"
+        # "x"  - "y"? -> Never
+        # "x"? - "y"  -> "x"?
+        # "x"? - "y"? -> Never
+        self.assert_restriction(str1, str2, str1)
+        self.assert_restriction(str1, str2_inst, uninhabited)
+        self.assert_restriction(str1_inst, str2, str1_inst)
+        self.assert_restriction(str1_inst, str2_inst, uninhabited)
diff --git a/mypy/test/testtypes.py b/mypy/test/testtypes.py
index f5f4c6797db2..ae36befec6bd 100644
--- a/mypy/test/testtypes.py
+++ b/mypy/test/testtypes.py
@@ -589,7 +589,7 @@ def test_simplified_union_with_literals(self) -> None:
             [fx.lit1_inst, fx.lit3_inst], UnionType([fx.lit1_inst, fx.lit3_inst])
         )
         self.assert_simplified_union([fx.lit1_inst, fx.uninhabited], fx.lit1_inst)
-        self.assert_simplified_union([fx.lit1, fx.lit1_inst], fx.lit1)
+        self.assert_simplified_union([fx.lit1, fx.lit1_inst], fx.lit1_inst)
         self.assert_simplified_union([fx.lit1, fx.lit2_inst], UnionType([fx.lit1, fx.lit2_inst]))
         self.assert_simplified_union([fx.lit1, fx.lit3_inst], UnionType([fx.lit1, fx.lit3_inst]))
 
@@ -639,7 +639,46 @@ def test_simplified_union_with_mixed_str_literals(self) -> None:
             [fx.lit_str1, fx.lit_str2, fx.lit_str3_inst],
             UnionType([fx.lit_str1, fx.lit_str2, fx.lit_str3_inst]),
         )
-        self.assert_simplified_union([fx.lit_str1, fx.lit_str1, fx.lit_str1_inst], fx.lit_str1)
+        self.assert_simplified_union(
+            [fx.lit_str1, fx.lit_str1, fx.lit_str1_inst], fx.lit_str1_inst
+        )
+
+    def test_simplified_union_with_mixed_str_literals2(self) -> None:
+        str1 = self.fx.lit_str1
+        str2 = self.fx.lit_str2
+        str1_inst = self.fx.lit_str1_inst
+        str2_inst = self.fx.lit_str2_inst
+        str_type = self.fx.str_type
+
+        # other operand is the fallback type
+        # "x"  | str  -> str
+        # str  | "x"  -> str
+        # "x"? | str  -> str
+        # str  | "x"? -> str
+        self.assert_simplified_union([str1, str_type], str_type)
+        self.assert_simplified_union([str_type, str1], str_type)
+        self.assert_simplified_union([str1_inst, str_type], str_type)
+        self.assert_simplified_union([str_type, str1_inst], str_type)
+
+        # other operand is the same literal
+        # "x"  | "x"  -> "x"
+        # "x"  | "x"? -> "x"?
+        # "x"? | "x"  -> "x"?
+        # "x"? | "x"? -> "x"?
+        self.assert_simplified_union([str1, str1], str1)
+        self.assert_simplified_union([str1, str1_inst], str1_inst)
+        self.assert_simplified_union([str1_inst, str1], str1_inst)
+        self.assert_simplified_union([str1_inst, str1_inst], str1_inst)
+
+        # other operand is a different literal
+        # "x"  | "y"  -> "x"  | "y"
+        # "x"  | "y"? -> "x"  | "y"?
+        # "x"? | "y"  -> "x"? | "y"
+        # "x"? | "y"? -> "x"? | "y"?
+        self.assert_simplified_union([str1, str2], UnionType([str1, str2]))
+        self.assert_simplified_union([str1, str2_inst], UnionType([str1, str2_inst]))
+        self.assert_simplified_union([str1_inst, str2], UnionType([str1_inst, str2]))
+        self.assert_simplified_union([str1_inst, str2_inst], UnionType([str1_inst, str2_inst]))
 
     def assert_simplified_union(self, original: list[Type], union: Type) -> None:
         assert_equal(make_simplified_union(original), union)
@@ -999,6 +1038,39 @@ def test_literal_type(self) -> None:
             UnionType([lit2, lit3]), UnionType([lit1, lit2]), UnionType([lit2, lit3, lit1])
         )
 
+    def test_mixed_literal_types(self) -> None:
+        str1 = self.fx.lit_str1
+        str2 = self.fx.lit_str2
+        str1_inst = self.fx.lit_str1_inst
+        str2_inst = self.fx.lit_str2_inst
+        str_type = self.fx.str_type
+
+        # other operand is the fallback type
+        # "x" , str  -> str
+        # str , "x"  -> str
+        # "x"?, str  -> str
+        # str , "x"? -> str
+        self.assert_join(str1, str_type, str_type)
+        self.assert_join(str1_inst, str_type, str_type)
+
+        # other operand is the same literal
+        # "x" , "x"  -> "x"
+        # "x" , "x"? -> "x"?
+        # "x"?, "x"  -> "x"?
+        # "x"?, "x"? -> "x"?
+        self.assert_join(str1, str1, str1)
+        self.assert_join(str1, str1_inst, str1_inst)
+        self.assert_join(str1_inst, str1_inst, str1_inst)
+
+        # other operand is a different literal
+        # "x" , "y"  -> str (TODO: consider using "x" | "y" (treat real literals like enum))
+        # "x" , "y"? -> str
+        # "x"?, "y"  -> str
+        # "x"?, "y"? -> str
+        self.assert_join(str1, str2, str_type)
+        self.assert_join(str1, str2_inst, str_type)
+        self.assert_join(str1_inst, str2_inst, str_type)
+
     def test_variadic_tuple_joins(self) -> None:
         # These tests really test just the "arity", to be sure it is handled correctly.
         self.assert_join(
@@ -1321,6 +1393,39 @@ def test_literal_type(self) -> None:
         assert is_same_type(lit1, narrow_declared_type(lit1, a))
         assert is_same_type(lit2, narrow_declared_type(lit2, a))
 
+    def test_mixed_literal_types(self) -> None:
+        str1 = self.fx.lit_str1
+        str2 = self.fx.lit_str2
+        str1_inst = self.fx.lit_str1_inst
+        str2_inst = self.fx.lit_str2_inst
+        str_type = self.fx.str_type
+
+        # other operand is the fallback type
+        # "x" , str -> "x"
+        # str , "x" -> "x"
+        # "x"?, str  -> "x"?
+        # str , "x"? -> "x"?
+        self.assert_meet(str1, str_type, str1)
+        self.assert_meet(str1_inst, str_type, str1_inst)
+
+        # other operand is the same literal
+        # "x" , "x"  -> "x"
+        # "x" , "x"? -> "x"
+        # "x"?, "x"  -> "x"
+        # "x"?, "x"? -> "x"?
+        self.assert_meet(str1, str1, str1)
+        self.assert_meet(str1, str1_inst, str1)
+        self.assert_meet(str1_inst, str1_inst, str1_inst)
+
+        # other operand is a different literal
+        # "x" , "y"  -> Never
+        # "x" , "y"? -> Never
+        # "x"?, "y"  -> Never
+        # "x"?, "y"? -> str
+        self.assert_meet_uninhabited(str1, str2)
+        self.assert_meet_uninhabited(str1, str2_inst)
+        self.assert_meet(str1_inst, str2_inst, str_type)
+
     # FIX generic interfaces + ranges
 
     def assert_meet_uninhabited(self, s: Type, t: Type) -> None:
diff --git a/mypy/typeops.py b/mypy/typeops.py
index 02e1dbda514a..6dbd45a5f356 100644
--- a/mypy/typeops.py
+++ b/mypy/typeops.py
@@ -580,6 +580,8 @@ def make_simplified_union(
     * [int, Any] -> Union[int, Any] (Any types are not simplified away!)
     * [Any, Any] -> Any
     * [int, Union[bytes, str]] -> Union[int, bytes, str]
+    * [Literal[1]?, Literal[1]] -> Literal[1]?
+    * Literal["max"]?, Literal["max", "sum"] -> Literal["max"]? | Literal["sum"]
 
     Note: This must NOT be used during semantic analysis, since TypeInfos may not
           be fully initialized.
@@ -608,13 +610,22 @@ def make_simplified_union(
     ):
         simplified_set = try_contracting_literals_in_union(simplified_set)
 
+    # Step 5: Combine Literals and Instances with LKVs, e.g. Literal[1]?, Literal[1] -> Literal[1]?
+    proper_items: list[ProperType] = [get_proper_type(t) for t in simplified_set]
+    last_known_values: list[LiteralType | None] = [
+        p_t.last_known_value if isinstance(p_t, Instance) else None for p_t in proper_items
+    ]
+    simplified_set = [
+        item for item, p_t in zip(simplified_set, proper_items) if p_t not in last_known_values
+    ]
+
     result = get_proper_type(UnionType.make_union(simplified_set, line, column))
 
     nitems = len(items)
     if nitems > 1 and (
         nitems > 2 or not (type(items[0]) is NoneType or type(items[1]) is NoneType)
     ):
-        # Step 5: At last, we erase any (inconsistent) extra attributes on instances.
+        # Step 6: At last, we erase any (inconsistent) extra attributes on instances.
 
         # Initialize with None instead of an empty set as a micro-optimization. The set
         # is needed very rarely, so we try to avoid constructing it.
diff --git a/test-data/unit/check-inference.test b/test-data/unit/check-inference.test
index 7f970487bbe7..1aafee2f8d5a 100644
--- a/test-data/unit/check-inference.test
+++ b/test-data/unit/check-inference.test
@@ -4173,7 +4173,7 @@ def check_and(maybe: bool) -> None:
     bar = None
     if maybe and (foo := [1])[(bar := 0)]:
         reveal_type(foo)  # N: Revealed type is "builtins.list[builtins.int]"
-        reveal_type(bar)  # N: Revealed type is "builtins.int"
+        reveal_type(bar)  # N: Revealed type is "Literal[0]?"
     else:
         reveal_type(foo)  # N: Revealed type is "builtins.list[builtins.int] | None"
         reveal_type(bar)  # N: Revealed type is "builtins.int | None"
@@ -4199,7 +4199,7 @@ def check_or(maybe: bool) -> None:
         reveal_type(bar)  # N: Revealed type is "builtins.int | None"
     else:
         reveal_type(foo)  # N: Revealed type is "builtins.list[builtins.int]"
-        reveal_type(bar)  # N: Revealed type is "builtins.int"
+        reveal_type(bar)  # N: Revealed type is "Literal[0]?"
 
 def check_or_nested(maybe: bool) -> None:
     foo = None
diff --git a/test-data/unit/check-literal.test b/test-data/unit/check-literal.test
index d71370eb4191..ddb6ddc3c00a 100644
--- a/test-data/unit/check-literal.test
+++ b/test-data/unit/check-literal.test
@@ -3092,18 +3092,46 @@ z: Type[Literal[1, 2]]  # E: Type[...] can't contain "Union[Literal[...], Litera
 [case testJoinLiteralAndInstance]
 from typing import Generic, TypeVar, Literal
 
-T = TypeVar("T")
+T_co = TypeVar("T_co", covariant=True)
+T = TypeVar("T", covariant=False, contravariant=False)
+S = TypeVar("S", covariant=False, contravariant=False)
 
-class A(Generic[T]): ...
+class A_inv(Generic[T]): ...
+class A_co(Generic[T_co]): ...
 
-def f(a: A[T], t: T) -> T: ...
-def g(a: T, t: A[T]) -> T: ...
+def check_inv(obj: A_inv[Literal[1]]) -> None:
+    def f(a: A_inv[S], t: S) -> S: ...
+    def g(a: S, t: A_inv[S]) -> S: ...
 
-def check(obj: A[Literal[1]]) -> None:
     reveal_type(f(obj, 1))  # N: Revealed type is "Literal[1]"
-    reveal_type(f(obj, ''))  # E: Cannot infer value of type parameter "T" of "f" \
-                             # N: Revealed type is "Any"
+    reveal_type(f(obj, '')) # E: Cannot infer value of type parameter "S" of "f" \
+                            # N: Revealed type is "Any"
     reveal_type(g(1, obj))  # N: Revealed type is "Literal[1]"
-    reveal_type(g('', obj))  # E: Cannot infer value of type parameter "T" of "g" \
-                             # N: Revealed type is "Any"
+    reveal_type(g('', obj)) # E: Cannot infer value of type parameter "S" of "g" \
+                            # N: Revealed type is "Any"
+
+def check_co(obj: A_co[Literal[1]]) -> None:
+    def f(a: A_co[S], t: S) -> S: ...
+    def g(a: S, t: A_co[S]) -> S: ...
+
+    reveal_type(f(obj, 1))   # N: Revealed type is "builtins.int"
+    reveal_type(f(obj, ''))  # N: Revealed type is "builtins.object"
+    reveal_type(g(1, obj))   # N: Revealed type is "builtins.int"
+    reveal_type(g('', obj))  # N: Revealed type is "builtins.object"
+
+[case testJoinLiteralInstanceAndEnum]
+from typing import Final, TypeVar
+from enum import StrEnum
+
+T = TypeVar("T")
+def join(a: T, b: T) -> T: ...
+
+class Foo(StrEnum):
+    A = "a"
+
+CONST: Final = "const"
+
+reveal_type(CONST)  # N: Revealed type is "Literal['const']?"
+reveal_type(join(Foo.A, CONST))  # N: Revealed type is "builtins.str"
+reveal_type(join(CONST, Foo.A))  # N: Revealed type is "builtins.str"
 [builtins fixtures/tuple.pyi]
diff --git a/test-data/unit/check-python310.test b/test-data/unit/check-python310.test
index 98d625958368..85aa52f80bd0 100644
--- a/test-data/unit/check-python310.test
+++ b/test-data/unit/check-python310.test
@@ -1520,7 +1520,7 @@ m: str
 
 match m:
     case a if a := "test":
-        reveal_type(a)  # N: Revealed type is "builtins.str"
+        reveal_type(a)  # N: Revealed type is "Literal['test']?"
 
 [case testMatchNarrowingPatternGuard]
 m: object
@@ -2848,7 +2848,7 @@ def int_literal() -> None:
         case other:
             other  # E: Statement is unreachable
 
-def str_literal() -> None:
+def str_literal_from_literal() -> None:
     match 'foo':
         case 'a' as s:
             reveal_type(s)  # E: Statement is unreachable
@@ -2857,6 +2857,16 @@ def str_literal() -> None:
         case other:
             other  # E: Statement is unreachable
 
+
+def str_literal_from_str(arg: str) -> None:
+    match arg:
+        case 'a' as s:
+            reveal_type(s)  # N: Revealed type is "Literal['a']"
+        case str(i):
+            reveal_type(i)  # N: Revealed type is "builtins.str"
+        case other:
+            other  # E: Statement is unreachable
+
 [case testMatchOperations]
 # flags: --warn-unreachable
 
diff --git a/test-data/unit/check-python38.test b/test-data/unit/check-python38.test
index c32dec94a62d..8e1df01973a3 100644
--- a/test-data/unit/check-python38.test
+++ b/test-data/unit/check-python38.test
@@ -214,10 +214,10 @@ i(arg=0)  # E: Unexpected keyword argument "arg"
 from typing import Final, NamedTuple, Optional, List
 
 if a := 2:
-    reveal_type(a)  # N: Revealed type is "builtins.int"
+    reveal_type(a)  # N: Revealed type is "Literal[2]?"
 
 while b := "x":
-    reveal_type(b)  # N: Revealed type is "builtins.str"
+    reveal_type(b)  # N: Revealed type is "Literal['x']?"
 
 l = [y2 := 1, y2 + 2, y2 + 3]
 reveal_type(y2)  # N: Revealed type is "builtins.int"
@@ -242,10 +242,10 @@ reveal_type(new_v)  # N: Revealed type is "builtins.int"
 
 def f(x: int = (c := 4)) -> int:
     if a := 2:
-        reveal_type(a)  # N: Revealed type is "builtins.int"
+        reveal_type(a)  # N: Revealed type is "Literal[2]?"
 
     while b := "x":
-        reveal_type(b)  # N: Revealed type is "builtins.str"
+        reveal_type(b)  # N: Revealed type is "Literal['x']?"
 
     x = (y := 1) + (z := 2)
     reveal_type(x)  # N: Revealed type is "builtins.int"
@@ -284,7 +284,7 @@ def f(x: int = (c := 4)) -> int:
     f(x=(y7 := 3))
     reveal_type(y7)  # N: Revealed type is "builtins.int"
 
-    reveal_type((lambda: (y8 := 3) and y8)())  # N: Revealed type is "builtins.int"
+    reveal_type((lambda: (y8 := 3) and y8)())  # N: Revealed type is "Literal[3]?"
     y8  # E: Name "y8" is not defined
 
     y7 = 1.0  # E: Incompatible types in assignment (expression has type "float", variable has type "int")
@@ -325,16 +325,16 @@ def check_binder(x: Optional[int], y: Optional[int], z: Optional[int], a: Option
         reveal_type(y)  # N: Revealed type is "builtins.int | None"
 
     if x and (y := 1):
-        reveal_type(y)  # N: Revealed type is "builtins.int"
+        reveal_type(y)  # N: Revealed type is "Literal[1]?"
 
     if (a := 1) and x:
-        reveal_type(a)  # N: Revealed type is "builtins.int"
+        reveal_type(a)  # N: Revealed type is "Literal[1]?"
 
     if (b := 1) or x:
         reveal_type(b)  # N: Revealed type is "builtins.int"
 
     if z := 1:
-        reveal_type(z)  # N: Revealed type is "builtins.int"
+        reveal_type(z)  # N: Revealed type is "Literal[1]?"
 
 def check_partial() -> None:
     x = None
diff --git a/test-data/unit/check-warnings.test b/test-data/unit/check-warnings.test
index a2d201fa301d..25aec01566b5 100644
--- a/test-data/unit/check-warnings.test
+++ b/test-data/unit/check-warnings.test
@@ -49,13 +49,27 @@ from typing import cast
 a = 1
 b = cast(object, 1)
 
-[case testCastFromLiteralRedundant]
-# flags: --warn-redundant-casts
-from typing import cast
+[case testLiteralRedundantCast]
+# https://github.com/python/mypy/issues/19055
+# flags: --warn-redundant-cast
 
-cast(int, 1)
-[out]
-main:4: error: Redundant cast to "int"
+from typing import Literal, cast
+
+# "a" is an AnyOf[str, Literal["a"]], denoted Literal['a']?
+# See: https://github.com/python/typing/issues/566
+
+# This cast is not redundant because Literal["a"]? is not identical to Literal["a"]
+LiteralOnly = Literal["a"]
+reveal_type("a")  # N: Revealed type is "Literal['a']?"
+cast(LiteralOnly, "a")
+
+# This cast is redundant because the type is already Literal["a"]
+already_literal: Literal["a"] = "a"
+reveal_type(already_literal)  # N: Revealed type is "Literal['a']"
+cast(LiteralOnly, already_literal)  # E: Redundant cast to "Literal['a']"
+
+LiteralUnion = Literal["a", "b"]
+cast(LiteralUnion, "a")
 
 [case testCastFromUnionOfAnyOk]
 # flags: --warn-redundant-casts