Nadrieril
Nadrieril
You're right, but this is quite difficult to fix in general. Is this something you need or just something you noticed?
Ok than it's a known imperfection of Charon that I hope we can fix eventually, but not a priority. Leaving the issue open for anyone else who notices this.
In this case it's related to closures, which are things that only exist inside a MIR body and as such tend to have erased lifetimes even in their definition. Another...
There are no constants involved here though
We already compute a graph of all definitions in `reorder_decls`; it might be relatively easy to add a reachability analysis to it, where the roots of the reachability would be...
Interesting, this is an explicit hack here: https://github.com/AeneasVerif/charon/blob/bc5918c6e736a9cf815d4e5fb4f2935cd4c4c8c0/charon/src/transform/reorder_decls.rs?plain=1#L393-L410
As the comment says, we can likely remove this hack once aeneas makes use of `--remove-associated-types`.
@sonmarcho with your recent change, is this still the case?
Could you link the other open issues we have on the topic?
#495 has been solved, but unfortunately there are still mismatches in function generics around closures. This is tracked in #194.