diff --git a/mypy/checker.py b/mypy/checker.py
index c244a7a07d8a..a1395df05827 100644
--- a/mypy/checker.py
+++ b/mypy/checker.py
@@ -28,7 +28,7 @@
     Type, AnyType, CallableType, FunctionLike, Overloaded, TupleType, TypedDictType,
     Instance, NoneTyp, ErrorType, strip_type, TypeType,
     UnionType, TypeVarId, TypeVarType, PartialType, DeletedType, UninhabitedType, TypeVarDef,
-    true_only, false_only, function_type, is_named_instance
+    true_only, false_only, function_type, is_named_instance, union_items
 )
 from mypy.sametypes import is_same_type, is_same_types
 from mypy.messages import MessageBuilder
@@ -812,44 +812,45 @@ def check_overlapping_op_methods(self,
         # of x in __radd__ would not be A, the methods could be
         # non-overlapping.
 
-        if isinstance(forward_type, CallableType):
-            # TODO check argument kinds
-            if len(forward_type.arg_types) < 1:
-                # Not a valid operator method -- can't succeed anyway.
-                return
+        for forward_item in union_items(forward_type):
+            if isinstance(forward_item, CallableType):
+                # TODO check argument kinds
+                if len(forward_item.arg_types) < 1:
+                    # Not a valid operator method -- can't succeed anyway.
+                    return
 
-            # Construct normalized function signatures corresponding to the
-            # operator methods. The first argument is the left operand and the
-            # second operand is the right argument -- we switch the order of
-            # the arguments of the reverse method.
-            forward_tweaked = CallableType(
-                [forward_base, forward_type.arg_types[0]],
-                [nodes.ARG_POS] * 2,
-                [None] * 2,
-                forward_type.ret_type,
-                forward_type.fallback,
-                name=forward_type.name)
-            reverse_args = reverse_type.arg_types
-            reverse_tweaked = CallableType(
-                [reverse_args[1], reverse_args[0]],
-                [nodes.ARG_POS] * 2,
-                [None] * 2,
-                reverse_type.ret_type,
-                fallback=self.named_type('builtins.function'),
-                name=reverse_type.name)
-
-            if is_unsafe_overlapping_signatures(forward_tweaked,
-                                                reverse_tweaked):
-                self.msg.operator_method_signatures_overlap(
-                    reverse_class.name(), reverse_name,
-                    forward_base.type.name(), forward_name, context)
-        elif isinstance(forward_type, Overloaded):
-            for item in forward_type.items():
-                self.check_overlapping_op_methods(
-                    reverse_type, reverse_name, reverse_class,
-                    item, forward_name, forward_base, context)
-        elif not isinstance(forward_type, AnyType):
-            self.msg.forward_operator_not_callable(forward_name, context)
+                # Construct normalized function signatures corresponding to the
+                # operator methods. The first argument is the left operand and the
+                # second operand is the right argument -- we switch the order of
+                # the arguments of the reverse method.
+                forward_tweaked = CallableType(
+                    [forward_base, forward_item.arg_types[0]],
+                    [nodes.ARG_POS] * 2,
+                    [None] * 2,
+                    forward_item.ret_type,
+                    forward_item.fallback,
+                    name=forward_item.name)
+                reverse_args = reverse_type.arg_types
+                reverse_tweaked = CallableType(
+                    [reverse_args[1], reverse_args[0]],
+                    [nodes.ARG_POS] * 2,
+                    [None] * 2,
+                    reverse_type.ret_type,
+                    fallback=self.named_type('builtins.function'),
+                    name=reverse_type.name)
+
+                if is_unsafe_overlapping_signatures(forward_tweaked,
+                                                    reverse_tweaked):
+                    self.msg.operator_method_signatures_overlap(
+                        reverse_class.name(), reverse_name,
+                        forward_base.type.name(), forward_name, context)
+            elif isinstance(forward_item, Overloaded):
+                for item in forward_item.items():
+                    self.check_overlapping_op_methods(
+                        reverse_type, reverse_name, reverse_class,
+                        item, forward_name, forward_base, context)
+            elif not isinstance(forward_item, AnyType):
+                self.msg.forward_operator_not_callable(forward_name, context)
 
     def check_inplace_operator_method(self, defn: FuncBase) -> None:
         """Check an inplace operator method such as __iadd__.
diff --git a/mypy/checkexpr.py b/mypy/checkexpr.py
index 51a6f92e9ce6..6736c4f8f513 100644
--- a/mypy/checkexpr.py
+++ b/mypy/checkexpr.py
@@ -32,7 +32,7 @@
 from mypy import messages
 from mypy.infer import infer_type_arguments, infer_function_type_arguments
 from mypy import join
-from mypy.meet import meet_simple
+from mypy.meet import narrow_declared_type
 from mypy.maptype import map_instance_to_supertype
 from mypy.subtypes import is_subtype, is_equivalent
 from mypy import applytype
@@ -2221,7 +2221,7 @@ def narrow_type_from_binder(self, expr: Expression, known_type: Type) -> Type:
         if expr.literal >= LITERAL_TYPE:
             restriction = self.chk.binder.get(expr)
             if restriction:
-                ans = meet_simple(known_type, restriction)
+                ans = narrow_declared_type(known_type, restriction)
                 return ans
         return known_type
 
diff --git a/mypy/erasetype.py b/mypy/erasetype.py
index 9a44b0456522..5ea1df156c6f 100644
--- a/mypy/erasetype.py
+++ b/mypy/erasetype.py
@@ -76,7 +76,8 @@ def visit_typeddict_type(self, t: TypedDictType) -> Type:
         return t.fallback.accept(self)
 
     def visit_union_type(self, t: UnionType) -> Type:
-        return AnyType()        # XXX: return underlying type if only one?
+        erased_items = [erase_type(item) for item in t.items]
+        return UnionType.make_simplified_union(erased_items)
 
     def visit_type_type(self, t: TypeType) -> Type:
         return TypeType(t.item.accept(self), line=t.line)
diff --git a/mypy/join.py b/mypy/join.py
index 06d5416cd2ea..1713cd61ea63 100644
--- a/mypy/join.py
+++ b/mypy/join.py
@@ -10,7 +10,7 @@
     UninhabitedType, TypeType, true_or_false
 )
 from mypy.maptype import map_instance_to_supertype
-from mypy.subtypes import is_subtype, is_equivalent, is_subtype_ignoring_tvars
+from mypy.subtypes import is_subtype, is_equivalent, is_subtype_ignoring_tvars, is_proper_subtype
 
 from mypy import experiments
 
@@ -29,10 +29,10 @@ def join_simple(declaration: Type, s: Type, t: Type) -> Type:
     if isinstance(s, ErasedType):
         return t
 
-    if is_subtype(s, t):
+    if is_proper_subtype(s, t):
         return t
 
-    if is_subtype(t, s):
+    if is_proper_subtype(t, s):
         return s
 
     if isinstance(declaration, UnionType):
diff --git a/mypy/meet.py b/mypy/meet.py
index 22d0a709838b..82fec33c0cb2 100644
--- a/mypy/meet.py
+++ b/mypy/meet.py
@@ -25,21 +25,26 @@ def meet_types(s: Type, t: Type) -> Type:
     return t.accept(TypeMeetVisitor(s))
 
 
-def meet_simple(s: Type, t: Type, default_right: bool = True) -> Type:
-    if s == t:
-        return s
-    if isinstance(s, UnionType):
-        return UnionType.make_simplified_union([meet_types(x, t) for x in s.items])
-    elif not is_overlapping_types(s, t, use_promotions=True):
+def narrow_declared_type(declared: Type, narrowed: Type) -> Type:
+    """Return the declared type narrowed down to another type."""
+    if declared == narrowed:
+        return declared
+    if isinstance(declared, UnionType):
+        return UnionType.make_simplified_union([narrow_declared_type(x, narrowed)
+                                                for x in declared.items])
+    elif not is_overlapping_types(declared, narrowed, use_promotions=True):
         if experiments.STRICT_OPTIONAL:
             return UninhabitedType()
         else:
             return NoneTyp()
-    else:
-        if default_right:
-            return t
-        else:
-            return s
+    elif isinstance(narrowed, UnionType):
+        return UnionType.make_simplified_union([narrow_declared_type(declared, x)
+                                                for x in narrowed.items])
+    elif isinstance(narrowed, AnyType):
+        return narrowed
+    elif isinstance(declared, (Instance, TupleType)):
+        return meet_types(declared, narrowed)
+    return narrowed
 
 
 def is_overlapping_types(t: Type, s: Type, use_promotions: bool = False) -> bool:
@@ -249,6 +254,10 @@ def visit_tuple_type(self, t: TupleType) -> Type:
         elif (isinstance(self.s, Instance) and
               self.s.type.fullname() == 'builtins.tuple' and self.s.args):
             return t.copy_modified(items=[meet_types(it, self.s.args[0]) for it in t.items])
+        elif (isinstance(self.s, Instance) and t.fallback.type == self.s.type):
+            # Uh oh, a broken named tuple type (https://github.com/python/mypy/issues/3016).
+            # Do something reasonable until that bug is fixed.
+            return t
         else:
             return self.default(self.s)
 
diff --git a/mypy/subtypes.py b/mypy/subtypes.py
index c98bb8e8d144..b96618da28eb 100644
--- a/mypy/subtypes.py
+++ b/mypy/subtypes.py
@@ -7,6 +7,7 @@
 )
 import mypy.applytype
 import mypy.constraints
+from mypy.erasetype import erase_type
 # Circular import; done in the function instead.
 # import mypy.solve
 from mypy import messages, sametypes
@@ -15,6 +16,7 @@
     ARG_POS, ARG_OPT, ARG_NAMED, ARG_NAMED_OPT, ARG_STAR, ARG_STAR2,
 )
 from mypy.maptype import map_instance_to_supertype
+from mypy.sametypes import is_same_type
 
 from mypy import experiments
 
@@ -280,9 +282,15 @@ def visit_type_type(self, left: TypeType) -> bool:
 
 def is_callable_subtype(left: CallableType, right: CallableType,
                         ignore_return: bool = False,
-                        ignore_pos_arg_names: bool = False) -> bool:
+                        ignore_pos_arg_names: bool = False,
+                        use_proper_subtype: bool = False) -> bool:
     """Is left a subtype of right?"""
 
+    if use_proper_subtype:
+        is_compat = is_proper_subtype
+    else:
+        is_compat = is_subtype
+
     # If either function is implicitly typed, ignore positional arg names too
     if left.implicit or right.implicit:
         ignore_pos_arg_names = True
@@ -309,7 +317,7 @@ def is_callable_subtype(left: CallableType, right: CallableType,
             return False
 
     # Check return types.
-    if not ignore_return and not is_subtype(left.ret_type, right.ret_type):
+    if not ignore_return and not is_compat(left.ret_type, right.ret_type):
         return False
 
     if right.is_ellipsis_args:
@@ -366,7 +374,7 @@ def is_callable_subtype(left: CallableType, right: CallableType,
                 right_by_position = right.argument_by_position(j)
                 assert right_by_position is not None
                 if not are_args_compatible(left_by_position, right_by_position,
-                                           ignore_pos_arg_names):
+                                           ignore_pos_arg_names, use_proper_subtype):
                     return False
                 j += 1
             continue
@@ -389,7 +397,7 @@ def is_callable_subtype(left: CallableType, right: CallableType,
                 right_by_name = right.argument_by_name(name)
                 assert right_by_name is not None
                 if not are_args_compatible(left_by_name, right_by_name,
-                                           ignore_pos_arg_names):
+                                           ignore_pos_arg_names, use_proper_subtype):
                     return False
             continue
 
@@ -398,7 +406,7 @@ def is_callable_subtype(left: CallableType, right: CallableType,
         if left_arg is None:
             return False
 
-        if not are_args_compatible(left_arg, right_arg, ignore_pos_arg_names):
+        if not are_args_compatible(left_arg, right_arg, ignore_pos_arg_names, use_proper_subtype):
             return False
 
     done_with_positional = False
@@ -414,11 +422,11 @@ def is_callable_subtype(left: CallableType, right: CallableType,
 
         # Check that *args and **kwargs types match in this loop
         if left_kind == ARG_STAR:
-            if right_star_type is not None and not is_subtype(right_star_type, left_arg.typ):
+            if right_star_type is not None and not is_compat(right_star_type, left_arg.typ):
                 return False
             continue
         elif left_kind == ARG_STAR2:
-            if right_star2_type is not None and not is_subtype(right_star2_type, left_arg.typ):
+            if right_star2_type is not None and not is_compat(right_star2_type, left_arg.typ):
                 return False
             continue
 
@@ -449,7 +457,8 @@ def is_callable_subtype(left: CallableType, right: CallableType,
 def are_args_compatible(
         left: FormalArgument,
         right: FormalArgument,
-        ignore_pos_arg_names: bool) -> bool:
+        ignore_pos_arg_names: bool,
+        use_proper_subtype: bool) -> bool:
     # If right has a specific name it wants this argument to be, left must
     # have the same.
     if right.name is not None and left.name != right.name:
@@ -460,8 +469,12 @@ def are_args_compatible(
     if right.pos is not None and left.pos != right.pos:
         return False
     # Left must have a more general type
-    if not is_subtype(right.typ, left.typ):
-        return False
+    if use_proper_subtype:
+        if not is_proper_subtype(right.typ, left.typ):
+            return False
+    else:
+        if not is_subtype(right.typ, left.typ):
+            return False
     # If right's argument is optional, left's must also be.
     if not right.required and left.required:
         return False
@@ -496,52 +509,192 @@ def unify_generic_callable(type: CallableType, target: CallableType,
 
 
 def restrict_subtype_away(t: Type, s: Type) -> Type:
-    """Return a supertype of (t intersect not s)
+    """Return t minus s.
 
-    Currently just remove elements of a union type.
+    If we can't determine a precise result, return a supertype of the
+    ideal result (just t is a valid result).
+
+    This is used for type inference of runtime type checks such as
+    isinstance.
+
+    Currently this just removes elements of a union type.
     """
     if isinstance(t, UnionType):
-        new_items = [item for item in t.items if (not is_subtype(item, s)
-                                                  or isinstance(item, AnyType))]
+        # Since runtime type checks will ignore type arguments, erase the types.
+        erased_s = erase_type(s)
+        new_items = [item for item in t.items
+                     if (not is_proper_subtype(erase_type(item), erased_s)
+                         or isinstance(item, AnyType))]
         return UnionType.make_union(new_items)
     else:
         return t
 
 
-def is_proper_subtype(t: Type, s: Type) -> bool:
-    """Check if t is a proper subtype of s?
+def is_proper_subtype(left: Type, right: Type) -> bool:
+    """Is left a proper subtype of right?
 
     For proper subtypes, there's no need to rely on compatibility due to
-    Any types. Any instance type t is also a proper subtype of t.
+    Any types. Every usable type is a proper subtype of itself.
     """
-    # FIX tuple types
-    if isinstance(s, UnionType):
-        if isinstance(t, UnionType):
-            return all([is_proper_subtype(item, s) for item in t.items])
-        else:
-            return any([is_proper_subtype(t, item) for item in s.items])
+    if isinstance(right, UnionType) and not isinstance(left, UnionType):
+        return any([is_proper_subtype(left, item)
+                    for item in right.items])
+    return left.accept(ProperSubtypeVisitor(right))
+
+
+class ProperSubtypeVisitor(TypeVisitor[bool]):
+    def __init__(self, right: Type) -> None:
+        self.right = right
 
-    if isinstance(t, Instance):
-        if isinstance(s, Instance):
-            if not t.type.has_base(s.type.fullname()):
+    def visit_unbound_type(self, left: UnboundType) -> bool:
+        # This can be called if there is a bad type annotation. The result probably
+        # doesn't matter much but by returning True we simplify these bad types away
+        # from unions, which could filter out some bogus messages.
+        return True
+
+    def visit_error_type(self, left: ErrorType) -> bool:
+        # This isn't a real type.
+        return False
+
+    def visit_type_list(self, left: TypeList) -> bool:
+        assert False, 'Should not happen'
+
+    def visit_any(self, left: AnyType) -> bool:
+        return isinstance(self.right, AnyType)
+
+    def visit_none_type(self, left: NoneTyp) -> bool:
+        if experiments.STRICT_OPTIONAL:
+            return (isinstance(self.right, NoneTyp) or
+                    is_named_instance(self.right, 'builtins.object'))
+        return True
+
+    def visit_uninhabited_type(self, left: UninhabitedType) -> bool:
+        return True
+
+    def visit_erased_type(self, left: ErasedType) -> bool:
+        # This may be encountered during type inference. The result probably doesn't
+        # matter much.
+        return True
+
+    def visit_deleted_type(self, left: DeletedType) -> bool:
+        return True
+
+    def visit_instance(self, left: Instance) -> bool:
+        right = self.right
+        if isinstance(right, Instance):
+            for base in left.type.mro:
+                if base._promote and is_proper_subtype(base._promote, right):
+                    return True
+
+            if not left.type.has_base(right.type.fullname()):
                 return False
 
-            def check_argument(left: Type, right: Type, variance: int) -> bool:
+            def check_argument(leftarg: Type, rightarg: Type, variance: int) -> bool:
                 if variance == COVARIANT:
-                    return is_proper_subtype(left, right)
+                    return is_proper_subtype(leftarg, rightarg)
                 elif variance == CONTRAVARIANT:
-                    return is_proper_subtype(right, left)
+                    return is_proper_subtype(rightarg, leftarg)
                 else:
-                    return sametypes.is_same_type(left, right)
+                    return sametypes.is_same_type(leftarg, rightarg)
 
             # Map left type to corresponding right instances.
-            t = map_instance_to_supertype(t, s.type)
+            left = map_instance_to_supertype(left, right.type)
 
             return all(check_argument(ta, ra, tvar.variance) for ta, ra, tvar in
-                       zip(t.args, s.args, s.type.defn.type_vars))
+                       zip(left.args, right.args, right.type.defn.type_vars))
+        return False
+
+    def visit_type_var(self, left: TypeVarType) -> bool:
+        if isinstance(self.right, TypeVarType) and left.id == self.right.id:
+            return True
+        # TODO: Value restrictions
+        return is_proper_subtype(left.upper_bound, self.right)
+
+    def visit_callable_type(self, left: CallableType) -> bool:
+        right = self.right
+        if isinstance(right, CallableType):
+            return is_callable_subtype(
+                left, right,
+                ignore_pos_arg_names=False,
+                use_proper_subtype=True)
+        elif isinstance(right, Overloaded):
+            return all(is_proper_subtype(left, item)
+                       for item in right.items())
+        elif isinstance(right, Instance):
+            return is_proper_subtype(left.fallback, right)
+        elif isinstance(right, TypeType):
+            # This is unsound, we don't check the __init__ signature.
+            return left.is_type_obj() and is_proper_subtype(left.ret_type, right.item)
+        return False
+
+    def visit_tuple_type(self, left: TupleType) -> bool:
+        right = self.right
+        if isinstance(right, Instance):
+            if (is_named_instance(right, 'builtins.tuple') or
+                    is_named_instance(right, 'typing.Iterable') or
+                    is_named_instance(right, 'typing.Container') or
+                    is_named_instance(right, 'typing.Sequence') or
+                    is_named_instance(right, 'typing.Reversible')):
+                if not right.args:
+                    return False
+                iter_type = right.args[0]
+                if is_named_instance(right, 'builtins.tuple') and isinstance(iter_type, AnyType):
+                    # TODO: We shouldn't need this special case. This is currently needed
+                    #       for isinstance(x, tuple), though it's unclear why.
+                    return True
+                return all(is_proper_subtype(li, iter_type) for li in left.items)
+            return is_proper_subtype(left.fallback, right)
+        elif isinstance(right, TupleType):
+            if len(left.items) != len(right.items):
+                return False
+            for l, r in zip(left.items, right.items):
+                if not is_proper_subtype(l, r):
+                    return False
+            return is_proper_subtype(left.fallback, right.fallback)
+        return False
+
+    def visit_typeddict_type(self, left: TypedDictType) -> bool:
+        right = self.right
+        if isinstance(right, TypedDictType):
+            for name, typ in left.items.items():
+                if name in right.items and not is_same_type(typ, right.items[name]):
+                    return False
+            for name, typ in right.items.items():
+                if name not in left.items:
+                    return False
+            return True
+        return is_proper_subtype(left.fallback, right)
+
+    def visit_overloaded(self, left: Overloaded) -> bool:
+        # TODO: What's the right thing to do here?
+        return False
+
+    def visit_union_type(self, left: UnionType) -> bool:
+        return all([is_proper_subtype(item, self.right) for item in left.items])
+
+    def visit_partial_type(self, left: PartialType) -> bool:
+        # TODO: What's the right thing to do here?
+        return False
+
+    def visit_type_type(self, left: TypeType) -> bool:
+        # TODO: Handle metaclasses?
+        right = self.right
+        if isinstance(right, TypeType):
+            # This is unsound, we don't check the __init__ signature.
+            return is_proper_subtype(left.item, right.item)
+        if isinstance(right, CallableType):
+            # This is also unsound because of __init__.
+            return right.is_type_obj() and is_proper_subtype(left.item, right.ret_type)
+        if isinstance(right, Instance):
+            if right.type.fullname() == 'builtins.type':
+                # TODO: Strictly speaking, the type builtins.type is considered equivalent to
+                #       Type[Any]. However, this would break the is_proper_subtype check in
+                #       conditional_type_map for cases like isinstance(x, type) when the type
+                #       of x is Type[int]. It's unclear what's the right way to address this.
+                return True
+            if right.type.fullname() == 'builtins.object':
+                return True
         return False
-    else:
-        return sametypes.is_same_type(t, s)
 
 
 def is_more_precise(t: Type, s: Type) -> bool:
diff --git a/mypy/test/testtypes.py b/mypy/test/testtypes.py
index 9fc6a71b5594..3c1c31fd6c90 100644
--- a/mypy/test/testtypes.py
+++ b/mypy/test/testtypes.py
@@ -658,7 +658,7 @@ def test_tuples(self) -> None:
 
         self.assert_meet(self.tuple(self.fx.a, self.fx.a),
                          self.fx.std_tuple,
-                         NoneTyp())
+                         self.tuple(self.fx.a, self.fx.a))
         self.assert_meet(self.tuple(self.fx.a),
                          self.tuple(self.fx.a, self.fx.a),
                          NoneTyp())
diff --git a/mypy/typeanal.py b/mypy/typeanal.py
index e33daa2eed3c..930d8eb6a6df 100644
--- a/mypy/typeanal.py
+++ b/mypy/typeanal.py
@@ -7,7 +7,7 @@
     Type, UnboundType, TypeVarType, TupleType, TypedDictType, UnionType, Instance,
     AnyType, CallableType, NoneTyp, DeletedType, TypeList, TypeVarDef, TypeVisitor,
     StarType, PartialType, EllipsisType, UninhabitedType, TypeType, get_typ_args, set_typ_args,
-    get_type_vars,
+    get_type_vars, union_items
 )
 from mypy.nodes import (
     BOUND_TVAR, UNBOUND_TVAR, TYPE_ALIAS, UNBOUND_IMPORTED,
@@ -109,7 +109,7 @@ def visit_unbound_type(self, t: UnboundType) -> Type:
             t.optional = False
             # We don't need to worry about double-wrapping Optionals or
             # wrapping Anys: Union simplification will take care of that.
-            return UnionType.make_simplified_union([self.visit_unbound_type(t), NoneTyp()])
+            return make_optional_type(self.visit_unbound_type(t))
         sym = self.lookup(t.name, t)
         if sym is not None:
             if sym.node is None:
@@ -151,7 +151,7 @@ def visit_unbound_type(self, t: UnboundType) -> Type:
                     self.fail('Optional[...] must have exactly one type argument', t)
                     return AnyType()
                 item = self.anal_type(t.args[0])
-                return UnionType.make_simplified_union([item, NoneTyp()])
+                return make_optional_type(item)
             elif fullname == 'typing.Callable':
                 return self.analyze_callable_type(t)
             elif fullname == 'typing.Type':
@@ -557,3 +557,21 @@ def visit_partial_type(self, t: PartialType) -> None:
 
     def visit_type_type(self, t: TypeType) -> None:
         pass
+
+
+def make_optional_type(t: Type) -> Type:
+    """Return the type corresponding to Optional[t].
+
+    Note that we can't use normal union simplification, since this function
+    is called during semantic analysis and simplification only works during
+    type checking.
+    """
+    if not experiments.STRICT_OPTIONAL:
+        return t
+    if isinstance(t, NoneTyp):
+        return t
+    if isinstance(t, UnionType):
+        items = [item for item in union_items(t)
+                 if not isinstance(item, NoneTyp)]
+        return UnionType(items + [NoneTyp()], t.line, t.column)
+    return UnionType([t, NoneTyp()], t.line, t.column)
diff --git a/mypy/types.py b/mypy/types.py
index 3da1609421c3..95f59b849a48 100644
--- a/mypy/types.py
+++ b/mypy/types.py
@@ -996,6 +996,23 @@ def make_union(items: List[Type], line: int = -1, column: int = -1) -> Type:
 
     @staticmethod
     def make_simplified_union(items: List[Type], line: int = -1, column: int = -1) -> Type:
+        """Build union type with redundant union items removed.
+
+        If only a single item remains, this may return a non-union type.
+
+        Examples:
+
+        * [int, str] -> Union[int, str]
+        * [int, object] -> object
+        * [int, int] -> int
+        * [int, Any] -> Union[int, Any] (Any types are not simplified away!)
+        * [Any, Any] -> Any
+
+        Note: This must NOT be used during semantic analysis, since TypeInfos may not
+              be fully initialized.
+        """
+        # TODO: Make this a function living somewhere outside mypy.types. Most other non-trivial
+        #       type operations are not static methods, so this is inconsistent.
         while any(isinstance(typ, UnionType) for typ in items):
             all_items = []  # type: List[Type]
             for typ in items:
@@ -1005,11 +1022,7 @@ def make_simplified_union(items: List[Type], line: int = -1, column: int = -1) -
                     all_items.append(typ)
             items = all_items
 
-        if any(isinstance(typ, AnyType) for typ in items):
-            return AnyType()
-
-        from mypy.subtypes import is_subtype
-        from mypy.sametypes import is_same_type
+        from mypy.subtypes import is_proper_subtype
 
         removed = set()  # type: Set[int]
         for i, ti in enumerate(items):
@@ -1017,10 +1030,8 @@ def make_simplified_union(items: List[Type], line: int = -1, column: int = -1) -
             # Keep track of the truishness info for deleted subtypes which can be relevant
             cbt = cbf = False
             for j, tj in enumerate(items):
-                if (i != j
-                    and is_subtype(tj, ti)
-                    and (not (isinstance(tj, Instance) and tj.type.fallback_to_any)
-                         or is_same_type(ti, tj))):
+                if (i != j and is_proper_subtype(tj, ti)):
+                    # We found a redundant item in the union.
                     removed.add(j)
                     cbt = cbt or tj.can_be_true
                     cbf = cbf or tj.can_be_false
@@ -1724,7 +1735,7 @@ def set_typ_args(tp: Type, new_args: List[Type], line: int = -1, column: int = -
     if isinstance(tp, TupleType):
         return tp.copy_modified(items=new_args)
     if isinstance(tp, UnionType):
-        return UnionType.make_simplified_union(new_args, line, column)
+        return UnionType(new_args, line, column)
     if isinstance(tp, CallableType):
         return tp.copy_modified(arg_types=new_args[:-1], ret_type=new_args[-1],
                                 line=line, column=column)
@@ -1752,6 +1763,20 @@ def get_type_vars(typ: Type) -> List[TypeVarType]:
     return tvars
 
 
+def union_items(typ: Type) -> List[Type]:
+    """Return the flattened items of a union type.
+
+    For non-union types, return a list containing just the argument.
+    """
+    if isinstance(typ, UnionType):
+        items = []
+        for item in typ.items:
+            items.extend(union_items(item))
+        return items
+    else:
+        return [typ]
+
+
 deserialize_map = {
     key: obj.deserialize  # type: ignore
     for key, obj in globals().items()
diff --git a/test-data/unit/check-classes.test b/test-data/unit/check-classes.test
index 84932472c858..ce2ee52d0df6 100644
--- a/test-data/unit/check-classes.test
+++ b/test-data/unit/check-classes.test
@@ -2439,9 +2439,9 @@ class A: pass
 class B(A): pass
 
 @overload
-def f(a: Type[A]) -> int: pass  # E: Overloaded function signatures 1 and 2 overlap with incompatible return types
+def f(a: Type[B]) -> int: pass  # E: Overloaded function signatures 1 and 2 overlap with incompatible return types
 @overload
-def f(a: Type[B]) -> str: pass
+def f(a: Type[A]) -> str: pass
 [builtins fixtures/classmethod.pyi]
 [out]
 
diff --git a/test-data/unit/check-dynamic-typing.test b/test-data/unit/check-dynamic-typing.test
index 9529a421977a..70d6d32aa475 100644
--- a/test-data/unit/check-dynamic-typing.test
+++ b/test-data/unit/check-dynamic-typing.test
@@ -79,8 +79,8 @@ n = 0
 d in a  # E: Unsupported right operand type for in ("A")
 d and a
 d or a
-c = d and b # Unintuitive type inference?
-c = d or b  # Unintuitive type inference?
+c = d and b # E: Incompatible types in assignment (expression has type "Union[Any, bool]", variable has type "C")
+c = d or b  # E: Incompatible types in assignment (expression has type "Union[Any, bool]", variable has type "C")
 
 c = d + a
 c = d - a
@@ -123,8 +123,8 @@ n = 0
 a and d
 a or d
 c = a in d
-c = b and d # Unintuitive type inference?
-c = b or d  # Unintuitive type inference?
+c = b and d # E: Incompatible types in assignment (expression has type "Union[bool, Any]", variable has type "C")
+c = b or d  # E: Incompatible types in assignment (expression has type "Union[bool, Any]", variable has type "C")
 b = a + d
 b = a / d
 
diff --git a/test-data/unit/check-generics.test b/test-data/unit/check-generics.test
index 7d035d0ed992..64d010e313fd 100644
--- a/test-data/unit/check-generics.test
+++ b/test-data/unit/check-generics.test
@@ -779,7 +779,7 @@ if not isinstance(s, str):
 
 z = None # type: TNode # Same as TNode[Any]
 z.x
-z.foo() # Any simplifies Union to Any now. This test should be updated after #2197
+z.foo() # E: Some element of union has no attribute "foo"
 
 [builtins fixtures/isinstance.pyi]
 
diff --git a/test-data/unit/check-isinstance.test b/test-data/unit/check-isinstance.test
index 973d463d6085..1490dc0bb089 100644
--- a/test-data/unit/check-isinstance.test
+++ b/test-data/unit/check-isinstance.test
@@ -399,6 +399,7 @@ def f(x: Union[List[int], List[str], int]) -> None:
             a + 'x' # E: Unsupported operand types for + ("int" and "str")
 
         # type of a?
+        reveal_type(x) # E: Revealed type is 'Union[builtins.list[builtins.int], builtins.list[builtins.str]]'
         x + 1 # E: Unsupported operand types for + (likely involving Union)
     else:
         x[0] # E: Value of type "int" is not indexable
@@ -910,7 +911,8 @@ def foo() -> Union[int, str, A]: pass
 
 def bar() -> None:
     x = foo()
-    x + 1  # E: Unsupported left operand type for + (some union)
+    x + 1  # E: Unsupported left operand type for + (some union) \
+           # E: Unsupported operand types for + (likely involving Union)
     if isinstance(x, A):
        x.a
     else:
@@ -1275,6 +1277,7 @@ if isinstance(x, A):
     reveal_type(x)  # unreachable
 else:
     reveal_type(x)  # E: Revealed type is '__main__.B'
+reveal_type(x)  # E: Revealed type is '__main__.B'
 [builtins fixtures/isinstance.pyi]
 
 [case testAssertIsinstance]
@@ -1305,6 +1308,9 @@ from typing import List, Union
 def f(x: Union[List[int], str]) -> None:
     if isinstance(x, list):
         x[0]()
+    else:
+        reveal_type(x) # E: Revealed type is 'builtins.str'
+    reveal_type(x) # E: Revealed type is 'Union[builtins.list[builtins.int], builtins.str]'
 [builtins fixtures/isinstancelist.pyi]
 [out]
 main:4: error: "int" not callable
@@ -1322,6 +1328,7 @@ if isinstance(x1, B) or isinstance(x1, C):
 else:
     reveal_type(x1) # E: Revealed type is '__main__.A'
     f = 0
+reveal_type(x1) # E: Revealed type is '__main__.A'
 x2 = A()
 if isinstance(x2, A) or isinstance(x2, C):
     reveal_type(x2) # E: Revealed type is '__main__.A'
@@ -1329,6 +1336,7 @@ if isinstance(x2, A) or isinstance(x2, C):
 else:
     # unreachable
     1()
+reveal_type(x2) # E: Revealed type is '__main__.A'
 [builtins fixtures/isinstance.pyi]
 [out]
 [case testComprehensionIsInstance]
@@ -1370,6 +1378,7 @@ def f(x: Union[int, str], typ: type) -> None:
         reveal_type(x)  # E: Revealed type is 'Union[builtins.int, builtins.str]'
     else:
         reveal_type(x)  # E: Revealed type is 'builtins.str'
+    reveal_type(x) # E: Revealed type is 'Union[builtins.int, builtins.str]'
 [builtins fixtures/isinstancelist.pyi]
 
 
@@ -1382,6 +1391,7 @@ def f(x: Union[int, A], a: Type[A]) -> None:
         reveal_type(x)  # E: Revealed type is 'Union[builtins.int, __main__.A]'
     else:
         reveal_type(x)  # E: Revealed type is '__main__.A'
+    reveal_type(x) # E: Revealed type is 'Union[builtins.int, __main__.A]'
 
 [builtins fixtures/isinstancelist.pyi]
 
@@ -1412,3 +1422,29 @@ def f(x: Union[int, A], a: Type[A]) -> None:
 
 [builtins fixtures/isinstancelist.pyi]
 
+
+[case testIsinstanceAndNarrowTypeVariable]
+from typing import TypeVar
+
+class A: pass
+class B(A): pass
+
+T = TypeVar('T', bound=A)
+
+def f(x: T) -> None:
+    if isinstance(x, B):
+        reveal_type(x) # E: Revealed type is '__main__.B'
+    else:
+        reveal_type(x) # E: Revealed type is 'T`-1'
+    reveal_type(x) # E: Revealed type is 'T`-1'
+[builtins fixtures/isinstance.pyi]
+
+[case testIsinstanceAndTypeType]
+from typing import Type
+def f(x: Type[int]) -> None:
+    if isinstance(x, type):
+        reveal_type(x) # E: Revealed type is 'Type[builtins.int]'
+    else:
+        reveal_type(x)  # Unreachable
+    reveal_type(x) # E: Revealed type is 'Type[builtins.int]'
+[builtins fixtures/isinstancelist.pyi]
diff --git a/test-data/unit/check-namedtuple.test b/test-data/unit/check-namedtuple.test
index 71a058b24ac6..51260733064a 100644
--- a/test-data/unit/check-namedtuple.test
+++ b/test-data/unit/check-namedtuple.test
@@ -427,3 +427,25 @@ from typing import NamedTuple
 def f() -> None:
     A = NamedTuple('A', [('x', int)])
 A  # E: Name 'A' is not defined
+
+[case testNamedTupleWithImportCycle]
+import a
+[file a.py]
+from collections import namedtuple
+from b import f
+
+N = namedtuple('N', 'a')
+
+class X(N): pass
+[file b.py]
+import a
+
+def f(x: a.X) -> None:
+    # The type of x is broken (https://github.com/python/mypy/issues/3016) but we need to
+    # do something reasonable here to avoid a regression.
+    reveal_type(x)
+    x = a.X(1)
+    reveal_type(x)
+[out]
+tmp/b.py:6: error: Revealed type is 'a.X'
+tmp/b.py:8: error: Revealed type is 'Tuple[Any, fallback=a.X]'
diff --git a/test-data/unit/check-optional.test b/test-data/unit/check-optional.test
index 4286aab48bfd..05a9c93529f9 100644
--- a/test-data/unit/check-optional.test
+++ b/test-data/unit/check-optional.test
@@ -75,6 +75,7 @@ if x is None:
   reveal_type(x)  # E: Revealed type is 'builtins.None'
 else:
   reveal_type(x)  # E: Revealed type is 'builtins.int'
+reveal_type(x)  # E: Revealed type is 'Union[builtins.int, builtins.None]'
 [builtins fixtures/bool.pyi]
 
 [case testAnyCanBeNone]
@@ -537,9 +538,10 @@ f = lambda x: None
 f(0)
 [builtins fixtures/function.pyi]
 
-[case testUnionSimplificationWithStrictOptional]
+[case testDontSimplifyNoneUnionsWithStrictOptional]
 from typing import Any, TypeVar, Union
-class C(Any): pass
+A = None  # type: Any
+class C(A): pass
 T = TypeVar('T')
 S = TypeVar('S')
 def u(x: T, y: S) -> Union[S, T]: pass
@@ -549,9 +551,39 @@ a = None # type: Any
 reveal_type(u(C(), None))  # E: Revealed type is 'Union[builtins.None, __main__.C*]'
 reveal_type(u(None, C()))  # E: Revealed type is 'Union[__main__.C*, builtins.None]'
 
-# This will be fixed later
-reveal_type(u(a, None))  # E: Revealed type is 'Any'
-reveal_type(u(None, a))  # E: Revealed type is 'Any'
+reveal_type(u(a, None))  # E: Revealed type is 'Union[builtins.None, Any]'
+reveal_type(u(None, a))  # E: Revealed type is 'Union[Any, builtins.None]'
 
 reveal_type(u(1, None))  # E: Revealed type is 'Union[builtins.None, builtins.int*]'
 reveal_type(u(None, 1))  # E: Revealed type is 'Union[builtins.int*, builtins.None]'
+
+[case testOptionalAndAnyBaseClass]
+from typing import Any, Optional
+A = None  # type: Any
+class C(A):
+    pass
+x = None  # type: Optional[C]
+x.foo()  # E: Some element of union has no attribute "foo"
+
+[case testIsinstanceAndOptionalAndAnyBase]
+from typing import Any, Optional
+
+B = None  # type: Any
+class A(B): pass
+
+def f(a: Optional[A]):
+    reveal_type(a) # E: Revealed type is 'Union[__main__.A, builtins.None]'
+    if a is not None:
+        reveal_type(a) # E: Revealed type is '__main__.A'
+    else:
+        reveal_type(a) # E: Revealed type is 'builtins.None'
+    reveal_type(a) # E: Revealed type is 'Union[__main__.A, builtins.None]'
+[builtins fixtures/isinstance.pyi]
+
+[case testFlattenOptionalUnion]
+from typing import Optional, Union
+
+x: Optional[Union[int, str]]
+reveal_type(x) # E: Revealed type is 'Union[builtins.int, builtins.str, builtins.None]'
+y: Optional[Union[int, None]]
+reveal_type(y) # E: Revealed type is 'Union[builtins.int, builtins.None]'
diff --git a/test-data/unit/check-statements.test b/test-data/unit/check-statements.test
index 2ac3619c438c..e33f3cc0a411 100644
--- a/test-data/unit/check-statements.test
+++ b/test-data/unit/check-statements.test
@@ -723,11 +723,11 @@ try:
 except BaseException as e1:
     reveal_type(e1)  # E: Revealed type is 'builtins.BaseException'
 except (E1, BaseException) as e2:
-    reveal_type(e2)  # E: Revealed type is 'Any'
+    reveal_type(e2)  # E: Revealed type is 'Union[Any, builtins.BaseException]'
 except (E1, E2) as e3:
-    reveal_type(e3)  # E: Revealed type is 'Any'
+    reveal_type(e3)  # E: Revealed type is 'Union[Any, __main__.E2]'
 except (E1, E2, BaseException) as e4:
-    reveal_type(e4)  # E: Revealed type is 'Any'
+    reveal_type(e4)  # E: Revealed type is 'Union[Any, builtins.BaseException]'
 
 try: pass
 except E1 as e1:
diff --git a/test-data/unit/check-tuples.test b/test-data/unit/check-tuples.test
index c836fe8cd41e..08345706f0d9 100644
--- a/test-data/unit/check-tuples.test
+++ b/test-data/unit/check-tuples.test
@@ -826,7 +826,7 @@ def g(x: Union[str, Tuple[str, str]]) -> None:
 [builtins fixtures/tuple.pyi]
 [out]
 
-[case testTupleMeetTUpleAnyComplex]
+[case testTupleMeetTupleAnyComplex]
 from typing import Tuple, Union
 
 Pair = Tuple[int, int]
diff --git a/test-data/unit/check-typeddict.test b/test-data/unit/check-typeddict.test
index 78fade8c8258..74d958dee3df 100644
--- a/test-data/unit/check-typeddict.test
+++ b/test-data/unit/check-typeddict.test
@@ -610,3 +610,60 @@ def f() -> None:
     A = TypedDict('A', {'x': int})
 A  # E: Name 'A' is not defined
 [builtins fixtures/dict.pyi]
+
+
+-- Union simplification / proper subtype checks
+
+[case testTypedDictUnionSimplification]
+from typing import TypeVar, Union, Any, cast
+from mypy_extensions import TypedDict
+
+T = TypeVar('T')
+S = TypeVar('S')
+def u(x: T, y: S) -> Union[S, T]: pass
+
+C = TypedDict('C', {'a': int})
+D = TypedDict('D', {'a': int, 'b': int})
+E = TypedDict('E', {'a': str})
+F = TypedDict('F', {'x': int})
+G = TypedDict('G', {'a': Any})
+
+c = C(a=1)
+d = D(a=1, b=1)
+e = E(a='')
+f = F(x=1)
+g = G(a=cast(Any, 1))  # Work around #2610
+
+reveal_type(u(d, d)) # E: Revealed type is 'TypedDict(a=builtins.int, b=builtins.int, _fallback=typing.Mapping[builtins.str, builtins.int])'
+reveal_type(u(c, d)) # E: Revealed type is 'TypedDict(a=builtins.int, _fallback=typing.Mapping[builtins.str, builtins.int])'
+reveal_type(u(d, c)) # E: Revealed type is 'TypedDict(a=builtins.int, _fallback=typing.Mapping[builtins.str, builtins.int])'
+reveal_type(u(c, e)) # E: Revealed type is 'Union[TypedDict(a=builtins.str, _fallback=typing.Mapping[builtins.str, builtins.str]), TypedDict(a=builtins.int, _fallback=typing.Mapping[builtins.str, builtins.int])]'
+reveal_type(u(e, c)) # E: Revealed type is 'Union[TypedDict(a=builtins.int, _fallback=typing.Mapping[builtins.str, builtins.int]), TypedDict(a=builtins.str, _fallback=typing.Mapping[builtins.str, builtins.str])]'
+reveal_type(u(c, f)) # E: Revealed type is 'Union[TypedDict(x=builtins.int, _fallback=typing.Mapping[builtins.str, builtins.int]), TypedDict(a=builtins.int, _fallback=typing.Mapping[builtins.str, builtins.int])]'
+reveal_type(u(f, c)) # E: Revealed type is 'Union[TypedDict(a=builtins.int, _fallback=typing.Mapping[builtins.str, builtins.int]), TypedDict(x=builtins.int, _fallback=typing.Mapping[builtins.str, builtins.int])]'
+reveal_type(u(c, g)) # E: Revealed type is 'Union[TypedDict(a=Any, _fallback=typing.Mapping[builtins.str, Any]), TypedDict(a=builtins.int, _fallback=typing.Mapping[builtins.str, builtins.int])]'
+reveal_type(u(g, c)) # E: Revealed type is 'Union[TypedDict(a=builtins.int, _fallback=typing.Mapping[builtins.str, builtins.int]), TypedDict(a=Any, _fallback=typing.Mapping[builtins.str, Any])]'
+[builtins fixtures/dict.pyi]
+
+[case testTypedDictUnionSimplification2]
+from typing import TypeVar, Union, Mapping, Any
+from mypy_extensions import TypedDict
+
+T = TypeVar('T')
+S = TypeVar('S')
+def u(x: T, y: S) -> Union[S, T]: pass
+
+C = TypedDict('C', {'a': int, 'b': int})
+
+c = C(a=1, b=1)
+m_s_i: Mapping[str, int]
+m_s_s: Mapping[str, str]
+m_i_i: Mapping[int, int]
+m_s_a: Mapping[str, Any]
+
+reveal_type(u(c, m_s_i)) # E: Revealed type is 'typing.Mapping*[builtins.str, builtins.int]'
+reveal_type(u(m_s_i, c)) # E: Revealed type is 'typing.Mapping*[builtins.str, builtins.int]'
+reveal_type(u(c, m_s_s)) # E: Revealed type is 'Union[typing.Mapping*[builtins.str, builtins.str], TypedDict(a=builtins.int, b=builtins.int, _fallback=typing.Mapping[builtins.str, builtins.int])]'
+reveal_type(u(c, m_i_i)) # E: Revealed type is 'Union[typing.Mapping*[builtins.int, builtins.int], TypedDict(a=builtins.int, b=builtins.int, _fallback=typing.Mapping[builtins.str, builtins.int])]'
+reveal_type(u(c, m_s_a)) # E: Revealed type is 'Union[typing.Mapping*[builtins.str, Any], TypedDict(a=builtins.int, b=builtins.int, _fallback=typing.Mapping[builtins.str, builtins.int])]'
+[builtins fixtures/dict.pyi]
diff --git a/test-data/unit/check-unions.test b/test-data/unit/check-unions.test
index f6a149e354b8..4f2539f10a43 100644
--- a/test-data/unit/check-unions.test
+++ b/test-data/unit/check-unions.test
@@ -37,7 +37,7 @@ def f(x: Union[int, str]) -> None:
 [case testUnionAnyIsInstance]
 from typing import Any, Union
 
-def func(v:Union[int, Any]) -> None:
+def func(v: Union[int, Any]) -> None:
     if isinstance(v, int):
         reveal_type(v) # E: Revealed type is 'builtins.int'
     else:
@@ -61,7 +61,8 @@ y = w.y
 z = w.y       # E: Incompatible types in assignment (expression has type "int", variable has type "str")
 w.y = 'a'     # E: Incompatible types in assignment (expression has type "str", variable has type "int")
 y = x.y       # E: Some element of union has no attribute "y"
-z = x.y       # E: Some element of union has no attribute "y"
+zz = x.y      # E: Some element of union has no attribute "y"
+z = zz        # E: Incompatible types in assignment (expression has type "Union[int, Any]", variable has type "str")
 
 [builtins fixtures/isinstance.pyi]
 
@@ -186,9 +187,8 @@ a = None # type: Any
 reveal_type(u(C(), None))  # E: Revealed type is '__main__.C*'
 reveal_type(u(None, C()))  # E: Revealed type is '__main__.C*'
 
-# This will be fixed later
-reveal_type(u(C(), a))  # E: Revealed type is 'Any'
-reveal_type(u(a, C()))  # E: Revealed type is 'Any'
+reveal_type(u(C(), a))  # E: Revealed type is 'Union[Any, __main__.C*]'
+reveal_type(u(a, C()))  # E: Revealed type is 'Union[__main__.C*, Any]'
 
 reveal_type(u(C(), C()))  # E: Revealed type is '__main__.C*'
 reveal_type(u(a, a))  # E: Revealed type is 'Any'
@@ -220,3 +220,219 @@ class M(Generic[V]):
 def f(x: M[C]) -> None:
     y = x.get(None)
     reveal_type(y) # E: Revealed type is '__main__.C'
+
+[case testUnionSimplificationSpecialCases]
+from typing import Any, TypeVar, Union
+
+class C(Any): pass
+
+T = TypeVar('T')
+S = TypeVar('S')
+def u(x: T, y: S) -> Union[S, T]: pass
+
+a = None # type: Any
+
+# Base-class-Any and None, simplify
+reveal_type(u(C(), None))  # E: Revealed type is '__main__.C*'
+reveal_type(u(None, C()))  # E: Revealed type is '__main__.C*'
+
+# Normal instance type and None, simplify
+reveal_type(u(1, None))  # E: Revealed type is 'builtins.int*'
+reveal_type(u(None, 1))  # E: Revealed type is 'builtins.int*'
+
+# Normal instance type and base-class-Any, no simplification
+reveal_type(u(C(), 1))  # E: Revealed type is 'Union[builtins.int*, __main__.C*]'
+reveal_type(u(1, C()))  # E: Revealed type is 'Union[__main__.C*, builtins.int*]'
+
+# Normal instance type and Any, no simplification
+reveal_type(u(1, a))  # E: Revealed type is 'Union[Any, builtins.int*]'
+reveal_type(u(a, 1))  # E: Revealed type is 'Union[builtins.int*, Any]'
+
+# Any and base-class-Any, no simplificaiton
+reveal_type(u(C(), a))  # E: Revealed type is 'Union[Any, __main__.C*]'
+reveal_type(u(a, C()))  # E: Revealed type is 'Union[__main__.C*, Any]'
+
+# Two normal instance types, simplify
+reveal_type(u(1, object()))  # E: Revealed type is 'builtins.object*'
+reveal_type(u(object(), 1))  # E: Revealed type is 'builtins.object*'
+
+# Two normal instance types, no simplification
+reveal_type(u(1, ''))  # E: Revealed type is 'Union[builtins.str*, builtins.int*]'
+reveal_type(u('', 1))  # E: Revealed type is 'Union[builtins.int*, builtins.str*]'
+
+[case testUnionSimplificationWithDuplicateItems]
+from typing import Any, TypeVar, Union
+
+class C(Any): pass
+
+T = TypeVar('T')
+S = TypeVar('S')
+R = TypeVar('R')
+def u(x: T, y: S, z: R) -> Union[R, S, T]: pass
+
+a = None # type: Any
+
+reveal_type(u(1, 1, 1))  # E: Revealed type is 'builtins.int*'
+reveal_type(u(C(), C(), None))  # E: Revealed type is '__main__.C*'
+reveal_type(u(a, a, 1))  # E: Revealed type is 'Union[builtins.int*, Any]'
+reveal_type(u(a, C(), a))  # E: Revealed type is 'Union[Any, __main__.C*]'
+reveal_type(u('', 1, 1))  # E: Revealed type is 'Union[builtins.int*, builtins.str*]'
+
+[case testUnionAndBinaryOperation]
+from typing import Union
+class A: pass
+def f(x: Union[int, str, A]):
+    x + object() # E: Unsupported left operand type for + (some union) \
+        # E: Unsupported operand types for + (likely involving Union)
+
+[case testNarrowingDownNamedTupleUnion]
+from typing import NamedTuple, Union
+
+A = NamedTuple('A', [('y', int)])
+B = NamedTuple('B', [('x', int)])
+C = NamedTuple('C', [('x', int)])
+
+def foo(a: Union[A, B, C]):
+    if isinstance(a, (B, C)):
+        reveal_type(a) # E: Revealed type is 'Union[Tuple[builtins.int, fallback=__main__.B], Tuple[builtins.int, fallback=__main__.C]]'
+        a.x
+        a.y # E: Some element of union has no attribute "y"
+        b = a # type: Union[B, C]
+[builtins fixtures/isinstance.pyi]
+
+[case testSimplifyingUnionAndTypePromotions]
+from typing import TypeVar, Union
+T = TypeVar('T')
+S = TypeVar('S')
+def u(x: T, y: S) -> Union[S, T]: pass
+
+reveal_type(u(1, 2.3))  # E: Revealed type is 'builtins.float*'
+reveal_type(u(2.3, 1))  # E: Revealed type is 'builtins.float*'
+reveal_type(u(False, 2.2)) # E: Revealed type is 'builtins.float*'
+reveal_type(u(2.2, False)) # E: Revealed type is 'builtins.float*'
+[builtins fixtures/primitives.pyi]
+
+[case testSimplifyingUnionWithTypeTypes1]
+from typing import TypeVar, Union, Type, Any
+
+T = TypeVar('T')
+S = TypeVar('S')
+def u(x: T, y: S) -> Union[S, T]: pass
+
+t_o = None  # type: Type[object]
+t_s = None  # type: Type[str]
+t_a = None  # type: Type[Any]
+
+# Two identical items
+reveal_type(u(t_o, t_o)) # E: Revealed type is 'Type[builtins.object]'
+reveal_type(u(t_s, t_s)) # E: Revealed type is 'Type[builtins.str]'
+reveal_type(u(t_a, t_a)) # E: Revealed type is 'Type[Any]'
+reveal_type(u(type, type)) # E: Revealed type is 'def (x: builtins.Any) -> builtins.type'
+
+# One type, other non-type
+reveal_type(u(t_s, 1)) # E: Revealed type is 'Union[builtins.int*, Type[builtins.str]]'
+reveal_type(u(1, t_s)) # E: Revealed type is 'Union[Type[builtins.str], builtins.int*]'
+reveal_type(u(type, 1)) # E: Revealed type is 'Union[builtins.int*, def (x: builtins.Any) -> builtins.type]'
+reveal_type(u(1, type)) # E: Revealed type is 'Union[def (x: builtins.Any) -> builtins.type, builtins.int*]'
+reveal_type(u(t_a, 1)) # E: Revealed type is 'Union[builtins.int*, Type[Any]]'
+reveal_type(u(1, t_a)) # E: Revealed type is 'Union[Type[Any], builtins.int*]'
+reveal_type(u(t_o, 1)) # E: Revealed type is 'Union[builtins.int*, Type[builtins.object]]'
+reveal_type(u(1, t_o)) # E: Revealed type is 'Union[Type[builtins.object], builtins.int*]'
+
+[case testSimplifyingUnionWithTypeTypes2]
+from typing import TypeVar, Union, Type, Any
+
+T = TypeVar('T')
+S = TypeVar('S')
+def u(x: T, y: S) -> Union[S, T]: pass
+
+t_o = None  # type: Type[object]
+t_s = None  # type: Type[str]
+t_a = None  # type: Type[Any]
+t = None    # type: type
+
+# Union with object
+reveal_type(u(t_o, object())) # E: Revealed type is 'builtins.object*'
+reveal_type(u(object(), t_o)) # E: Revealed type is 'builtins.object*'
+reveal_type(u(t_s, object())) # E: Revealed type is 'builtins.object*'
+reveal_type(u(object(), t_s)) # E: Revealed type is 'builtins.object*'
+reveal_type(u(t_a, object())) # E: Revealed type is 'builtins.object*'
+reveal_type(u(object(), t_a)) # E: Revealed type is 'builtins.object*'
+
+# Union between type objects
+reveal_type(u(t_o, t_a)) # E: Revealed type is 'Union[Type[Any], Type[builtins.object]]'
+reveal_type(u(t_a, t_o)) # E: Revealed type is 'Union[Type[builtins.object], Type[Any]]'
+reveal_type(u(t_s, t_o)) # E: Revealed type is 'Type[builtins.object]'
+reveal_type(u(t_o, t_s)) # E: Revealed type is 'Type[builtins.object]'
+reveal_type(u(t_o, type)) # E: Revealed type is 'Type[builtins.object]'
+reveal_type(u(type, t_o)) # E: Revealed type is 'Type[builtins.object]'
+reveal_type(u(t_a, t)) # E: Revealed type is 'builtins.type*'
+reveal_type(u(t, t_a)) # E: Revealed type is 'builtins.type*'
+# The following should arguably not be simplified, but it's unclear how to fix then
+# without causing regressions elsewhere.
+reveal_type(u(t_o, t)) # E: Revealed type is 'builtins.type*'
+reveal_type(u(t, t_o)) # E: Revealed type is 'builtins.type*'
+
+[case testNotSimplifyingUnionWithMetaclass]
+from typing import TypeVar, Union, Type, Any
+
+class M(type): pass
+class M2(M): pass
+class A(metaclass=M): pass
+
+T = TypeVar('T')
+S = TypeVar('S')
+def u(x: T, y: S) -> Union[S, T]: pass
+
+a: Any
+t_a: Type[A]
+
+reveal_type(u(M(*a), t_a)) # E: Revealed type is 'Union[Type[__main__.A], __main__.M*]'
+reveal_type(u(t_a, M(*a))) # E: Revealed type is 'Union[__main__.M*, Type[__main__.A]]'
+
+reveal_type(u(M2(*a), t_a)) # E: Revealed type is 'Union[Type[__main__.A], __main__.M2*]'
+reveal_type(u(t_a, M2(*a))) # E: Revealed type is 'Union[__main__.M2*, Type[__main__.A]]'
+
+[case testSimplifyUnionWithCallable]
+from typing import TypeVar, Union, Any, Callable
+
+T = TypeVar('T')
+S = TypeVar('S')
+def u(x: T, y: S) -> Union[S, T]: pass
+
+class C: pass
+class D(C): pass
+
+D_C: Callable[[D], C]
+A_C: Callable[[Any], C]
+D_A: Callable[[D], Any]
+C_C: Callable[[C], C]
+D_D: Callable[[D], D]
+i_C: Callable[[int], C]
+
+# TODO: Test argument names and kinds once we have flexible callable types.
+
+reveal_type(u(D_C, D_C)) # E: Revealed type is 'def (__main__.D) -> __main__.C'
+
+reveal_type(u(A_C, D_C)) # E: Revealed type is 'Union[def (__main__.D) -> __main__.C, def (Any) -> __main__.C]'
+reveal_type(u(D_C, A_C)) # E: Revealed type is 'Union[def (Any) -> __main__.C, def (__main__.D) -> __main__.C]'
+
+reveal_type(u(D_A, D_C)) # E: Revealed type is 'Union[def (__main__.D) -> __main__.C, def (__main__.D) -> Any]'
+reveal_type(u(D_C, D_A)) # E: Revealed type is 'Union[def (__main__.D) -> Any, def (__main__.D) -> __main__.C]'
+
+reveal_type(u(D_C, C_C)) # E: Revealed type is 'def (__main__.D) -> __main__.C'
+reveal_type(u(C_C, D_C)) # E: Revealed type is 'def (__main__.D) -> __main__.C'
+
+reveal_type(u(D_C, D_D)) # E: Revealed type is 'def (__main__.D) -> __main__.C'
+reveal_type(u(D_D, D_C)) # E: Revealed type is 'def (__main__.D) -> __main__.C'
+
+reveal_type(u(D_C, i_C)) # E: Revealed type is 'Union[def (builtins.int) -> __main__.C, def (__main__.D) -> __main__.C]'
+
+[case testUnionOperatorMethodSpecialCase]
+from typing import Union
+class C:
+    def __le__(self, x: 'C') -> int: ...
+class D:
+    def __le__(self, other) -> int: ...
+class E:
+    def __ge__(self, other: Union[C, D]) -> int: ...
diff --git a/test-data/unit/fixtures/primitives.pyi b/test-data/unit/fixtures/primitives.pyi
index 3b0ba0ce3719..4b5611b0bace 100644
--- a/test-data/unit/fixtures/primitives.pyi
+++ b/test-data/unit/fixtures/primitives.pyi
@@ -11,7 +11,7 @@ class int:
     def __add__(self, i: int) -> int: pass
 class float: pass
 class complex: pass
-class bool: pass
+class bool(int): pass
 class str:
     def __add__(self, s: str) -> str: pass
     def format(self, *args) -> str: pass