Nontransitive subtyping involving protocols and `object`

[JelleZijlstra]

Summary

ty currently fails the last assert in this file:

from ty_extensions import static_assert, is_subtype_of
from typing import Protocol

class P(Protocol):
    def __str__(self) -> str: ...

class P2(Protocol):
    x: int

static_assert(is_subtype_of(object, P))
static_assert(is_subtype_of(P2, object))
static_assert(is_subtype_of(P2, P))

https://play.ty.dev/23be40f7-3ebf-4785-991b-29c7508b5e22

That is, it accepts that P2 <: object and object <: P, but not that P2 <: P.

ty has a property test asserting that subtyping is transitive, but it apparently didn't catch this case.

Transitivity of subtyping is important for making union simplification deterministic, but it seems that is not an issue in practice here, because P is also a subtype of object (in the other direction) and ty prefers simplifying to object.

I think this is more of a curiosity than a real bug that can break soundness, but reporting it anyway in case it's more serious than I thought.

Version

No response

[AlexWaygood]

ty has a property test asserting that subtyping is transitive, but it apparently didn't catch this case.

yes, we don't generate any protocol types to throw at our property tests yet, because our subtyping/assignability implementation for protocols is very much unfinished. I expect there are probably quite a few more issues like this you'd be able to find if you put your mind to it ;-) My plan had been to add protocols to our property tests once we were a bit further along on our protocols implementation.

Progress on protocols has been a bit slower than expected because it turns out that as soon as you start naively poking at the types of a protocol's members to do a subtype check, you end up with stack overflows if that protocol's members contain (directly or indirectly) a recursive reference back to the original protocol... and protocols like that are surprisingly common!

[AlexWaygood]

This was fixed in astral-sh/ruff#20284