<nothing> is inferred when mimicking GADT

[msakai]

As mypy understands isinstance checks, I wondered if I can use this to mimic GADT (Generalized algebraic data type) in functional languages such as Haskell and OCaml.

I tried to mimic following Haskell code

data Expr a where
    Const :: a  -> Expr a
    Add :: Expr Int -> Expr Int -> Expr Int

eval :: Expr a -> a
eval (Const x) = x
eval (Add a b) = eval a + eval b

with the following Python code:

import abc
from typing import Generic, TypeVar


A = TypeVar('A')


class Expr(Generic[A], metaclass=abc.ABCMeta):
    pass


class Const(Expr[A]):
    value: A
    
    def __init__(self, value: A):
        self.value = value


class Add(Expr[int]):
    left: Expr[int]
    right: Expr[int]
    
    def __init__(self, left: Expr[int], right: Expr[int]):
        self.left = left
        self.right = right


def eval(e: Expr[A]) -> A:
    if isinstance(e, Const):
        # reveal_type(e)  # => Const[Any]
        return e.value
    elif isinstance(e, Add):
        # reveal_type(e)  # => <nothing>
        return eval(e.left) + eval(e.right)
        # error: <nothing> has no attribute "left"
        # error: <nothing> has no attribute "right"
    else:
        assert False


example = Add(Const[int](2), Const[int](1))
print(eval(example))

But in the elif isinstance(e, Add) branch the type of e is inferred as '<nothing>' causing type errors.

As '<nothing>' is not documented (c.f. #3030), I'm not sure if this is intended behavior. So I report it here just in case, though the attempt is just out of curiosity.

[cpeisert]

In the example below of the same bug, after the isinstance(obj, SubclassA) check, obj is inferred to be <nothing>.

from typing import Generic, Optional, TypeVar

T = TypeVar("T")

class BaseClass(Generic[T]):
    def __init__(self, item: T) -> None:
        self.item: T = item

class SubclassA(BaseClass[int]):
    pass

def generic_func(obj: BaseClass[T]) -> Optional[T]:
    if isinstance(obj, SubclassA):
        return obj.item
        # error: Returning Any from function declared to return "Optional[T]"
        # error: <nothing> has no attribute "item"
    return None

[pdarragh]

I also ran into this recently. From some more playing around with it, it seems like there's an issue when:

1. The function explicitly references the generic type parameter, or:
2. The function is a method in a superclass of the checked instance's type.

My minimal examples to show this:

from typing import Any, Generic, TypeVar


T = TypeVar('T')


class Foo(Generic[T]):
    def __init__(self, value: T):
        self.value = value

    def int_through_superclass(self) -> int:
        if isinstance(self, IntFoo):
            # error: <nothing> has no attribute "value"
            return self.value
        return -1


class IntFoo(Foo[int]):
    def int_through_subclass(self) -> int:
        # no issue
        return self.value

    def int_through_subclass_with_isinstance_check(self) -> int:
        if isinstance(self, IntFoo):
            # no issue
            return self.value
        return -1


def t_func(foo: Foo[T]) -> T:
    if isinstance(foo, IntFoo):
        # error: <nothing> has no attribute "value"
        return foo.value
    return foo.value


def int_func(foo: Foo) -> int:
    if isinstance(foo, IntFoo):
        # no issue
        return foo.value
    return -1


def int_t_func(foo: Foo[T]) -> int:
    if isinstance(foo, IntFoo):
        # error: <nothing> has no attribute "value"
        return foo.value
    return -1

There may be other cases (like methods in subclasses), but I didn't check them.

[noudin-ledger]

Still opened and still an issue, I'd love being able to mimick GADTs in python

[ichard26]

While this issue came before, I'm closing this in favour of #12949 which describes the same bug in a much simpler way. Thanks for reporting!