-
Notifications
You must be signed in to change notification settings - Fork 17
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Make Self
clause explicit in trait item declarations
#514
base: main
Are you sure you want to change the base?
Conversation
19dc60a
to
ea90198
Compare
I think this goes in the right direction, but there are some details I don't fully get. In particular I'm not sure I understand: "The special clause is passed when the method is bound in the |
Here's an example inspired from the tests diff: trait test_crate::Trait<Self, B>
{
parent_clause0 : [@TraitClause0]: core::marker::Sized<B>
parent_clause1 : [@TraitClause1]: core::marker::Sized<Self::Item>
type Item
fn method<C, [@TraitClause0]: core::marker::Sized<C>> = test_crate::Trait::method<Self, B, C>[Self, @TraitClause0_0]
// ^^^^ `TraitRefKind::SelfId`
// ^^^^ normal type param named `Self`
// before this PR:
// fn method<C, [@TraitClause0]: core::marker::Sized<C>> = test_crate::Trait::method<Self, B, C>[@TraitClause0_0]
}
fn test_crate::Trait::method<Self, B, C>() -> @TraitClause0::Item // was `-> Self::Item` before
where
[@TraitClause0]: test_crate::Trait<Self, B>, // added by this PR
[@TraitClause1]: core::marker::Sized<C>, As you can see, since #512 in a trait declaration/implementation a method is not just a |
Ok, thanks! So we agree that now all trait method declarations are mutually recursive with the trait itself? Doesn't that cause issues on the Aeneas' side? |
Yep
I don't know yet, this requires more binder-related fixes on the aeneas side first. If it does cause issues I hope that'll be only for provided methods (which I'll be fixing next), we'll see. |
928747f
to
7f8bece
Compare
Self
clause explicit in trait method declarationsSelf
clause explicit in trait item declarations
dcde15c
to
0c3cbb3
Compare
But we agree that implementations of trait methods don't change (in particular their signature - I don't fully understand this sentence: "Note that this does not affect method signatures: the clauses needed to call a method don't change.")? |
Absolutely
I lack good terminology here. The important property about the two-binding-levels-for-methods I introduced recently is that the The note I was trying to make is that these generics are unchanged by this PR. The thing that is changed by this PR is the generics of the |
0c3cbb3
to
d773757
Compare
Both for consistency fir the corresponding method generics and in case the default const uses values from `Self`.
It was causing type inference problems in visitors.
7d70f18
to
c7243f2
Compare
This is clear and makes sense to me, thanks :) |
For #180 I want trait methods to be completely non-magical functions. #512 made huge progress towards this, but I had forgotten about
Self
clauses.Within a trait declaration (including its associated items), we can use
TraitRefKind::SelfId
to refer to the ambiantSelf: ThisTrait
clause. This is used e.g. to recursively call other trait methods, or access the value of theSelf::Type
associated types. Trait implementations don't need this, because they always know the correct method/type to use directly.In order for methods to be normal functions, I needed to remove uses of this implicit clause. This PR instead makes the clause explicit in the
FunDecl
that corresponds to each method declaration. Note that this does not affect method signatures: the clauses needed to call a method don't change. The special clause is passed when the method is bound in theTraitDecl
(which we can express thanks to #512).