Alexandre Martin

@nikomatsakis I don’t think there’s any good reason why the where clauses are not inlined. I probably thought it was equivalent because there would be a « perfect match »...

@nikomatsakis I guess for that RFC, we could just move the `ObjectSafe` condition from the WF rules onto the generated impls (in the where clauses of the generated impls, presumably)...

Well I don't know, currently we still have rules of the form `WF(T: Trait) :- WF(T)` (i.e. we still require that the input types are well formed), so maybe tweak...

Here is my last take at that. So we need to cleanly separate impls and WF requirements. The following impl block: ```rust impl Foo for SomeType where W1, ..., Wk...

No, the caller just has to prove that `T: Foo` holds, because indeed `i32FooImplWF` has already been proven. This is actually related to how I formally defined soundness: let `A`...

@arielb1 Yes I agree with you, and actually I did think about that when I sketched my proof. The thing is that we cannot ask for your definition in an...

Ah sorry, I responsed to the un-edited message. Is `WF(Γ)` the same thing as `Implied(Γ)`? If so, I agree.

cc @nikomatsakis, @withoutboats ## Plan for GATs OK so we still need to figure out how to translate bounds on GATs, especially when it comes to WF requirements and implied...

Actually this has been longly discussed :) If you put it on the fallback clause instead of the WF clause, this allows for a slight inconsistency within implied bounds. That...

@nikomatsakis there is a bug in the implied bounds rule for GATs as described above, I think it should be: ``` FromEnv(::Item: Bounds) :- FromEnv(Self: Foo), FromEnv(WC) ``` also @LukasKalbertodt...