diff --git a/mypy/checker.py b/mypy/checker.py
index 335344a590a3..d0a51dac70d4 100644
--- a/mypy/checker.py
+++ b/mypy/checker.py
@@ -32,7 +32,7 @@
 from mypy.types import (
     Type, AnyType, CallableType, Void, FunctionLike, Overloaded, TupleType,
     Instance, NoneTyp, ErrorType, strip_type,
-    UnionType, TypeVarType, PartialType, DeletedType
+    UnionType, TypeVarType, PartialType, DeletedType, UninhabitedType
 )
 from mypy.sametypes import is_same_type
 from mypy.messages import MessageBuilder
@@ -53,6 +53,8 @@
 from mypy.treetransform import TransformVisitor
 from mypy.meet import meet_simple, nearest_builtin_ancestor, is_overlapping_types
 
+from mypy import experiments
+
 
 T = TypeVar('T')
 
@@ -223,14 +225,14 @@ def get_declaration(self, expr: Any) -> Type:
         else:
             return self.frames[0].get(expr.literal_hash)
 
-    def assign_type(self, expr: Node, type: Type,
+    def assign_type(self, expr: Node,
+                    type: Type,
+                    declared_type: Type,
                     restrict_any: bool = False) -> None:
         if not expr.literal:
             return
         self.invalidate_dependencies(expr)
 
-        declared_type = self.get_declaration(expr)
-
         if declared_type is None:
             # Not sure why this happens.  It seems to mainly happen in
             # member initialization.
@@ -1200,7 +1202,11 @@ def check_assignment(self, lvalue: Node, rvalue: Node, infer_lvalue_type: bool =
                         partial_types = self.find_partial_types(var)
                         if partial_types is not None:
                             if not self.current_node_deferred:
-                                var.type = rvalue_type
+                                if experiments.STRICT_OPTIONAL:
+                                    var.type = UnionType.make_simplified_union(
+                                        [rvalue_type, NoneTyp()])
+                                else:
+                                    var.type = rvalue_type
                             else:
                                 var.type = None
                             del partial_types[var]
@@ -1208,10 +1214,19 @@ def check_assignment(self, lvalue: Node, rvalue: Node, infer_lvalue_type: bool =
                     # an error will be reported elsewhere.
                     self.infer_partial_type(lvalue_type.var, lvalue, rvalue_type)
                     return
-                rvalue_type = self.check_simple_assignment(lvalue_type, rvalue, lvalue)
+                if (is_literal_none(rvalue) and
+                        isinstance(lvalue, NameExpr) and
+                        isinstance(lvalue.node, Var) and
+                        lvalue.node.is_initialized_in_class):
+                    # Allow None's to be assigned to class variables with non-Optional types.
+                    rvalue_type = lvalue_type
+                else:
+                    rvalue_type = self.check_simple_assignment(lvalue_type, rvalue, lvalue)
 
                 if rvalue_type and infer_lvalue_type:
-                    self.binder.assign_type(lvalue, rvalue_type,
+                    self.binder.assign_type(lvalue,
+                                            rvalue_type,
+                                            lvalue_type,
                                             self.typing_mode_weak())
             elif index_lvalue:
                 self.check_indexed_assignment(index_lvalue, rvalue, rvalue)
@@ -1444,7 +1459,7 @@ def infer_variable_type(self, name: Var, lvalue: Node,
         """Infer the type of initialized variables from initializer type."""
         if self.typing_mode_weak():
             self.set_inferred_type(name, lvalue, AnyType())
-            self.binder.assign_type(lvalue, init_type, True)
+            self.binder.assign_type(lvalue, init_type, self.binder.get_declaration(lvalue), True)
         elif isinstance(init_type, Void):
             self.check_not_void(init_type, context)
             self.set_inference_error_fallback_type(name, lvalue, init_type, context)
@@ -1467,16 +1482,16 @@ def infer_variable_type(self, name: Var, lvalue: Node,
             self.set_inferred_type(name, lvalue, init_type)
 
     def infer_partial_type(self, name: Var, lvalue: Node, init_type: Type) -> bool:
-        if isinstance(init_type, NoneTyp):
-            partial_type = PartialType(None, name)
+        if isinstance(init_type, (NoneTyp, UninhabitedType)):
+            partial_type = PartialType(None, name, [init_type])
         elif isinstance(init_type, Instance):
             fullname = init_type.type.fullname()
-            if ((fullname == 'builtins.list' or fullname == 'builtins.set' or
-                 fullname == 'builtins.dict')
-                    and isinstance(init_type.args[0], NoneTyp)
-                    and (fullname != 'builtins.dict' or isinstance(init_type.args[1], NoneTyp))
-                    and isinstance(lvalue, NameExpr)):
-                partial_type = PartialType(init_type.type, name)
+            if (isinstance(lvalue, NameExpr) and
+                    (fullname == 'builtins.list' or
+                     fullname == 'builtins.set' or
+                     fullname == 'builtins.dict') and
+                    all(isinstance(t, (NoneTyp, UninhabitedType)) for t in init_type.args)):
+                partial_type = PartialType(init_type.type, name, init_type.args)
             else:
                 return False
         else:
@@ -1559,8 +1574,8 @@ def try_infer_partial_type_from_indexed_assignment(
             self, lvalue: IndexExpr, rvalue: Node) -> None:
         # TODO: Should we share some of this with try_infer_partial_type?
         if isinstance(lvalue.base, RefExpr) and isinstance(lvalue.base.node, Var):
-            var = cast(Var, lvalue.base.node)
-            if var is not None and isinstance(var.type, PartialType):
+            var = lvalue.base.node
+            if isinstance(var.type, PartialType):
                 type_type = var.type.type
                 if type_type is None:
                     return  # The partial type is None.
@@ -1572,10 +1587,15 @@ def try_infer_partial_type_from_indexed_assignment(
                     # TODO: Don't infer things twice.
                     key_type = self.accept(lvalue.index)
                     value_type = self.accept(rvalue)
-                    if is_valid_inferred_type(key_type) and is_valid_inferred_type(value_type):
+                    full_key_type = UnionType.make_simplified_union(
+                        [key_type, var.type.inner_types[0]])
+                    full_value_type = UnionType.make_simplified_union(
+                        [value_type, var.type.inner_types[1]])
+                    if (is_valid_inferred_type(full_key_type) and
+                            is_valid_inferred_type(full_value_type)):
                         if not self.current_node_deferred:
                             var.type = self.named_generic_type('builtins.dict',
-                                                               [key_type, value_type])
+                                                               [full_key_type, full_value_type])
                         del partial_types[var]
 
     def visit_expression_stmt(self, s: ExpressionStmt) -> Type:
@@ -1881,7 +1901,10 @@ def analyze_iterable_item_type(self, expr: Node) -> Type:
 
         self.check_not_void(iterable, expr)
         if isinstance(iterable, TupleType):
-            joined = NoneTyp()  # type: Type
+            if experiments.STRICT_OPTIONAL:
+                joined = UninhabitedType()  # type: Type
+            else:
+                joined = NoneTyp()
             for item in iterable.items:
                 joined = join_types(joined, item)
             if isinstance(joined, ErrorType):
@@ -1932,7 +1955,9 @@ def flatten(t: Node) -> List[Node]:
             s.expr.accept(self)
             for elt in flatten(s.expr):
                 if isinstance(elt, NameExpr):
-                    self.binder.assign_type(elt, DeletedType(source=elt.name),
+                    self.binder.assign_type(elt,
+                                            DeletedType(source=elt.name),
+                                            self.binder.get_declaration(elt),
                                             self.typing_mode_weak())
             return None
 
@@ -2311,8 +2336,12 @@ def leave_partial_types(self) -> None:
         partial_types = self.partial_types.pop()
         if not self.current_node_deferred:
             for var, context in partial_types.items():
-                self.msg.fail(messages.NEED_ANNOTATION_FOR_VAR, context)
-                var.type = AnyType()
+                if experiments.STRICT_OPTIONAL and cast(PartialType, var.type).type is None:
+                    # None partial type: assume variable is intended to have type None
+                    var.type = NoneTyp()
+                else:
+                    self.msg.fail(messages.NEED_ANNOTATION_FOR_VAR, context)
+                    var.type = AnyType()
 
     def find_partial_types(self, var: Var) -> Optional[Dict[Var, Context]]:
         for partial_types in reversed(self.partial_types):
@@ -2356,11 +2385,48 @@ def method_type(self, func: FuncBase) -> FunctionLike:
         return method_type_with_fallback(func, self.named_type('builtins.function'))
 
 
+def conditional_type_map(expr: Node,
+                         current_type: Optional[Type],
+                         proposed_type: Optional[Type],
+                         *,
+                         weak: bool = False
+                         ) -> Tuple[Optional[Dict[Node, Type]], Optional[Dict[Node, Type]]]:
+    """Takes in an expression, the current type of the expression, and a
+    proposed type of that expression.
+
+    Returns a 2-tuple: The first element is a map from the expression to
+    the proposed type, if the expression can be the proposed type.  The
+    second element is a map from the expression to the type it would hold
+    if it was not the proposed type, if any."""
+    if proposed_type:
+        if current_type:
+            if is_proper_subtype(current_type, proposed_type):
+                return {expr: proposed_type}, None
+            elif not is_overlapping_types(current_type, proposed_type):
+                return None, {expr: current_type}
+            else:
+                remaining_type = restrict_subtype_away(current_type, proposed_type)
+                return {expr: proposed_type}, {expr: remaining_type}
+        else:
+            return {expr: proposed_type}, {}
+    else:
+        # An isinstance check, but we don't understand the type
+        if weak:
+            return {expr: AnyType()}, {expr: current_type}
+        else:
+            return {}, {}
+
+
+def is_literal_none(n: Node) -> bool:
+    return isinstance(n, NameExpr) and n.fullname == 'builtins.None'
+
+
 def find_isinstance_check(node: Node,
                           type_map: Dict[Node, Type],
-                          weak: bool=False) \
-        -> Tuple[Optional[Dict[Node, Type]], Optional[Dict[Node, Type]]]:
-    """Find any isinstance checks (within a chain of ands).
+                          weak: bool=False
+                          ) -> Tuple[Optional[Dict[Node, Type]], Optional[Dict[Node, Type]]]:
+    """Find any isinstance checks (within a chain of ands).  Includes
+    implicit and explicit checks for None.
 
     Return value is a map of variables to their types if the condition
     is true and a map of variables to their types if the condition is false.
@@ -2376,20 +2442,31 @@ def find_isinstance_check(node: Node,
             if expr.literal == LITERAL_TYPE:
                 vartype = type_map[expr]
                 type = get_isinstance_type(node.args[1], type_map)
-                if type:
-                    elsetype = vartype
-                    if vartype:
-                        if is_proper_subtype(vartype, type):
-                            return {expr: type}, None
-                        elif not is_overlapping_types(vartype, type):
-                            return None, {expr: elsetype}
-                        else:
-                            elsetype = restrict_subtype_away(vartype, type)
-                    return {expr: type}, {expr: elsetype}
-                else:
-                    # An isinstance check, but we don't understand the type
-                    if weak:
-                        return {expr: AnyType()}, {expr: vartype}
+                return conditional_type_map(expr, vartype, type, weak=weak)
+    elif (isinstance(node, ComparisonExpr) and any(is_literal_none(n) for n in node.operands) and
+          experiments.STRICT_OPTIONAL):
+        # Check for `x is None` and `x is not None`.
+        is_not = node.operators == ['is not']
+        if is_not or node.operators == ['is']:
+            if_vars = {}  # type: Dict[Node, Type]
+            else_vars = {}  # type: Dict[Node, Type]
+            for expr in node.operands:
+                if expr.literal == LITERAL_TYPE and not is_literal_none(expr) and expr in type_map:
+                    # This should only be true at most once: there should be
+                    # two elements in node.operands, and at least one of them
+                    # should represent a None.
+                    vartype = type_map[expr]
+                    if_vars, else_vars = conditional_type_map(expr, vartype, NoneTyp(), weak=weak)
+                    break
+
+            if is_not:
+                if_vars, else_vars = else_vars, if_vars
+            return if_vars, else_vars
+    elif isinstance(node, RefExpr) and experiments.STRICT_OPTIONAL:
+        # The type could be falsy, so we can't deduce anything new about the else branch
+        vartype = type_map[node]
+        _, if_vars = conditional_type_map(node, vartype, NoneTyp(), weak=weak)
+        return if_vars, {}
     elif isinstance(node, OpExpr) and node.op == 'and':
         left_if_vars, right_else_vars = find_isinstance_check(
             node.left,
@@ -2571,6 +2648,12 @@ def is_valid_inferred_type(typ: Type) -> bool:
     Examples of invalid types include the None type or a type with a None component.
     """
     if is_same_type(typ, NoneTyp()):
+        # With strict Optional checking, we *may* eventually infer NoneTyp, but
+        # we only do that if we can't infer a specific Optional type.  This
+        # resolution happens in leave_partial_types when we pop a partial types
+        # scope.
+        return False
+    if is_same_type(typ, UninhabitedType()):
         return False
     elif isinstance(typ, Instance):
         for arg in typ.args:
diff --git a/mypy/checkexpr.py b/mypy/checkexpr.py
index 64263ce6cfb2..d759c96475e1 100644
--- a/mypy/checkexpr.py
+++ b/mypy/checkexpr.py
@@ -5,7 +5,7 @@
 from mypy.types import (
     Type, AnyType, CallableType, Overloaded, NoneTyp, Void, TypeVarDef,
     TupleType, Instance, TypeVarType, ErasedType, UnionType,
-    PartialType, DeletedType, UnboundType, TypeType
+    PartialType, DeletedType, UnboundType, UninhabitedType, TypeType
 )
 from mypy.nodes import (
     NameExpr, RefExpr, Var, FuncDef, OverloadedFuncDef, TypeInfo, CallExpr,
@@ -35,6 +35,7 @@
 from mypy.constraints import get_actual_type
 from mypy.checkstrformat import StringFormatterChecker
 
+from mypy import experiments
 
 # Type of callback user for checking individual function arguments. See
 # check_args() below for details.
@@ -154,19 +155,21 @@ def try_infer_partial_type(self, e: CallExpr) -> None:
             var = cast(Var, e.callee.expr.node)
             partial_types = self.chk.find_partial_types(var)
             if partial_types is not None and not self.chk.current_node_deferred:
-                partial_type_type = cast(PartialType, var.type).type
-                if partial_type_type is None:
+                partial_type = cast(PartialType, var.type)
+                if partial_type.type is None:
                     # A partial None type -> can't infer anything.
                     return
-                typename = partial_type_type.fullname()
+                typename = partial_type.type.fullname()
                 methodname = e.callee.name
                 # Sometimes we can infer a full type for a partial List, Dict or Set type.
                 # TODO: Don't infer argument expression twice.
                 if (typename in self.item_args and methodname in self.item_args[typename]
                         and e.arg_kinds == [ARG_POS]):
                     item_type = self.accept(e.args[0])
-                    if mypy.checker.is_valid_inferred_type(item_type):
-                        var.type = self.chk.named_generic_type(typename, [item_type])
+                    full_item_type = UnionType.make_simplified_union(
+                        [item_type, partial_type.inner_types[0]])
+                    if mypy.checker.is_valid_inferred_type(full_item_type):
+                        var.type = self.chk.named_generic_type(typename, [full_item_type])
                         del partial_types[var]
                 elif (typename in self.container_args
                       and methodname in self.container_args[typename]
@@ -175,10 +178,15 @@ def try_infer_partial_type(self, e: CallExpr) -> None:
                     if isinstance(arg_type, Instance):
                         arg_typename = arg_type.type.fullname()
                         if arg_typename in self.container_args[typename][methodname]:
+                            full_item_types = [
+                                UnionType.make_simplified_union([item_type, prev_type])
+                                for item_type, prev_type
+                                in zip(arg_type.args, partial_type.inner_types)
+                            ]
                             if all(mypy.checker.is_valid_inferred_type(item_type)
-                                   for item_type in arg_type.args):
+                                   for item_type in full_item_types):
                                 var.type = self.chk.named_generic_type(typename,
-                                                                       list(arg_type.args))
+                                                                       list(full_item_types))
                                 del partial_types[var]
 
     def check_call_expr_with_callee_type(self, callee_type: Type,
@@ -411,7 +419,7 @@ def infer_function_type_arguments_using_context(
         # Only substitute non-None and non-erased types.
         new_args = []  # type: List[Type]
         for arg in args:
-            if isinstance(arg, NoneTyp) or has_erased_component(arg):
+            if isinstance(arg, (NoneTyp, UninhabitedType)) or has_erased_component(arg):
                 new_args.append(None)
             else:
                 new_args.append(arg)
@@ -470,7 +478,7 @@ def infer_function_type_arguments(self, callee_type: CallableType,
                 #       if they shuffle type variables around, as we assume that there is a 1-1
                 #       correspondence with dict type variables. This is a marginal issue and
                 #       a little tricky to fix so it's left unfixed for now.
-                if isinstance(inferred_args[0], NoneTyp):
+                if isinstance(inferred_args[0], (NoneTyp, UninhabitedType)):
                     inferred_args[0] = self.named_type('builtins.str')
                 elif not is_subtype(self.named_type('builtins.str'), inferred_args[0]):
                     self.msg.fail(messages.KEYWORD_ARGUMENT_REQUIRES_STR_KEY_TYPE,
@@ -504,7 +512,7 @@ def infer_function_type_arguments_pass2(
         # information to infer the argument. Replace them with None values so
         # that they are not applied yet below.
         for i, arg in enumerate(inferred_args):
-            if isinstance(arg, NoneTyp) or has_erased_component(arg):
+            if isinstance(arg, (NoneTyp, UninhabitedType)) or has_erased_component(arg):
                 inferred_args[i] = None
 
         callee_type = cast(CallableType, self.apply_generic_arguments(
@@ -1730,11 +1738,14 @@ def overload_arg_similarity(actual: Type, formal: Type) -> int:
         actual = actual.erase_to_union_or_bound()
     if isinstance(formal, TypeVarType):
         formal = formal.erase_to_union_or_bound()
-    if (isinstance(actual, NoneTyp) or isinstance(actual, AnyType) or
+    if (isinstance(actual, UninhabitedType) or isinstance(actual, AnyType) or
             isinstance(formal, AnyType) or isinstance(formal, CallableType) or
             (isinstance(actual, Instance) and actual.type.fallback_to_any)):
         # These could match anything at runtime.
         return 2
+    if not experiments.STRICT_OPTIONAL and isinstance(actual, NoneTyp):
+        # NoneTyp matches anything if we're not doing strict Optional checking
+        return 2
     if isinstance(actual, UnionType):
         return max(overload_arg_similarity(item, formal)
                    for item in actual.items)
diff --git a/mypy/constraints.py b/mypy/constraints.py
index 8e5fdee06b70..016a1593c659 100644
--- a/mypy/constraints.py
+++ b/mypy/constraints.py
@@ -5,7 +5,7 @@
 from mypy.types import (
     CallableType, Type, TypeVisitor, UnboundType, AnyType, Void, NoneTyp, TypeVarType,
     Instance, TupleType, UnionType, Overloaded, ErasedType, PartialType, DeletedType,
-    TypeType, is_named_instance
+    UninhabitedType, TypeType, is_named_instance
 )
 from mypy.maptype import map_instance_to_supertype
 from mypy import nodes
@@ -222,6 +222,9 @@ def visit_void(self, template: Void) -> List[Constraint]:
     def visit_none_type(self, template: NoneTyp) -> List[Constraint]:
         return []
 
+    def visit_uninhabited_type(self, template: UninhabitedType) -> List[Constraint]:
+        return []
+
     def visit_erased_type(self, template: ErasedType) -> List[Constraint]:
         return []
 
diff --git a/mypy/erasetype.py b/mypy/erasetype.py
index e805f8563b0f..17b51e3782af 100644
--- a/mypy/erasetype.py
+++ b/mypy/erasetype.py
@@ -3,7 +3,7 @@
 from mypy.types import (
     Type, TypeVisitor, UnboundType, ErrorType, AnyType, Void, NoneTyp,
     Instance, TypeVarType, CallableType, TupleType, UnionType, Overloaded, ErasedType,
-    PartialType, DeletedType, TypeTranslator, TypeList, TypeType
+    PartialType, DeletedType, TypeTranslator, TypeList, UninhabitedType, TypeType
 )
 
 
@@ -43,6 +43,9 @@ def visit_void(self, t: Void) -> Type:
     def visit_none_type(self, t: NoneTyp) -> Type:
         return t
 
+    def visit_uninhabited_type(self, t: UninhabitedType) -> Type:
+        return t
+
     def visit_erased_type(self, t: ErasedType) -> Type:
         # Should not get here.
         raise RuntimeError()
diff --git a/mypy/expandtype.py b/mypy/expandtype.py
index e25190fe4329..25b1093318a0 100644
--- a/mypy/expandtype.py
+++ b/mypy/expandtype.py
@@ -3,7 +3,7 @@
 from mypy.types import (
     Type, Instance, CallableType, TypeVisitor, UnboundType, ErrorType, AnyType,
     Void, NoneTyp, TypeVarType, Overloaded, TupleType, UnionType, ErasedType, TypeList,
-    PartialType, DeletedType, TypeType
+    PartialType, DeletedType, UninhabitedType, TypeType
 )
 
 
@@ -53,6 +53,9 @@ def visit_void(self, t: Void) -> Type:
     def visit_none_type(self, t: NoneTyp) -> Type:
         return t
 
+    def visit_uninhabited_type(self, t: UninhabitedType) -> Type:
+        return t
+
     def visit_deleted_type(self, t: DeletedType) -> Type:
         return t
 
diff --git a/mypy/experiments.py b/mypy/experiments.py
new file mode 100644
index 000000000000..a4684cc55ad1
--- /dev/null
+++ b/mypy/experiments.py
@@ -0,0 +1 @@
+STRICT_OPTIONAL = False
diff --git a/mypy/fixup.py b/mypy/fixup.py
index 73fb22775d3d..9c8bcc628b82 100644
--- a/mypy/fixup.py
+++ b/mypy/fixup.py
@@ -8,7 +8,7 @@
                         LDEF, MDEF, GDEF, MODULE_REF)
 from mypy.types import (CallableType, EllipsisType, Instance, Overloaded, TupleType,
                         TypeList, TypeVarType, UnboundType, UnionType, TypeVisitor,
-                        TypeType)
+                        UninhabitedType, TypeType)
 from mypy.visitor import NodeVisitor
 
 
@@ -182,6 +182,9 @@ def visit_deleted_type(self, o: Any) -> None:
     def visit_none_type(self, o: Any) -> None:
         pass  # Nothing to descend into.
 
+    def visit_uninhabited_type(self, o: Any) -> None:
+        pass  # Nothing to descend into.
+
     def visit_partial_type(self, o: Any) -> None:
         raise RuntimeError("Shouldn't get here", o)
 
diff --git a/mypy/join.py b/mypy/join.py
index 0c42b64d7d62..c28216b5de69 100644
--- a/mypy/join.py
+++ b/mypy/join.py
@@ -6,11 +6,13 @@
     Type, AnyType, NoneTyp, Void, TypeVisitor, Instance, UnboundType,
     ErrorType, TypeVarType, CallableType, TupleType, ErasedType, TypeList,
     UnionType, FunctionLike, Overloaded, PartialType, DeletedType,
-    TypeType
+    UninhabitedType, TypeType
 )
 from mypy.maptype import map_instance_to_supertype
 from mypy.subtypes import is_subtype, is_equivalent, is_subtype_ignoring_tvars
 
+from mypy import experiments
+
 
 def join_simple(declaration: Type, s: Type, t: Type) -> Type:
     """Return a simple least upper bound given the declared type."""
@@ -18,9 +20,6 @@ def join_simple(declaration: Type, s: Type, t: Type) -> Type:
     if isinstance(s, AnyType):
         return s
 
-    if isinstance(s, NoneTyp) and not isinstance(t, Void):
-        return t
-
     if isinstance(s, ErasedType):
         return t
 
@@ -33,6 +32,12 @@ def join_simple(declaration: Type, s: Type, t: Type) -> Type:
     if isinstance(declaration, UnionType):
         return UnionType.make_simplified_union([s, t])
 
+    if isinstance(s, NoneTyp) and not isinstance(t, NoneTyp):
+        s, t = t, s
+
+    if isinstance(s, UninhabitedType) and not isinstance(t, UninhabitedType):
+        s, t = t, s
+
     value = t.accept(TypeJoinVisitor(s))
 
     if value is None:
@@ -58,12 +63,12 @@ def join_types(s: Type, t: Type) -> Type:
     if isinstance(s, AnyType):
         return s
 
-    if isinstance(s, NoneTyp) and not isinstance(t, Void):
-        return t
-
     if isinstance(s, ErasedType):
         return t
 
+    if isinstance(s, NoneTyp) and not isinstance(t, NoneTyp):
+        s, t = t, s
+
     # Use a visitor to handle non-trivial cases.
     return t.accept(TypeJoinVisitor(s))
 
@@ -106,6 +111,18 @@ def visit_void(self, t: Void) -> Type:
             return ErrorType()
 
     def visit_none_type(self, t: NoneTyp) -> Type:
+        if experiments.STRICT_OPTIONAL:
+            if isinstance(self.s, (NoneTyp, UninhabitedType)):
+                return t
+            else:
+                return self.default(self.s)
+        else:
+            if not isinstance(self.s, Void):
+                return self.s
+            else:
+                return self.default(self.s)
+
+    def visit_uninhabited_type(self, t: UninhabitedType) -> Type:
         if not isinstance(self.s, Void):
             return self.s
         else:
@@ -333,8 +350,12 @@ def join_type_list(types: List[Type]) -> Type:
     if not types:
         # This is a little arbitrary but reasonable. Any empty tuple should be compatible
         # with all variable length tuples, and this makes it possible. A better approach
-        # would be to use a special bottom type.
-        return NoneTyp()
+        # would be to use a special bottom type, which we do when strict Optional
+        # checking is enabled.
+        if experiments.STRICT_OPTIONAL:
+            return UninhabitedType()
+        else:
+            return NoneTyp()
     joined = types[0]
     for t in types[1:]:
         joined = join_types(joined, t)
diff --git a/mypy/main.py b/mypy/main.py
index d405dd9d982b..256abb429e2d 100644
--- a/mypy/main.py
+++ b/mypy/main.py
@@ -10,6 +10,7 @@
 from mypy import build
 from mypy import defaults
 from mypy import git
+from mypy import experiments
 from mypy.build import BuildSource, BuildResult, PYTHON_EXTENSIONS
 from mypy.errors import CompileError, set_drop_into_pdb
 
@@ -156,6 +157,8 @@ def parse_version(v):
                         help="enable experimental fast parser")
     parser.add_argument('-i', '--incremental', action='store_true',
                         help="enable experimental module cache")
+    parser.add_argument('--strict-optional', action='store_true',
+                        help="enable experimental strict Optional checks")
     parser.add_argument('-f', '--dirty-stubs', action='store_true',
                         help="don't warn if typeshed is out of sync")
     parser.add_argument('--pdb', action='store_true', help="invoke pdb on fatal error")
@@ -254,6 +257,8 @@ def parse_version(v):
         options.build_flags.append(build.FAST_PARSER)
     if args.incremental:
         options.build_flags.append(build.INCREMENTAL)
+    if args.strict_optional:
+        experiments.STRICT_OPTIONAL = True
 
     # Set reports.
     for flag, val in vars(args).items():
diff --git a/mypy/meet.py b/mypy/meet.py
index eff2eedf8fab..9c2516d9bf05 100644
--- a/mypy/meet.py
+++ b/mypy/meet.py
@@ -3,12 +3,14 @@
 from mypy.join import is_similar_callables, combine_similar_callables
 from mypy.types import (
     Type, AnyType, TypeVisitor, UnboundType, Void, ErrorType, NoneTyp, TypeVarType,
-    Instance, CallableType, TupleType, ErasedType, TypeList,
-    UnionType, PartialType, DeletedType, TypeType
+    Instance, CallableType, TupleType, ErasedType, TypeList, UnionType, PartialType,
+    DeletedType, UninhabitedType, TypeType
 )
 from mypy.subtypes import is_subtype
 from mypy.nodes import TypeInfo
 
+from mypy import experiments
+
 # TODO Describe this module.
 
 
@@ -29,7 +31,10 @@ def meet_simple(s: Type, t: Type, default_right: bool = True) -> Type:
     if isinstance(s, UnionType):
         return UnionType.make_simplified_union([meet_types(x, t) for x in s.items])
     elif not is_overlapping_types(s, t, use_promotions=True):
-        return NoneTyp()
+        if experiments.STRICT_OPTIONAL:
+            return UninhabitedType()
+        else:
+            return NoneTyp()
     else:
         if default_right:
             return t
@@ -89,6 +94,10 @@ class C(A, B): ...
     if isinstance(s, UnionType):
         return any(is_overlapping_types(t, item)
                    for item in s.items)
+    if experiments.STRICT_OPTIONAL:
+        if isinstance(t, NoneTyp) != isinstance(s, NoneTyp):
+            # NoneTyp does not overlap with other non-Union types under strict Optional checking
+            return False
     # We conservatively assume that non-instance, non-union types can overlap any other
     # types.
     return True
@@ -110,6 +119,11 @@ def visit_unbound_type(self, t: UnboundType) -> Type:
         if isinstance(self.s, Void) or isinstance(self.s, ErrorType):
             return ErrorType()
         elif isinstance(self.s, NoneTyp):
+            if experiments.STRICT_OPTIONAL:
+                return AnyType()
+            else:
+                return self.s
+        elif isinstance(self.s, UninhabitedType):
             return self.s
         else:
             return AnyType()
@@ -141,6 +155,19 @@ def visit_void(self, t: Void) -> Type:
             return ErrorType()
 
     def visit_none_type(self, t: NoneTyp) -> Type:
+        if experiments.STRICT_OPTIONAL:
+            if isinstance(self.s, NoneTyp) or (isinstance(self.s, Instance) and
+                                               self.s.type.fullname() == 'builtins.object'):
+                return t
+            else:
+                return UninhabitedType()
+        else:
+            if not isinstance(self.s, Void) and not isinstance(self.s, ErrorType):
+                return t
+            else:
+                return ErrorType()
+
+    def visit_uninhabited_type(self, t: UninhabitedType) -> Type:
         if not isinstance(self.s, Void) and not isinstance(self.s, ErrorType):
             return t
         else:
@@ -149,6 +176,11 @@ def visit_none_type(self, t: NoneTyp) -> Type:
     def visit_deleted_type(self, t: DeletedType) -> Type:
         if not isinstance(self.s, Void) and not isinstance(self.s, ErrorType):
             if isinstance(self.s, NoneTyp):
+                if experiments.STRICT_OPTIONAL:
+                    return t
+                else:
+                    return self.s
+            elif isinstance(self.s, UninhabitedType):
                 return self.s
             else:
                 return t
@@ -176,7 +208,10 @@ def visit_instance(self, t: Instance) -> Type:
                         args.append(self.meet(t.args[i], si.args[i]))
                     return Instance(t.type, args)
                 else:
-                    return NoneTyp()
+                    if experiments.STRICT_OPTIONAL:
+                        return UninhabitedType()
+                    else:
+                        return NoneTyp()
             else:
                 if is_subtype(t, self.s):
                     return t
@@ -184,7 +219,10 @@ def visit_instance(self, t: Instance) -> Type:
                     # See also above comment.
                     return self.s
                 else:
-                    return NoneTyp()
+                    if experiments.STRICT_OPTIONAL:
+                        return UninhabitedType()
+                    else:
+                        return NoneTyp()
         elif isinstance(self.s, TypeType):
             return meet_types(t, self.s)
         else:
@@ -230,4 +268,7 @@ def default(self, typ):
         elif isinstance(typ, Void) or isinstance(typ, ErrorType):
             return ErrorType()
         else:
-            return NoneTyp()
+            if experiments.STRICT_OPTIONAL:
+                return UninhabitedType()
+            else:
+                return NoneTyp()
diff --git a/mypy/messages.py b/mypy/messages.py
index 2946910696f7..c73f641d3afd 100644
--- a/mypy/messages.py
+++ b/mypy/messages.py
@@ -249,14 +249,21 @@ def format_simple(self, typ: Type, verbosity: int = 0) -> str:
             else:
                 return 'tuple(length {})'.format(len(items))
         elif isinstance(typ, UnionType):
-            items = []
-            for t in typ.items:
-                items.append(strip_quotes(self.format(t)))
-            s = '"Union[{}]"'.format(', '.join(items))
-            if len(s) < 40:
-                return s
+            # Only print Unions as Optionals if the Optional wouldn't have to contain another Union
+            print_as_optional = (len(typ.items) -
+                                 sum(isinstance(t, NoneTyp) for t in typ.items) == 1)
+            if print_as_optional:
+                rest = [t for t in typ.items if not isinstance(t, NoneTyp)]
+                return '"Optional[{}]"'.format(strip_quotes(self.format(rest[0])))
             else:
-                return 'union type ({} items)'.format(len(items))
+                items = []
+                for t in typ.items:
+                    items.append(strip_quotes(self.format(t)))
+                s = '"Union[{}]"'.format(', '.join(items))
+                if len(s) < 40:
+                    return s
+                else:
+                    return 'union type ({} items)'.format(len(items))
         elif isinstance(typ, Void):
             return 'None'
         elif isinstance(typ, NoneTyp):
diff --git a/mypy/parse.py b/mypy/parse.py
index 4cd3389dd5bb..b55fe7956954 100644
--- a/mypy/parse.py
+++ b/mypy/parse.py
@@ -37,6 +37,8 @@
     parse_type, parse_types, parse_signature, TypeParseError, parse_str_as_signature
 )
 
+from mypy import experiments
+
 
 precedence = {
     '**': 16,
@@ -482,6 +484,9 @@ def parse_function(self, no_type_checks: bool=False) -> FuncDef:
             if is_error:
                 return None
 
+            if typ and isinstance(typ.ret_type, UnboundType):
+                typ.ret_type.is_ret_type = True
+
             node = FuncDef(name, args, body, typ)
             node.set_line(def_tok)
             if typ is not None:
@@ -782,8 +787,18 @@ def parse_normal_arg(self, require_named: bool,
             else:
                 kind = nodes.ARG_POS
 
+        self.set_type_optional(type, initializer)
+
         return Argument(variable, type, initializer, kind), require_named
 
+    def set_type_optional(self, type: Type, initializer: Node) -> None:
+        if not experiments.STRICT_OPTIONAL:
+            return
+        # Indicate that type should be wrapped in an Optional if arg is initialized to None.
+        optional = isinstance(initializer, NameExpr) and initializer.name == 'None'
+        if isinstance(type, UnboundType):
+            type.optional = optional
+
     def parse_parameter_annotation(self) -> Node:
         if self.current_str() == ':':
             self.skip()
diff --git a/mypy/sametypes.py b/mypy/sametypes.py
index 319af509e70c..afdcd72fa4ca 100644
--- a/mypy/sametypes.py
+++ b/mypy/sametypes.py
@@ -2,8 +2,8 @@
 
 from mypy.types import (
     Type, UnboundType, ErrorType, AnyType, NoneTyp, Void, TupleType, UnionType, CallableType,
-    TypeVarType, Instance, TypeVisitor, ErasedType, TypeList,
-    Overloaded, PartialType, DeletedType, TypeType
+    TypeVarType, Instance, TypeVisitor, ErasedType, TypeList, Overloaded, PartialType,
+    DeletedType, UninhabitedType, TypeType
 )
 
 
@@ -70,6 +70,9 @@ def visit_void(self, left: Void) -> bool:
     def visit_none_type(self, left: NoneTyp) -> bool:
         return isinstance(self.right, NoneTyp)
 
+    def visit_uninhabited_type(self, t: UninhabitedType) -> bool:
+        return isinstance(self.right, UninhabitedType)
+
     def visit_erased_type(self, left: ErasedType) -> bool:
         # Should not get here.
         raise RuntimeError()
diff --git a/mypy/solve.py b/mypy/solve.py
index a2cfa282eec7..9d751dd6b2db 100644
--- a/mypy/solve.py
+++ b/mypy/solve.py
@@ -2,12 +2,14 @@
 
 from typing import List, Dict
 
-from mypy.types import Type, Void, NoneTyp, AnyType, ErrorType
+from mypy.types import Type, Void, NoneTyp, AnyType, ErrorType, UninhabitedType
 from mypy.constraints import Constraint, SUPERTYPE_OF
 from mypy.join import join_types
 from mypy.meet import meet_types
 from mypy.subtypes import is_subtype
 
+from mypy import experiments
+
 
 def solve_constraints(vars: List[int], constraints: List[Constraint],
                       strict=True) -> List[Type]:
@@ -58,7 +60,10 @@ def solve_constraints(vars: List[int], constraints: List[Constraint],
             else:
                 # No constraints for type variable -- type 'None' is the most specific type.
                 if strict:
-                    candidate = NoneTyp()
+                    if experiments.STRICT_OPTIONAL:
+                        candidate = UninhabitedType()
+                    else:
+                        candidate = NoneTyp()
                 else:
                     candidate = AnyType()
         elif top is None:
diff --git a/mypy/subtypes.py b/mypy/subtypes.py
index ea47c3f67b5d..cf457e6cb2b6 100644
--- a/mypy/subtypes.py
+++ b/mypy/subtypes.py
@@ -3,7 +3,7 @@
 from mypy.types import (
     Type, AnyType, UnboundType, TypeVisitor, ErrorType, Void, NoneTyp,
     Instance, TypeVarType, CallableType, TupleType, UnionType, Overloaded, ErasedType, TypeList,
-    PartialType, DeletedType, TypeType, is_named_instance
+    PartialType, DeletedType, UninhabitedType, TypeType, is_named_instance
 )
 import mypy.applytype
 import mypy.constraints
@@ -13,6 +13,8 @@
 from mypy.nodes import CONTRAVARIANT, COVARIANT
 from mypy.maptype import map_instance_to_supertype
 
+from mypy import experiments
+
 
 TypeParameterChecker = Callable[[Type, Type, int], bool]
 
@@ -99,6 +101,13 @@ def visit_void(self, left: Void) -> bool:
         return isinstance(self.right, Void)
 
     def visit_none_type(self, left: NoneTyp) -> bool:
+        if experiments.STRICT_OPTIONAL:
+            return (isinstance(self.right, NoneTyp) or
+                    is_named_instance(self.right, 'builtins.object'))
+        else:
+            return not isinstance(self.right, Void)
+
+    def visit_uninhabited_type(self, left: UninhabitedType) -> bool:
         return not isinstance(self.right, Void)
 
     def visit_erased_type(self, left: ErasedType) -> bool:
diff --git a/mypy/test/data/check-dynamic-typing.test b/mypy/test/data/check-dynamic-typing.test
index c58e1d57306c..8f41e2ed6260 100644
--- a/mypy/test/data/check-dynamic-typing.test
+++ b/mypy/test/data/check-dynamic-typing.test
@@ -191,7 +191,7 @@ a = d.foo(a()) # E: "A" not callable
 a = d.x
 a = d.foo(a, a)
 d.x = a
-d.x.y.z
+d.x.y.z  # E: "A" has no attribute "y"
 
 class A: pass
 [out]
diff --git a/mypy/test/data/check-inference.test b/mypy/test/data/check-inference.test
index bbf0f6bc2c0e..fe5c4f9150df 100644
--- a/mypy/test/data/check-inference.test
+++ b/mypy/test/data/check-inference.test
@@ -1415,13 +1415,16 @@ main: note: In member "f" of class "A":
 [case testAttributePartiallyInitializedToNoneWithMissingAnnotation]
 class A:
     def f(self) -> None:
-        self.x = None # E: Need type annotation for variable
+        self.x = None
 
     def g(self) -> None:
         self.x = 1
         self.x()
 [out]
 main: note: In member "f" of class "A":
+main:3: error: Need type annotation for variable
+main: note: In member "g" of class "A":
+main:7: error: "int" not callable
 
 [case testGlobalInitializedToNoneSetFromFunction]
 a = None
diff --git a/mypy/test/data/check-lists.test b/mypy/test/data/check-lists.test
index 62c3bf6a6694..3bafa99245d1 100644
--- a/mypy/test/data/check-lists.test
+++ b/mypy/test/data/check-lists.test
@@ -61,4 +61,4 @@ class B: pass
 class C: pass
 [builtins fixtures/list.py]
 [out]
-main: note: In function "f":
\ No newline at end of file
+main: note: In function "f":
diff --git a/mypy/test/data/check-optional.test b/mypy/test/data/check-optional.test
new file mode 100644
index 000000000000..7dad0933cf24
--- /dev/null
+++ b/mypy/test/data/check-optional.test
@@ -0,0 +1,169 @@
+-- Tests for strict Optional behavior
+
+[case testImplicitNoneType]
+x = None
+x()  # E: None not callable
+
+[case testExplicitNoneType]
+x = None  # type: None
+x()  # E: None not callable
+
+[case testNoneMemberOfOptional]
+from typing import Optional
+x = None  # type: Optional[int]
+
+[case testTypeMemberOfOptional]
+from typing import Optional
+x = 0  # type: Optional[int]
+
+[case testNoneNotMemberOfType]
+x = None  # type: int
+[out]
+main:1: error: Incompatible types in assignment (expression has type None, variable has type "int")
+
+[case testTypeNotMemberOfNone]
+x = 0  # type: None
+[out]
+main:1: error: Incompatible types in assignment (expression has type "int", variable has type None)
+
+[case testOptionalNotMemberOfType]
+from typing import Optional
+def f(a: int) -> None: pass
+x = None  # type:  Optional[int]
+f(x)  # E: Argument 1 to "f" has incompatible type "Optional[int]"; expected "int"
+
+[case testIsinstanceCases]
+from typing import Optional
+x = None  # type:  Optional[int]
+if isinstance(x, int):
+  reveal_type(x)  # E: Revealed type is 'builtins.int'
+else:
+  reveal_type(x)  # E: Revealed type is 'builtins.None'
+[builtins fixtures/isinstance.py]
+
+[case testIfCases]
+from typing import Optional
+x = None  # type:  Optional[int]
+if x:
+  reveal_type(x)  # E: Revealed type is 'builtins.int'
+else:
+  reveal_type(x)  # E: Revealed type is 'Union[builtins.int, builtins.None]'
+[builtins fixtures/bool.py]
+
+[case testIfNotCases]
+from typing import Optional
+x = None  # type:  Optional[int]
+if not x:
+  reveal_type(x)  # E: Revealed type is 'Union[builtins.int, builtins.None]'
+else:
+  reveal_type(x)  # E: Revealed type is 'builtins.int'
+[builtins fixtures/bool.py]
+
+[case testIsNotNoneCases]
+from typing import Optional
+x = None  # type:  Optional[int]
+if x is not None:
+  reveal_type(x)  # E: Revealed type is 'builtins.int'
+else:
+  reveal_type(x)  # E: Revealed type is 'builtins.None'
+[builtins fixtures/bool.py]
+
+[case testIsNoneCases]
+from typing import Optional
+x = None  # type:  Optional[int]
+if x is None:
+  reveal_type(x)  # E: Revealed type is 'builtins.None'
+else:
+  reveal_type(x)  # E: Revealed type is 'builtins.int'
+[builtins fixtures/bool.py]
+
+[case testLambdaReturningNone]
+f = lambda: None
+x = f()
+
+[case testFunctionStillVoid]
+def f() -> None: pass
+f()
+x = f()  # E: "f" does not return a value
+
+[case testNoneArgumentType]
+def f(x: None) -> None: pass
+f(None)
+
+[case testInferOptionalFromDefaultNone]
+def f(x: int = None) -> None:
+  x + 1  # E: Unsupported left operand type for + (some union)
+f(None)
+[out]
+main: note: In function "f":
+
+[case testInferOptionalType]
+x = None
+x = 1
+reveal_type(x)  # E: Revealed type is 'Union[builtins.int, builtins.None]'
+
+[case testInferOptionalTypeFromOptional]
+from typing import Optional
+y = None  # type: Optional[int]
+x = None
+x = y
+reveal_type(x)  # E: Revealed type is 'Union[builtins.int, builtins.None]'
+
+[case testInferOptionalListType]
+x = [None]
+x.append(1)
+reveal_type(x)  # E: Revealed type is 'builtins.list[Union[builtins.int, builtins.None]]'
+[builtins fixtures/list.py]
+
+[case testInferNonOptionalListType]
+x = []
+x.append(1)
+x()  # E: List[int] not callable
+[builtins fixtures/list.py]
+
+[case testInferOptionalDictKeyValueTypes]
+x = {None: None}
+x["bar"] = 1
+reveal_type(x)  # E: Revealed type is 'builtins.dict[Union[builtins.str, builtins.None], Union[builtins.int, builtins.None]]'
+[builtins fixtures/dict.py]
+
+[case testInferNonOptionalDictType]
+x = {}
+x["bar"] = 1
+x()  # E: Dict[str, int] not callable
+[builtins fixtures/dict.py]
+
+[case testNoneClassVariable]
+from typing import Optional
+class C:
+    x = None  # type: int
+    def __init__(self) -> None:
+        self.x = 0
+
+[case testNoneClassVariableInInit]
+from typing import Optional
+class C:
+    x = None  # type: int
+    def __init__(self) -> None:
+        self.x = None  # E: Incompatible types in assignment (expression has type None, variable has type "int")
+[out]
+main: note: In member "__init__" of class "C":
+
+[case testMultipleAssignmentNoneClassVariableInInit]
+from typing import Optional
+class C:
+    x, y = None, None  # type: int, str
+    def __init__(self) -> None:
+        self.x = None  # E: Incompatible types in assignment (expression has type None, variable has type "int")
+        self.y = None  # E: Incompatible types in assignment (expression has type None, variable has type "str")
+[out]
+main: note: In member "__init__" of class "C":
+
+[case testOverloadWithNone]
+from typing import overload
+@overload
+def f(x: None) -> str: pass
+@overload
+def f(x: int) -> int: pass
+reveal_type(f(None))  # E: Revealed type is 'builtins.str'
+reveal_type(f(0))  # E: Revealed type is 'builtins.int'
diff --git a/mypy/test/data/check-tuples.test b/mypy/test/data/check-tuples.test
index 5af176f8ab27..7c03014fd5c8 100644
--- a/mypy/test/data/check-tuples.test
+++ b/mypy/test/data/check-tuples.test
@@ -289,7 +289,7 @@ a, b = None, None # type: (A, B)
 a1, b1 = a, a # type: (A, B)  # E: Incompatible types in assignment (expression has type "A", variable has type "B")
 a2, b2 = b, b # type: (A, B)  # E: Incompatible types in assignment (expression has type "B", variable has type "A")
 a3, b3 = a # type: (A, B)     # E: '__main__.A' object is not iterable
-a4, b4 = None # type: (A, B)  # E: ''None'' object is not iterable
+a4, b4 = None # type: (A, B)  # E: 'builtins.None' object is not iterable
 a5, b5 = a, b, a # type: (A, B)  # E: Too many values to unpack (2 expected, 3 provided)
 
 ax, bx = a, b # type: (A, B)
@@ -303,7 +303,7 @@ class B: pass
 a, b = None, None # type: (A, B)
 def f(): pass
 
-a, b = None # E: ''None'' object is not iterable
+a, b = None # E: 'builtins.None' object is not iterable
 a, b = a   # E: '__main__.A' object is not iterable
 a, b = f   # E: 'def () -> Any' object is not iterable
 
diff --git a/mypy/test/data/typexport-basic.test b/mypy/test/data/typexport-basic.test
index b284a35cdc1e..0264bc981fc1 100644
--- a/mypy/test/data/typexport-basic.test
+++ b/mypy/test/data/typexport-basic.test
@@ -232,7 +232,7 @@ NameExpr(6) : A
 NameExpr(6) : A
 MemberExpr(7) : A
 MemberExpr(7) : A
-MemberExpr(7) : Any
+MemberExpr(7) : A
 NameExpr(7) : A
 NameExpr(7) : A
 
diff --git a/mypy/test/testcheck.py b/mypy/test/testcheck.py
index d64f3a4dec36..62341282482e 100644
--- a/mypy/test/testcheck.py
+++ b/mypy/test/testcheck.py
@@ -19,6 +19,7 @@
 )
 from mypy.errors import CompileError
 
+from mypy import experiments
 
 # List of files that contain test case descriptions.
 files = [
@@ -57,6 +58,7 @@
     'check-flags.test',
     'check-incremental.test',
     'check-bound.test',
+    'check-optional.test',
     'check-fastparse.test',
 ]
 
@@ -72,12 +74,19 @@ def cases(self) -> List[DataDrivenTestCase]:
 
     def run_test(self, testcase: DataDrivenTestCase) -> None:
         incremental = 'Incremental' in testcase.name.lower() or 'incremental' in testcase.file
+        optional = 'optional' in testcase.file
         if incremental:
             # Incremental tests are run once with a cold cache, once with a warm cache.
             # Expect success on first run, errors from testcase.output (if any) on second run.
             self.clear_cache()
             self.run_test_once(testcase, 1)
             self.run_test_once(testcase, 2)
+        elif optional:
+            try:
+                experiments.STRICT_OPTIONAL = True
+                self.run_test_once(testcase)
+            finally:
+                experiments.STRICT_OPTIONAL = False
         else:
             self.run_test_once(testcase)
 
diff --git a/mypy/typeanal.py b/mypy/typeanal.py
index 6a7ef29cf9b1..b6cedd143711 100644
--- a/mypy/typeanal.py
+++ b/mypy/typeanal.py
@@ -5,7 +5,7 @@
 from mypy.types import (
     Type, UnboundType, TypeVarType, TupleType, UnionType, Instance, AnyType, CallableType,
     Void, NoneTyp, DeletedType, TypeList, TypeVarDef, TypeVisitor, StarType, PartialType,
-    EllipsisType, TypeType
+    EllipsisType, UninhabitedType, TypeType
 )
 from mypy.nodes import (
     BOUND_TVAR, TYPE_ALIAS, UNBOUND_IMPORTED,
@@ -16,6 +16,7 @@
 from mypy.exprtotype import expr_to_unanalyzed_type, TypeTranslationError
 from mypy.subtypes import satisfies_upper_bound
 from mypy import nodes
+from mypy import experiments
 
 
 type_constructors = {'typing.Tuple', 'typing.Union', 'typing.Callable', 'typing.Type'}
@@ -73,6 +74,11 @@ def __init__(self,
         self.fail = fail_func
 
     def visit_unbound_type(self, t: UnboundType) -> Type:
+        if t.optional:
+            t.optional = False
+            # We don't need to worry about double-wrapping Optionals or
+            # wrapping Anys: Union simplification will take care of that.
+            return UnionType.make_simplified_union([self.visit_unbound_type(t), NoneTyp()])
         sym = self.lookup(t.name, t)
         if sym is not None:
             if sym.node is None:
@@ -91,7 +97,13 @@ def visit_unbound_type(self, t: UnboundType) -> Type:
                                    tvar_expr.variance,
                                    t.line)
             elif fullname == 'builtins.None':
-                return Void()
+                if experiments.STRICT_OPTIONAL:
+                    if t.is_ret_type:
+                        return Void()
+                    else:
+                        return NoneTyp()
+                else:
+                    return Void()
             elif fullname == 'typing.Any':
                 return AnyType()
             elif fullname == 'typing.Tuple':
@@ -110,8 +122,11 @@ def visit_unbound_type(self, t: UnboundType) -> Type:
                     self.fail('Optional[...] must have exactly one type argument', t)
                     return AnyType()
                 items = self.anal_array(t.args)
-                # Currently Optional[t] is just an alias for t.
-                return items[0]
+                if experiments.STRICT_OPTIONAL:
+                    return UnionType.make_simplified_union([items[0], NoneTyp()])
+                else:
+                    # Without strict Optional checking Optional[t] is just an alias for t.
+                    return items[0]
             elif fullname == 'typing.Callable':
                 return self.analyze_callable_type(t)
             elif fullname == 'typing.Type':
@@ -172,6 +187,9 @@ def visit_void(self, t: Void) -> Type:
     def visit_none_type(self, t: NoneTyp) -> Type:
         return t
 
+    def visit_uninhabited_type(self, t: UninhabitedType) -> Type:
+        return t
+
     def visit_deleted_type(self, t: DeletedType) -> Type:
         return t
 
@@ -384,6 +402,9 @@ def visit_void(self, t: Void) -> None:
     def visit_none_type(self, t: NoneTyp) -> None:
         pass
 
+    def visit_uninhabited_type(self, t: UninhabitedType) -> None:
+        pass
+
     def visit_deleted_type(self, t: DeletedType) -> None:
         pass
 
diff --git a/mypy/types.py b/mypy/types.py
index 92b86593c992..9b1e93e27863 100644
--- a/mypy/types.py
+++ b/mypy/types.py
@@ -6,6 +6,8 @@
 import mypy.nodes
 from mypy.nodes import INVARIANT, SymbolNode
 
+from mypy import experiments
+
 
 T = TypeVar('T')
 
@@ -99,12 +101,23 @@ class UnboundType(Type):
 
     name = ''
     args = None  # type: List[Type]
+    # should this type be wrapped in an Optional?
+    optional = False
+    # is this type a return type?
+    is_ret_type = False
 
-    def __init__(self, name: str, args: List[Type] = None, line: int = -1) -> None:
+    def __init__(self,
+                 name: str,
+                 args: List[Type] = None,
+                 line: int = -1,
+                 optional: bool = False,
+                 is_ret_type: bool = False) -> None:
         if not args:
             args = []
         self.name = name
         self.args = args
+        self.optional = optional
+        self.is_ret_type = is_ret_type
         super().__init__(line)
 
     def accept(self, visitor: 'TypeVisitor[T]') -> T:
@@ -205,17 +218,51 @@ def deserialize(cls, data: JsonDict) -> 'Void':
         return Void()
 
 
+class UninhabitedType(Type):
+    """This type has no members.
+
+    This type is almost the bottom type, except it is not a subtype of Void.
+    With strict Optional checking, it is the only common subtype between all
+    other types, which allows `meet` to be well defined.  Without strict
+    Optional checking, NoneTyp fills this role.
+
+    In general, for any type T that isn't Void:
+        join(UninhabitedType, T) = T
+        meet(UninhabitedType, T) = UninhabitedType
+        is_subtype(UninhabitedType, T) = True
+    """
+
+    def __init__(self, line: int = -1) -> None:
+        super().__init__(line)
+
+    def accept(self, visitor: 'TypeVisitor[T]') -> T:
+        return visitor.visit_uninhabited_type(self)
+
+    def serialize(self) -> JsonDict:
+        return {'.class': 'UninhabitedType'}
+
+    @classmethod
+    def deserialize(cls, data: JsonDict) -> 'UninhabitedType':
+        assert data['.class'] == 'UninhabitedType'
+        return UninhabitedType()
+
+
 class NoneTyp(Type):
     """The type of 'None'.
 
-    This is only used internally during type inference.  Programs
-    cannot declare a variable of this type, and the type checker
-    refuses to infer this type for a variable. However, subexpressions
-    often have this type. Note that this is not used as the result
-    type when calling a function with a void type, even though
-    semantically such a function returns a None value; the void type
-    is used instead so that we can report an error if the caller tries
-    to do anything with the return value.
+    Without strict Optional checking:
+        This is only used internally during type inference.  Programs
+        cannot declare a variable of this type, and the type checker
+        refuses to infer this type for a variable. However, subexpressions
+        often have this type. Note that this is not used as the result
+        type when calling a function with a void type, even though
+        semantically such a function returns a None value; the void type
+        is used instead so that we can report an error if the caller tries
+        to do anything with the return value.
+
+    With strict Optional checking:
+        This type can be written by users as 'None', except as the return value
+        of a function, where 'None' means Void.
     """
 
     def __init__(self, line: int = -1) -> None:
@@ -683,7 +730,10 @@ def make_union(items: List[Type], line: int = -1) -> Type:
         elif len(items) == 1:
             return items[0]
         else:
-            return Void()
+            if experiments.STRICT_OPTIONAL:
+                return UninhabitedType()
+            else:
+                return Void()
 
     @staticmethod
     def make_simplified_union(items: List[Type], line: int = -1) -> Type:
@@ -754,10 +804,15 @@ class PartialType(Type):
     # None for the 'None' partial type; otherwise a generic class
     type = None  # type: Optional[mypy.nodes.TypeInfo]
     var = None  # type: mypy.nodes.Var
+    inner_types = None  # type: List[Type]
 
-    def __init__(self, type: Optional['mypy.nodes.TypeInfo'], var: 'mypy.nodes.Var') -> None:
+    def __init__(self,
+                 type: Optional['mypy.nodes.TypeInfo'],
+                 var: 'mypy.nodes.Var',
+                 inner_types: List[Type]) -> None:
         self.type = type
         self.var = var
+        self.inner_types = inner_types
 
     def accept(self, visitor: 'TypeVisitor[T]') -> T:
         return visitor.visit_partial_type(self)
@@ -869,6 +924,10 @@ def visit_void(self, t: Void) -> T:
     def visit_none_type(self, t: NoneTyp) -> T:
         pass
 
+    @abstractmethod
+    def visit_uninhabited_type(self, t: UninhabitedType) -> T:
+        pass
+
     def visit_erased_type(self, t: ErasedType) -> T:
         raise self._notimplemented_helper('erased_type')
 
@@ -939,6 +998,9 @@ def visit_void(self, t: Void) -> Type:
     def visit_none_type(self, t: NoneTyp) -> Type:
         return t
 
+    def visit_uninhabited_type(self, t: UninhabitedType) -> Type:
+        return t
+
     def visit_erased_type(self, t: ErasedType) -> Type:
         return t
 
@@ -1025,8 +1087,11 @@ def visit_void(self, t):
         return 'void'
 
     def visit_none_type(self, t):
-        # Include quotes to make this distinct from the None value.
-        return "'None'"
+        # Fully qualify to make this distinct from the None value.
+        return "builtins.None"
+
+    def visit_uninhabited_type(self, t):
+        return "<uninhabited>"
 
     def visit_erased_type(self, t):
         return "<Erased>"
@@ -1172,6 +1237,9 @@ def visit_any(self, t: AnyType) -> bool:
     def visit_void(self, t: Void) -> bool:
         return self.default
 
+    def visit_uninhabited_type(self, t: UninhabitedType) -> bool:
+        return self.default
+
     def visit_none_type(self, t: NoneTyp) -> bool:
         return self.default