Mutually recursive type variables

[sk-]

When answering a question on StackOverflow, I found a weird issue with pyre.

The following code checks:

from typing import Iterable, TypeVar, Callable

T1 = TypeVar('T1')
T2 = TypeVar('T2')


def chain(
        functions: Iterable[Callable[[T1], T1]]
    ) -> Callable[[T1], T1]:

    def compose(
            f: Callable[[T1], T1],
            g: Callable[[T1], T1]
        ) -> Callable[[T1], T1]:
        def h(x: T1) -> T1:
            return g(f(x))
        return h

    def identity(x: T1, /) -> T1:
        return x
    return reduce(functions, compose, identity)

def reduce(
        items: Iterable[T1], 
        op:    Callable[[T2, T1], T2],
        init:  T2
    ) -> T2:
    for item in items:
        init = op(init, item)
    return init

def add_one(x):
    return x + 1

def mul_two(x):
    return x * 2

assert chain([add_one, mul_two, mul_two, add_one])(7) == 33

But if we move the identity function outside compose, then the code fails with

Mutually recursive type variables [36]: Solving type variables for call `reduce` led to infinite recursion.

But then If I replaced the custom reduce with functools.reduce, the code checks again:

import functools
from typing import Iterable, TypeVar, Callable

T1 = TypeVar('T1')
T2 = TypeVar('T2')

def identity(x: T1, /) -> T1:
    return x

def chain(
        functions: Iterable[Callable[[T1], T1]]
    ) -> Callable[[T1], T1]:

    def compose(
            f: Callable[[T1], T1],
            g: Callable[[T1], T1]
        ) -> Callable[[T1], T1]:
        def h(x: T1) -> T1:
            return g(f(x))
        return h

    return functools.reduce(compose, functions, identity)

def add_one(x):
    return x + 1

def mul_two(x):
    return x * 2

assert chain([add_one, mul_two, mul_two, add_one])(7) == 33

[pradeep90]

@sk- Thanks for the thoughtful question. Overall, Pyre doesn't yet have great support for higher-order generic functions called with other generic functions. We plan to substantially improve Pyre's type inference over the next year.

There are two subtle bugs here:

1. Essentially, when checking compatibility for reduce(...), in one of the steps, Pyre confuses identity.T1 with reduce.T1. This was triggered by moving identity out of chain, which made identity.T1 a free variable. This eventually leads to the nonsensical "mutually recursive type variables" error, which is a catch-all and pretty mystifying error when we are unable to find a satisfying assignment to the type variables.

   Using functools.reduce removes that problem. As does using unique type variables for each function. (Note that you shouldn't need to create unique type variables in general; this example happened to trigger the bug.)

2. That uncovers the second bug. In the repro below, calling foo with identity (where T1 is free) and bar (where T3 is bound by some_generic_function) makes Pyre fail to see the solution T2 = T1 = T3.

   Repro:

      from typing import *
   
      T1 = TypeVar('T1')
      T2 = TypeVar('T2')
      T3 = TypeVar('T3')
   
      def identity(x: T1) -> T1: ...
   
      def foo(x: T2, y: Callable[[T2], None]) -> None: ...
   
      def some_generic_function(x: T3) -> None:
          # Moving this out of this function eliminates the error since `T3` becomes a free variable.
          def bar(x: T3) -> None: ...
   
          # Error: Incompatible parameter type 
          foo(identity, bar)
   

Thanks again for the bug report.