Honestly I wish mypy was smart enough to figure out that the empty list in this case has the same type as the non-default list return value...

Not much related, shouldn't it be infered as a List[Any] instead?

It inferred the type Union[List[Constraint], List[None]] for a, then it tried to check a.append(con) with a having each type from the union.

Honestly I wish mypy was smart enough to figure out that the empty list in this case has the same type as the non-default list return value...

This reminds me of the situation with x if b else y where you implemented some special logic to type check y with the inferred type of x, IIRC. Seems sensible to do something similar here but I don't know how we'd tell mypy to do that.

In principle mypy could determine that the [] must have type List[Constraint] from the usage on the next line, but that is pretty far outside its capabilities at the moment.

What I did for [...] if ... else [] was different -- there I play games with using either side as context for the other. That doesn't seem applicable here, at least it seems harder since the general case may be arbitrarily complex. I think it would be possible if [] came out with some type other than List[None] so that the unification code (I think in join.py) could special-case it safely (it currently can't know whether the List[None] came from [] or from actually writing e.g. [None, None]).

Not much related, shouldn't it be infered as a List[Any] instead?

It inferred the type Union[List[Constraint], List[None]] for a, then it tried to check a.append(con) with a having each type from the union.

I meant for [], that it should get infered a List[Any]. Or eventually a special case for an empty list agreeing to join with any other type of list.