language-servers/roc
1
0
Fork 0
mirror of https://github.com/roc-lang/roc.git synced 2025-07-24 15:03:46 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions 6

Simplify unification with uninhabited tags to happen anytime tags are uninhabited

Browse source 
I believe this is safe! No need to gate it behind a mode.
This commit is contained in:
Ayaz Hafiz 2022-09-20 14:13:55 -05:00
parent 16e8a07e27
commit b0598ef817
No known key found for this signature in database
GPG key ID: 0E2A37416A25EF58
2 changed files with 34 additions and 39 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -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;

64
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,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<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;