That's just plain-old dependent typing, isn't it? What's in this and not in, say, Idris, such that you can say that it's a whole new paradigm?