Если вы хотите наиболее простую систему типов, то это вероятно будут зависимые типы (когда сами типы становятся объектами первого класса).
По взрослому, это Coq, F*, Agda, Idris, Lean. Но страшно далеки они от мэйнстрима :)

Однако в питончике уже есть, в некотором смысле, завтипы, т.к. он позволяет манипулировать ими (да и ещё много-много чем) нативно.

И при желании можно вот так легко и просто реализовать dependent types в Python.