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

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.

Start by running the minimal parser-combinator example with mypy and compare ws_then1 with the inline re call in ws_then2. Trace how type variables flow through re, ws, and then, focusing on why is fixed instead of remaining compatible with S. Done means ws_then1 typechecks with the same generic behavior as ws_then2.