Don't include uninhabited constructors in exhaustiveness checking

This commit is contained in:
Ayaz Hafiz 2022-09-16 15:36:54 -05:00
parent 52f0dfbaf4
commit 1d7aef8c96
No known key found for this signature in database
GPG Key ID: 0E2A37416A25EF58
2 changed files with 83 additions and 1 deletions

View File

@ -6,8 +6,11 @@ use roc_exhaustive::{
is_useful, Ctor, CtorName, Error, Guard, Literal, Pattern, RenderAs, TagId, Union,
};
use roc_module::ident::{TagIdIntType, TagName};
use roc_module::symbol::ModuleId;
use roc_region::all::{Loc, Region};
use roc_types::subs::{Content, FlatType, RedundantMark, Subs, SubsFmtContent, Variable};
use roc_types::subs::{
Content, FlatType, GetSubsSlice, RedundantMark, Subs, SubsFmtContent, Variable,
};
use roc_types::types::AliasKind;
pub use roc_exhaustive::Context as ExhaustiveContext;
@ -354,6 +357,64 @@ fn to_nonredundant_rows(subs: &Subs, rows: SketchedRows) -> NonRedundantSummary
}
}
/// Returns true iff the given type is inhabited by at least one value.
fn is_inhabited(subs: &Subs, var: Variable) -> bool {
let mut stack = vec![var];
while let Some(var) = stack.pop() {
match subs.get_content_without_compacting(var) {
Content::FlexVar(_)
| Content::RigidVar(_)
| Content::FlexAbleVar(_, _)
| Content::RigidAbleVar(_, _)
// We don't need to look into recursion vars here, because if they show up in this
// position, they *must* belong to an inhabited type. That's because
// - if the recursion var was inferred from a value, then we know there is a value of
// the given type.
// - if the recursion var comes from an explicit annotation, then it must be an a tag
// union of the form `Rec : [ R1 Rec, R2 Rec, ..., Rn Rec ]`. However, such annotations
// are determined as illegal and reported during canonicalization, because you
// cannot have a tag union without a non-recursive variant.
| Content::RecursionVar { .. } => {}
Content::LambdaSet(_) => {}
Content::Structure(structure) => match structure {
FlatType::Apply(_, args) => stack.extend(subs.get_subs_slice(*args)),
FlatType::Func(args, _, ret) => {
stack.extend(subs.get_subs_slice(*args));
stack.push(*ret);
}
FlatType::Record(fields, ext) => {
if let Ok(iter) = fields.unsorted_iterator(subs, *ext) {
let field_vars = iter.map(|(_, field)| *field.as_inner());
stack.extend(field_vars)
}
}
FlatType::TagUnion(tags, ext) | FlatType::RecursiveTagUnion(_, tags, ext) => {
let mut has_no_tags = true;
for (_tag, vars) in tags.unsorted_iterator(subs, *ext) {
has_no_tags = false;
stack.extend(vars);
}
if has_no_tags {
return false;
}
}
FlatType::FunctionOrTagUnion(_, _, _) => {}
FlatType::Erroneous(_) => {}
FlatType::EmptyRecord => {}
FlatType::EmptyTagUnion => {
return false;
}
},
Content::Alias(name, _, var, _) if name.module_id() == ModuleId::NUM => {},
Content::Alias(_, _, var, _) => stack.push(*var),
Content::RangedNumber(_) => {}
Content::Error => {}
}
}
true
}
fn convert_tag(subs: &Subs, whole_var: Variable, this_tag: &TagName) -> (Union, TagId) {
let content = subs.get_content_without_compacting(whole_var);
@ -385,6 +446,13 @@ fn convert_tag(subs: &Subs, whole_var: Variable, this_tag: &TagName) -> (Union,
let alternatives_iter = sorted_tags.into_iter().chain(opt_openness_tag.into_iter());
for (index, (tag, args)) in alternatives_iter.enumerate() {
let is_inhabited = args.iter().all(|v| is_inhabited(subs, *v));
if !is_inhabited {
// This constructor is not material; we don't need to match over it!
continue;
}
let tag_id = TagId(index as TagIdIntType);
if this_tag == &tag {
my_tag_id = tag_id;

View File

@ -10534,4 +10534,18 @@ All branches in an `if` must have the same type!
Maybe you wanted to use a `Result`?
"###
);
test_report!(
uninhabited_type_is_trivially_exhaustive,
indoc!(
r#"
x : Result {} []
when x is
Ok {} -> ""
"#
),
@r###"
"###
);
}