There are a few places related to trait solving in charon and hax where we call normalize_erasing_regions. This has the benefit of normalizing associated types (e.g. <T as Trait>::Type becomes RealType in cases where the real type is known) but the drawback of losing region information. Moreover it's not done consistently. We should do this consistently.
There are a few places related to trait solving in
charonandhaxwhere we callnormalize_erasing_regions. This has the benefit of normalizing associated types (e.g.<T as Trait>::TypebecomesRealTypein cases where the real type is known) but the drawback of losing region information. Moreover it's not done consistently. We should do this consistently.If it's only used for associated types we could also normalize these ourselves as part of https://github.com/AeneasVerif/charon/issues/127.