Chalkify - Tweak Clause definition and HRTBs
#49497
Conversation
shepmaster
added
the
S-waiting-on-review
| goal: impl_trait, | ||
| hypotheses: vec![from_env], | ||
| }; | ||
| Lrc::new(vec![Clause::ForAll(ty::Binder::dummy(clause))]) |
There was a problem hiding this comment.
This could still be a Clause::Implies, no?
There was a problem hiding this comment.
In chalk, clauses which come from the program are always fully quantified so as to account for generic parameters, e.g.:
impl<T> Foo for T {}would lower to the following clause:
forall<T> { T: Foo }
In rustc, there is no concept of « quantified by type », only by lifetime (and quantification by lifetime is only used for higher ranked types like in for<‘a> fn(&’a i32)).
So the binder in front of the clause is indeed not useful for the moment, but you can view it as just a placeholder until rustc binders are reworked in order to account for types.
| goal: trait_pred, | ||
| hypotheses: where_clauses.into_iter().map(|wc| wc.into()).collect() | ||
| }; | ||
| Lrc::new(vec![Clause::ForAll(ty::Binder::dummy(clause))]) |
src/librustc_traits/lowering.rs
Outdated
| Clause::Implies(program_clause) => program_clause, | ||
| Clause::ForAll(program_clause) => program_clause.skip_binder(), | ||
| }; | ||
| // Skip the top-level binder for a less verbose output |
There was a problem hiding this comment.
very nit, but it seems like this comment is describing the let program_clause = match ... more so than the code below it
There was a problem hiding this comment.
Yeah definitely, I’ll fix that :)
| /// is equivalent to the implication `G1..Gn => D`; we usually write | ||
| /// it with the reverse implication operator `:-` to emphasize the way | ||
| /// that programs are actually solved (via backchaining, which starts | ||
| /// with the goal to solve and proceeds from there). |
There was a problem hiding this comment.
(Actually @nikomatsakis’s comment from his chalkify-engine branch :p)
|
@nikomatsakis done ✅ |
|
@bors r+ |
|
📌 Commit 1074a22 has been approved by |
bors
added
S-waiting-on-bors
Chalkify - Tweak `Clause` definition and HRTBs r? @nikomatsakis
tmandry
added
the
WG-traits
r? @nikomatsakis