How to use dependent types in practice is still a research topic. There’s some interesting problems with having a Turing powerful type system. Like type equality doesn’t work the same way.