static verification of equality in python! try it on a typechecker like pyright

README.md

use it in pyright: playground link

static_equality.py

from __future__ import annotations

import abc
import dataclasses
import typing

type Nat = Zero | Succ[Nat]

@dataclasses.dataclass(slots=True, frozen=True)
@typing.final
class Zero:
    pass

@dataclasses.dataclass(slots=True, frozen=True)
@typing.final
class Succ[N: Nat]:
    n: Nat

class Eq[T, U](abc.ABC):
    @abc.abstractmethod
    def __new__(cls) -> Eq[T, T]:
        pass

@typing.final
class Refl[T](Eq[T, T]):
    __match_args__ = ("x",)

    @typing.override
    def __new__(cls) -> Eq[T, T]:
        return super().__new__(cls)

type Two = Succ[Succ[Zero]]
type Three = Succ[Two]

two: Two = Succ(Succ(Zero()))
three: Three = Succ(Succ(Succ(Zero())))

good_eq_two_two: Eq[Two, Two] = Refl()
bad_refl_two: Eq[Two, Three] = Refl()