Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Recursive sequence type of Sequence[NotAString] should not accept str #819

Open
jorenham opened this issue Nov 24, 2024 · 14 comments
Open
Labels

Comments

@jorenham
Copy link
Collaborator

jorenham commented Nov 24, 2024

This is a (p)repost from python#18184, which also applies here:

The false negative can be reproduced with:

from collections.abc import Sequence
from typing import TypeAlias

class Scalar: ...

Vector: TypeAlias = Sequence[Scalar]
Tensor: TypeAlias = Vector | Sequence["Tensor"]

accepted_vector: Vector = [Scalar()]     # true negative
rejected_vector: Vector = "duck"         # true positive: ducks aren't vectors

accepted_tensor: Tensor = [[[Scalar()]]] # true negative
rejected_tensor1: Tensor = object()      # true positive: objects aren't tensors
rejected_tensor2: Tensor = "duck"        # false negative: ducks are tensors...?

mypy-play


alternative example:

class Increment[T]:  # covariant
    def current(self, /) -> T: ...  # type: ignore[empty-body]

type Infinity = Increment[Infinity]

type Zero = Increment[None]
type Integer = Zero | Increment[Integer]


def int2inf(integer: Integer, /) -> Infinity:
    return integer  # rejected => ok

def inf2int(infinity: Infinity, /) -> Integer:
    return infinity  # accepted => wut
@jorenham
Copy link
Collaborator Author

oh woops, this should be labeled as bug

@jorenham jorenham changed the title false negative with recursive type alias involving float sequences Recursive sequence type of Sequence[NotAString] should not accept str Nov 24, 2024
@KotlinIsland
Copy link
Owner

oh woops, this should be labeled as bug

feel free to update it 😁

@jorenham jorenham added bug Something isn't working and removed feature labels Nov 24, 2024
@KotlinIsland
Copy link
Owner

is this the same thing?

class C[T]: ...
type A = C[A] | int
type B = C[B]

b: B
a: A = b

@KotlinIsland
Copy link
Owner

KotlinIsland commented Nov 24, 2024

@jorenham
Copy link
Collaborator Author

is this the same thing?

class C[T]: ...
type A = C[A] | int
type B = C[B]

b: B
a: A = b

What's the | int for btw 🤔 ?

@KotlinIsland
Copy link
Owner

What's the | int for btw 🤔 ?

just for being closer to the original egg

@jorenham
Copy link
Collaborator Author

this seems relevant

basedmypy/mypy/subtypes.py

Lines 170 to 189 in 0935784

if mypy.typeops.is_recursive_pair(left, right):
# This case requires special care because it may cause infinite recursion.
# Our view on recursive types is known under a fancy name of iso-recursive mu-types.
# Roughly this means that a recursive type is defined as an alias where right hand side
# can refer to the type as a whole, for example:
# A = Union[int, Tuple[A, ...]]
# and an alias unrolled once represents the *same type*, in our case all these represent
# the same type:
# A
# Union[int, Tuple[A, ...]]
# Union[int, Tuple[Union[int, Tuple[A, ...]], ...]]
# The algorithm for subtyping is then essentially under the assumption that left <: right,
# check that get_proper_type(left) <: get_proper_type(right). On the example above,
# If we start with:
# A = Union[int, Tuple[A, ...]]
# B = Union[int, Tuple[B, ...]]
# When checking if A <: B we push pair (A, B) onto 'assuming' stack, then when after few
# steps we come back to initial call is_subtype(A, B) and immediately return True.
with pop_on_exit(type_state.get_assumptions(is_proper=False), left, right):
return _is_subtype(left, right, subtype_context, proper_subtype=False)

@KotlinIsland
Copy link
Owner

i really don't understand this. if you could put together an egg, that would be good

@jorenham
Copy link
Collaborator Author

how about the egg in the issue itself?

@KotlinIsland
Copy link
Owner

KotlinIsland commented Nov 29, 2024

how about the egg in the issue itself?

i don't get that one 😅

probably an egg where it's not using any stdlib, and there is a positive and a negative

@jorenham
Copy link
Collaborator Author

class Increment[T]:  # covariant
    def current(self, /) -> T: ...  # type: ignore[empty-body]

type Infinity = Increment[Infinity]

type Zero = Increment[None]
type Integer = Zero | Increment[Integer]


def int2inf(integer: Integer, /) -> Infinity:
    return integer  # rejected => ok

def inf2int(infinity: Infinity, /) -> Integer:
    return infinity  # accepted => wut

@KotlinIsland
Copy link
Owner

does the covariance impact the situation?

is this the same thing?

class Thing: ...
class Box[T]: ...

type CouldEnd = Box[CouldEnd] | Thing
type Recursive = Box[Recursive]

b: Recursive = Box()
a: CouldEnd = b # this should be an error

c: CouldEnd = Box[Box[Box[Thing]]]() # this is just for fun

@jorenham
Copy link
Collaborator Author

jorenham commented Dec 1, 2024

does the covariance impact the situation?

is this the same thing?

class Thing: ...
class Box[T]: ...

type CouldEnd = Box[CouldEnd] | Thing
type Recursive = Box[Recursive]

b: Recursive = Box()
a: CouldEnd = b # this should be an error

c: CouldEnd = Box[Box[Box[Thing]]]() # this is just for fun

I thought that both mypy and pyright (incorrectly) inferred T@Box as covariant in such cases 🤔

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

2 participants