mypy plugin allows false positive error when exhaustively pattern matching on Result

[johnthagen]

Bug report

What's wrong

Again, this is a really cool project ❤️

Consider the following code:

from enum import Enum, auto
import math
from typing import TypeAlias

from returns.result import Failure, Result, Success


class MathError(Enum):
    DivisionByZero = auto()
    NonPositiveLogarithm = auto()


MathResult: TypeAlias = Result[float, MathError]


def div(x: float, y: float) -> MathResult:
    if y == 0.0:
        return Failure(MathError.DivisionByZero)

    return Success(x / y)


def ln(x: float) -> MathResult:
    if x <= 0.0:
        return Failure(MathError.NonPositiveLogarithm)

    return Success(math.log(x))


def op_(x: float, y: float) -> MathResult:
    z = div(x, y)
    match z:
        case Success(ratio):
            return ln(ratio)
        case Failure(_):
            return z

mypy configuration in pyproject.toml

[tool.mypy]
ignore_missing_imports = true
strict = true
plugins = [
    "returns.contrib.mypy.returns_plugin",
]

Running:

$ mypy pattern_div.py
pattern_div.py:32: error: Missing return statement

Related to #1090

How is that should be

As far as I can tell (new to returns), I'm matching exhaustively here, so I would not expect a mypy error.

mypy seems to understand exhaustive matching in general. mypy does not throw a type checking error in the following snippet.

def test(err: MathError) -> int:
    match err:
        case MathError.DivisionByZero:
            return 0
        case MathError.NonPositiveLogarithm:
            return 1

System information

• python version: 3.10.2
• returns version: 0.19.0
• mypy version: 0.942

$ pip list
Package           Version
----------------- -------
black             22.3.0
click             8.1.2
distlib           0.3.4
filelock          3.6.0
isort             5.10.1
mypy              0.942
mypy-extensions   0.4.3
packaging         21.3
pathspec          0.9.0
pep517            0.12.0
pip               22.0.4
pip-tools         6.6.0
platformdirs      2.5.1
pluggy            1.0.0
py                1.11.0
pyparsing         3.0.8
returns           0.19.0
setuptools        62.1.0
six               1.16.0
toml              0.10.2
tomli             2.0.1
tox               3.25.0
typing_extensions 4.1.1
virtualenv        20.14.1
wheel             0.37.1

[johnthagen]

Also, related to this issue and #1090, is this still valid?

returns/setup.cfg

Lines 164 to 165 in cd08c2a

	# mypy is not ready to deal with Pattern Matching
	exclude = .*test_.*pattern_matching

Curious if @ariebovenberg has any thoughts as someone who has been using pattern matching and returns.

[sobolevn]

I am 80% sure that this is a mypy bug 🤔

[johnthagen]

I did a little more digging and added an assert_never statement:

#!/usr/bin/env python3

from enum import Enum, auto
import math
from typing import NoReturn

from returns.result import Failure, Result, Success


# TODO: Remove this once mypy > 0.942 is released and simply import typing_extensions.assert_never
#   https://github.com/python/mypy/issues/12613
def assert_never(__arg: NoReturn) -> NoReturn:
    """Assert to the type checker that a line of code is unreachable.

    Example::

        def int_or_str(arg: int | str) -> None:
            match arg:
                case int():
                    print("It's an int")
                case str():
                    print("It's a str")
                case _:
                    assert_never(arg)

    If a type checker finds that a call to assert_never() is
    reachable, it will emit an error.

    At runtime, this throws an exception when called.

    """
    raise AssertionError("Expected code to be unreachable")


class MathError(Enum):
    DivisionByZero = auto()
    NonPositiveLogarithm = auto()


MathResult = Result[float, MathError]


def div(x: float, y: float) -> MathResult:
    if y == 0.0:
        return Failure(MathError.DivisionByZero)

    return Success(x / y)


def ln(x: float) -> MathResult:
    if x <= 0.0:
        return Failure(MathError.NonPositiveLogarithm)

    return Success(math.log(x))


def op_(x: float, y: float) -> MathResult:
    z = div(x, y)
    match z:
        case Success(ratio):
            return ln(ratio)
        case Failure(_):
            return z
        case _ as u:
            assert_never(u)

This reveals the type that is "slipping through" the match (i.e. all of the type), though it doesn't shed much more light on why the narrowing/exhaustiveness isn't happening:

$ mypy pattern_div.py
pattern_div.py:65: error: Argument 1 to "assert_never" has incompatible type "Result[float, MathError]"; expected "NoReturn"

When using assert_never with Union-based algebraic data types, I was able to narrow down which variants in a match were missing, but I'm guessing Result[T] is much more complex.

An example I was using: johnthagen/sealed-typing-pep#4 (comment)

[sobolevn]

I guess we can refactor Result to be Union 🤦
I remember that a long time ago there were some problems with this approach. But, I don't remember the details.

[ariebovenberg]

One problem with the union approach, I found, was that you can't have nice classmethods on the union. Something like Maybe.from_optional wouldn't be possible if Maybe was a union. It'd have to be a standalone function, which is a lot less convenient.

Regarding refactoring to Union: there was once a plan to include typing.sealed in PEP622, but it was dropped. I heard that they wanted to perhaps include this later. If this proposal is still alive, it could be worth it to wait.

[sobolevn]

At least this works in mypy (latest):

from typing import Union, TypeAlias

class A:
    @classmethod
    def from_some(cls) -> A:
        return A()

class B:
    @classmethod
    def from_some(cls) -> B:
        return B()

Result: Union[A, B]
reveal_type(Result.from_some())  # N: Revealed type is "Union[ex.A, ex.B]"

The runtime part is always easier 😉

[sobolevn]

Oh, I see one more problem: Union[ex.A, ex.B] is not very readable. Result[R, E] is much better than Union[Success[R], Failure[E]] 😞

[johnthagen]

@ariebovenberg Funny you should bring up typing.sealed, I am actually working on a PEP for this currently: https://github.com/johnthagen/sealed-typing-pep

There is some initial discussion on the typing-sig about this: https://mail.python.org/archives/list/typing-sig@python.org/thread/7TB36OWSWRUIHUG36F4FHE3PVKVM3RSC/

Having more people voice support for an ADT in which methods and state can be added to the base type could be helpful.

[sobolevn]

You totally have my support on this! Where should I sign? 😆

[johnthagen]

@sobolevn Working on the PEP with @drhagen. We'll hopefully have a draft ready soon. When we do, joining typing-sig and providing support for your use case would be helpful.

[sobolevn]

I am already there, just not very active 😉
I've seen recent @sealed discussions there.

[sobolevn]

This does not look possible with the current way of doing things:

from typing import Union

class S:
    def method(self) -> int:
        ...

class F:
    def method(self) -> int:
        ...

Result1 = Union[S, F]
reveal_type(Result1)
# note: Revealed type is "builtins.object"
reveal_type(Result1.method)
# error: "object" has no attribute "method"
# note: Revealed type is "Any"

Result2: Union[S, F]

# error: Variable "ex.Result2" is not valid as a type
# note: See https://mypy.readthedocs.io/en/stable/common_issues.html#variables-vs-type-aliases
def some() -> Result2:
    ...

So, we need @sealed 🙏

[johnthagen]

So, we need @Sealed 🙏

Okay, good to know. We are nearing the completion of the PEP and will ping you when there is a draft ready for you to review.

[johnthagen]

@sobolevn We have revived and resubmitted the @sealed PEP over on Discourse.

• https://discuss.python.org/t/draft-pep-sealed-decorator-for-static-typing/49206