<nothing> is inferred when mimicking GADT

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.

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

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

The function explicitly references the generic type parameter, or:
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.

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

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!

Navigation Menu

Repository navigation

<nothing> is inferred when mimicking GADT #8252

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

<nothing> is inferred when mimicking GADT #8252

Description

Activity

cpeisert commented on Jan 8, 2021

pdarragh commented on May 3, 2021

noudin-ledger commented on Jun 7, 2023

ichard26 commented on Aug 22, 2023

Metadata

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

Issue actions