Unify type alias "real variables"

Turns out that we can't always assume that a successful unification of
type alias type variables means that those aliases had the same real
type from the start. Because type variables may contain unbound type
variables and grow during their unification (for example,
`[InvalidNumStr]a ~ [ListWasEmpty]b` unify to give `[InvalidNumStr,
ListWasEmpty]`), the real type may grow as well.

For this reason, continue to explicitly unify alias real types for now.
We can get away with not having to do so when the type variable
unification causes no changes to the unification tree at all, but we
don't have a great way to detect that right now (maybe snapshots?)

Closes #2583
This commit is contained in:
Ayaz Hafiz 2022-04-05 11:21:52 -04:00
parent 19c02aa087
commit 163c6b39d6
No known key found for this signature in database
GPG key ID: 0E2A37416A25EF58
6 changed files with 86 additions and 8 deletions

View file

@ -5622,4 +5622,16 @@ mod solve_expr {
r#"Outer"#,
)
}
#[test]
fn issue_2583_specialize_errors_behind_unified_branches() {
infer_eq_without_problem(
indoc!(
r#"
if True then List.first [] else Str.toI64 ""
"#
),
"Result I64 [ InvalidNumStr, ListWasEmpty ]*",
)
}
}

View file

@ -256,3 +256,15 @@ fn roc_result_err() {
RocResult<i64, RocStr>
);
}
#[test]
#[cfg(any(feature = "gen-llvm"))]
fn issue_2583_specialize_errors_behind_unified_branches() {
assert_evals_to!(
r#"
if True then List.first [15] else Str.toI64 ""
"#,
RocResult::ok(15i64),
RocResult<i64, bool>
)
}

View file

@ -0,0 +1,43 @@
procedure : `List.first` [C Int1, C I64]
procedure = `List.first` (`#Attr.#arg1`):
let `#UserApp.19` : U64 = 0i64;
let `#UserApp.20` : U64 = lowlevel ListLen `#Attr.#arg1`;
let `#UserApp.15` : Int1 = lowlevel NotEq `#UserApp.19` `#UserApp.20`;
if `#UserApp.15` then <no branch info>
let `#UserApp.18` : U64 = 0i64;
let `#UserApp.17` : I64 = lowlevel ListGetUnsafe `#Attr.#arg1` `#UserApp.18`;
let `#UserApp.16` : [C Int1, C I64] = Ok `#UserApp.17`;
ret `#UserApp.16`;
else <no branch info>
let `#UserApp.14` : Int1 = true;
let `#UserApp.13` : [C Int1, C I64] = Err `#UserApp.14`;
ret `#UserApp.13`;
procedure : `Str.toI64` [C Int1, C I64]
procedure = `Str.toI64` (`#Attr.#arg1`):
let `#Attr.#arg2` : {I64, U8} = lowlevel StrToNum `#Attr.#arg1`;
let `#UserApp.8` : U8 = StructAtIndex 1 `#Attr.#arg2`;
let `#UserApp.9` : U8 = 0i64;
let `#UserApp.5` : Int1 = lowlevel NumGt `#UserApp.8` `#UserApp.9`;
if `#UserApp.5` then <no branch info>
let `#UserApp.7` : Int1 = false;
let `#UserApp.6` : [C Int1, C I64] = Err `#UserApp.7`;
ret `#UserApp.6`;
else <no branch info>
let `#UserApp.4` : I64 = StructAtIndex 0 `#Attr.#arg2`;
let `#UserApp.3` : [C Int1, C I64] = Ok `#UserApp.4`;
ret `#UserApp.3`;
procedure : `#UserApp.main` [C Int1, C I64]
procedure = `#UserApp.main` ():
let `#UserApp.10` : Int1 = true;
if `#UserApp.10` then <no branch info>
let `#UserApp.12` : List I64 = Array [];
let `#UserApp.11` : [C Int1, C I64] = CallByName `List.first` `#UserApp.12`;
dec `#UserApp.12`;
ret `#UserApp.11`;
else <no branch info>
let `#UserApp.2` : Str = "";
let `#UserApp.1` : [C Int1, C I64] = CallByName `Str.toI64` `#UserApp.2`;
dec `#UserApp.2`;
ret `#UserApp.1`;

View file

@ -1273,6 +1273,15 @@ fn issue_2725_alias_polymorphic_lambda() {
)
}
#[mono_test]
fn issue_2583_specialize_errors_behind_unified_branches() {
indoc!(
r#"
if True then List.first [] else Str.toI64 ""
"#
)
}
// #[ignore]
// #[mono_test]
// fn static_str_closure() {

View file

@ -1287,7 +1287,7 @@ fn integer_type(
Content::Alias(
Symbol::NUM_INTEGER,
vars,
at_signed64,
at_integer_signed64,
AliasKind::Structural,
)
});
@ -1532,7 +1532,7 @@ fn float_type(
Content::Alias(
Symbol::NUM_FLOATINGPOINT,
vars,
at_binary64,
at_float_binary64,
AliasKind::Structural,
)
});

View file

@ -332,13 +332,15 @@ fn unify_alias(
problems.extend(merge(subs, ctx, *other_content));
}
// THEORY: if two aliases or opaques have the same name and arguments, their
// real_var is the same and we don't need to check it.
// See https://github.com/rtfeldman/roc/pull/1510
// NOTE: we need to do this unification because unification of type variables
// may have made them larger, which then needs to be reflected in the `real_var`.
//
// if problems.is_empty() && either_is_opaque {
// problems.extend(unify_pool(subs, pool, real_var, *other_real_var, ctx.mode));
// }
// We can skip this if we know type variable unification didn't require
// modification of any variables, but we don't have that kind of information
// yet.
if problems.is_empty() {
problems.extend(unify_pool(subs, pool, real_var, *other_real_var, ctx.mode));
}
problems
} else {