Which is despite, a decade of attempts, still missing dependent types. Time to embrace Idris.

Or embrace logic + functional programming: Curry. https://curry-language.org/