diff --git a/mypy/checkexpr.py b/mypy/checkexpr.py
index 76d247986e47..ef31ed9e5e3a 100644
--- a/mypy/checkexpr.py
+++ b/mypy/checkexpr.py
@@ -210,7 +210,10 @@ def analyze_ref_expr(self, e: RefExpr, lvalue: bool = False) -> Type:
 
     def analyze_var_ref(self, var: Var, context: Context) -> Type:
         if var.type:
-            return var.type
+            if is_literal_type_like(self.type_context[-1]) and var.name() in {'True', 'False'}:
+                return LiteralType(var.name() == 'True', self.named_type('builtins.bool'))
+            else:
+                return var.type
         else:
             if not var.is_ready and self.chk.in_checked_function():
                 self.chk.handle_cannot_determine_type(var.name(), context)
@@ -1721,11 +1724,17 @@ def analyze_external_member_access(self, member: str, base_type: Type,
 
     def visit_int_expr(self, e: IntExpr) -> Type:
         """Type check an integer literal (trivial)."""
-        return self.named_type('builtins.int')
+        typ = self.named_type('builtins.int')
+        if is_literal_type_like(self.type_context[-1]):
+            return LiteralType(value=e.value, fallback=typ)
+        return typ
 
     def visit_str_expr(self, e: StrExpr) -> Type:
         """Type check a string literal (trivial)."""
-        return self.named_type('builtins.str')
+        typ = self.named_type('builtins.str')
+        if is_literal_type_like(self.type_context[-1]):
+            return LiteralType(value=e.value, fallback=typ)
+        return typ
 
     def visit_bytes_expr(self, e: BytesExpr) -> Type:
         """Type check a bytes literal (trivial)."""
@@ -3583,3 +3592,17 @@ def merge_typevars_in_callables_by_name(
         output.append(target)
 
     return output, variables
+
+
+def is_literal_type_like(t: Optional[Type]) -> bool:
+    """Returns 'true' if the given type context is potentially either a LiteralType,
+    a Union of LiteralType, or something similar.
+    """
+    if t is None:
+        return False
+    elif isinstance(t, LiteralType):
+        return True
+    elif isinstance(t, UnionType):
+        return any(is_literal_type_like(item) for item in t.items)
+    else:
+        return False
diff --git a/mypy/constraints.py b/mypy/constraints.py
index 7e1ac22bb3b8..71a601a03853 100644
--- a/mypy/constraints.py
+++ b/mypy/constraints.py
@@ -260,6 +260,9 @@ def visit_erased_type(self, template: ErasedType) -> List[Constraint]:
     def visit_deleted_type(self, template: DeletedType) -> List[Constraint]:
         return []
 
+    def visit_literal_type(self, template: LiteralType) -> List[Constraint]:
+        return []
+
     # Errors
 
     def visit_partial_type(self, template: PartialType) -> List[Constraint]:
@@ -472,9 +475,6 @@ def visit_typeddict_type(self, template: TypedDictType) -> List[Constraint]:
         else:
             return []
 
-    def visit_literal_type(self, template: LiteralType) -> List[Constraint]:
-        raise NotImplementedError()
-
     def visit_union_type(self, template: UnionType) -> List[Constraint]:
         assert False, ("Unexpected UnionType in ConstraintBuilderVisitor"
                        " (should have been handled in infer_constraints)")
diff --git a/mypy/join.py b/mypy/join.py
index faf5860bd86e..9a0c4c102bce 100644
--- a/mypy/join.py
+++ b/mypy/join.py
@@ -163,6 +163,8 @@ def visit_instance(self, t: Instance) -> Type:
             return join_types(t, self.s)
         elif isinstance(self.s, TypedDictType):
             return join_types(t, self.s)
+        elif isinstance(self.s, LiteralType):
+            return join_types(t, self.s)
         else:
             return self.default(self.s)
 
@@ -268,7 +270,13 @@ def visit_typeddict_type(self, t: TypedDictType) -> Type:
             return self.default(self.s)
 
     def visit_literal_type(self, t: LiteralType) -> Type:
-        raise NotImplementedError()
+        if isinstance(self.s, LiteralType):
+            if t == self.s:
+                return t
+            else:
+                return join_types(self.s.fallback, t.fallback)
+        else:
+            return join_types(self.s, t.fallback)
 
     def visit_partial_type(self, t: PartialType) -> Type:
         # We only have partial information so we can't decide the join result. We should
diff --git a/mypy/test/testtypes.py b/mypy/test/testtypes.py
index 6ed2d25a652a..f6b670126e94 100644
--- a/mypy/test/testtypes.py
+++ b/mypy/test/testtypes.py
@@ -249,11 +249,11 @@ def test_is_proper_subtype_and_subtype_literal_types(self) -> None:
         fx = self.fx
 
         lit1 = LiteralType(1, fx.a)
-        lit2 = LiteralType("foo", fx.b)
-        lit3 = LiteralType("bar", fx.b)
+        lit2 = LiteralType("foo", fx.d)
+        lit3 = LiteralType("bar", fx.d)
 
         assert_true(is_proper_subtype(lit1, fx.a))
-        assert_false(is_proper_subtype(lit1, fx.b))
+        assert_false(is_proper_subtype(lit1, fx.d))
         assert_false(is_proper_subtype(fx.a, lit1))
         assert_true(is_proper_subtype(fx.uninhabited, lit1))
         assert_false(is_proper_subtype(lit1, fx.uninhabited))
@@ -262,7 +262,7 @@ def test_is_proper_subtype_and_subtype_literal_types(self) -> None:
         assert_false(is_proper_subtype(lit2, lit3))
 
         assert_true(is_subtype(lit1, fx.a))
-        assert_false(is_subtype(lit1, fx.b))
+        assert_false(is_subtype(lit1, fx.d))
         assert_false(is_subtype(fx.a, lit1))
         assert_true(is_subtype(fx.uninhabited, lit1))
         assert_false(is_subtype(lit1, fx.uninhabited))
@@ -621,6 +621,41 @@ def test_type_type(self) -> None:
         self.assert_join(self.fx.type_type, self.fx.type_any, self.fx.type_type)
         self.assert_join(self.fx.type_b, self.fx.anyt, self.fx.anyt)
 
+    def test_literal_type(self) -> None:
+        a = self.fx.a
+        d = self.fx.d
+        lit1 = LiteralType(1, a)
+        lit2 = LiteralType(2, a)
+        lit3 = LiteralType("foo", d)
+
+        self.assert_join(lit1, lit1, lit1)
+        self.assert_join(lit1, a, a)
+        self.assert_join(lit1, d, self.fx.o)
+        self.assert_join(lit1, lit2, a)
+        self.assert_join(lit1, lit3, self.fx.o)
+        self.assert_join(lit1, self.fx.anyt, self.fx.anyt)
+        self.assert_join(UnionType([lit1, lit2]), lit2, UnionType([lit1, lit2]))
+        self.assert_join(UnionType([lit1, lit2]), a, a)
+        self.assert_join(UnionType([lit1, lit3]), a, UnionType([a, lit3]))
+        self.assert_join(UnionType([d, lit3]), lit3, UnionType([d, lit3]))
+        self.assert_join(UnionType([d, lit3]), d, UnionType([d, lit3]))
+        self.assert_join(UnionType([a, lit1]), lit1, UnionType([a, lit1]))
+        self.assert_join(UnionType([a, lit1]), lit2, UnionType([a, lit1]))
+        self.assert_join(UnionType([lit1, lit2]),
+                         UnionType([lit1, lit2]),
+                         UnionType([lit1, lit2]))
+
+        # The order in which we try joining two unions influences the
+        # ordering of the items in the final produced unions. So, we
+        # manually call 'assert_simple_join' and tune the output
+        # after swapping the arguments here.
+        self.assert_simple_join(UnionType([lit1, lit2]),
+                                UnionType([lit2, lit3]),
+                                UnionType([lit1, lit2, lit3]))
+        self.assert_simple_join(UnionType([lit2, lit3]),
+                                UnionType([lit1, lit2]),
+                                UnionType([lit2, lit3, lit1]))
+
     # There are additional test cases in check-inference.test.
 
     # TODO: Function types + varargs and default args.
diff --git a/mypy/typeanal.py b/mypy/typeanal.py
index 646bb4e05b0d..0c79c11c10c6 100644
--- a/mypy/typeanal.py
+++ b/mypy/typeanal.py
@@ -1086,6 +1086,8 @@ def visit_unbound_type(self, t: UnboundType) -> TypeVarList:
             return [(name, node.node)]
         elif not self.include_callables and self._seems_like_callable(t):
             return []
+        elif node and node.fullname in ('typing_extensions.Literal', 'typing.Literal'):
+            return []
         else:
             return super().visit_unbound_type(t)
 
diff --git a/test-data/unit/check-literal.test b/test-data/unit/check-literal.test
index 59e8b47ce7dc..c7f35c94ec5e 100644
--- a/test-data/unit/check-literal.test
+++ b/test-data/unit/check-literal.test
@@ -170,6 +170,14 @@ c2: c2t
 reveal_type(a2)  # E: Revealed type is 'Literal[4]'
 reveal_type(b2)  # E: Revealed type is 'Literal[42]'
 reveal_type(c2)  # E: Revealed type is 'Literal[-300]'
+
+def f1(x: Literal[4]) -> Literal[4]: pass
+def f2(x: Literal[0x2a]) -> Literal[0x2a]: pass
+def f3(x: Literal[-300]) -> Literal[-300]: pass
+
+reveal_type(f1)  # E: Revealed type is 'def (x: Literal[4]) -> Literal[4]'
+reveal_type(f2)  # E: Revealed type is 'def (x: Literal[42]) -> Literal[42]'
+reveal_type(f3)  # E: Revealed type is 'def (x: Literal[-300]) -> Literal[-300]'
 [out]
 
 [case testLiteralBasicBoolUsage]
@@ -188,6 +196,12 @@ b2: b2t
 
 reveal_type(a2)  # E: Revealed type is 'Literal[True]'
 reveal_type(b2)  # E: Revealed type is 'Literal[False]'
+
+def f1(x: Literal[True]) -> Literal[True]: pass
+def f2(x: Literal[False]) -> Literal[False]: pass
+
+reveal_type(f1)  # E: Revealed type is 'def (x: Literal[True]) -> Literal[True]'
+reveal_type(f2)  # E: Revealed type is 'def (x: Literal[False]) -> Literal[False]'
 [builtins fixtures/bool.pyi]
 [out]
 
@@ -197,10 +211,26 @@ from typing_extensions import Literal
 a: Literal[""]
 b: Literal["  foo bar  "]
 c: Literal['  foo bar  ']
+d: Literal["foo"]
+e: Literal['foo']
 
 reveal_type(a)  # E: Revealed type is 'Literal['']'
 reveal_type(b)  # E: Revealed type is 'Literal['  foo bar  ']'
 reveal_type(c)  # E: Revealed type is 'Literal['  foo bar  ']'
+reveal_type(d)  # E: Revealed type is 'Literal['foo']'
+reveal_type(e)  # E: Revealed type is 'Literal['foo']'
+
+def f1(x: Literal[""]) -> Literal[""]: pass
+def f2(x: Literal["  foo bar  "]) -> Literal["  foo bar  "]: pass
+def f3(x: Literal['  foo bar  ']) -> Literal['  foo bar  ']: pass
+def f4(x: Literal["foo"]) -> Literal["foo"]: pass
+def f5(x: Literal['foo']) -> Literal['foo']: pass
+
+reveal_type(f1)  # E: Revealed type is 'def (x: Literal['']) -> Literal['']'
+reveal_type(f2)  # E: Revealed type is 'def (x: Literal['  foo bar  ']) -> Literal['  foo bar  ']'
+reveal_type(f3)  # E: Revealed type is 'def (x: Literal['  foo bar  ']) -> Literal['  foo bar  ']'
+reveal_type(f4)  # E: Revealed type is 'def (x: Literal['foo']) -> Literal['foo']'
+reveal_type(f5)  # E: Revealed type is 'def (x: Literal['foo']) -> Literal['foo']'
 [out]
 
 [case testLiteralBasicStrUsageSlashes]
@@ -216,10 +246,43 @@ main:6: error: Revealed type is 'Literal['foo\\nbar']'
 main:7: error: Revealed type is 'Literal['foo\nbar']'
 
 [case testLiteralBasicNoneUsage]
+# Note: Literal[None] and None are equivalent
 from typing_extensions import Literal
 a: Literal[None]
 reveal_type(a)   # E: Revealed type is 'None'
-# Note: Literal[None] and None are equivalent
+
+def f1(x: Literal[None]) -> None: pass
+def f2(x: None) -> Literal[None]: pass
+def f3(x: Literal[None]) -> Literal[None]: pass
+
+reveal_type(f1)  # E: Revealed type is 'def (x: None)'
+reveal_type(f2)  # E: Revealed type is 'def (x: None)'
+reveal_type(f3)  # E: Revealed type is 'def (x: None)'
+[out]
+
+[case testLiteralCallingUnionFunction]
+from typing_extensions import Literal
+
+def func(x: Literal['foo', 'bar', '  foo  ']) -> None: ...
+
+func('foo')
+func('bar')
+func('  foo  ')
+func('baz')       # E: Argument 1 to "func" has incompatible type "Literal['baz']"; expected "Union[Literal['foo'], Literal['bar'], Literal['  foo  ']]"
+
+a: Literal['foo']
+b: Literal['bar']
+c: Literal['  foo  ']
+d: Literal['foo', 'bar']
+e: Literal['foo', 'bar', '  foo  ']
+f: Literal['foo', 'bar', 'baz']
+
+func(a)
+func(b)
+func(c)
+func(d)
+func(e)
+func(f)  # E: Argument 1 to "func" has incompatible type "Union[Literal['foo'], Literal['bar'], Literal['baz']]"; expected "Union[Literal['foo'], Literal['bar'], Literal['  foo  ']]"
 [out]
 
 [case testLiteralDisallowAny]
@@ -528,7 +591,6 @@ f_lit(b)
 f_lit(c)
 [out]
 
-
 [case testLiteralCallingOverloadedFunction]
 from typing import overload, Generic, TypeVar, Any
 from typing_extensions import Literal
@@ -633,23 +695,428 @@ c: Literal[15]
 
 
 --
--- Here are a few misc tests that deliberately do not work.
--- I'm including these as skipped tests partly because I wanted to
--- clarify the scope of what this diff did and did not do, and
--- partly because I already wrote these and would like to avoid having
--- to rewrite them in the future.
+-- Check to make sure we handle inference of literal values correctly,
+-- especially when doing assignments or calls
 --
 
-[case testLiteralActualAssignment-skip]
-# TODO: fix this test. The 1 is currently always given a type of 'int'
+[case testLiteralInferredInAssignment]
 from typing_extensions import Literal
 
-a: Literal[1] = 1
+int1: Literal[1] = 1
+int2 = 1
+int3: int = 1
+
+str1: Literal["foo"] = "foo"
+str2 = "foo"
+str3: str = "foo"
+
+bool1: Literal[True] = True
+bool2 = True
+bool3: bool = True
+
+none1: Literal[None] = None
+none2 = None
+none3: None = None
+
+reveal_type(int1)   # E: Revealed type is 'Literal[1]'
+reveal_type(int2)   # E: Revealed type is 'builtins.int'
+reveal_type(int3)   # E: Revealed type is 'builtins.int'
+reveal_type(str1)   # E: Revealed type is 'Literal['foo']'
+reveal_type(str2)   # E: Revealed type is 'builtins.str'
+reveal_type(str3)   # E: Revealed type is 'builtins.str'
+reveal_type(bool1)  # E: Revealed type is 'Literal[True]'
+reveal_type(bool2)  # E: Revealed type is 'builtins.bool'
+reveal_type(bool3)  # E: Revealed type is 'builtins.bool'
+reveal_type(none1)  # E: Revealed type is 'None'
+reveal_type(none2)  # E: Revealed type is 'None'
+reveal_type(none3)  # E: Revealed type is 'None'
+[builtins fixtures/primitives.pyi]
 [out]
 
---
--- Tests that make sure we're correctly using the fallback
---
+[case testLiteralInferredOnlyForActualLiterals]
+from typing_extensions import Literal
+
+w: Literal[1]
+x: Literal["foo"]
+y: Literal[True]
+z: Literal[None]
+combined: Literal[1, "foo", True, None]
+
+a = 1
+b = "foo"
+c = True
+d = None
+
+w = a  # E: Incompatible types in assignment (expression has type "int", variable has type "Literal[1]")
+x = b  # E: Incompatible types in assignment (expression has type "str", variable has type "Literal['foo']")
+y = c  # E: Incompatible types in assignment (expression has type "bool", variable has type "Literal[True]")
+z = d  # This is ok: Literal[None] and None are equivalent.
+
+combined = a  # E: Incompatible types in assignment (expression has type "int", variable has type "Union[Literal[1], Literal['foo'], Literal[True], None]")
+combined = b  # E: Incompatible types in assignment (expression has type "str", variable has type "Union[Literal[1], Literal['foo'], Literal[True], None]")
+combined = c  # E: Incompatible types in assignment (expression has type "bool", variable has type "Union[Literal[1], Literal['foo'], Literal[True], None]")
+combined = d  # Also ok, for similar reasons.
+
+e: Literal[1] = 1
+f: Literal["foo"] = "foo"
+g: Literal[True] = True
+h: Literal[None] = None
+
+w = e
+x = f
+y = g
+z = h
+combined = e
+combined = f
+combined = g
+combined = h
+
+[builtins fixtures/primitives.pyi]
+[out]
+
+[case testLiteralInferredTypeMustMatchExpected]
+from typing_extensions import Literal
+
+a: Literal[1] = 2           # E: Incompatible types in assignment (expression has type "Literal[2]", variable has type "Literal[1]")
+b: Literal["foo"] = "bar"   # E: Incompatible types in assignment (expression has type "Literal['bar']", variable has type "Literal['foo']")
+c: Literal[True] = False    # E: Incompatible types in assignment (expression has type "Literal[False]", variable has type "Literal[True]")
+
+d: Literal[1, 2] = 3                # E: Incompatible types in assignment (expression has type "Literal[3]", variable has type "Union[Literal[1], Literal[2]]")
+e: Literal["foo", "bar"] = "baz"    # E: Incompatible types in assignment (expression has type "Literal['baz']", variable has type "Union[Literal['foo'], Literal['bar']]")
+f: Literal[True, 4] = False         # E: Incompatible types in assignment (expression has type "Literal[False]", variable has type "Union[Literal[True], Literal[4]]")
+
+[builtins fixtures/primitives.pyi]
+[out]
+
+[case testLiteralInferredInCall]
+from typing_extensions import Literal
+
+def f_int_lit(x: Literal[1]) -> None: pass
+def f_int(x: int) -> None: pass
+
+def f_str_lit(x: Literal["foo"]) -> None: pass
+def f_str(x: str) -> None: pass
+
+def f_bool_lit(x: Literal[True]) -> None: pass
+def f_bool(x: bool) -> None: pass
+
+def f_none_lit(x: Literal[None]) -> None: pass
+def f_none(x: None) -> None: pass
+
+i1: Literal[1]
+i2: Literal[2]
+f_int_lit(1)
+f_int_lit(2)  # E: Argument 1 to "f_int_lit" has incompatible type "Literal[2]"; expected "Literal[1]"
+f_int(1)
+f_int_lit(i1)
+f_int_lit(i2) # E: Argument 1 to "f_int_lit" has incompatible type "Literal[2]"; expected "Literal[1]"
+
+s1: Literal["foo"]
+s2: Literal["bar"]
+f_str_lit("foo")
+f_str_lit("bar")  # E: Argument 1 to "f_str_lit" has incompatible type "Literal['bar']"; expected "Literal['foo']"
+f_str("baz")
+f_str_lit(s1)
+f_str_lit(s2)     # E: Argument 1 to "f_str_lit" has incompatible type "Literal['bar']"; expected "Literal['foo']"
+
+b1: Literal[True]
+b2: Literal[False]
+f_bool_lit(True)
+f_bool_lit(False)  # E: Argument 1 to "f_bool_lit" has incompatible type "Literal[False]"; expected "Literal[True]"
+f_bool(True)
+f_bool_lit(b1)
+f_bool_lit(b2)     # E: Argument 1 to "f_bool_lit" has incompatible type "Literal[False]"; expected "Literal[True]"
+
+n1: Literal[None]
+f_none_lit(None)
+f_none(None)
+f_none_lit(n1)
+[builtins fixtures/primitives.pyi]
+[out]
+
+[case testLiteralInferredInReturnContext]
+from typing_extensions import Literal
+
+def f1() -> int:
+    return 1
+
+def f2() -> Literal[1]:
+    return 1
+
+def f3() -> Literal[1]:
+    return 2  # E: Incompatible return value type (got "Literal[2]", expected "Literal[1]")
+
+def f4(x: Literal[1]) -> Literal[1]:
+    return x
+
+def f5(x: Literal[2]) -> Literal[1]:
+    return x  # E: Incompatible return value type (got "Literal[2]", expected "Literal[1]")
+
+[out]
+
+[case testLiteralInferredInListContext]
+from typing import List
+from typing_extensions import Literal
+
+a: List[Literal[1]] = [1, 1, 1]
+b = [1, 1, 1]
+c: List[Literal[1, 2, 3]] = [1, 2, 3]
+d = [1, 2, 3]
+e: List[Literal[1, "x"]] = [1, "x"]
+f = [1, "x"]
+g: List[List[List[Literal[1, 2, 3]]]] = [[[1, 2, 3], [3]]]
+h: List[Literal[1]] = []
+
+reveal_type(a)  # E: Revealed type is 'builtins.list[Literal[1]]'
+reveal_type(b)  # E: Revealed type is 'builtins.list[builtins.int*]'
+reveal_type(c)  # E: Revealed type is 'builtins.list[Union[Literal[1], Literal[2], Literal[3]]]'
+reveal_type(d)  # E: Revealed type is 'builtins.list[builtins.int*]'
+reveal_type(e)  # E: Revealed type is 'builtins.list[Union[Literal[1], Literal['x']]]'
+reveal_type(f)  # E: Revealed type is 'builtins.list[builtins.object*]'
+reveal_type(g)  # E: Revealed type is 'builtins.list[builtins.list[builtins.list[Union[Literal[1], Literal[2], Literal[3]]]]]'
+reveal_type(h)  # E: Revealed type is 'builtins.list[Literal[1]]'
+
+lit1: Literal[1]
+lit2: Literal[2]
+lit3: Literal["foo"]
+
+arr1 = [lit1, lit1, lit1]
+arr2 = [lit1, lit2]
+arr3 = [lit1, 4, 5]
+arr4 = [lit1, lit2, lit3]
+arr5 = [object(), lit1]
+
+reveal_type(arr1)  # E: Revealed type is 'builtins.list[Literal[1]]'
+reveal_type(arr2)  # E: Revealed type is 'builtins.list[builtins.int*]'
+reveal_type(arr3)  # E: Revealed type is 'builtins.list[builtins.int*]'
+reveal_type(arr4)  # E: Revealed type is 'builtins.list[builtins.object*]'
+reveal_type(arr5)  # E: Revealed type is 'builtins.list[builtins.object*]'
+
+bad: List[Literal[1, 2]] = [1, 2, 3]  # E: List item 2 has incompatible type "Literal[3]"; expected "Union[Literal[1], Literal[2]]"
+
+[builtins fixtures/list.pyi]
+[out]
+
+[case testLiteralInferredInTupleContext]
+# Note: most of the 'are we handling context correctly' tests should have been
+# handled up above, so we keep things comparatively simple for tuples and dicts.
+from typing import Tuple
+from typing_extensions import Literal
+
+a: Tuple[Literal[1], Literal[2]] = (1, 2)
+b: Tuple[int, Literal[1, 2], Literal[3], Tuple[Literal["foo"]]] = (1, 2, 3, ("foo",))
+c: Tuple[Literal[1], Literal[2]] = (2, 1)  # E: Incompatible types in assignment (expression has type "Tuple[Literal[2], Literal[1]]", variable has type "Tuple[Literal[1], Literal[2]]")
+d = (1, 2)
+
+reveal_type(d)  # E: Revealed type is 'Tuple[builtins.int, builtins.int]'
+
+[builtins fixtures/tuple.pyi]
+[out]
+
+[case testLiteralInferredInDictContext]
+from typing import Dict
+from typing_extensions import Literal
+
+a = {"x": 1, "y": 2}
+b: Dict[str, Literal[1, 2]] = {"x": 1, "y": 2}
+c: Dict[Literal["x", "y"], int] = {"x": 1, "y": 2}
+
+reveal_type(a)  # E: Revealed type is 'builtins.dict[builtins.str*, builtins.int*]'
+
+[builtins fixtures/dict.pyi]
+[out]
+
+[case testLiteralInferredInOverloadContextBasic]
+from typing import overload
+from typing_extensions import Literal
+
+@overload
+def func(x: Literal[1]) -> str: ...
+@overload
+def func(x: Literal[2]) -> int: ...
+@overload
+def func(x: int) -> object: ...
+def func(x: int) -> object: pass
+
+a: Literal[1]
+b: Literal[2]
+c: Literal[1, 2]
+
+reveal_type(func(1))  # E: Revealed type is 'builtins.str'
+reveal_type(func(2))  # E: Revealed type is 'builtins.int'
+reveal_type(func(3))  # E: Revealed type is 'builtins.object'
+reveal_type(func(a))  # E: Revealed type is 'builtins.str'
+reveal_type(func(b))  # E: Revealed type is 'builtins.int'
+
+# Note: the fact that we don't do union math here is consistent
+# with the output we would have gotten if we replaced int and the
+# Literal types here with regular classes/subclasses.
+reveal_type(func(c))  # E: Revealed type is 'builtins.object'
+[out]
+
+[case testLiteralOverloadProhibitUnsafeOverlaps]
+from typing import overload
+from typing_extensions import Literal
+
+@overload
+def func1(x: Literal[1]) -> str: ...  # E: Overloaded function signatures 1 and 2 overlap with incompatible return types
+@overload
+def func1(x: int) -> int: ...
+def func1(x): pass
+
+@overload
+def func2(x: Literal['a']) -> int: ...  # E: Overloaded function signatures 1 and 2 overlap with incompatible return types
+@overload
+def func2(x: str) -> Literal[2]: ...
+def func2(x): pass
+
+# This one is typesafe
+@overload
+def func3(x: Literal['a']) -> Literal[2]: ...
+@overload
+def func3(x: str) -> int: ...
+def func3(x): pass
+[out]
+
+[case testLiteralInferredInOverloadContextUnionMath]
+from typing import overload, Union
+from typing_extensions import Literal
+
+class A: pass
+class B: pass
+class C: pass
+
+@overload
+def func(x: Literal[-40]) -> A: ...
+@overload
+def func(x: Literal[3, 4, 5, 6]) -> B: ...
+@overload
+def func(x: Literal["foo"]) -> C: ...
+def func(x: Union[int, str]) -> Union[A, B, C]: pass
+
+a: Literal[-40, "foo"]
+b: Literal[3]
+c: Literal[3, -40]
+d: Literal[6, 7]
+e: int
+f: Literal[7, "bar"]
+
+reveal_type(func(a))  # E: Revealed type is 'Union[__main__.A, __main__.C]'
+reveal_type(func(b))  # E: Revealed type is '__main__.B'
+reveal_type(func(c))  # E: Revealed type is 'Union[__main__.B, __main__.A]'
+reveal_type(func(d))  # E: Revealed type is '__main__.B' \
+                      # E: Argument 1 to "func" has incompatible type "Union[Literal[6], Literal[7]]"; expected "Union[Literal[3], Literal[4], Literal[5], Literal[6]]"
+
+reveal_type(func(e))  # E: Revealed type is 'Any' \
+                      # E: No overload variant of "func" matches argument type "int" \
+                      # N: Possible overload variants: \
+                      # N:     def func(x: Literal[-40]) -> A \
+                      # N:     def func(x: Union[Literal[3], Literal[4], Literal[5], Literal[6]]) -> B \
+                      # N:     def func(x: Literal['foo']) -> C
+
+reveal_type(func(f))  # E: Revealed type is 'Any' \
+                      # E: No overload variant of "func" matches argument type "Union[Literal[7], Literal['bar']]" \
+                      # N: Possible overload variants: \
+                      # N:     def func(x: Literal[-40]) -> A \
+                      # N:     def func(x: Union[Literal[3], Literal[4], Literal[5], Literal[6]]) -> B \
+                      # N:     def func(x: Literal['foo']) -> C
+[out]
+
+[case testLiteralInferredInOverloadContextUnionMathOverloadingReturnsBestType]
+# This test is a transliteration of check-overloading::testUnionMathOverloadingReturnsBestType
+from typing import overload
+from typing_extensions import Literal
+
+@overload
+def f(x: Literal[1, 2]) -> int: ...
+@overload
+def f(x: int) -> object: ...
+def f(x):
+    pass
+
+x: Literal[1, 2]
+y: Literal[1, 2, 3]
+z: Literal[1, 2, "three"]
+reveal_type(f(x))  # E: Revealed type is 'builtins.int'
+reveal_type(f(1))  # E: Revealed type is 'builtins.int'
+reveal_type(f(2))  # E: Revealed type is 'builtins.int'
+reveal_type(f(y))  # E: Revealed type is 'builtins.object'
+reveal_type(f(z))  # E: Revealed type is 'builtins.int' \
+                   # E: Argument 1 to "f" has incompatible type "Union[Literal[1], Literal[2], Literal['three']]"; expected "Union[Literal[1], Literal[2]]"
+[out]
+
+[case testLiteralInferredInOverloadContextWithTypevars]
+from typing import TypeVar, overload, Union
+from typing_extensions import Literal
+
+T = TypeVar('T')
+
+@overload
+def f1(x: T, y: int) -> T: ...
+@overload
+def f1(x: T, y: str) -> Union[T, str]: ...
+def f1(x, y): pass
+
+a: Literal[1]
+reveal_type(f1(1, 1))  # E: Revealed type is 'builtins.int*'
+reveal_type(f1(a, 1))  # E: Revealed type is 'Literal[1]'
+
+@overload
+def f2(x: T, y: Literal[3]) -> T: ...
+@overload
+def f2(x: T, y: str) -> Union[T]: ...
+def f2(x, y): pass
+
+reveal_type(f2(1, 3))  # E: Revealed type is 'builtins.int*'
+reveal_type(f2(a, 3))  # E: Revealed type is 'Literal[1]'
+
+@overload
+def f3(x: Literal[3]) -> Literal[3]: ...
+@overload
+def f3(x: T) -> T: ...
+def f3(x): pass
+
+reveal_type(f3(1))  # E: Revealed type is 'builtins.int*'
+reveal_type(f3(a))  # E: Revealed type is 'Literal[1]'
+
+@overload
+def f4(x: str) -> str: ...
+@overload
+def f4(x: T) -> T: ...
+def f4(x): pass
+
+b: Literal['foo']
+reveal_type(f4(1))      # E: Revealed type is 'builtins.int*'
+reveal_type(f4(a))      # E: Revealed type is 'Literal[1]'
+reveal_type(f4("foo"))  # E: Revealed type is 'builtins.str'
+
+# Note: first overload is selected and prevents the typevar from
+# ever inferring a Literal["something"].
+reveal_type(f4(b))      # E: Revealed type is 'builtins.str'
+[out]
+
+[case testLiteralInferredInOverloadContextUnionMathTrickyOverload]
+# This test is a transliteration of check-overloading::testUnionMathTrickyOverload1
+from typing import overload
+from typing_extensions import Literal
+
+@overload
+def f(x: Literal['a'], y: Literal['a']) -> int: ...
+@overload
+def f(x: str, y: Literal['b']) -> str: ...
+def f(x):
+    pass
+
+x: Literal['a', 'b']
+y: Literal['a', 'b']
+f(x, y)  # E: Argument 1 to "f" has incompatible type "Union[Literal['a'], Literal['b']]"; expected "Literal['a']" \
+         # E: Argument 2 to "f" has incompatible type "Union[Literal['a'], Literal['b']]"; expected "Literal['a']" \
+[out]
+
+
+---
+--- Tests that make sure we're correctly using the fallback
+---
 
 [case testLiteralFallbackOperatorsWorkCorrectly]
 from typing_extensions import Literal