You very quickly get undecidable type checking with such a powerful typesystem. Then you need a way to handle that, usually the solution is to help the type che

You very quickly get undecidable type checking with such a powerful typesystem. Then you need a way to handle that, usually the solution is to help the type checker along by providing a proof that your code inhabits the claimed type. Then you need a way to have the proof live together with the code, a proof language, and preferably a whole library of proofs people can build on. If this sounds fun then you can go play with e.g idris or F*.