Allow uninhabited type extension to happen on either unification side

This commit is contained in:
Ayaz Hafiz 2022-09-20 14:20:47 -05:00
parent 49ba8b92b4
commit f96c825aa4
No known key found for this signature in database
GPG key ID: 0E2A37416A25EF58
2 changed files with 22 additions and 23 deletions

View file

@ -1356,19 +1356,8 @@ fn solve(
); );
let snapshot = subs.snapshot(); let snapshot = subs.snapshot();
let unify_cond_and_patterns_outcome = { let unify_cond_and_patterns_outcome =
// When unifying the cond type with what the branches expect, we'll want the unify(&mut UEnv::new(subs), branches_var, real_var, Mode::EQ);
// branches to gain constructors that are uninabited; that way, we can permit
// unification of things like
// [Ok Str] ~ [Ok Str, Result []]
// which we want here, because `Result []` need not be matched - it is
// impossible to construct!
//
// The order of variables is important here - to do such a unification, the
// unifier expects the branch variable on the left, and the condition variable
// (containing uninhabited variants to grow by) on the right.
unify(&mut UEnv::new(subs), branches_var, real_var, Mode::EQ)
};
let should_check_exhaustiveness; let should_check_exhaustiveness;
match unify_cond_and_patterns_outcome { match unify_cond_and_patterns_outcome {

View file

@ -2096,10 +2096,6 @@ enum Rec {
/// ///
/// NB: the tag union extension to grow should be `ext1`, and the candidate /// NB: the tag union extension to grow should be `ext1`, and the candidate
/// NB: uninhabited type should be `candidate_type`. /// NB: uninhabited type should be `candidate_type`.
/// NB:
/// NB: as such, it is generally expected that
/// NB: - the BRANCH TYPE is passed on the LEFT
/// NB: - the CONDITION TYPE is passed on the RIGHT
/// of the variables under unification /// of the variables under unification
fn should_extend_ext_with_uninhabited_type( fn should_extend_ext_with_uninhabited_type(
subs: &Subs, subs: &Subs,
@ -2123,7 +2119,7 @@ fn unify_tag_unions<M: MetaCollector>(
initial_ext2: Variable, initial_ext2: Variable,
recursion_var: Rec, recursion_var: Rec,
) -> Outcome<M> { ) -> Outcome<M> {
let (separate, mut ext1, ext2) = let (separate, mut ext1, mut ext2) =
separate_union_tags(env.subs, tags1, initial_ext1, tags2, initial_ext2); separate_union_tags(env.subs, tags1, initial_ext1, tags2, initial_ext2);
let shared_tags = separate.in_both; let shared_tags = separate.in_both;
@ -2222,15 +2218,29 @@ fn unify_tag_unions<M: MetaCollector>(
shared_tags_outcome shared_tags_outcome
} }
} else if separate.only_in_2.is_empty() { } else if separate.only_in_2.is_empty() {
let unique_tags1 = UnionTags::insert_slices_into_subs(env.subs, separate.only_in_1); let extra_tags_in_1 = {
let flat_type = FlatType::TagUnion(unique_tags1, ext1); let unique_tags1 = UnionTags::insert_slices_into_subs(env.subs, separate.only_in_1);
let sub_record = fresh(env, pool, ctx, Structure(flat_type)); let flat_type = FlatType::TagUnion(unique_tags1, ext1);
fresh(env, pool, ctx, Structure(flat_type))
};
let mut total_outcome = Outcome::default(); let mut total_outcome = Outcome::default();
// In a presence context, we don't care about ext2 being equal to tags1 // In a presence context, we don't care about ext2 being equal to tags1
if ctx.mode.is_eq() { if ctx.mode.is_eq() {
let ext_outcome = unify_pool(env, pool, sub_record, ext2, ctx.mode); // SPECIAL-CASE: if we can grow empty extensions with uninhabited types,
// patch `ext2` to grow accordingly.
if should_extend_ext_with_uninhabited_type(env.subs, ext2, extra_tags_in_1) {
let new_ext = fresh(env, pool, ctx, Content::FlexVar(None));
let new_union = Structure(FlatType::TagUnion(tags2, new_ext));
let mut new_desc = ctx.second_desc;
new_desc.content = new_union;
env.subs.set(ctx.second, new_desc);
ext2 = new_ext;
}
let ext_outcome = unify_pool(env, pool, extra_tags_in_1, ext2, ctx.mode);
if !ext_outcome.mismatches.is_empty() { if !ext_outcome.mismatches.is_empty() {
return ext_outcome; return ext_outcome;
@ -2244,7 +2254,7 @@ fn unify_tag_unions<M: MetaCollector>(
ctx, ctx,
shared_tags, shared_tags,
OtherTags2::Empty, OtherTags2::Empty,
sub_record, extra_tags_in_1,
recursion_var, recursion_var,
); );
total_outcome.union(shared_tags_outcome); total_outcome.union(shared_tags_outcome);