Let charon manage Self clauses

[Nadrieril]

Companion PR to AeneasVerif/charon#514.

This removes the need for managing the special Self clause in methods ourselves. One consequence is that in AeneasVerif/charon#514 I had to add a pass that removes unused Self clauses otherwise any trait impl that reuses an associated constant default would end up self-recursive. That's why you can see in the tests diff that some provided methods end up losing their Self clause: it's because of that same pass. This may be leaving the translation in a bit of an incorrect state while AeneasVerif/charon#180 isn't finished.

[Nadrieril]

Ah, this in fact doesn't pass typechecking in lean. I wasn't sure these methods were used. I guess I have to finish AeneasVerif/charon#180 first.

[sonmarcho]

Ah, this in fact doesn't pass typechecking in lean. I wasn't sure these methods were used. I guess I have to finish AeneasVerif/charon#180 first.

What doesn't typecheck? I don't see any issue in the diffs or in CI.

[Nadrieril]

What doesn't typecheck? I don't see any issue in the diffs or in CI.

That's because I just fixed it :) I had messed up the self clauses and didn't think I could easily fix it but I found a way.

[sonmarcho]

Also, about the code you generate: at some point I thought of making the default methods take as inputs exactly the list of functions they need rather than a whole instance of the trait. Removing the input self clause when it is not needed is already a nice improvement (and I'm thinking that taking a list of functions may be a bit too fine-grained).

[Nadrieril]

at some point I thought of making the default methods take as inputs exactly the list of functions they need

Yes we discussed this together :p