You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Ok, so there's a couple things going on here, and I'll try to explain it succinctly since I'm traveling today (so on mobile at least for the minute).
So first, it's maybe not obvious from the PR (and maybe not even wrong), but something I found when looking through CHALK_DEBUG output. But in apply_answer_subst, we can't properly check if the delayed subgoals are equal to the table goal, because the delayed subgoals get unique inference variables. (Perhaps this would be easier/quicker to check using the variant3 test and adding dbg statements there.)
Second, I would REALLY prefer to have these be checked before they are added to the answer. But, because of 1, we have to wait until they are both canonicalized, which happens in pursue_answer. At that point it is too late because that doesn't know about the subgoal. That was mostly the point of this FIXME: we can be smarter here I think, but it requires a bit of refactoring.
Third, there are essentially two places that do this check. First is in apply_answer_subst and second is here. They aren't the same: removing this causes the variant3 test to fail. Removing the other causes...many of the conductive tests to fail (and a never-ending test for one that I don't remember off the top of my head). I'm not convinced that there couldn't be just one check in the right place.
So, overall. I'm a bit skeptical. Between both checks, everything works. But as I said, I don't know if it's perfectly correct and I definitely think there's room for improvement. Whether that needs to be done in this PR or can be done separately idk.
Nonetheless, I should have some time soon to, at the very least, cleanup this FIXME and a couple other things. (Like the extra apply_binders function that was added but isn't used anymore). If we decide to land the PR as is, I'll file a followup issue with more detailed info.
In #272, @jackh726 commented:
Ok, so there's a couple things going on here, and I'll try to explain it succinctly since I'm traveling today (so on mobile at least for the minute).
So first, it's maybe not obvious from the PR (and maybe not even wrong), but something I found when looking through
CHALK_DEBUG
output. But inapply_answer_subst
, we can't properly check if the delayed subgoals are equal to the table goal, because the delayed subgoals get unique inference variables. (Perhaps this would be easier/quicker to check using the variant3 test and adding dbg statements there.)Second, I would REALLY prefer to have these be checked before they are added to the answer. But, because of 1, we have to wait until they are both canonicalized, which happens in pursue_answer. At that point it is too late because that doesn't know about the subgoal. That was mostly the point of this FIXME: we can be smarter here I think, but it requires a bit of refactoring.
Third, there are essentially two places that do this check. First is in
apply_answer_subst
and second is here. They aren't the same: removing this causes the variant3 test to fail. Removing the other causes...many of the conductive tests to fail (and a never-ending test for one that I don't remember off the top of my head). I'm not convinced that there couldn't be just one check in the right place.So, overall. I'm a bit skeptical. Between both checks, everything works. But as I said, I don't know if it's perfectly correct and I definitely think there's room for improvement. Whether that needs to be done in this PR or can be done separately idk.
Nonetheless, I should have some time soon to, at the very least, cleanup this FIXME and a couple other things. (Like the extra apply_binders function that was added but isn't used anymore). If we decide to land the PR as is, I'll file a followup issue with more detailed info.
Originally posted by @jackh726 in #272
This issue has been assigned to @zaharidichev via this comment.
The text was updated successfully, but these errors were encountered: