Move trait methods in cyclic dependencies bundling.

[maximebuyse]

Fixes #1068

[W95Psp]

Mmh, here the problem is that we assume (in the F* backend!) that a top-level foo exists in the module where a trait with a method foo was defined.
This is true only because of how F* deals with type-classes: we can't "leak" this backend-specific representation globally.

Also, we want to get rid of type-classes in F*, when we will do so, things will break.

I see two options:

1. I can fix F* upstream to make that include Foo {my_typeclass} by default includes also the methods
2. we can hack something in the F* backend

What do you think? Would (2) be easy enough? I won't have time to do (1) before my holidays.

[maximebuyse]

Mmh, here the problem is that we assume (in the F* backend!) that a top-level foo exists in the module where a trait with a method foo was defined. This is true only because of how F* deals with type-classes: we can't "leak" this backend-specific representation globally.

Also, we want to get rid of type-classes in F*, when we will do so, things will break.

I see two options:

1. I can fix F* upstream to make that `include Foo {my_typeclass}` by default includes also the methods

2. we can hack something in the F* backend

What do you think? Would (2) be easy enough? I won't have time to do (1) before my holidays.

I am not sure (1) would work because then things in the bundle could still refer to the original module creating a cyclic dependency. And if the plan is to get rid of type classes someday I guess (2) makes sense. I'll try to do something like that.

[maximebuyse]

Mmh, here the problem is that we assume (in the F* backend!) that a top-level foo exists in the module where a trait with a method foo was defined. This is true only because of how F* deals with type-classes: we can't "leak" this backend-specific representation globally.
Also, we want to get rid of type-classes in F*, when we will do so, things will break.
I see two options:

1. I can fix F* upstream to make that `include Foo {my_typeclass}` by default includes also the methods

2. we can hack something in the F* backend

What do you think? Would (2) be easy enough? I won't have time to do (1) before my holidays.

I am not sure (1) would work because then things in the bundle could still refer to the original module creating a cyclic dependency. And if the plan is to get rid of type classes someday I guess (2) makes sense. I'll try to do something like that.

Actually I think what we want is a modified version of what I implemented in this PR. We want to do the renaming of references to the trait method, we just don't want the includes in the original module for the trait methods.

The problem with this approach is if we translate a library (that contains a trait that gets bundled) and then some other crate that uses the trait from the library. If we translate them with two different applications of hax, then we might refer to the trait methods in the wrong module. But is it possible to translate things independently like that @W95Psp ?

[W95Psp]

Yes, I agree: we want to renaming, but maybe not the includes.
However, aren't the renaming local to the moved items? e.g. only renaming occurs only for items within a bundle?

And yes, definitively, this would be an issue when we extract two different crates where one uses the other.
We do so in libcrux, and we want to support that, generally.

[maximebuyse]

Yes, I agree: we want to renaming, but maybe not the includes. However, aren't the renaming local to the moved items? e.g. only renaming occurs only for items within a bundle?

And yes, definitively, this would be an issue when we extract two different crates where one uses the other. We do so in libcrux, and we want to support that, generally.

After discussing this the decision is to go with (2). We'll open an issue to get rid of this once we stop using fstar type classes.

[maximebuyse]

@W95Psp I implemented what we discussed. #1078 is the issue to keep track of this hack and remember to get rid of it when possible.

[W95Psp]

I was expecting to see a condition based on includes_for_bundled_trait_methods only at the place where you create Alias. I don't get why there are two.
Unrelated to this PR, I think the arguments to shallow_copy are getting unclear. I wonder if we should not inline this function: the argument variants_renamings looks unrelated to the notion of "making a shallow copy".

[maximebuyse]

Yes, maybe we should refactor. The thing is where we create aliases, we also do the renaming. But in case we don't create aliases we still want to do the renaming (but we don't want to do it twice in the other case). So that's why we have this condition here (but maybe we could improve).