Idris[1] already has a working system for this, and it's type system is more complicated (it has much more support for dependent typing). It allows this princip

Idris[1] already has a working system for this, and it's type system is more complicated (it has much more support for dependent typing). It allows this principle for regular function names as well. [1]: http://www.idris-lang.org/ http://www.idris-lang.org/