A unifier fix for #1616 #1985
A unifier fix for #1616 #1985
Conversation
| * | ||
| * Example: | ||
| * If we have (x,y |- ?u : ty)[(x:a) <- x, (y:int) <- 42], we will make | ||
| * ?u' with x in its binders, abstracted over y: |
There was a problem hiding this comment.
This comment is great. But I found one aspect of it slightly misleading. It suggests that you have special treatment for variables that are substituted to themselves, choosing not to abstract over them. However, such identity substitutions are rare. It's more that you simply check if a variable is invariant under the substitution, and if it is then it's not abstracted.
There was a problem hiding this comment.
Good point. I can make that clearer.
| gamma |> List.partition (function | ||
| | Binding_var x -> not_affected_by s x | ||
| | _ -> true) | ||
| in |
There was a problem hiding this comment.
I don't think it's safe to split gamma this way.
The gamma is telescope of binders and splitting binders to either side could make both returned lists ill-formed. E.g., consider
Gamma = x:tx, y: ty x, z:tz y
with only y affected by the substitution.
This seems to be a problem in the original code itself.
How about instead taking the least suffix of gamma that mentions all the affected variables.
There was a problem hiding this comment.
Good point, yes. The only reason we do not simply take all binders is for performance, right? (Checking so I can write a proper comment.)
| let t1, wl = ensure_no_uvar_subst t1 wl in | ||
| let t2, wl = ensure_no_uvar_subst t2 wl in | ||
| let f1 = destruct_flex_t' t1 in | ||
| let f2 = destruct_flex_t' t2 in |
There was a problem hiding this comment.
Why not retain the original calls, since those are now safely calling ensure_no_uvar_subst?
There was a problem hiding this comment.
It's required that we call ensure_no_uvar_subst on both sides before we destruct, since we may be dealing with the same ctx_uvar on each side. If we don't, the uvar returned by the first call to destruct_flex_t may be solved during the second call.
If the uvars carry the same substitution (like in the original issue) then there is no problem since the ensure_no_uvar_subst will now be a no-op, but if the substs are different we need to do it like this.
(I did not actually test that it's needed though, since I'm not sure how to even construct such an example, but I'm pretty sure it would explode again.)
There was a problem hiding this comment.
Ah, that's subtle. I didn't fully appreciate that from the comment. Maybe some kind of bold warning there with some version of your comment above copied (rather than just linked).
|
I've updated the PR with your suggestions. I wanted to try simply hoisting all of the uvar's binders and compare performance against this, but turns out that doesn't really work, I believe because we run into #1486. |
|
Many thanks Guido! This looks good. Please merge once you have an everest green. |
|
Got an everest green here, merging. |
Comments in the code and in #1616 (comment)