In dependent types, types depend on values. Here, the type depends on the value that is the function name :) As far as I know, this is literally actually possible in Idris, right now.
> the more code you put into the type system the higher the chance that your dependent type specification haS a bug in it.
Unbounded infinity has infinite, uncountable bugs. A defined, bounded, well-constructed, proven type system has fewer bugs. Dependent types are not an axis of explosion, but rather a way to express useful bounds on multiple axes.
Reading your other comment, I'll concede that it's not impossible to encode these things into the type system. I don't think it will scale beyond toy examples (at least until AGI is a thing). There are plenty of function names that represent highly specific business processes (and jargon) and I don't see how any type system will have enough context for that.
Less bugs does sound good, but after a minute thought there still seem to be uncountably infinite bugs even in the presence of dependent types. Just a few less than without. :)
Wrote a bit more earlier: https://news.ycombinator.com/item?id=24716477
> the more code you put into the type system the higher the chance that your dependent type specification haS a bug in it.
Unbounded infinity has infinite, uncountable bugs. A defined, bounded, well-constructed, proven type system has fewer bugs. Dependent types are not an axis of explosion, but rather a way to express useful bounds on multiple axes.