Why is ident-to-string conversion done during parsing instead of compilation?

[andres-erbsen]

IIUC let/n and such associate binders with string names so that compilation can use the same names for Bedrock2 variables. But why do it eagerly, as opposed to accepting normal binders and calling ident_to_string during compilation?

Looking at https://pit-claudel.fr/clement/PhD/RelationalCompilation_Pit-Claudel_2022.pdf page 103 I see an instance where the non-string names change around applying a lemma. Is it the case that nlet is needed so that names can be propagated goals before a lemma is applied to goals after a lemma is applied even if the binder appears both in the conclusion and premise of the lemma?