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/