Be sure to unify recursion var structure if it hasn't been seen

This commit is contained in:
Ayaz Hafiz 2023-03-27 09:27:11 -05:00
parent d2b9a1a33c
commit e06eac9769
No known key found for this signature in database
GPG key ID: 0E2A37416A25EF58

View file

@ -3778,30 +3778,38 @@ fn unify_recursion<M: MetaCollector>(
structure: Variable,
other: &Content,
) -> Outcome<M> {
if !matches!(other, RecursionVar { .. }) {
if env.seen_recursion_pair(ctx.first, ctx.second) {
return Default::default();
}
env.add_recursion_pair(ctx.first, ctx.second);
if env.seen_recursion_pair(ctx.first, ctx.second) {
return Default::default();
}
env.add_recursion_pair(ctx.first, ctx.second);
let outcome = match other {
RecursionVar {
opt_name: other_opt_name,
structure: _other_structure,
structure: other_structure,
} => {
// NOTE: structure and other_structure may not be unified yet, but will be
// we should not do that here, it would create an infinite loop!
// We haven't seen these two recursion vars yet, so go and unify their structures.
// We need to do this before we merge the two recursion vars, since the unification of
// the structures may be material.
let mut outcome = unify_pool(env, pool, structure, *other_structure, ctx.mode);
if !outcome.mismatches.is_empty() {
return outcome;
}
let name = (*opt_name).or(*other_opt_name);
merge(
let merge_outcome = merge(
env,
ctx,
RecursionVar {
opt_name: name,
structure,
},
)
);
outcome.union(merge_outcome);
outcome
}
Structure(_) => {
@ -3863,9 +3871,7 @@ fn unify_recursion<M: MetaCollector>(
Error => merge(env, ctx, Error),
};
if !matches!(other, RecursionVar { .. }) {
env.remove_recursion_pair(ctx.first, ctx.second);
}
env.remove_recursion_pair(ctx.first, ctx.second);
outcome
}