diff --git a/lib-typing/2.7/typing.py b/lib-typing/2.7/typing.py
index 7d298ae52693..44d884417dd7 100644
--- a/lib-typing/2.7/typing.py
+++ b/lib-typing/2.7/typing.py
@@ -156,7 +156,7 @@ def NamedTuple(typename, fields):
 
 
 class TypeVar(object):
-    def __init__(self, name, *values):
+    def __init__(self, name, *values, **kwargs):
         self.name = name
         if not values:
             values = None
@@ -204,6 +204,7 @@ def overload(func):
 T = TypeVar('T')
 KT = TypeVar('KT')
 VT = TypeVar('VT')
+VT_co = TypeVar('VT_co', covariant=True)
 
 
 class SupportsInt(_Protocol):
@@ -231,7 +232,7 @@ class Sized(_Protocol):
     def __len__(self): pass
 
 
-class Container(_Protocol[T]):
+class Container(_Protocol[VT_co]):
     @abstractmethod
     def __contains__(self, x): pass
 
@@ -241,12 +242,12 @@ class Iterable(_Protocol[T]):
     def __iter__(self): pass
 
 
-class Iterator(Iterable[T], _Protocol[T]):
+class Iterator(Iterable[VT_co], _Protocol[VT_co]):
     @abstractmethod
     def next(self): pass
 
 
-class Sequence(Sized, Iterable[T], Container[T], Generic[T]):
+class Sequence(Sized, Iterable[VT_co], Container[VT_co], Generic[VT_co]):
     @abstractmethod
     def __getitem__(self, i): pass
 
@@ -267,7 +268,7 @@ def count(self, x): pass
     Sequence.register(t)
 
 
-class AbstractSet(Sized, Iterable[T], Generic[T]):
+class AbstractSet(Sized, Iterable[VT_co], Generic[VT_co]):
     @abstractmethod
     def __contains__(self, x): pass
     @abstractmethod
diff --git a/lib-typing/3.2/typing.py b/lib-typing/3.2/typing.py
index 38e07ad50b75..e399d0d6ebf4 100644
--- a/lib-typing/3.2/typing.py
+++ b/lib-typing/3.2/typing.py
@@ -1374,7 +1374,7 @@ class MutableSet(AbstractSet[T], extra=collections_abc.MutableSet):
     pass
 
 
-class Mapping(Sized, Iterable[KT_co], Container[KT_co], Generic[KT_co, VT_co],
+class Mapping(Sized, Iterable[KT], Container[KT], Generic[KT, VT_co],
               extra=collections_abc.Mapping):
     pass
 
diff --git a/mypy/checkmember.py b/mypy/checkmember.py
index f5f96dc87b19..d176a807c2f6 100644
--- a/mypy/checkmember.py
+++ b/mypy/checkmember.py
@@ -235,8 +235,8 @@ def add_class_tvars(t: Type, info: TypeInfo, is_classmethod: bool,
                     builtin_type: Callable[[str], Instance]) -> Type:
     if isinstance(t, CallableType):
         # TODO: Should we propagate type variable values?
-        vars = [TypeVarDef(n, i + 1, None, builtin_type('builtins.object'))
-                for i, n in enumerate(info.type_vars)]
+        vars = [TypeVarDef(n, i + 1, None, builtin_type('builtins.object'), tv.variance)
+                for (i, n), tv in zip(enumerate(info.type_vars), info.defn.type_vars)]
         arg_types = t.arg_types
         arg_kinds = t.arg_kinds
         arg_names = t.arg_names
@@ -290,7 +290,7 @@ def class_callable(init_type: CallableType, info: TypeInfo, type_type: Instance)
     """Create a type object type based on the signature of __init__."""
     variables = []  # type: List[TypeVarDef]
     for i, tvar in enumerate(info.defn.type_vars):
-        variables.append(TypeVarDef(tvar.name, i + 1, tvar.values, tvar.upper_bound))
+        variables.append(TypeVarDef(tvar.name, i + 1, tvar.values, tvar.upper_bound, tvar.variance))
 
     initvars = init_type.variables
     variables.extend(initvars)
@@ -319,7 +319,7 @@ def visit_type_var(self, t: TypeVarType) -> Type:
         if t.id < 0:
             return t
         else:
-            return TypeVarType(t.name, -t.id - self.num_func_tvars, t.values, t.upper_bound)
+            return TypeVarType(t.name, -t.id - self.num_func_tvars, t.values, t.upper_bound, t.variance)
 
     def translate_variables(self,
                             variables: List[TypeVarDef]) -> List[TypeVarDef]:
@@ -329,7 +329,7 @@ def translate_variables(self,
         for v in variables:
             if v.id > 0:
                 items.append(TypeVarDef(v.name, -v.id - self.num_func_tvars,
-                                        v.values, v.upper_bound))
+                                        v.values, v.upper_bound, v.variance))
             else:
                 items.append(v)
         return items
diff --git a/mypy/join.py b/mypy/join.py
index 3d9e6cb9b6f9..a5c0319c9abf 100644
--- a/mypy/join.py
+++ b/mypy/join.py
@@ -8,7 +8,7 @@
     UnionType, FunctionLike
 )
 from mypy.maptype import map_instance_to_supertype
-from mypy.subtypes import is_subtype, is_equivalent
+from mypy.subtypes import is_subtype, is_equivalent, is_subtype_ignoring_tvars
 
 
 def join_simple(declaration: Type, s: Type, t: Type) -> Type:
@@ -179,7 +179,7 @@ def join_instances(t: Instance, s: Instance) -> Type:
     if t.type == s.type:
         # Simplest case: join two types with the same base type (but
         # potentially different arguments).
-        if is_subtype(t, s):
+        if is_subtype(t, s) or is_subtype(s, t):
             # Compatible; combine type arguments.
             args = []  # type: List[Type]
             for i in range(len(t.args)):
@@ -188,7 +188,7 @@ def join_instances(t: Instance, s: Instance) -> Type:
         else:
             # Incompatible; return trivial result object.
             return object_from_instance(t)
-    elif t.type.bases and is_subtype(t, s):
+    elif t.type.bases and is_subtype_ignoring_tvars(t, s):
         return join_instances_via_supertype(t, s)
     else:
         # Now t is not a subtype of s, and t != s. Now s could be a subtype
diff --git a/mypy/meet.py b/mypy/meet.py
index 92fe9e7b6db0..76162fecf1c4 100644
--- a/mypy/meet.py
+++ b/mypy/meet.py
@@ -23,7 +23,7 @@ def meet_types(s: Type, t: Type) -> Type:
     return t.accept(TypeMeetVisitor(s))
 
 
-def meet_simple(s: Type, t: Type, default_right: bool = True) -> Type:
+def meet_simple(s: Type, t: Type, default_right: bool=True) -> Type:
     if s == t:
         return s
     if isinstance(s, UnionType):
@@ -131,7 +131,7 @@ def visit_instance(self, t: Instance) -> Type:
         if isinstance(self.s, Instance):
             si = cast(Instance, self.s)
             if t.type == si.type:
-                if is_subtype(t, self.s):
+                if is_subtype(t, self.s) or is_subtype(self.s, t):
                     # Combine type arguments. We could have used join below
                     # equivalently.
                     args = []  # type: List[Type]
diff --git a/mypy/nodes.py b/mypy/nodes.py
index ea9e3cced71f..5c8205e34945 100644
--- a/mypy/nodes.py
+++ b/mypy/nodes.py
@@ -1292,6 +1292,10 @@ def accept(self, visitor: NodeVisitor[T]) -> T:
         return visitor.visit_type_application(self)
 
 
+INVARIANT = 0  # type: int
+COVARIANT = 1  # type: int
+CONTRAVARIANT = 2  # type: int
+
 class TypeVarExpr(SymbolNode):
     """Type variable expression TypeVar(...)."""
 
@@ -1300,12 +1304,15 @@ class TypeVarExpr(SymbolNode):
     # Value restriction: only types in the list are valid as values. If the
     # list is empty, there is no restriction.
     values = None  # type: List[mypy.types.Type]
+    variance = INVARIANT
 
     def __init__(self, name: str, fullname: str,
-                 values: List['mypy.types.Type']) -> None:
+                 values: List['mypy.types.Type'],
+                 variance: int=INVARIANT) -> None:
         self._name = name
         self._fullname = fullname
         self.values = values
+        self.variance = variance
 
     def name(self) -> str:
         return self._name
diff --git a/mypy/semanal.py b/mypy/semanal.py
index 68d6585e5a89..02432b55ec85 100644
--- a/mypy/semanal.py
+++ b/mypy/semanal.py
@@ -58,7 +58,8 @@
     StrExpr, PrintStmt, ConditionalExpr, PromoteExpr,
     ComparisonExpr, StarExpr, ARG_POS, ARG_NAMED, MroError, type_aliases,
     YieldFromStmt, YieldFromExpr, NamedTupleExpr, NonlocalDecl,
-    SetComprehension, DictionaryComprehension, TYPE_ALIAS, TypeAliasExpr
+    SetComprehension, DictionaryComprehension, TYPE_ALIAS, TypeAliasExpr,
+    COVARIANT, CONTRAVARIANT, INVARIANT
 )
 from mypy.visitor import NodeVisitor
 from mypy.traverser import TraverserVisitor
@@ -250,37 +251,37 @@ def update_function_type_variables(self, defn: FuncDef) -> None:
             functype = cast(CallableType, defn.type)
             typevars = self.infer_type_variables(functype)
             # Do not define a new type variable if already defined in scope.
-            typevars = [(tvar, values) for tvar, values in typevars
-                        if not self.is_defined_type_var(tvar, defn)]
+            typevars = [(name, tvar) for name, tvar in typevars
+                        if not self.is_defined_type_var(name, defn)]
             if typevars:
-                defs = [TypeVarDef(tvar[0], -i - 1, tvar[1], self.object_type())
+                defs = [TypeVarDef(tvar[0], -i - 1, tvar[1].values, self.object_type(), tvar[1].variance)
                         for i, tvar in enumerate(typevars)]
                 functype.variables = defs
 
     def infer_type_variables(self,
-                             type: CallableType) -> List[Tuple[str, List[Type]]]:
+                             type: CallableType) -> List[Tuple[str, TypeVarExpr]]:
         """Return list of unique type variables referred to in a callable."""
         names = []  # type: List[str]
-        values = []  # type: List[List[Type]]
+        tvars = []  # type: List[TypeVarExpr]
         for arg in type.arg_types + [type.ret_type]:
-            for tvar, vals in self.find_type_variables_in_type(arg):
-                if tvar not in names:
-                    names.append(tvar)
-                    values.append(vals)
-        return list(zip(names, values))
+            for name, tvar_expr in self.find_type_variables_in_type(arg):
+                if name not in names:
+                    names.append(name)
+                    tvars.append(tvar_expr)
+        return list(zip(names, tvars))
 
     def find_type_variables_in_type(
-            self, type: Type) -> List[Tuple[str, List[Type]]]:
-        """Return a list of all unique type variable references in an non-analyzed type.
+            self, type: Type) -> List[Tuple[str, TypeVarExpr]]:
+        """Return a list of all unique type variable references in type.
 
         This effectively does partial name binding, results of which are mostly thrown away.
         """
-        result = []  # type: List[Tuple[str, List[Type]]]
+        result = []  # type: List[Tuple[str, TypeVarExpr]]
         if isinstance(type, UnboundType):
             name = type.name
             node = self.lookup_qualified(name, type)
             if node and node.kind == UNBOUND_TVAR:
-                result.append((name, cast(TypeVarExpr, node.node).values))
+                result.append((name, cast(TypeVarExpr, node.node)))
             for arg in type.args:
                 result.extend(self.find_type_variables_in_type(arg))
         elif isinstance(type, TypeList):
@@ -553,10 +554,9 @@ def clean_up_bases_and_infer_type_variables(self, defn: ClassDef) -> None:
                 if type_vars:
                     self.fail('Duplicate Generic in bases', defn)
                 removed.append(i)
-                for j, tvar in enumerate(tvars):
-                    name, values = tvar
-                    type_vars.append(TypeVarDef(name, j + 1, values,
-                                                self.object_type()))
+                for j, (name, tvar_expr) in enumerate(tvars):
+                    type_vars.append(TypeVarDef(name, j + 1, tvar_expr.values,
+                                                self.object_type(), tvar_expr.variance))
         if type_vars:
             defn.type_vars = type_vars
             if defn.info:
@@ -564,8 +564,7 @@ def clean_up_bases_and_infer_type_variables(self, defn: ClassDef) -> None:
         for i in reversed(removed):
             del defn.base_type_exprs[i]
 
-    def analyze_typevar_declaration(self, t: Type) -> List[Tuple[str,
-                                                                 List[Type]]]:
+    def analyze_typevar_declaration(self, t: Type) -> List[Tuple[str, TypeVarExpr]]:
         if not isinstance(t, UnboundType):
             return None
         unbound = cast(UnboundType, t)
@@ -573,7 +572,7 @@ def analyze_typevar_declaration(self, t: Type) -> List[Tuple[str,
         if sym is None:
             return None
         if sym.node.fullname() == 'typing.Generic':
-            tvars = []  # type: List[Tuple[str, List[Type]]]
+            tvars = []  # type: List[Tuple[str, TypeVarExpr]]
             for arg in unbound.args:
                 tvar = self.analyze_unbound_tvar(arg)
                 if tvar:
@@ -584,13 +583,13 @@ def analyze_typevar_declaration(self, t: Type) -> List[Tuple[str,
             return tvars
         return None
 
-    def analyze_unbound_tvar(self, t: Type) -> Tuple[str, List[Type]]:
+    def analyze_unbound_tvar(self, t: Type) -> Tuple[str, TypeVarExpr]:
         if not isinstance(t, UnboundType):
             return None
         unbound = cast(UnboundType, t)
         sym = self.lookup_qualified(unbound.name, unbound)
         if sym is not None and sym.kind == UNBOUND_TVAR:
-            return unbound.name, cast(TypeVarExpr, sym.node).values[:]
+            return unbound.name, cast(TypeVarExpr, sym.node)
         return None
 
     def setup_class_def_analysis(self, defn: ClassDef) -> None:
@@ -713,10 +712,9 @@ def bind_class_type_variables_in_symbol_table(
             self, info: TypeInfo) -> List[SymbolTableNode]:
         vars = info.type_vars
         nodes = []  # type: List[SymbolTableNode]
-        if vars:
-            for i in range(len(vars)):
-                node = self.bind_type_var(vars[i], i + 1, info)
-                nodes.append(node)
+        for index, var in enumerate(vars, 1):
+            node = self.bind_type_var(var, index, info)
+            nodes.append(node)
         return nodes
 
     def visit_import(self, i: Import) -> None:
@@ -1031,57 +1029,121 @@ def store_declared_types(self, lvalue: Node, typ: Type) -> None:
 
     def process_typevar_declaration(self, s: AssignmentStmt) -> None:
         """Check if s declares a TypeVar; it yes, store it in symbol table."""
-        if len(s.lvalues) != 1 or not isinstance(s.lvalues[0], NameExpr):
-            return
-        if not isinstance(s.rvalue, CallExpr):
-            return
-        call = cast(CallExpr, s.rvalue)
-        if not isinstance(call.callee, RefExpr):
-            return
-        callee = cast(RefExpr, call.callee)
-        if callee.fullname != 'typing.TypeVar':
-            return
-        # TODO Share code with check_argument_count in checkexpr.py?
-        if len(call.args) < 1:
-            self.fail("Too few arguments for TypeVar()", s)
-            return
-        if call.arg_kinds != [ARG_POS] * len(call.arg_kinds):
-            if call.arg_kinds == [ARG_POS, ARG_NAMED] and call.arg_names[1] == 'values':
-                # Probably using obsolete syntax with values=(...). Explain the current syntax.
-                self.fail("TypeVar 'values' argument not supported", s)
-                self.fail("Use TypeVar('T', t, ...) instead of TypeVar('T', values=(t, ...))",
-                          s)
-            else:
-                self.fail("Unexpected arguments to TypeVar()", s)
-            return
-        if not isinstance(call.args[0], StrExpr):
-            self.fail("TypeVar() expects a string literal argument", s)
+        call = self.get_typevar_declaration(s)
+        if not call:
             return
+
         lvalue = cast(NameExpr, s.lvalues[0])
         name = lvalue.name
-        if cast(StrExpr, call.args[0]).value != name:
-            self.fail("Unexpected TypeVar() argument value", s)
-            return
         if not lvalue.is_def:
             if s.type:
                 self.fail("Cannot declare the type of a type variable", s)
             else:
                 self.fail("Cannot redefine '%s' as a type variable" % name, s)
             return
-        if len(call.args) > 1:
-            # Analyze enumeration of type variable values.
-            values = self.analyze_types(call.args[1:])
-        else:
-            # Type variables can refer to an arbitrary type.
-            values = []
+
+        if not self.check_typevar_name(call, name, s):
+            return
+
+        # Constraining types
+        n_values = call.arg_kinds[1:].count(ARG_POS)
+        values = self.analyze_types(call.args[1:1+n_values])
+
+        variance = self.process_typevar_parameters(call.args[1+n_values:],
+                                                   call.arg_names[1+n_values:],
+                                                   call.arg_kinds[1+n_values:],
+                                                   s)
+        if variance is None:
+            return
+
         # Yes, it's a valid type variable definition! Add it to the symbol table.
         node = self.lookup(name, s)
         node.kind = UNBOUND_TVAR
-        TypeVar = TypeVarExpr(name, node.fullname, values)
+        TypeVar = TypeVarExpr(name, node.fullname, values, variance)
         TypeVar.line = call.line
         call.analyzed = TypeVar
         node.node = TypeVar
 
+    def check_typevar_name(self, call: CallExpr, name: str, context: Context) -> bool:
+        if len(call.args) < 1:
+            self.fail("Too few arguments for TypeVar()", context)
+            return False
+        if not isinstance(call.args[0], StrExpr) or not call.arg_kinds[0] == ARG_POS:
+            self.fail("TypeVar() expects a string literal as first argument", context)
+            return False
+        if cast(StrExpr, call.args[0]).value != name:
+            self.fail("Unexpected TypeVar() argument value", context)
+            return False
+        return True
+
+    def get_typevar_declaration(self, s: AssignmentStmt) -> Optional[CallExpr]:
+        """ Returns the TypeVar() call expression if `s` is a type var declaration
+        or None otherwise.
+        """
+        if len(s.lvalues) != 1 or not isinstance(s.lvalues[0], NameExpr):
+            return None
+        if not isinstance(s.rvalue, CallExpr):
+            return None
+        call = cast(CallExpr, s.rvalue)
+        if not isinstance(call.callee, RefExpr):
+            return None
+        callee = cast(RefExpr, call.callee)
+        if callee.fullname != 'typing.TypeVar':
+            return None
+        return call
+
+    def process_typevar_parameters(self, args: List[Node],
+                                   names: List[Optional[str]],
+                                   kinds: List[int],
+                                   context: Context) -> Optional[int]:
+        covariant = False
+        contravariant = False
+        for param_value, param_name, param_kind in zip(args, names, kinds):
+            if not param_kind == ARG_NAMED:
+                self.fail("Unexpected argument to TypeVar()", context)
+                return None
+            if param_name == 'covariant':
+                if isinstance(param_value, NameExpr):
+                    if param_value.name == 'True':
+                        covariant = True
+                    else:
+                        self.fail("TypeVar 'covariant' may only be 'True'", context)
+                        return None
+                else:
+                    self.fail("TypeVar 'covariant' may only be 'True'", context)
+                    return None
+            elif param_name == 'contravariant':
+                if isinstance(param_value, NameExpr):
+                    if param_value.name == 'True':
+                        contravariant = True
+                    else:
+                        self.fail("TypeVar 'contravariant' may only be 'True'", context)
+                        return None
+                else:
+                    self.fail("TypeVar 'contravariant' may only be 'True'", context)
+                    return None
+            elif param_name == 'bound':
+                self.fail("TypeVar 'bound' argument not supported yet.", context)
+                return None
+            elif param_name == 'values':
+                # Probably using obsolete syntax with values=(...). Explain the current syntax.
+                self.fail("TypeVar 'values' argument not supported", context)
+                self.fail("Use TypeVar('T', t, ...) instead of TypeVar('T', values=(t, ...))",
+                          context)
+                return None
+            else:
+                self.fail("Unexpected argument to TypeVar(): {}".format(param_name), context)
+                return None
+        if covariant and contravariant:
+            self.fail("TypeVar cannot be both covariant and contravariant.", context)
+            return None
+        elif covariant:
+            return COVARIANT
+        elif contravariant:
+            return CONTRAVARIANT
+        else:
+            return INVARIANT
+
     def process_namedtuple_definition(self, s: AssignmentStmt) -> None:
         """Check if s defines a namedtuple; if yes, store the definition in symbol table."""
         if len(s.lvalues) != 1 or not isinstance(s.lvalues[0], NameExpr):
@@ -2022,7 +2084,8 @@ def self_type(typ: TypeInfo) -> Union[Instance, TupleType]:
     for i in range(len(typ.type_vars)):
         tv.append(TypeVarType(typ.type_vars[i], i + 1,
                           typ.defn.type_vars[i].values,
-                          typ.defn.type_vars[i].upper_bound))
+                          typ.defn.type_vars[i].upper_bound,
+                          typ.defn.type_vars[i].variance))
     inst = Instance(typ, tv)
     if typ.tuple_type is None:
         return inst
diff --git a/mypy/strconv.py b/mypy/strconv.py
index 39303971b987..677dfecd4efa 100644
--- a/mypy/strconv.py
+++ b/mypy/strconv.py
@@ -382,6 +382,8 @@ def visit_type_application(self, o):
         return self.dump([o.expr, ('Types', o.types)], o)
 
     def visit_type_var_expr(self, o):
+        if o.variance == mypy.nodes.COVARIANT:
+            return self.dump([('Variance', 'COVARIANT')], o)
         if o.values:
             return self.dump([('Values', o.values)], o)
         else:
diff --git a/mypy/subtypes.py b/mypy/subtypes.py
index b09358d1c4e0..80203f5a37e5 100644
--- a/mypy/subtypes.py
+++ b/mypy/subtypes.py
@@ -1,4 +1,4 @@
-from typing import cast, List, Dict
+from typing import cast, List, Dict, Callable
 
 from mypy.types import (
     Type, AnyType, UnboundType, TypeVisitor, ErrorType, Void, NoneTyp,
@@ -8,42 +8,62 @@
 import mypy.applytype
 import mypy.constraints
 from mypy import messages, sametypes
-from mypy.nodes import TypeInfo
-from mypy.expandtype import expand_type
+from mypy.nodes import CONTRAVARIANT, COVARIANT
 from mypy.maptype import map_instance_to_supertype
 
 
-def is_immutable(t: Instance) -> bool:
-    # TODO: The name is confusing, since the values need not be immutable.
-    return t.type.fullname() in ('typing.Iterable',
-                                 'typing.Sequence',
-                                 'typing.Reversible',
-                                 )
+TypeParameterChecker = Callable[[Type, Type, int], bool]
 
 
-def is_subtype(left: Type, right: Type) -> bool:
+def check_type_parameter(lefta: Type, righta: Type, variance: int) -> bool:
+    if variance == COVARIANT:
+        return is_subtype(lefta, righta, check_type_parameter)
+    elif variance == CONTRAVARIANT:
+        return is_subtype(righta, lefta, check_type_parameter)
+    else:
+        return is_equivalent(lefta, righta, check_type_parameter)
+
+
+def is_subtype(left: Type, right: Type,
+               type_parameter_checker: TypeParameterChecker=check_type_parameter) -> bool:
     """Is 'left' subtype of 'right'?
 
     Also consider Any to be a subtype of any type, and vice versa. This
     recursively applies to components of composite types (List[int] is subtype
     of List[Any], for example).
+
+    type_parameter_checker is used to check the type parameters (for example,
+    A with B in is_subtype(C[A], C[B]). The default checks for subtype relation
+    between the type arguments (e.g., A and B), taking the variance of the
+    type var into account.
     """
     if (isinstance(right, AnyType) or isinstance(right, UnboundType)
             or isinstance(right, ErasedType)):
         return True
     elif isinstance(right, UnionType) and not isinstance(left, UnionType):
-        return any(is_subtype(left, item) for item in cast(UnionType, right).items)
+        return any(is_subtype(left, item, type_parameter_checker)
+                   for item in cast(UnionType, right).items)
     else:
-        return left.accept(SubtypeVisitor(right))
+        return left.accept(SubtypeVisitor(right, type_parameter_checker))
+
+
+def is_subtype_ignoring_tvars(left: Type, right: Type) -> bool:
+    def ignore_tvars(s: Type, t: Type, v: int) -> bool:
+        return True
+    return is_subtype(left, right, ignore_tvars)
 
 
-def is_equivalent(a: Type, b: Type) -> bool:
-    return is_subtype(a, b) and is_subtype(b, a)
+def is_equivalent(a: Type, b: Type,
+                  type_parameter_checker=check_type_parameter) -> bool:
+    return is_subtype(a, b, type_parameter_checker) and is_subtype(b, a, type_parameter_checker)
 
 
 class SubtypeVisitor(TypeVisitor[bool]):
-    def __init__(self, right: Type) -> None:
+
+    def __init__(self, right: Type,
+                 type_parameter_checker: TypeParameterChecker) -> None:
         self.right = right
+        self.check_type_parameter = type_parameter_checker
 
     # visit_x(left) means: is left (which is an instance of X) a subtype of
     # right?
@@ -73,7 +93,8 @@ def visit_instance(self, left: Instance) -> bool:
         right = self.right
         if isinstance(right, Instance):
             if left.type._promote and is_subtype(left.type._promote,
-                                                 self.right):
+                                                 self.right,
+                                                 self.check_type_parameter):
                 return True
             rname = right.type.fullname()
             if not left.type.has_base(rname) and rname != 'builtins.object':
@@ -81,13 +102,10 @@ def visit_instance(self, left: Instance) -> bool:
 
             # Map left type to corresponding right instances.
             t = map_instance_to_supertype(left, right.type)
-            if not is_immutable(right):
-                result = all(is_equivalent(ta, ra) for (ta, ra) in
-                             zip(t.args, right.args))
-            else:
-                result = all(is_subtype(ta, ra) for (ta, ra) in
-                             zip(t.args, right.args))
-            return result
+
+            return all(self.check_type_parameter(lefta, righta, tvar.variance)
+                       for lefta, righta, tvar in
+                       zip(t.args, right.args, right.type.defn.type_vars))
         else:
             return False
 
@@ -103,7 +121,8 @@ def visit_callable_type(self, left: CallableType) -> bool:
         if isinstance(right, CallableType):
             return is_callable_subtype(left, right)
         elif isinstance(right, Overloaded):
-            return all(is_subtype(left, item) for item in right.items())
+            return all(is_subtype(left, item, self.check_type_parameter)
+                       for item in right.items())
         elif is_named_instance(right, 'builtins.object'):
             return True
         elif (is_named_instance(right, 'builtins.type') and
@@ -128,9 +147,9 @@ def visit_tuple_type(self, left: TupleType) -> bool:
             if len(left.items) != len(right.items):
                 return False
             for i in range(len(left.items)):
-                if not is_subtype(left.items[i], right.items[i]):
+                if not is_subtype(left.items[i], right.items[i], self.check_type_parameter):
                     return False
-            if not is_subtype(left.fallback, right.fallback):
+            if not is_subtype(left.fallback, right.fallback, self.check_type_parameter):
                 return False
             return True
         else:
@@ -143,7 +162,7 @@ def visit_overloaded(self, left: Overloaded) -> bool:
         elif isinstance(right, CallableType) or is_named_instance(
                 right, 'builtins.type'):
             for item in left.items():
-                if is_subtype(item, right):
+                if is_subtype(item, right, self.check_type_parameter):
                     return True
             return False
         elif isinstance(right, Overloaded):
@@ -151,7 +170,7 @@ def visit_overloaded(self, left: Overloaded) -> bool:
             if len(left.items()) != len(right.items()):
                 return False
             for i in range(len(left.items())):
-                if not is_subtype(left.items()[i], right.items()[i]):
+                if not is_subtype(left.items()[i], right.items()[i], self.check_type_parameter):
                     return False
             return True
         elif isinstance(right, UnboundType):
@@ -160,7 +179,8 @@ def visit_overloaded(self, left: Overloaded) -> bool:
             return False
 
     def visit_union_type(self, left: UnionType) -> bool:
-        return all(is_subtype(item, self.right) for item in left.items)
+        return all(is_subtype(item, self.right, self.check_type_parameter)
+                   for item in left.items)
 
 
 def is_callable_subtype(left: CallableType, right: CallableType,
@@ -271,13 +291,20 @@ def is_proper_subtype(t: Type, s: Type) -> bool:
         if isinstance(s, Instance):
             if not t.type.has_base(s.type.fullname()):
                 return False
+
+            def check_argument(left: Type, right: Type, variance: int) -> bool:
+                if variance == COVARIANT:
+                    return is_proper_subtype(left, right)
+                elif variance == CONTRAVARIANT:
+                    return is_proper_subtype(right, left)
+                else:
+                    return sametypes.is_same_type(left, right)
+
+            # Map left type to corresponding right instances.
             t = map_instance_to_supertype(t, s.type)
-            if not is_immutable(s):
-                return all(sametypes.is_same_type(ta, ra) for (ta, ra) in
-                           zip(t.args, s.args))
-            else:
-                return all(is_proper_subtype(ta, ra) for (ta, ra) in
-                           zip(t.args, s.args))
+
+            return all(check_argument(ta, ra, tvar.variance) for ta, ra, tvar in
+                       zip(t.args, s.args, s.type.defn.type_vars))
         return False
     else:
         return sametypes.is_same_type(t, s)
diff --git a/mypy/test/data/check-generic-subtyping.test b/mypy/test/data/check-generic-subtyping.test
index a46aebf00817..792d7e5b76b6 100644
--- a/mypy/test/data/check-generic-subtyping.test
+++ b/mypy/test/data/check-generic-subtyping.test
@@ -613,3 +613,64 @@ n, n = Nums()
 s, s = Nums() # E: Incompatible types in assignment (expression has type "int", variable has type "str")
 [builtins fixtures/for.py]
 [out]
+
+
+-- Variance
+-- --------
+
+[case testCovariant]
+from typing import TypeVar, Generic
+True = 1
+
+T = TypeVar('T', covariant=True)
+
+class G(Generic[T]): pass
+class A: pass
+class B(A): pass
+class C(B): pass
+
+a = None  # type: G[A]
+b = None  # type: G[B]
+c = None  # type: G[C]
+
+b = a  # E: Incompatible types in assignment (expression has type G[A], variable has type G[B])
+b = c
+[out]
+
+[case testContravariant]
+from typing import TypeVar, Generic
+True = 1
+
+T = TypeVar('T', contravariant=True)
+
+class G(Generic[T]): pass
+class A: pass
+class B(A): pass
+class C(B): pass
+
+a = None  # type: G[A]
+b = None  # type: G[B]
+c = None  # type: G[C]
+
+b = a
+b = c  # E: Incompatible types in assignment (expression has type G[C], variable has type G[B])
+[out]
+
+[case testInvariant]
+from typing import TypeVar, Generic
+True = 1
+
+T = TypeVar('T')  # invariant (default)
+
+class G(Generic[T]): pass
+class A: pass
+class B(A): pass
+class C(B): pass
+
+a = None  # type: G[A]
+b = None  # type: G[B]
+c = None  # type: G[C]
+
+b = a  # E: Incompatible types in assignment (expression has type G[A], variable has type G[B])
+b = c  # E: Incompatible types in assignment (expression has type G[C], variable has type G[B])
+[out]
diff --git a/mypy/test/data/pythoneval.test b/mypy/test/data/pythoneval.test
index 159343105740..466da8fd1386 100644
--- a/mypy/test/data/pythoneval.test
+++ b/mypy/test/data/pythoneval.test
@@ -37,7 +37,7 @@ f()
 {1: 3} typing.Sequence[+T_co] False
 <str_iterator object at 0x...> typing.Iterator[+T_co] True
 'x' typing.Iterable[+T_co] True
-{} typing.Mapping[+KT_co, +VT_co] True
+{} typing.Mapping[~KT, +VT_co] True
 {1} typing.AbstractSet[+T_co] True
 
 [case testSized]
diff --git a/mypy/test/data/semanal-errors.test b/mypy/test/data/semanal-errors.test
index 61d7af0c76fc..dd886e66b4c4 100644
--- a/mypy/test/data/semanal-errors.test
+++ b/mypy/test/data/semanal-errors.test
@@ -1055,17 +1055,17 @@ class A(metaclass=f): pass # E: Invalid metaclass 'f'
 [case testInvalidTypevarArguments]
 from typing import TypeVar
 a = TypeVar()       # E: Too few arguments for TypeVar()
-b = TypeVar(x='b')  # E: Unexpected arguments to TypeVar()
-c = TypeVar(1)      # E: TypeVar() expects a string literal argument
+b = TypeVar(x='b')  # E: TypeVar() expects a string literal as first argument
+c = TypeVar(1)      # E: TypeVar() expects a string literal as first argument
 d = TypeVar('D')    # E: Unexpected TypeVar() argument value
-e = TypeVar('e', int, str, x=1) # E: Unexpected arguments to TypeVar()
+e = TypeVar('e', int, str, x=1) # E: Unexpected argument to TypeVar(): x
 f = TypeVar('f', (int, str)) # E: Type expected
-g = TypeVar('g', x=(int, str)) # E: Unexpected arguments to TypeVar()
+g = TypeVar('g', x=(int, str)) # E: Unexpected argument to TypeVar(): x
 [out]
 
 [case testInvalidTypevarValues]
 from typing import TypeVar
-b = TypeVar('b', *[int]) # E: Unexpected arguments to TypeVar()
+b = TypeVar('b', *[int]) # E: Unexpected argument to TypeVar()
 c = TypeVar('c', int, 2) # E: Type expected
 [out]
 
diff --git a/mypy/test/testsubtypes.py b/mypy/test/testsubtypes.py
index cffedfb77931..93025d07c0af 100644
--- a/mypy/test/testsubtypes.py
+++ b/mypy/test/testsubtypes.py
@@ -1,27 +1,28 @@
-import typing
-
 from mypy.myunit import Suite, assert_true, run_test
+from mypy.nodes import CONTRAVARIANT, INVARIANT, COVARIANT
 from mypy.subtypes import is_subtype
 from mypy.typefixture import TypeFixture, InterfaceTypeFixture
 
 
 class SubtypingSuite(Suite):
     def set_up(self):
-        self.fx = TypeFixture()
+        self.fx = TypeFixture(INVARIANT)
+        self.fx_contra = TypeFixture(CONTRAVARIANT)
+        self.fx_co = TypeFixture(COVARIANT)
 
     def test_trivial_cases(self):
-        for simple in self.fx.void, self.fx.a, self.fx.o, self.fx.b:
+        for simple in self.fx_co.void, self.fx_co.a, self.fx_co.o, self.fx_co.b:
             self.assert_subtype(simple, simple)
 
     def test_instance_subtyping(self):
-        self.assert_proper_subtype(self.fx.a, self.fx.o)
-        self.assert_proper_subtype(self.fx.b, self.fx.o)
-        self.assert_proper_subtype(self.fx.b, self.fx.a)
+        self.assert_strict_subtype(self.fx.a, self.fx.o)
+        self.assert_strict_subtype(self.fx.b, self.fx.o)
+        self.assert_strict_subtype(self.fx.b, self.fx.a)
 
         self.assert_not_subtype(self.fx.a, self.fx.d)
         self.assert_not_subtype(self.fx.b, self.fx.c)
 
-    def test_simple_generic_instance_subtyping(self):
+    def test_simple_generic_instance_subtyping_invariant(self):
         self.assert_subtype(self.fx.ga, self.fx.ga)
         self.assert_subtype(self.fx.hab, self.fx.hab)
 
@@ -29,9 +30,36 @@ def test_simple_generic_instance_subtyping(self):
         self.assert_not_subtype(self.fx.ga, self.fx.gb)
         self.assert_not_subtype(self.fx.gb, self.fx.ga)
 
-    def test_generic_subtyping_with_inheritance(self):
+    def test_simple_generic_instance_subtyping_covariant(self):
+        self.assert_subtype(self.fx_co.ga, self.fx_co.ga)
+        self.assert_subtype(self.fx_co.hab, self.fx_co.hab)
+
+        self.assert_not_subtype(self.fx_co.ga, self.fx_co.g2a)
+        self.assert_not_subtype(self.fx_co.ga, self.fx_co.gb)
+        self.assert_subtype(self.fx_co.gb, self.fx_co.ga)
+
+    def test_simple_generic_instance_subtyping_contravariant(self):
+        self.assert_subtype(self.fx_contra.ga, self.fx_contra.ga)
+        self.assert_subtype(self.fx_contra.hab, self.fx_contra.hab)
+
+        self.assert_not_subtype(self.fx_contra.ga, self.fx_contra.g2a)
+        self.assert_subtype(self.fx_contra.ga, self.fx_contra.gb)
+        self.assert_not_subtype(self.fx_contra.gb, self.fx_contra.ga)
+
+    def test_generic_subtyping_with_inheritance_invariant(self):
         self.assert_subtype(self.fx.gsab, self.fx.gb)
         self.assert_not_subtype(self.fx.gsab, self.fx.ga)
+        self.assert_not_subtype(self.fx.gsaa, self.fx.gb)
+
+    def test_generic_subtyping_with_inheritance_covariant(self):
+        self.assert_subtype(self.fx_co.gsab, self.fx_co.gb)
+        self.assert_subtype(self.fx_co.gsab, self.fx_co.ga)
+        self.assert_not_subtype(self.fx_co.gsaa, self.fx_co.gb)
+
+    def test_generic_subtyping_with_inheritance_contravariant(self):
+        self.assert_subtype(self.fx_contra.gsab, self.fx_contra.gb)
+        self.assert_not_subtype(self.fx_contra.gsab, self.fx_contra.ga)
+        self.assert_subtype(self.fx_contra.gsaa, self.fx_contra.gb)
 
     def test_interface_subtyping(self):
         self.assert_subtype(self.fx.e, self.fx.f)
@@ -50,9 +78,9 @@ def test_generic_interface_subtyping(self):
         self.assert_equivalent(fx2.gfa, fx2.gfa)
 
     def test_basic_callable_subtyping(self):
-        self.assert_proper_subtype(self.fx.callable(self.fx.o, self.fx.d),
+        self.assert_strict_subtype(self.fx.callable(self.fx.o, self.fx.d),
                                    self.fx.callable(self.fx.a, self.fx.d))
-        self.assert_proper_subtype(self.fx.callable(self.fx.d, self.fx.b),
+        self.assert_strict_subtype(self.fx.callable(self.fx.d, self.fx.b),
                                    self.fx.callable(self.fx.d, self.fx.a))
 
         self.assert_unrelated(self.fx.callable(self.fx.a, self.fx.a),
@@ -63,15 +91,15 @@ def test_basic_callable_subtyping(self):
             self.fx.callable(self.fx.a, self.fx.a))
 
     def test_default_arg_callable_subtyping(self):
-        self.assert_proper_subtype(
+        self.assert_strict_subtype(
             self.fx.callable_default(1, self.fx.a, self.fx.d, self.fx.a),
             self.fx.callable(self.fx.a, self.fx.d, self.fx.a))
 
-        self.assert_proper_subtype(
+        self.assert_strict_subtype(
             self.fx.callable_default(1, self.fx.a, self.fx.d, self.fx.a),
             self.fx.callable(self.fx.a, self.fx.a))
 
-        self.assert_proper_subtype(
+        self.assert_strict_subtype(
             self.fx.callable_default(0, self.fx.a, self.fx.d, self.fx.a),
             self.fx.callable_default(1, self.fx.a, self.fx.d, self.fx.a))
 
@@ -88,32 +116,32 @@ def test_default_arg_callable_subtyping(self):
             self.fx.callable(self.fx.a, self.fx.a, self.fx.a))
 
     def test_var_arg_callable_subtyping_1(self):
-        self.assert_proper_subtype(
+        self.assert_strict_subtype(
             self.fx.callable_var_arg(0, self.fx.a, self.fx.a),
             self.fx.callable_var_arg(0, self.fx.b, self.fx.a))
 
     def test_var_arg_callable_subtyping_2(self):
-        self.assert_proper_subtype(
+        self.assert_strict_subtype(
             self.fx.callable_var_arg(0, self.fx.a, self.fx.a),
             self.fx.callable(self.fx.b, self.fx.a))
 
     def test_var_arg_callable_subtyping_3(self):
-        self.assert_proper_subtype(
+        self.assert_strict_subtype(
             self.fx.callable_var_arg(0, self.fx.a, self.fx.a),
             self.fx.callable(self.fx.a))
 
     def test_var_arg_callable_subtyping_4(self):
-        self.assert_proper_subtype(
+        self.assert_strict_subtype(
             self.fx.callable_var_arg(1, self.fx.a, self.fx.d, self.fx.a),
             self.fx.callable(self.fx.b, self.fx.a))
 
     def test_var_arg_callable_subtyping_5(self):
-        self.assert_proper_subtype(
+        self.assert_strict_subtype(
             self.fx.callable_var_arg(0, self.fx.a, self.fx.d, self.fx.a),
             self.fx.callable(self.fx.b, self.fx.a))
 
     def test_var_arg_callable_subtyping_6(self):
-        self.assert_proper_subtype(
+        self.assert_strict_subtype(
             self.fx.callable_var_arg(0, self.fx.a, self.fx.f, self.fx.d),
             self.fx.callable_var_arg(0, self.fx.b, self.fx.e, self.fx.d))
 
@@ -139,14 +167,14 @@ def test_var_arg_callable_subtyping_9(self):
             self.fx.callable_var_arg(0, self.fx.b, self.fx.d))
 
     def test_type_callable_subtyping(self):
-        self.assert_proper_subtype(
+        self.assert_strict_subtype(
             self.fx.callable_type(self.fx.d, self.fx.a), self.fx.type_type)
 
-        self.assert_proper_subtype(
+        self.assert_strict_subtype(
             self.fx.callable_type(self.fx.d, self.fx.b),
             self.fx.callable(self.fx.d, self.fx.a))
 
-        self.assert_proper_subtype(self.fx.callable_type(self.fx.a, self.fx.b),
+        self.assert_strict_subtype(self.fx.callable_type(self.fx.a, self.fx.b),
                                    self.fx.callable(self.fx.a, self.fx.b))
 
     # IDEA: Maybe add these test cases (they are tested pretty well in type
@@ -166,7 +194,7 @@ def assert_subtype(self, s, t):
     def assert_not_subtype(self, s, t):
         assert_true(not is_subtype(s, t), '{} subtype of {}'.format(s, t))
 
-    def assert_proper_subtype(self, s, t):
+    def assert_strict_subtype(self, s, t):
         self.assert_subtype(s, t)
         self.assert_not_subtype(t, s)
 
diff --git a/mypy/test/testtypes.py b/mypy/test/testtypes.py
index da5ae1428ed4..afda5734fc6f 100644
--- a/mypy/test/testtypes.py
+++ b/mypy/test/testtypes.py
@@ -13,7 +13,7 @@
     UnboundType, AnyType, Void, CallableType, TupleType, TypeVarDef, Type,
     Instance, NoneTyp, ErrorType
 )
-from mypy.nodes import ARG_POS, ARG_OPT, ARG_STAR
+from mypy.nodes import ARG_POS, ARG_OPT, ARG_STAR, CONTRAVARIANT, INVARIANT, COVARIANT
 from mypy.replacetvars import replace_type_vars
 from mypy.subtypes import is_subtype, is_more_precise, is_proper_subtype
 from mypy.typefixture import TypeFixture, InterfaceTypeFixture
@@ -96,7 +96,9 @@ def test_generic_function_type(self):
 
 class TypeOpsSuite(Suite):
     def set_up(self):
-        self.fx = TypeFixture()
+        self.fx = TypeFixture(INVARIANT)
+        self.fx_co = TypeFixture(COVARIANT)
+        self.fx_contra = TypeFixture(CONTRAVARIANT)
 
     # expand_type
 
@@ -213,15 +215,39 @@ def test_is_proper_subtype(self):
 
         assert_true(is_proper_subtype(fx.ga, fx.ga))
         assert_true(is_proper_subtype(fx.gdyn, fx.gdyn))
-        assert_true(is_proper_subtype(fx.gsab, fx.gb))
-        assert_false(is_proper_subtype(fx.gsab, fx.ga))
-        assert_false(is_proper_subtype(fx.gb, fx.ga))
         assert_false(is_proper_subtype(fx.ga, fx.gdyn))
         assert_false(is_proper_subtype(fx.gdyn, fx.ga))
 
         assert_true(is_proper_subtype(fx.t, fx.t))
         assert_false(is_proper_subtype(fx.t, fx.s))
 
+    def test_is_proper_subtype_covariance(self):
+        fx_co = self.fx_co
+
+        assert_true(is_proper_subtype(fx_co.gsab, fx_co.gb))
+        assert_true(is_proper_subtype(fx_co.gsab, fx_co.ga))
+        assert_false(is_proper_subtype(fx_co.gsaa, fx_co.gb))
+        assert_true(is_proper_subtype(fx_co.gb, fx_co.ga))
+        assert_false(is_proper_subtype(fx_co.ga, fx_co.gb))
+
+    def test_is_proper_subtype_contravariance(self):
+        fx_contra = self.fx_contra
+
+        assert_true(is_proper_subtype(fx_contra.gsab, fx_contra.gb))
+        assert_false(is_proper_subtype(fx_contra.gsab, fx_contra.ga))
+        assert_true(is_proper_subtype(fx_contra.gsaa, fx_contra.gb))
+        assert_false(is_proper_subtype(fx_contra.gb, fx_contra.ga))
+        assert_true(is_proper_subtype(fx_contra.ga, fx_contra.gb))
+
+    def test_is_proper_subtype_invariance(self):
+        fx = self.fx
+
+        assert_true(is_proper_subtype(fx.gsab, fx.gb))
+        assert_false(is_proper_subtype(fx.gsab, fx.ga))
+        assert_false(is_proper_subtype(fx.gsaa, fx.gb))
+        assert_false(is_proper_subtype(fx.gb, fx.ga))
+        assert_false(is_proper_subtype(fx.ga, fx.gb))
+
     # Helpers
 
     def tuple(self, *a):
@@ -350,7 +376,8 @@ def test_error_type(self):
 
     def test_simple_generics(self):
         self.assert_join(self.fx.ga, self.fx.ga, self.fx.ga)
-        self.assert_join(self.fx.ga, self.fx.gb, self.fx.o)
+        self.assert_join(self.fx.ga, self.fx.gb, self.fx.ga)
+        self.assert_join(self.fx.ga, self.fx.gd, self.fx.o)
         self.assert_join(self.fx.ga, self.fx.g2a, self.fx.o)
 
         self.assert_join(self.fx.ga, self.fx.nonet, self.fx.ga)
@@ -362,16 +389,18 @@ def test_simple_generics(self):
 
     def test_generics_with_multiple_args(self):
         self.assert_join(self.fx.hab, self.fx.hab, self.fx.hab)
-        self.assert_join(self.fx.hab, self.fx.haa, self.fx.o)
-        self.assert_join(self.fx.hab, self.fx.hbb, self.fx.o)
+        self.assert_join(self.fx.hab, self.fx.hbb, self.fx.hab)
+        self.assert_join(self.fx.had, self.fx.haa, self.fx.o)
 
     def test_generics_with_inheritance(self):
         self.assert_join(self.fx.gsab, self.fx.gb, self.fx.gb)
-        self.assert_join(self.fx.gsba, self.fx.gb, self.fx.o)
+        self.assert_join(self.fx.gsba, self.fx.gb, self.fx.ga)
+        self.assert_join(self.fx.gsab, self.fx.gd, self.fx.o)
 
     def test_generics_with_inheritance_and_shared_supertype(self):
         self.assert_join(self.fx.gsba, self.fx.gs2a, self.fx.ga)
-        self.assert_join(self.fx.gsab, self.fx.gs2a, self.fx.o)
+        self.assert_join(self.fx.gsab, self.fx.gs2a, self.fx.ga)
+        self.assert_join(self.fx.gsab, self.fx.gs2d, self.fx.o)
 
     def test_generic_types_and_any(self):
         self.assert_join(self.fx.gdyn, self.fx.ga, self.fx.gdyn)
@@ -581,7 +610,8 @@ def test_error_type(self):
     def test_simple_generics(self):
         self.assert_meet(self.fx.ga, self.fx.ga, self.fx.ga)
         self.assert_meet(self.fx.ga, self.fx.o, self.fx.ga)
-        self.assert_meet(self.fx.ga, self.fx.gb, self.fx.nonet)
+        self.assert_meet(self.fx.ga, self.fx.gb, self.fx.gb)
+        self.assert_meet(self.fx.ga, self.fx.gd, self.fx.nonet)
         self.assert_meet(self.fx.ga, self.fx.g2a, self.fx.nonet)
 
         self.assert_meet(self.fx.ga, self.fx.nonet, self.fx.nonet)
@@ -593,8 +623,9 @@ def test_simple_generics(self):
 
     def test_generics_with_multiple_args(self):
         self.assert_meet(self.fx.hab, self.fx.hab, self.fx.hab)
-        self.assert_meet(self.fx.hab, self.fx.haa, self.fx.nonet)
-        self.assert_meet(self.fx.hab, self.fx.hbb, self.fx.nonet)
+        self.assert_meet(self.fx.hab, self.fx.haa, self.fx.hab)
+        self.assert_meet(self.fx.hab, self.fx.had, self.fx.nonet)
+        self.assert_meet(self.fx.hab, self.fx.hbb, self.fx.hbb)
 
     def test_generics_with_inheritance(self):
         self.assert_meet(self.fx.gsab, self.fx.gb, self.fx.gsab)
diff --git a/mypy/typeanal.py b/mypy/typeanal.py
index 032f49e4f960..8c17a742605c 100644
--- a/mypy/typeanal.py
+++ b/mypy/typeanal.py
@@ -222,6 +222,7 @@ def anal_var_defs(self, var_defs: List[TypeVarDef]) -> List[TypeVarDef]:
         for vd in var_defs:
             a.append(TypeVarDef(vd.name, vd.id, self.anal_array(vd.values),
                                 vd.upper_bound.accept(self),
+                                vd.variance,
                                 vd.line))
         return a
 
diff --git a/mypy/typefixture.py b/mypy/typefixture.py
index 174ae40413b0..9fd2a370f8b4 100644
--- a/mypy/typefixture.py
+++ b/mypy/typefixture.py
@@ -9,8 +9,8 @@
     TypeVarType, AnyType, Void, ErrorType, NoneTyp, Instance, CallableType, TypeVarDef
 )
 from mypy.nodes import (
-    TypeInfo, ClassDef, Block, ARG_POS, ARG_OPT, ARG_STAR, SymbolTable
-)
+    TypeInfo, ClassDef, Block, ARG_POS, ARG_OPT, ARG_STAR, SymbolTable,
+    COVARIANT)
 
 
 class TypeFixture:
@@ -19,19 +19,19 @@ class TypeFixture:
     The members are initialized to contain various type-related values.
     """
 
-    def __init__(self):
+    def __init__(self, variance: int=COVARIANT) -> None:
         # The 'object' class
         self.oi = self.make_type_info('builtins.object')               # class object
         self.o = Instance(self.oi, [])                        # object
 
         # Type variables
-        self.t = TypeVarType('T', 1, [], self.o)     # T`1 (type variable)
-        self.tf = TypeVarType('T', -1, [], self.o)   # T`-1 (type variable)
-        self.tf2 = TypeVarType('T', -2, [], self.o)  # T`-2 (type variable)
-        self.s = TypeVarType('S', 2, [], self.o)     # S`2 (type variable)
-        self.s1 = TypeVarType('S', 1, [], self.o)    # S`1 (type variable)
-        self.sf = TypeVarType('S', -2, [], self.o)   # S`-2 (type variable)
-        self.sf1 = TypeVarType('S', -1, [], self.o)  # S`-1 (type variable)
+        self.t = TypeVarType('T', 1, [], self.o, variance)     # T`1 (type variable)
+        self.tf = TypeVarType('T', -1, [], self.o, variance)   # T`-1 (type variable)
+        self.tf2 = TypeVarType('T', -2, [], self.o, variance)  # T`-2 (type variable)
+        self.s = TypeVarType('S', 2, [], self.o, variance)     # S`2 (type variable)
+        self.s1 = TypeVarType('S', 1, [], self.o, variance)    # S`1 (type variable)
+        self.sf = TypeVarType('S', -2, [], self.o, variance)   # S`-2 (type variable)
+        self.sf1 = TypeVarType('S', -1, [], self.o, variance)  # S`-1 (type variable)
 
         # Simple types
         self.anyt = AnyType()
@@ -67,22 +67,31 @@ def __init__(self):
 
         # Generic class TypeInfos
         # G[T]
-        self.gi = self.make_type_info('G', mro=[self.oi], typevars=['T'])
+        self.gi = self.make_type_info('G', mro=[self.oi],
+                                      typevars=['T'],
+                                      variances=[variance])
         # G2[T]
-        self.g2i = self.make_type_info('G2', mro=[self.oi], typevars=['T'])
+        self.g2i = self.make_type_info('G2', mro=[self.oi],
+                                       typevars=['T'],
+                                       variances=[variance])
         # H[S, T]
-        self.hi = self.make_type_info('H', mro=[self.oi], typevars=['S', 'T'])
+        self.hi = self.make_type_info('H', mro=[self.oi],
+                                      typevars=['S', 'T'],
+                                      variances=[variance, variance])
         # GS[T, S] <: G[S]
         self.gsi = self.make_type_info('GS', mro=[self.gi, self.oi],
                                        typevars=['T', 'S'],
+                                       variances=[variance, variance],
                                        bases=[Instance(self.gi, [self.s])])
         # GS2[S] <: G[S]
         self.gs2i = self.make_type_info('GS2', mro=[self.gi, self.oi],
                                         typevars=['S'],
+                                        variances=[variance],
                                         bases=[Instance(self.gi, [self.s1])])
         # list[T]
         self.std_listi = self.make_type_info('builtins.list', mro=[self.oi],
-                                             typevars=['T'])
+                                             typevars=['T'],
+                                             variances=[variance])
 
         # Instance types
         self.std_tuple = Instance(self.std_tuplei, [])        # tuple
@@ -104,6 +113,7 @@ def __init__(self):
         # Generic instance types
         self.ga = Instance(self.gi, [self.a])        # G[A]
         self.gb = Instance(self.gi, [self.b])        # G[B]
+        self.gd = Instance(self.gi, [self.d])        # G[D]
         self.go = Instance(self.gi, [self.o])        # G[object]
         self.gt = Instance(self.gi, [self.t])        # G[T`1]
         self.gtf = Instance(self.gi, [self.tf])      # G[T`-1]
@@ -113,15 +123,19 @@ def __init__(self):
 
         self.g2a = Instance(self.g2i, [self.a])      # G2[A]
 
+        self.gsaa = Instance(self.gsi, [self.a, self.a])  # GS[A, A]
         self.gsab = Instance(self.gsi, [self.a, self.b])  # GS[A, B]
         self.gsba = Instance(self.gsi, [self.b, self.a])  # GS[B, A]
 
         self.gs2a = Instance(self.gs2i, [self.a])    # GS2[A]
+        self.gs2b = Instance(self.gs2i, [self.b])    # GS2[B]
+        self.gs2d = Instance(self.gs2i, [self.d])    # GS2[D]
 
         self.hab = Instance(self.hi, [self.a, self.b])    # H[A, B]
         self.haa = Instance(self.hi, [self.a, self.a])    # H[A, A]
         self.hbb = Instance(self.hi, [self.b, self.b])    # H[B, B]
         self.hts = Instance(self.hi, [self.t, self.s])    # H[T, S]
+        self.had = Instance(self.hi, [self.a, self.d])    # H[A, D]
 
         self.lsta = Instance(self.std_listi, [self.a])  # List[A]
         self.lstb = Instance(self.std_listi, [self.b])  # List[B]
@@ -169,7 +183,8 @@ def make_type_info(self, name: str,
                        is_abstract: bool = False,
                        mro: List[TypeInfo] = None,
                        bases: List[Instance] = None,
-                       typevars: List[str] = None) -> TypeInfo:
+                       typevars: List[str] = None,
+                       variances: List[int] = None) -> TypeInfo:
         """Make a TypeInfo suitable for use in unit tests."""
 
         class_def = ClassDef(name, Block([]), None, [])
@@ -177,10 +192,12 @@ def make_type_info(self, name: str,
 
         if typevars:
             v = []  # type: List[TypeVarDef]
-            id = 1
-            for n in typevars:
-                v.append(TypeVarDef(n, id, None, self.oi))
-                id += 1
+            for id, n in enumerate(typevars, 1):
+                if variances:
+                    variance = variances[id-1]
+                else:
+                    variance = COVARIANT
+                v.append(TypeVarDef(n, id, None, self.o, variance=variance))
             class_def.type_vars = v
 
         info = TypeInfo(SymbolTable(), class_def)
diff --git a/mypy/types.py b/mypy/types.py
index 0ea70407481b..4e971acac5fa 100644
--- a/mypy/types.py
+++ b/mypy/types.py
@@ -4,6 +4,7 @@
 from typing import Any, TypeVar, List, Tuple, cast, Generic, Set
 
 import mypy.nodes
+from mypy.nodes import INVARIANT
 
 
 T = TypeVar('T')
@@ -34,14 +35,16 @@ class TypeVarDef(mypy.nodes.Context):
     id = 0
     values = None  # type: List[Type]
     upper_bound = None  # type: Type
+    variance = INVARIANT  # type: int
     line = 0
 
-    def __init__(self, name: str, id: int, values: List[Type], upper_bound: Type,
-                 line: int = -1) -> None:
+    def __init__(self, name: str, id: int, values: List[Type],
+                 upper_bound: Type, variance: int=INVARIANT, line: int=-1) -> None:
         self.name = name
         self.id = id
         self.values = values
         self.upper_bound = upper_bound
+        self.variance = variance
         self.line = line
 
     def get_line(self) -> int:
@@ -186,13 +189,15 @@ class TypeVarType(Type):
     id = 0     # 1, 2, ... for type-related, -1, ... for function-related
     values = None  # type: List[Type]  # Value restriction, empty list if no restriction
     upper_bound = None  # type: Type   # Upper bound for values (currently always 'object')
+    variance = INVARIANT  # type: int
 
     def __init__(self, name: str, id: int, values: List[Type], upper_bound: Type,
-                 line: int = -1) -> None:
+                 variance: int=INVARIANT, line: int=-1) -> None:
         self.name = name
         self.id = id
         self.values = values
         self.upper_bound = upper_bound
+        self.variance = variance
         super().__init__(line)
 
     def accept(self, visitor: 'TypeVisitor[T]') -> T:
diff --git a/stubs/2.7/typing.pyi b/stubs/2.7/typing.pyi
index ddc064c65d2a..d28b5133874d 100644
--- a/stubs/2.7/typing.pyi
+++ b/stubs/2.7/typing.pyi
@@ -34,9 +34,14 @@ AnyStr = TypeVar('AnyStr', str, unicode)
 
 # Abstract base classes.
 
-_T = TypeVar('_T')
-_KT = TypeVar('_KT')
-_VT = TypeVar('_VT')
+# Some unconstrained type variables.  These are used by the container types.
+_T = TypeVar('_T')  # Any type.
+_KT = TypeVar('_KT')  # Key type.
+_VT = TypeVar('_VT')  # Value type.
+_T_co = TypeVar('_T_co', covariant=True)  # Any type covariant containers.
+_V_co = TypeVar('_V_co', covariant=True)  # Any type covariant containers.
+_VT_co = TypeVar('_VT_co', covariant=True)  # Value type covariant containers.
+_T_contra = TypeVar('_T_contra', contravariant=True)  # Ditto contravariant.
 
 # TODO Container etc.
 
@@ -64,49 +69,49 @@ class Sized(metaclass=ABCMeta):
     @abstractmethod
     def __len__(self) -> int: pass
 
-class Iterable(Generic[_T]):
+class Iterable(Generic[_T_co]):
     @abstractmethod
-    def __iter__(self) -> Iterator[_T]: pass
+    def __iter__(self) -> Iterator[_T_co]: pass
 
-class Iterator(Iterable[_T], Generic[_T]):
+class Iterator(Iterable[_T_co], Generic[_T_co]):
     @abstractmethod
-    def next(self) -> _T: pass
+    def next(self) -> _T_co: pass
 
-class Sequence(Sized, Iterable[_T], Generic[_T]):
+class Sequence(Sized, Iterable[_T_co], Generic[_T_co]):
     @abstractmethod
     def __contains__(self, x: object) -> bool: pass
     @overload
     @abstractmethod
-    def __getitem__(self, i: int) -> _T: pass
+    def __getitem__(self, i: int) -> _T_co: pass
     @overload
     @abstractmethod
-    def __getitem__(self, s: slice) -> Sequence[_T]: pass
+    def __getitem__(self, s: slice) -> Sequence[_T_co]: pass
     @abstractmethod
     def index(self, x: Any) -> int: pass
     @abstractmethod
     def count(self, x: Any) -> int: pass
 
-class AbstractSet(Sized, Iterable[_T], Generic[_T]):
+class AbstractSet(Sized, Iterable[_T_co], Generic[_T_co]):
     @abstractmethod
     def __contains__(self, x: object) -> bool: pass
     # TODO __le__, __lt__, __gt__, __ge__
     @abstractmethod
-    def __and__(self, s: AbstractSet[_T]) -> AbstractSet[_T]: pass
+    def __and__(self, s: AbstractSet[_T_co]) -> AbstractSet[_T_co]: pass
     @abstractmethod
-    def __or__(self, s: AbstractSet[_T]) -> AbstractSet[_T]: pass
+    def __or__(self, s: AbstractSet[_T_co]) -> AbstractSet[_T_co]: pass
     @abstractmethod
-    def __sub__(self, s: AbstractSet[_T]) -> AbstractSet[_T]: pass
+    def __sub__(self, s: AbstractSet[_T_co]) -> AbstractSet[_T_co]: pass
     @abstractmethod
-    def __xor__(self, s: AbstractSet[_T]) -> AbstractSet[_T]: pass
+    def __xor__(self, s: AbstractSet[_T_co]) -> AbstractSet[_T_co]: pass
     # TODO argument can be any container?
     @abstractmethod
-    def isdisjoint(self, s: AbstractSet[_T]) -> bool: pass
+    def isdisjoint(self, s: AbstractSet[_T_co]) -> bool: pass
 
-class Mapping(Sized, Iterable[_KT], Generic[_KT, _VT]):
+class Mapping(Sized, Iterable[_KT], Generic[_KT, _VT_co]):
     @abstractmethod
-    def __getitem__(self, k: _KT) -> _VT: pass
+    def __getitem__(self, k: _KT) -> _VT_co: pass
     @abstractmethod
-    def __setitem__(self, k: _KT, v: _VT) -> None: pass
+    def __setitem__(self, k: _KT, v: _VT_co) -> None: pass
     @abstractmethod
     def __delitem__(self, v: _KT) -> None: pass
     @abstractmethod
@@ -115,48 +120,48 @@ class Mapping(Sized, Iterable[_KT], Generic[_KT, _VT]):
     @abstractmethod
     def clear(self) -> None: pass
     @abstractmethod
-    def copy(self) -> Mapping[_KT, _VT]: pass
+    def copy(self) -> Mapping[_KT, _VT_co]: pass
     @overload
     @abstractmethod
-    def get(self, k: _KT) -> _VT: pass
+    def get(self, k: _KT) -> _VT_co: pass
     @overload
     @abstractmethod
-    def get(self, k: _KT, default: _VT) -> _VT: pass
+    def get(self, k: _KT, default: _VT_co) -> _VT_co: pass
     @overload
     @abstractmethod
-    def pop(self, k: _KT) -> _VT: pass
+    def pop(self, k: _KT) -> _VT_co: pass
     @overload
     @abstractmethod
-    def pop(self, k: _KT, default: _VT) -> _VT: pass
+    def pop(self, k: _KT, default: _VT_co) -> _VT_co: pass
     @abstractmethod
-    def popitem(self) -> Tuple[_KT, _VT]: pass
+    def popitem(self) -> Tuple[_KT, _VT_co]: pass
     @overload
     @abstractmethod
-    def setdefault(self, k: _KT) -> _VT: pass
+    def setdefault(self, k: _KT) -> _VT_co: pass
     @overload
     @abstractmethod
-    def setdefault(self, k: _KT, default: _VT) -> _VT: pass
+    def setdefault(self, k: _KT, default: _VT_co) -> _VT_co: pass
 
     # TODO keyword arguments
     @overload
     @abstractmethod
-    def update(self, m: Mapping[_KT, _VT]) -> None: pass
+    def update(self, m: Mapping[_KT, _VT_co]) -> None: pass
     @overload
     @abstractmethod
-    def update(self, m: Iterable[Tuple[_KT, _VT]]) -> None: pass
+    def update(self, m: Iterable[Tuple[_KT, _VT_co]]) -> None: pass
 
     @abstractmethod
     def keys(self) -> list[_KT]: pass
     @abstractmethod
-    def values(self) -> list[_VT]: pass
+    def values(self) -> list[_VT_co]: pass
     @abstractmethod
-    def items(self) -> list[Tuple[_KT, _VT]]: pass
+    def items(self) -> list[Tuple[_KT, _VT_co]]: pass
     @abstractmethod
     def iterkeys(self) -> Iterator[_KT]: pass
     @abstractmethod
-    def itervalues(self) -> Iterator[_VT]: pass
+    def itervalues(self) -> Iterator[_VT_co]: pass
     @abstractmethod
-    def iteritems(self) -> Iterator[Tuple[_KT, _VT]]: pass
+    def iteritems(self) -> Iterator[Tuple[_KT, _VT_co]]: pass
 
 class IO(Iterable[AnyStr], Generic[AnyStr]):
     # TODO detach
diff --git a/stubs/3.2/typing.pyi b/stubs/3.2/typing.pyi
index e9356182e25d..1e6e71679be2 100644
--- a/stubs/3.2/typing.pyi
+++ b/stubs/3.2/typing.pyi
@@ -35,9 +35,15 @@ AnyStr = TypeVar('AnyStr', str, bytes)
 
 # Abstract base classes.
 
-_T = TypeVar('_T')
-_KT = TypeVar('_KT')
-_VT = TypeVar('_VT')
+# Some unconstrained type variables.  These are used by the container types.
+_T = TypeVar('_T')  # Any type.
+_KT = TypeVar('_KT')  # Key type.
+_VT = TypeVar('_VT')  # Value type.
+_T_co = TypeVar('_T_co', covariant=True)  # Any type covariant containers.
+_V_co = TypeVar('_V_co', covariant=True)  # Any type covariant containers.
+_KT_co = TypeVar('_KT_co', covariant=True)  # Key type covariant containers.
+_VT_co = TypeVar('_VT_co', covariant=True)  # Value type covariant containers.
+_T_contra = TypeVar('_T_contra', contravariant=True)  # Ditto contravariant.
 
 # TODO Container etc.
 
@@ -72,32 +78,32 @@ class Hashable(metaclass=ABCMeta):
     @abstractmethod
     def __hash__(self) -> int: pass
 
-class Iterable(Generic[_T]):
+class Iterable(Generic[_T_co]):
     @abstractmethod
-    def __iter__(self) -> Iterator[_T]: pass
+    def __iter__(self) -> Iterator[_T_co]: pass
 
-class Iterator(Iterable[_T], Generic[_T]):
+class Iterator(Iterable[_T_co], Generic[_T_co]):
     @abstractmethod
-    def __next__(self) -> _T: pass
-    def __iter__(self) -> Iterator[_T]: pass
+    def __next__(self) -> _T_co: pass
+    def __iter__(self) -> Iterator[_T_co]: pass
 
-class Container(Generic[_T]):
+class Container(Generic[_T_co]):
     @abstractmethod
     def __contains__(self, x: object) -> bool: pass
 
-class Sequence(Iterable[_T], Container[_T], Sized, Reversible[_T], Generic[_T]):
+class Sequence(Iterable[_T_co], Container[_T_co], Sized, Reversible[_T_co], Generic[_T_co]):
     @overload
     @abstractmethod
-    def __getitem__(self, i: int) -> _T: pass
+    def __getitem__(self, i: int) -> _T_co: pass
     @overload
     @abstractmethod
-    def __getitem__(self, s: slice) -> Sequence[_T]: pass
+    def __getitem__(self, s: slice) -> Sequence[_T_co]: pass
     # Mixin methods
     def index(self, x: Any) -> int: pass
     def count(self, x: Any) -> int: pass
     def __contains__(self, x: object) -> bool: pass
-    def __iter__(self) -> Iterator[_T]: pass
-    def __reversed__(self) -> Iterator[_T]: pass
+    def __iter__(self) -> Iterator[_T_co]: pass
+    def __reversed__(self) -> Iterator[_T_co]: pass
 
 class MutableSequence(Sequence[_T], Generic[_T]):
     @abstractmethod
@@ -118,7 +124,7 @@ class MutableSequence(Sequence[_T], Generic[_T]):
     def remove(self, object: _T) -> None: pass
     def __iadd__(self, x: Iterable[_T]) -> MutableSequence[_T]: pass
 
-class AbstractSet(Iterable[_T], Container[_T], Sized, Generic[_T]):
+class AbstractSet(Iterable[_KT_co], Container[_KT_co], Sized, Generic[_KT_co]):
     @abstractmethod
     def __contains__(self, x: object) -> bool: pass
     # Mixin methods
@@ -126,12 +132,12 @@ class AbstractSet(Iterable[_T], Container[_T], Sized, Generic[_T]):
     def __lt__(self, s: AbstractSet[Any]) -> bool: pass
     def __gt__(self, s: AbstractSet[Any]) -> bool: pass
     def __ge__(self, s: AbstractSet[Any]) -> bool: pass
-    def __and__(self, s: AbstractSet[Any]) -> AbstractSet[_T]: pass
+    def __and__(self, s: AbstractSet[Any]) -> AbstractSet[_KT_co]: pass
     # In order to support covariance, _T should not be used within an argument
     # type. We need union types to properly model this.
-    def __or__(self, s: AbstractSet[_T]) -> AbstractSet[_T]: pass
-    def __sub__(self, s: AbstractSet[Any]) -> AbstractSet[_T]: pass
-    def __xor__(self, s: AbstractSet[_T]) -> AbstractSet[_T]: pass
+    def __or__(self, s: AbstractSet[_KT_co]) -> AbstractSet[_KT_co]: pass
+    def __sub__(self, s: AbstractSet[Any]) -> AbstractSet[_KT_co]: pass
+    def __xor__(self, s: AbstractSet[_KT_co]) -> AbstractSet[_KT_co]: pass
     # TODO: Argument can be a more general ABC?
     def isdisjoint(self, s: AbstractSet[Any]) -> bool: pass
 
@@ -152,26 +158,26 @@ class MutableSet(AbstractSet[_T], Generic[_T]):
 class MappingView(Sized):
     def __len__(self) -> int: pass
 
-class ItemsView(AbstractSet[Tuple[_KT, _VT]], MappingView, Generic[_KT, _VT]):
+class ItemsView(AbstractSet[Tuple[_KT_co, _VT_co]], MappingView, Generic[_KT_co, _VT_co]):
     def __contains__(self, o: object) -> bool: pass
-    def __iter__(self) -> Iterator[Tuple[_KT, _VT]]: pass
+    def __iter__(self) -> Iterator[Tuple[_KT_co, _VT_co]]: pass
 
-class KeysView(AbstractSet[_T], MappingView, Generic[_T]):
+class KeysView(AbstractSet[_KT_co], MappingView, Generic[_KT_co]):
     def __contains__(self, o: object) -> bool: pass
-    def __iter__(self) -> Iterator[_T]: pass
+    def __iter__(self) -> Iterator[_KT_co]: pass
 
-class ValuesView(MappingView, Iterable[_T], Generic[_T]):
+class ValuesView(MappingView, Iterable[_VT_co], Generic[_VT_co]):
     def __contains__(self, o: object) -> bool: pass
-    def __iter__(self) -> Iterator[_T]: pass
+    def __iter__(self) -> Iterator[_VT_co]: pass
 
-class Mapping(Iterable[_KT], Container[_KT], Sized, Generic[_KT, _VT]):
+class Mapping(Iterable[_KT], Container[_KT], Sized, Generic[_KT, _VT_co]):
     @abstractmethod
-    def __getitem__(self, k: _KT) -> _VT: pass
+    def __getitem__(self, k: _KT) -> _VT_co: pass
     # Mixin methods
-    def get(self, k: _KT, default: _VT = ...) -> _VT: pass
-    def items(self) -> AbstractSet[Tuple[_KT, _VT]]: pass
+    def get(self, k: _KT, default: _VT = ...) -> _VT_co: pass
+    def items(self) -> AbstractSet[Tuple[_KT, _VT_co]]: pass
     def keys(self) -> AbstractSet[_KT]: pass
-    def values(self) -> ValuesView[_VT]: pass
+    def values(self) -> ValuesView[_VT_co]: pass
     def __contains__(self, o: object) -> bool: pass
 
 class MutableMapping(Mapping[_KT, _VT], Generic[_KT, _VT]):