Repository navigation
Refactor ProgramClauseData to remove Implies variant - #514
Conversation
jackh726
left a comment
There was a problem hiding this comment.
Just quickly looking over this, the changes look correct. So there's something a bit more subtle here that I'll have to look more deeply at.
|
My best guess for the error is that by introducing an empty chalk/chalk-ir/src/fold/binder_impls.rs Lines 38 to 56 in a6400eb I managed to reproduce the same set of errors (the ones in the list above) with this commit alone: https://github.com/declanvk/chalk/commit/e96058569721eb71587ea294b82ee9c527ebcbf3 |
|
That fixed it! I had to export the |
| .intern(interner) | ||
| }; | ||
|
|
||
| ProgramClauseData(Binders::empty(interner, implication.shifted_in(interner))) |
There was a problem hiding this comment.
I wonder if we should make a helper for this -- i.e., for inserting a binders into something with no captures.
But also, this strikes me as a bit dubious. I wonder if in the Cast routines we could, instead of shifting, assert that !implication.needs_shift(interner).
In particular, I feel like we don't normally embed ProgramClauses within other binders, so I wouldn't expect any references to bound variables in outer scopes -- and if there are any, it feels like the "intent" from a cast operation is sort of ambiguous to me.
So I'd be happier if we don't use cast in these cases.
There was a problem hiding this comment.
That said, it seems like needs_shift needs to be rewritten from a hard-coded helper routine to a method that is available on anything that implements the Visit trait.
|
Yeah, that was going to be my next comment: if we got rid of the Cast impl for one that does the shift, can we find the root "cause" there |
|
I wonder if those cast impls are even used. Probably. |
|
@nikomatsakis nope, neither |
|
Well then let's just remove them and avoid the problem =) |
|
I removed the impl<I, T> Binders<T>
where
T: Visit<I> + Fold<I, I, Result = T> + HasInterner<Interner = I>,
I: Interner,
{
pub fn empty_shift_if_required(interner: &T::Interner, value: T) -> Self {
let value = if value.has_free_vars(interner) {
// If this type contains "bound" types/lifetimes, then it
// needs to be shifted across binders.
value.shifted_in(interner)
} else {
value
};
Self::empty(interner, value)
}
}instead of having to apply |
nikomatsakis
left a comment
There was a problem hiding this comment.
OK, I know I'm changing my mind, but seeing the diff makes me want to keep the impls -- or at least the one that goes from DomainGoal to ProgramClause.
It's hard to figure out the best API for dealing with debruijn indices, but I do think it's nice to have a way to say "here is some fact that contains types etc that are in scope, let me construct a program clause out of it" and not have to worry about the forall binder that would otherwise get added there.
I would perhaps instead just make the |
|
But in any case that's just an optimization, so let's address it separately. It actually fits in with another theme of work I think we should pursue, which is propagating "flags" and the like, similar to what rustc has, which can enable us to create fast-paths quite efficiently. |
|
I removed the unused Should I rebase/squash to address conflicts? |
|
@declanvk Squashing doesn't matter. Rebase yes :) |
The `Implies` variant can be represented as a `ForAll` variant that lacks any variables in the `Binder`.
jackh726
left a comment
There was a problem hiding this comment.
Seems like rebase problems with recursive.rs
Closes #511
As far as I can tell, I didn't change the logic of anything. However, when I checked the test suite there were still some failing tests. I've listed them here just in case they are relevant.Initially failing tests
Looking into the reason now.