From c53e0ca4b6baecead00365911ffe6a412fcef795 Mon Sep 17 00:00:00 2001
From: Jukka Lehtosalo <jukka.lehtosalo@iki.fi>
Date: Tue, 14 Mar 2017 12:13:21 +0000
Subject: [PATCH 01/17] Fixes to union simplification and isinstance

The main change is that unions containing Any are no longer simplified
to just Any.

This required changes in various other places to keep the existing
semantics, and resulted in some fixes to existing test cases.
---
 mypy/checkexpr.py                        |   5 +-
 mypy/meet.py                             |  26 +++--
 mypy/subtypes.py                         | 123 ++++++++++++++++++++++-
 mypy/types.py                            |  10 +-
 test-data/unit/check-classes.test        |   4 +-
 test-data/unit/check-dynamic-typing.test |   8 +-
 test-data/unit/check-generics.test       |   2 +-
 test-data/unit/check-isinstance.test     |   1 +
 test-data/unit/check-optional.test       |  28 +++++-
 test-data/unit/check-statements.test     |   6 +-
 test-data/unit/check-unions.test         |  73 +++++++++++++-
 11 files changed, 245 insertions(+), 41 deletions(-)

diff --git a/mypy/checkexpr.py b/mypy/checkexpr.py
index ba598f166a81..cd69f7336d1d 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
@@ -2213,8 +2213,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)
-                return ans
+                return narrow_declared_type(known_type, restriction)
         return known_type
 
 
diff --git a/mypy/meet.py b/mypy/meet.py
index e1e698683a76..45f6c28d1e96 100644
--- a/mypy/meet.py
+++ b/mypy/meet.py
@@ -25,21 +25,25 @@ 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."""
+    # TODO: What are the reasons for not just using meet_types()?
+    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
+    return meet_types(declared, narrowed)
 
 
 def is_overlapping_types(t: Type, s: Type, use_promotions: bool = False) -> bool:
diff --git a/mypy/subtypes.py b/mypy/subtypes.py
index c98bb8e8d144..43334087211f 100644
--- a/mypy/subtypes.py
+++ b/mypy/subtypes.py
@@ -508,12 +508,17 @@ def restrict_subtype_away(t: Type, s: Type) -> Type:
         return t
 
 
-def is_proper_subtype(t: Type, s: Type) -> bool:
+def is_proper_subtype(left: Type, right: Type) -> bool:
     """Check if t is a proper subtype of s?
 
     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.
     """
+    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))
+
     # FIX tuple types
     if isinstance(s, UnionType):
         if isinstance(t, UnionType):
@@ -544,6 +549,122 @@ def check_argument(left: Type, right: Type, variance: int) -> bool:
         return sametypes.is_same_type(t, s)
 
 
+class ProperSubtypeVisitor(TypeVisitor[bool]):
+    def __init__(self, right: Type) -> None:
+        self.right = right
+
+    def visit_unbound_type(self, left: UnboundType) -> bool:
+        return True
+
+    def visit_error_type(self, left: ErrorType) -> bool:
+        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_void(self, left: Void) -> bool:
+        return True
+
+    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'))
+        else:
+            return not isinstance(self.right, Void)
+
+    def visit_uninhabited_type(self, left: UninhabitedType) -> bool:
+        return not isinstance(self.right, Void)
+
+    def visit_erased_type(self, left: ErasedType) -> bool:
+        return True
+
+    def visit_deleted_type(self, left: DeletedType) -> bool:
+        return True
+
+    def visit_instance(self, left: Instance) -> bool:
+        if isinstance(self.right, Instance):
+            if not left.type.has_base(self.right.type.fullname()):
+                return False
+
+            def check_argument(leftarg: Type, rightarg: Type, variance: int) -> bool:
+                if variance == COVARIANT:
+                    return is_proper_subtype(leftarg, rightarg)
+                elif variance == CONTRAVARIANT:
+                    return is_proper_subtype(rightarg, leftarg)
+                else:
+                    return sametypes.is_same_type(leftarg, rightarg)
+
+            # Map left type to corresponding right instances.
+            left = map_instance_to_supertype(left, self.right.type)
+
+            return all(check_argument(ta, ra, tvar.variance) for ta, ra, tvar in
+                       zip(left.args, self.right.args, self.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
+        return is_proper_subtype(left.upper_bound, self.right)
+
+    def visit_callable_type(self, left: CallableType) -> bool:
+        # TODO: Implement this properly
+        return is_subtype(left, self.right)
+
+    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]
+                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:
+        # TODO: Does it make sense to support TypedDict here?
+        return False
+
+    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:
+        right = self.right
+        if isinstance(right, TypeType):
+            return is_proper_subtype(left.item, right.item)
+        if isinstance(right, CallableType):
+            # This is unsound, we don't check the __init__ signature.
+            return right.is_type_obj() and is_proper_subtype(left.item, right.ret_type)
+        if isinstance(right, Instance):
+            if right.type.fullname() in ('builtins.type', 'builtins.object'):
+                return True
+            item = left.item
+            return isinstance(item, Instance) and is_proper_subtype(item, right.type.metaclass_type)
+        return False
+
+
 def is_more_precise(t: Type, s: Type) -> bool:
     """Check if t is a more precise type than s.
 
diff --git a/mypy/types.py b/mypy/types.py
index 9621c0f859fa..bc9f76d341aa 100644
--- a/mypy/types.py
+++ b/mypy/types.py
@@ -995,11 +995,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):
@@ -1008,9 +1004,7 @@ def make_simplified_union(items: List[Type], line: int = -1, column: int = -1) -
             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))):
+                    and is_proper_subtype(tj, ti)):
                     removed.add(j)
                     cbt = cbt or tj.can_be_true
                     cbf = cbf or tj.can_be_false
diff --git a/test-data/unit/check-classes.test b/test-data/unit/check-classes.test
index d841394196a5..1ce01d22c220 100644
--- a/test-data/unit/check-classes.test
+++ b/test-data/unit/check-classes.test
@@ -2388,9 +2388,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 e1efd0a3f559..5e960bca17b2 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..3d6889d5c05f 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
diff --git a/test-data/unit/check-optional.test b/test-data/unit/check-optional.test
index d5f2c06aebf4..48d7e3389743 100644
--- a/test-data/unit/check-optional.test
+++ b/test-data/unit/check-optional.test
@@ -547,9 +547,31 @@ 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
+class C(Any):
+    pass
+x = None  # type: Optional[C]
+x.foo()  # E: Some element of union has no attribute "foo"
+
+[case testUnionSimplificationWithStrictOptional]
+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
+
+# Test both orders
+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]'
+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]'
diff --git a/test-data/unit/check-statements.test b/test-data/unit/check-statements.test
index eb0d7e194aaa..31d82038ed63 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-unions.test b/test-data/unit/check-unions.test
index c51cb06a0002..a713e87899ad 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]
 
@@ -183,9 +184,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'
@@ -217,3 +217,66 @@ 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)

From dc62a998f20d38351c1c806f09c2a13b32f09ba7 Mon Sep 17 00:00:00 2001
From: Jukka Lehtosalo <jukka.lehtosalo@iki.fi>
Date: Tue, 14 Mar 2017 13:48:48 +0000
Subject: [PATCH 02/17] Fix #2978.

---
 mypy/checkexpr.py                  |  3 ++-
 mypy/join.py                       |  6 +++---
 mypy/subtypes.py                   | 21 +++++++++++++++++----
 test-data/unit/check-optional.test | 14 ++++++++++++++
 4 files changed, 36 insertions(+), 8 deletions(-)

diff --git a/mypy/checkexpr.py b/mypy/checkexpr.py
index cd69f7336d1d..ca2857c98c96 100644
--- a/mypy/checkexpr.py
+++ b/mypy/checkexpr.py
@@ -2213,7 +2213,8 @@ 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:
-                return narrow_declared_type(known_type, restriction)
+                ans = narrow_declared_type(known_type, restriction)
+                return ans
         return known_type
 
 
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/subtypes.py b/mypy/subtypes.py
index 43334087211f..9ced783d0896 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
@@ -496,13 +497,22 @@ 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
@@ -624,6 +634,9 @@ def visit_tuple_type(self, left: TupleType) -> bool:
                 if not right.args:
                     return False
                 iter_type = right.args[0]
+                if is_named_instance(right, 'builtins.tuple') and isinstance(iter_type, AnyType):
+                    # Special case plain 'tuple' which is needed for isinstance(x, tuple).
+                    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):
diff --git a/test-data/unit/check-optional.test b/test-data/unit/check-optional.test
index 48d7e3389743..51c85168241c 100644
--- a/test-data/unit/check-optional.test
+++ b/test-data/unit/check-optional.test
@@ -575,3 +575,17 @@ 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 testIsinstanceAndOptionalAndAnyBase]
+from typing import Any, Optional
+
+class A(Any): 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]

From 07d64f5c9cb98e89754bd5e5104e76fd71c280f3 Mon Sep 17 00:00:00 2001
From: Jukka Lehtosalo <jukka.lehtosalo@iki.fi>
Date: Tue, 14 Mar 2017 13:53:21 +0000
Subject: [PATCH 03/17] Add test case

Fix #1914.
---
 test-data/unit/check-unions.test | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/test-data/unit/check-unions.test b/test-data/unit/check-unions.test
index a713e87899ad..bd4683a6a670 100644
--- a/test-data/unit/check-unions.test
+++ b/test-data/unit/check-unions.test
@@ -280,3 +280,18 @@ from typing import Union
 class A: pass
 def f(x: Union[int, str, A]):
     x + object() # E: Unsupported left operand type for + (some 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]

From 0beffeef1f258366da3ce3e560fd194334c62934 Mon Sep 17 00:00:00 2001
From: Jukka Lehtosalo <jukka.lehtosalo@iki.fi>
Date: Wed, 15 Mar 2017 16:19:09 +0000
Subject: [PATCH 04/17] Fix test failures

---
 mypy/meet.py                         |  5 +++--
 mypy/subtypes.py                     | 32 ++--------------------------
 mypy/types.py                        |  4 ++--
 test-data/unit/check-isinstance.test | 13 +++++++++++
 4 files changed, 20 insertions(+), 34 deletions(-)

diff --git a/mypy/meet.py b/mypy/meet.py
index 45f6c28d1e96..48c7b63d4204 100644
--- a/mypy/meet.py
+++ b/mypy/meet.py
@@ -27,7 +27,6 @@ def meet_types(s: Type, t: Type) -> Type:
 
 def narrow_declared_type(declared: Type, narrowed: Type) -> Type:
     """Return the declared type narrowed down to another type."""
-    # TODO: What are the reasons for not just using meet_types()?
     if declared == narrowed:
         return declared
     if isinstance(declared, UnionType):
@@ -43,7 +42,9 @@ def narrow_declared_type(declared: Type, narrowed: Type) -> Type:
                                                 for x in narrowed.items])
     elif isinstance(narrowed, AnyType):
         return narrowed
-    return meet_types(declared, 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:
diff --git a/mypy/subtypes.py b/mypy/subtypes.py
index 9ced783d0896..e4b293911ecd 100644
--- a/mypy/subtypes.py
+++ b/mypy/subtypes.py
@@ -529,35 +529,6 @@ def is_proper_subtype(left: Type, right: Type) -> bool:
                     for item in right.items])
     return left.accept(ProperSubtypeVisitor(right))
 
-    # 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(t, Instance):
-        if isinstance(s, Instance):
-            if not t.type.has_base(s.type.fullname()):
-                return False
-
-            def check_argument(left: Type, right: Type, variance: int) -> bool:
-                if variance == COVARIANT:
-                    return is_proper_subtype(left, right)
-                elif variance == CONTRAVARIANT:
-                    return is_proper_subtype(right, left)
-                else:
-                    return sametypes.is_same_type(left, right)
-
-            # Map left type to corresponding right instances.
-            t = map_instance_to_supertype(t, s.type)
-
-            return all(check_argument(ta, ra, tvar.variance) for ta, ra, tvar in
-                       zip(t.args, s.args, s.type.defn.type_vars))
-        return False
-    else:
-        return sametypes.is_same_type(t, s)
-
 
 class ProperSubtypeVisitor(TypeVisitor[bool]):
     def __init__(self, right: Type) -> None:
@@ -674,7 +645,8 @@ def visit_type_type(self, left: TypeType) -> bool:
             if right.type.fullname() in ('builtins.type', 'builtins.object'):
                 return True
             item = left.item
-            return isinstance(item, Instance) and is_proper_subtype(item, right.type.metaclass_type)
+            return isinstance(item, Instance) and is_proper_subtype(item,
+                                                                    right.type.metaclass_type)
         return False
 
 
diff --git a/mypy/types.py b/mypy/types.py
index bc9f76d341aa..91012cabd9e1 100644
--- a/mypy/types.py
+++ b/mypy/types.py
@@ -1003,8 +1003,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_proper_subtype(tj, ti)):
+                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
diff --git a/test-data/unit/check-isinstance.test b/test-data/unit/check-isinstance.test
index 3d6889d5c05f..55835fe00162 100644
--- a/test-data/unit/check-isinstance.test
+++ b/test-data/unit/check-isinstance.test
@@ -1413,3 +1413,16 @@ 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'
+[builtins fixtures/isinstance.pyi]

From e3ff2c7864b63cfe6f415b7396ca535d8813cb75 Mon Sep 17 00:00:00 2001
From: Jukka Lehtosalo <jukka.lehtosalo@iki.fi>
Date: Sat, 18 Mar 2017 13:58:17 -0700
Subject: [PATCH 05/17] Fix meet of a broken named tuple and a good named tuple

---
 mypy/meet.py                         |  4 ++++
 mypy/test/testtypes.py               |  2 +-
 test-data/unit/check-namedtuple.test | 22 ++++++++++++++++++++++
 3 files changed, 27 insertions(+), 1 deletion(-)

diff --git a/mypy/meet.py b/mypy/meet.py
index 48c7b63d4204..19e3299f21fb 100644
--- a/mypy/meet.py
+++ b/mypy/meet.py
@@ -253,6 +253,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/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/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]'

From 4cb86738d814b01b75666f902a08eaa443f361f8 Mon Sep 17 00:00:00 2001
From: Jukka Lehtosalo <jukka.lehtosalo@iki.fi>
Date: Sat, 18 Mar 2017 17:25:28 -0700
Subject: [PATCH 06/17] Fix erasing union types

---
 mypy/erasetype.py | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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)

From fc57a76ec1c3a8b50e100c429dc6ba9c1c9e07bb Mon Sep 17 00:00:00 2001
From: Jukka Lehtosalo <jukka.lehtosalo@iki.fi>
Date: Sun, 19 Mar 2017 13:44:39 -0700
Subject: [PATCH 07/17] Remove references to Void

---
 mypy/subtypes.py | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

diff --git a/mypy/subtypes.py b/mypy/subtypes.py
index e4b293911ecd..d81eb195b587 100644
--- a/mypy/subtypes.py
+++ b/mypy/subtypes.py
@@ -546,18 +546,14 @@ def visit_type_list(self, left: TypeList) -> bool:
     def visit_any(self, left: AnyType) -> bool:
         return isinstance(self.right, AnyType)
 
-    def visit_void(self, left: Void) -> bool:
-        return True
-
     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'))
-        else:
-            return not isinstance(self.right, Void)
+        return True
 
     def visit_uninhabited_type(self, left: UninhabitedType) -> bool:
-        return not isinstance(self.right, Void)
+        return True
 
     def visit_erased_type(self, left: ErasedType) -> bool:
         return True

From 9cf911466a6016c66de080672b03fb0f346e97b1 Mon Sep 17 00:00:00 2001
From: Jukka Lehtosalo <jukka.lehtosalo@iki.fi>
Date: Mon, 20 Mar 2017 10:10:29 -0700
Subject: [PATCH 08/17] Proper subtype checks use type promotions

---
 mypy/subtypes.py                       |  5 +++++
 test-data/unit/check-unions.test       | 12 ++++++++++++
 test-data/unit/fixtures/primitives.pyi |  2 +-
 3 files changed, 18 insertions(+), 1 deletion(-)

diff --git a/mypy/subtypes.py b/mypy/subtypes.py
index d81eb195b587..3b2a618bdc55 100644
--- a/mypy/subtypes.py
+++ b/mypy/subtypes.py
@@ -563,6 +563,10 @@ def visit_deleted_type(self, left: DeletedType) -> bool:
 
     def visit_instance(self, left: Instance) -> bool:
         if isinstance(self.right, Instance):
+            for base in left.type.mro:
+                if base._promote and is_proper_subtype(base._promote, self.right):
+                    return True
+
             if not left.type.has_base(self.right.type.fullname()):
                 return False
 
@@ -579,6 +583,7 @@ def check_argument(leftarg: Type, rightarg: Type, variance: int) -> bool:
 
             return all(check_argument(ta, ra, tvar.variance) for ta, ra, tvar in
                        zip(left.args, self.right.args, self.right.type.defn.type_vars))
+        # TODO: TypeType
         return False
 
     def visit_type_var(self, left: TypeVarType) -> bool:
diff --git a/test-data/unit/check-unions.test b/test-data/unit/check-unions.test
index bd4683a6a670..bfd408d65849 100644
--- a/test-data/unit/check-unions.test
+++ b/test-data/unit/check-unions.test
@@ -295,3 +295,15 @@ def foo(a: Union[A, B, C]):
         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]
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

From d406157f649aad993e256941cb3119b61bf52c28 Mon Sep 17 00:00:00 2001
From: Jukka Lehtosalo <jukka.lehtosalo@iki.fi>
Date: Mon, 20 Mar 2017 10:51:43 -0700
Subject: [PATCH 09/17] Don't call union simplification during semantic
 analysis

We generally don't have fully constructed TypeInfos so
we can't do proper union simplification. Just implement
simple-minded simplifaction that deals with the cases we
care about.
---
 mypy/typeanal.py | 21 +++++++++++++++++++--
 mypy/types.py    | 17 ++++++++++++++++-
 2 files changed, 35 insertions(+), 3 deletions(-)

diff --git a/mypy/typeanal.py b/mypy/typeanal.py
index e33daa2eed3c..b2c3de8b7770 100644
--- a/mypy/typeanal.py
+++ b/mypy/typeanal.py
@@ -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,20 @@ 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) and any(isinstance(item, NoneTyp)
+                                        for item in t.items):
+        return t
+    return UnionType([t, NoneTyp()], t.line, t.column)
diff --git a/mypy/types.py b/mypy/types.py
index 91012cabd9e1..b0d196c01b71 100644
--- a/mypy/types.py
+++ b/mypy/types.py
@@ -986,6 +986,21 @@ 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.
+        """
         while any(isinstance(typ, UnionType) for typ in items):
             all_items = []  # type: List[Type]
             for typ in items:
@@ -1708,7 +1723,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)

From d745a50e7283eaadbc6e91e1e6939efee8769c3d Mon Sep 17 00:00:00 2001
From: Jukka Lehtosalo <jukka.lehtosalo@iki.fi>
Date: Mon, 20 Mar 2017 14:25:40 -0700
Subject: [PATCH 10/17] Add union simplification test cases

---
 mypy/subtypes.py                 |  1 -
 test-data/unit/check-unions.test | 54 ++++++++++++++++++++++++++++++++
 typeshed                         |  2 +-
 3 files changed, 55 insertions(+), 2 deletions(-)

diff --git a/mypy/subtypes.py b/mypy/subtypes.py
index 3b2a618bdc55..1d93a805e8d0 100644
--- a/mypy/subtypes.py
+++ b/mypy/subtypes.py
@@ -583,7 +583,6 @@ def check_argument(leftarg: Type, rightarg: Type, variance: int) -> bool:
 
             return all(check_argument(ta, ra, tvar.variance) for ta, ra, tvar in
                        zip(left.args, self.right.args, self.right.type.defn.type_vars))
-        # TODO: TypeType
         return False
 
     def visit_type_var(self, left: TypeVarType) -> bool:
diff --git a/test-data/unit/check-unions.test b/test-data/unit/check-unions.test
index bfd408d65849..ccdfe8548633 100644
--- a/test-data/unit/check-unions.test
+++ b/test-data/unit/check-unions.test
@@ -307,3 +307,57 @@ 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]
+
+# 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]'
diff --git a/typeshed b/typeshed
index bd5b33f3b18f..48920fea7ee6 160000
--- a/typeshed
+++ b/typeshed
@@ -1 +1 @@
-Subproject commit bd5b33f3b18fc8811ad2403d35f21ad6aae94b62
+Subproject commit 48920fea7ee6c1d413fba12fe709c652da065393

From a638e72c81bd9c0359a8d4bf1d622e49b16b1281 Mon Sep 17 00:00:00 2001
From: Jukka Lehtosalo <jukka.lehtosalo@iki.fi>
Date: Fri, 24 Mar 2017 16:34:33 +0000
Subject: [PATCH 11/17] Address review feedback

---
 mypy/subtypes.py                     | 85 ++++++++++++++++++++--------
 test-data/unit/check-isinstance.test | 14 ++++-
 test-data/unit/check-optional.test   | 28 +++------
 test-data/unit/check-tuples.test     |  2 +-
 test-data/unit/check-unions.test     | 58 ++++++++++++++++++-
 5 files changed, 140 insertions(+), 47 deletions(-)

diff --git a/mypy/subtypes.py b/mypy/subtypes.py
index 1d93a805e8d0..b45df078e3ce 100644
--- a/mypy/subtypes.py
+++ b/mypy/subtypes.py
@@ -281,9 +281,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
@@ -310,7 +316,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:
@@ -399,7 +405,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
@@ -415,11 +421,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
 
@@ -450,7 +456,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:
@@ -461,8 +468,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
@@ -519,10 +530,10 @@ def restrict_subtype_away(t: Type, s: Type) -> Type:
 
 
 def is_proper_subtype(left: Type, right: Type) -> bool:
-    """Check if t is a proper subtype of s?
+    """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.
     """
     if isinstance(right, UnionType) and not isinstance(left, UnionType):
         return any([is_proper_subtype(left, item)
@@ -535,9 +546,13 @@ def __init__(self, right: Type) -> None:
         self.right = right
 
     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:
@@ -556,18 +571,21 @@ 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:
-        if isinstance(self.right, Instance):
+        right = self.right
+        if isinstance(right, Instance):
             for base in left.type.mro:
-                if base._promote and is_proper_subtype(base._promote, self.right):
+                if base._promote and is_proper_subtype(base._promote, right):
                     return True
 
-            if not left.type.has_base(self.right.type.fullname()):
+            if not left.type.has_base(right.type.fullname()):
                 return False
 
             def check_argument(leftarg: Type, rightarg: Type, variance: int) -> bool:
@@ -579,20 +597,34 @@ def check_argument(leftarg: Type, rightarg: Type, variance: int) -> bool:
                     return sametypes.is_same_type(leftarg, rightarg)
 
             # Map left type to corresponding right instances.
-            left = map_instance_to_supertype(left, self.right.type)
+            left = map_instance_to_supertype(left, right.type)
 
             return all(check_argument(ta, ra, tvar.variance) for ta, ra, tvar in
-                       zip(left.args, self.right.args, self.right.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:
-        # TODO: Implement this properly
-        return is_subtype(left, self.right)
+        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
@@ -606,7 +638,8 @@ def visit_tuple_type(self, left: TupleType) -> bool:
                     return False
                 iter_type = right.args[0]
                 if is_named_instance(right, 'builtins.tuple') and isinstance(iter_type, AnyType):
-                    # Special case plain 'tuple' which is needed for isinstance(x, tuple).
+                    # 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)
@@ -620,8 +653,13 @@ def visit_tuple_type(self, left: TupleType) -> bool:
         return False
 
     def visit_typeddict_type(self, left: TypedDictType) -> bool:
-        # TODO: Does it make sense to support TypedDict here?
-        return False
+        right = self.right
+        if isinstance(right, TypedDictType):
+            for name, typ in left.items():
+                if name not in right or not is_same_type(typ, right.items[name]):
+                    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?
@@ -635,18 +673,17 @@ def visit_partial_type(self, left: PartialType) -> bool:
         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 unsound, we don't check the __init__ signature.
+            # 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() in ('builtins.type', 'builtins.object'):
                 return True
-            item = left.item
-            return isinstance(item, Instance) and is_proper_subtype(item,
-                                                                    right.type.metaclass_type)
         return False
 
 
diff --git a/test-data/unit/check-isinstance.test b/test-data/unit/check-isinstance.test
index 55835fe00162..4eeff6e83959 100644
--- a/test-data/unit/check-isinstance.test
+++ b/test-data/unit/check-isinstance.test
@@ -911,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:
@@ -1276,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]
@@ -1306,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
@@ -1323,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'
@@ -1330,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]
@@ -1371,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]
 
 
@@ -1383,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]
 
@@ -1425,4 +1434,7 @@ 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]
diff --git a/test-data/unit/check-optional.test b/test-data/unit/check-optional.test
index 51c85168241c..91206368adbc 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]
@@ -535,9 +536,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
@@ -555,31 +557,17 @@ reveal_type(u(None, 1))  # E: Revealed type is 'Union[builtins.int*, builtins.No
 
 [case testOptionalAndAnyBaseClass]
 from typing import Any, Optional
-class C(Any):
+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 testUnionSimplificationWithStrictOptional]
-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
-
-# Test both orders
-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]'
-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 testIsinstanceAndOptionalAndAnyBase]
 from typing import Any, Optional
 
-class A(Any): pass
+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]'
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-unions.test b/test-data/unit/check-unions.test
index ccdfe8548633..529026ae9f6b 100644
--- a/test-data/unit/check-unions.test
+++ b/test-data/unit/check-unions.test
@@ -279,7 +279,8 @@ reveal_type(u('', 1, 1))  # E: Revealed type is 'Union[builtins.int*, builtins.s
 from typing import Union
 class A: pass
 def f(x: Union[int, str, A]):
-    x + object() # E: Unsupported left operand type for + (some union)
+    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
@@ -361,3 +362,58 @@ 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]'
+
+[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]'

From ca511d8632e8652336109e66056e6b004758e982 Mon Sep 17 00:00:00 2001
From: Jukka Lehtosalo <jukka.lehtosalo@iki.fi>
Date: Fri, 24 Mar 2017 18:10:32 +0000
Subject: [PATCH 12/17] Fix test case failures

---
 mypy/checker.py                  | 77 ++++++++++++++++----------------
 mypy/subtypes.py                 |  9 ++--
 mypy/types.py                    | 14 ++++++
 test-data/unit/check-unions.test |  9 ++++
 4 files changed, 67 insertions(+), 42 deletions(-)

diff --git a/mypy/checker.py b/mypy/checker.py
index 0afdbe0779de..5d37ba3beda7 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
@@ -768,44 +768,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/subtypes.py b/mypy/subtypes.py
index b45df078e3ce..1ba86206bc16 100644
--- a/mypy/subtypes.py
+++ b/mypy/subtypes.py
@@ -16,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
 
@@ -373,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
@@ -396,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
 
@@ -655,8 +656,8 @@ def visit_tuple_type(self, left: TupleType) -> bool:
     def visit_typeddict_type(self, left: TypedDictType) -> bool:
         right = self.right
         if isinstance(right, TypedDictType):
-            for name, typ in left.items():
-                if name not in right or not is_same_type(typ, right.items[name]):
+            for name, typ in left.items.items():
+                if name not in right.items or not is_same_type(typ, right.items[name]):
                     return False
             return True
         return is_proper_subtype(left.fallback, right)
diff --git a/mypy/types.py b/mypy/types.py
index b0d196c01b71..0f12bb3afbf7 100644
--- a/mypy/types.py
+++ b/mypy/types.py
@@ -1751,6 +1751,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-unions.test b/test-data/unit/check-unions.test
index 529026ae9f6b..9a6b52e8e412 100644
--- a/test-data/unit/check-unions.test
+++ b/test-data/unit/check-unions.test
@@ -417,3 +417,12 @@ 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: ...

From 807924cb7d2a0a0dc14a2f75d23cde9617a2fa32 Mon Sep 17 00:00:00 2001
From: Jukka Lehtosalo <jukka.lehtosalo@iki.fi>
Date: Fri, 24 Mar 2017 18:16:14 +0000
Subject: [PATCH 13/17] Flatten Optional[Union[...]] types

---
 mypy/typeanal.py                   | 9 +++++----
 test-data/unit/check-optional.test | 8 ++++++++
 2 files changed, 13 insertions(+), 4 deletions(-)

diff --git a/mypy/typeanal.py b/mypy/typeanal.py
index b2c3de8b7770..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,
@@ -570,7 +570,8 @@ def make_optional_type(t: Type) -> Type:
         return t
     if isinstance(t, NoneTyp):
         return t
-    if isinstance(t, UnionType) and any(isinstance(item, NoneTyp)
-                                        for item in t.items):
-        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/test-data/unit/check-optional.test b/test-data/unit/check-optional.test
index 91206368adbc..5e400b95df75 100644
--- a/test-data/unit/check-optional.test
+++ b/test-data/unit/check-optional.test
@@ -577,3 +577,11 @@ def f(a: Optional[A]):
         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]'

From ef46cfadad687ccd7ffc78f6324fe61263c98924 Mon Sep 17 00:00:00 2001
From: Jukka Lehtosalo <jukka.lehtosalo@iki.fi>
Date: Mon, 27 Mar 2017 11:53:21 +0100
Subject: [PATCH 14/17] Add TODO comment about make_simplified_union

---
 mypy/types.py | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/mypy/types.py b/mypy/types.py
index 0f12bb3afbf7..de2f3773626c 100644
--- a/mypy/types.py
+++ b/mypy/types.py
@@ -1001,6 +1001,8 @@ def make_simplified_union(items: List[Type], line: int = -1, column: int = -1) -
         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:

From 6cd09f1f0873c3d40da15e4cabbc534fbbf072db Mon Sep 17 00:00:00 2001
From: Jukka Lehtosalo <jukka.lehtosalo@iki.fi>
Date: Mon, 27 Mar 2017 11:54:55 +0100
Subject: [PATCH 15/17] Add test case

---
 test-data/unit/check-isinstance.test | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/test-data/unit/check-isinstance.test b/test-data/unit/check-isinstance.test
index 4eeff6e83959..1490dc0bb089 100644
--- a/test-data/unit/check-isinstance.test
+++ b/test-data/unit/check-isinstance.test
@@ -1438,3 +1438,13 @@ def f(x: T) -> None:
         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]

From 39f94a17bcfe4d08667c9fc3a4707486e8dafe52 Mon Sep 17 00:00:00 2001
From: Jukka Lehtosalo <jukka.lehtosalo@iki.fi>
Date: Mon, 27 Mar 2017 11:55:14 +0100
Subject: [PATCH 16/17] Partially address comments about type object types

---
 mypy/subtypes.py                 | 8 +++++++-
 test-data/unit/check-unions.test | 7 +++++++
 2 files changed, 14 insertions(+), 1 deletion(-)

diff --git a/mypy/subtypes.py b/mypy/subtypes.py
index 1ba86206bc16..92818c342644 100644
--- a/mypy/subtypes.py
+++ b/mypy/subtypes.py
@@ -683,7 +683,13 @@ def visit_type_type(self, left: TypeType) -> bool:
             # 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() in ('builtins.type', 'builtins.object'):
+            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
 
diff --git a/test-data/unit/check-unions.test b/test-data/unit/check-unions.test
index 9a6b52e8e412..4ce546c679d8 100644
--- a/test-data/unit/check-unions.test
+++ b/test-data/unit/check-unions.test
@@ -346,6 +346,7 @@ 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*'
@@ -362,6 +363,12 @@ 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

From 0826cc3c4ab708771716e1170376f3f3531cbb84 Mon Sep 17 00:00:00 2001
From: Jukka Lehtosalo <jukka.lehtosalo@iki.fi>
Date: Mon, 27 Mar 2017 12:29:26 +0100
Subject: [PATCH 17/17] Fixes to TypedDict proper subtype checks + add tests

---
 mypy/subtypes.py                    |  5 ++-
 test-data/unit/check-typeddict.test | 57 +++++++++++++++++++++++++++++
 2 files changed, 61 insertions(+), 1 deletion(-)

diff --git a/mypy/subtypes.py b/mypy/subtypes.py
index 92818c342644..b96618da28eb 100644
--- a/mypy/subtypes.py
+++ b/mypy/subtypes.py
@@ -657,7 +657,10 @@ def visit_typeddict_type(self, left: TypedDictType) -> bool:
         right = self.right
         if isinstance(right, TypedDictType):
             for name, typ in left.items.items():
-                if name not in right.items or not is_same_type(typ, right.items[name]):
+                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)
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]