Move exhaustiveness checking to type checking

This commit is contained in:
Ayaz Hafiz 2022-04-22 15:23:56 -04:00
parent f7e04490c0
commit 85e3373d8b
No known key found for this signature in database
GPG key ID: 0E2A37416A25EF58
15 changed files with 346 additions and 94 deletions

View file

@ -580,17 +580,18 @@ pub fn constrain_expr(
}
}
When {
cond_var,
cond_var: real_cond_var,
expr_var,
loc_cond,
branches,
branches_cond_var,
..
} => {
let cond_var = *cond_var;
let cond_type = Variable(cond_var);
let branches_cond_var = *branches_cond_var;
let branches_cond_type = Variable(branches_cond_var);
let branch_var = *expr_var;
let branch_type = Variable(branch_var);
let body_var = *expr_var;
let body_type = Variable(body_var);
let branches_region = {
debug_assert!(!branches.is_empty());
@ -615,13 +616,13 @@ pub fn constrain_expr(
index,
region: ann_source.region(),
},
branch_type.clone(),
body_type.clone(),
)
}
_ => ForReason(
Reason::WhenBranch { index },
branch_type.clone(),
body_type.clone(),
branch_region,
),
};
@ -659,7 +660,7 @@ pub fn constrain_expr(
index: HumanIndex::zero_based(index),
sub_pattern,
},
cond_type.clone(),
branches_cond_type.clone(),
sub_region,
)
};
@ -703,15 +704,16 @@ pub fn constrain_expr(
// After solving the condition variable with what's expected from the branch patterns,
// check it against the condition expression.
// TODO: when we have exhaustiveness checking during the typechecking phase, perform
// exhaustiveness checking when this expectation fails. That will produce better error
// messages.
let expr_con = constrain_expr(
//
// First, solve the condition type.
let real_cond_var = *real_cond_var;
let real_cond_type = Type::Variable(real_cond_var);
let cond_constraint = constrain_expr(
constraints,
env,
loc_cond.region,
&loc_cond.value,
Expected::ForReason(Reason::WhenBranches, cond_type, branches_region),
Expected::NoExpectation(real_cond_type),
);
// branch_cons.extend(pattern_cons);
// branch_constraints.push(constraints.and_constraint(pattern_cons));
@ -719,10 +721,18 @@ pub fn constrain_expr(
// total_cons.push(expr_con);
pattern_cons.push(expr_con);
let sketched_rows = sketch_rows(cond_var, branches_region, &branches);
let exhaustiveness_constraint =
constraints.exhaustive(sketched_rows, ExhaustiveContext::BadCase);
pattern_cons.push(exhaustiveness_constraint);
// Now check the condition against the type expected by the branches.
let sketched_rows = sketch_rows(real_cond_var, branches_region, &branches);
// let exhaustive_reason = Reason::Exhaustive(sketched_rows, ExhaustiveContext::BadCase);
let cond_matches_branches_constraint = constraints.exhaustive(
real_cond_var,
loc_cond.region,
loc_cond.value.category(),
Expected::ForReason(Reason::WhenBranches, branches_cond_type, branches_region),
sketched_rows,
ExhaustiveContext::BadCase,
);
pattern_cons.push(cond_matches_branches_constraint);
// Solve all the pattern constraints together, introducing variables in the pattern as
// need be before solving the bodies.
@ -742,7 +752,10 @@ pub fn constrain_expr(
let total_cons = [when_body_con, result_con];
let branch_constraints = constraints.and_constraint(total_cons);
constraints.exists([cond_var, *expr_var], branch_constraints)
constraints.exists(
[branches_cond_var, real_cond_var, *expr_var],
branch_constraints,
)
}
Access {
record_var,