Keep generic types when translating trait alias in monomorphized mode#1087
Keep generic types when translating trait alias in monomorphized mode#1087Nadrieril merged 8 commits intoAeneasVerif:mainfrom
Conversation
|
Hm that feels wrong, the way trait aliases are translated is that they're translated twice: once as |
I see. I misunderstood how impl blocks work for trait aliases. So we should keep a single trait declaration and provide separate impl blocks for different types, just like the normal traits. Is that correct? |
|
Yep, that's what I had in mind so that trait aliases can be as close to normal traits as possible |
|
The remark is updated to include clearer explanations and examples on how trait implementations for aliases are translated in mono mode. If anything is still unclear or confusing, please let me know. |
| // As an exception, we do not push generics for impls of trait aliases, | ||
| // since this information is already encoded in the impl block itself, | ||
| // just like impls of normal traits. |
There was a problem hiding this comment.
I still don't understand why this ever comes up, and you've not explained why there would ever be generics applied to an item which is monomorphic. But I'll accept this fix since it only applies to names
There was a problem hiding this comment.
I just expect there's a deeper bug with trait aliases + mono that will show up somewhere else, so let's keep that in mind
There was a problem hiding this comment.
I still don't understand why this ever comes up, and you've not explained why there would ever be generics applied to an item which is monomorphic. But I'll accept this fix since it only applies to names
This comes up from a difference between how normal trait impls and trait alias impls are represented in Hax. In Mono mode, the generic_args stored in the Hax item_ref for normal trait impls is empty. In contrast, for trait alias impls, the generic_args field still contains type arguments (including those for Self and other generic parameters).
At the same time, other monomorphic items (e.g., functions instantiated from generics) require an Instantiated suffix (e.g., f::<i32>) to record the concrete instantiation in their names. However, for impl blocks, the generic arguments are already encoded directly in the impl itself (e.g., impl A<i32> for u32). Therefore, I treat trait alias impls specially and avoid pushing generics for them.
There was a problem hiding this comment.
I just expect there's a deeper bug with trait aliases + mono that will show up somewhere else, so let's keep that in mind
I did encounter another issue related to trait aliases when translating the Rust standard library in Mono mode. I have not yet checked it in detail. I'll do that next.
There was a problem hiding this comment.
In Mono mode, the generic_args stored in the Hax item_ref for normal trait impls is empty.
That doesn't seem right, an ItemRef always should have exactly the number of arguments that the item's ParamEnv expects
There was a problem hiding this comment.
I understand now: your code is right, and in fact should apply to all impls and not just trait alias impls. See the last commit of #1123.
There was a problem hiding this comment.
I see. The current code that deals with names is much more strucutured and general. Thank you!
2 participants
This PR closes #1086 . We keep the generic types (such as
Self) of trait aliases in their declarations and impl blocks to make it consistent with the "normal" trait declarations in mono mode.