[@model_trace: <name>] labels redundant?

Is there a reason to have these labels on symbols, in addition to [@model]? It seems that the name they carry always coincides with id_string of the symbol ident. If we need to change the name, e.g. for the SPARK-produced inputs, maybe we can only use [@model_trace: ...] in these cases, but not by default?