From b0598ef81769d30d45c01deaed4017e4c4f70b08 Mon Sep 17 00:00:00 2001 From: Ayaz Hafiz Date: Tue, 20 Sep 2022 14:13:55 -0500 Subject: [PATCH 1/5] Simplify unification with uninhabited tags to happen anytime tags are uninhabited I believe this is safe! No need to gate it behind a mode. --- crates/compiler/solve/src/solve.rs | 9 +++-- crates/compiler/unify/src/unify.rs | 64 +++++++++++++----------------- 2 files changed, 34 insertions(+), 39 deletions(-) diff --git a/crates/compiler/solve/src/solve.rs b/crates/compiler/solve/src/solve.rs index 0c1744fc3d..cfaf22dabe 100644 --- a/crates/compiler/solve/src/solve.rs +++ b/crates/compiler/solve/src/solve.rs @@ -1357,14 +1357,17 @@ fn solve( let snapshot = subs.snapshot(); let unify_cond_and_patterns_outcome = { - // When unifying the cond type with what the branches expect, allow the + // When unifying the cond type with what the branches expect, we'll want the // 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! - let mode = Mode::EQ_WITH_EXTENSION_BY_UNINHABITED_TYPES; - unify(&mut UEnv::new(subs), branches_var, real_var, mode) + // + // 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; diff --git a/crates/compiler/unify/src/unify.rs b/crates/compiler/unify/src/unify.rs index b230d4c1d5..de0f652222 100644 --- a/crates/compiler/unify/src/unify.rs +++ b/crates/compiler/unify/src/unify.rs @@ -104,25 +104,6 @@ bitflags! { /// specialization algorithm is running. This has implications for the unification of /// unspecialized lambda sets; see [`unify_unspecialized_lambdas`]. const LAMBDA_SET_SPECIALIZATION = Mode::EQ.bits | (1 << 2); - /// Like [`Mode::EQ`], but permits extension of tag union types by other tag unions that - /// are uninhabited. This is relevant for the unification strategy of branch and condition - /// types, where we would like - /// - /// x : Result Str [] - /// when x is - /// Ok x -> x - /// - /// to typecheck, because [Ok Str][] = [Ok Str, Result []][] (up to isomorphism). - /// - /// Traditionally, such types do not unify because the right-hand side is seen to have a - /// `Result` constructor, but for branches, that constructor is not material. - /// - /// Note that such a unification is sound, precisely because `Result` is uninhabited! - /// - /// NOTE: when run in this mode, it is expected that - /// - the BRANCH TYPE is passed on the LEFT - /// - the CONDITION TYPE is passed on the RIGHT - const EQ_WITH_EXTENSION_BY_UNINHABITED_TYPES = Mode::EQ.bits | (1 << 3); } } @@ -142,11 +123,6 @@ impl Mode { self.contains(Mode::LAMBDA_SET_SPECIALIZATION) } - fn permit_extension_by_uninhabited_types(&self) -> bool { - debug_assert!(!self.contains(Mode::EQ | Mode::PRESENT)); - self.contains(Mode::EQ_WITH_EXTENSION_BY_UNINHABITED_TYPES) - } - fn as_eq(self) -> Self { (self - Mode::PRESENT) | Mode::EQ } @@ -2102,22 +2078,38 @@ enum Rec { } /// Checks if an extension type `ext1` should be permitted to grow by the `candidate_type`, if it -/// uninhabited. Only relevant for [Mode::EQ_WITH_EXTENSION_BY_UNINHABITED_TYPES]. +/// uninhabited. /// -/// Per the expect invariant of the mode, the tag union extension to grow should be `ext1`, and the -/// candidate uninhabited type should be `candidate_type`. +/// This is relevant for the unification strategy of branch and condition +/// types, where we would like +/// +/// x : Result Str [] +/// when x is +/// Ok x -> x +/// +/// to typecheck, because [Ok Str][] = [Ok Str, Result []][] (up to isomorphism). +/// +/// Traditionally, such types do not unify because the right-hand side is seen to have a +/// `Result` constructor, but for branches, that constructor is not material. +/// +/// Note that such a unification is sound, precisely because `Result` is uninhabited! +/// +/// NB: the tag union extension to grow should be `ext1`, and the candidate +/// 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 fn should_extend_ext_with_uninhabited_type( subs: &Subs, - mode: Mode, ext1: Variable, candidate_type: Variable, ) -> bool { - mode.permit_extension_by_uninhabited_types() - && matches!( - subs.get_content_without_compacting(ext1), - Content::Structure(FlatType::EmptyTagUnion) - ) - && !subs.is_inhabited(candidate_type) + matches!( + subs.get_content_without_compacting(ext1), + Content::Structure(FlatType::EmptyTagUnion) + ) && !subs.is_inhabited(candidate_type) } #[allow(clippy::too_many_arguments)] @@ -2197,9 +2189,9 @@ fn unify_tag_unions( fresh(env, pool, ctx, Structure(flat_type)) }; - // SPECIAL-CASE: if we are permitted to grow empty extensions with uninhabited types, + // SPECIAL-CASE: if we can grow empty extensions with uninhabited types, // patch `ext1` to grow accordingly. - if should_extend_ext_with_uninhabited_type(env.subs, ctx.mode, ext1, extra_tags_in_2) { + if should_extend_ext_with_uninhabited_type(env.subs, ext1, extra_tags_in_2) { let new_ext = fresh(env, pool, ctx, Content::FlexVar(None)); let new_union = Structure(FlatType::TagUnion(tags1, new_ext)); let mut new_desc = ctx.first_desc; From 49ba8b92b44aecf111cdd4cf946728cfd5ac875b Mon Sep 17 00:00:00 2001 From: Ayaz Hafiz Date: Tue, 20 Sep 2022 14:14:31 -0500 Subject: [PATCH 2/5] Remove unreachable branches in Program.roc --- examples/interactive/cli-platform/Program.roc | 3 --- 1 file changed, 3 deletions(-) diff --git a/examples/interactive/cli-platform/Program.roc b/examples/interactive/cli-platform/Program.roc index a126df773c..a71ef24216 100644 --- a/examples/interactive/cli-platform/Program.roc +++ b/examples/interactive/cli-platform/Program.roc @@ -62,7 +62,6 @@ noArgs = \task -> |> Effect.map \result -> when result is Ok (@ExitCode u8) -> u8 - Err _ -> 0 # TODO this is unreachable! Remove it after https://github.com/roc-lang/roc/issues/4054 lands InternalProgram.fromEffect effect @@ -83,7 +82,6 @@ withArgs = \toTask -> |> Effect.map \result -> when result is Ok (@ExitCode u8) -> u8 - Err _ -> 0 # TODO this is unreachable! Remove it after https://github.com/roc-lang/roc/issues/4054 lands InternalProgram.fromEffect effect @@ -108,7 +106,6 @@ withEnv = \toTask -> |> Effect.map \result -> when result is Ok (@ExitCode code) -> code - Err _ -> 0 # TODO this is unreachable! Remove it after https://github.com/roc-lang/roc/issues/4054 lands InternalProgram.fromEffect effect From f96c825aa44b8433042bc2bf8e0c616e94fc9a45 Mon Sep 17 00:00:00 2001 From: Ayaz Hafiz Date: Tue, 20 Sep 2022 14:20:47 -0500 Subject: [PATCH 3/5] Allow uninhabited type extension to happen on either unification side --- crates/compiler/solve/src/solve.rs | 15 ++------------- crates/compiler/unify/src/unify.rs | 30 ++++++++++++++++++++---------- 2 files changed, 22 insertions(+), 23 deletions(-) diff --git a/crates/compiler/solve/src/solve.rs b/crates/compiler/solve/src/solve.rs index cfaf22dabe..a0cad01882 100644 --- a/crates/compiler/solve/src/solve.rs +++ b/crates/compiler/solve/src/solve.rs @@ -1356,19 +1356,8 @@ fn solve( ); let snapshot = subs.snapshot(); - let unify_cond_and_patterns_outcome = { - // When unifying the cond type with what the branches expect, we'll want the - // 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 unify_cond_and_patterns_outcome = + unify(&mut UEnv::new(subs), branches_var, real_var, Mode::EQ); let should_check_exhaustiveness; match unify_cond_and_patterns_outcome { diff --git a/crates/compiler/unify/src/unify.rs b/crates/compiler/unify/src/unify.rs index de0f652222..fa6f87d5bc 100644 --- a/crates/compiler/unify/src/unify.rs +++ b/crates/compiler/unify/src/unify.rs @@ -2096,10 +2096,6 @@ enum Rec { /// /// NB: the tag union extension to grow should be `ext1`, and the candidate /// 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 fn should_extend_ext_with_uninhabited_type( subs: &Subs, @@ -2123,7 +2119,7 @@ fn unify_tag_unions( initial_ext2: Variable, recursion_var: Rec, ) -> Outcome { - let (separate, mut ext1, ext2) = + let (separate, mut ext1, mut ext2) = separate_union_tags(env.subs, tags1, initial_ext1, tags2, initial_ext2); let shared_tags = separate.in_both; @@ -2222,15 +2218,29 @@ fn unify_tag_unions( shared_tags_outcome } } else if separate.only_in_2.is_empty() { - let unique_tags1 = UnionTags::insert_slices_into_subs(env.subs, separate.only_in_1); - let flat_type = FlatType::TagUnion(unique_tags1, ext1); - let sub_record = fresh(env, pool, ctx, Structure(flat_type)); + let extra_tags_in_1 = { + let unique_tags1 = UnionTags::insert_slices_into_subs(env.subs, separate.only_in_1); + let flat_type = FlatType::TagUnion(unique_tags1, ext1); + fresh(env, pool, ctx, Structure(flat_type)) + }; let mut total_outcome = Outcome::default(); // In a presence context, we don't care about ext2 being equal to tags1 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() { return ext_outcome; @@ -2244,7 +2254,7 @@ fn unify_tag_unions( ctx, shared_tags, OtherTags2::Empty, - sub_record, + extra_tags_in_1, recursion_var, ); total_outcome.union(shared_tags_outcome); From 412c73c54c800f9ec94c38dd7b6f9834f33191d1 Mon Sep 17 00:00:00 2001 From: Ayaz Hafiz Date: Tue, 20 Sep 2022 14:22:40 -0500 Subject: [PATCH 4/5] Add test cases for uninhabited variant collapsing with destructure patterns Closes #4080 --- crates/compiler/solve/tests/solve_expr.rs | 32 +++++++++++++++++++++++ 1 file changed, 32 insertions(+) diff --git a/crates/compiler/solve/tests/solve_expr.rs b/crates/compiler/solve/tests/solve_expr.rs index bef37cf3e6..ae6dc7dbcb 100644 --- a/crates/compiler/solve/tests/solve_expr.rs +++ b/crates/compiler/solve/tests/solve_expr.rs @@ -7791,4 +7791,36 @@ mod solve_expr { "Str", ); } + + #[test] + fn match_on_result_with_uninhabited_error_destructuring() { + infer_eq_without_problem( + indoc!( + r#" + x : Result Str [] + x = Ok "abc" + + Ok str = x + + str + "# + ), + "Str", + ); + } + + #[test] + fn match_on_result_with_uninhabited_error_destructuring_in_lambda_syntax() { + infer_eq_without_problem( + indoc!( + r#" + x : Result Str [] -> Str + x = \Ok s -> s + + x + "# + ), + "Result Str [] -> Str", + ); + } } From 0cb48c64047ee98aab723814954fb19fe581caa9 Mon Sep 17 00:00:00 2001 From: Ayaz Hafiz Date: Tue, 20 Sep 2022 14:30:25 -0500 Subject: [PATCH 5/5] Simplify CLI platform arms further --- examples/interactive/cli-platform/Program.roc | 12 +++--------- 1 file changed, 3 insertions(+), 9 deletions(-) diff --git a/examples/interactive/cli-platform/Program.roc b/examples/interactive/cli-platform/Program.roc index a71ef24216..7cefc46f0c 100644 --- a/examples/interactive/cli-platform/Program.roc +++ b/examples/interactive/cli-platform/Program.roc @@ -59,9 +59,7 @@ noArgs : Task ExitCode [] * -> Program noArgs = \task -> effect = InternalTask.toEffect task - |> Effect.map \result -> - when result is - Ok (@ExitCode u8) -> u8 + |> Effect.map \Ok (@ExitCode u8) -> u8 InternalProgram.fromEffect effect @@ -79,9 +77,7 @@ withArgs = \toTask -> effect = Effect.after Effect.args \args -> toTask args |> InternalTask.toEffect - |> Effect.map \result -> - when result is - Ok (@ExitCode u8) -> u8 + |> Effect.map \Ok (@ExitCode u8) -> u8 InternalProgram.fromEffect effect @@ -103,9 +99,7 @@ withEnv = \toTask -> toTask args dict |> InternalTask.toEffect - |> Effect.map \result -> - when result is - Ok (@ExitCode code) -> code + |> Effect.map \Ok (@ExitCode u8) -> u8 InternalProgram.fromEffect effect