We no longer abuse empty strings for anonymous binders. Instead, we
now have a data type for binders: a binder is either named or
anonymous.