Improve alias<->opaque unification logic

This commit is contained in:
Ayaz Hafiz 2022-04-24 12:48:37 -04:00
parent a53ba3498b
commit 8b291854d3
No known key found for this signature in database
GPG key ID: 0E2A37416A25EF58
2 changed files with 148 additions and 57 deletions

View file

@ -5759,13 +5759,13 @@ mod solve_expr {
r#"
app "test" provides [ effectAlways ] to "./platform"
Effect a : [ @Effect ({} -> a) ]
Effect a := {} -> a
effectAlways : a -> Effect a
effectAlways = \x ->
inner = \{} -> x
@Effect inner
$Effect inner
"#
),
r#"a -> Effect a"#,
@ -6211,4 +6211,23 @@ mod solve_expr {
indoc!(r#"Expr -> Expr"#),
)
}
#[test]
fn opaque_and_alias_unify() {
infer_eq_without_problem(
indoc!(
r#"
app "test" provides [ always ] to "./platform"
Effect a := {} -> a
Task a err : Effect (Result a err)
always : a -> Task a *
always = \x -> $Effect (\{} -> Ok x)
"#
),
"a -> Task a *",
);
}
}

View file

@ -358,8 +358,11 @@ fn unify_context(subs: &mut Subs, pool: &mut Pool, ctx: Context) -> Outcome {
Structure(flat_type) => {
unify_structure(subs, pool, &ctx, flat_type, &ctx.second_desc.content)
}
Alias(symbol, args, real_var, kind) => {
unify_alias(subs, pool, &ctx, *symbol, *args, *real_var, *kind)
Alias(symbol, args, real_var, AliasKind::Structural) => {
unify_alias(subs, pool, &ctx, *symbol, *args, *real_var)
}
Alias(symbol, args, real_var, AliasKind::Opaque) => {
unify_opaque(subs, pool, &ctx, *symbol, *args, *real_var)
}
&RangedNumber(typ, range_vars) => unify_ranged_number(subs, pool, &ctx, typ, range_vars),
Error => {
@ -449,40 +452,17 @@ fn check_valid_range(
}
#[inline(always)]
fn unify_alias(
fn unify_two_aliases(
subs: &mut Subs,
pool: &mut Pool,
ctx: &Context,
symbol: Symbol,
args: AliasVariables,
real_var: Variable,
kind: AliasKind,
other_args: AliasVariables,
other_real_var: Variable,
other_content: &Content,
) -> Outcome {
let other_content = &ctx.second_desc.content;
let either_is_opaque =
kind == AliasKind::Opaque || matches!(other_content, Alias(_, _, _, AliasKind::Opaque));
match other_content {
FlexVar(_) => {
// Alias wins
merge(subs, ctx, Alias(symbol, args, real_var, kind))
}
RecursionVar { structure, .. } if !either_is_opaque => {
unify_pool(subs, pool, real_var, *structure, ctx.mode)
}
RigidVar(_) | RigidAbleVar(..) => unify_pool(subs, pool, real_var, ctx.second, ctx.mode),
FlexAbleVar(_, ability) if kind == AliasKind::Opaque && args.is_empty() => {
// Opaque type wins
let mut outcome = merge(subs, ctx, Alias(symbol, args, real_var, kind));
outcome.must_implement_ability.push(MustImplementAbility { typ: symbol, ability: *ability });
outcome
}
Alias(other_symbol, other_args, other_real_var, _)
// Opaques types are only equal if the opaque symbols are equal!
if !either_is_opaque || symbol == *other_symbol =>
{
if symbol == *other_symbol {
if args.len() == other_args.len() {
let mut outcome = Outcome::default();
let it = args
@ -502,13 +482,15 @@ fn unify_alias(
outcome.union(merge(subs, ctx, *other_content));
}
let args_unification_had_changes = !subs.vars_since_snapshot(&args_unification_snapshot).is_empty();
let args_unification_had_changes = !subs
.vars_since_snapshot(&args_unification_snapshot)
.is_empty();
subs.commit_snapshot(args_unification_snapshot);
if !args.is_empty() && args_unification_had_changes && outcome.mismatches.is_empty() {
// We need to unify the real vars because unification of type variables
// may have made them larger, which then needs to be reflected in the `real_var`.
outcome.union(unify_pool(subs, pool, real_var, *other_real_var, ctx.mode));
outcome.union(unify_pool(subs, pool, real_var, other_real_var, ctx.mode));
}
outcome
@ -516,12 +498,51 @@ fn unify_alias(
dbg!(args.len(), other_args.len());
mismatch!("{:?}", symbol)
}
}
// Unifies a structural alias
#[inline(always)]
fn unify_alias(
subs: &mut Subs,
pool: &mut Pool,
ctx: &Context,
symbol: Symbol,
args: AliasVariables,
real_var: Variable,
) -> Outcome {
let other_content = &ctx.second_desc.content;
let kind = AliasKind::Structural;
match other_content {
FlexVar(_) => {
// Alias wins
merge(subs, ctx, Alias(symbol, args, real_var, kind))
}
RecursionVar { structure, .. } => unify_pool(subs, pool, real_var, *structure, ctx.mode),
RigidVar(_) | RigidAbleVar(..) | FlexAbleVar(..) => {
unify_pool(subs, pool, real_var, ctx.second, ctx.mode)
}
Alias(_, _, _, AliasKind::Opaque) => unify_pool(subs, pool, real_var, ctx.second, ctx.mode),
Alias(other_symbol, other_args, other_real_var, AliasKind::Structural) => {
if symbol == *other_symbol {
unify_two_aliases(
subs,
pool,
ctx,
symbol,
args,
real_var,
*other_args,
*other_real_var,
other_content,
)
} else {
unify_pool(subs, pool, real_var, *other_real_var, ctx.mode)
}
}
Structure(_) if !either_is_opaque => unify_pool(subs, pool, real_var, ctx.second, ctx.mode),
RangedNumber(other_real_var, other_range_vars) if !either_is_opaque => {
Structure(_) => unify_pool(subs, pool, real_var, ctx.second, ctx.mode),
RangedNumber(other_real_var, other_range_vars) => {
let outcome = unify_pool(subs, pool, real_var, *other_real_var, ctx.mode);
if outcome.mismatches.is_empty() {
check_valid_range(subs, pool, real_var, *other_range_vars, ctx.mode)
@ -530,9 +551,60 @@ fn unify_alias(
}
}
Error => merge(subs, ctx, Error),
}
}
#[inline(always)]
fn unify_opaque(
subs: &mut Subs,
pool: &mut Pool,
ctx: &Context,
symbol: Symbol,
args: AliasVariables,
real_var: Variable,
) -> Outcome {
let other_content = &ctx.second_desc.content;
let kind = AliasKind::Opaque;
match other_content {
FlexVar(_) => {
// Alias wins
merge(subs, ctx, Alias(symbol, args, real_var, kind))
}
RigidVar(_) | RigidAbleVar(..) => unify_pool(subs, pool, real_var, ctx.second, ctx.mode),
FlexAbleVar(_, ability) if args.is_empty() => {
// Opaque type wins
let mut outcome = merge(subs, ctx, Alias(symbol, args, real_var, kind));
outcome.must_implement_ability.push(MustImplementAbility {
typ: symbol,
ability: *ability,
});
outcome
}
Alias(_, _, other_real_var, AliasKind::Structural) => {
unify_pool(subs, pool, ctx.first, *other_real_var, ctx.mode)
}
Alias(other_symbol, other_args, other_real_var, AliasKind::Opaque) => {
// Opaques types are only equal if the opaque symbols are equal!
if symbol == *other_symbol {
unify_two_aliases(
subs,
pool,
ctx,
symbol,
args,
real_var,
*other_args,
*other_real_var,
other_content,
)
} else {
mismatch!("{:?}", symbol)
}
}
other => {
// The type on the left is an alias, but the one on the right is not!
debug_assert!(either_is_opaque);
// The type on the left is an opaque, but the one on the right is not!
mismatch!("Cannot unify opaque {:?} with {:?}", symbol, other)
}
}