From 9c70f3dec46190e41256562d245b8199e72d0cfe Mon Sep 17 00:00:00 2001
From: Reid Barton <rwbarton@gmail.com>
Date: Sun, 26 Jun 2016 08:32:02 -0400
Subject: [PATCH 01/13] Replace the binder's breaking_out by an 'unreachable'
 property of Frame

Also add some comments to the binder.
---
 mypy/binder.py    | 87 ++++++++++++++++++++++++++++++++++-------------
 mypy/checker.py   | 86 ++++++++++++++++++++++++----------------------
 mypy/checkexpr.py |  8 ++---
 3 files changed, 113 insertions(+), 68 deletions(-)

diff --git a/mypy/binder.py b/mypy/binder.py
index bc633e57e2c0..3c556487bcf8 100644
--- a/mypy/binder.py
+++ b/mypy/binder.py
@@ -10,7 +10,19 @@
 
 
 class Frame(Dict[Any, Type]):
-    pass
+    """A Frame represents a specific point in the execution of a program.
+    It carries information about the current types of expressions at
+    that point, arising either from assignments to those expressions
+    or the result of isinstance checks. It also records whether it is
+    possible to reach that point at all.
+
+    This information is not copied into a new Frame when it is pushed
+    onto the stack, so a given Frame only has information about types
+    that were assigned in that frame.
+    """
+
+    def __init__(self) -> None:
+        self.unreachable = False
 
 
 class Key(AnyType):
@@ -39,13 +51,19 @@ class A:
     """
 
     def __init__(self) -> None:
-        # The set of frames currently used.  These map
+        # The stack of frames currently used.  These map
         # expr.literal_hash -- literals like 'foo.bar' --
-        # to types.
+        # to types. The last element of this list is the
+        # top-most, current frame. Each earlier element
+        # records the state as of when that frame was last
+        # on top of the stack.
         self.frames = [Frame()]
 
         # For frames higher in the stack, we record the set of
-        # Frames that can escape there
+        # Frames that can escape there, either by falling off
+        # the end of the frame or by a loop control construct
+        # or raised exception. The last element of self.frames
+        # has no corresponding element in this list.
         self.options_on_return = []  # type: List[List[Frame]]
 
         # Maps expr.literal_hash] to get_declaration(expr)
@@ -55,16 +73,8 @@ def __init__(self) -> None:
         # Whenever a new key (e.g. x.a.b) is added, we update this
         self.dependencies = {}  # type: Dict[Key, Set[Key]]
 
-        # breaking_out is set to True on return/break/continue/raise
-        # It is cleared on pop_frame() and placed in last_pop_breaking_out
-        # Lines of code after breaking_out = True are unreachable and not
-        # typechecked.
-        self.breaking_out = False
-
         # Whether the last pop changed the newly top frame on exit
         self.last_pop_changed = False
-        # Whether the last pop was necessarily breaking out, and couldn't fall through
-        self.last_pop_breaking_out = False
 
         self.try_frames = set()  # type: Set[int]
         self.loop_frames = []  # type: List[int]
@@ -105,9 +115,15 @@ def push(self, node: Node, typ: Type) -> None:
             self._add_dependencies(key)
         self._push(key, typ)
 
+    def unreachable(self) -> bool:
+        self.frames[-1].unreachable = True
+
     def get(self, expr: Union[Expression, Var]) -> Type:
         return self._get(expr.literal_hash)
 
+    def is_unreachable(self) -> bool:
+        return self.frames[-1].unreachable
+
     def cleanse(self, expr: Expression) -> None:
         """Remove all references to a Node from the binder."""
         self._cleanse_key(expr.literal_hash)
@@ -126,6 +142,7 @@ def update_from_options(self, frames: List[Frame]) -> bool:
         options are the same.
         """
 
+        frames = [f for f in frames if not f.unreachable]
         changed = False
         keys = set(key for f in frames for key in f)
 
@@ -133,6 +150,9 @@ def update_from_options(self, frames: List[Frame]) -> bool:
             current_value = self._get(key)
             resulting_values = [f.get(key, current_value) for f in frames]
             if any(x is None for x in resulting_values):
+                # We didn't know anything about key before
+                # (current_value must be None), and we still don't
+                # know anything about key in at least one possible frame.
                 continue
 
             if isinstance(self.declarations.get(key), AnyType):
@@ -147,21 +167,26 @@ def update_from_options(self, frames: List[Frame]) -> bool:
                 self._push(key, type)
                 changed = True
 
+        self.frames[-1].unreachable = not frames
+
         return changed
 
-    def pop_frame(self, fall_through: int = 0) -> Frame:
+    def pop_frame(self, can_skip: bool, fall_through: int) -> Frame:
         """Pop a frame and return it.
 
         See frame_context() for documentation of fall_through.
         """
-        if fall_through and not self.breaking_out:
+
+        if fall_through > 0:
             self.allow_jump(-fall_through)
 
         result = self.frames.pop()
         options = self.options_on_return.pop()
 
+        if can_skip:
+            options.insert(0, self.frames[-1])
+
         self.last_pop_changed = self.update_from_options(options)
-        self.last_pop_breaking_out = self.breaking_out
 
         return result
 
@@ -239,6 +264,8 @@ def allow_jump(self, index: int) -> None:
         frame = Frame()
         for f in self.frames[index + 1:]:
             frame.update(f)
+            if f.unreachable:
+                frame.unreachable = True
         self.options_on_return[index].append(frame)
 
     def push_loop_frame(self) -> None:
@@ -248,16 +275,30 @@ def pop_loop_frame(self) -> None:
         self.loop_frames.pop()
 
     @contextmanager
-    def frame_context(self, fall_through: int = 0) -> Iterator[Frame]:
+    def frame_context(self, *, can_skip: bool, fall_through: int = 1) -> Iterator[Frame]:
         """Return a context manager that pushes/pops frames on enter/exit.
 
-        If fall_through > 0, then it will allow the frame to escape to
-        its ancestor `fall_through` levels higher.
+        If can_skip is True, control flow is allowed to bypass the
+        newly-created frame.
 
-        A simple 'with binder.frame_context(): pass' will change the
-        last_pop_* flags but nothing else.
+        If fall_through > 0, then it will allow control flow that
+        falls off the end of the frame to escape to its ancestor
+        `fall_through` levels higher. Otherwise control flow ends
+        at the end of the frame.
+
+        After the context manager exits, self.last_pop_changed indicates
+        whether any types changed in the newly-topmost frame as a result
+        of popping this frame.
+        """
+        assert len(self.frames) > 1
+        yield self.push_frame()
+        self.pop_frame(can_skip, fall_through)
+
+    @contextmanager
+    def top_frame_context(self) -> Iterator[Frame]:
+        """A variant of frame_context for use at the top level of
+        a namespace (module, function, or class).
         """
-        was_breaking_out = self.breaking_out
+        assert len(self.frames) == 1
         yield self.push_frame()
-        self.pop_frame(fall_through)
-        self.breaking_out = was_breaking_out
+        self.pop_frame(True, 0)
diff --git a/mypy/checker.py b/mypy/checker.py
index 8394e1bc9662..72a164691c62 100644
--- a/mypy/checker.py
+++ b/mypy/checker.py
@@ -161,8 +161,9 @@ def visit_file(self, file_node: MypyFile, path: str, options: Options) -> None:
                                                 for pattern
                                                 in self.options.strict_optional_whitelist)
 
-        for d in file_node.defs:
-            self.accept(d)
+        with self.binder.top_frame_context():
+            for d in file_node.defs:
+                self.accept(d)
 
         self.leave_partial_types()
 
@@ -232,12 +233,10 @@ def accept_loop(self, body: Union[IfStmt, Block], else_body: Block = None) -> Ty
         Then check the else_body.
         """
         # The outer frame accumulates the results of all iterations
-        with self.binder.frame_context(1) as outer_frame:
+        with self.binder.frame_context(can_skip=False):
             self.binder.push_loop_frame()
             while True:
-                with self.binder.frame_context(1):
-                    # We may skip each iteration
-                    self.binder.options_on_return[-1].append(outer_frame)
+                with self.binder.frame_context(can_skip=True):
                     self.accept(body)
                 if not self.binder.last_pop_changed:
                     break
@@ -505,7 +504,7 @@ def check_func_def(self, defn: FuncItem, typ: CallableType, name: str) -> None:
         for item, typ in self.expand_typevars(defn, typ):
             old_binder = self.binder
             self.binder = ConditionalTypeBinder()
-            with self.binder.frame_context():
+            with self.binder.top_frame_context():
                 defn.expanded.append(item)
 
                 # We may be checking a function definition or an anonymous
@@ -605,7 +604,7 @@ def is_implicit_any(t: Type) -> bool:
                         self.accept(init)
 
             # Type check body in a new scope.
-            with self.binder.frame_context():
+            with self.binder.top_frame_context():
                 self.accept(item.body)
 
             self.return_types.pop()
@@ -918,7 +917,7 @@ def visit_class_def(self, defn: ClassDef) -> Type:
         self.enter_partial_types()
         old_binder = self.binder
         self.binder = ConditionalTypeBinder()
-        with self.binder.frame_context():
+        with self.binder.top_frame_context():
             self.accept(defn.defs)
         self.binder = old_binder
         if not defn.has_incompatible_baseclass:
@@ -1016,9 +1015,9 @@ def visit_block(self, b: Block) -> Type:
         if b.is_unreachable:
             return None
         for s in b.body:
-            self.accept(s)
-            if self.binder.breaking_out:
+            if self.binder.is_unreachable():
                 break
+            self.accept(s)
 
     def visit_assignment_stmt(self, s: AssignmentStmt) -> Type:
         """Type check an assignment statement.
@@ -1455,7 +1454,10 @@ def visit_expression_stmt(self, s: ExpressionStmt) -> Type:
 
     def visit_return_stmt(self, s: ReturnStmt) -> Type:
         """Type check a return statement."""
-        self.binder.breaking_out = True
+        self.check_return_stmt(s)
+        self.binder.unreachable()
+
+    def check_return_stmt(self, s: ReturnStmt) -> None:
         if self.is_within_function():
             defn = self.function_stack[-1]
             if defn.is_generator:
@@ -1522,9 +1524,9 @@ def count_nested_types(self, typ: Instance, check_type: str) -> int:
 
     def visit_if_stmt(self, s: IfStmt) -> Type:
         """Type check an if statement."""
-        breaking_out = True
         # This frame records the knowledge from previous if/elif clauses not being taken.
-        with self.binder.frame_context():
+        # Fall-through to the original frame is handled explicitly in each block.
+        with self.binder.frame_context(can_skip=False, fall_through=0):
             for e, b in zip(s.expr, s.body):
                 t = self.accept(e)
                 self.check_usable_type(t, e)
@@ -1535,13 +1537,12 @@ def visit_if_stmt(self, s: IfStmt) -> Type:
                     pass
                 else:
                     # Only type check body if the if condition can be true.
-                    with self.binder.frame_context(2):
+                    with self.binder.frame_context(can_skip=True, fall_through=2):
                         if if_map:
                             for var, type in if_map.items():
                                 self.binder.push(var, type)
 
                         self.accept(b)
-                    breaking_out = breaking_out and self.binder.last_pop_breaking_out
 
                     if else_map:
                         for var, type in else_map.items():
@@ -1554,12 +1555,9 @@ def visit_if_stmt(self, s: IfStmt) -> Type:
                     # print("Warning: isinstance always true")
                     break
             else:  # Didn't break => can't prove one of the conditions is always true
-                with self.binder.frame_context(2):
+                with self.binder.frame_context(can_skip=False, fall_through=2):
                     if s.else_body:
                         self.accept(s.else_body)
-                breaking_out = breaking_out and self.binder.last_pop_breaking_out
-        if breaking_out:
-            self.binder.breaking_out = True
         return None
 
     def visit_while_stmt(self, s: WhileStmt) -> Type:
@@ -1592,11 +1590,11 @@ def visit_assert_stmt(self, s: AssertStmt) -> Type:
 
     def visit_raise_stmt(self, s: RaiseStmt) -> Type:
         """Type check a raise statement."""
-        self.binder.breaking_out = True
         if s.expr:
             self.type_check_raise(s.expr, s)
         if s.from_expr:
             self.type_check_raise(s.from_expr, s)
+        self.binder.unreachable()
 
     def type_check_raise(self, e: Expression, s: RaiseStmt) -> None:
         typ = self.accept(e)
@@ -1625,44 +1623,52 @@ def type_check_raise(self, e: Expression, s: RaiseStmt) -> None:
     def visit_try_stmt(self, s: TryStmt) -> Type:
         """Type check a try statement."""
         # Our enclosing frame will get the result if the try/except falls through.
-        # This one gets all possible intermediate states
-        with self.binder.frame_context():
+        # This one gets all possible states after the try block exited abnormally
+        # (by exception, return, break, etc.)
+        with self.binder.frame_context(can_skip=False, fall_through=0):
             if s.finally_body:
                 self.binder.try_frames.add(len(self.binder.frames) - 1)
-                breaking_out = self.visit_try_without_finally(s)
+                self.visit_try_without_finally(s)
                 self.binder.try_frames.remove(len(self.binder.frames) - 1)
                 # First we check finally_body is type safe for all intermediate frames
                 self.accept(s.finally_body)
-                breaking_out = breaking_out or self.binder.breaking_out
             else:
-                breaking_out = self.visit_try_without_finally(s)
-
-        if not breaking_out and s.finally_body:
-            # Then we try again for the more restricted set of options that can fall through
+                self.visit_try_without_finally(s)
+
+        if s.finally_body:
+            # Then we try again for the more restricted set of options
+            # that can fall through. (Why do we need to check the
+            # finally clause twice? Depending on whether the finally
+            # clause was reached by the try clause falling off the end
+            # or exiting abnormally, after completing the finally clause
+            # either flow will continue to after the entire try statement
+            # or the exception/return/etc. will be processed and control
+            # flow will escape. We need to check that the finally clause
+            # type checks in both contexts, but only the resulting types
+            # from the latter context affect the type state in the code
+            # that follows the try statement.)
             self.accept(s.finally_body)
-        self.binder.breaking_out = breaking_out
+
         return None
 
-    def visit_try_without_finally(self, s: TryStmt) -> bool:
+    def visit_try_without_finally(self, s: TryStmt) -> None:
         """Type check a try statement, ignoring the finally block.
 
-        Return whether we are guaranteed to be breaking out.
         Otherwise, it will place the results possible frames of
         that don't break out into self.binder.frames[-2].
         """
-        breaking_out = True
         # This frame records the possible states that exceptions can leave variables in
         # during the try: block
-        with self.binder.frame_context():
-            with self.binder.frame_context(3):
+        with self.binder.frame_context(can_skip=False, fall_through=0):
+            with self.binder.frame_context(can_skip=False, fall_through=3):
                 self.binder.try_frames.add(len(self.binder.frames) - 2)
+                self.binder.allow_jump(-1)
                 self.accept(s.body)
                 self.binder.try_frames.remove(len(self.binder.frames) - 2)
                 if s.else_body:
                     self.accept(s.else_body)
-            breaking_out = breaking_out and self.binder.last_pop_breaking_out
             for i in range(len(s.handlers)):
-                with self.binder.frame_context(3):
+                with self.binder.frame_context(can_skip=True, fall_through=3):
                     if s.types[i]:
                         t = self.visit_except_handler_test(s.types[i])
                         if s.vars[i]:
@@ -1686,8 +1692,6 @@ def visit_try_without_finally(self, s: TryStmt) -> bool:
                         var = cast(Var, s.vars[i].node)
                         var.type = DeletedType(source=source)
                         self.binder.cleanse(s.vars[i])
-                breaking_out = breaking_out and self.binder.last_pop_breaking_out
-        return breaking_out
 
     def visit_except_handler_test(self, n: Expression) -> Type:
         """Type check an exception handler test clause."""
@@ -1990,13 +1994,13 @@ def visit_member_expr(self, e: MemberExpr) -> Type:
         return self.expr_checker.visit_member_expr(e)
 
     def visit_break_stmt(self, s: BreakStmt) -> Type:
-        self.binder.breaking_out = True
         self.binder.allow_jump(self.binder.loop_frames[-1] - 1)
+        self.binder.unreachable()
         return None
 
     def visit_continue_stmt(self, s: ContinueStmt) -> Type:
-        self.binder.breaking_out = True
         self.binder.allow_jump(self.binder.loop_frames[-1])
+        self.binder.unreachable()
         return None
 
     def visit_int_expr(self, e: IntExpr) -> Type:
diff --git a/mypy/checkexpr.py b/mypy/checkexpr.py
index 1524a6528fee..551886c8ca41 100644
--- a/mypy/checkexpr.py
+++ b/mypy/checkexpr.py
@@ -1201,7 +1201,7 @@ def check_boolean_op(self, e: OpExpr, context: Context) -> Type:
             restricted_left_type = true_only(left_type)
             result_is_left = not left_type.can_be_false
 
-        with self.chk.binder.frame_context():
+        with self.chk.binder.frame_context(can_skip=True, fall_through=0):
             if right_map:
                 for var, type in right_map.items():
                     self.chk.binder.push(var, type)
@@ -1645,7 +1645,7 @@ def check_generator_or_comprehension(self, gen: GeneratorExpr,
                                          type_name: str,
                                          id_for_messages: str) -> Type:
         """Type check a generator expression or a list comprehension."""
-        with self.chk.binder.frame_context():
+        with self.chk.binder.frame_context(can_skip=True, fall_through=0):
             self.check_for_comp(gen)
 
             # Infer the type of the list comprehension by using a synthetic generic
@@ -1665,7 +1665,7 @@ def check_generator_or_comprehension(self, gen: GeneratorExpr,
 
     def visit_dictionary_comprehension(self, e: DictionaryComprehension) -> Type:
         """Type check a dictionary comprehension."""
-        with self.chk.binder.frame_context():
+        with self.chk.binder.frame_context(can_skip=True, fall_through=0):
             self.check_for_comp(e)
 
             # Infer the type of the list comprehension by using a synthetic generic
@@ -1739,7 +1739,7 @@ def visit_conditional_expr(self, e: ConditionalExpr) -> Type:
 
     def analyze_cond_branch(self, map: Optional[Dict[Expression, Type]],
                             node: Expression, context: Optional[Type]) -> Type:
-        with self.chk.binder.frame_context():
+        with self.chk.binder.frame_context(can_skip=True, fall_through=0):
             if map:
                 for var, type in map.items():
                     self.chk.binder.push(var, type)

From 673b2059eed1f980713e712bfeb2ce5be9152ca1 Mon Sep 17 00:00:00 2001
From: Reid Barton <rwbarton@gmail.com>
Date: Tue, 28 Jun 2016 16:59:29 -0400
Subject: [PATCH 02/13] Minor type cleanup in the binder and explanation of Key

This also fixes a bug where the index expression x['m'] was being treated
by the binder as equivalent to the member expression x.m.
---
 mypy/binder.py | 20 ++++++--------
 mypy/nodes.py  | 71 ++++++++++++++++++++++++++++++++++++++++----------
 2 files changed, 65 insertions(+), 26 deletions(-)

diff --git a/mypy/binder.py b/mypy/binder.py
index 3c556487bcf8..b1631753d1b9 100644
--- a/mypy/binder.py
+++ b/mypy/binder.py
@@ -1,15 +1,15 @@
-from typing import (Any, Dict, List, Set, Iterator, Union)
+from typing import (Dict, List, Set, Iterator, Union)
 from contextlib import contextmanager
 
 from mypy.types import Type, AnyType, PartialType
-from mypy.nodes import (Node, Expression, Var, RefExpr, SymbolTableNode)
+from mypy.nodes import (Key, Node, Expression, Var, RefExpr, SymbolTableNode)
 
 from mypy.subtypes import is_subtype
 from mypy.join import join_simple
 from mypy.sametypes import is_same_type
 
 
-class Frame(Dict[Any, Type]):
+class Frame(Dict[Key, Type]):
     """A Frame represents a specific point in the execution of a program.
     It carries information about the current types of expressions at
     that point, arising either from assignments to those expressions
@@ -25,10 +25,6 @@ def __init__(self) -> None:
         self.unreachable = False
 
 
-class Key(AnyType):
-    pass
-
-
 class ConditionalTypeBinder:
     """Keep track of conditional types of variables.
 
@@ -84,8 +80,8 @@ def _add_dependencies(self, key: Key, value: Key = None) -> None:
             value = key
         else:
             self.dependencies.setdefault(key, set()).add(value)
-        if isinstance(key, tuple):
-            for elt in key:
+        for elt in key:
+            if isinstance(elt, Key):
                 self._add_dependencies(elt, value)
 
     def push_frame(self) -> Frame:
@@ -190,9 +186,9 @@ def pop_frame(self, can_skip: bool, fall_through: int) -> Frame:
 
         return result
 
-    def get_declaration(self, node: Node) -> Type:
-        if isinstance(node, (RefExpr, SymbolTableNode)) and isinstance(node.node, Var):
-            type = node.node.type
+    def get_declaration(self, expr: Node) -> Type:
+        if isinstance(expr, RefExpr) and isinstance(expr.node, Var):
+            type = expr.node.type
             if isinstance(type, PartialType):
                 return None
             return type
diff --git a/mypy/nodes.py b/mypy/nodes.py
index ae1a630df2c8..064272b03b7d 100644
--- a/mypy/nodes.py
+++ b/mypy/nodes.py
@@ -91,6 +91,10 @@ def get_column(self) -> int: pass
                             for alias, name in type_aliases.items())  # type: Dict[str, str]
 
 
+# See [Note Literals and literal_hash] below
+Key = tuple
+
+
 class Node(Context):
     """Common base class for all non-type parse tree nodes."""
 
@@ -98,8 +102,9 @@ class Node(Context):
     column = -1
 
     # TODO: Move to Expression
+    # See [Note Literals and literal_hash] below
     literal = LITERAL_NO
-    literal_hash = None  # type: Any
+    literal_hash = None  # type: Key
 
     def __str__(self) -> str:
         ans = self.accept(mypy.strconv.StrConv())
@@ -146,6 +151,44 @@ class Expression(Node):
 Lvalue = Expression
 
 
+# [Note Literals and literal_hash]
+# ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+#
+# Mypy uses the term "literal" to refer to any expression built out of
+# the following:
+#
+# * Plain literal expressions, like `1` (integer, float, string, etc.)
+#
+# * Compound literal expressions, like `(lit1, lit2)` (list, dict,
+#   set, or tuple)
+#
+# * Operator expressions, like `lit1 + lit2`
+#
+# * Variable references, like `x`
+#
+# * Member references, like `lit.m`
+#
+# * Index expressions, like `lit[0]`
+#
+# A typical "literal" looks like `x[(i,j+1)].m`.
+#
+# An expression that is a literal has a `literal_hash`, with the
+# following properties.
+#
+# * `literal_hash` is a Key: a tuple containing basic data types and
+#   possibly other Keys. So it can be used as a key in a dictionary
+#   that will be compared by value (as opposed to the Node itself,
+#   which is compared by identity).
+#
+# * Two expressions have equal `literal_hash`es if and only if they
+#   are syntactically equal expressions. (NB: Actually, we also
+#   identify as equal expressions like `3` and `3.0`; is this a good
+#   idea?)
+#
+# * The elements of `literal_hash` that are tuples are exactly the
+#   subexpressions of the original expression (e.g. the base and index
+#   of an index expression, or the operands of an operator expression).
+
 class SymbolNode(Node):
     # Nodes that can be stored in a symbol table.
 
@@ -1002,7 +1045,7 @@ class IntExpr(Expression):
 
     def __init__(self, value: int) -> None:
         self.value = value
-        self.literal_hash = value
+        self.literal_hash = ('Literal', value)
 
     def accept(self, visitor: NodeVisitor[T]) -> T:
         return visitor.visit_int_expr(self)
@@ -1027,7 +1070,7 @@ class StrExpr(Expression):
 
     def __init__(self, value: str) -> None:
         self.value = value
-        self.literal_hash = value
+        self.literal_hash = ('Literal', value)
 
     def accept(self, visitor: NodeVisitor[T]) -> T:
         return visitor.visit_str_expr(self)
@@ -1041,7 +1084,7 @@ class BytesExpr(Expression):
 
     def __init__(self, value: str) -> None:
         self.value = value
-        self.literal_hash = value
+        self.literal_hash = ('Literal', value)
 
     def accept(self, visitor: NodeVisitor[T]) -> T:
         return visitor.visit_bytes_expr(self)
@@ -1055,7 +1098,7 @@ class UnicodeExpr(Expression):
 
     def __init__(self, value: str) -> None:
         self.value = value
-        self.literal_hash = value
+        self.literal_hash = ('Literal', value)
 
     def accept(self, visitor: NodeVisitor[T]) -> T:
         return visitor.visit_unicode_expr(self)
@@ -1069,7 +1112,7 @@ class FloatExpr(Expression):
 
     def __init__(self, value: float) -> None:
         self.value = value
-        self.literal_hash = value
+        self.literal_hash = ('Literal', value)
 
     def accept(self, visitor: NodeVisitor[T]) -> T:
         return visitor.visit_float_expr(self)
@@ -1083,7 +1126,7 @@ class ComplexExpr(Expression):
 
     def __init__(self, value: complex) -> None:
         self.value = value
-        self.literal_hash = value
+        self.literal_hash = ('Literal', value)
 
     def accept(self, visitor: NodeVisitor[T]) -> T:
         return visitor.visit_complex_expr(self)
@@ -1271,7 +1314,7 @@ def __init__(self, base: Expression, index: Expression) -> None:
         self.analyzed = None
         if self.index.literal == LITERAL_YES:
             self.literal = self.base.literal
-            self.literal_hash = ('Member', base.literal_hash,
+            self.literal_hash = ('Index', base.literal_hash,
                                  index.literal_hash)
 
     def accept(self, visitor: NodeVisitor[T]) -> T:
@@ -1390,7 +1433,7 @@ def __init__(self, operators: List[str], operands: List[Expression]) -> None:
         self.operands = operands
         self.method_types = []
         self.literal = min(o.literal for o in self.operands)
-        self.literal_hash = (('Comparison',) + tuple(operators) +
+        self.literal_hash = ((cast(Any, 'Comparison'),) + tuple(operators) +
                              tuple(o.literal_hash for o in operands))
 
     def accept(self, visitor: NodeVisitor[T]) -> T:
@@ -1481,7 +1524,7 @@ def __init__(self, items: List[Expression]) -> None:
         self.items = items
         if all(x.literal == LITERAL_YES for x in items):
             self.literal = LITERAL_YES
-            self.literal_hash = ('List',) + tuple(x.literal_hash for x in items)
+            self.literal_hash = (cast(Any, 'List'),) + tuple(x.literal_hash for x in items)
 
     def accept(self, visitor: NodeVisitor[T]) -> T:
         return visitor.visit_list_expr(self)
@@ -1499,8 +1542,8 @@ def __init__(self, items: List[Tuple[Expression, Expression]]) -> None:
         if all(x[0] and x[0].literal == LITERAL_YES and x[1].literal == LITERAL_YES
                for x in items):
             self.literal = LITERAL_YES
-            self.literal_hash = ('Dict',) + tuple(
-                (x[0].literal_hash, x[1].literal_hash) for x in items)  # type: ignore
+            self.literal_hash = (cast(Any, 'Dict'),) + tuple(
+                (x[0].literal_hash, x[1].literal_hash) for x in items)
 
     def accept(self, visitor: NodeVisitor[T]) -> T:
         return visitor.visit_dict_expr(self)
@@ -1515,7 +1558,7 @@ def __init__(self, items: List[Expression]) -> None:
         self.items = items
         if all(x.literal == LITERAL_YES for x in items):
             self.literal = LITERAL_YES
-            self.literal_hash = ('Tuple',) + tuple(x.literal_hash for x in items)
+            self.literal_hash = (cast(Any, 'Tuple'),) + tuple(x.literal_hash for x in items)
 
     def accept(self, visitor: NodeVisitor[T]) -> T:
         return visitor.visit_tuple_expr(self)
@@ -1530,7 +1573,7 @@ def __init__(self, items: List[Expression]) -> None:
         self.items = items
         if all(x.literal == LITERAL_YES for x in items):
             self.literal = LITERAL_YES
-            self.literal_hash = ('Set',) + tuple(x.literal_hash for x in items)
+            self.literal_hash = (cast(Any, 'Set'),) + tuple(x.literal_hash for x in items)
 
     def accept(self, visitor: NodeVisitor[T]) -> T:
         return visitor.visit_set_expr(self)

From 73815df3514c19a8575ea6abecf4d2a56b7bfd0d Mon Sep 17 00:00:00 2001
From: Reid Barton <rbarton@dropbox.com>
Date: Tue, 28 Jun 2016 14:26:01 -0700
Subject: [PATCH 03/13] Learn that loop condition is False on exit from while
 loop

---
 mypy/checker.py                      | 12 ++++++++--
 test-data/unit/check-isinstance.test | 36 ++++++++++++++++++++++++++++
 2 files changed, 46 insertions(+), 2 deletions(-)

diff --git a/mypy/checker.py b/mypy/checker.py
index 72a164691c62..36df3a1aec6a 100644
--- a/mypy/checker.py
+++ b/mypy/checker.py
@@ -227,8 +227,10 @@ def accept(self, node: Union[Expression, Statement, FuncItem],
         else:
             return typ
 
-    def accept_loop(self, body: Union[IfStmt, Block], else_body: Block = None) -> Type:
+    def accept_loop(self, body: Statement, else_body: Statement = None, *,
+                    exit_condition: Expression = None) -> Type:
         """Repeatedly type check a loop body until the frame doesn't change.
+        If exit_condition is set, assume it must be False on exit from the loop.
 
         Then check the else_body.
         """
@@ -241,6 +243,11 @@ def accept_loop(self, body: Union[IfStmt, Block], else_body: Block = None) -> Ty
                 if not self.binder.last_pop_changed:
                     break
             self.binder.pop_loop_frame()
+            if exit_condition:
+                _, else_map = find_isinstance_check(exit_condition, self.type_map)
+                if else_map:
+                    for var, type in else_map.items():
+                        self.binder.push(var, type)
             if else_body:
                 self.accept(else_body)
 
@@ -1562,7 +1569,8 @@ def visit_if_stmt(self, s: IfStmt) -> Type:
 
     def visit_while_stmt(self, s: WhileStmt) -> Type:
         """Type check a while statement."""
-        self.accept_loop(IfStmt([s.expr], [s.body], None), s.else_body)
+        self.accept_loop(IfStmt([s.expr], [s.body], None), s.else_body,
+                         exit_condition=s.expr)
 
     def visit_operator_assignment_stmt(self,
                                        s: OperatorAssignmentStmt) -> Type:
diff --git a/test-data/unit/check-isinstance.test b/test-data/unit/check-isinstance.test
index aae773b47c1c..f4f98b76cc33 100644
--- a/test-data/unit/check-isinstance.test
+++ b/test-data/unit/check-isinstance.test
@@ -908,6 +908,42 @@ def bar() -> None:
 [out]
 main: note: In function "bar":
 
+[case testWhileExitCondition1]
+from typing import Union
+x = 1  # type: Union[int, str]
+while isinstance(x, int):
+    if bool():
+        continue
+    x = 'a'
+else:
+    reveal_type(x)  # E: Revealed type is 'builtins.str'
+reveal_type(x)  # E: Revealed type is 'builtins.str'
+[builtins fixtures/isinstance.pyi]
+
+[case testWhileExitCondition2]
+from typing import Union
+x = 1  # type: Union[int, str]
+while isinstance(x, int):
+    if bool():
+        break
+    x = 'a'
+else:
+    reveal_type(x)  # E: Revealed type is 'builtins.str'
+reveal_type(x)  # E: Revealed type is 'Union[builtins.int, builtins.str]'
+[builtins fixtures/isinstance.pyi]
+
+[case testWhileLinkedList]
+from typing import Union
+LinkedList = Union['Cons', 'Nil']
+class Nil: pass
+class Cons:
+    tail = None  # type: LinkedList
+def last(x: LinkedList) -> Nil:
+    while isinstance(x, Cons):
+        x = x.tail
+    return x
+[builtins fixtures/isinstance.pyi]
+
 [case testReturnAndFlow]
 def foo() -> int:
     return 1 and 2

From 0a9c3c5ed4c0deb7d5cb3e9e4b963cbc687d5dac Mon Sep 17 00:00:00 2001
From: Reid Barton <rbarton@dropbox.com>
Date: Tue, 28 Jun 2016 14:41:25 -0700
Subject: [PATCH 04/13] Use bool() in tests when we want an unspecified bool in
 a conditional

---
 test-data/unit/check-fastparse.test        |  2 +-
 test-data/unit/check-functions.test        |  3 +-
 test-data/unit/check-isinstance.test       | 62 +++++++++++-----------
 test-data/unit/check-unreachable-code.test |  3 +-
 test-data/unit/fixtures/exception.pyi      |  1 +
 test-data/unit/fixtures/list.pyi           |  1 +
 test-data/unit/fixtures/property.pyi       |  1 +
 7 files changed, 39 insertions(+), 34 deletions(-)

diff --git a/test-data/unit/check-fastparse.test b/test-data/unit/check-fastparse.test
index c8865004a2ba..1ebb5ffa0cf1 100644
--- a/test-data/unit/check-fastparse.test
+++ b/test-data/unit/check-fastparse.test
@@ -36,7 +36,7 @@ class C:
 [case testFastParseConditionalProperty]
 # flags: --fast-parser
 class C:
-  if 1:
+  if bool():
     @property
     def x(self) -> str: pass
     @x.setter
diff --git a/test-data/unit/check-functions.test b/test-data/unit/check-functions.test
index 21fc62a9eca0..eee26199b9f1 100644
--- a/test-data/unit/check-functions.test
+++ b/test-data/unit/check-functions.test
@@ -1481,12 +1481,13 @@ g()
 [builtins fixtures/list.pyi]
 
 [case testFunctionDefinitionWithWhileStatement]
-while 1:
+while bool():
     def f(): pass
 else:
     def g(): pass
 f()
 g()
+[builtins fixtures/bool.pyi]
 
 [case testBareCallable]
 from typing import Callable, Any
diff --git a/test-data/unit/check-isinstance.test b/test-data/unit/check-isinstance.test
index f4f98b76cc33..3264a7cbf774 100644
--- a/test-data/unit/check-isinstance.test
+++ b/test-data/unit/check-isinstance.test
@@ -12,7 +12,7 @@ x = None # type: List[Any]
 def foo() -> List[int]: pass
 def bar() -> List[str]: pass
 
-if 1:
+if bool():
     x = foo()
 else:
     x = bar()
@@ -143,11 +143,11 @@ def bar() -> None:
     x = foo()
     if isinstance(x, int):
         return
-    while 1:
+    while bool():
         x + 'a'
-        while 1:
+        while bool():
             x = foo()
-            if 1:
+            if bool():
                 return
             x = 'a'
     x + 'a'
@@ -163,11 +163,11 @@ def bar() -> None:
     x = foo()
     if isinstance(x, int):
         return
-    while 1:
+    while bool():
         x + 'a'
-        while 1:
+        while bool():
             x = foo()
-            if 1:
+            if bool():
                 return
             x = 'a'
     x + 'a'
@@ -175,12 +175,12 @@ def bar() -> None:
     x = foo()
     if isinstance(x, int):
         return
-    while 1:
+    while bool():
         x + 'a'
-        while 1:
+        while bool():
             x + 'a'         # E: Unsupported operand types for + (likely involving Union)
             x = foo()
-            if 1:
+            if bool():
                 continue
             x = 'a'
         x = 'a'
@@ -269,7 +269,7 @@ class A: pass
 class B(A): z = 1
 
 x = A()
-while 1:
+while bool():
     try:
         x.z # E: "A" has no attribute "z"
         x = A()
@@ -473,7 +473,7 @@ class House:
 h = House()
 h.pet = Dog()
 
-while 1:
+while bool():
     if isinstance(h.pet, Dog):
         if isinstance(h.pet.paws, str):
             x = h.pet.paws + 'a'
@@ -560,7 +560,7 @@ if isinstance(h.pet, Dog):
     if isinstance(h.pet.paws, str):
         for i in [1]:
             h.pet.paws + 'a'
-            if 1:
+            if bool():
                 break
             h.pet.paws = 1
             h.pet.paws + 1
@@ -612,7 +612,7 @@ from typing import Union, List
 
 x = None # type: Union[int, str, List[int]]
 
-while 1:
+while bool():
     if isinstance(x, int):
         x + 1
     elif isinstance(x, str):
@@ -628,7 +628,7 @@ from typing import Union, List
 
 x = None # type: Union[int, str, List[int]]
 
-while 1:
+while bool():
     if isinstance(x, int):
         x + 1
         break
@@ -644,7 +644,7 @@ x + [1]               # E: Unsupported operand types for + (likely involving Uni
 [case testIsInstanceThreeUnion3]
 from typing import Union, List
 
-while 1:
+while bool():
     x = None # type: Union[int, str, List[int]]
     x = 1
     if isinstance(x, int):
@@ -724,7 +724,7 @@ x + 1      # E: Unsupported operand types for + ("str" and "int")
 x = 1
 x + 1
 
-while 1:
+while bool():
       x + 1    # E: Unsupported operand types for + (likely involving Union)
       x = 'a'
 [builtins fixtures/isinstancelist.pyi]
@@ -757,7 +757,7 @@ def foo() -> Union[int, str]: pass
 x = foo()
 x = 1
 
-while 1:
+while bool():
     x + 1
     x = 'a'
     break
@@ -782,9 +782,9 @@ def foo() -> Union[int, str]: pass
 x = foo()
 x = 1
 
-while 1:
+while bool():
     x + 1
-    if 1:
+    if bool():
         x = 'a'
         break
 else:
@@ -792,9 +792,9 @@ else:
     x = 'a'
 x + 'a'
 x = 1
-while 1:
+while bool():
     x + 1 # E: Unsupported operand types for + (likely involving Union)
-    if 1:
+    if bool():
         x = 'a'
         continue
 else:
@@ -812,7 +812,7 @@ x = 1
 
 for y in [1]:
     x + 1
-    if 1:
+    if bool():
         x = 'a'
         break
 else:
@@ -822,7 +822,7 @@ x + 'a'
 x = 1
 for y in [1]:
     x + 1 # E: Unsupported operand types for + (likely involving Union)
-    if 1:
+    if bool():
         x = 'a'
         continue
 else:
@@ -848,8 +848,8 @@ else:
     x + 1
 x + 1 # E: Unsupported operand types for + (likely involving Union)
 x = 1
-while 1:
-    while 1:
+while bool():
+    while bool():
         break
     else:
         x = 'a'
@@ -883,13 +883,13 @@ def bar() -> None:
     if isinstance(x, str):
        x + 'a'
     else:
-       while 1:
+       while bool():
           if isinstance(x, int):
              x + 1
           else:
              x.a
           break
-       while 1:
+       while bool():
           if isinstance(x, int):
              x + 1
           else:
@@ -897,7 +897,7 @@ def bar() -> None:
           continue
 
        #for i in [1]:
-       while 1:
+       while bool():
           if isinstance(x, int):
              x + 1
           else:
@@ -967,7 +967,7 @@ x + 'a'   # E: Unsupported operand types for + ("int" and "str")
 [case testUnreachableCode]
 x = 1 # type: int
 
-while 1:
+while bool():
     x = 'a'           # E: Incompatible types in assignment (expression has type "str", variable has type "int")
     break
     x = 'a'           # Note: no error because unreachable code
@@ -975,7 +975,7 @@ while 1:
 
 [case testUnreachableCode2]
 x = 1
-while 1:
+while bool():
     try:
         pass
     except:
diff --git a/test-data/unit/check-unreachable-code.test b/test-data/unit/check-unreachable-code.test
index 36ad7bbe1988..d540a2db8beb 100644
--- a/test-data/unit/check-unreachable-code.test
+++ b/test-data/unit/check-unreachable-code.test
@@ -146,12 +146,13 @@ def f(): pass
 PY3 = f()
 if PY3:
     pass
-elif 1:
+elif bool():
     import nonexistent
     1 + ''
 else:
     import bad_name
     1 + ''
+[builtins fixtures/bool.pyi]
 [out]
 
 [case testSysVersionInfo_python2]
diff --git a/test-data/unit/fixtures/exception.pyi b/test-data/unit/fixtures/exception.pyi
index db9370c3e55f..05015ec443af 100644
--- a/test-data/unit/fixtures/exception.pyi
+++ b/test-data/unit/fixtures/exception.pyi
@@ -7,5 +7,6 @@ class tuple: pass
 class function: pass
 class int: pass
 class str: pass
+class bool: pass
 
 class BaseException: pass
diff --git a/test-data/unit/fixtures/list.pyi b/test-data/unit/fixtures/list.pyi
index 220ab529b818..2f9893d727bb 100644
--- a/test-data/unit/fixtures/list.pyi
+++ b/test-data/unit/fixtures/list.pyi
@@ -26,3 +26,4 @@ class tuple: pass
 class function: pass
 class int: pass
 class str: pass
+class bool: pass
diff --git a/test-data/unit/fixtures/property.pyi b/test-data/unit/fixtures/property.pyi
index 503bc1aba915..b2e747bbbd3e 100644
--- a/test-data/unit/fixtures/property.pyi
+++ b/test-data/unit/fixtures/property.pyi
@@ -14,3 +14,4 @@ class int: pass
 class str: pass
 class bytes: pass
 class tuple: pass
+class bool: pass

From d064ce5b4223add82260aa7b0bf9e94ebd3da57e Mon Sep 17 00:00:00 2001
From: Reid Barton <rbarton@dropbox.com>
Date: Tue, 28 Jun 2016 15:35:40 -0700
Subject: [PATCH 05/13] Handle 'while True', 'assert False'

---
 mypy/checker.py                      | 24 +++++++-
 test-data/unit/check-isinstance.test | 83 ++++++++++++++++++++++++++++
 test-data/unit/check-modules.test    | 11 ++++
 test-data/unit/check-optional.test   |  4 +-
 4 files changed, 117 insertions(+), 5 deletions(-)

diff --git a/mypy/checker.py b/mypy/checker.py
index 36df3a1aec6a..828e9cdea958 100644
--- a/mypy/checker.py
+++ b/mypy/checker.py
@@ -245,7 +245,9 @@ def accept_loop(self, body: Statement, else_body: Statement = None, *,
             self.binder.pop_loop_frame()
             if exit_condition:
                 _, else_map = find_isinstance_check(exit_condition, self.type_map)
-                if else_map:
+                if else_map is None:
+                    self.binder.unreachable()
+                else:
                     for var, type in else_map.items():
                         self.binder.push(var, type)
             if else_body:
@@ -1592,7 +1594,9 @@ def visit_assert_stmt(self, s: AssertStmt) -> Type:
         # If this is asserting some isinstance check, bind that type in the following code
         true_map, _ = find_isinstance_check(s.expr, self.type_map)
 
-        if true_map:
+        if true_map is None:
+            self.binder.unreachable()
+        else:
             for var, type in true_map.items():
                 self.binder.push(var, type)
 
@@ -2384,6 +2388,16 @@ def conditional_type_map(expr: Expression,
         return {}, {}
 
 
+def is_true_literal(n: Expression) -> bool:
+    return (refers_to_fullname(n, 'builtins.True')
+            or isinstance(n, IntExpr) and n.value == 1)
+
+
+def is_false_literal(n: Expression) -> bool:
+    return (refers_to_fullname(n, 'builtins.False')
+            or isinstance(n, IntExpr) and n.value == 0)
+
+
 def is_literal_none(n: Expression) -> bool:
     return isinstance(n, NameExpr) and n.fullname == 'builtins.None'
 
@@ -2446,7 +2460,11 @@ def find_isinstance_check(node: Expression,
 
     Guaranteed to not return None, None. (But may return {}, {})
     """
-    if isinstance(node, CallExpr):
+    if is_true_literal(node):
+        return {}, None
+    elif is_false_literal(node):
+        return None, {}
+    elif isinstance(node, CallExpr):
         if refers_to_fullname(node.callee, 'builtins.isinstance'):
             expr = node.args[0]
             if expr.literal == LITERAL_TYPE:
diff --git a/test-data/unit/check-isinstance.test b/test-data/unit/check-isinstance.test
index 3264a7cbf774..e222b11b6222 100644
--- a/test-data/unit/check-isinstance.test
+++ b/test-data/unit/check-isinstance.test
@@ -985,6 +985,89 @@ while bool():
     x + 'a'
 [builtins fixtures/isinstance.pyi]
 
+[case testUnreachableWhileTrue]
+def f(x: int) -> None:
+    while True:
+        if x:
+            return
+    1()
+[builtins fixtures/bool.pyi]
+
+[case testUnreachableAssertFalse]
+def f() -> None:
+    assert False
+    1()
+[builtins fixtures/bool.pyi]
+
+[case testUnreachableAssertFalse2]
+# flags: --fast-parser
+def f() -> None:
+    # The old parser doesn't understand the syntax below
+    assert False, "hi"
+    1()
+[builtins fixtures/bool.pyi]
+
+[case testUnreachableReturnOrAssertFalse]
+def f(x: int) -> int:
+    if x:
+        return x
+    else:
+        assert False
+    1()
+[builtins fixtures/bool.pyi]
+
+[case testUnreachableTryExcept]
+def f() -> None:
+    try:
+        f()
+        return
+    except BaseException:
+        return
+    1()
+[builtins fixtures/exception.pyi]
+
+[case testUnreachableTryExceptElse]
+def f() -> None:
+    try:
+        f()
+    except BaseException:
+        return
+    else:
+        return
+    1()
+[builtins fixtures/exception.pyi]
+
+[case testUnreachableTryReturnFinally1]
+def f() -> None:
+    try:
+        return
+    finally:
+        pass
+    1()
+
+[case testUnreachableTryReturnFinally2]
+def f() -> None:
+    try:
+        pass
+    finally:
+        return
+    1()
+
+[case testUnreachableTryReturnExceptRaise]
+def f() -> None:
+    try:
+        return
+    except:
+        raise
+    1()
+
+[case testUnreachableReturnLambda]
+from typing import Callable
+def g(t: Callable[[int], int]) -> int: pass
+def f() -> int:
+    return g(lambda x: x)
+    1()
+
 [case testIsinstanceAnd]
 class A:
     pass
diff --git a/test-data/unit/check-modules.test b/test-data/unit/check-modules.test
index 981554369359..c25c0f168e0c 100644
--- a/test-data/unit/check-modules.test
+++ b/test-data/unit/check-modules.test
@@ -1026,6 +1026,17 @@ bar = 0
 [builtins fixtures/module.pyi]
 [out]
 
+[case testIfFalseImport]
+if False:
+    import a
+def f(x: 'a.A') -> int:
+    return x.f()
+[file a.py]
+class A:
+    def f(self) -> int:
+        return 0
+[builtins fixtures/bool.pyi]
+
 
 -- Test stability under import cycles
 -- ----------------------------------
diff --git a/test-data/unit/check-optional.test b/test-data/unit/check-optional.test
index e1400620960b..8e8daf74522e 100644
--- a/test-data/unit/check-optional.test
+++ b/test-data/unit/check-optional.test
@@ -86,7 +86,7 @@ y2 = x or 1
 reveal_type(y2)  # E: Revealed type is 'Union[builtins.str, builtins.int]'
 z1 = 'a' or x
 reveal_type(z1)  # E: Revealed type is 'Union[builtins.str, builtins.None]'
-z2 = 1 or x
+z2 = int() or x
 reveal_type(z2)  # E: Revealed type is 'Union[builtins.int, builtins.str, builtins.None]'
 
 [case testAndCases]
@@ -98,7 +98,7 @@ y2 = x and 1  # x could be '', so...
 reveal_type(y2)  # E: Revealed type is 'Union[builtins.str, builtins.None, builtins.int]'
 z1 = 'b' and x
 reveal_type(z1)  # E: Revealed type is 'Union[builtins.str, builtins.None]'
-z2 = 1 and x
+z2 = int() and x
 reveal_type(z2)  # E: Revealed type is 'Union[builtins.int, builtins.str, builtins.None]'
 
 [case testLambdaReturningNone]

From cf50f439db38f13b61ff5cf87dc0a29adc941a5f Mon Sep 17 00:00:00 2001
From: Reid Barton <rbarton@dropbox.com>
Date: Tue, 28 Jun 2016 16:08:32 -0700
Subject: [PATCH 06/13] Reduce duplication with find_isinstance_check and
 binder.push

The resulting simplification of visit_if_expr revealed a bug in the
binder: if a frame was marked as unreachable, but then a new frame
context was begun immediately, the new frame was not marked as
unreachable, and a block visited inside the new frame would be type
checked. For now we check all frames for reachability; probably there
is a more efficient way to do this.

This commit also cleans up check_boolean_op slightly.
---
 mypy/binder.py                        |  4 +-
 mypy/checker.py                       | 69 +++++++++++----------------
 mypy/checkexpr.py                     | 24 ++++------
 test-data/unit/check-expressions.test |  7 +--
 4 files changed, 46 insertions(+), 58 deletions(-)

diff --git a/mypy/binder.py b/mypy/binder.py
index b1631753d1b9..6db7d50876bc 100644
--- a/mypy/binder.py
+++ b/mypy/binder.py
@@ -118,7 +118,9 @@ def get(self, expr: Union[Expression, Var]) -> Type:
         return self._get(expr.literal_hash)
 
     def is_unreachable(self) -> bool:
-        return self.frames[-1].unreachable
+        # TODO: Copy the value of unreachable into new frames to avoid
+        # this traversal on every statement?
+        return any(f.unreachable for f in self.frames)
 
     def cleanse(self, expr: Expression) -> None:
         """Remove all references to a Node from the binder."""
diff --git a/mypy/checker.py b/mypy/checker.py
index 828e9cdea958..42c98222e886 100644
--- a/mypy/checker.py
+++ b/mypy/checker.py
@@ -244,12 +244,8 @@ def accept_loop(self, body: Statement, else_body: Statement = None, *,
                     break
             self.binder.pop_loop_frame()
             if exit_condition:
-                _, else_map = find_isinstance_check(exit_condition, self.type_map)
-                if else_map is None:
-                    self.binder.unreachable()
-                else:
-                    for var, type in else_map.items():
-                        self.binder.push(var, type)
+                _, else_map = self.find_isinstance_check(exit_condition)
+                self.push_type_map(else_map)
             if else_body:
                 self.accept(else_body)
 
@@ -1539,34 +1535,19 @@ def visit_if_stmt(self, s: IfStmt) -> Type:
             for e, b in zip(s.expr, s.body):
                 t = self.accept(e)
                 self.check_usable_type(t, e)
-                if_map, else_map = find_isinstance_check(e, self.type_map)
-                if if_map is None:
-                    # The condition is always false
-                    # XXX should issue a warning?
-                    pass
-                else:
-                    # Only type check body if the if condition can be true.
-                    with self.binder.frame_context(can_skip=True, fall_through=2):
-                        if if_map:
-                            for var, type in if_map.items():
-                                self.binder.push(var, type)
-
-                        self.accept(b)
-
-                    if else_map:
-                        for var, type in else_map.items():
-                            self.binder.push(var, type)
-                if else_map is None:
-                    # The condition is always true => remaining elif/else blocks
-                    # can never be reached.
-
-                    # Might also want to issue a warning
-                    # print("Warning: isinstance always true")
-                    break
-            else:  # Didn't break => can't prove one of the conditions is always true
-                with self.binder.frame_context(can_skip=False, fall_through=2):
-                    if s.else_body:
-                        self.accept(s.else_body)
+                if_map, else_map = self.find_isinstance_check(e)
+
+                # XXX Issue a warning if condition is always False?
+                with self.binder.frame_context(can_skip=True, fall_through=2):
+                    self.push_type_map(if_map)
+                    self.accept(b)
+
+                # XXX Issue a warning if condition is always True?
+                self.push_type_map(else_map)
+
+            with self.binder.frame_context(can_skip=False, fall_through=2):
+                if s.else_body:
+                    self.accept(s.else_body)
         return None
 
     def visit_while_stmt(self, s: WhileStmt) -> Type:
@@ -1592,13 +1573,9 @@ def visit_assert_stmt(self, s: AssertStmt) -> Type:
         self.accept(s.expr)
 
         # If this is asserting some isinstance check, bind that type in the following code
-        true_map, _ = find_isinstance_check(s.expr, self.type_map)
+        true_map, _ = self.find_isinstance_check(s.expr)
 
-        if true_map is None:
-            self.binder.unreachable()
-        else:
-            for var, type in true_map.items():
-                self.binder.push(var, type)
+        self.push_type_map(true_map)
 
     def visit_raise_stmt(self, s: RaiseStmt) -> Type:
         """Type check a raise statement."""
@@ -2343,6 +2320,18 @@ def function_type(self, func: FuncBase) -> FunctionLike:
     def method_type(self, func: FuncBase) -> FunctionLike:
         return method_type_with_fallback(func, self.named_type('builtins.function'))
 
+    # TODO: These next two functions should refer to TypeMap below
+    def find_isinstance_check(self, n: Expression) -> Tuple[Optional[Dict[Expression, Type]],
+                                                            Optional[Dict[Expression, Type]]]:
+        return find_isinstance_check(n, self.type_map)
+
+    def push_type_map(self, type_map: Optional[Dict[Expression, Type]]) -> None:
+        if type_map is None:
+            self.binder.unreachable()
+        else:
+            for expr, type in type_map.items():
+                self.binder.push(expr, type)
+
 
 # Data structure returned by find_isinstance_check representing
 # information learned from the truth or falsehood of a condition.  The
diff --git a/mypy/checkexpr.py b/mypy/checkexpr.py
index 551886c8ca41..6f4de4a060ea 100644
--- a/mypy/checkexpr.py
+++ b/mypy/checkexpr.py
@@ -1191,22 +1191,15 @@ def check_boolean_op(self, e: OpExpr, context: Context) -> Type:
         assert e.op in ('and', 'or')  # Checked by visit_op_expr
 
         if e.op == 'and':
-            right_map, left_map = \
-                mypy.checker.find_isinstance_check(e.left, self.chk.type_map)
+            right_map, left_map = self.chk.find_isinstance_check(e.left)
             restricted_left_type = false_only(left_type)
             result_is_left = not left_type.can_be_true
         elif e.op == 'or':
-            left_map, right_map = \
-                mypy.checker.find_isinstance_check(e.left, self.chk.type_map)
+            left_map, right_map = self.chk.find_isinstance_check(e.left)
             restricted_left_type = true_only(left_type)
             result_is_left = not left_type.can_be_false
 
-        with self.chk.binder.frame_context(can_skip=True, fall_through=0):
-            if right_map:
-                for var, type in right_map.items():
-                    self.chk.binder.push(var, type)
-
-            right_type = self.accept(e.right, left_type)
+        right_type = self.analyze_cond_branch(right_map, e.right, left_type)
 
         self.check_usable_type(left_type, context)
         self.check_usable_type(right_type, context)
@@ -1712,7 +1705,7 @@ def visit_conditional_expr(self, e: ConditionalExpr) -> Type:
 
         # Gain type information from isinstance if it is there
         # but only for the current expression
-        if_map, else_map = mypy.checker.find_isinstance_check(e.cond, self.chk.type_map)
+        if_map, else_map = self.chk.find_isinstance_check(e.cond)
 
         if_type = self.analyze_cond_branch(if_map, e.if_expr, context=ctx)
 
@@ -1740,9 +1733,12 @@ def visit_conditional_expr(self, e: ConditionalExpr) -> Type:
     def analyze_cond_branch(self, map: Optional[Dict[Expression, Type]],
                             node: Expression, context: Optional[Type]) -> Type:
         with self.chk.binder.frame_context(can_skip=True, fall_through=0):
-            if map:
-                for var, type in map.items():
-                    self.chk.binder.push(var, type)
+            if map is None:
+                # We still need to type check node, in case we want to
+                # process it for isinstance checks later
+                self.accept(node, context=context)
+                return UninhabitedType()
+            self.chk.push_type_map(map)
             return self.accept(node, context=context)
 
     def visit_backquote_expr(self, e: BackquoteExpr) -> Type:
diff --git a/test-data/unit/check-expressions.test b/test-data/unit/check-expressions.test
index 2878e42ab26f..6ea0a9fba912 100644
--- a/test-data/unit/check-expressions.test
+++ b/test-data/unit/check-expressions.test
@@ -1298,16 +1298,17 @@ x = 1 if f() else 2 # E: "f" does not return a value
 import typing
 class A: pass
 class B(A): pass
-x = B() if None else A()
+x = B() if bool() else A()
 x = A()
 x = '' # E: Incompatible types in assignment (expression has type "str", variable has type "A")
-y = A() if None else B()
+y = A() if bool() else B()
 y = A()
 y = '' # E: Incompatible types in assignment (expression has type "str", variable has type "A")
+[builtins fixtures/bool.pyi]
 
 [case testConditionalExpressionAndTypeContext]
 import typing
-x = [1] if None else []
+x = [1] if bool() else []
 x = [1]
 x = ['x'] # E: List item 0 has incompatible type "str"
 [builtins fixtures/list.pyi]

From 4388a8145eea27692a0884c7716b919aafe85f69 Mon Sep 17 00:00:00 2001
From: Reid Barton <rbarton@dropbox.com>
Date: Tue, 28 Jun 2016 18:24:23 -0700
Subject: [PATCH 07/13] Process try statements in top-to-bottom order

Fixes #1289 (again).
---
 mypy/checker.py                      | 79 +++++++++++++++-------------
 test-data/unit/check-optional.test   |  3 --
 test-data/unit/check-statements.test |  2 +-
 3 files changed, 44 insertions(+), 40 deletions(-)

diff --git a/mypy/checker.py b/mypy/checker.py
index 42c98222e886..a4c1eb4a68bf 100644
--- a/mypy/checker.py
+++ b/mypy/checker.py
@@ -1643,44 +1643,51 @@ def visit_try_stmt(self, s: TryStmt) -> Type:
     def visit_try_without_finally(self, s: TryStmt) -> None:
         """Type check a try statement, ignoring the finally block.
 
-        Otherwise, it will place the results possible frames of
-        that don't break out into self.binder.frames[-2].
+        On entry, the top frame should receive all flow that exits the
+        try block abnormally (i.e., such that the else block does not
+        execute), and its parent should receive all flow that exits
+        the try block normally.
         """
-        # This frame records the possible states that exceptions can leave variables in
-        # during the try: block
-        with self.binder.frame_context(can_skip=False, fall_through=0):
-            with self.binder.frame_context(can_skip=False, fall_through=3):
-                self.binder.try_frames.add(len(self.binder.frames) - 2)
-                self.binder.allow_jump(-1)
-                self.accept(s.body)
-                self.binder.try_frames.remove(len(self.binder.frames) - 2)
-                if s.else_body:
-                    self.accept(s.else_body)
-            for i in range(len(s.handlers)):
-                with self.binder.frame_context(can_skip=True, fall_through=3):
-                    if s.types[i]:
-                        t = self.visit_except_handler_test(s.types[i])
+        # This frame will run the else block if the try fell through.
+        # In that case, control flow continues to the parent of what
+        # was the top frame on entry.
+        with self.binder.frame_context(can_skip=False, fall_through=2):
+            # This frame receives exit via exception, and runs exception handlers
+            with self.binder.frame_context(can_skip=False, fall_through=2):
+                # Finally, the body of the try statement
+                with self.binder.frame_context(can_skip=False, fall_through=2):
+                    self.binder.try_frames.add(len(self.binder.frames) - 2)
+                    self.binder.allow_jump(-1)
+                    self.accept(s.body)
+                    self.binder.try_frames.remove(len(self.binder.frames) - 2)
+                for i in range(len(s.handlers)):
+                    with self.binder.frame_context(can_skip=True, fall_through=4):
+                        if s.types[i]:
+                            t = self.visit_except_handler_test(s.types[i])
+                            if s.vars[i]:
+                                # To support local variables, we make this a definition line,
+                                # causing assignment to set the variable's type.
+                                s.vars[i].is_def = True
+                                self.check_assignment(s.vars[i], self.temp_node(t, s.vars[i]))
+                        self.accept(s.handlers[i])
                         if s.vars[i]:
-                            # To support local variables, we make this a definition line,
-                            # causing assignment to set the variable's type.
-                            s.vars[i].is_def = True
-                            self.check_assignment(s.vars[i], self.temp_node(t, s.vars[i]))
-                    self.accept(s.handlers[i])
-                    if s.vars[i]:
-                        # Exception variables are deleted in python 3 but not python 2.
-                        # But, since it's bad form in python 2 and the type checking
-                        # wouldn't work very well, we delete it anyway.
-
-                        # Unfortunately, this doesn't let us detect usage before the
-                        # try/except block.
-                        if self.options.python_version[0] >= 3:
-                            source = s.vars[i].name
-                        else:
-                            source = ('(exception variable "{}", which we do not accept outside'
-                                      'except: blocks even in python 2)'.format(s.vars[i].name))
-                        var = cast(Var, s.vars[i].node)
-                        var.type = DeletedType(source=source)
-                        self.binder.cleanse(s.vars[i])
+                            # Exception variables are deleted in python 3 but not python 2.
+                            # But, since it's bad form in python 2 and the type checking
+                            # wouldn't work very well, we delete it anyway.
+
+                            # Unfortunately, this doesn't let us detect usage before the
+                            # try/except block.
+                            if self.options.python_version[0] >= 3:
+                                source = s.vars[i].name
+                            else:
+                                source = ('(exception variable "{}", which we do not '
+                                          'accept outside except: blocks even in '
+                                          'python 2)'.format(s.vars[i].name))
+                            var = cast(Var, s.vars[i].node)
+                            var.type = DeletedType(source=source)
+                            self.binder.cleanse(s.vars[i])
+            if s.else_body:
+                self.accept(s.else_body)
 
     def visit_except_handler_test(self, n: Expression) -> Type:
         """Type check an exception handler test clause."""
diff --git a/test-data/unit/check-optional.test b/test-data/unit/check-optional.test
index 8e8daf74522e..7a20715cc9c4 100644
--- a/test-data/unit/check-optional.test
+++ b/test-data/unit/check-optional.test
@@ -368,9 +368,6 @@ def lookup_field(name, obj):
         attr = f()
     else:
         attr = None
-[out]
-main: note: In function "lookup_field":
-main:10: error: Need type annotation for variable
 
 [case testTernaryWithNone]
 reveal_type(None if bool() else 0)  # 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 b53912190149..0bbe47e9e686 100644
--- a/test-data/unit/check-statements.test
+++ b/test-data/unit/check-statements.test
@@ -530,7 +530,7 @@ else:
   object(None) # E: Too many arguments for "object"
 [builtins fixtures/exception.pyi]
 
-[case testRedefinedFunctionInTryWithElse-skip]
+[case testRedefinedFunctionInTryWithElse]
 def f() -> None: pass
 try:
     pass

From 5b5118104d0285f07170693cf0e5c6438110d4ca Mon Sep 17 00:00:00 2001
From: Reid Barton <rbarton@dropbox.com>
Date: Thu, 30 Jun 2016 17:08:33 -0700
Subject: [PATCH 08/13] Fix return type of binder.unreachable

---
 mypy/binder.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/mypy/binder.py b/mypy/binder.py
index 6db7d50876bc..64fc6e9364ef 100644
--- a/mypy/binder.py
+++ b/mypy/binder.py
@@ -111,7 +111,7 @@ def push(self, node: Node, typ: Type) -> None:
             self._add_dependencies(key)
         self._push(key, typ)
 
-    def unreachable(self) -> bool:
+    def unreachable(self) -> None:
         self.frames[-1].unreachable = True
 
     def get(self, expr: Union[Expression, Var]) -> Type:

From 1f6a43b02332c9022c3b8d90b212e33b6e60c93e Mon Sep 17 00:00:00 2001
From: Eric Price <ecprice@mit.edu>
Date: Wed, 22 Jun 2016 13:35:34 -0700
Subject: [PATCH 09/13] Add warn-no-return flag to give a note on missing
 return statements

---
 mypy/checker.py                    | 22 +++++++++-
 mypy/main.py                       |  2 +
 mypy/messages.py                   |  1 +
 mypy/options.py                    |  3 ++
 test-data/unit/check-warnings.test | 70 ++++++++++++++++++++++++++++++
 5 files changed, 97 insertions(+), 1 deletion(-)

diff --git a/mypy/checker.py b/mypy/checker.py
index a4c1eb4a68bf..37767f39bbd7 100644
--- a/mypy/checker.py
+++ b/mypy/checker.py
@@ -19,7 +19,7 @@
     TypeApplication, DictExpr, SliceExpr, FuncExpr, TempNode, SymbolTableNode,
     Context, ListComprehension, ConditionalExpr, GeneratorExpr,
     Decorator, SetExpr, TypeVarExpr, NewTypeExpr, PrintStmt,
-    LITERAL_TYPE, BreakStmt, ContinueStmt, ComparisonExpr, StarExpr,
+    LITERAL_TYPE, BreakStmt, PassStmt, ContinueStmt, ComparisonExpr, StarExpr,
     YieldFromExpr, NamedTupleExpr, SetComprehension,
     DictionaryComprehension, ComplexExpr, EllipsisExpr, TypeAliasExpr,
     RefExpr, YieldExpr, BackquoteExpr, ImportFrom, ImportAll, ImportBase,
@@ -611,11 +611,31 @@ def is_implicit_any(t: Type) -> bool:
             # Type check body in a new scope.
             with self.binder.top_frame_context():
                 self.accept(item.body)
+                unreachable = self.binder.is_unreachable()
+
+            if (self.options.warn_no_return and not unreachable
+                    and not isinstance(self.return_types[-1], (Void, AnyType))
+                    and not defn.is_generator):
+                # Control flow fell off the end of a function that was
+                # declared to return a non-None type.
+                # Allow functions that are entirely pass/Ellipsis.
+                if self.is_trivial_body(defn.body):
+                    pass
+                else:
+                    self.msg.note(messages.MISSING_RETURN_STATEMENT, defn)
 
             self.return_types.pop()
 
             self.binder = old_binder
 
+    def is_trivial_body(self, block: Block) -> bool:
+        if len(block.body) != 1:
+            return False
+        stmt = block.body[0]
+        return (isinstance(stmt, PassStmt) or
+                (isinstance(stmt, ExpressionStmt) and
+                 isinstance(stmt.expr, EllipsisExpr)))
+
     def check_reverse_op_method(self, defn: FuncItem, typ: CallableType,
                                 method: str) -> None:
         """Check a reverse operator method such as __radd__."""
diff --git a/mypy/main.py b/mypy/main.py
index bbc30028639d..d29e5ff0c103 100644
--- a/mypy/main.py
+++ b/mypy/main.py
@@ -160,6 +160,8 @@ def process_options(args: List[str],
                         " --check-untyped-defs enabled")
     parser.add_argument('--warn-redundant-casts', action='store_true',
                         help="warn about casting an expression to its inferred type")
+    parser.add_argument('--warn-no-return', action='store_true',
+                        help="warn about functions that end without returning")
     parser.add_argument('--warn-unused-ignores', action='store_true',
                         help="warn about unneeded '# type: ignore' comments")
     parser.add_argument('--hide-error-context', action='store_true',
diff --git a/mypy/messages.py b/mypy/messages.py
index b4828f1bfe08..e39a424fbf40 100644
--- a/mypy/messages.py
+++ b/mypy/messages.py
@@ -23,6 +23,7 @@
 # that do not have any parameters.
 
 NO_RETURN_VALUE_EXPECTED = 'No return value expected'
+MISSING_RETURN_STATEMENT = 'Missing return statement'
 INCOMPATIBLE_RETURN_VALUE_TYPE = 'Incompatible return value type'
 RETURN_VALUE_EXPECTED = 'Return value expected'
 BOOLEAN_VALUE_EXPECTED = 'Boolean value expected'
diff --git a/mypy/options.py b/mypy/options.py
index 1d0945645a83..62f0fe42cb66 100644
--- a/mypy/options.py
+++ b/mypy/options.py
@@ -57,6 +57,9 @@ def __init__(self) -> None:
         # Warn about casting an expression to its inferred type
         self.warn_redundant_casts = False
 
+        # Warn about falling off the end of a function returning non-None
+        self.warn_no_return = False
+
         # Warn about unused '# type: ignore' comments
         self.warn_unused_ignores = False
 
diff --git a/test-data/unit/check-warnings.test b/test-data/unit/check-warnings.test
index 7b430b4dbd48..587de0895a79 100644
--- a/test-data/unit/check-warnings.test
+++ b/test-data/unit/check-warnings.test
@@ -56,3 +56,73 @@ pass
 [out]
 main:3: note: unused 'type: ignore' comment
 main:4: note: unused 'type: ignore' comment
+
+
+-- No return
+-- ---------
+
+[case testNoReturn]
+# flags: --warn-no-return
+def f() -> int:
+    pass
+
+def g() -> int:
+    if bool():
+        return 1
+[builtins fixtures/list.pyi]
+[out]
+main: note: In function "g":
+main:5: note: Missing return statement
+
+[case testNoReturnWhile]
+# flags: --warn-no-return
+def h() -> int:
+    while True:
+        if bool():
+            return 1
+
+def i() -> int:
+    while 1:
+        if bool():
+            return 1
+        if bool():
+            break
+
+def j() -> int:
+    while 1:
+        if bool():
+            return 1
+        if bool():
+            continue
+[builtins fixtures/list.pyi]
+[out]
+main: note: In function "i":
+main:7: note: Missing return statement
+
+[case testNoReturnExcept]
+# flags: --warn-no-return
+def f() -> int:
+    try:
+        return 1
+    except:
+        pass
+def g() -> int:
+    try:
+        pass
+    except:
+        return 1
+    else:
+        return 1
+def h() -> int:
+    try:
+        pass
+    except:
+        pass
+    else:
+        pass
+    finally:
+        return 1
+[builtins fixtures/exception.pyi]
+[out]
+main: note: In function "f":
+main:2: note: Missing return statement

From a6c2119bd47eb5f78a01a5fd417799ea51908a85 Mon Sep 17 00:00:00 2001
From: Reid Barton <rbarton@dropbox.com>
Date: Thu, 30 Jun 2016 17:47:28 -0700
Subject: [PATCH 10/13] Skip docstring when determining whether function body
 is trivial

---
 mypy/checker.py                    | 11 +++++++++--
 test-data/unit/check-warnings.test |  7 +++++++
 2 files changed, 16 insertions(+), 2 deletions(-)

diff --git a/mypy/checker.py b/mypy/checker.py
index 37767f39bbd7..73a0f91362f9 100644
--- a/mypy/checker.py
+++ b/mypy/checker.py
@@ -629,9 +629,16 @@ def is_implicit_any(t: Type) -> bool:
             self.binder = old_binder
 
     def is_trivial_body(self, block: Block) -> bool:
-        if len(block.body) != 1:
+        body = block.body
+
+        # Skip a docstring
+        if (isinstance(body[0], ExpressionStmt) and
+                isinstance(body[0].expr, StrExpr)):
+            body = block.body[1:]
+
+        if len(body) != 1:
             return False
-        stmt = block.body[0]
+        stmt = body[0]
         return (isinstance(stmt, PassStmt) or
                 (isinstance(stmt, ExpressionStmt) and
                  isinstance(stmt.expr, EllipsisExpr)))
diff --git a/test-data/unit/check-warnings.test b/test-data/unit/check-warnings.test
index 587de0895a79..b537deece415 100644
--- a/test-data/unit/check-warnings.test
+++ b/test-data/unit/check-warnings.test
@@ -126,3 +126,10 @@ def h() -> int:
 [out]
 main: note: In function "f":
 main:2: note: Missing return statement
+
+[case testNoReturnEmptyBodyWithDocstring]
+def f() -> int:
+    """Return the number of peppers."""
+    # This might be an @abstractmethod, for example
+    pass
+[out]

From 6fbddbaa6ff84692664baf319702b8a0b6119d1e Mon Sep 17 00:00:00 2001
From: Reid Barton <rbarton@dropbox.com>
Date: Fri, 1 Jul 2016 09:00:03 -0700
Subject: [PATCH 11/13] Remove None return values from check_return_stmt

---
 mypy/checker.py | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/mypy/checker.py b/mypy/checker.py
index 73a0f91362f9..320425c3dceb 100644
--- a/mypy/checker.py
+++ b/mypy/checker.py
@@ -1503,13 +1503,13 @@ def check_return_stmt(self, s: ReturnStmt) -> None:
                 typ = self.accept(s.expr, return_type)
                 # Returning a value of type Any is always fine.
                 if isinstance(typ, AnyType):
-                    return None
+                    return
 
                 if self.is_unusable_type(return_type):
                     # Lambdas are allowed to have a unusable returns.
                     # Functions returning a value of type None are allowed to have a Void return.
                     if isinstance(self.function_stack[-1], FuncExpr) or isinstance(typ, NoneTyp):
-                        return None
+                        return
                     self.fail(messages.NO_RETURN_VALUE_EXPECTED, s)
                 else:
                     self.check_subtype(
@@ -1522,10 +1522,10 @@ def check_return_stmt(self, s: ReturnStmt) -> None:
             else:
                 # Empty returns are valid in Generators with Any typed returns.
                 if (self.function_stack[-1].is_generator and isinstance(return_type, AnyType)):
-                    return None
+                    return
 
                 if isinstance(return_type, (Void, NoneTyp, AnyType)):
-                    return None
+                    return
 
                 if self.in_checked_function():
                     self.fail(messages.RETURN_VALUE_EXPECTED, s)

From 0af223635dd16a2d3740383a64b1012fc415f499 Mon Sep 17 00:00:00 2001
From: Reid Barton <rbarton@dropbox.com>
Date: Fri, 1 Jul 2016 11:12:56 -0700
Subject: [PATCH 12/13] Explain why two try frames are needed for a finally
 clause; add a test

---
 mypy/checker.py                      |  7 ++++++-
 test-data/unit/check-isinstance.test | 16 ++++++++++++++++
 2 files changed, 22 insertions(+), 1 deletion(-)

diff --git a/mypy/checker.py b/mypy/checker.py
index 320425c3dceb..0abf51c44775 100644
--- a/mypy/checker.py
+++ b/mypy/checker.py
@@ -1643,10 +1643,15 @@ def visit_try_stmt(self, s: TryStmt) -> Type:
         # (by exception, return, break, etc.)
         with self.binder.frame_context(can_skip=False, fall_through=0):
             if s.finally_body:
+                # Not only might the body of the try statement exit abnormally,
+                # but so might an exception handler or else clause. The finally
+                # clause runs in *all* cases, so we need an outer try frame to
+                # catch all intermediate states in case an exception is raised
+                # during an except or else clause.
                 self.binder.try_frames.add(len(self.binder.frames) - 1)
                 self.visit_try_without_finally(s)
                 self.binder.try_frames.remove(len(self.binder.frames) - 1)
-                # First we check finally_body is type safe for all intermediate frames
+                # First we check finally_body is type safe on all abnormal exit paths
                 self.accept(s.finally_body)
             else:
                 self.visit_try_without_finally(s)
diff --git a/test-data/unit/check-isinstance.test b/test-data/unit/check-isinstance.test
index e222b11b6222..650e2acb9966 100644
--- a/test-data/unit/check-isinstance.test
+++ b/test-data/unit/check-isinstance.test
@@ -352,6 +352,22 @@ while 2:
         break
         x.b
     x.b
+[case testUnionTryFinally6]
+class A: pass
+class B(A): b = 1
+
+def f() -> int:
+    x = B()  # type: A
+    try:
+        x = B()
+    except:
+        x = A()
+        # An exception could occur here
+        x = B()
+    finally:
+        return x.b # E: "A" has no attribute "b"
+[out]
+main: note: In function "f":
 [case testUnionListIsinstance]
 
 from typing import Union, List

From f20db903df7edc6f654a0ae168c88c653e3448e2 Mon Sep 17 00:00:00 2001
From: Reid Barton <rbarton@dropbox.com>
Date: Fri, 1 Jul 2016 11:42:06 -0700
Subject: [PATCH 13/13] Decouple checker and binder by adding more options to
 frame_context

No more poking around by the checker in loop_frames and try_frames.
---
 mypy/binder.py  | 48 +++++++++++++++++++++++++++++++++++++++++-------
 mypy/checker.py | 38 +++++++++++++++-----------------------
 2 files changed, 56 insertions(+), 30 deletions(-)

diff --git a/mypy/binder.py b/mypy/binder.py
index 64fc6e9364ef..23be259e82cf 100644
--- a/mypy/binder.py
+++ b/mypy/binder.py
@@ -73,7 +73,8 @@ def __init__(self) -> None:
         self.last_pop_changed = False
 
         self.try_frames = set()  # type: Set[int]
-        self.loop_frames = []  # type: List[int]
+        self.break_frames = []  # type: List[int]
+        self.continue_frames = []  # type: List[int]
 
     def _add_dependencies(self, key: Key, value: Key = None) -> None:
         if value is None:
@@ -266,14 +267,18 @@ def allow_jump(self, index: int) -> None:
                 frame.unreachable = True
         self.options_on_return[index].append(frame)
 
-    def push_loop_frame(self) -> None:
-        self.loop_frames.append(len(self.frames) - 1)
+    def handle_break(self) -> None:
+        self.allow_jump(self.break_frames[-1])
+        self.unreachable()
 
-    def pop_loop_frame(self) -> None:
-        self.loop_frames.pop()
+    def handle_continue(self) -> None:
+        self.allow_jump(self.continue_frames[-1])
+        self.unreachable()
 
     @contextmanager
-    def frame_context(self, *, can_skip: bool, fall_through: int = 1) -> Iterator[Frame]:
+    def frame_context(self, *, can_skip: bool, fall_through: int = 1,
+                      break_frame: int = 0, continue_frame: int = 0,
+                      try_frame: bool = False) -> Iterator[Frame]:
         """Return a context manager that pushes/pops frames on enter/exit.
 
         If can_skip is True, control flow is allowed to bypass the
@@ -284,14 +289,43 @@ def frame_context(self, *, can_skip: bool, fall_through: int = 1) -> Iterator[Fr
         `fall_through` levels higher. Otherwise control flow ends
         at the end of the frame.
 
+        If break_frame > 0, then 'break' statements within this frame
+        will jump out to the frame break_frame levels higher than the
+        frame created by this call to frame_context. Similarly for
+        continue_frame and 'continue' statements.
+
+        If try_frame is true, then execution is allowed to jump at any
+        point within the newly created frame (or its descendents) to
+        its parent (i.e., to the frame that was on top before this
+        call to frame_context).
+
         After the context manager exits, self.last_pop_changed indicates
         whether any types changed in the newly-topmost frame as a result
         of popping this frame.
         """
         assert len(self.frames) > 1
-        yield self.push_frame()
+
+        if break_frame:
+            self.break_frames.append(len(self.frames) - break_frame)
+        if continue_frame:
+            self.continue_frames.append(len(self.frames) - continue_frame)
+        if try_frame:
+            self.try_frames.add(len(self.frames) - 1)
+
+        new_frame = self.push_frame()
+        if try_frame:
+            # An exception may occur immediately
+            self.allow_jump(-1)
+        yield new_frame
         self.pop_frame(can_skip, fall_through)
 
+        if break_frame:
+            self.break_frames.pop()
+        if continue_frame:
+            self.continue_frames.pop()
+        if try_frame:
+            self.try_frames.remove(len(self.frames) - 1)
+
     @contextmanager
     def top_frame_context(self) -> Iterator[Frame]:
         """A variant of frame_context for use at the top level of
diff --git a/mypy/checker.py b/mypy/checker.py
index 0abf51c44775..6a0a987ad783 100644
--- a/mypy/checker.py
+++ b/mypy/checker.py
@@ -236,13 +236,12 @@ def accept_loop(self, body: Statement, else_body: Statement = None, *,
         """
         # The outer frame accumulates the results of all iterations
         with self.binder.frame_context(can_skip=False):
-            self.binder.push_loop_frame()
             while True:
-                with self.binder.frame_context(can_skip=True):
+                with self.binder.frame_context(can_skip=True,
+                                               break_frame=2, continue_frame=1):
                     self.accept(body)
                 if not self.binder.last_pop_changed:
                     break
-            self.binder.pop_loop_frame()
             if exit_condition:
                 _, else_map = self.find_isinstance_check(exit_condition)
                 self.push_type_map(else_map)
@@ -1642,19 +1641,17 @@ def visit_try_stmt(self, s: TryStmt) -> Type:
         # This one gets all possible states after the try block exited abnormally
         # (by exception, return, break, etc.)
         with self.binder.frame_context(can_skip=False, fall_through=0):
+            # Not only might the body of the try statement exit
+            # abnormally, but so might an exception handler or else
+            # clause. The finally clause runs in *all* cases, so we
+            # need an outer try frame to catch all intermediate states
+            # in case an exception is raised during an except or else
+            # clause. As an optimization, only create the outer try
+            # frame when there actually is a finally clause.
+            self.visit_try_without_finally(s, try_frame=bool(s.finally_body))
             if s.finally_body:
-                # Not only might the body of the try statement exit abnormally,
-                # but so might an exception handler or else clause. The finally
-                # clause runs in *all* cases, so we need an outer try frame to
-                # catch all intermediate states in case an exception is raised
-                # during an except or else clause.
-                self.binder.try_frames.add(len(self.binder.frames) - 1)
-                self.visit_try_without_finally(s)
-                self.binder.try_frames.remove(len(self.binder.frames) - 1)
                 # First we check finally_body is type safe on all abnormal exit paths
                 self.accept(s.finally_body)
-            else:
-                self.visit_try_without_finally(s)
 
         if s.finally_body:
             # Then we try again for the more restricted set of options
@@ -1672,7 +1669,7 @@ def visit_try_stmt(self, s: TryStmt) -> Type:
 
         return None
 
-    def visit_try_without_finally(self, s: TryStmt) -> None:
+    def visit_try_without_finally(self, s: TryStmt, try_frame: bool) -> None:
         """Type check a try statement, ignoring the finally block.
 
         On entry, the top frame should receive all flow that exits the
@@ -1683,15 +1680,12 @@ def visit_try_without_finally(self, s: TryStmt) -> None:
         # This frame will run the else block if the try fell through.
         # In that case, control flow continues to the parent of what
         # was the top frame on entry.
-        with self.binder.frame_context(can_skip=False, fall_through=2):
+        with self.binder.frame_context(can_skip=False, fall_through=2, try_frame=try_frame):
             # This frame receives exit via exception, and runs exception handlers
             with self.binder.frame_context(can_skip=False, fall_through=2):
                 # Finally, the body of the try statement
-                with self.binder.frame_context(can_skip=False, fall_through=2):
-                    self.binder.try_frames.add(len(self.binder.frames) - 2)
-                    self.binder.allow_jump(-1)
+                with self.binder.frame_context(can_skip=False, fall_through=2, try_frame=True):
                     self.accept(s.body)
-                    self.binder.try_frames.remove(len(self.binder.frames) - 2)
                 for i in range(len(s.handlers)):
                     with self.binder.frame_context(can_skip=True, fall_through=4):
                         if s.types[i]:
@@ -2022,13 +2016,11 @@ def visit_member_expr(self, e: MemberExpr) -> Type:
         return self.expr_checker.visit_member_expr(e)
 
     def visit_break_stmt(self, s: BreakStmt) -> Type:
-        self.binder.allow_jump(self.binder.loop_frames[-1] - 1)
-        self.binder.unreachable()
+        self.binder.handle_break()
         return None
 
     def visit_continue_stmt(self, s: ContinueStmt) -> Type:
-        self.binder.allow_jump(self.binder.loop_frames[-1])
-        self.binder.unreachable()
+        self.binder.handle_continue()
         return None
 
     def visit_int_expr(self, e: IntExpr) -> Type: