fix triple (or more) mutualy recursive type aliases

This commit is contained in:
Folkert 2020-06-30 14:25:47 +02:00
parent 5483ec819f
commit c589be43c6
3 changed files with 47 additions and 9 deletions

View File

@ -1929,8 +1929,9 @@ fn aliases_to_attr_type(var_store: &mut VarStore, aliases: &mut SendMap<Symbol,
_ => unreachable!("`annotation_to_attr_type` always gives back an Attr"),
}
// TODO can we "just" fix this in alias instantiation?
// e.g. does this work for a triple-mutually-recursive alias?
// Check that if the alias is a recursive tag union, all structures containing the
// recursion variable get the same uniqueness as the recursion variable (and thus as the
// recursive tag union itself)
if let Some(b) = &alias.uniqueness {
fix_mutual_recursive_alias(&mut alias.typ, b);
}
@ -2358,10 +2359,12 @@ fn fix_mutual_recursive_alias_help_help(rec_var: Variable, attribute: &Type, int
}
RecursiveTagUnion(_, tags, ext) | TagUnion(tags, ext) => {
fix_mutual_recursive_alias_help(rec_var, attribute, ext);
tags.iter_mut()
.map(|v| v.1.iter_mut())
.flatten()
.for_each(|arg| fix_mutual_recursive_alias_help(rec_var, attribute, arg));
for (_tag, args) in tags.iter_mut() {
for arg in args.iter_mut() {
fix_mutual_recursive_alias_help(rec_var, attribute, arg);
}
}
}
Record(fields, ext) => {
@ -2371,7 +2374,8 @@ fn fix_mutual_recursive_alias_help_help(rec_var: Variable, attribute: &Type, int
.for_each(|arg| fix_mutual_recursive_alias_help(rec_var, attribute, arg));
}
Alias(_, _, actual_type) => {
fix_mutual_recursive_alias_help(rec_var, attribute, actual_type);
// call help_help, because actual_type is not wrapped in ATTR
fix_mutual_recursive_alias_help_help(rec_var, attribute, actual_type);
}
Apply(_, args) => {
args.iter_mut()

View File

@ -2009,6 +2009,40 @@ mod test_uniq_solve {
);
}
#[test]
fn typecheck_triple_mutually_recursive_tag_union() {
infer_eq(
indoc!(
r#"
ListA a b : [ Cons a (ListB b a), Nil ]
ListB a b : [ Cons a (ListC b a), Nil ]
ListC a b : [ Cons a (ListA b a), Nil ]
ConsList q : [ Cons q (ConsList q), Nil ]
toAs : (q -> p), ListA p q -> ConsList p
toAs =
\f, lista ->
when lista is
Nil -> Nil
Cons a listb ->
when listb is
Nil -> Nil
Cons b listc ->
when listc is
Nil ->
Nil
Cons c newListA ->
Cons a (Cons (f b) (Cons c (toAs f newListA)))
toAs
"#
),
"Attr Shared (Attr Shared (Attr a q -> Attr b p), Attr (* | a | b) (ListA (Attr b p) (Attr a q)) -> Attr * (ConsList (Attr b p)))"
);
}
#[test]
fn infer_mutually_recursive_tag_union() {
infer_eq(

View File

@ -573,11 +573,11 @@ fn unify_shared_tags(
// with uniqueness inference). Thus we must expand the recursive tag union to
// unify if with the non-recursive one. Thus:
// replace the rvar with ctx.second in expected
// replace the rvar with ctx.second (the whole recursive tag union) in expected
subs.explicit_substitute(rvar, ctx.second, expected);
// but, by the `is_structure` condition above, only if we're unifying with a structure!
// when `actual` is just a flex/rigid variable, the substitution will expand a
// when `actual` is just a flex/rigid variable, the substitution would expand a
// recursive tag union infinitely!
unify_pool(subs, pool, actual, expected)