Supporting `dyn Trait`

[ssyram]

Thanks to the hard and quick work by @Nadrieril , now most parts of this PR have been merged into the main branch, with only two non-urgent parts:

• The drop shim for array or tuples could be handled by some parts of VTable Metadata pass: size, align & drop , this is yet to separate and integrate to the current mechanism.
• The vtable instances support for closures.

These will be further split into new PRs, but as they are not that urgent, it may take place in the coming year.

Former Text (As History of What this PR Did)

Now the dyn Trait Support should be quite ready with a few TODOs.

Features Implemented

• Supporting associated types, now the vtable structs & instances all additionally take additional generic types corresponding to and taken from &dyn Trait's associated type restrictions. The basic support of the associated types are from #796.
• The vtable instances are now properly generated for the concrete impls, i.e., those with explicit impl Trait for Ty environments.
• The vtable method calls are propertly generated that, calling methods of &dyn Trait will be translated to finding the corresponding function pointer from the vtable (fetched by ptr_metadata operation) and then call the function pointer.
• A new pass is added to compute the correct vtable instance metadata when possible, i.e., the size, align and, the most complex case, the drop fields. Naturally, the content will not be computable if the stuff is behind a generics, this is inevitable and the fields will remain unknown. But everything should be explicit in the monomorphized case in the future. Specifically, the size and align subjects to whether the layout of the type is properly computable. The drop field, as the most complex case, now also handles the cases when the concrete impl types are Arrays & Tuples -- they should be the only composite cases.
• The vtable instances support for closures are now added. All tests passed. But there are identified issues, see ssyram/charon#20 for the closure itself. But it should work properly in most of the cases -- as dyn FnOnce is really strange, and rare.

TODOs

• [ ] Monomorphization support for dyn Trait.
• [x] Vtable instances for closures.

[Nadrieril]

Haven't reviewed everything but from what I've seen: could you change how we represent the existential predicates? The current encoding will cause issues with generics (see inline comments).

[ssyram]

Thanks for all the suggestions from both of you! I'm still not sure about how to refractor the Predicate form. So I will leave it to the discussion in Zulip. Let me fetch & implement the vtable struct & instances first.

[ssyram]

Many fixes applied. Thanks for the advice. Mainly involving the fix for the three kinds of existential predicates. But I'm still not sure about if they work as expected...

[Nadrieril]

Could you add a lot of tests please? We need to cover edge cases even if we don't support them yet (write //@ known-failure at the top for these cases). We should have tests for supertraits, multiple supertraits, casting in a generic context, associated type projections, + 'a bounds, multiple trait bounds (dyn Any + Send), just builtins (dyn Send), traits with methods that are generic and have a Self: Sized bound (which makes them dyn-compatible but means the vtable doesn't have all the methods), etc.

[ssyram]

Yes, of course. Many tests are coming when the infrastructure is about to get done... Maybe we can focus on the implementation for now?

[Nadrieril]

Maybe we can focus on the implementation for now?

The tests will help me understand what the implementation is doing, I can't just be running the code in my head. It's imo crucial to add the tests while doing the implementation because that's when we think of edge cases. When we're done implementing it's too late.

[ssyram]

The original info is too messy, I reset everything and let it be the same as #796 and will start working on it from this point.

[Nadrieril]

For the CI failures, unfortunately I don't know of a good way to normalize the paths, so just add //@ no-check-output to those test files.

[Nadrieril]

Could you please split this PR into several for the many features it implements? I see at least:

• Remove the redundant TraitDeclRefs in TraitRefKind (that one could just be its own commit, doesn't need a full PR);
• Handle dyn Trait with associated types;
• Translate dyn Trait method calls;
• Support dyn Fn* for closures;
• There's probably more.

I can't review it like this with a messy commit history and a bunch of different features implemented at once. What I do see looks good though!

[ssyram]

The base of this, which implements the first feature you mentioned, is in your PR #796 . I reset the PR to start from that branch. I've made the PR to be as explicit as possible by trying to have one new feature in one commit ever since 171b81a. To break everything into new PRs involves resolving the connection with the current main branch... This is quite a tough work... So basically, the basic support is up until 171b81a, which accomplished the support of instances for Concrete impl blocks. Then, the pass to compute the metadata (e.g., size) is basically done in f68593d. After that, the support for vtables of closures is done in 8778c91 (sorry for the name, it should be vtables support for closures).

Another point is that the modification is one based on another, which makes it very hard to break into several self-contained PR... Do you have any good idea on this?

Also, the //@ no-check-output has been added but some new errors came.

[Nadrieril]

Sorry, I didn't mean that the PRs should be independent. It's ok if one PR depends on another. What I want is to be able to review one change at a time.