Type variables set to <nothing> do not unify with more specific variables when used in a more specific context

[bwo]

possibly related to #6613?

Here is some simplified code for an imaginary typed parser combinator library.

from typing import Callable, Optional, Tuple, Pattern, Union, TypeVar, Generic, Text

S = TypeVar('S')
T = TypeVar('T')
A = TypeVar('A')
B = TypeVar('B')


class ParserState(Generic[S, T]):
    pass


ParseResult = Optional[Tuple[A, ParserState[S, T]]]
Parser = Callable[[ParserState[S, T]], ParseResult[A, S, T]]


# the idea here is that `re` gives a parser that works with `Text` input and produces a bit of `Text` as output, with a bit of parser state `S` regarding which this parser is agnostic.
def re(pat):
    # type: (Union[Text, Pattern]) -> Parser[S, Text, Text]
    raise NotImplementedError


def then(p1, p2):
    # type: (Parser[S, T, A], Parser[S, T, B]) -> Parser[S, T, B]
    raise NotImplementedError


ws = re(u'\\s*')


# this fails to typecheck
def ws_then1(p):
    # type: (Parser[S, Text, A]) -> Parser[S, Text, A]
    return then(ws, p)


# this typechecks
def ws_then2(p):
    # type: (Parser[S, Text, A]) -> Parser[S, Text, A]
    return then(re(u'\\s*'), p)

The inferred type of ws is def (simpleparser.ParserState[<nothing>, builtins.str]) -> Union[Tuple[builtins.str, simpleparser.ParserState[<nothing>, builtins.str]], None], which I take to mean that all the type variables have been fully instantiated, with the unsupplied S being instantiated as <nothing>, which seems to be a kind of placeholder that unifies with nothing else. As a result, ws can't be used as-is in ws_then1:

simpleparser.py:33: error: Argument 1 to "then" has incompatible type "Callable[[ParserState[<nothing>, str]], Optional[Tuple[str, ParserState[<nothing>, str]]]]"; expected "Callable[[ParserState[S, str]], Optional[Tuple[str, ParserState[S, str]]]]"

But when its definition is inlined into ws_then2, it typechecks.

What I expected was that ws would have a revealed type like def [S] (simpleparser.ParserState[S`-1, builtins.str]) -> Union[Tuple[builtins.str, simpleparser.ParserState[S`-1, builtins.str]], None], i.e., that the variables in fact assigned <nothing> would remain general, or that <nothing> would unify with other type variables, or … something like that.

[bwo]

On doing some searching, judging from the still-open #3032. my expected behavior is the intended behavior? Specifically with reference to this comment:

3. If a concrete type found for a type variable is <uninhabited>, but the constraint is not equality, leave the type variable unsubstituted, so it becomes a type parameter in the final result

[ilevkivskyi]

This is how type variables work in mypy. A variable type can't bind type variables, i.e. type of ws can't be Parser[S, Text, Text]. Type inference for ws is clearly underspecified so S gets inferred as bottom type (this is what <nothing> is, a type with no values).

One problem I see here is that normally we should give an error in such cases asking for type annotation. The problem is that is_valid_inferred_type() is a bunch of ad-hoc isinstances() instead of a proper visitor. @JukkaL is this intentional?

Also in principle we can allow "standalone" types with free type variables for callable types, like in your case, but there is a separate place for this discussion, see #5738.