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, x: T) -> Eq[T, T]:
        pass

    @staticmethod
    def refl(n: T) -> Eq[T, T]:
        return Refl(n)


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

    @typing.override
    def __new__(cls, x: T) -> Eq[T, T]:
        return super().__new__(cls, x)
    
    def __init__(self, x: T) -> None:
        self._x: typing.Final = x


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(two)
bad_refl_two: Eq[Two, Three] = Refl(two)
bad_refl_three: Eq[Two, Three] = Refl(three)