language-servers/roc
1
0
Fork 0
mirror of https://github.com/roc-lang/roc.git synced 2025-08-03 11:52:19 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions 6

Merge pull request #4082 from roc-lang/update-cli-platform-unreachables

Browse source 
Support unification with uninhabited tag variants in more places
This commit is contained in:
Folkert de Vries 2022-09-21 12:18:38 +02:00 • committed by GitHub
commit cc202a4cf9
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
4 changed files with 81 additions and 64 deletions
Download patch file Download diff file Expand all files Collapse all files

12
crates/compiler/solve/src/solve.rs
View file

@ -1356,16 +1356,8 @@ fn solve(
);
let snapshot = subs.snapshot();
let unify_cond_and_patterns_outcome = {
// When unifying the cond type with what the branches expect, allow 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)
};
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 {

32
crates/compiler/solve/tests/solve_expr.rs
View file

@ -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",
);
}
}

86
crates/compiler/unify/src/unify.rs
View file

@ -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,34 @@ 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`.
/// 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)]
@ -2131,7 +2119,7 @@ fn unify_tag_unions<M: MetaCollector>(
initial_ext2: Variable,
recursion_var: Rec,
) -> Outcome<M> {
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;
@ -2197,9 +2185,9 @@ fn unify_tag_unions<M: MetaCollector>(
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;
@ -2230,15 +2218,29 @@ fn unify_tag_unions<M: MetaCollector>(
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;
@ -2252,7 +2254,7 @@ fn unify_tag_unions<M: MetaCollector>(
ctx,
shared_tags,
OtherTags2::Empty,
sub_record,
extra_tags_in_1,
recursion_var,
);
total_outcome.union(shared_tags_outcome);

15
examples/interactive/cli-platform/Program.roc
View file

@ -59,10 +59,7 @@ noArgs : Task ExitCode [] * -> Program
noArgs = \task ->
effect =
InternalTask.toEffect 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
|> Effect.map \Ok (@ExitCode u8) -> u8
InternalProgram.fromEffect effect
@ -80,10 +77,7 @@ withArgs = \toTask ->
effect = Effect.after Effect.args \args ->
toTask args
|> InternalTask.toEffect
|> 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
|> Effect.map \Ok (@ExitCode u8) -> u8
InternalProgram.fromEffect effect
@ -105,10 +99,7 @@ withEnv = \toTask ->
toTask args dict
|> InternalTask.toEffect
|> 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
|> Effect.map \Ok (@ExitCode u8) -> u8
InternalProgram.fromEffect effect