fix recursion bug

previously, `Cons 1 (Cons {} Nil)` would get inferred as ConsList Int, because only the outer layer of a tag union was checked with the recursive tag union. Now this is done continually.
This commit is contained in:
Folkert 2020-06-29 00:16:21 +02:00
parent bd086e5c9b
commit 3fc2323891
5 changed files with 273 additions and 86 deletions

View file

@ -128,8 +128,12 @@ pub fn unify_pool(subs: &mut Subs, pool: &mut Pool, var1: Variable, var2: Variab
}
fn unify_context(subs: &mut Subs, pool: &mut Pool, ctx: Context) -> Outcome {
let print_debug_messages = false;
if print_debug_messages {
if false {
// if true, print the types that are unified.
//
// NOTE: names are generated here (when creating an error type) and that modifies names
// generated by pretty_print.rs. So many test will fail with changes in variable names when
// this block runs.
let (type1, _problems1) = subs.var_to_error_type(ctx.first);
let (type2, _problems2) = subs.var_to_error_type(ctx.second);
println!("\n --------------- \n");
@ -530,7 +534,29 @@ fn unify_shared_tags(
let expected_len = expected_vars.len();
for (actual, expected) in actual_vars.into_iter().zip(expected_vars.into_iter()) {
let problems = unify_pool(subs, pool, actual, expected);
// NOTE the arguments of a tag can be recursive. For instance in the expression
//
// Cons 1 (Cons "foo" Nil)
//
// We need to not just check the outer layer (inferring ConsList Int)
// but also the inner layer (finding a type error, as desired)
//
// This correction introduces the same issue as in https://github.com/elm/compiler/issues/1964
// Polymorphic recursion is now a type error.
let problems = if let Some(rvar) = recursion_var {
if expected == rvar {
unify_pool(subs, pool, actual, ctx.second)
} else {
// replace the rvar with ctx.second in expected
subs.explicit_substitute(rvar, ctx.second, expected);
unify_pool(subs, pool, actual, expected)
}
} else {
// we always unify NonRecursive with Recursive, so this should never happen
debug_assert!(Some(actual) != recursion_var);
unify_pool(subs, pool, actual, expected)
};
if problems.is_empty() {
matching_vars.push(actual);
@ -612,18 +638,24 @@ fn unify_flat_type(
unify_tag_union(subs, pool, ctx, union1, union2, (None, None))
}
(RecursiveTagUnion(_, _, _), TagUnion(_, _)) => {
unreachable!("unify of recursive with non-recursive tag union should not occur");
}
(TagUnion(tags1, ext1), RecursiveTagUnion(recursion_var, tags2, ext2)) => {
let union1 = gather_tags(subs, tags1.clone(), *ext1);
let union2 = gather_tags(subs, tags2.clone(), *ext2);
unify_tag_union(
let result = unify_tag_union(
subs,
pool,
ctx,
union1,
union2,
(None, Some(*recursion_var)),
)
);
result
}
(RecursiveTagUnion(rec1, tags1, ext1), RecursiveTagUnion(rec2, tags2, ext2)) => {