diff --git a/mypy/checkmember.py b/mypy/checkmember.py
index 14491f74b8ca..c06f23899754 100644
--- a/mypy/checkmember.py
+++ b/mypy/checkmember.py
@@ -9,7 +9,8 @@
 )
 from mypy.nodes import (
     TypeInfo, FuncBase, Var, FuncDef, SymbolNode, Context, MypyFile, TypeVarExpr,
-    ARG_POS, ARG_STAR, ARG_STAR2, Decorator, OverloadedFuncDef, TypeAlias, TempNode
+    ARG_POS, ARG_STAR, ARG_STAR2, Decorator, OverloadedFuncDef, TypeAlias, TempNode,
+    is_final_node
 )
 from mypy.messages import MessageBuilder
 from mypy.maptype import map_instance_to_supertype
@@ -895,8 +896,3 @@ def erase_to_bound(t: Type) -> Type:
         if isinstance(t.item, TypeVarType):
             return TypeType.make_normalized(t.item.upper_bound)
     return t
-
-
-def is_final_node(node: Optional[SymbolNode]) -> bool:
-    """Check whether `node` corresponds to a final attribute."""
-    return isinstance(node, (Var, FuncDef, OverloadedFuncDef, Decorator)) and node.is_final
diff --git a/mypy/main.py b/mypy/main.py
index ebd75c73e414..2696e5bbdfff 100644
--- a/mypy/main.py
+++ b/mypy/main.py
@@ -523,6 +523,10 @@ def add_invertible_flag(flag: str,
                         help="Suppress toplevel errors caused by missing annotations",
                         group=strictness_group)
 
+    add_invertible_flag('--allow-redefinition', default=False, strict_flag=False,
+                        help="Allow unconditional variable redefinition with a new type",
+                        group=strictness_group)
+
     incremental_group = parser.add_argument_group(
         title='Incremental mode',
         description="Adjust how mypy incrementally type checks and caches modules. "
diff --git a/mypy/messages.py b/mypy/messages.py
index 1cff185574c7..3512bd878cb6 100644
--- a/mypy/messages.py
+++ b/mypy/messages.py
@@ -29,6 +29,7 @@
     ReturnStmt, NameExpr, Var, CONTRAVARIANT, COVARIANT, SymbolNode,
     CallExpr
 )
+from mypy.util import unmangle
 from mypy import message_registry
 
 MYPY = False
@@ -952,7 +953,7 @@ def cant_assign_to_final(self, name: str, attr_assign: bool, ctx: Context) -> No
         Pass `attr_assign=True` if the assignment assigns to an attribute.
         """
         kind = "attribute" if attr_assign else "name"
-        self.fail('Cannot assign to final {} "{}"'.format(kind, name), ctx)
+        self.fail('Cannot assign to final {} "{}"'.format(kind, unmangle(name)), ctx)
 
     def protocol_members_cant_be_final(self, ctx: Context) -> None:
         self.fail("Protocol member cannot be final", ctx)
@@ -1064,7 +1065,7 @@ def unimported_type_becomes_any(self, prefix: str, typ: Type, ctx: Context) -> N
                   ctx)
 
     def need_annotation_for_var(self, node: SymbolNode, context: Context) -> None:
-        self.fail("Need type annotation for '{}'".format(node.name()), context)
+        self.fail("Need type annotation for '{}'".format(unmangle(node.name())), context)
 
     def explicit_any(self, ctx: Context) -> None:
         self.fail('Explicit "Any" is not allowed', ctx)
diff --git a/mypy/nodes.py b/mypy/nodes.py
index cf7cef74f9f8..1990440c00d0 100644
--- a/mypy/nodes.py
+++ b/mypy/nodes.py
@@ -924,15 +924,18 @@ def accept(self, visitor: StatementVisitor[T]) -> T:
 
 
 class AssignmentStmt(Statement):
-    """Assignment statement
+    """Assignment statement.
+
     The same node class is used for single assignment, multiple assignment
     (e.g. x, y = z) and chained assignment (e.g. x = y = z), assignments
-    that define new names, and assignments with explicit types (# type).
+    that define new names, and assignments with explicit types ("# type: t"
+    or "x: t [= ...]").
 
-    An lvalue can be NameExpr, TupleExpr, ListExpr, MemberExpr, IndexExpr.
+    An lvalue can be NameExpr, TupleExpr, ListExpr, MemberExpr, or IndexExpr.
     """
 
     lvalues = None  # type: List[Lvalue]
+    # This is a TempNode if and only if no rvalue (x: t).
     rvalue = None  # type: Expression
     # Declared type in a comment, may be None.
     type = None  # type: Optional[mypy.types.Type]
@@ -2968,3 +2971,8 @@ def is_class_var(expr: NameExpr) -> bool:
     if isinstance(expr.node, Var):
         return expr.node.is_classvar
     return False
+
+
+def is_final_node(node: Optional[SymbolNode]) -> bool:
+    """Check whether `node` corresponds to a final attribute."""
+    return isinstance(node, (Var, FuncDef, OverloadedFuncDef, Decorator)) and node.is_final
diff --git a/mypy/options.py b/mypy/options.py
index f36ef9190e04..f063cf444c83 100644
--- a/mypy/options.py
+++ b/mypy/options.py
@@ -21,6 +21,7 @@ class BuildType:
 PER_MODULE_OPTIONS = {
     # Please keep this list sorted
     "allow_untyped_globals",
+    "allow_redefinition",
     "always_false",
     "always_true",
     "check_untyped_defs",
@@ -149,6 +150,10 @@ def __init__(self) -> None:
         # Suppress toplevel errors caused by missing annotations
         self.allow_untyped_globals = False
 
+        # Allow variable to be redefined with an arbitrary type in the same block
+        # and the same nesting level as the initialization
+        self.allow_redefinition = False
+
         # Variable names considered True
         self.always_true = []  # type: List[str]
 
diff --git a/mypy/plugins/attrs.py b/mypy/plugins/attrs.py
index db222bd8be73..60fa4cdae698 100644
--- a/mypy/plugins/attrs.py
+++ b/mypy/plugins/attrs.py
@@ -19,6 +19,7 @@
     Overloaded, UnionType, FunctionLike
 )
 from mypy.typevars import fill_typevars
+from mypy.util import unmangle
 from mypy.server.trigger import make_wildcard_trigger
 
 MYPY = False
@@ -376,9 +377,10 @@ def _attribute_from_auto_attrib(ctx: 'mypy.plugin.ClassDefContext',
                                 rvalue: Expression,
                                 stmt: AssignmentStmt) -> Attribute:
     """Return an Attribute for a new type assignment."""
+    name = unmangle(lhs.name)
     # `x: int` (without equal sign) assigns rvalue to TempNode(AnyType())
     has_rhs = not isinstance(rvalue, TempNode)
-    return Attribute(lhs.name, ctx.cls.info, has_rhs, True, kw_only, Converter(), stmt)
+    return Attribute(name, ctx.cls.info, has_rhs, True, kw_only, Converter(), stmt)
 
 
 def _attribute_from_attrib_maker(ctx: 'mypy.plugin.ClassDefContext',
@@ -443,7 +445,8 @@ def _attribute_from_attrib_maker(ctx: 'mypy.plugin.ClassDefContext',
         converter = convert
     converter_info = _parse_converter(ctx, converter)
 
-    return Attribute(lhs.name, ctx.cls.info, attr_has_default, init, kw_only, converter_info, stmt)
+    name = unmangle(lhs.name)
+    return Attribute(name, ctx.cls.info, attr_has_default, init, kw_only, converter_info, stmt)
 
 
 def _parse_converter(ctx: 'mypy.plugin.ClassDefContext',
diff --git a/mypy/renaming.py b/mypy/renaming.py
new file mode 100644
index 000000000000..d348599e4166
--- /dev/null
+++ b/mypy/renaming.py
@@ -0,0 +1,384 @@
+from typing import Dict, List, Set
+
+from mypy.nodes import (
+    Block, AssignmentStmt, NameExpr, MypyFile, FuncDef, Lvalue, ListExpr, TupleExpr, TempNode,
+    WhileStmt, ForStmt, BreakStmt, ContinueStmt, TryStmt, WithStmt, StarExpr, ImportFrom,
+    MemberExpr, IndexExpr, Import, ClassDef
+)
+from mypy.traverser import TraverserVisitor
+
+MYPY = False
+if MYPY:
+    from typing_extensions import Final
+
+
+# Scope kinds
+FILE = 0  # type: Final
+FUNCTION = 1  # type: Final
+CLASS = 2  # type: Final
+
+
+class VariableRenameVisitor(TraverserVisitor):
+    """Rename variables to allow redefinition of variables.
+
+    For example, consider this code:
+
+      x = 0
+      f(x)
+
+      x = "a"
+      g(x)
+
+    It will be transformed like this:
+
+      x' = 0
+      f(x')
+
+      x = "a"
+      g(x)
+
+    There will be two independent variables (x' and x) that will have separate
+    inferred types. The publicly exposed variant will get the non-suffixed name.
+    This is the last definition at module top level and the first definition
+    (argument) within a function.
+
+    Renaming only happens for assignments within the same block. Renaming is
+    performed before semantic analysis, immediately after parsing.
+
+    The implementation performs a rudimentary static analysis. The analysis is
+    overly conservative to keep things simple.
+    """
+
+    def __init__(self) -> None:
+        # Counter for labeling new blocks
+        self.block_id = 0
+        # Number of surrounding try statements that disallow variable redefinition
+        self.disallow_redef_depth = 0
+        # Number of surrounding loop statements
+        self.loop_depth = 0
+        # Map block id to loop depth.
+        self.block_loop_depth = {}  # type: Dict[int, int]
+        # Stack of block ids being processed.
+        self.blocks = []  # type: List[int]
+        # List of scopes; each scope maps short (unqualified) name to block id.
+        self.var_blocks = []  # type: List[Dict[str, int]]
+
+        # References to variables that we may need to rename. List of
+        # scopes; each scope is a mapping from name to list of collections
+        # of names that refer to the same logical variable.
+        self.refs = []  # type: List[Dict[str, List[List[NameExpr]]]]
+        # Number of reads of the most recent definition of a variable (per scope)
+        self.num_reads = []  # type: List[Dict[str, int]]
+        # Kinds of nested scopes (FILE, FUNCTION or CLASS)
+        self.scope_kinds = []  # type: List[int]
+
+    def visit_mypy_file(self, file_node: MypyFile) -> None:
+        """Rename variables within a file.
+
+        This is the main entry point to this class.
+        """
+        self.clear()
+        self.enter_scope(FILE)
+        self.enter_block()
+
+        for d in file_node.defs:
+            d.accept(self)
+
+        self.leave_block()
+        self.leave_scope()
+
+    def visit_func_def(self, fdef: FuncDef) -> None:
+        # Conservatively do not allow variable defined before a function to
+        # be redefined later, since function could refer to either definition.
+        self.reject_redefinition_of_vars_in_scope()
+
+        self.enter_scope(FUNCTION)
+        self.enter_block()
+
+        for arg in fdef.arguments:
+            name = arg.variable.name()
+            # 'self' can't be redefined since it's special as it allows definition of
+            # attributes. 'cls' can't be used to define attributes so we can ignore it.
+            can_be_redefined = name != 'self'  # TODO: Proper check
+            self.record_assignment(arg.variable.name(), can_be_redefined)
+            self.handle_arg(name)
+
+        for stmt in fdef.body.body:
+            stmt.accept(self)
+
+        self.leave_block()
+        self.leave_scope()
+
+    def visit_class_def(self, cdef: ClassDef) -> None:
+        self.reject_redefinition_of_vars_in_scope()
+        self.enter_scope(CLASS)
+        super().visit_class_def(cdef)
+        self.leave_scope()
+
+    def visit_block(self, block: Block) -> None:
+        self.enter_block()
+        super().visit_block(block)
+        self.leave_block()
+
+    def visit_while_stmt(self, stmt: WhileStmt) -> None:
+        self.enter_loop()
+        super().visit_while_stmt(stmt)
+        self.leave_loop()
+
+    def visit_for_stmt(self, stmt: ForStmt) -> None:
+        stmt.expr.accept(self)
+        self.analyze_lvalue(stmt.index, True)
+        # Also analyze as non-lvalue so that every for loop index variable is assumed to be read.
+        stmt.index.accept(self)
+        self.enter_loop()
+        stmt.body.accept(self)
+        self.leave_loop()
+        if stmt.else_body:
+            stmt.else_body.accept(self)
+
+    def visit_break_stmt(self, stmt: BreakStmt) -> None:
+        self.reject_redefinition_of_vars_in_loop()
+
+    def visit_continue_stmt(self, stmt: ContinueStmt) -> None:
+        self.reject_redefinition_of_vars_in_loop()
+
+    def visit_try_stmt(self, stmt: TryStmt) -> None:
+        # Variables defined by a try statement get special treatment in the
+        # type checker which allows them to be always redefined, so no need to
+        # do renaming here.
+        self.enter_with_or_try()
+        super().visit_try_stmt(stmt)
+        self.leave_with_or_try()
+
+    def visit_with_stmt(self, stmt: WithStmt) -> None:
+        for expr in stmt.expr:
+            expr.accept(self)
+        for target in stmt.target:
+            if target is not None:
+                self.analyze_lvalue(target)
+        self.enter_with_or_try()
+        stmt.body.accept(self)
+        self.leave_with_or_try()
+
+    def visit_import(self, imp: Import) -> None:
+        for id, as_id in imp.ids:
+            self.record_assignment(as_id or id, False)
+
+    def visit_import_from(self, imp: ImportFrom) -> None:
+        for id, as_id in imp.names:
+            self.record_assignment(as_id or id, False)
+
+    def visit_assignment_stmt(self, s: AssignmentStmt) -> None:
+        s.rvalue.accept(self)
+        for lvalue in s.lvalues:
+            self.analyze_lvalue(lvalue)
+
+    def analyze_lvalue(self, lvalue: Lvalue, is_nested: bool = False) -> None:
+        """Process assignment; in particular, keep track of (re)defined names.
+
+        Args:
+            is_nested: True for non-outermost Lvalue in a multiple assignment such as
+                "x, y = ..."
+        """
+        if isinstance(lvalue, NameExpr):
+            name = lvalue.name
+            is_new = self.record_assignment(name, True)
+            if is_new:
+                self.handle_def(lvalue)
+            else:
+                self.handle_refine(lvalue)
+            if is_nested:
+                # This allows these to be redefined freely even if never read. Multiple
+                # assignment like "x, _ _ = y" defines dummy variables that are never read.
+                self.handle_ref(lvalue)
+        elif isinstance(lvalue, (ListExpr, TupleExpr)):
+            for item in lvalue.items:
+                self.analyze_lvalue(item, is_nested=True)
+        elif isinstance(lvalue, MemberExpr):
+            lvalue.expr.accept(self)
+        elif isinstance(lvalue, IndexExpr):
+            lvalue.base.accept(self)
+            lvalue.index.accept(self)
+        elif isinstance(lvalue, StarExpr):
+            # Propagate is_nested since in a typical use case like "x, *rest = ..." 'rest' may
+            # be freely reused.
+            self.analyze_lvalue(lvalue.expr, is_nested=is_nested)
+
+    def visit_name_expr(self, expr: NameExpr) -> None:
+        self.handle_ref(expr)
+
+    # Helpers for renaming references
+
+    def handle_arg(self, name: str) -> None:
+        """Store function argument."""
+        self.refs[-1][name] = [[]]
+        self.num_reads[-1][name] = 0
+
+    def handle_def(self, expr: NameExpr) -> None:
+        """Store new name definition."""
+        name = expr.name
+        names = self.refs[-1].setdefault(name, [])
+        names.append([expr])
+        self.num_reads[-1][name] = 0
+
+    def handle_refine(self, expr: NameExpr) -> None:
+        """Store assignment to an existing name (that replaces previous value, if any)."""
+        name = expr.name
+        if name in self.refs[-1]:
+            names = self.refs[-1][name]
+            if not names:
+                names.append([])
+            names[-1].append(expr)
+
+    def handle_ref(self, expr: NameExpr) -> None:
+        """Store reference to defined name."""
+        name = expr.name
+        if name in self.refs[-1]:
+            names = self.refs[-1][name]
+            if not names:
+                names.append([])
+            names[-1].append(expr)
+        num_reads = self.num_reads[-1]
+        num_reads[name] = num_reads.get(name, 0) + 1
+
+    def flush_refs(self) -> None:
+        """Rename all references within the current scope.
+
+        This will be called at the end of a scope.
+        """
+        is_func = self.scope_kinds[-1] == FUNCTION
+        for name, refs in self.refs[-1].items():
+            if len(refs) == 1:
+                # Only one definition -- no renaming neeed.
+                continue
+            if is_func:
+                # In a function, don't rename the first definition, as it
+                # may be an argument that must preserve the name.
+                to_rename = refs[1:]
+            else:
+                # At module top level, don't rename the final definition,
+                # as it will be publicly visible outside the module.
+                to_rename = refs[:-1]
+            for i, item in enumerate(to_rename):
+                self.rename_refs(item, i)
+        self.refs.pop()
+
+    def rename_refs(self, names: List[NameExpr], index: int) -> None:
+        name = names[0].name
+        new_name = name + "'" * (index + 1)
+        for expr in names:
+            expr.name = new_name
+
+    # Helpers for determining which assignments define new variables
+
+    def clear(self) -> None:
+        self.blocks = []
+        self.var_blocks = []
+
+    def enter_block(self) -> None:
+        self.block_id += 1
+        self.blocks.append(self.block_id)
+        self.block_loop_depth[self.block_id] = self.loop_depth
+
+    def leave_block(self) -> None:
+        self.blocks.pop()
+
+    def enter_with_or_try(self) -> None:
+        self.disallow_redef_depth += 1
+
+    def leave_with_or_try(self) -> None:
+        self.disallow_redef_depth -= 1
+
+    def enter_loop(self) -> None:
+        self.loop_depth += 1
+
+    def leave_loop(self) -> None:
+        self.loop_depth -= 1
+
+    def current_block(self) -> int:
+        return self.blocks[-1]
+
+    def enter_scope(self, kind: int) -> None:
+        self.var_blocks.append({})
+        self.refs.append({})
+        self.num_reads.append({})
+        self.scope_kinds.append(kind)
+
+    def leave_scope(self) -> None:
+        self.flush_refs()
+        self.var_blocks.pop()
+        self.num_reads.pop()
+        self.scope_kinds.pop()
+
+    def is_nested(self) -> int:
+        return len(self.var_blocks) > 1
+
+    def reject_redefinition_of_vars_in_scope(self) -> None:
+        """Make it impossible to redefine defined variables in the current scope.
+
+        This is used if we encounter a function definition that
+        can make it ambiguous which definition is live. Example:
+
+          x = 0
+
+          def f() -> int:
+              return x
+
+          x = ''  # Error -- cannot redefine x across function definition
+        """
+        var_blocks = self.var_blocks[-1]
+        for key in var_blocks:
+            var_blocks[key] = -1
+
+    def reject_redefinition_of_vars_in_loop(self) -> None:
+        """Reject redefinition of variables in the innermost loop.
+
+        If there is an early exit from a loop, there may be ambiguity about which
+        value may escpae the loop. Example where this matters:
+
+          while f():
+              x = 0
+              if g():
+                  break
+              x = ''  # Error -- not a redefinition
+          reveal_type(x)  # int
+
+        This method ensures that the second assignment to 'x' doesn't introduce a new
+        variable.
+        """
+        var_blocks = self.var_blocks[-1]
+        for key, block in var_blocks.items():
+            if self.block_loop_depth.get(block) == self.loop_depth:
+                var_blocks[key] = -1
+
+    def record_assignment(self, name: str, can_be_redefined: bool) -> bool:
+        """Record assignment to given name and return True if it defines a new variable.
+
+        Args:
+            can_be_redefined: If True, allows assignment in the same block to redefine
+                this name (if this is a new definition)
+        """
+        if self.num_reads[-1].get(name, -1) == 0:
+            # Only set, not read, so no reason to redefine
+            return False
+        if self.disallow_redef_depth > 0:
+            # Can't redefine within try/with a block.
+            can_be_redefined = False
+        block = self.current_block()
+        var_blocks = self.var_blocks[-1]
+        if name not in var_blocks:
+            # New definition in this scope.
+            if can_be_redefined:
+                # Store the block where this was defined to allow redefinition in
+                # the same block only.
+                var_blocks[name] = block
+            else:
+                # This doesn't support arbitrary redefinition.
+                var_blocks[name] = -1
+            return True
+        elif var_blocks[name] == block:
+            # Redefinition -- defines a new variable with the same name.
+            return True
+        else:
+            # Assigns to an existing variable.
+            return False
diff --git a/mypy/semanal.py b/mypy/semanal.py
index 12e7182c7681..bb2ef45a5531 100644
--- a/mypy/semanal.py
+++ b/mypy/semanal.py
@@ -56,7 +56,7 @@
     YieldExpr, ExecStmt, BackquoteExpr, ImportBase, AwaitExpr,
     IntExpr, FloatExpr, UnicodeExpr, TempNode, ImportedName, OverloadPart,
     COVARIANT, CONTRAVARIANT, INVARIANT, UNBOUND_IMPORTED, LITERAL_YES, nongen_builtins,
-    get_member_expr_fullname, REVEAL_TYPE, REVEAL_LOCALS
+    get_member_expr_fullname, REVEAL_TYPE, REVEAL_LOCALS, is_final_node
 )
 from mypy.tvar_scope import TypeVarScope
 from mypy.typevars import fill_typevars
@@ -83,7 +83,7 @@
     Plugin, ClassDefContext, SemanticAnalyzerPluginInterface,
     DynamicClassDefContext
 )
-from mypy.util import get_prefix, correct_relative_import
+from mypy.util import get_prefix, correct_relative_import, unmangle
 from mypy.semanal_shared import SemanticAnalyzerInterface, set_callable_name
 from mypy.scope import Scope
 from mypy.semanal_namedtuple import NamedTupleAnalyzer, NAMEDTUPLE_PROHIBITED_NAMES
@@ -369,6 +369,7 @@ def file_context(self, file_node: MypyFile, fnam: str, options: Options,
     def visit_func_def(self, defn: FuncDef) -> None:
         if not self.recurse_into_functions:
             return
+
         with self.scope.function_scope(defn):
             self._visit_func_def(defn)
 
@@ -1483,6 +1484,7 @@ def allow_patching(self, parent_mod: MypyFile, child: str) -> bool:
 
     def add_module_symbol(self, id: str, as_id: str, module_public: bool,
                           context: Context, module_hidden: bool = False) -> None:
+        """Add symbol that is a reference to a module object."""
         if id in self.modules:
             m = self.modules[id]
             kind = self.current_symbol_kind()
@@ -1750,11 +1752,11 @@ def add_type_alias_deps(self, aliases_used: Iterable[str],
         self.cur_mod_node.alias_deps[target].update(aliases_used)
 
     def visit_assignment_stmt(self, s: AssignmentStmt) -> None:
-        self.unwrap_final(s)
+        s.is_final_def = self.unwrap_final(s)
         self.analyze_lvalues(s)
+        s.rvalue.accept(self)
         self.check_final_implicit_def(s)
         self.check_classvar(s)
-        s.rvalue.accept(self)
         self.process_type_annotation(s)
         self.apply_dynamic_class_hook(s)
         self.check_and_set_up_type_alias(s)
@@ -1769,14 +1771,10 @@ def visit_assignment_stmt(self, s: AssignmentStmt) -> None:
         self.process__all__(s)
 
     def analyze_lvalues(self, s: AssignmentStmt) -> None:
-        def final_cb(keep_final: bool) -> None:
-            self.fail("Cannot redefine an existing name as final", s)
-            if not keep_final:
-                s.is_final_def = False
-
         for lval in s.lvalues:
-            self.analyze_lvalue(lval, explicit_type=s.type is not None,
-                                final_cb=final_cb if s.is_final_def else None)
+            self.analyze_lvalue(lval,
+                                explicit_type=s.type is not None,
+                                is_final=s.is_final_def)
 
     def apply_dynamic_class_hook(self, s: AssignmentStmt) -> None:
         if len(s.lvalues) > 1:
@@ -1793,15 +1791,19 @@ def apply_dynamic_class_hook(self, s: AssignmentStmt) -> None:
             if hook:
                 hook(DynamicClassDefContext(call, lval.name, self))
 
-    def unwrap_final(self, s: AssignmentStmt) -> None:
+    def unwrap_final(self, s: AssignmentStmt) -> bool:
         """Strip Final[...] if present in an assignment.
 
         This is done to invoke type inference during type checking phase for this
-        assignment. Also, Final[...] desn't affect type in any way, it is rather an
+        assignment. Also, Final[...] desn't affect type in any way -- it is rather an
         access qualifier for given `Var`.
+
+        Also perform various consistency checks.
+
+        Returns True if Final[...] was present.
         """
         if not s.type or not self.is_final_type(s.type):
-            return
+            return False
         assert isinstance(s.type, UnboundType)
         if len(s.type.args) > 1:
             self.fail("Final[...] takes at most one type argument", s.type)
@@ -1815,10 +1817,9 @@ def unwrap_final(self, s: AssignmentStmt) -> None:
             s.type = s.type.args[0]
         if len(s.lvalues) != 1 or not isinstance(s.lvalues[0], RefExpr):
             self.fail("Invalid final declaration", s)
-            return
+            return False
         lval = s.lvalues[0]
         assert isinstance(lval, RefExpr)
-        s.is_final_def = True
         if self.loop_depth > 0:
             self.fail("Cannot use Final inside a loop", s)
         if self.type and self.type.is_protocol:
@@ -1827,7 +1828,7 @@ def unwrap_final(self, s: AssignmentStmt) -> None:
                 not self.is_stub_file and not self.is_class_scope()):
             if not invalid_bare_final:  # Skip extra error messages.
                 self.msg.final_without_value(s)
-        return
+        return True
 
     def check_final_implicit_def(self, s: AssignmentStmt) -> None:
         """Do basic checks for final declaration on self in __init__.
@@ -2067,22 +2068,22 @@ def check_and_set_up_type_alias(self, s: AssignmentStmt) -> None:
     def analyze_lvalue(self, lval: Lvalue, nested: bool = False,
                        add_global: bool = False,
                        explicit_type: bool = False,
-                       final_cb: Optional[Callable[[bool], None]] = None) -> None:
+                       is_final: bool = False) -> None:
         """Analyze an lvalue or assignment target.
 
+        Note that this is used in both pass 1 and 2.
+
         Args:
             lval: The target lvalue
             nested: If true, the lvalue is within a tuple or list lvalue expression
             add_global: Add name to globals table only if this is true (used in first pass)
             explicit_type: Assignment has type annotation
-            final_cb: A callback to call in situation where a final declaration on `self`
-                overrides an existing name.
         """
         if isinstance(lval, NameExpr):
-            self.analyze_name_lvalue(lval, add_global, explicit_type, final_cb)
+            self.analyze_name_lvalue(lval, add_global, explicit_type, is_final)
         elif isinstance(lval, MemberExpr):
             if not add_global:
-                self.analyze_member_lvalue(lval, explicit_type, final_cb=final_cb)
+                self.analyze_member_lvalue(lval, explicit_type, is_final)
             if explicit_type and not self.is_self_member_ref(lval):
                 self.fail('Type cannot be declared in assignment to non-self '
                           'attribute', lval)
@@ -2108,11 +2109,17 @@ def analyze_name_lvalue(self,
                             lval: NameExpr,
                             add_global: bool,
                             explicit_type: bool,
-                            final_cb: Optional[Callable[[bool], None]]) -> None:
+                            is_final: bool) -> None:
         """Analyze an lvalue that targets a name expression.
 
         Arguments are similar to "analyze_lvalue".
         """
+        if self.is_alias_for_final_name(lval.name):
+            if is_final:
+                self.fail("Cannot redefine an existing name as final", lval)
+            else:
+                self.msg.cant_assign_to_final(lval.name, self.type is not None, lval)
+
         # Top-level definitions within some statements (at least while) are
         # not handled in the first pass, so they have to be added now.
         nested_global = (not self.is_func_scope() and
@@ -2128,23 +2135,61 @@ def analyze_name_lvalue(self,
                 # already in the first pass and added to the symbol table.
                 # An exception is typing module with incomplete test fixtures.
                 assert lval.node.name() in self.globals or self.cur_mod_id == 'typing'
+                # A previously defined name cannot be redefined as a final name even when
+                # using renaming.
+                if (is_final
+                        and self.is_mangled_global(lval.name)
+                        and not self.is_initial_mangled_global(lval.name)):
+                    self.fail("Cannot redefine an existing name as final", lval)
         elif (self.locals[-1] is not None and lval.name not in self.locals[-1] and
               lval.name not in self.global_decls[-1] and
               lval.name not in self.nonlocal_decls[-1]):
             # Define new local name.
             v = self.make_name_lvalue_var(lval, LDEF, not explicit_type)
             self.add_local(v, lval)
-            if lval.name == '_':
+            if unmangle(lval.name) == '_':
                 # Special case for assignment to local named '_': always infer 'Any'.
                 typ = AnyType(TypeOfAny.special_form)
                 self.store_declared_types(lval, typ)
         elif not self.is_func_scope() and (self.type and
                                            lval.name not in self.type.names):
             # Define a new attribute within class body.
+            if is_final and unmangle(lval.name) + "'" in self.type.names:
+                self.fail("Cannot redefine an existing name as final", lval)
             v = self.make_name_lvalue_var(lval, MDEF, not explicit_type)
             self.type.names[lval.name] = SymbolTableNode(MDEF, v)
         else:
-            self.make_name_lvalue_point_to_existing_def(lval, explicit_type, final_cb)
+            self.make_name_lvalue_point_to_existing_def(lval, explicit_type, is_final)
+
+    def is_mangled_global(self, name: str) -> bool:
+        # A global is mangled if there exists at least one renamed variant.
+        return unmangle(name) + "'" in self.globals
+
+    def is_initial_mangled_global(self, name: str) -> bool:
+        # If there are renamed definitions for a global, the first one has exactly one prime.
+        return name == unmangle(name) + "'"
+
+    def is_alias_for_final_name(self, name: str) -> bool:
+        if self.is_func_scope():
+            if not name.endswith("'"):
+                # Not a mangled name -- can't be an alias
+                return False
+            name = unmangle(name)
+            assert self.locals[-1] is not None, "No locals at function scope"
+            existing = self.locals[-1].get(name)
+            return existing is not None and is_final_node(existing.node)
+        elif self.type is not None:
+            orig_name = unmangle(name) + "'"
+            if name == orig_name:
+                return False
+            existing = self.type.names.get(orig_name)
+            return existing is not None and is_final_node(existing.node)
+        else:
+            orig_name = unmangle(name) + "'"
+            if name == orig_name:
+                return False
+            existing = self.globals.get(orig_name)
+            return existing is not None and is_final_node(existing.node)
 
     def make_name_lvalue_var(self, lvalue: NameExpr, kind: int, inferred: bool) -> Var:
         """Return a Var node for an lvalue that is a name expression."""
@@ -2173,7 +2218,11 @@ def make_name_lvalue_point_to_existing_def(
             self,
             lval: NameExpr,
             explicit_type: bool,
-            final_cb: Optional[Callable[[bool], None]]) -> None:
+            is_final: bool) -> None:
+        """Update an lvalue to point to existing definition in the same scope.
+
+        Arguments are similar to "analyze_lvalue".
+        """
         # Assume that an existing name exists. Try to find the original definition.
         global_def = self.globals.get(lval.name)
         if self.locals:
@@ -2189,12 +2238,8 @@ def make_name_lvalue_point_to_existing_def(
         original_def = global_def or local_def or type_def
 
         # Redefining an existing name with final is always an error.
-        if final_cb is not None:
-            # We avoid extra errors if the original definition is also final
-            # by keeping the final status of this assignment.
-            keep_final = bool(original_def and isinstance(original_def.node, Var) and
-                              original_def.node.is_final)
-            final_cb(keep_final)
+        if is_final:
+            self.fail("Cannot redefine an existing name as final", lval)
         if explicit_type:
             # Don't re-bind types
             self.name_already_defined(lval.name, lval, original_def)
@@ -2219,30 +2264,28 @@ def analyze_tuple_or_list_lvalue(self, lval: TupleExpr,
                 self.analyze_lvalue(i, nested=True, add_global=add_global,
                                     explicit_type=explicit_type)
 
-    def analyze_member_lvalue(self, lval: MemberExpr, explicit_type: bool = False,
-                              final_cb: Optional[Callable[[bool], None]] = None) -> None:
+    def analyze_member_lvalue(self, lval: MemberExpr, explicit_type: bool, is_final: bool) -> None:
         """Analyze lvalue that is a member expression.
 
         Arguments:
             lval: The target lvalue
             explicit_type: Assignment has type annotation
-            final_cb: A callback to call in situation where a final declaration on `self`
-                overrides an existing name.
+            is_final: Is the target final
         """
         lval.accept(self)
         if self.is_self_member_ref(lval):
             assert self.type, "Self member outside a class"
             cur_node = self.type.names.get(lval.name, None)
             node = self.type.get(lval.name)
-            if cur_node and final_cb is not None:
+            if cur_node and is_final:
                 # Overrides will be checked in type checker.
-                final_cb(False)
+                self.fail("Cannot redefine an existing name as final", lval)
             # If the attribute of self is not defined in superclasses, create a new Var, ...
             if ((node is None or isinstance(node.node, Var) and node.node.is_abstract_var) or
                     # ... also an explicit declaration on self also creates a new Var.
                     # Note that `explicit_type` might has been erased for bare `Final`,
                     # so we also check if `final_cb` is passed.
-                    (cur_node is None and (explicit_type or final_cb is not None))):
+                    (cur_node is None and (explicit_type or is_final))):
                 if self.type.is_protocol and node is None:
                     self.fail("Protocol members cannot be defined via assignment to self", lval)
                 else:
@@ -2367,6 +2410,7 @@ def process_typevar_declaration(self, s: AssignmentStmt) -> None:
         node.node = type_var
 
     def check_typevar_name(self, call: CallExpr, name: str, context: Context) -> bool:
+        name = unmangle(name)
         if len(call.args) < 1:
             self.fail("Too few arguments for TypeVar()", context)
             return False
@@ -2502,6 +2546,7 @@ def parse_bool(self, expr: Expression) -> Optional[bool]:
         return None
 
     def check_classvar(self, s: AssignmentStmt) -> None:
+        """Check if assignment defines a class variable."""
         lvalue = s.lvalues[0]
         if len(s.lvalues) != 1 or not isinstance(lvalue, RefExpr):
             return
@@ -3612,6 +3657,7 @@ def current_symbol_kind(self) -> int:
 
     def add_symbol(self, name: str, node: SymbolTableNode,
                    context: Context) -> None:
+        """Add symbol to the currently active symbol table."""
         # NOTE: This logic mostly parallels SemanticAnalyzerPass1.add_symbol. If you change
         #     this, you may have to change the other method as well.
         # TODO: Combine these methods in the first and second pass into a single one.
@@ -3648,6 +3694,7 @@ def add_symbol(self, name: str, node: SymbolTableNode,
             self.globals[name] = node
 
     def add_local(self, node: Union[Var, FuncDef, OverloadedFuncDef], ctx: Context) -> None:
+        """Add local variable or function."""
         assert self.locals[-1] is not None, "Should not add locals outside a function"
         name = node.name()
         if name in self.locals[-1]:
@@ -3702,7 +3749,7 @@ def name_already_defined(self, name: str, ctx: Context,
             extra_msg = ' on line {}'.format(node.line)
         else:
             extra_msg = ' (possibly by an import)'
-        self.fail("Name '{}' already defined{}".format(name, extra_msg), ctx)
+        self.fail("Name '{}' already defined{}".format(unmangle(name), extra_msg), ctx)
 
     def fail(self, msg: str, ctx: Context, serious: bool = False, *,
              blocker: bool = False) -> None:
diff --git a/mypy/semanal_pass1.py b/mypy/semanal_pass1.py
index 871e179720f1..8e659beb172a 100644
--- a/mypy/semanal_pass1.py
+++ b/mypy/semanal_pass1.py
@@ -14,7 +14,8 @@
 bind names, which only happens in pass 2.
 
 This pass also infers the reachability of certain if statements, such as
-those with platform checks.
+those with platform checks. This lets us filter out unreachable imports
+at an early stage.
 """
 
 from typing import List, Tuple
@@ -33,6 +34,7 @@
 from mypy.options import Options
 from mypy.sametypes import is_same_type
 from mypy.visitor import NodeVisitor
+from mypy.renaming import VariableRenameVisitor
 
 
 class SemanticAnalyzerPass1(NodeVisitor[None]):
@@ -60,6 +62,9 @@ def visit_file(self, file: MypyFile, fnam: str, mod_id: str, options: Options) -
         and these will get resolved in later phases of semantic
         analysis.
         """
+        if options.allow_redefinition:
+            # Perform renaming across the AST to allow variable redefinitions
+            file.accept(VariableRenameVisitor())
         sem = self.sem
         self.sem.options = options  # Needed because we sometimes call into it
         self.pyversion = options.python_version
diff --git a/mypy/test/testcheck.py b/mypy/test/testcheck.py
index 7f8de5bbbb3e..eb7729c2106e 100644
--- a/mypy/test/testcheck.py
+++ b/mypy/test/testcheck.py
@@ -80,6 +80,7 @@
     'check-ctypes.test',
     'check-dataclasses.test',
     'check-final.test',
+    'check-redefine.test',
     'check-literal.test',
 ]
 
diff --git a/mypy/test/testsemanal.py b/mypy/test/testsemanal.py
index 096bdd4dacb2..e42a84e8365b 100644
--- a/mypy/test/testsemanal.py
+++ b/mypy/test/testsemanal.py
@@ -8,7 +8,7 @@
 from mypy.modulefinder import BuildSource
 from mypy.defaults import PYTHON3_VERSION
 from mypy.test.helpers import (
-    assert_string_arrays_equal, normalize_error_messages, testfile_pyversion,
+    assert_string_arrays_equal, normalize_error_messages, testfile_pyversion, parse_options
 )
 from mypy.test.data import DataDrivenTestCase, DataSuite
 from mypy.test.config import test_temp_dir
@@ -35,8 +35,8 @@
                  'semanal-python2.test']
 
 
-def get_semanal_options() -> Options:
-    options = Options()
+def get_semanal_options(program_text: str, testcase: DataDrivenTestCase) -> Options:
+    options = parse_options(program_text, testcase, 1)
     options.use_builtins_fixtures = True
     options.semantic_analysis_only = True
     options.show_traceback = True
@@ -61,7 +61,7 @@ def test_semanal(testcase: DataDrivenTestCase) -> None:
 
     try:
         src = '\n'.join(testcase.input)
-        options = get_semanal_options()
+        options = get_semanal_options(src, testcase)
         options.python_version = testfile_pyversion(testcase.file)
         result = build.build(sources=[BuildSource('main', None, src)],
                              options=options,
@@ -112,7 +112,7 @@ def test_semanal_error(testcase: DataDrivenTestCase) -> None:
     try:
         src = '\n'.join(testcase.input)
         res = build.build(sources=[BuildSource('main', None, src)],
-                          options=get_semanal_options(),
+                          options=get_semanal_options(src, testcase),
                           alt_lib_path=test_temp_dir)
         a = res.errors
         assert a, 'No errors reported in {}, line {}'.format(testcase.file, testcase.line)
@@ -139,7 +139,7 @@ def run_case(self, testcase: DataDrivenTestCase) -> None:
             # Build test case input.
             src = '\n'.join(testcase.input)
             result = build.build(sources=[BuildSource('main', None, src)],
-                                 options=get_semanal_options(),
+                                 options=get_semanal_options(src, testcase),
                                  alt_lib_path=test_temp_dir)
             # The output is the symbol table converted into a string.
             a = result.errors
@@ -169,7 +169,7 @@ def run_case(self, testcase: DataDrivenTestCase) -> None:
             # Build test case input.
             src = '\n'.join(testcase.input)
             result = build.build(sources=[BuildSource('main', None, src)],
-                                 options=get_semanal_options(),
+                                 options=get_semanal_options(src, testcase),
                                  alt_lib_path=test_temp_dir)
             a = result.errors
             if a:
diff --git a/mypy/test/testtransform.py b/mypy/test/testtransform.py
index b4703f1906ac..014d0c17ceaf 100644
--- a/mypy/test/testtransform.py
+++ b/mypy/test/testtransform.py
@@ -5,7 +5,7 @@
 from mypy import build
 from mypy.modulefinder import BuildSource
 from mypy.test.helpers import (
-    assert_string_arrays_equal, testfile_pyversion, normalize_error_messages
+    assert_string_arrays_equal, testfile_pyversion, normalize_error_messages, parse_options
 )
 from mypy.test.data import DataDrivenTestCase, DataSuite
 from mypy.test.config import test_temp_dir
@@ -36,11 +36,10 @@ def test_transform(testcase: DataDrivenTestCase) -> None:
 
     try:
         src = '\n'.join(testcase.input)
-        options = Options()
+        options = parse_options(src, testcase, 1)
         options.use_builtins_fixtures = True
         options.semantic_analysis_only = True
         options.show_traceback = True
-        options.python_version = testfile_pyversion(testcase.file)
         result = build.build(sources=[BuildSource('main', None, src)],
                              options=options,
                              alt_lib_path=test_temp_dir)
diff --git a/mypy/util.py b/mypy/util.py
index 8c83eaac9a9e..df054814df4e 100644
--- a/mypy/util.py
+++ b/mypy/util.py
@@ -254,6 +254,11 @@ def hard_exit(status: int = 0) -> None:
     os._exit(status)
 
 
+def unmangle(name: str) -> str:
+    """Remove internal suffixes from a short name."""
+    return name.rstrip("'")
+
+
 # The following is a backport of stream redirect utilities from Lib/contextlib.py
 # We need this for 3.4 support. They can be removed in March 2019!
 
diff --git a/test-data/unit/check-final.test b/test-data/unit/check-final.test
index 7f895b97d277..be17b1da1333 100644
--- a/test-data/unit/check-final.test
+++ b/test-data/unit/check-final.test
@@ -336,14 +336,15 @@ class C:
 -- Reassignments
 
 [case testFinalReassignModuleVar]
+# flags: --allow-redefinition
 from typing import Final
 
 x: Final = 1
-x  # Dummy reference to allow renaming once implemented
+x
 x = 2  # E: Cannot assign to final name "x"
 def f() -> int:
     global x
-    x = 3  # E: Cannot assign to final name "x"
+    x = 3  # No error here is okay since we reported an error above
     return x
 
 x2: Final = 1
@@ -353,13 +354,58 @@ def f2() -> None:
     x2 = 1  # E: Cannot assign to final name "x2"
 
 y = 1
-y  # Dummy reference to allow renaming once implemented
-y: Final = 2  # E: Name 'y' already defined on line 17 \
+y
+y: Final = 2  # E: Cannot redefine an existing name as final
+y = 3  # E: Cannot assign to final name "y"
+
+z: Final = 1
+z: Final = 2  # E: Name 'z' already defined on line 23 \
+              # E: Cannot redefine an existing name as final
+z = 3  # E: Cannot assign to final name "z"
+
+[case testFinalReassignModuleVar2]
+# flags: --allow-redefinition
+from typing import Final
+
+x: Final = 1
+x
+def f() -> int:
+    global x
+    x = 3  # E: Cannot assign to final name "x"
+    return x
+
+y = 1
+y
+y = 2
+y
+y: Final = 3  # E: Cannot redefine an existing name as final
+
+[case testFinalReassignModuleVar3]
+# flags: --disallow-redefinition
+from typing import Final
+
+x: Final = 1
+x
+x = 2  # E: Cannot assign to final name "x"
+def f() -> int:
+    global x
+    x = 3  # E: Cannot assign to final name "x"
+    return x
+
+x2: Final = 1
+x2
+def f2() -> None:
+    global x2
+    x2 = 1  # E: Cannot assign to final name "x2"
+
+y = 1 # E: Cannot assign to final name "y"
+y
+y: Final = 2  # E: Name 'y' already defined on line 18 \
               # E: Cannot redefine an existing name as final
-y = 3  # No error here, first definition wins
+y = 3  # E: Cannot assign to final name "y"
 
 z: Final = 1
-z: Final = 2  # E: Name 'z' already defined on line 22 \
+z: Final = 2  # E: Name 'z' already defined on line 23 \
               # E: Cannot redefine an existing name as final
 z = 3  # E: Cannot assign to final name "z"
 
@@ -421,7 +467,7 @@ class C:
     x: Final = 1
     x = 2  # E: Cannot assign to final name "x"
 
-    y = 1
+    y = 1  # E: Cannot assign to final name "y"
     y: Final = 2  # E: Cannot redefine an existing name as final
 [out]
 
diff --git a/test-data/unit/check-inference.test b/test-data/unit/check-inference.test
index 1b636e173384..84339aca5629 100644
--- a/test-data/unit/check-inference.test
+++ b/test-data/unit/check-inference.test
@@ -1045,6 +1045,27 @@ class B: pass
 [builtins fixtures/for.pyi]
 
 [case testReusingInferredForIndex2]
+# flags: --allow-redefinition
+
+def f() -> None:
+    for a in [A()]: pass
+    a = A()
+    a
+    if int():
+        a = B() \
+            # E: Incompatible types in assignment (expression has type "B", variable has type "A")
+    for a in []: pass # E: Need type annotation for 'a'
+    a = A()
+    if int():
+        a = B() \
+            # E: Incompatible types in assignment (expression has type "B", variable has type "A")
+class A: pass
+class B: pass
+[builtins fixtures/for.pyi]
+[out]
+
+[case testReusingInferredForIndex3]
+# flags: --disallow-redefinition
 def f() -> None:
     for a in [A()]: pass
     a = A()
@@ -2434,9 +2455,18 @@ _ = 0
 _ = '' # E: Incompatible types in assignment (expression has type "str", variable has type "int")
 
 [case testUnusedTargetNotClass]
+# flags: --allow-redefinition
 class C:
-    _ = 0
+    _, _ = 0, 0
+    _ = ''
+reveal_type(C._) # E: Revealed type is 'builtins.str'
+
+[case testUnusedTargetNotClass2]
+# flags: --disallow-redefinition
+class C:
+    _, _ = 0, 0
     _ = ''  # E: Incompatible types in assignment (expression has type "str", variable has type "int")
+reveal_type(C._) # E: Revealed type is 'builtins.int'
 
 [case testUnusedTargetTupleUnpacking]
 def foo() -> None:
diff --git a/test-data/unit/check-redefine.test b/test-data/unit/check-redefine.test
new file mode 100644
index 000000000000..eef95ccf9154
--- /dev/null
+++ b/test-data/unit/check-redefine.test
@@ -0,0 +1,476 @@
+-- Test cases for the redefinition of variable with a different type.
+
+
+-- Redefine local variable
+-- -----------------------
+
+
+[case testRedefineLocalWithDifferentType]
+# flags: --allow-redefinition
+def f() -> None:
+    x = 0
+    reveal_type(x) # E: Revealed type is 'builtins.int'
+    x = ''
+    reveal_type(x) # E: Revealed type is 'builtins.str'
+
+[case testCannotConditionallyRedefineLocalWithDifferentType]
+# flags: --allow-redefinition
+def f() -> None:
+    y = 0
+    reveal_type(y) # E: Revealed type is 'builtins.int'
+    if int():
+        y = ''  \
+        # E: Incompatible types in assignment (expression has type "str", variable has type "int")
+        reveal_type(y)  # E: Revealed type is 'builtins.int'
+    reveal_type(y) # E: Revealed type is 'builtins.int'
+
+[case testRedefineFunctionArg]
+# flags: --allow-redefinition
+def f(x: int) -> None:
+    g(x)
+    x = ''
+    reveal_type(x) # E: Revealed type is 'builtins.str'
+def g(x: int) -> None:
+    if int():
+        x = '' # E: Incompatible types in assignment (expression has type "str", variable has type "int")
+        reveal_type(x) # E: Revealed type is 'builtins.int'
+
+[case testRedefineAnnotationOnly]
+# flags: --allow-redefinition
+def f() -> None:
+    x: int
+    x = '' \
+        # E: Incompatible types in assignment (expression has type "str", variable has type "int")
+    reveal_type(x) # E: Revealed type is 'builtins.int'
+def g() -> None:
+    x: int
+    x = 1
+    reveal_type(x) # E: Revealed type is 'builtins.int'
+    x = ''
+    reveal_type(x) # E: Revealed type is 'builtins.str'
+
+[case testRedefineLocalUsingOldValue]
+# flags: --allow-redefinition
+from typing import TypeVar, Union
+
+T = TypeVar('T')
+
+def f(x: int) -> None:
+    x = g(x)
+    reveal_type(x)  # E: Revealed type is 'Union[builtins.int*, builtins.str]'
+    y = 1
+    y = g(y)
+    reveal_type(y)  # E: Revealed type is 'Union[builtins.int*, builtins.str]'
+
+def g(x: T) -> Union[T, str]: pass
+
+[case testRedefineLocalForLoopIndexVariable]
+# flags: --allow-redefinition
+from typing import Iterable
+def f(a: Iterable[int], b: Iterable[str]) -> None:
+    for x in a:
+        x = '' \
+        # E: Incompatible types in assignment (expression has type "str", variable has type "int")
+    reveal_type(x) # E: Revealed type is 'builtins.int*'
+    for x in b:
+        x = 1 \
+        # E: Incompatible types in assignment (expression has type "int", variable has type "str")
+    reveal_type(x) # E: Revealed type is 'builtins.str*'
+
+def g(a: Iterable[int]) -> None:
+    for x in a: pass
+    x = ''
+
+def h(a: Iterable[int]) -> None:
+    x = ''
+    reveal_type(x)  # E: Revealed type is 'builtins.str'
+    for x in a: pass
+
+[case testCannotRedefineLocalWithinTry]
+# flags: --allow-redefinition
+def f() -> None:
+    try:
+        x = 0
+        x
+        g()  # Might raise an exception
+        x = '' \
+        # E: Incompatible types in assignment (expression has type "str", variable has type "int")
+    except:
+        pass
+    reveal_type(x) # E: Revealed type is 'builtins.int'
+    y = 0
+    y
+    y = ''
+
+def g(): pass
+
+[case testCannotRedefineLocalWithinWith]
+# flags: --allow-redefinition
+def f() -> None:
+    with g():
+        x = 0
+        x
+        g()  # Might raise an exception
+        x = '' \
+        # E: Incompatible types in assignment (expression has type "str", variable has type "int")
+    reveal_type(x) # E: Revealed type is 'builtins.int'
+    y = 0
+    y
+    y = ''
+
+def g(): pass
+
+[case testCannotRedefineAcrossNestedFunction]
+# flags: --allow-redefinition
+def f() -> None:
+    x = 0
+    x
+    def g() -> None:
+        x
+    g()
+    x = '' \
+    # E: Incompatible types in assignment (expression has type "str", variable has type "int")
+    g()
+    y = 0
+    y
+    y = ''
+
+[case testCannotRedefineAcrossNestedDecoratedFunction]
+# flags: --allow-redefinition
+def dec(f): return f
+
+def f() -> None:
+    x = 0
+    x
+    @dec
+    def g() -> None:
+        x
+    g()
+    x = '' \
+    # E: Incompatible types in assignment (expression has type "str", variable has type "int")
+    g()
+    y = 0
+    y
+    y = ''
+
+[case testCannotRedefineAcrossNestedOverloadedFunction]
+# flags: --allow-redefinition
+from typing import overload
+
+def f() -> None:
+    x = 0
+    x
+    @overload
+    def g() -> None: pass
+    @overload
+    def g(x: int) -> None: pass
+    def g(x=0):
+        pass
+    g()
+    x = '' \
+    # E: Incompatible types in assignment (expression has type "str", variable has type "int")
+    g()
+    y = 0
+    y
+    y = ''
+
+[case testRedefineLocalInMultipleAssignment]
+# flags: --allow-redefinition
+def f() -> None:
+    x, x = 1, ''
+    reveal_type(x) # E: Revealed type is 'builtins.str'
+    x = object()
+    reveal_type(x) # E: Revealed type is 'builtins.object'
+
+def g() -> None:
+    x = 1
+    if 1:
+        x, x = '', 1 \
+        # E: Incompatible types in assignment (expression has type "str", variable has type "int")
+
+[case testRedefineUnderscore]
+# flags: --allow-redefinition
+def f() -> None:
+    _, _ = 1, ''
+    if 1:
+        _, _ = '', 1
+        reveal_type(_) # E: Revealed type is 'Any'
+
+[case testRedefineWithBreakAndContinue]
+# flags: --allow-redefinition
+def f() -> None:
+    y = 0
+    y
+    while int():
+        z = 0
+        z
+        z = ''
+        x = 0
+        if int():
+            break
+        x = '' \
+        # E: Incompatible types in assignment (expression has type "str", variable has type "int")
+    reveal_type(x) # E: Revealed type is 'builtins.int'
+    y = ''
+
+def g() -> None:
+    y = 0
+    y
+    for a in h():
+        z = 0
+        z
+        z = ''
+        x = 0
+        if int():
+            continue
+        x = '' \
+        # E: Incompatible types in assignment (expression has type "str", variable has type "int")
+    reveal_type(x) # E: Revealed type is 'builtins.int'
+    y = ''
+
+def h(): pass
+
+[case testRedefineLocalAndNestedLoops]
+# flags: --allow-redefinition
+def f() -> None:
+    z = 0
+    z
+    while int():
+        x = 0
+        x
+        while int():
+            if 1:
+                y = 1
+                y
+                if int():
+                    break
+                y = '' # E: Incompatible types in assignment (expression has type "str", variable has type "int")
+        x = ''
+    z = ''
+
+[case testCannotRedefineVarAsFunction]
+# flags: --allow-redefinition
+def f() -> None:
+    def x(): pass
+    x = 1 # E: Incompatible types in assignment (expression has type "int", variable has type "Callable[[], Any]")
+    reveal_type(x) # E: Revealed type is 'def () -> Any'
+    y = 1
+    def y(): pass # E: Name 'y' already defined on line 6
+
+[case testCannotRedefineVarAsClass]
+# flags: --allow-redefinition
+def f() -> None:
+    class x: pass
+    x = 1 # E: Cannot assign to a type \
+          # E: Incompatible types in assignment (expression has type "int", variable has type "Type[x]")
+    y = 1
+    class y: pass # E: Name 'y' already defined on line 5
+
+[case testRedefineVarAsTypeVar]
+# flags: --allow-redefinition
+from typing import TypeVar
+def f() -> None:
+    x = TypeVar('x')
+    x = 1  # E: Invalid assignment target
+    reveal_type(x) # E: Revealed type is 'builtins.int'
+    y = 1
+    # NOTE: '"int" not callable' is due to test stubs
+    y = TypeVar('y')  # E: Cannot redefine 'y' as a type variable \
+                      # E: "int" not callable
+    def h(a: y) -> y: return a # E: Invalid type "y"
+
+[case testCannotRedefineVarAsModule]
+# flags: --allow-redefinition
+def f() -> None:
+    import typing as m
+    m = 1 # E: Incompatible types in assignment (expression has type "int", variable has type Module)
+    n = 1
+    import typing as n # E: Name 'n' already defined on line 5
+[builtins fixtures/module.pyi]
+
+[case testRedefineLocalWithTypeAnnotation]
+# flags: --allow-redefinition
+def f() -> None:
+    x = 1
+    reveal_type(x) # E: Revealed type is 'builtins.int'
+    x = ''  # type: object
+    reveal_type(x) # E: Revealed type is 'builtins.object'
+def g() -> None:
+    x = 1
+    reveal_type(x) # E: Revealed type is 'builtins.int'
+    x: object = ''
+    reveal_type(x) # E: Revealed type is 'builtins.object'
+def h() -> None:
+    x: int
+    x = 1
+    reveal_type(x) # E: Revealed type is 'builtins.int'
+    x: object
+    x: object = '' # E: Name 'x' already defined on line 16
+def farg(x: int) -> None:
+    x: str = '' # E: Name 'x' already defined on line 18
+def farg2(x: int) -> None:
+    x: str = x # E: Incompatible types in assignment (expression has type "int", variable has type "str")
+
+[case testRedefineLocalWithTypeAnnotationSpecialCases]
+# flags: --allow-redefinition
+def f() -> None:
+    x: object
+    x = 1
+    if int():
+        x = ''
+    reveal_type(x) # E: Revealed type is 'builtins.object'
+    x = ''
+    reveal_type(x) # E: Revealed type is 'builtins.str'
+    if int():
+        x = 2 \
+        # E: Incompatible types in assignment (expression has type "int", variable has type "str")
+
+
+[case testCannotRedefineSelf]
+# flags: --allow-redefinition
+class A:
+    x = 0
+
+    def f(self) -> None:
+        reveal_type(self.x) # E: Revealed type is 'builtins.int'
+        self = f()
+        self.y: str = ''
+        reveal_type(self.y) # E: Revealed type is 'builtins.str'
+
+def f() -> A: return A()
+
+
+-- Redefine global variable
+-- ------------------------
+
+
+[case testRedefineGlobalWithDifferentType]
+# flags: --allow-redefinition
+import m
+reveal_type(m.x)
+[file m.py]
+x = 0
+reveal_type(x)
+x = object()
+reveal_type(x)
+x = ''
+reveal_type(x)
+[out]
+tmp/m.py:2: error: Revealed type is 'builtins.int'
+tmp/m.py:4: error: Revealed type is 'builtins.object'
+tmp/m.py:6: error: Revealed type is 'builtins.str'
+main:3: error: Revealed type is 'builtins.str'
+
+[case testRedefineGlobalForIndex]
+# flags: --allow-redefinition
+import m
+reveal_type(m.x)
+[file m.py]
+from typing import Iterable
+def f(): pass
+it1: Iterable[int] = f()
+it2: Iterable[str] = f()
+for x in it1:
+    reveal_type(x)
+for x in it2:
+    reveal_type(x)
+reveal_type(x)
+[out]
+tmp/m.py:6: error: Revealed type is 'builtins.int*'
+tmp/m.py:8: error: Revealed type is 'builtins.str*'
+tmp/m.py:9: error: Revealed type is 'builtins.str*'
+main:3: error: Revealed type is 'builtins.str*'
+
+[case testRedefineGlobalBasedOnPreviousValues]
+# flags: --allow-redefinition
+from typing import TypeVar, Iterable
+T = TypeVar('T')
+def f(x: T) -> Iterable[T]: pass
+a = 0
+a = f(a)
+reveal_type(a) # E: Revealed type is 'typing.Iterable[builtins.int*]'
+
+[case testRedefineGlobalWithSeparateDeclaration]
+# flags: --allow-redefinition
+x = ''
+reveal_type(x) # E: Revealed type is 'builtins.str'
+x: int
+x = '' # E: Incompatible types in assignment (expression has type "str", variable has type "int")
+reveal_type(x) # E: Revealed type is 'builtins.int'
+x: object
+x = 1
+reveal_type(x) # E: Revealed type is 'builtins.int'
+if int():
+    x = object()
+
+[case testRedefineGlobalUsingForLoop]
+# flags: --allow-redefinition
+from typing import Iterable, TypeVar, Union
+T = TypeVar('T')
+def f(x: T) -> Iterable[Union[T, str]]: pass
+x = 0
+reveal_type(x)  # E: Revealed type is 'builtins.int'
+for x in f(x):
+    pass
+reveal_type(x)  # E: Revealed type is 'Union[builtins.int*, builtins.str]'
+
+[case testNoRedefinitionIfOnlyInitialized]
+# flags: --allow-redefinition --no-strict-optional
+x = None  # type: int
+x = '' # E: Incompatible types in assignment (expression has type "str", variable has type "int")
+x = object() # E: Incompatible types in assignment (expression has type "object", variable has type "int")
+x  # Reference to variable
+x = ''
+
+y = 0
+y = '' # E: Incompatible types in assignment (expression has type "str", variable has type "int")
+
+[case testNoRedefinitionIfNoValueAssigned]
+# flags: --allow-redefinition
+x: int
+x = '' # E: Incompatible types in assignment (expression has type "str", variable has type "int")
+reveal_type(x) # E: Revealed type is 'builtins.int'
+x: object
+
+[case testNoRedefinitionIfExplicitlyDisallowed]
+# flags: --disallow-redefinition
+x = 0
+x = 2
+x = ''  # E: Incompatible types in assignment (expression has type "str", variable has type "int")
+def f() -> None:
+    y = 0
+    y = '' # E: Incompatible types in assignment (expression has type "str", variable has type "int")
+class C:
+    y = 0
+    y = '' # E: Incompatible types in assignment (expression has type "str", variable has type "int")
+def g() -> None:
+    # _ is a special case
+    _ = 0
+    _ = ''
+    x, _ = 0, C()
+[builtins fixtures/tuple.pyi]
+
+[case testRedefineAsException]
+# flags: --allow-redefinition
+e = 1
+reveal_type(e) # E: Revealed type is 'builtins.int'
+try:
+    pass
+except Exception as e:
+    reveal_type(e) # E: Revealed type is 'builtins.Exception'
+e = ''
+reveal_type(e) # E: Revealed type is 'builtins.str'
+[builtins fixtures/exception.pyi]
+
+[case testRedefineUsingWithStatement]
+# flags: --allow-redefinition
+class A:
+    def __enter__(self) -> int: ...
+    def __exit__(self, x, y, z) -> None: ...
+class B:
+    def __enter__(self) -> str: ...
+    def __exit__(self, x, y, z) -> None: ...
+with A() as x:
+    reveal_type(x) # E: Revealed type is 'builtins.int'
+with B() as x:
+    x = 0 # E: Incompatible types in assignment (expression has type "int", variable has type "str")
diff --git a/test-data/unit/semanal-basic.test b/test-data/unit/semanal-basic.test
index 238544ff8ea9..22231f067de3 100644
--- a/test-data/unit/semanal-basic.test
+++ b/test-data/unit/semanal-basic.test
@@ -334,25 +334,26 @@ MypyFile:1(
           NameExpr(self [l]))))))
 
 [case testGlobalDefinedInBlock]
+# flags: --allow-redefinition
 if object:
     x = object()
     x = x
 x
 [out]
 MypyFile:1(
-  IfStmt:1(
+  IfStmt:2(
     If(
       NameExpr(object [builtins.object]))
     Then(
-      AssignmentStmt:2(
-        NameExpr(x* [__main__.x])
-        CallExpr:2(
+      AssignmentStmt:3(
+        NameExpr(x'* [__main__.x'])
+        CallExpr:3(
           NameExpr(object [builtins.object])
           Args()))
-      AssignmentStmt:3(
-        NameExpr(x [__main__.x])
-        NameExpr(x [__main__.x]))))
-  ExpressionStmt:4(
+      AssignmentStmt:4(
+        NameExpr(x* [__main__.x])
+        NameExpr(x' [__main__.x']))))
+  ExpressionStmt:5(
     NameExpr(x [__main__.x])))
 
 [case testNonlocalDecl]
diff --git a/test-data/unit/semanal-expressions.test b/test-data/unit/semanal-expressions.test
index 32a28f7fe879..1ddc9c20e587 100644
--- a/test-data/unit/semanal-expressions.test
+++ b/test-data/unit/semanal-expressions.test
@@ -219,14 +219,14 @@ MypyFile:1(
 
 [case testListComprehensionWithCondition]
 a = 0
-a = [x for x in a if x]
+b = [x for x in a if x]
 [out]
 MypyFile:1(
   AssignmentStmt:1(
     NameExpr(a* [__main__.a])
     IntExpr(0))
   AssignmentStmt:2(
-    NameExpr(a [__main__.a])
+    NameExpr(b* [__main__.b])
     ListComprehension:2(
       GeneratorExpr:2(
         NameExpr(x [l])
@@ -254,14 +254,14 @@ MypyFile:1(
 
 [case testSetComprehensionWithCondition]
 a = 0
-a = {x for x in a if x}
+b = {x for x in a if x}
 [out]
 MypyFile:1(
   AssignmentStmt:1(
     NameExpr(a* [__main__.a])
     IntExpr(0))
   AssignmentStmt:2(
-    NameExpr(a [__main__.a])
+    NameExpr(b* [__main__.b])
     SetComprehension:2(
       GeneratorExpr:2(
         NameExpr(x [l])
@@ -289,14 +289,14 @@ MypyFile:1(
 
 [case testDictionaryComprehensionWithCondition]
 a = 0
-a = {x: x + 1 for x in a if x}
+b = {x: x + 1 for x in a if x}
 [out]
 MypyFile:1(
   AssignmentStmt:1(
     NameExpr(a* [__main__.a])
     IntExpr(0))
   AssignmentStmt:2(
-    NameExpr(a [__main__.a])
+    NameExpr(b* [__main__.b])
     DictionaryComprehension:2(
       NameExpr(x [l])
       OpExpr:2(
diff --git a/test-data/unit/semanal-statements.test b/test-data/unit/semanal-statements.test
index 891113a3aa7a..b6136da37f6b 100644
--- a/test-data/unit/semanal-statements.test
+++ b/test-data/unit/semanal-statements.test
@@ -157,24 +157,26 @@ MypyFile:1(
         NameExpr(x [l])))))
 
 [case testReusingForLoopIndexVariable]
+# flags: --allow-redefinition
 for x in None:
     pass
 for x in None:
     pass
 [out]
 MypyFile:1(
-  ForStmt:1(
-    NameExpr(x* [__main__.x])
+  ForStmt:2(
+    NameExpr(x'* [__main__.x'])
     NameExpr(None [builtins.None])
-    Block:1(
-      PassStmt:2()))
-  ForStmt:3(
-    NameExpr(x [__main__.x])
+    Block:2(
+      PassStmt:3()))
+  ForStmt:4(
+    NameExpr(x* [__main__.x])
     NameExpr(None [builtins.None])
-    Block:3(
-      PassStmt:4())))
+    Block:4(
+      PassStmt:5())))
 
 [case testReusingForLoopIndexVariable2]
+# flags: --allow-redefinition
 def f():
     for x in None:
         pass
@@ -182,19 +184,19 @@ def f():
         pass
 [out]
 MypyFile:1(
-  FuncDef:1(
+  FuncDef:2(
     f
-    Block:1(
-      ForStmt:2(
+    Block:2(
+      ForStmt:3(
         NameExpr(x* [l])
         NameExpr(None [builtins.None])
-        Block:2(
-          PassStmt:3()))
-      ForStmt:4(
-        NameExpr(x [l])
+        Block:3(
+          PassStmt:4()))
+      ForStmt:5(
+        NameExpr(x'* [l])
         NameExpr(None [builtins.None])
-        Block:4(
-          PassStmt:5())))))
+        Block:5(
+          PassStmt:6())))))
 
 [case testLoopWithElse]
 for x in []:
@@ -310,12 +312,12 @@ MypyFile:1(
 
 [case testLvalues]
 x = y = 1
-x = 1
+xx = 1
 x.m = 1
 x[y] = 1
-x, y = 1
-[x, y] = 1
-(x, y) = 1
+x2, y2 = 1
+[x3, y3] = 1
+(x4, y4) = 1
 [out]
 MypyFile:1(
   AssignmentStmt:1(
@@ -324,7 +326,7 @@ MypyFile:1(
       NameExpr(y* [__main__.y]))
     IntExpr(1))
   AssignmentStmt:2(
-    NameExpr(x [__main__.x])
+    NameExpr(xx* [__main__.xx])
     IntExpr(1))
   AssignmentStmt:3(
     MemberExpr:3(
@@ -338,64 +340,66 @@ MypyFile:1(
     IntExpr(1))
   AssignmentStmt:5(
     TupleExpr:5(
-      NameExpr(x [__main__.x])
-      NameExpr(y [__main__.y]))
+      NameExpr(x2* [__main__.x2])
+      NameExpr(y2* [__main__.y2]))
     IntExpr(1))
   AssignmentStmt:6(
     TupleExpr:6(
-      NameExpr(x [__main__.x])
-      NameExpr(y [__main__.y]))
+      NameExpr(x3* [__main__.x3])
+      NameExpr(y3* [__main__.y3]))
     IntExpr(1))
   AssignmentStmt:7(
     TupleExpr:7(
-      NameExpr(x [__main__.x])
-      NameExpr(y [__main__.y]))
+      NameExpr(x4* [__main__.x4])
+      NameExpr(y4* [__main__.y4]))
     IntExpr(1)))
 
 [case testStarLvalues]
+# flags: --allow-redefinition
 *x, y = 1
 *x, (y, *z) = 1
 *(x, q), r = 1
 [out]
 MypyFile:1(
-  AssignmentStmt:1(
-    TupleExpr:1(
-      StarExpr:1(
-        NameExpr(x* [__main__.x]))
-      NameExpr(y* [__main__.y]))
-    IntExpr(1))
   AssignmentStmt:2(
     TupleExpr:2(
       StarExpr:2(
-        NameExpr(x [__main__.x]))
-      TupleExpr:2(
-        NameExpr(y [__main__.y])
-        StarExpr:2(
-          NameExpr(z* [__main__.z]))))
+        NameExpr(x'* [__main__.x']))
+      NameExpr(y'* [__main__.y']))
     IntExpr(1))
   AssignmentStmt:3(
     TupleExpr:3(
       StarExpr:3(
-        TupleExpr:3(
-          NameExpr(x [__main__.x])
+        NameExpr(x''* [__main__.x'']))
+      TupleExpr:3(
+        NameExpr(y* [__main__.y])
+        StarExpr:3(
+          NameExpr(z* [__main__.z]))))
+    IntExpr(1))
+  AssignmentStmt:4(
+    TupleExpr:4(
+      StarExpr:4(
+        TupleExpr:4(
+          NameExpr(x* [__main__.x])
           NameExpr(q* [__main__.q])))
       NameExpr(r* [__main__.r]))
     IntExpr(1)))
 
 [case testMultipleDefinition]
+# flags: --allow-redefinition
 x, y = 1
 x, y = 2
 [out]
 MypyFile:1(
-  AssignmentStmt:1(
-    TupleExpr:1(
-      NameExpr(x* [__main__.x])
-      NameExpr(y* [__main__.y]))
-    IntExpr(1))
   AssignmentStmt:2(
     TupleExpr:2(
-      NameExpr(x [__main__.x])
-      NameExpr(y [__main__.y]))
+      NameExpr(x'* [__main__.x'])
+      NameExpr(y'* [__main__.y']))
+    IntExpr(1))
+  AssignmentStmt:3(
+    TupleExpr:3(
+      NameExpr(x* [__main__.x])
+      NameExpr(y* [__main__.y]))
     IntExpr(2)))
 
 [case testComplexDefinitions]
@@ -458,27 +462,32 @@ MypyFile:1(
 
 [case testMultipleDefOnlySomeNewNestedLists]
 x = 1
-y, [x, z] = 1
-[p, [x, r]] = 1
+if x:
+    y, [x, z] = 1
+    [p, [x, r]] = 1
 [out]
 MypyFile:1(
   AssignmentStmt:1(
     NameExpr(x* [__main__.x])
     IntExpr(1))
-  AssignmentStmt:2(
-    TupleExpr:2(
-      NameExpr(y* [__main__.y])
-      TupleExpr:2(
-        NameExpr(x [__main__.x])
-        NameExpr(z* [__main__.z])))
-    IntExpr(1))
-  AssignmentStmt:3(
-    TupleExpr:3(
-      NameExpr(p* [__main__.p])
-      TupleExpr:3(
-        NameExpr(x [__main__.x])
-        NameExpr(r* [__main__.r])))
-    IntExpr(1)))
+  IfStmt:2(
+    If(
+      NameExpr(x [__main__.x]))
+    Then(
+      AssignmentStmt:3(
+        TupleExpr:3(
+          NameExpr(y* [__main__.y])
+          TupleExpr:3(
+            NameExpr(x [__main__.x])
+            NameExpr(z* [__main__.z])))
+        IntExpr(1))
+      AssignmentStmt:4(
+        TupleExpr:4(
+          NameExpr(p* [__main__.p])
+          TupleExpr:4(
+            NameExpr(x [__main__.x])
+            NameExpr(r* [__main__.r])))
+        IntExpr(1)))))
 
 [case testIndexedDel]
 x = y = 1
@@ -712,7 +721,8 @@ MypyFile:1(
 [case testVariableInBlock]
 while object:
   x = None
-  x = x
+  if x:
+    x = x
 [out]
 MypyFile:1(
   WhileStmt:1(
@@ -721,9 +731,13 @@ MypyFile:1(
       AssignmentStmt:2(
         NameExpr(x* [__main__.x])
         NameExpr(None [builtins.None]))
-      AssignmentStmt:3(
-        NameExpr(x [__main__.x])
-        NameExpr(x [__main__.x])))))
+      IfStmt:3(
+        If(
+          NameExpr(x [__main__.x]))
+        Then(
+          AssignmentStmt:4(
+            NameExpr(x [__main__.x])
+            NameExpr(x [__main__.x])))))))
 
 [case testVariableInExceptHandler]
 try:
@@ -804,20 +818,21 @@ MypyFile:1(
     PassStmt:8()))
 
 [case testMultipleAssignmentWithPartialNewDef]
+# flags: --allow-redefinition
 o = None
 x, o = o, o
 [out]
 MypyFile:1(
-  AssignmentStmt:1(
-    NameExpr(o* [__main__.o])
-    NameExpr(None [builtins.None]))
   AssignmentStmt:2(
-    TupleExpr:2(
+    NameExpr(o'* [__main__.o'])
+    NameExpr(None [builtins.None]))
+  AssignmentStmt:3(
+    TupleExpr:3(
       NameExpr(x* [__main__.x])
-      NameExpr(o [__main__.o]))
-    TupleExpr:2(
-      NameExpr(o [__main__.o])
-      NameExpr(o [__main__.o]))))
+      NameExpr(o* [__main__.o]))
+    TupleExpr:3(
+      NameExpr(o' [__main__.o'])
+      NameExpr(o' [__main__.o']))))
 
 [case testFunctionDecorator]
 def decorate(f): pass
@@ -927,3 +942,117 @@ MypyFile:1(
             TupleExpr:5(
               NameExpr(a [l])
               NameExpr(b [l]))))))))
+
+[case testRenameGlobalVariable]
+# flags: --allow-redefinition
+def f(a): pass
+x = 0
+f(x)
+x = ''
+f(x)
+[out]
+MypyFile:1(
+  FuncDef:2(
+    f
+    Args(
+      Var(a))
+    Block:2(
+      PassStmt:2()))
+  AssignmentStmt:3(
+    NameExpr(x'* [__main__.x'])
+    IntExpr(0))
+  ExpressionStmt:4(
+    CallExpr:4(
+      NameExpr(f [__main__.f])
+      Args(
+        NameExpr(x' [__main__.x']))))
+  AssignmentStmt:5(
+    NameExpr(x* [__main__.x])
+    StrExpr())
+  ExpressionStmt:6(
+    CallExpr:6(
+      NameExpr(f [__main__.f])
+      Args(
+        NameExpr(x [__main__.x])))))
+
+[case testNoRenameGlobalVariable]
+# flags: --disallow-redefinition
+def f(a): pass
+x = 0
+f(x)
+x = ''
+f(x)
+[out]
+MypyFile:1(
+  FuncDef:2(
+    f
+    Args(
+      Var(a))
+    Block:2(
+      PassStmt:2()))
+  AssignmentStmt:3(
+    NameExpr(x* [__main__.x])
+    IntExpr(0))
+  ExpressionStmt:4(
+    CallExpr:4(
+      NameExpr(f [__main__.f])
+      Args(
+        NameExpr(x [__main__.x]))))
+  AssignmentStmt:5(
+    NameExpr(x [__main__.x])
+    StrExpr())
+  ExpressionStmt:6(
+    CallExpr:6(
+      NameExpr(f [__main__.f])
+      Args(
+        NameExpr(x [__main__.x])))))
+
+[case testRenameLocalVariable]
+# flags: --allow-redefinition
+def f(a):
+    f(a)
+    a = ''
+    f(a)
+[out]
+MypyFile:1(
+  FuncDef:2(
+    f
+    Args(
+      Var(a))
+    Block:2(
+      ExpressionStmt:3(
+        CallExpr:3(
+          NameExpr(f [__main__.f])
+          Args(
+            NameExpr(a [l]))))
+      AssignmentStmt:4(
+        NameExpr(a'* [l])
+        StrExpr())
+      ExpressionStmt:5(
+        CallExpr:5(
+          NameExpr(f [__main__.f])
+          Args(
+            NameExpr(a' [l])))))))
+
+[case testCannotRenameExternalVarWithinClass]
+# flags: --allow-redefinition
+x = 0
+x
+class A:
+    x = 1
+x = ''
+[out]
+MypyFile:1(
+  AssignmentStmt:2(
+    NameExpr(x* [__main__.x])
+    IntExpr(0))
+  ExpressionStmt:3(
+    NameExpr(x [__main__.x]))
+  ClassDef:4(
+    A
+    AssignmentStmt:5(
+      NameExpr(x* [m])
+      IntExpr(1)))
+  AssignmentStmt:6(
+    NameExpr(x [__main__.x])
+    StrExpr()))
diff --git a/test-data/unit/typexport-basic.test b/test-data/unit/typexport-basic.test
index 263be9837616..d56e35720149 100644
--- a/test-data/unit/typexport-basic.test
+++ b/test-data/unit/typexport-basic.test
@@ -204,16 +204,18 @@ CallExpr(5) : B
 from typing import Any
 a = None # type: A
 b = a # type: Any
-b = a
-a = b
+if b:
+    b = a
+    a = b
 
 class A: pass
 [out]
 NameExpr(3) : A
-NameExpr(4) : A
 NameExpr(4) : Any
 NameExpr(5) : A
 NameExpr(5) : Any
+NameExpr(6) : A
+NameExpr(6) : Any
 
 [case testMemberAssignment]
 from typing import Any
@@ -851,7 +853,8 @@ from typing import List
 a = None # type: List[A]
 a or []
 a = a or []
-a = [] or a
+if int():
+    a = [] or a
 class A: pass
 [builtins fixtures/list.pyi]
 [out]
@@ -862,10 +865,12 @@ ListExpr(4) : builtins.list[A]
 NameExpr(4) : builtins.list[A]
 NameExpr(4) : builtins.list[A]
 OpExpr(4) : builtins.list[A]
-ListExpr(5) : builtins.list[A]
-NameExpr(5) : builtins.list[A]
-NameExpr(5) : builtins.list[A]
-OpExpr(5) : builtins.list[A]
+CallExpr(5) : builtins.int
+NameExpr(5) : def () -> builtins.int
+ListExpr(6) : builtins.list[A]
+NameExpr(6) : builtins.list[A]
+NameExpr(6) : builtins.list[A]
+OpExpr(6) : builtins.list[A]
 
 
 -- Class attributes