Correct occurs cycle under alias argument but not alias real var

At times we can have alias arguments that are recursive in their
position, but whose recursiveness is not immediately visible in the real
var.

Closes #5330
This commit is contained in:
Ayaz Hafiz 2023-05-02 16:47:09 -05:00
parent 8dc86a81b8
commit 8ca1e6c866
No known key found for this signature in database
GPG key ID: 0E2A37416A25EF58
2 changed files with 86 additions and 58 deletions

View file

@ -863,68 +863,77 @@ fn unify_two_aliases<M: MetaCollector>(
merged_args.push(merged_var);
}
for (l, r) in lambda_set_it {
let l_var = env.subs[l];
let r_var = env.subs[r];
outcome.union(unify_pool(env, pool, l_var, r_var, ctx.mode));
let merged_var = choose_merged_var(env.subs, l_var, r_var);
merged_lambda_set_args.push(merged_var);
if !outcome.mismatches.is_empty() {
return outcome;
}
for (l, r) in infer_ext_in_output_vars_it {
let l_var = env.subs[l];
let r_var = env.subs[r];
outcome.union(unify_pool(env, pool, l_var, r_var, ctx.mode));
// Even if there are no changes to alias arguments, and no new variables were
// introduced, we may still need to unify the "actual types" of the alias or opaque!
//
// The unification is not necessary from a types perspective (and in fact, we may want
// to disable it for `roc check` later on), but it is necessary for the monomorphizer,
// which expects identical types to be reflected in the same variable.
//
// As a concrete example, consider the unification of two opaques
//
// P := [Zero, Succ P]
//
// (@P (Succ n)) ~ (@P (Succ o))
//
// `P` has no arguments, and unification of the surface of `P` introduces nothing new.
// But if we do not unify the types of `n` and `o`, which are recursion variables, they
// will remain disjoint! Currently, the implication of this is that they will be seen
// to have separate recursive memory layouts in the monomorphizer - which is no good
// for our compilation model.
//
// As such, always unify the real vars.
let merged_var = choose_merged_var(env.subs, l_var, r_var);
merged_infer_ext_in_output_vars.push(merged_var);
// Don't report real_var mismatches, because they must always be surfaced higher, from
// the argument types.
let mut real_var_outcome = unify_pool::<M>(env, pool, real_var, other_real_var, ctx.mode);
let _ = real_var_outcome.mismatches.drain(..);
outcome.union(real_var_outcome);
let merged_real_var = choose_merged_var(env.subs, real_var, other_real_var);
// Now, we need to unify the lambda set and IOIOP variables of both aliases.
//
// We wait to do this until after we have unified the real vars, because the real vars
// should contain the lambda set and IOIOP variables of the aliases, so most of these
// should be short-circuits.
{
for (l, r) in lambda_set_it {
let l_var = env.subs[l];
let r_var = env.subs[r];
outcome.union(unify_pool(env, pool, l_var, r_var, ctx.mode));
let merged_var = choose_merged_var(env.subs, l_var, r_var);
merged_lambda_set_args.push(merged_var);
}
for (l, r) in infer_ext_in_output_vars_it {
let l_var = env.subs[l];
let r_var = env.subs[r];
outcome.union(unify_pool(env, pool, l_var, r_var, ctx.mode));
let merged_var = choose_merged_var(env.subs, l_var, r_var);
merged_infer_ext_in_output_vars.push(merged_var);
}
}
if outcome.mismatches.is_empty() {
// Even if there are no changes to alias arguments, and no new variables were
// introduced, we may still need to unify the "actual types" of the alias or opaque!
//
// The unification is not necessary from a types perspective (and in fact, we may want
// to disable it for `roc check` later on), but it is necessary for the monomorphizer,
// which expects identical types to be reflected in the same variable.
//
// As a concrete example, consider the unification of two opaques
//
// P := [Zero, Succ P]
//
// (@P (Succ n)) ~ (@P (Succ o))
//
// `P` has no arguments, and unification of the surface of `P` introduces nothing new.
// But if we do not unify the types of `n` and `o`, which are recursion variables, they
// will remain disjoint! Currently, the implication of this is that they will be seen
// to have separate recursive memory layouts in the monomorphizer - which is no good
// for our compilation model.
//
// As such, always unify the real vars.
// POSSIBLE OPT: choose_merged_var chooses the left when the choice is arbitrary. If
// the merged vars are all left, avoid re-insertion. Is checking for argument slice
// equality faster than re-inserting?
let merged_variables = AliasVariables::insert_into_subs(
env.subs,
merged_args,
merged_lambda_set_args,
merged_infer_ext_in_output_vars,
);
// Don't report real_var mismatches, because they must always be surfaced higher, from
// the argument types.
let mut real_var_outcome =
unify_pool::<M>(env, pool, real_var, other_real_var, ctx.mode);
let _ = real_var_outcome.mismatches.drain(..);
outcome.union(real_var_outcome);
let merged_content = Content::Alias(symbol, merged_variables, merged_real_var, kind);
let merged_real_var = choose_merged_var(env.subs, real_var, other_real_var);
// POSSIBLE OPT: choose_merged_var chooses the left when the choice is arbitrary. If
// the merged vars are all left, avoid re-insertion. Is checking for argument slice
// equality faster than re-inserting?
let merged_variables = AliasVariables::insert_into_subs(
env.subs,
merged_args,
merged_lambda_set_args,
merged_infer_ext_in_output_vars,
);
let merged_content = Content::Alias(symbol, merged_variables, merged_real_var, kind);
outcome.union(merge(env, ctx, merged_content));
}
outcome.union(merge(env, ctx, merged_content));
outcome
} else {