It's not that expensive: just use De Bruijn notation under the hood. (I've seen a system that does this, and this is how it works.)
But then the point of giving unique names to avoid using De Brujin indices is moot