Correct when fixpoint-fixed type variables can be reunified

With fixpoint-fixing, we don't want to re-unify type variables that were
just fixed, because doing so may change their shapes in ways that we
explicitly just set them up not to be changed (as fixpoint-fixing
clobbers type variable contents).

However, this restriction need only apply when we re-unify two type
variables that were both involved in the same fixpoint-fixing cycle. If
we have a type variable T that was involved in fixpoint-fixing, and we
unify it with U that wasn't, we know that the $U \notin \bar{T}$, where
$\bar{T}$ is the recursive closure of T. In these cases, we do want to
permit the usual in-band unification of $T \sim U$.
This commit is contained in:
Ayaz Hafiz 2022-11-21 15:57:36 -06:00
parent f32e329798
commit e1afd964c7
No known key found for this signature in database
GPG key ID: 0E2A37416A25EF58
3 changed files with 80 additions and 2 deletions

View file

@ -2814,8 +2814,13 @@ fn unify_shared_tags_merge_new<M: MetaCollector>(
new_ext_var: Variable,
recursion_var: Rec,
) -> Outcome<M> {
let was_fixed = env.was_fixed(ctx.first) || env.was_fixed(ctx.second);
if was_fixed {
if env.was_fixed(ctx.first) && env.was_fixed(ctx.second) {
// Both of the tags we're looking at were just involved in fixpoint-fixing, so their types
// should be aligned. As such, do not attempt to unify them and update the recursion
// pointer again.
debug_assert!(env
.subs
.equivalent_without_compacting(ctx.first, ctx.second));
return Default::default();
}