Merge pull request #3600 from rtfeldman/i3298

Various improvements to is-open constraints/catch-all branches in patterns
This commit is contained in:
Folkert de Vries 2022-07-23 12:49:35 +02:00 committed by GitHub
commit 860df057dc
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
7 changed files with 182 additions and 113 deletions

View File

@ -2705,7 +2705,7 @@ pub mod test_constrain {
A _ -> Z
"#
),
"[A [M, N]*] -> [X, Y, Z]*",
"[A [M, N]] -> [X, Y, Z]*",
)
}

View File

@ -735,7 +735,8 @@ pub fn constrain_expr(
let mut pattern_vars = Vec::with_capacity(branches.len());
let mut pattern_headers = SendMap::default();
let mut pattern_cons = Vec::with_capacity(branches.len() + 2);
let mut branch_cons = Vec::with_capacity(branches.len());
let mut delayed_is_open_constraints = Vec::with_capacity(2);
let mut body_cons = Vec::with_capacity(branches.len());
for (index, when_branch) in branches.iter().enumerate() {
let expected_pattern = |sub_pattern, sub_region| {
@ -749,19 +750,24 @@ pub fn constrain_expr(
)
};
let (new_pattern_vars, new_pattern_headers, pattern_con, branch_con) =
constrain_when_branch_help(
constraints,
env,
region,
when_branch,
expected_pattern,
branch_expr_reason(
&expected,
HumanIndex::zero_based(index),
when_branch.value.region,
),
);
let ConstrainedBranch {
vars: new_pattern_vars,
headers: new_pattern_headers,
pattern_constraints,
is_open_constrains,
body_constraints,
} = constrain_when_branch_help(
constraints,
env,
region,
when_branch,
expected_pattern,
branch_expr_reason(
&expected,
HumanIndex::zero_based(index),
when_branch.value.region,
),
);
pattern_vars.extend(new_pattern_vars);
@ -779,9 +785,10 @@ pub fn constrain_expr(
}
pattern_headers.extend(new_pattern_headers);
pattern_cons.push(pattern_con);
pattern_cons.push(pattern_constraints);
delayed_is_open_constraints.extend(is_open_constrains);
branch_cons.push(branch_con);
body_cons.push(body_constraints);
}
// Deviation: elm adds another layer of And nesting
@ -793,6 +800,11 @@ pub fn constrain_expr(
// The return type of each branch must equal the return type of
// the entire when-expression.
// Layer on the "is-open" constraints at the very end, after we know what the branch
// types are supposed to look like without open-ness.
let is_open_constr = constraints.and_constraint(delayed_is_open_constraints);
pattern_cons.push(is_open_constr);
// After solving the condition variable with what's expected from the branch patterns,
// check it against the condition expression.
//
@ -826,7 +838,7 @@ pub fn constrain_expr(
// Solve all the pattern constraints together, introducing variables in the pattern as
// need be before solving the bodies.
let pattern_constraints = constraints.and_constraint(pattern_cons);
let body_constraints = constraints.and_constraint(branch_cons);
let body_constraints = constraints.and_constraint(body_cons);
let when_body_con = constraints.let_constraint(
[],
pattern_vars,
@ -1790,6 +1802,14 @@ fn constrain_value_def(
}
}
struct ConstrainedBranch {
vars: Vec<Variable>,
headers: VecMap<Symbol, Loc<Type>>,
pattern_constraints: Constraint,
is_open_constrains: Vec<Constraint>,
body_constraints: Constraint,
}
/// Constrain a when branch, returning (variables in pattern, symbols introduced in pattern, pattern constraint, body constraint).
/// We want to constraint all pattern constraints in a "when" before body constraints.
#[inline(always)]
@ -1800,12 +1820,7 @@ fn constrain_when_branch_help(
when_branch: &WhenBranch,
pattern_expected: impl Fn(HumanIndex, Region) -> PExpected<Type>,
expr_expected: Expected<Type>,
) -> (
Vec<Variable>,
VecMap<Symbol, Loc<Type>>,
Constraint,
Constraint,
) {
) -> ConstrainedBranch {
let ret_constraint = constrain_expr(
constraints,
env,
@ -1869,41 +1884,43 @@ fn constrain_when_branch_help(
}
}
let (pattern_constraints, body_constraints) = if let Some(loc_guard) = &when_branch.guard {
let guard_constraint = constrain_expr(
constraints,
env,
region,
&loc_guard.value,
Expected::ForReason(
Reason::WhenGuard,
Type::Variable(Variable::BOOL),
loc_guard.region,
),
);
let (pattern_constraints, delayed_is_open_constraints, body_constraints) =
if let Some(loc_guard) = &when_branch.guard {
let guard_constraint = constrain_expr(
constraints,
env,
region,
&loc_guard.value,
Expected::ForReason(
Reason::WhenGuard,
Type::Variable(Variable::BOOL),
loc_guard.region,
),
);
// must introduce the headers from the pattern before constraining the guard
state
.constraints
.append(&mut state.delayed_is_open_constraints);
let state_constraints = constraints.and_constraint(state.constraints);
let inner = constraints.let_constraint([], [], [], guard_constraint, ret_constraint);
// must introduce the headers from the pattern before constraining the guard
let delayed_is_open_constraints = state.delayed_is_open_constraints;
let state_constraints = constraints.and_constraint(state.constraints);
let inner = constraints.let_constraint([], [], [], guard_constraint, ret_constraint);
(state_constraints, inner)
} else {
state
.constraints
.append(&mut state.delayed_is_open_constraints);
let state_constraints = constraints.and_constraint(state.constraints);
(state_constraints, ret_constraint)
};
(state_constraints, delayed_is_open_constraints, inner)
} else {
let delayed_is_open_constraints = state.delayed_is_open_constraints;
let state_constraints = constraints.and_constraint(state.constraints);
(
state_constraints,
delayed_is_open_constraints,
ret_constraint,
)
};
(
state.vars,
state.headers,
ConstrainedBranch {
vars: state.vars,
headers: state.headers,
pattern_constraints,
is_open_constrains: delayed_is_open_constraints,
body_constraints,
)
}
}
fn constrain_field(

View File

@ -498,9 +498,6 @@ pub fn constrain_pattern(
state.vars.push(*ext_var);
state.constraints.push(whole_con);
state.constraints.push(tag_con);
state
.constraints
.append(&mut state.delayed_is_open_constraints);
}
UnwrappedOpaque {

View File

@ -1653,25 +1653,35 @@ fn open_tag_union(subs: &mut Subs, var: Variable) {
use {Content::*, FlatType::*};
let desc = subs.get(var);
if let Structure(TagUnion(tags, ext)) = desc.content {
if let Structure(EmptyTagUnion) = subs.get_content_without_compacting(ext) {
let new_ext = subs.fresh_unnamed_flex_var();
subs.set_rank(new_ext, desc.rank);
let new_union = Structure(TagUnion(tags, new_ext));
subs.set_content(var, new_union);
match desc.content {
Structure(TagUnion(tags, ext)) => {
if let Structure(EmptyTagUnion) = subs.get_content_without_compacting(ext) {
let new_ext = subs.fresh_unnamed_flex_var();
subs.set_rank(new_ext, desc.rank);
let new_union = Structure(TagUnion(tags, new_ext));
subs.set_content(var, new_union);
}
// Also open up all nested tag unions.
let all_vars = tags.variables().into_iter();
stack.extend(all_vars.flat_map(|slice| subs[slice]).map(|var| subs[var]));
}
// Also open up all nested tag unions.
let all_vars = tags.variables().into_iter();
stack.extend(all_vars.flat_map(|slice| subs[slice]).map(|var| subs[var]));
Structure(Record(fields, _)) => {
// Open up all nested tag unions.
stack.extend(subs.get_subs_slice(fields.variables()));
}
_ => {
// Everything else is not a structural type that can be opened
// (i.e. cannot be matched in a pattern-match)
}
}
// Today, an "open" constraint doesn't affect any types
// other than tag unions. Recursive tag unions are constructed
// at a later time (during occurs checks after tag unions are
// resolved), so that's not handled here either.
// NB: Handle record types here if we add presence constraints
// to their type inference as well.
}
}

View File

@ -245,7 +245,13 @@ mod solve_expr {
assert_eq!(actual, expected.to_string());
}
fn infer_queries_help(src: &str, expected: impl FnOnce(&str), print_only_under_alias: bool) {
#[derive(Default)]
struct InferOptions {
print_only_under_alias: bool,
allow_errors: bool,
}
fn infer_queries_help(src: &str, expected: impl FnOnce(&str), options: InferOptions) {
let (
LoadedModule {
module_id: home,
@ -269,12 +275,14 @@ mod solve_expr {
let (can_problems, type_problems) =
format_problems(&src, home, &interns, can_problems, type_problems);
assert!(
can_problems.is_empty(),
"Canonicalization problems: {}",
can_problems
);
assert!(type_problems.is_empty(), "Type problems: {}", type_problems);
if !options.allow_errors {
assert!(
can_problems.is_empty(),
"Canonicalization problems: {}",
can_problems
);
assert!(type_problems.is_empty(), "Type problems: {}", type_problems);
}
let queries = parse_queries(&src);
assert!(!queries.is_empty(), "No queries provided!");
@ -295,7 +303,7 @@ mod solve_expr {
&interns,
DebugPrint {
print_lambda_sets: true,
print_only_under_alias,
print_only_under_alias: options.print_only_under_alias,
},
);
subs.rollback_to(snapshot);
@ -325,11 +333,10 @@ mod solve_expr {
}
macro_rules! infer_queries {
($program:expr, @$queries:literal $(,)?) => {
infer_queries_help($program, |golden| insta::assert_snapshot!(golden, @$queries), false)
};
($program:expr, @$queries:literal, print_only_under_alias=true $(,)?) => {
infer_queries_help($program, |golden| insta::assert_snapshot!(golden, @$queries), true)
($program:expr, @$queries:literal $($option:ident: $value:expr)*) => {
infer_queries_help($program, |golden| insta::assert_snapshot!(golden, @$queries), InferOptions {
$($option: $value,)* ..InferOptions::default()
})
};
}
@ -6662,7 +6669,7 @@ mod solve_expr {
A#id(4) : A -[[id(4)]]-> A
idChoice : a -[[] + a:id(2):1]-> a | a has Id
idChoice : A -[[id(4)]]-> A
"#,
"#
)
}
@ -6696,8 +6703,8 @@ mod solve_expr {
A#id(5) : {} -[[id(5)]]-> ({} -[[8(8)]]-> {})
Id#id(3) : {} -[[id(5)]]-> ({} -[[8(8)]]-> {})
alias : {} -[[id(5)]]-> ({} -[[8(8)]]-> {})
"#,
print_only_under_alias = true,
"#
print_only_under_alias: true
)
}
@ -6726,8 +6733,8 @@ mod solve_expr {
@r#"
A#id(5) : {} -[[id(5)]]-> ({} -[[8(8)]]-> {})
it : {} -[[8(8)]]-> {}
"#,
print_only_under_alias = true,
"#
print_only_under_alias: true
)
}
@ -6757,8 +6764,8 @@ mod solve_expr {
@r#"
A#id(5) : {} -[[id(5)]]-> ({} -[[8(8)]]-> {})
A#id(5) : {} -[[id(5)]]-> ({} -[[8(8)]]-> {})
"#,
print_only_under_alias = true,
"#
print_only_under_alias: true
)
}
@ -6895,8 +6902,8 @@ mod solve_expr {
Named name outerList : [Named Str (List a)] as a
name : Str
outerList : List ([Named Str (List a)] as a)
"#,
print_only_under_alias = true
"#
print_only_under_alias: true
)
}
@ -7012,8 +7019,8 @@ mod solve_expr {
#^^^{-1}
"#
),
@r#"fun : {} -[[thunk(9) (({} -[[15(15)]]-> { s1 : Str })) ({ s1 : Str } -[[g(4)]]-> ({} -[[13(13) Str]]-> Str)), thunk(9) (({} -[[14(14)]]-> Str)) (Str -[[f(3)]]-> ({} -[[11(11)]]-> Str))]]-> Str"#,
print_only_under_alias = true,
@r#"fun : {} -[[thunk(9) (({} -[[15(15)]]-> { s1 : Str })) ({ s1 : Str } -[[g(4)]]-> ({} -[[13(13) Str]]-> Str)), thunk(9) (({} -[[14(14)]]-> Str)) (Str -[[f(3)]]-> ({} -[[11(11)]]-> Str))]]-> Str"#
print_only_under_alias: true
);
}
@ -7402,4 +7409,35 @@ mod solve_expr {
"###
);
}
#[test]
fn catchall_branch_for_pattern_not_last() {
infer_queries!(
indoc!(
r#"
\x -> when x is
#^
A B _ -> ""
A _ C -> ""
"#
),
@r#"x : [A [B]* [C]*]"#
allow_errors: true
);
}
#[test]
fn catchall_branch_walk_into_nested_types() {
infer_queries!(
indoc!(
r#"
\x -> when x is
#^
{ a: A { b: B } } -> ""
_ -> ""
"#
),
@r#"x : { a : [A { b : [B]* }*]* }*"#
)
}
}

View File

@ -838,26 +838,7 @@ fn unify_structure<M: MetaCollector>(
match other {
FlexVar(_) => {
// If the other is flex, Structure wins!
let outcome = merge(subs, ctx, Structure(*flat_type));
// And if we see a flex variable on the right hand side of a presence
// constraint, we know we need to open up the structure we're trying to unify with.
match (ctx.mode.is_present(), flat_type) {
(true, FlatType::TagUnion(tags, _ext)) => {
let new_ext = subs.fresh_unnamed_flex_var();
let mut new_desc = ctx.first_desc;
new_desc.content = Structure(FlatType::TagUnion(*tags, new_ext));
subs.set(ctx.first, new_desc);
}
(true, FlatType::FunctionOrTagUnion(tn, sym, _ext)) => {
let new_ext = subs.fresh_unnamed_flex_var();
let mut new_desc = ctx.first_desc;
new_desc.content = Structure(FlatType::FunctionOrTagUnion(*tn, *sym, new_ext));
subs.set(ctx.first, new_desc);
}
_ => {}
}
outcome
merge(subs, ctx, Structure(*flat_type))
}
FlexAbleVar(_, ability) => {
// Structure wins

View File

@ -7727,7 +7727,7 @@ All branches in an `if` must have the same type!
But all the previous branches match:
F [A]a
F [A]
"###
);
@ -9875,4 +9875,30 @@ All branches in an `if` must have the same type!
your code don't wonder why it is there.
"###
);
test_report!(
flip_flop_catch_all_branches_not_exhaustive,
indoc!(
r#"
\x -> when x is
A B _ -> ""
A _ C -> ""
"#
),
@r###"
UNSAFE PATTERN /code/proj/Main.roc
This `when` does not cover all the possibilities:
4> \x -> when x is
5> A B _ -> ""
6> A _ C -> ""
Other possibilities include:
A _ _
I would have to crash if I saw one of those! Add branches for them!
"###
);
}