Behavior of mypy not matching example in PEP 483

[mbenbernard]

It appears that there's a discrepancy between one of the examples given in PEP 483 and the actual behavior of mypy (0.750).

So I ran mypy on the following code snippet:

class Employee: ...
class Manager(Employee): ..


T_co = TypeVar('T_co', Employee, Manager, covariant=True)
T_contra = TypeVar('T_contra', Employee, Manager, contravariant=True)


class Base(Generic[T_contra]):
    ...


class Derived(Base[T_co]):
    ...

def func1(a: Base[Employee]): ...

func1(Derived[Manager]())      # error: Argument 1 to "func1" has incompatible type "Derived[Manager]"; expected "Base[Employee]"

def func2(a: Base[Manager]): ...

func2(Derived[Employee]())     # OK; Derived[Employee] < Base[Manager]

As you can see, mypy complains about the call to func1(), but not for the one to func2().

These results seem to contradict what is stated in PEP 483: "[...] a type checker will also find that, e.g., Derived[Manager] is a subtype of Base[Employee]." But mypy seems to tell us instead that Derived[Employee] < Base[Manager].

Am I understanding things correctly? Is this a bug in mypy, or maybe an error/typo in PEP 483?

[msullivan]

Derived[Employee] < Base[Manager] is correct, per the PEP.

This does seem to be a bug in mypy, which does seem to understand all of the steps in the relationship Derived[Manager] < Derived[Employee] < Base[Employee] but fails to properly connect them together transitively.

The following passes:

x: Derived[Manager]
y: Derived[Employee] = x
z: Base[Employee] = y

but this fails
z2: Base[Employee] = x.

So this does seem like a bug. I will also say that it feels pretty low-priority. Mixing co and contra type variables in this way seems like a bad practice!

[mbenbernard]

I'm not super well-versed in type theory and I don't know the internals of mypy that much, so please bear with me.

My understanding is that for an assignment, the variance of the target is the one that applies during type checking:

x: Iterable[int]    # Covariant
y: List[bool]       # Invariant

x = y               # OK, because Iterable is covariant, List is a structural subtype of Iterable and bool is a subtype of int

Is this observation correct?

Assuming that it is correct, then what happens - from a type theory perspective - in the context of the Employee/Manager example?

x: Derived[Manager]
y: Derived[Employee] = x    # OK, because Derived is covariant, and Manager is a subtype of Employee
z: Base[Employee] = y       # OK, but why???
z2: Base[Employee] = x      # Should be OK, but causes an error, why???

I would assume that mypy behaves as it does because:

1. The variance of the target type is the one that's considered.
2. Base is contravariant, so it only allows assignments from a less specific type to a more specific one (e.g. Employee -> Employee or Employee -> Manager).
3. Derived is a subtype of Base.

What do you think?

[ilevkivskyi]

Actually this example in the PEP is kind of "pathological" (btw I wrote it long time ago), because in real life it is hard (if possible at all) to write a non-empty covariant generic subclass of a contravariant base (just because you can only add members). So I would not be worried too much about mypy behavior here.

There is actually an old issue to amend example in the PEP to be more realistic (e.g. have an invariant subclass of co- or contravariant base), and make mypy actually prohibit the original example, see #736