-
Notifications
You must be signed in to change notification settings - Fork 182
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
Refactor ProgramClauseData to remove Implies variant #514
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Your example made me realize what the problem probably is. Where we used to construct an Implies
, but now what essentially was a ForAll
, if there are bound vars in the ProgramClauseImplication
, then we have to shift them in.
That fixed it! I had to export the |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm not 100% sure if I think we should change this here or in follow-up PRs, but I do feel like probably the "cast" impls shouldn't be doing shifting.
.intern(interner) | ||
}; | ||
|
||
ProgramClauseData(Binders::empty(interner, implication.shifted_in(interner))) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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`.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Seems like rebase problems with recursive.rs
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM. I'll merge when CI is working again.
Just saw, guess CI is working again.
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.