You need more than an advanced type system. You need a declarative constraint solving and proof system. Instead of telling the compiler how to perform a task, y

You need more than an advanced type system. You need a declarative constraint solving and proof system. Instead of telling the compiler how to perform a task, you would declare the assumptions and the desired relationships and then, with the help of the proof system, determine what implementation fullfills exactly those constraints.