Various workarounds have been devised (see e.g. https://hal.archives-ouvertes.fr/ha...).
Recent additions to Coq (native integers, native arrays) are likely to make it feasible to formalize hash-consing natively and efficiently. The topic of the internship is to do achieve such formalization and apply it to useful sample use cases.
