Merge pull request #3679 from rtfeldman/i3669

Choose recursion var when merging arbitrary variables, when possible
This commit is contained in:
Folkert de Vries 2022-08-02 22:09:50 +02:00 committed by GitHub
commit a00cb58660
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
4 changed files with 133 additions and 54 deletions

View file

@ -0,0 +1,26 @@
procedure Bool.7 (#Attr.2, #Attr.3):
let Bool.9 : Int1 = lowlevel Eq #Attr.2 #Attr.3;
ret Bool.9;
procedure Test.2 (Test.19):
joinpoint Test.13 Test.7:
let Test.16 : U8 = 1i64;
let Test.17 : U8 = GetTagId Test.7;
let Test.18 : Int1 = lowlevel Eq Test.16 Test.17;
if Test.18 then
let Test.14 : {} = Struct {};
ret Test.14;
else
let Test.5 : [<rnu><null>, C *self] = UnionAtIndex (Id 0) (Index 0) Test.7;
jump Test.13 Test.5;
in
jump Test.13 Test.19;
procedure Test.0 ():
let Test.12 : [<rnu><null>, C *self] = TagId(1) ;
let Test.10 : {} = CallByName Test.2 Test.12;
dec Test.12;
let Test.11 : {} = Struct {};
let Test.8 : Int1 = CallByName Bool.7 Test.10 Test.11;
let Test.9 : Str = "";
ret Test.9;

View file

@ -1895,3 +1895,24 @@ fn issue_3560_nested_tag_constructor_is_newtype() {
"# "#
) )
} }
#[mono_test]
fn issue_3669() {
indoc!(
r#"
Peano a := [
Zero,
Successor (Peano a)
]
unwrap : Peano a -> {}
unwrap = \@Peano p ->
when p is
Zero -> {}
Successor inner -> unwrap inner
when unwrap (@Peano Zero) == {} is
_ -> ""
"#
)
}

View file

@ -2366,10 +2366,6 @@ impl AliasVariables {
let all_variables_len = (subs.variables.len() as u32 - variables_start) as u16; let all_variables_len = (subs.variables.len() as u32 - variables_start) as u16;
if type_variables_len == 3 {
panic!();
}
Self { Self {
variables_start, variables_start,
type_variables_len, type_variables_len,

View file

@ -680,25 +680,49 @@ fn unify_two_aliases<M: MetaCollector>(
env: &mut Env, env: &mut Env,
pool: &mut Pool, pool: &mut Pool,
ctx: &Context, ctx: &Context,
// _symbol has an underscore because it's unused in --release builds kind: AliasKind,
_symbol: Symbol, symbol: Symbol,
args: AliasVariables, args: AliasVariables,
real_var: Variable, real_var: Variable,
other_args: AliasVariables, other_args: AliasVariables,
other_real_var: Variable, other_real_var: Variable,
other_content: &Content,
) -> Outcome<M> { ) -> Outcome<M> {
if args.len() == other_args.len() { if args.len() == other_args.len() {
let mut outcome = Outcome::default(); let mut outcome = Outcome::default();
let it = args
.all_variables()
.into_iter()
.zip(other_args.all_variables().into_iter());
for (l, r) in it { let args_it = args
.type_variables()
.into_iter()
.zip(other_args.type_variables().into_iter());
let lambda_set_it = args
.lambda_set_variables()
.into_iter()
.zip(other_args.lambda_set_variables().into_iter());
let mut merged_args = Vec::with_capacity(args.type_variables().len());
let mut merged_lambda_set_args = Vec::with_capacity(args.lambda_set_variables().len());
debug_assert_eq!(
merged_args.capacity() + merged_lambda_set_args.capacity(),
args.all_variables_len as _
);
for (l, r) in args_it {
let l_var = env.subs[l]; let l_var = env.subs[l];
let r_var = env.subs[r]; let r_var = env.subs[r];
outcome.union(unify_pool(env, pool, l_var, r_var, ctx.mode)); 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_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() { if outcome.mismatches.is_empty() {
@ -730,12 +754,21 @@ fn unify_two_aliases<M: MetaCollector>(
let _ = real_var_outcome.mismatches.drain(..); let _ = real_var_outcome.mismatches.drain(..);
outcome.union(real_var_outcome); outcome.union(real_var_outcome);
outcome.union(merge(env, ctx, *other_content)); 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);
let merged_content = Content::Alias(symbol, merged_variables, merged_real_var, kind);
outcome.union(merge(env, ctx, merged_content));
} }
outcome outcome
} else { } else {
mismatch!("{:?}", _symbol) mismatch!("{:?}", symbol)
} }
} }
@ -769,12 +802,12 @@ fn unify_alias<M: MetaCollector>(
env, env,
pool, pool,
ctx, ctx,
AliasKind::Structural,
symbol, symbol,
args, args,
real_var, real_var,
*other_args, *other_args,
*other_real_var, *other_real_var,
other_content,
) )
} else { } else {
unify_pool(env, pool, real_var, *other_real_var, ctx.mode) unify_pool(env, pool, real_var, *other_real_var, ctx.mode)
@ -838,12 +871,12 @@ fn unify_opaque<M: MetaCollector>(
env, env,
pool, pool,
ctx, ctx,
AliasKind::Opaque,
symbol, symbol,
args, args,
real_var, real_var,
*other_args, *other_args,
*other_real_var, *other_real_var,
other_content,
) )
} else { } else {
mismatch!("{:?}", symbol) mismatch!("{:?}", symbol)
@ -2208,6 +2241,46 @@ fn maybe_mark_union_recursive(env: &mut Env, union_var: Variable) {
} }
} }
fn choose_merged_var(subs: &Subs, var1: Variable, var2: Variable) -> Variable {
// If one of the variables is a recursion var, keep that one, so that we avoid inlining
// a recursive tag union type content where we should have a recursion var instead.
//
// When might this happen? For example, in the code
//
// Indirect : [Indirect ConsList]
//
// ConsList : [Nil, Cons Indirect]
//
// l : ConsList
// l = Cons (Indirect (Cons (Indirect Nil)))
// # ^^^^^^^^^^^^^^^~~~~~~~~~~~~~~~~~~~~~^ region-a
// # ~~~~~~~~~~~~~~~~~~~~~ region-b
// l
//
// Suppose `ConsList` has the expanded type `[Nil, Cons [Indirect <rec>]] as <rec>`.
// After unifying the tag application annotated "region-b" with the recursion variable `<rec>`,
// we might have that e.g. `actual` is `<rec>` and `expected` is `[Cons (Indirect ...)]`.
//
// Now, we need to be careful to set the type we choose to represent the merged type
// here to be `<rec>`, not the tag union content of `expected`! Otherwise, we will
// have lost a recursion variable in the recursive tag union.
//
// This would not be incorrect from a type perspective, but causes problems later on for e.g.
// layout generation, which expects recursion variables to be placed correctly. Attempting to detect
// this during layout generation does not work so well because it may be that there *are* recursive
// tag unions that should be inlined, and not pass through recursion variables. So instead, resolve
// these cases here.
//
// See tests labeled "issue_2810" for more examples.
match (
(var1, subs.get_content_unchecked(var1)),
(var2, subs.get_content_unchecked(var2)),
) {
((var, Content::RecursionVar { .. }), _) | (_, (var, Content::RecursionVar { .. })) => var,
_ => var1,
}
}
fn unify_shared_tags_new<M: MetaCollector>( fn unify_shared_tags_new<M: MetaCollector>(
env: &mut Env, env: &mut Env,
pool: &mut Pool, pool: &mut Pool,
@ -2268,44 +2341,7 @@ fn unify_shared_tags_new<M: MetaCollector>(
outcome.union(unify_pool(env, pool, actual, expected, ctx.mode)); outcome.union(unify_pool(env, pool, actual, expected, ctx.mode));
if outcome.mismatches.is_empty() { if outcome.mismatches.is_empty() {
// If one of the variables is a recursion var, keep that one, so that we avoid inlining let merged_var = choose_merged_var(env.subs, actual, expected);
// a recursive tag union type content where we should have a recursion var instead.
//
// When might this happen? For example, in the code
//
// Indirect : [Indirect ConsList]
//
// ConsList : [Nil, Cons Indirect]
//
// l : ConsList
// l = Cons (Indirect (Cons (Indirect Nil)))
// # ^^^^^^^^^^^^^^^~~~~~~~~~~~~~~~~~~~~~^ region-a
// # ~~~~~~~~~~~~~~~~~~~~~ region-b
// l
//
// Suppose `ConsList` has the expanded type `[Nil, Cons [Indirect <rec>]] as <rec>`.
// After unifying the tag application annotated "region-b" with the recursion variable `<rec>`,
// we might have that e.g. `actual` is `<rec>` and `expected` is `[Cons (Indirect ...)]`.
//
// Now, we need to be careful to set the type we choose to represent the merged type
// here to be `<rec>`, not the tag union content of `expected`! Otherwise, we will
// have lost a recursion variable in the recursive tag union.
//
// This would not be incorrect from a type perspective, but causes problems later on for e.g.
// layout generation, which expects recursion variables to be placed correctly. Attempting to detect
// this during layout generation does not work so well because it may be that there *are* recursive
// tag unions that should be inlined, and not pass through recursion variables. So instead, resolve
// these cases here.
//
// See tests labeled "issue_2810" for more examples.
let merged_var = match (
(actual, env.subs.get_content_unchecked(actual)),
(expected, env.subs.get_content_unchecked(expected)),
) {
((var, Content::RecursionVar { .. }), _)
| (_, (var, Content::RecursionVar { .. })) => var,
_ => actual,
};
matching_vars.push(merged_var); matching_vars.push(merged_var);
} }